setIntegral_image_emb — Mathlib

English

If f is a measure-preserving embedding and g: Y → E, then the integral over the image f''s of s of g is equal to the integral over the preimage of s under f of g(f(x)).

Русский

Если f является вложением, сохраняющим меру, и g: Y → E, то интеграл по образу f''s(s) g равен интегралу по предобразу f^{-1}(s) g(f(x)).

LaTeX

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

Lean4

theorem setIntegral_image_emb {Y} {_ : MeasurableSpace Y} {f : X → Y} {ν} (h₁ : MeasurePreserving f μ ν)
    (h₂ : MeasurableEmbedding f) (g : Y → E) (s : Set X) : ∫ y in f '' s, g y ∂ν = ∫ x in s, g (f x) ∂μ :=
  Eq.symm <| (h₁.restrict_image_emb h₂ s).integral_comp h₂ _

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