awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm (-f) p μ = lpNorm f p μ
neg : ∀ (hf : ¬AEStronglyMeasurable f μ), lpNorm (-f) p μ = lpNorm f p μ
⊢ lpNorm (-f) p μ = lpNorm f p μ

Tactic:
by_cases hf : AEStronglyMeasurable f μ

Premises used: MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ lpNorm (-f) p μ = lpNorm f p μ

Tactic:
simp [← toReal_eLpNorm, hf, hf.neg]

Premises used: MeasureTheory.toReal_eLpNorm, MeasureTheory.AEStronglyMeasurable.neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable (-f) μ
⊢ AEStronglyMeasurable f μ

Tactic:
simpa using h.neg

Premises used: MeasureTheory.AEStronglyMeasurable.neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
neg : lpNorm (-f) p μ = 0
neg₁ neg₂ : Eq (α := ℝ) 0 0
⊢ lpNorm (-f) p μ = lpNorm f p μ

Tactic:
rw [lpNorm_of_not_aestronglyMeasurable hf,
      lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by simpa using h.neg]

Premises used: MeasureTheory.lpNorm_of_not_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm.{u_1, u_2} (E := E) (fun (x : α) ↦ -f x) p μ = lpNorm f p μ

Tactic:
lpNorm_neg ..

Premises used: MeasureTheory.lpNorm_neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f g : α → E
p : ℝ≥0∞
μ : Measure α
rw : lpNorm (-(f - g)) p μ = lpNorm (g - f) p μ
⊢ lpNorm (f - g) p μ = lpNorm (g - f) p μ

Tactic:
rw [← lpNorm_neg]

Premises used: MeasureTheory.lpNorm_neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
f g : α → E
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (-(f - g)) p μ = lpNorm (g - f) p μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ ‖f x‖) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
rw : (eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ).toReal = (eLpNorm f p μ).toReal
⊢ lpNorm (E := ℝ) (fun (x : α) ↦ ‖f x‖) p μ = lpNorm f p μ

Tactic:
rw [← toReal_eLpNorm hf, ← toReal_eLpNorm (by fun_prop)]

Premises used: MeasureTheory.toReal_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
⊢ (eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ).toReal = (eLpNorm f p μ).toReal

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
⊢ lpNorm |f| p μ = lpNorm f p μ

Tactic:
lpNorm_norm hf p

Premises used: abs, MeasureTheory.lpNorm_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
⊢ lpNorm (E := ℝ) (fun (x : α) ↦ |f x|) p μ = lpNorm f p μ

Tactic:
lpNorm_abs hf _

Premises used: abs, MeasureTheory.lpNorm_abs
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ 0
hμ : μ ≠ 0
c : E
⊢ lpNorm.{u_1, u_2} (E := E) (fun (_x : α) ↦ c) p μ = ‖c‖ * μ.real Set.univ ^ p.toReal⁻¹

Tactic:
simp [lpNorm, eLpNorm_const c hp hμ, Measure.real, ENNReal.toReal_rpow,
    aestronglyMeasurable_const]

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.Measure.real, MeasureTheory.eLpNorm_const, ENNReal.toReal_rpow, MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp₀ : p ≠ 0
hp : p ≠ ∞
c : E
⊢ lpNorm.{u_1, u_2} (E := E) (fun (_x : α) ↦ c) p μ = ‖c‖ * μ.real Set.univ ^ p.toReal⁻¹

Tactic:
simp [lpNorm, eLpNorm_const' c hp₀ hp, Measure.real, ENNReal.toReal_rpow,
    aestronglyMeasurable_const]

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.Measure.real, MeasureTheory.eLpNorm_const', ENNReal.toReal_rpow, MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_3
inst : NormedField 𝕜
hp : p ≠ 0
hμ : μ ≠ 0
⊢ lpNorm.{u_1, u_3} (E := 𝕜) 1 p μ = μ.real Set.univ ^ p.toReal⁻¹

Tactic:
simp [Pi.one_def, lpNorm_const hp hμ, Measure.real, ENNReal.toReal_rpow]

Premises used: MeasureTheory.Measure.real, Pi.one_def, ENNReal.toReal_rpow, MeasureTheory.lpNorm_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
𝕜 : Type u_3
inst : NormedField 𝕜
hp₀ : p ≠ 0
hp : p ≠ ∞
μ : Measure α
⊢ lpNorm.{u_1, u_3} (E := 𝕜) 1 p μ = μ.real Set.univ ^ p.toReal⁻¹

