comp_ae_measurable' — Mathlib

English

If f is AEStronglyMeasurable with respect to μ.map g and g is AEMeasurable with respect to μ, then f ∘ g is AEStronglyMeasurable with respect to μ.

Русский

Если f — AEStronglyMeasurable относительно μ.map g, а g — AEMeasurable относительно μ, то f ∘ g — AEStronglyMeasurable относительно μ.

LaTeX

$$$\text{AEStronglyMeasurable}_{m\mathord{\;}-comap g}(f\circ g)\;\mu$$

Lean4

theorem comp_ae_measurable' {α β γ : Type*} [TopologicalSpace β] {mα : MeasurableSpace α} {_ : MeasurableSpace γ}
    {f : α → β} {μ : Measure γ} {g : γ → α} (hf : AEStronglyMeasurable f (μ.map g)) (hg : AEMeasurable g μ) :
    AEStronglyMeasurable[mα.comap g] (f ∘ g) μ :=
  ⟨hf.mk f ∘ g, hf.stronglyMeasurable_mk.comp_measurable (measurable_iff_comap_le.mpr le_rfl),
    ae_eq_comp hg hf.ae_eq_mk⟩

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