memLp_truncation — Mathlib

English

If μ is finite and f is AEStronglyMeasurable, then truncation(f,A) belongs to L^p(μ) for all p.

Русский

Если мера μ конечна и f - AEStronglyMeasurable, то truncation(f,A) ∈ L^p(μ) для всех p.

LaTeX

$$$\forall A \forall p \in [0,\infty],\quad truncation(f,A) \in L^p(\mu)$$$

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.memLp_truncation [IsFiniteMeasure μ] (hf : AEStronglyMeasurable f μ)
    {A : ℝ} {p : ℝ≥0∞} : MemLp (truncation f A) p μ :=
  MemLp.of_bound hf.truncation |A| (Eventually.of_forall fun _ => abs_truncation_le_bound _ _ _)

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