truncation — Mathlib

English

If f is AEStronglyMeasurable, then its truncation by A is AEStronglyMeasurable with respect to the same measure.

Русский

Если f — AEStronglyMeasurable, то усечение f по A сохраняет AEStronglyMeasurable отношение к той же мере.

LaTeX

$$$$\text{AEStronglyMeasurable}(\text{truncation}(f,A), μ).$$$$

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.truncation (hf : AEStronglyMeasurable f μ) {A : ℝ} :
    AEStronglyMeasurable (truncation f A) μ :=
  by
  apply AEStronglyMeasurable.comp_aemeasurable _ hf.aemeasurable
  exact (stronglyMeasurable_id.indicator measurableSet_Ioc).aestronglyMeasurable

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