comp_aemeasurable — Mathlib

English

If g is integrable with respect to μ.map f and f is AEMeasurable, then g ∘ f is integrable with respect to μ.

Русский

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

LaTeX

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

Lean4

theorem comp_aemeasurable {f : α → α'} {g : α' → ε} (hg : Integrable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
    Integrable (g ∘ f) μ :=
  (integrable_map_measure hg.aestronglyMeasurable hf).mp hg

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