comp_quasiMeasurePreserving — Mathlib

English

If ν is a measure on δ, and f: α→δ, g: δ→β with hg AEMeasurable on ν and hf QuasiMeasurePreserving from μ to ν, then g∘f is AEMeasurable on μ.

Русский

Пусть ν — мера на δ, f: α→δ, g: δ→β, hg — AЕ-измеримая относительно ν, hf — квази-измеримая от μ к ν; тогда g∘f — AЕ-измеримая относительно μ.

LaTeX

$$$\mathrm{AEMeasurable}(g, \nu) \rightarrow \mathrm{QuasiMeasurePreserving}(f, \mu, \nu) \rightarrow \mathrm{AEMeasurable}(g \circ f, \mu)$$$

Lean4

@[fun_prop]
theorem comp_quasiMeasurePreserving {ν : Measure δ} {f : α → δ} {g : δ → β} (hg : AEMeasurable g ν)
    (hf : QuasiMeasurePreserving f μ ν) : AEMeasurable (g ∘ f) μ :=
  (hg.mono' hf.absolutelyContinuous).comp_measurable hf.measurable

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