comp_aemeasurable — Mathlib

English

If g is AEStronglyMeasurable w.r.t. Measure.map f μ and f is AEMeasurable, then the composition g ∘ f is AEStronglyMeasurable with respect to μ.

Русский

Если g AEStronglyMeasurable по Measure.map f μ, и f AEMeasurable, то композиция g ∘ f является AEStronglyMeasurable по μ.

LaTeX

$$$AEStronglyMeasurable g (Measure.map f \mu) \Rightarrow AEMeasurable f \mu \Rightarrow AEStronglyMeasurable (g \circ f) \mu$$$

Lean4

theorem comp_aemeasurable {γ : Type*} {_ : MeasurableSpace γ} {_ : MeasurableSpace α} {f : γ → α} {μ : Measure γ}
    (hg : AEStronglyMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) : AEStronglyMeasurable (g ∘ f) μ :=
  ⟨hg.mk g ∘ hf.mk f, hg.stronglyMeasurable_mk.comp_measurable hf.measurable_mk,
    (ae_eq_comp hf hg.ae_eq_mk).trans (hf.ae_eq_mk.fun_comp (hg.mk g))⟩

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