integrable_comp_of_integrable — Mathlib

English

If f is measure-preserving and g is integrable with respect to ν, then g ∘ f is integrable with respect to μ.

Русский

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

LaTeX

$$$\\mathrm{MeasurePreserving}(f)\\, μ\\nu \\Rightarrow \\mathrm{Integrable}(g\\circ f, μ) \\text{ if } \\mathrm{Integrable}(g, ν).$$$

Lean4

theorem integrable_comp_of_integrable {ν : Measure δ} {g : δ → ε} {f : α → δ} (hf : MeasurePreserving f μ ν)
    (hg : Integrable g ν) : Integrable (g ∘ f) μ :=
  hf.integrable_comp hg.aestronglyMeasurable |>.mpr hg

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