integrableOn_iff_comap — Mathlib

English

For a measurable embedding e, integrability of f on s w.r.t. μ is equivalent to integrability of f ∘ e on e^{-1}(s) w.r.t. μ.comap e.

Русский

Для измеримого вложения e интегрируемость f на s по μ эквивалентна интегрируемости f ∘ e на e^{-1}(s) по μ comap e.

LaTeX

$$IntegrableOn f s μ ↔ IntegrableOn (f ∘ e) (e^{-1}(s)) (μ.comap e)$$

Lean4

theorem _root_.MeasurableEmbedding.integrableOn_iff_comap [MeasurableSpace β] {e : α → β} (he : MeasurableEmbedding e)
    {f : β → ε} {μ : Measure β} {s : Set β} (hs : s ⊆ range e) :
    IntegrableOn f s μ ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) (μ.comap e) := by
  simp_rw [← he.integrableOn_map_iff, he.map_comap, IntegrableOn, Measure.restrict_restrict_of_subset hs]

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