integrable_comp — Mathlib

English

If f is a measurable equivalence with additional simp properties, integrability is preserved similarly.

Русский

Если f — измеримое эквивалентное отображение с дополнительными упрощениями, интегрируемость сохраняется аналогично.

LaTeX

$$$\\mathrm{Integrable}(g,\\mathrm{map}\, f\, μ) \\iff \\mathrm{Integrable}(g\\circ f, μ)$ (simp lemma).$$

Lean4

theorem integrable_comp {ν : Measure δ} {g : δ → ε} {f : α → δ} (hf : MeasurePreserving f μ ν)
    (hg : AEStronglyMeasurable g ν) : Integrable (g ∘ f) μ ↔ Integrable g ν :=
  by
  rw [← hf.map_eq] at hg ⊢
  exact (integrable_map_measure hg hf.measurable.aemeasurable).symm

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