α : Type u_1
E : Type ?u.831489
F : Type u_2
G : Type ?u.831495
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 ≠ ⊤
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) < ⊤
⊢ snorm f p μ < ⊤
α : Type u_1
E : Type ?u.831489
F : Type u_2
G : Type ?u.831495
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 ≠ ⊤
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) < ⊤ → snorm f p μ < ⊤
intro h
α : Type u_1
E : Type ?u.831489
F : Type u_2
G : Type ?u.831495
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 ≠ ⊤
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) < ⊤
hp' : 0 < ENNReal.toReal p
⊢ snorm f p μ < ⊤
α : Type u_1
E : Type ?u.831489
F : Type u_2
G : Type ?u.831495
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 ≠ ⊤
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) < ⊤
⊢ snorm f p μ < ⊤
have hp' := ENNReal.toReal_pos hp_ne_zero hp_ne_top
α : Type u_1
E : Type ?u.831489
F : Type u_2
G : Type ?u.831495
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 ≠ ⊤
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) < ⊤
hp' : 0 < ENNReal.toReal p
this : 0 < 1 / ENNReal.toReal p
⊢ snorm f p μ < ⊤
α : Type u_1
E : Type ?u.831489
F : Type u_2
G : Type ?u.831495
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 ≠ ⊤
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) < ⊤
hp' : 0 < ENNReal.toReal p
⊢ snorm f p μ < ⊤
have : 0 < 1 / p.toReal := div_pos zero_lt_one hp'
no goals
α : Type u_1
E : Type ?u.831489
F : Type u_2
G : Type ?u.831495
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 ≠ ⊤
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) < ⊤
hp' : 0 < ENNReal.toReal p
this : 0 < 1 / ENNReal.toReal p
⊢ snorm f p μ < ⊤
simpa [snorm_eq_lintegral_rpow_nnnorm hp_ne_zero hp_ne_top] using
  ENNReal.rpow_lt_top_of_nonneg (le_of_lt this) (ne_of_lt h)