integral_comp' — Mathlib

English

If f is measure-preserving, then the integral over μ of g∘f equals the integral over ν of g: ∫ g(f x) dμ = ∫ g y dν.

Русский

Если f сохраняет меру, то интеграл от g∘f по μ равен интегралу по ν: ∫ 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 μ ν) (g : β → G) :
    ∫ x, g (f x) ∂μ = ∫ y, g y ∂ν :=
  MeasurePreserving.integral_comp h f.measurableEmbedding _

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