α : Type u_1
E : Type ?u.1517887
F : Type u_2
G : Type ?u.1517893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ snorm f p μ ≤ ENNReal.ofReal C * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
α : Type u_1
E : Type ?u.1517887
F : Type u_2
G : Type ?u.1517893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ snorm f p μ ≤ ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹ * ENNReal.ofReal C
rw [← mul_comm]
no goals
α : Type u_1
E : Type ?u.1517887
F : Type u_2
G : Type ?u.1517893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ snorm f p μ ≤ ENNReal.ofReal C * ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
exact snorm_le_of_ae_nnnorm_bound (hfC.mono fun x hx => hx.trans C.le_coe_toNNReal)