memLp_two_iff_integrable_sq — Mathlib

English

The two-inequality version for MemLp with real-valued functions, linking MemLp 2 μ and integrability of f^2.

Русский

Две эквивалентности MemLp для реальных функций, связующие MemLp 2 μ и интегрируемость f^2.

LaTeX

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

Lean4

theorem memLp_two_iff_integrable_sq {f : α → ℝ} (hf : AEStronglyMeasurable f μ) :
    MemLp f 2 μ ↔ Integrable (fun x => f x ^ 2) μ :=
  by
  convert memLp_two_iff_integrable_sq_norm hf using 3
  simp

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