integrable_sq — Mathlib

English

For a function f: α → real, MemLp f 2 μ implies Integrable f^2 with respect to μ.

Русский

Для функции f: α → ℝ, MemLp f 2 μ ⇒ Integrable (f^2) μ.

LaTeX

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

Lean4

theorem integrable_sq {f : α → ℝ} (h : MemLp f 2 μ) : Integrable (fun x => f x ^ 2) μ := by
  simpa [← memLp_one_iff_integrable] using h.norm_rpow two_ne_zero ENNReal.ofNat_ne_top

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