memLp_two_iff_integrable_sq_norm — Mathlib

English

MemLp f 2 μ is equivalent to Integrable of |f|^2 when f is real-valued and measurable.

Русский

MemLp f 2 μ эквивалентно Integrable(|f|^2) μ для вещественно-значной f.

LaTeX

$$$ \\operatorname{MemLp} f 2 \\mu \\iff \\operatorname{Integrable}(x \\mapsto |f(x)|^2)\\mu$$$

Lean4

theorem memLp_two_iff_integrable_sq_norm {f : α → F} (hf : AEStronglyMeasurable f μ) :
    MemLp f 2 μ ↔ Integrable (fun x => ‖f x‖ ^ 2) μ :=
  by
  rw [← memLp_one_iff_integrable]
  convert (memLp_norm_rpow_iff hf two_ne_zero ENNReal.ofNat_ne_top).symm
  · simp
  · rw [div_eq_mul_inv, ENNReal.mul_inv_cancel two_ne_zero ENNReal.ofNat_ne_top]

Похожие утверждения