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⟩