case intro
α : Type u_1
E : Type u_2
F : Type ?u.436188
G : Type ?u.436191
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : IsFiniteMeasure μ
f : { x // x ∈ Lp E p }
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹) * ↑C
α : Type u_1
E : Type u_2
F : Type ?u.436188
G : Type ?u.436191
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : IsFiniteMeasure μ
f : { x // x ∈ Lp E p }
C : ℝ
hC : 0 ≤ C
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹) * C
lift C to ℝ≥0 using hC
case intro
α : Type u_1
E : Type u_2
F : Type ?u.436188
G : Type ?u.436191
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : IsFiniteMeasure μ
f : { x // x ∈ Lp E p }
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C
this : ‖f‖₊ ≤ measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹) * ↑C
case intro
α : Type u_1
E : Type u_2
F : Type ?u.436188
G : Type ?u.436191
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : IsFiniteMeasure μ
f : { x // x ∈ Lp E p }
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹) * ↑C
have := nnnorm_le_of_ae_bound hfC
no goals
case intro
α : Type u_1
E : Type u_2
F : Type ?u.436188
G : Type ?u.436191
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : IsFiniteMeasure μ
f : { x // x ∈ Lp E p }
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C
this : ‖f‖₊ ≤ measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹) * ↑C
rwa [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_rpow] at this