α : Type u_1
E : Type u_2
F : Type ?u.4265033
G : Type ?u.4265036
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ (ε * ↑↑μ {x | ε ≤ ↑‖f x‖₊ ^ ENNReal.toReal p}) ^ (1 / ENNReal.toReal p) ≤
    (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
α : Type u_1
E : Type u_2
F : Type ?u.4265033
G : Type ?u.4265036
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ (ε * ↑↑μ {x | ε ≤ ↑‖f x‖₊ ^ ENNReal.toReal p}) ^ (1 / ENNReal.toReal p) ≤ snorm f p μ
rw [snorm_eq_lintegral_rpow_nnnorm hp_ne_zero hp_ne_top]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.4265033
G : Type ?u.4265036
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ (ε * ↑↑μ {x | ε ≤ ↑‖f x‖₊ ^ ENNReal.toReal p}) ^ (1 / ENNReal.toReal p) ≤
    (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
exact
  ENNReal.rpow_le_rpow (mul_meas_ge_le_lintegral₀ (hf.ennnorm.pow_const _) ε)
    (one_div_nonneg.2 ENNReal.toReal_nonneg)