α : Type u_1
E : Type u_2
F : Type ?u.4184586
G : Type ?u.4184589
m✝ m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ✝ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
h_le_μ : snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
⊢ snorm' f p μ ≤ snorm' f q μ
α : Type u_1
E : Type u_2
F : Type ?u.4184586
G : Type ?u.4184589
m✝ m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ✝ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
⊢ snorm' f p μ ≤ snorm' f q μ
have h_le_μ := snorm'_le_snorm'_mul_rpow_measure_univ hp0_lt hpq hf
no goals
α : Type u_1
E : Type u_2
F : Type ?u.4184586
G : Type ?u.4184589
m✝ m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ✝ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
h_le_μ : snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
⊢ snorm' f p μ ≤ snorm' f q μ
rwa [measure_univ, ENNReal.one_rpow, mul_one] at h_le_μ