memLp_of_isFiniteMeasure — Mathlib

English

If μ is finite, MemLp f p μ holds for any simple function f.

Русский

Если мера μ конечна, то для любой простой функции f верно MemLp f p μ.

LaTeX

$$$\\text{IsFiniteMeasure}(\\mu) \\Rightarrow \\mathrm{MemLp}(f,p,\\mu)$$$

Lean4

theorem memLp_of_isFiniteMeasure (f : α →ₛ E) (p : ℝ≥0∞) (μ : Measure α) [IsFiniteMeasure μ] : MemLp f p μ :=
  let ⟨C, hfC⟩ := f.exists_forall_norm_le
  MemLp.of_bound f.aestronglyMeasurable C <| Eventually.of_forall hfC

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