integrable_truncation — Mathlib

English

If f is AEStronglyMeasurable and μ is finite, then truncation(f,A) is integrable.

Русский

Если f является AEStronglyMeasurable и μ конечна, то truncation(f,A) интегрируема.

LaTeX

$$Integrable (truncation(f,A)) μ$$

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.integrable_truncation [IsFiniteMeasure μ]
    (hf : AEStronglyMeasurable f μ) {A : ℝ} : Integrable (truncation f A) μ := by rw [← memLp_one_iff_integrable];
  exact hf.memLp_truncation

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