Tactic:
simp [Pi.one_def, lpNorm_const' hp₀ hp, Measure.real, ENNReal.toReal_rpow]

Premises used: MeasureTheory.Measure.real, Pi.one_def, ENNReal.toReal_rpow, MeasureTheory.lpNorm_const'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
neg : ∀ (hf : ¬AEStronglyMeasurable f μ), lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
⊢ lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ

Tactic:
by_cases hf : AEStronglyMeasurable f μ

Premises used: MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ

Tactic:
simp [lpNorm, eLpNorm_const_smul, hf, hf.const_smul]

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul, MeasureTheory.eLpNorm_const_smul, MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
neg : lpNorm (HSMul.hSMul (α := 𝕜) 0 f) p μ = (↑(nnnorm.{u_3} (E := 𝕜) 0) : ℝ) * lpNorm f p μ
neg₁ : ∀ (hc : c ≠ 0), lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ
⊢ lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
f : α → E
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm (HSMul.hSMul (α := 𝕜) 0 f) p μ = (↑(nnnorm.{u_3} (E := 𝕜) 0) : ℝ) * lpNorm f p μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
hc : c ≠ 0
h : AEStronglyMeasurable (c • f) μ
⊢ AEStronglyMeasurable f μ

Tactic:
simpa [hc] using h.const_smul c⁻¹

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul, Inv.inv
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
hc : c ≠ 0
neg : 0 = (↑‖c‖₊ : ℝ) * 0
⊢ lpNorm (c • f) p μ = (↑‖c‖₊ : ℝ) * lpNorm f p μ

Tactic:
rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by
    simpa [hc] using h.const_smul c⁻¹]

Premises used: MeasureTheory.lpNorm_of_not_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
f : α → E
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
hc : c ≠ 0
⊢ 0 = (↑‖c‖₊ : ℝ) * 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
f : α → E
μ : Measure α
⊢ lpNorm (n • f) p μ = n • lpNorm f p μ

Tactic:
simpa [Nat.cast_smul_eq_nsmul] using lpNorm_const_smul (n : ℝ) f μ (p := p)

Premises used: Nat.cast, MeasureTheory.lpNorm_const_smul, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
n : ℕ
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm ((↑n : α → 𝕜) * f) p μ = (↑n : ℝ) * lpNorm f p μ

Tactic:
simpa only [nsmul_eq_mul] using lpNorm_nsmul n f μ

Premises used: MeasureTheory.lpNorm_nsmul, nsmul_eq_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
n : ℕ
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm.{u_1, u_3} (E := 𝕜) (fun (x : α) ↦ (↑n : 𝕜) * f x) p μ = (↑n : ℝ) * lpNorm f p μ

Tactic:
lpNorm_natCast_mul ..

Premises used: MeasureTheory.lpNorm_natCast_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
f : α → 𝕜
n : ℕ
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (f * (↑n : α → 𝕜)) p μ = lpNorm f p μ * (↑n : ℝ)

Tactic:
simpa only [mul_comm] using lpNorm_natCast_mul n f p μ

Premises used: mul_comm, MeasureTheory.lpNorm_natCast_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
f : α → 𝕜
n : ℕ
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm.{u_1, u_3} (E := 𝕜) (fun (x : α) ↦ f x * (↑n : 𝕜)) p μ = lpNorm f p μ * (↑n : ℝ)

Tactic:
lpNorm_mul_natCast ..

Premises used: MeasureTheory.lpNorm_mul_natCast
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : CharZero 𝕜
n : ℕ
hn : n ≠ 0
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : CharZero 𝕜
n : ℕ
hn : n ≠ 0
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
rw : lpNorm (f / (↑n : α → 𝕜) * (↑n : α → 𝕜)) p μ = lpNorm f p μ
⊢ lpNorm (f / (↑n : α → 𝕜)) p μ = lpNorm f p μ / (↑n : ℝ)

Tactic:
rw [eq_div_iff (by positivity), ← lpNorm_mul_natCast]

Premises used: MeasureTheory.lpNorm_mul_natCast, eq_div_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : CharZero 𝕜
n : ℕ
hn : n ≠ 0
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm (f / (↑n : α → 𝕜) * (↑n : α → 𝕜)) p μ = lpNorm f p μ

