awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.SMul (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ
have inr : eLpNorm' f q μ ≤ eLpNorm' (c • f) q μ / ‖c‖ₑ
Tactic: refine le_antisymm (eLpNorm'_const_smul_le hq_pos) <| ENNReal.mul_le_of_le_div' ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.SMul (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
⊢ eLpNormEssSup (c • f) μ = ‖c‖ₑ * eLpNormEssSup f μ
have simp_rw : essSup (fun (x : α) ↦ ‖(c • f) x‖ₑ) μ = ‖c‖ₑ * essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
Tactic: simp_rw [eLpNormEssSup_eq_essSup_enorm, Pi.smul_apply, enorm_smul,
    ENNReal.essSup_const_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.SMul (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
simp_rw : essSup (fun (x : α) ↦ ‖(c • f) x‖ₑ) μ = ‖c‖ₑ * essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
⊢ eLpNormEssSup (c • f) μ = ‖c‖ₑ * eLpNormEssSup f μ
have simp_rw₁ : essSup (fun (x : α) ↦ ‖c • f x‖ₑ) μ = ‖c‖ₑ * essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
Tactic: simp_rw [eLpNormEssSup_eq_essSup_enorm, Pi.smul_apply, enorm_smul,
    ENNReal.essSup_const_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.SMul (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
simp_rw : essSup (fun (x : α) ↦ ‖(c • f) x‖ₑ) μ = ‖c‖ₑ * essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
simp_rw₁ : essSup (fun (x : α) ↦ ‖c • f x‖ₑ) μ = ‖c‖ₑ * essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
⊢ eLpNormEssSup (c • f) μ = ‖c‖ₑ * eLpNormEssSup f μ
have simp_rw₂ : essSup (fun (x : α) ↦ ‖c‖ₑ * ‖f x‖ₑ) μ = ‖c‖ₑ * essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
Tactic: simp_rw [eLpNormEssSup_eq_essSup_enorm, Pi.smul_apply, enorm_smul,
    ENNReal.essSup_const_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.SMul (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ
have inl : eLpNorm (HSMul.hSMul (α := 𝕜) 0 f) p μ = enorm.{u_3} (E := 𝕜) 0 * eLpNorm f p μ
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.SMul (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
inl : eLpNorm (HSMul.hSMul (α := 𝕜) 0 f) p μ = enorm.{u_3} (E := 𝕜) 0 * eLpNorm f p μ
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ
have inr : ∀ (hc : c ≠ 0), eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.SMul (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ
have inr : eLpNorm f p μ ≤ eLpNorm (c • f) p μ / ‖c‖ₑ
Tactic: refine le_antisymm eLpNorm_const_smul_le <| ENNReal.mul_le_of_le_div' ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
q : ℝ
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hq1 : 1 ≤ q
⊢ (∫⁻ (a : α), ‖(f + g) a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ^ q ∂μ) ^
      (1 / q)
have h₁ : ∀ (a : α), ‖(f + g) a‖ₑ ≤ HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a
Tactic: gcongr with a
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
q : ℝ
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hq0 : 0 ≤ q
hq1 : q ≤ 1
⊢ (∫⁻ (a : α), ‖(f + g) a‖ₑ ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ^ q ∂μ) ^
      (1 / q)
have h₁ : ∀ (a : α), ‖(f + g) a‖ₑ ≤ HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a
Tactic: gcongr with a
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
⊢ eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ
have refine : ∀ (x : α),
  (fun (x : α) ↦ ‖(f + g) x‖ₑ) x ≤
    HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
Tactic: refine le_trans (essSup_mono_ae (Eventually.of_forall fun x => ?_)) (ENNReal.essSup_add_le _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
x : α
⊢ (fun (x : α) ↦ ‖(f + g) x‖ₑ) x ≤
    HAdd.hAdd (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
have simp_rw : ‖f x + g x‖ₑ ≤ ‖f x‖ₑ + ‖g x‖ₑ
Tactic: simp_rw [Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
have pos : ∀ (hp0 : p = 0), eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
pos : ∀ (hp0 : p = 0), eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
have neg : ∀ (hp0 : ¬p = 0), eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
have pos : ∀ (hp_top : p = ∞), eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
have neg : ∀ (hp_top : ¬p = ∞), eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ 1 ≤ p.toReal
have rwa : ENNReal.toReal 1 ≤ p.toReal
Tactic: rwa [← ENNReal.toReal_one, ENNReal.toReal_le_toReal ENNReal.one_ne_top hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (hypothesis)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
have hp1_real : 1 ≤ p.toReal
Tactic: have hp1_real : 1 ≤ p.toReal := by
    rwa [← ENNReal.toReal_one, ENNReal.toReal_le_toReal ENNReal.one_ne_top hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
have neg : eLpNorm' (f + g) p.toReal μ ≤ eLpNorm f p μ + eLpNorm g p μ
Tactic: rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
⊢ eLpNorm' (f + g) p.toReal μ ≤ eLpNorm f p μ + eLpNorm g p μ
have neg : eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm g p μ
Tactic: rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
⊢ eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm g p μ
have neg : eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ
Tactic: rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
have neg : eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ
Tactic: repeat rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
have inl : eLpNorm (f + g) 0 μ ≤ LpAddConst 0 * (eLpNorm f 0 μ + eLpNorm g 0 μ)
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
inl : eLpNorm (f + g) 0 μ ≤ LpAddConst 0 * (eLpNorm f 0 μ + eLpNorm g 0 μ)
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
have inr : ∀ (hp : p ≠ 0), eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
have inr : ∀ (h'p : p < 1), eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
Tactic: rcases lt_or_ge p 1 with (h'p | h'p)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
inr : ∀ (h'p : p < 1), eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
have inr₁ : ∀ (h'p : 1 ≤ p), eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
Tactic: rcases lt_or_ge p 1 with (h'p | h'p)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
have inr : eLpNorm' (f + g) p.toReal μ ≤ p.LpAddConst * (eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ)
Tactic: simp only [eLpNorm_eq_eLpNorm' hp (h'p.trans ENNReal.one_lt_top).ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ eLpNorm' (f + g) p.toReal μ ≤ p.LpAddConst * (eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ)
have h : p.LpAddConst = HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1)
Tactic: convert! eLpNorm'_add_le_of_le_one hf ENNReal.toReal_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
h : p.LpAddConst = HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1)
⊢ eLpNorm' (f + g) p.toReal μ ≤ p.LpAddConst * (eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ)
have inr : p.toReal ≤ 1
Tactic: convert! eLpNorm'_add_le_of_le_one hf ENNReal.toReal_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (hypothesis)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ p.LpAddConst = HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1)
have this : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p
Tactic: have : p ∈ Set.Ioo (0 : ℝ≥0∞) 1 := ⟨hp.bot_lt, h'p⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (hypothesis)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
⊢ ∃ (η : ℝ≥0∞),
    0 < η ∧
      ∀ (f g : α → ε),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
have this : Tendsto (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 (p.LpAddConst * HAdd.hAdd (α := ℝ≥0∞) 0 0))
Tactic: have :
    Tendsto (fun η : ℝ≥0∞ => LpAddConst p * (η + η)) (𝓝[>] 0)
        (𝓝 (LpAddConst p * (0 + 0))) :=
    (ENNReal.Tendsto.const_mul (tendsto_id.add tendsto_id)
          (Or.inr (LpAddConst_lt_top p).ne)).mono_left
      nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (hypothesis)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 (p.LpAddConst * HAdd.hAdd (α := ℝ≥0∞) 0 0))
⊢ ∃ (η : ℝ≥0∞),
    0 < η ∧
      ∀ (f g : α → ε),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
have this₁ : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
Tactic: simp only [add_zero, mul_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
⊢ ∃ (η : ℝ≥0∞),
    0 < η ∧
      ∀ (f g : α → ε),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
have rcases : ∀ (η : ℝ≥0∞) (hη : p.LpAddConst * (η + η) < δ) (ηpos : 0 < η),
  ∃ (η : ℝ≥0∞),
    0 < η ∧
      ∀ (f g : α → ε),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
Tactic: rcases (((tendsto_order.1 this).2 δ hδ.bot_lt).and self_mem_nhdsWithin).exists with ⟨η, hη, ηpos⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : p.LpAddConst * (η + η) < δ
ηpos : 0 < η
⊢ ∃ (η : ℝ≥0∞),
    0 < η ∧
      ∀ (f g : α → ε),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
have refine : ∀ (f g : α → ε) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (Hf : eLpNorm f p μ ≤ η)
  (Hg : eLpNorm g p μ ≤ η), eLpNorm (f + g) p μ < δ
Tactic: refine ⟨η, ηpos, fun f g hf hg Hf Hg => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : p.LpAddConst * (η + η) < δ
ηpos : 0 < η
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
Hf : eLpNorm f p μ ≤ η
Hg : eLpNorm g p μ ≤ η
⊢ eLpNorm (f + g) p μ < δ
have eLpNorm : p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ) ≤ p.LpAddConst * (η + η)
Tactic: calc
    eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ) :=
      eLpNorm_add_le' hf hg p
    _ ≤ LpAddConst p * (η + η) := by gcongr
    _ < δ := hη
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : MemLp f p μ
hg : MemLp g p μ
⊢ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ) < ∞
have apply : eLpNorm f p μ + eLpNorm g p μ < ∞
Tactic: apply ENNReal.mul_lt_top (LpAddConst_lt_top p)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ MemLp (f - g) p μ
have rw : MemLp (f + -g) p μ
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, MemLp (f i) p μ
⊢ MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
have haveI : ∀ (this : DecidableEq ι), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
Tactic: haveI : DecidableEq ι := Classical.decEq _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, MemLp (f i) p μ
this : DecidableEq ι
⊢ MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
have revert : ∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
Tactic: revert hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
this : DecidableEq ι
⊢ ∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
have refine_1 : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) p μ),
  MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ ∅, f i a) p μ
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
this : DecidableEq ι
refine_1 :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) p μ),
    MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ ∅, f i a) p μ
⊢ ∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ) →
      ∀ (hf : ∀ i ∈ insert a s, MemLp (f i) p μ),
        MemLp.{u_1, u_4} (ε := ε') (fun (a_3 : α) ↦ ∑ i ∈ insert a s, f i a_3) p μ
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (goal)
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s_1 : Finset ι
f : ι → α → ε'
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
hf : ∀ i_1 ∈ insert i s, MemLp (f i_1) p μ
⊢ MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ insert i s, f i a) p μ
have refine_2 : MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ f i a + ∑ i ∈ s, f i a) p μ
Tactic: simp only [his, Finset.sum_insert, not_false_iff]