case h.e'_2.h.e'_5.h
α : Type u_1
F : Type ?u.18682
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → ℝ
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ f x✝ ^ 2 = ‖f x✝‖ ^ 2
α : Type u_1
F : Type ?u.18682
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → ℝ
hf : AEStronglyMeasurable f μ
⊢ Memℒp f 2 ↔ Integrable fun x => f x ^ 2
convert memℒp_two_iff_integrable_sq_norm hf using 3
no goals
case h.e'_2.h.e'_5.h
α : Type u_1
F : Type ?u.18682
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → ℝ
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ f x✝ ^ 2 = ‖f x✝‖ ^ 2
simp