case inl
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ snorm (f + g) 0 μ ≤ LpAddConst 0 * (snorm f 0 μ + snorm g 0 μ)

case inr
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
⊢ snorm (f + g) p μ ≤ LpAddConst p * (snorm f p μ + snorm g p μ)
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ snorm (f + g) p μ ≤ LpAddConst p * (snorm f p μ + snorm g p μ)
rcases eq_or_ne p 0 with (rfl | hp)
case inr.inl
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ snorm (f + g) p μ ≤ LpAddConst p * (snorm f p μ + snorm g p μ)

case inr.inr
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : 1 ≤ p
⊢ snorm (f + g) p μ ≤ LpAddConst p * (snorm f p μ + snorm g p μ)
case inr
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
⊢ snorm (f + g) p μ ≤ LpAddConst p * (snorm f p μ + snorm g p μ)
rcases lt_or_le p 1 with (h'p | h'p)
no goals
case inl
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ snorm (f + g) 0 μ ≤ LpAddConst 0 * (snorm f 0 μ + snorm g 0 μ)
simp only [snorm_exponent_zero, add_zero, MulZeroClass.mul_zero, le_zero_iff]
case inr.inl
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ snorm' (f + g) (ENNReal.toReal p) μ ≤ LpAddConst p * (snorm' f (ENNReal.toReal p) μ + snorm' g (ENNReal.toReal p) μ)
case inr.inl
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ snorm (f + g) p μ ≤ LpAddConst p * (snorm f p μ + snorm g p μ)
simp only [snorm_eq_snorm' hp (h'p.trans ENNReal.one_lt_top).ne]
case h.e'_4.h.e'_5
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ LpAddConst p = 2 ^ (1 / ENNReal.toReal p - 1)

case inr.inl.convert_3
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ ENNReal.toReal p ≤ 1
case inr.inl
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ snorm' (f + g) (ENNReal.toReal p) μ ≤ LpAddConst p * (snorm' f (ENNReal.toReal p) μ + snorm' g (ENNReal.toReal p) μ)
convert snorm'_add_le_of_le_one hf ENNReal.toReal_nonneg _
case h.e'_4.h.e'_5
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
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 / ENNReal.toReal p - 1)
case h.e'_4.h.e'_5
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ LpAddConst p = 2 ^ (1 / ENNReal.toReal p - 1)
have : p ∈ Set.Ioo (0 : ℝ≥0∞) 1 := ⟨hp.bot_lt, h'p⟩
no goals
case h.e'_4.h.e'_5
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
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 / ENNReal.toReal p - 1)
simp only [LpAddConst, if_pos this]
no goals
case inr.inl.convert_3
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ ENNReal.toReal p ≤ 1
simpa using ENNReal.toReal_mono ENNReal.one_ne_top h'p.le
case inr.inr
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : 1 ≤ p
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
case inr.inr
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : 1 ≤ p
⊢ snorm (f + g) p μ ≤ LpAddConst p * (snorm f p μ + snorm g p μ)
simp [LpAddConst_of_one_le h'p]
no goals
case inr.inr
α : Type u_1
E : Type u_2
F : Type ?u.3024839
G : Type ?u.3024842
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : 1 ≤ p
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
exact snorm_add_le hf hg h'p