comp_measurable — Mathlib

English

If g is AEStronglyMeasurable w.r.t. Measure.map f μ and f is measurable, then g ∘ f is AEStronglyMeasurable with respect to μ.

Русский

Если g AEStronglyMeasurable по Measure.map f μ и f измерима, то произведение g ∘ f измеримо AES.

LaTeX

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

Lean4

theorem comp_measurable {γ : Type*} {_ : MeasurableSpace γ} {_ : MeasurableSpace α} {f : γ → α} {μ : Measure γ}
    (hg : AEStronglyMeasurable g (Measure.map f μ)) (hf : Measurable f) : AEStronglyMeasurable (g ∘ f) μ :=
  hg.comp_aemeasurable hf.aemeasurable

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