setIntegral_map — Mathlib

English

Let f: X → Y be a measurable embedding and g: Y → E. Then the integral over s with respect to map f μ equals the integral over preimage f^{-1}(s) of g(f(x)).

Русский

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

LaTeX

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

Lean4

theorem _root_.MeasurableEmbedding.setIntegral_map {Y} {_ : MeasurableSpace Y} {f : X → Y} (hf : MeasurableEmbedding f)
    (g : Y → E) (s : Set Y) : ∫ y in s, g y ∂Measure.map f μ = ∫ x in f ⁻¹' s, g (f x) ∂μ := by
  rw [hf.restrict_map, hf.integral_map]

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