-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem eLpNorm_add_le' (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
    (p : ℝ≥0∞) : eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

Proof state:
case h.e'_4.h.e'_5
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ LpAddConst p = 2 ^ (1 / p.toReal - 1)

Tactic:
have : p ∈ Set.Ioo (0 : ℝ≥0∞) 1 := ⟨hp.bot_lt, h'p⟩

Result:
case h.e'_4.h.e'_5
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
this : p ∈ Set.Ioo 0 1
⊢ LpAddConst p = 2 ^ (1 / p.toReal - 1)

Proof state:
case inr.inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
simp only [eLpNorm_eq_eLpNorm' hp (h'p.trans ENNReal.one_lt_top).ne]

Result:
case inr.inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ eLpNorm' (f + g) p.toReal μ ≤ LpAddConst p * (eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ)

Proof state:
case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
⊢ eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
rcases lt_or_le p 1 with (h'p | h'p)

Result:
case inr.inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

case inr.inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : 1 ≤ p
⊢ eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

Proof state:
case inr.inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ eLpNorm' (f + g) p.toReal μ ≤ LpAddConst p * (eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ)

Tactic:
convert eLpNorm'_add_le_of_le_one hf ENNReal.toReal_nonneg _

Result:
case h.e'_4.h.e'_5
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ LpAddConst p = 2 ^ (1 / p.toReal - 1)

case inr.inl.convert_3
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ p.toReal ≤ 1

Proof state:
case inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ eLpNorm (f + g) 0 μ ≤ LpAddConst 0 * (eLpNorm f 0 μ + eLpNorm g 0 μ)

Tactic:
simp only [eLpNorm_exponent_zero, add_zero, mul_zero, le_zero_iff]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Result:
case inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ eLpNorm (f + g) 0 μ ≤ LpAddConst 0 * (eLpNorm f 0 μ + eLpNorm g 0 μ)

case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
⊢ eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

Proof state:
case inr.inl.convert_3
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ p.toReal ≤ 1

Tactic:
simpa using ENNReal.toReal_mono ENNReal.one_ne_top h'p.le

Result:
no goals

Proof state:
case h.e'_4.h.e'_5
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
this : p ∈ Set.Ioo 0 1
⊢ LpAddConst p = 2 ^ (1 / p.toReal - 1)

Tactic:
simp only [LpAddConst, if_pos this]

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : 1 ≤ p
⊢ eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
simpa [LpAddConst_of_one_le h'p] using eLpNorm_add_le hf hg h'p

Result:
no goals