setLIntegral_map — Mathlib

English

For a measurable set s and measurable f, the integral of f over map g μ restricted to s equals the integral of f(g x) over μ restricted to g^{-1}(s).

Русский

Для измеримого множества s и измеримой f: ∫ over map g μ restricted to s f = ∫ over μ restricted to g^{-1}(s) f ∘ g.

LaTeX

$$$$ \int⁻ y \in s, f(y)\, d(map\ g\ μ) = \int⁻ x \in g^{-1}' s, f(g(x))\, dμ.$$$$

Lean4

theorem setLIntegral_map {f : β → ℝ≥0∞} {g : α → β} {s : Set β} (hs : MeasurableSet s) (hf : Measurable f)
    (hg : Measurable g) : ∫⁻ y in s, f y ∂map g μ = ∫⁻ x in g ⁻¹' s, f (g x) ∂μ := by
  rw [restrict_map hg hs, lintegral_map hf hg]

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