integral_comp — Mathlib

English

If f is measure-preserving with respect to a map, then the integral is preserved under the map: ∫ g(f x) dμ = ∫ g y dν.

Русский

Если отображение сохраняет меру, то интеграл сохраняется: ∫ g(f(x)) dμ = ∫ g(y) dν.

LaTeX

$$$$\int x, g(f(x)) \partial\mu = \int y, g(y) \partial\nu.$$$$

Lean4

theorem integral_comp {β} {_ : MeasurableSpace β} {f : α → β} {ν} (h₁ : MeasurePreserving f μ ν)
    (h₂ : MeasurableEmbedding f) (g : β → G) : ∫ x, g (f x) ∂μ = ∫ y, g y ∂ν :=
  h₁.map_eq ▸ (h₂.integral_map g).symm

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