aestronglyMeasurable_map_iff — Mathlib

English

For a measurable embedding f, AEStronglyMeasurable g on Measure.map f μ is equivalent to AEStronglyMeasurable (g ∘ f) μ.

Русский

Для измеримого вложения f AEStronglyMeasurable g на Measure.map f μ эквивалентно AEStronglyMeasurable (g ∘ f) μ.

LaTeX

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

Lean4

theorem _root_.MeasurableEmbedding.aestronglyMeasurable_map_iff {γ : Type*} {mγ : MeasurableSpace γ}
    {mα : MeasurableSpace α} {f : γ → α} {μ : Measure γ} (hf : MeasurableEmbedding f) {g : α → β} :
    AEStronglyMeasurable g (Measure.map f μ) ↔ AEStronglyMeasurable (g ∘ f) μ :=
  by
  refine ⟨fun H => H.comp_measurable hf.measurable, ?_⟩
  rintro ⟨g₁, hgm₁, heq⟩
  rcases hf.exists_stronglyMeasurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩
  exact ⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩

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