comp_measurePreserving — Mathlib

English

If g is AEStronglyMeasurable and f is measure-preserving, then g ∘ f is AEStronglyMeasurable.

Русский

Если g силово измеримо AE и f сохраняет меру, то g ∘ f измеримо AE.

LaTeX

$$$$\\text{AEStronglyMeasurable}(g, \\nu) \\wedge \\text{MeasurePreserving}(f, \\mu, \\nu) \\Rightarrow \\text{AEStronglyMeasurable}(g \\circ f, \\mu).$$$$

Lean4

theorem comp_measurePreserving {γ : Type*} {_ : MeasurableSpace γ} {_ : MeasurableSpace α} {f : γ → α} {μ : Measure γ}
    {ν : Measure α} (hg : AEStronglyMeasurable g ν) (hf : MeasurePreserving f μ ν) : AEStronglyMeasurable (g ∘ f) μ :=
  hg.comp_quasiMeasurePreserving hf.quasiMeasurePreserving

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