setIntegral_preimage_emb — Mathlib

English

If f is measure-preserving and a measurable embedding, then for all g and s, ∫ x in f^{-1}(s) g(f(x)) dμ = ∫ y in s g(y) dν.

Русский

Если f сохраняет меру и является измеримо встроенным, то для любых g и s выполняется равенство интегралов над предобразом и самой областью.

LaTeX

$$$$ \\int_{x \\in f^{-1}(s)} g(f(x)) \\, d\\mu(x) = \\int_{y \\in s} g(y) \\, d\\nu(y) $$$$

Lean4

theorem setIntegral_preimage_emb {Y} {_ : MeasurableSpace Y} {f : X → Y} {ν} (h₁ : MeasurePreserving f μ ν)
    (h₂ : MeasurableEmbedding f) (g : Y → E) (s : Set Y) : ∫ x in f ⁻¹' s, g (f x) ∂μ = ∫ y in s, g y ∂ν :=
  (h₁.restrict_preimage_emb h₂ s).integral_comp h₂ _

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