Tactic:
simp [Pi.mul_def, hn]

Premises used: Pi.mul_def
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : CharZero 𝕜
n : ℕ
hn : n ≠ 0
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm.{u_1, u_3} (E := 𝕜) (fun (x : α) ↦ f x / (↑n : 𝕜)) p μ = lpNorm f p μ / (↑n : ℝ)

Tactic:
lpNorm_div_natCast hn ..

Premises used: MeasureTheory.lpNorm_div_natCast
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
pos : ∀ (hg : MemLp g p μ), lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ
neg : ∀ (hg : ¬MemLp g p μ), lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ

Tactic:
by_cases hg : MemLp g p μ

Premises used: MeasureTheory.MemLp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : MemLp g p μ
pos : (eLpNorm (f + g) p μ).toReal ≤ (eLpNorm f p μ + eLpNorm g p μ).toReal
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ

Tactic:
rw [← toReal_eLpNorm (hf.add hg).aestronglyMeasurable,
      ← toReal_eLpNorm hf.aestronglyMeasurable, ← toReal_eLpNorm hg.aestronglyMeasurable,
      ← ENNReal.toReal_add hf.eLpNorm_ne_top hg.eLpNorm_ne_top]

Premises used: ENNReal.toReal_add, MeasureTheory.toReal_eLpNorm, MeasureTheory.MemLp.add, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.MemLp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : MemLp g p μ
pos : eLpNorm f p μ + eLpNorm g p μ ≠ ∞
pos₁ : eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
⊢ (eLpNorm (f + g) p μ).toReal ≤ (eLpNorm f p μ + eLpNorm g p μ).toReal

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : MemLp g p μ
⊢ eLpNorm f p μ + eLpNorm g p μ ≠ ∞

Tactic:
ENNReal.add_ne_top.2 ⟨hf.eLpNorm_ne_top, hg.eLpNorm_ne_top⟩

Premises used: Iff.mpr, And.intro, ENNReal.add_ne_top, MeasureTheory.MemLp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : MemLp g p μ
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
eLpNorm_add_le hf.aestronglyMeasurable hg.aestronglyMeasurable hp

Premises used: MeasureTheory.eLpNorm_add_le, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : MemLp g p μ
⊢ eLpNorm f p μ + eLpNorm g p μ ≠ ∞

Tactic:
exacts [ENNReal.add_ne_top.2 ⟨hf.eLpNorm_ne_top, hg.eLpNorm_ne_top⟩,
      eLpNorm_add_le hf.aestronglyMeasurable hg.aestronglyMeasurable hp]

Premises used: Iff.mpr, And.intro, MeasureTheory.eLpNorm_add_le, MeasureTheory.MemLp.aestronglyMeasurable, ENNReal.add_ne_top, MeasureTheory.MemLp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : ¬MemLp g p μ
hfg : MemLp (f + g) p μ
⊢ MemLp g p μ

Tactic:
simpa using hfg.sub hf

Premises used: MeasureTheory.MemLp.sub
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : ¬MemLp g p μ
neg : 0 ≤ lpNorm f p μ + 0
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ

Tactic:
rw [lpNorm_of_not_memLp fun hfg ↦ hg <| by simpa using hfg.sub hf, lpNorm_of_not_memLp hg]

Premises used: MeasureTheory.lpNorm_of_not_memLp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : ¬MemLp g p μ
⊢ 0 ≤ lpNorm f p μ + 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ

Tactic:
simpa [add_comm] using lpNorm_add_le hg (g := f) hp

Premises used: MeasureTheory.lpNorm_add_le, add_comm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
⊢ lpNorm (f - g) p μ ≤ lpNorm f p μ + lpNorm g p μ

Tactic:
simpa [sub_eq_add_neg] using lpNorm_add_le hf (g := -g) hp

Premises used: MeasureTheory.lpNorm_add_le, sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm g p μ + lpNorm (f - g) p μ

Tactic:
simpa using lpNorm_add_le hg (g := f - g) hp

Premises used: MeasureTheory.lpNorm_add_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm g p μ + lpNorm (g - f) p μ

Tactic:
simpa [neg_add_eq_sub] using lpNorm_add_le hg.neg (g := g - f) hp

