compQuasiMeasurePreserving — Mathlib

English

Composition of an almost everywhere equal function with a quasi-measure-preserving map yields a new AEEqFun.

Русский

Композиция AEEqFun с отображением, сохраняющим квазимеру, образует новое AEEqFun.

LaTeX

$$$\\text{compQuasiMeasurePreserving}(g,f,hf) =\\mathrm{mk}(g \\circ f) (g\\,\\text{aestronglyMeasurable} \\circ hf)$$$

Lean4

/-- Composition of an almost everywhere equal function and a quasi-measure-preserving function.

See also `AEEqFun.compMeasurePreserving`. -/
def compQuasiMeasurePreserving (g : β →ₘ[ν] γ) (f : α → β) (hf : QuasiMeasurePreserving f μ ν) : α →ₘ[μ] γ :=
  Quotient.liftOn' g (fun g ↦ mk (g ∘ f) <| g.2.comp_quasiMeasurePreserving hf) fun _ _ h ↦
    mk_eq_mk.2 <| h.comp_tendsto hf.tendsto_ae

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