case pos
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : p = 0
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ

case neg
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
by_cases hp0 : p = 0
case pos
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ

case neg
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
by_cases hp_top : p = ∞
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ⊤
hp1_real : 1 ≤ ENNReal.toReal p
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
have hp1_real : 1 ≤ p.toReal := by
  rwa [← ENNReal.one_toReal, ENNReal.toReal_le_toReal ENNReal.one_ne_top hp_top]
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ⊤
hp1_real : 1 ≤ ENNReal.toReal p
⊢ snorm' (f + g) (ENNReal.toReal p) μ ≤ snorm' f (ENNReal.toReal p) μ + snorm' g (ENNReal.toReal p) μ
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ⊤
hp1_real : 1 ≤ ENNReal.toReal p
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
repeat rw [snorm_eq_snorm' hp0 hp_top]
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ⊤
hp1_real : 1 ≤ ENNReal.toReal p
⊢ snorm' (f + g) (ENNReal.toReal p) μ ≤ snorm' f (ENNReal.toReal p) μ + snorm' g (ENNReal.toReal p) μ
exact snorm'_add_le hf hg hp1_real
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : p = 0
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
simp [hp0]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ snorm (f + g) p μ ≤ snorm f p μ + snorm g p μ
simp [hp_top, snormEssSup_add_le]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ 1 ≤ ENNReal.toReal p
rwa [← ENNReal.one_toReal, ENNReal.toReal_le_toReal ENNReal.one_ne_top hp_top]
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ⊤
hp1_real : 1 ≤ ENNReal.toReal p
⊢ snorm' (f + g) (ENNReal.toReal p) μ ≤ snorm' f (ENNReal.toReal p) μ + snorm' g (ENNReal.toReal p) μ
case neg
α : Type u_1
E : Type u_2
F : Type ?u.2940197
G : Type ?u.2940200
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 μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ⊤
hp1_real : 1 ≤ ENNReal.toReal p
⊢ snorm' (f + g) (ENNReal.toReal p) μ ≤ snorm' f (ENNReal.toReal p) μ + snorm' g (ENNReal.toReal p) μ
rw [snorm_eq_snorm' hp0 hp_top]