α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ Memℒp f 2 ↔ Memℒp (fun x => ‖f x‖ ^ 2) 1
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ Memℒp f 2 ↔ Integrable fun x => ‖f x‖ ^ 2
rw [← memℒp_one_iff_integrable]
case h.e'_2.h.e'_5.h
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ ‖f x✝‖ ^ 2 = ‖f x✝‖ ^ ENNReal.toReal 2

case h.e'_2.h.e'_6
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 / 2
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ Memℒp f 2 ↔ Memℒp (fun x => ‖f x‖ ^ 2) 1
convert (memℒp_norm_rpow_iff hf two_ne_zero ENNReal.two_ne_top).symm
no goals
case h.e'_2.h.e'_5.h
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ ‖f x✝‖ ^ 2 = ‖f x✝‖ ^ ENNReal.toReal 2
simp
no goals
case h.e'_2.h.e'_6
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 / 2
rw [div_eq_mul_inv, ENNReal.mul_inv_cancel two_ne_zero ENNReal.two_ne_top]