case hq0_lt
α : Type u_1
E : Type ?u.755518
F : Type u_2
G : Type ?u.755524
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hfp : snorm f p μ < ⊤
⊢ 0 < ENNReal.toReal p

case hfq
α : Type u_1
E : Type ?u.755518
F : Type u_2
G : Type ?u.755524
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hfp : snorm f p μ < ⊤
⊢ snorm' (fun a => f a) (ENNReal.toReal p) μ < ⊤
α : Type u_1
E : Type ?u.755518
F : Type u_2
G : Type ?u.755524
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hfp : snorm f p μ < ⊤
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) < ⊤
apply lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top
no goals
case hq0_lt
α : Type u_1
E : Type ?u.755518
F : Type u_2
G : Type ?u.755524
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hfp : snorm f p μ < ⊤
⊢ 0 < ENNReal.toReal p
exact ENNReal.toReal_pos hp_ne_zero hp_ne_top
no goals
case hfq
α : Type u_1
E : Type ?u.755518
F : Type u_2
G : Type ?u.755524
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hfp : snorm f p μ < ⊤
⊢ snorm' (fun a => f a) (ENNReal.toReal p) μ < ⊤
simpa [snorm_eq_snorm' hp_ne_zero hp_ne_top] using hfp