case pos
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : μ = 0
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹

case neg
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
by_cases hμ : μ = 0
case neg
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
case neg
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
haveI : μ.ae.NeBot := ae_neBot.mpr hμ
case pos
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hp : p = 0
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹

case neg
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hp : ¬p = 0
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
case neg
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
by_cases hp : p = 0
case neg
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖↑C‖₊
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
case neg
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hp : ¬p = 0
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
have : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖(C : ℝ)‖₊ := hfC.mono fun x hx => hx.trans_eq C.nnnorm_eq.symm
case neg
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖↑C‖₊
⊢ snorm (fun x => ↑C) p μ = C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
case neg
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖↑C‖₊
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
refine' (snorm_mono_ae this).trans_eq _
no goals
case neg
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖↑C‖₊
⊢ snorm (fun x => ↑C) p μ = C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
rw [snorm_const _ hp hμ, C.nnnorm_eq, one_div, ENNReal.smul_def, smul_eq_mul]
no goals
case pos
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : μ = 0
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
simp [hμ]
no goals
case pos
α : Type u_1
E : Type ?u.1436902
F : Type u_2
G : Type ?u.1436908
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hp : p = 0
⊢ snorm f p μ ≤ C • ↑↑μ Set.univ ^ (ENNReal.toReal p)⁻¹
simp [hp]