setIntegral_map_equiv — Mathlib

English

Let e be a measurable equivalence X ≃ᵐ Y. Then for any f: Y → E and s ⊆ Y, the integral over map e μ restricted to s equals the integral over μ restricted to preimage of s of f(e(x)).

Русский

Пусть e — измеримое эквивариантное отображение X ≃ᵐ Y. Тогда для любого f: Y → E и s ⊆ Y интеграл по map e μ на s равен интегралу по μ на предобразе e^{-1}(s) от f(e(x)).

LaTeX

$$$$ \\int_{y \\in \\mathrm{map}\, e\\, \\mu} f(y) \\, dy = \\int_{x \\in e^{-1}(s)} f(e(x)) \\, d\\mu(x) $$$$

Lean4

theorem setIntegral_map_equiv {Y} [MeasurableSpace Y] (e : X ≃ᵐ Y) (f : Y → E) (s : Set Y) :
    ∫ y in s, f y ∂Measure.map e μ = ∫ x in e ⁻¹' s, f (e x) ∂μ :=
  e.measurableEmbedding.setIntegral_map f s

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