case h.e'_3.h.e'_6.h.e'_3.h.e'_2
α : Type u_1
E : Type u_2
F : Type ?u.4640914
G : Type ?u.4640917
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∞
⊢ (fun x => ε ≤ ↑‖f x‖₊) = fun x => ε ^ ENNReal.toReal p ≤ ↑‖f x‖₊ ^ ENNReal.toReal p
α : Type u_1
E : Type u_2
F : Type ?u.4640914
G : Type ?u.4640917
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 * ↑↑μ {x | ε ≤ ↑‖f x‖₊} ≤ snorm f p μ ^ ENNReal.toReal p
convert mul_meas_ge_le_pow_snorm μ hp_ne_zero hp_ne_top hf (ε ^ p.toReal) using 4
case h.e'_3.h.e'_6.h.e'_3.h.e'_2.h.a
α : Type u_1
E : Type u_2
F : Type ?u.4640914
G : Type ?u.4640917
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 ≤ ↑‖f x‖₊ ^ ENNReal.toReal p
case h.e'_3.h.e'_6.h.e'_3.h.e'_2
α : Type u_1
E : Type u_2
F : Type ?u.4640914
G : Type ?u.4640917
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∞
⊢ (fun x => ε ≤ ↑‖f x‖₊) = fun x => ε ^ ENNReal.toReal p ≤ ↑‖f x‖₊ ^ ENNReal.toReal p
ext x
no goals
case h.e'_3.h.e'_6.h.e'_3.h.e'_2.h.a
α : Type u_1
E : Type u_2
F : Type ?u.4640914
G : Type ?u.4640917
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 ≤ ↑‖f x‖₊ ^ ENNReal.toReal p
rw [ENNReal.rpow_le_rpow_iff (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]