integrableOn_range_iff_comap — Mathlib

English

For a measurable embedding e, integrability over the range of e corresponds to integrability of f ∘ e over the domain with μ.comap e.

Русский

Интегрируемость по диапазону отображения e соответствует интегрируемости f ∘ e на области определения с μ.comap e.

LaTeX

$$IntegrableOn f (range e) μ ↔ Integrable (f ∘ e) (μ.comap e)$$

Lean4

theorem _root_.MeasurableEmbedding.integrableOn_range_iff_comap [MeasurableSpace β] {e : α → β}
    (he : MeasurableEmbedding e) {f : β → ε} {μ : Measure β} :
    IntegrableOn f (range e) μ ↔ Integrable (f ∘ e) (μ.comap e) := by
  rw [he.integrableOn_iff_comap .rfl, preimage_range, integrableOn_univ]

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