comp_measurable — Mathlib

English

If g is integrable w.r.t. μ.map f and f is measurable, then g ∘ f is integrable w.r.t μ.

Русский

Если g интегрируемо по μ.map f и f измерима, то g ∘ f интегрируемо по μ.

LaTeX

$$$\\mathrm{Integrable}(g\\circ f, μ)$ provided $\\mathrm{Integrable}(g, \\mathrm{map}\, f\, μ)$ and $f$ measurable.$$

Lean4

theorem comp_measurable {f : α → α'} {g : α' → ε} (hg : Integrable g (Measure.map f μ)) (hf : Measurable f) :
    Integrable (g ∘ f) μ :=
  hg.comp_aemeasurable hf.aemeasurable

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