awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
η : ℝ≥0
hη_pos : 0 < η
hη_le : ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞)
inr : ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤ ε
inr₁ :
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal)
⊢ eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
have inr₂ : ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal)
Tactic: grw [eLpNorm_indicator_const_le, ← hη_le, hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
⊢ MemLp f p μ
have this : MemLp f ∞ μ
Tactic: have := memLp_top_of_bound h2f C hfC
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ≥0∞
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ₑ ≤ C
hC : C ≠ ∞
⊢ MemLp f p μ
have this : MemLp f ∞ μ
Tactic: have : MemLp f ∞ μ :=
    ⟨h2f, eLpNormEssSup_le_of_ae_enorm_bound hfC |>.trans_lt hC.lt_top⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
⊢ MemLp f p μ
have this : MemLp f ∞ μ
Tactic: have := hf.memLp_top_of_hasCompactSupport h'f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c c' : E
⊢ HAdd.hAdd (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := s) p hs hμs c') =
    indicatorConstLp (s := s) p hs hμs (c + c')
have simp_rw : MemLp.toLp (HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (s.indicator fun (x : α) ↦ c')) sorry =
  MemLp.toLp (fun (a : α) ↦ HAdd.hAdd (α := E) (s.indicator (fun (x : α) ↦ c) a) (s.indicator (fun (x : α) ↦ c') a)) sorry
Tactic: simp_rw [indicatorConstLp, ← MemLp.toLp_add, indicator_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c c' : E
⊢ HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := s) p hs hμs c') =
    indicatorConstLp (s := s) p hs hμs (c - c')
have simp_rw : MemLp.toLp (HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (s.indicator fun (x : α) ↦ c')) sorry =
  MemLp.toLp (fun (a : α) ↦ HSub.hSub (α := E) (s.indicator (fun (x : α) ↦ c) a) (s.indicator (fun (x : α) ↦ c') a)) sorry
Tactic: simp_rw [indicatorConstLp, ← MemLp.toLp_sub, indicator_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
have rw : (eLpNorm (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) p μ).toReal = ‖c‖ * μ.real s ^ (1 / p.toReal)
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const hs hp_ne_zero hp_ne_top, ENNReal.toReal_mul, measureReal_def,
    ENNReal.toReal_rpow, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
rw :
  (eLpNorm (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) p μ).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
have rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal = ‖c‖ * μ.real s ^ (1 / p.toReal)
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const hs hp_ne_zero hp_ne_top, ENNReal.toReal_mul, measureReal_def,
    ENNReal.toReal_rpow, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
rw :
  (eLpNorm (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) p μ).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal = ‖c‖ * μ.real s ^ (1 / p.toReal)
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
have rw₂ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * μ.real s ^ (1 / p.toReal)
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const hs hp_ne_zero hp_ne_top, ENNReal.toReal_mul, measureReal_def,
    ENNReal.toReal_rpow, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
rw :
  (eLpNorm (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) p μ).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal = ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₂ :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
have rw₃ : ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * μ.real s ^ (1 / p.toReal)
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const hs hp_ne_zero hp_ne_top, ENNReal.toReal_mul, measureReal_def,
    ENNReal.toReal_rpow, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
rw :
  (eLpNorm (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) p μ).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal = ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₂ :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₃ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
have rw₄ : ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) ^ (1 / p.toReal)
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const hs hp_ne_zero hp_ne_top, ENNReal.toReal_mul, measureReal_def,
    ENNReal.toReal_rpow, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
rw :
  (eLpNorm (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) p μ).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal = ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₂ :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₃ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₄ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) ^ (1 / p.toReal)
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
have rw₅ : ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const hs hp_ne_zero hp_ne_top, ENNReal.toReal_mul, measureReal_def,
    ENNReal.toReal_rpow, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
rw :
  (eLpNorm (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) p μ).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal = ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₂ :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₃ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₄ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) ^ (1 / p.toReal)
rw₅ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
have rw₆ : ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const hs hp_ne_zero hp_ne_top, ENNReal.toReal_mul, measureReal_def,
    ENNReal.toReal_rpow, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hμs_ne_zero : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖
have rw : (eLpNorm (↑(↑(indicatorConstLp (s := s) ∞ hs hμs c) : α →ₘ[μ] E) : α → E) ∞ μ).toReal = ‖c‖
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.toReal_top,
    _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hμs_ne_zero : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : (eLpNorm (↑(↑(indicatorConstLp (s := s) ∞ hs hμs c) : α →ₘ[μ] E) : α → E) ∞ μ).toReal = ‖c‖
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖
have rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) ∞ μ).toReal = ‖c‖
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.toReal_top,
    _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hμs_ne_zero : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : (eLpNorm (↑(↑(indicatorConstLp (s := s) ∞ hs hμs c) : α →ₘ[μ] E) : α → E) ∞ μ).toReal = ‖c‖
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) ∞ μ).toReal = ‖c‖
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖
have rw₂ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal ∞)).toReal = ‖c‖
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.toReal_top,
    _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hμs_ne_zero : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : (eLpNorm (↑(↑(indicatorConstLp (s := s) ∞ hs hμs c) : α →ₘ[μ] E) : α → E) ∞ μ).toReal = ‖c‖
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) ∞ μ).toReal = ‖c‖
rw₂ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal ∞)).toReal = ‖c‖
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖
have rw₃ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / 0)).toReal = ‖c‖
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.toReal_top,
    _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hμs_ne_zero : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : (eLpNorm (↑(↑(indicatorConstLp (s := s) ∞ hs hμs c) : α →ₘ[μ] E) : α → E) ∞ μ).toReal = ‖c‖
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) ∞ μ).toReal = ‖c‖
rw₂ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal ∞)).toReal = ‖c‖
rw₃ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / 0)).toReal = ‖c‖
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖
have rw₄ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) 0).toReal = ‖c‖
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.toReal_top,
    _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hμs_ne_zero : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : (eLpNorm (↑(↑(indicatorConstLp (s := s) ∞ hs hμs c) : α →ₘ[μ] E) : α → E) ∞ μ).toReal = ‖c‖
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) ∞ μ).toReal = ‖c‖
rw₂ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal ∞)).toReal = ‖c‖
rw₃ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / 0)).toReal = ‖c‖
rw₄ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) 0).toReal = ‖c‖
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖
have rw₅ : (‖c‖ₑ * 1).toReal = ‖c‖
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.toReal_top,
    _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hμs_ne_zero : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : (eLpNorm (↑(↑(indicatorConstLp (s := s) ∞ hs hμs c) : α →ₘ[μ] E) : α → E) ∞ μ).toReal = ‖c‖
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) ∞ μ).toReal = ‖c‖
rw₂ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal ∞)).toReal = ‖c‖
rw₃ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / 0)).toReal = ‖c‖
rw₄ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) 0).toReal = ‖c‖
rw₅ : (‖c‖ₑ * 1).toReal = ‖c‖
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖
have rw₆ : ‖c‖ₑ.toReal = ‖c‖
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.toReal_top,
    _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hμs_ne_zero : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : (eLpNorm (↑(↑(indicatorConstLp (s := s) ∞ hs hμs c) : α →ₘ[μ] E) : α → E) ∞ μ).toReal = ‖c‖
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) ∞ μ).toReal = ‖c‖
rw₂ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal ∞)).toReal = ‖c‖
rw₃ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / 0)).toReal = ‖c‖
rw₄ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) 0).toReal = ‖c‖
rw₅ : (‖c‖ₑ * 1).toReal = ‖c‖
rw₆ : ‖c‖ₑ.toReal = ‖c‖
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖
have rw₇ : ‖c‖ = ‖c‖
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.toReal_top,
    _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_pos : p ≠ 0
hμs_pos : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
have pos : ∀ (hp_top : p = ∞), norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_pos : p ≠ 0
hμs_pos : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (hp_top : p = ∞), norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
have neg : ∀ (hp_top : ¬p = ∞), norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_pos : p ≠ 0
hμs_pos : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hp_top : p = ∞
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
have pos : norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖
Tactic: rw [hp_top, ENNReal.toReal_top, _root_.div_zero, Real.rpow_zero, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)
have rw : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)
Tactic: rw [indicatorConstLp, Lp.norm_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)
have refine : eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ENNReal.ofReal (‖c‖ * μ.real s ^ (1 / p.toReal))
Tactic: refine ENNReal.toReal_le_of_le_ofReal (by positivity) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ENNReal.ofReal (‖c‖ * μ.real s ^ (1 / p.toReal))
have refine : ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) =
  ENNReal.ofReal (‖c‖ * μ.real s ^ (1 / p.toReal))
Tactic: refine (eLpNorm_indicator_const_le _ _).trans_eq ?_