case pos
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : μ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C

case neg
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : ¬μ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
by_cases hμ : μ = 0
case neg
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : ¬μ = 0
⊢ snorm (↑↑f) p μ ≤ ↑(measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : ¬μ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C
rw [← ENNReal.coe_le_coe, nnnorm_def, ENNReal.coe_toNNReal (snorm_ne_top _)]
case neg
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : ¬μ = 0
⊢ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹ = ↑(measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : ¬μ = 0
⊢ snorm (↑↑f) p μ ≤ ↑(measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C)
refine' (snorm_le_of_ae_nnnorm_bound hfC).trans_eq _
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : ¬μ = 0
⊢ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹ = ↑(measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C)
rw [← coe_measureUnivNNReal μ, ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne',
  ENNReal.coe_mul, mul_comm, ENNReal.smul_def, smul_eq_mul]
case pos
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : μ = 0
hp : (ENNReal.toReal p)⁻¹ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C

case neg
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : μ = 0
hp : ¬(ENNReal.toReal p)⁻¹ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C
case pos
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : μ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C
by_cases hp : p.toReal⁻¹ = 0
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : μ = 0
hp : (ENNReal.toReal p)⁻¹ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C
simp [hp, hμ, nnnorm_def]
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.431143
G : Type ?u.431146
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
hμ : μ = 0
hp : ¬(ENNReal.toReal p)⁻¹ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * C
simp [hμ, nnnorm_def, Real.zero_rpow hp]