aemeasurable_comp_iff — Mathlib

English

If g is a MeasurableEmbedding, AEMeasurable (g ∘ f) μ is equivalent to AEMeasurable f μ.

Русский

Если g — измеримое вложение, AЕ-измеримость g∘f относительно μ эквивалентна AЕ-измеримости f относительно μ.

LaTeX

$$$\mathrm{AEMeasurable}(g \circ f, \mu) \iff \mathrm{AEMeasurable}(f, \mu)$$$

Lean4

theorem aemeasurable_comp_iff {g : β → γ} (hg : MeasurableEmbedding g) {μ : Measure α} :
    AEMeasurable (g ∘ f) μ ↔ AEMeasurable f μ :=
  by
  refine ⟨fun H => ?_, hg.measurable.comp_aemeasurable⟩
  suffices AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ by
    rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
  exact hg.measurable_rangeSplitting.comp_aemeasurable H.subtype_mk

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