case pos
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
hp0 : p = 0
⊢ snorm f p ν ≤ snorm f p μ

case neg
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
hp0 : ¬p = 0
⊢ snorm f p ν ≤ snorm f p μ
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
⊢ snorm f p ν ≤ snorm f p μ
by_cases hp0 : p = 0
case pos
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ snorm f p ν ≤ snorm f p μ

case neg
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm f p ν ≤ snorm f p μ
case neg
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
hp0 : ¬p = 0
⊢ snorm f p ν ≤ snorm f p μ
by_cases hp_top : p = ∞
case neg
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm' f (ENNReal.toReal p) ν ≤ snorm' f (ENNReal.toReal p) μ
case neg
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm f p ν ≤ snorm f p μ
simp_rw [snorm_eq_snorm' hp0 hp_top]
no goals
case neg
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm' f (ENNReal.toReal p) ν ≤ snorm' f (ENNReal.toReal p) μ
exact snorm'_mono_measure f hμν ENNReal.toReal_nonneg
no goals
case pos
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
hp0 : p = 0
⊢ snorm f p ν ≤ snorm f p μ
simp [hp0]
no goals
case pos
α : Type u_1
E : Type ?u.1987947
F : Type u_2
G : Type ?u.1987953
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ snorm f p ν ≤ snorm f p μ
simp [hp_top, snormEssSup_mono_measure f (Measure.absolutelyContinuous_of_le hμν)]