α : Type u_1
E : Type u_2
F : Type ?u.4415601
G : Type ?u.4415604
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / ENNReal.toReal p * ENNReal.toReal p = 1
⊢ ε * ↑↑μ {x | ε ≤ ↑‖f x‖₊ ^ ENNReal.toReal p} ≤ snorm f p μ ^ ENNReal.toReal p
α : Type u_1
E : Type u_2
F : Type ?u.4415601
G : Type ?u.4415604
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ε * ↑↑μ {x | ε ≤ ↑‖f x‖₊ ^ ENNReal.toReal p} ≤ snorm f p μ ^ ENNReal.toReal p
have : 1 / p.toReal * p.toReal = 1 := by
  refine' one_div_mul_cancel _
  rw [Ne, ENNReal.toReal_eq_zero_iff]
  exact not_or_of_not hp_ne_zero hp_ne_top
α : Type u_1
E : Type u_2
F : Type ?u.4415601
G : Type ?u.4415604
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / ENNReal.toReal p * ENNReal.toReal p = 1
⊢ ((ε * ↑↑μ {x | ε ≤ ↑‖f x‖₊ ^ ENNReal.toReal p}) ^ (1 / ENNReal.toReal p)) ^ ENNReal.toReal p ≤
    snorm f p μ ^ ENNReal.toReal p
α : Type u_1
E : Type u_2
F : Type ?u.4415601
G : Type ?u.4415604
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / ENNReal.toReal p * ENNReal.toReal p = 1
⊢ ε * ↑↑μ {x | ε ≤ ↑‖f x‖₊ ^ ENNReal.toReal p} ≤ snorm f p μ ^ ENNReal.toReal p
rw [← ENNReal.rpow_one (ε * μ { x | ε ≤ (‖f x‖₊ : ℝ≥0∞) ^ p.toReal }), ← this, ENNReal.rpow_mul]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.4415601
G : Type ?u.4415604
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / ENNReal.toReal p * ENNReal.toReal p = 1
⊢ ((ε * ↑↑μ {x | ε ≤ ↑‖f x‖₊ ^ ENNReal.toReal p}) ^ (1 / ENNReal.toReal p)) ^ ENNReal.toReal p ≤
    snorm f p μ ^ ENNReal.toReal p
exact
  ENNReal.rpow_le_rpow (pow_mul_meas_ge_le_snorm μ hp_ne_zero hp_ne_top hf ε)
    ENNReal.toReal_nonneg
α : Type u_1
E : Type u_2
F : Type ?u.4415601
G : Type ?u.4415604
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ENNReal.toReal p ≠ 0
α : Type u_1
E : Type u_2
F : Type ?u.4415601
G : Type ?u.4415604
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ 1 / ENNReal.toReal p * ENNReal.toReal p = 1
refine' one_div_mul_cancel _
α : Type u_1
E : Type u_2
F : Type ?u.4415601
G : Type ?u.4415604
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ¬(p = 0 ∨ p = ⊤)
α : Type u_1
E : Type u_2
F : Type ?u.4415601
G : Type ?u.4415604
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ENNReal.toReal p ≠ 0
rw [Ne, ENNReal.toReal_eq_zero_iff]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.4415601
G : Type ?u.4415604
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ¬(p = 0 ∨ p = ⊤)
exact not_or_of_not hp_ne_zero hp_ne_top