English
Equality of two-step composition in the measurable setting reduces to a single-step composition.
Русский
Равенство двухступенчатой композиции сводится к простой композиции.
LaTeX
$$$(comp g hg f).compQuasiMeasurePreserving φ hφ = comp g hg (f.compQuasiMeasurePreserving φ hφ)$$$
Lean4
/-- Given a measurable function `g : β → γ`, and an almost everywhere equal function `[f] : α →ₘ β`,
return the equivalence class of `g ∘ f`, i.e., the almost everywhere equal function
`[g ∘ f] : α →ₘ γ`. This requires that `γ` has a second countable topology. -/
def compMeasurable (g : β → γ) (hg : Measurable g) (f : α →ₘ[μ] β) : α →ₘ[μ] γ :=
Quotient.liftOn' f (fun f' => mk (g ∘ (f' : α → β)) (hg.comp_aemeasurable f'.2.aemeasurable).aestronglyMeasurable)
fun _ _ H => mk_eq_mk.2 <| H.fun_comp g
