comp_quasiMeasurePreserving — Mathlib

English

If g is AEStronglyMeasurable w.r.t. Measure.map f μ and f is QuasiMeasurePreserving from μ to ν, then g ∘ f is AEStronglyMeasurable w.r.t. μ.

Русский

Если g AEStronglyMeasurable по Measure.map f μ и f — QuasiMeasurePreserving μ → ν, то g ∘ f — AEStronglyMeasurable по μ.

LaTeX

$$$AEStronglyMeasurable g (Measure.map f \mu) \Rightarrow MeasureTheory.QuasiMeasurePreserving f \mu \nu \Rightarrow AEStronglyMeasurable (g \circ f) \mu$$$

Lean4

theorem comp_quasiMeasurePreserving {γ : Type*} {_ : MeasurableSpace γ} {_ : MeasurableSpace α} {f : γ → α}
    {μ : Measure γ} {ν : Measure α} (hg : AEStronglyMeasurable g ν) (hf : QuasiMeasurePreserving f μ ν) :
    AEStronglyMeasurable (g ∘ f) μ :=
  (hg.mono_ac hf.absolutelyContinuous).comp_measurable hf.measurable

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