Premises used: neg_add_eq_sub, MeasureTheory.lpNorm_add_le, MeasureTheory.MemLp.neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm (f + g) p μ + lpNorm g p μ

Tactic:
simpa using lpNorm_add_le' (f := f + g) hg.neg hp

Premises used: MeasureTheory.lpNorm_add_le', MeasureTheory.MemLp.neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g h : α → E
hf : MemLp f p μ
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm (f - h) p μ ≤ lpNorm (f - g) p μ + lpNorm (g - h) p μ

Tactic:
simpa using lpNorm_add_le (hf.sub hg) (g := g - h) hp

Premises used: MeasureTheory.lpNorm_add_le, MeasureTheory.MemLp.sub
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
rw : (eLpNorm.{u_1, u_2} (ε := E) (∑ i ∈ s, f i) p μ).toReal ≤ ENNReal.toReal (∑ a ∈ s, eLpNorm (f a) p μ)
⊢ lpNorm.{u_1, u_2} (E := E) (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, lpNorm (f i) p μ

Tactic:
rw [← Finset.sum_congr rfl fun i hi ↦ toReal_eLpNorm (hf i hi).aestronglyMeasurable,
    ← ENNReal.toReal_sum fun i hi ↦ (hf i hi).2.ne,
    ← toReal_eLpNorm (Finset.aestronglyMeasurable_sum _ fun i hi ↦ (hf i hi).aestronglyMeasurable)]

Premises used: MeasureTheory.toReal_eLpNorm, And.right, Finset.aestronglyMeasurable_sum, ENNReal.toReal_sum, MeasureTheory.MemLp.aestronglyMeasurable, Finset.sum_congr, rfl, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
h₁ : Ne (α := ℝ≥0∞) (∑ i ∈ s, eLpNorm (f i) p μ) ∞
⊢ (eLpNorm.{u_1, u_2} (ε := E) (∑ i ∈ s, f i) p μ).toReal ≤ ENNReal.toReal (∑ a ∈ s, eLpNorm (f a) p μ)

Tactic:
grw [eLpNorm_sum_le (fun i hi ↦ (hf _ hi).aestronglyMeasurable) hp]

Premises used: MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.eLpNorm_sum_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
⊢ Ne (α := ℝ≥0∞) (∑ i ∈ s, eLpNorm (f i) p μ) ∞

Tactic:
simpa using fun i hi ↦ (hf i hi).2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
inl :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) p μ),
    lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ ∅, f i) p μ ≤ 𝔼 i ∈ ∅, lpNorm (f i) p μ
inr : ∀ (hs : s.Nonempty), lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ ≤ 𝔼 i ∈ s, lpNorm (f i) p μ
⊢ lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ ≤ 𝔼 i ∈ s, lpNorm (f i) p μ

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
f : ι → α → E
hp : 1 ≤ p
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) p μ
⊢ lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ ∅, f i) p μ ≤ 𝔼 i ∈ ∅, lpNorm (f i) p μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
⊢ LT.lt (α := ℚ≥0) 0 (↑s.card : ℚ≥0)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
inr :
  HSMul.hSMul (α := ℚ≥0) (↑s.card : ℚ≥0) (lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ) ≤
    ∑ i ∈ s, (fun (i : ι) ↦ lpNorm (f i) p μ) i
⊢ lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ ≤ 𝔼 i ∈ s, lpNorm (f i) p μ

Tactic:
refine (le_inv_smul_iff_of_pos <| by positivity).2 ?_

Premises used: Iff.mpr, le_inv_smul_iff_of_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : Module ℚ≥0 E
inst_2 : NormedSpace ℝ E
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
hp : 1 ≤ p
hs : s.Nonempty
inr : lpNorm.{u_1, u_2} (E := E) (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, (fun (i : ι) ↦ lpNorm (f i) p μ) i
⊢ HSMul.hSMul (α := ℚ≥0) (↑s.card : ℚ≥0) (lpNorm.{u_1, u_2} (E := E) (𝔼 i ∈ s, f i) p μ) ≤
    ∑ i ∈ s, (fun (i : ι) ↦ lpNorm (f i) p μ) i

Tactic:
rw [Nat.cast_smul_eq_nsmul, ← lpNorm_nsmul, Finset.card_smul_expect]

Premises used: Finset.card_smul_expect, MeasureTheory.lpNorm_nsmul, Nat.cast_smul_eq_nsmul