integral_map_equiv — Mathlib

English

If e is a measurable equivalence, the integral over β maps to α via e: ∫ f d map e μ = ∫ f(e x) dμ.

Русский

Если e — измеримое эквивалентность, интеграл по β через отображение e равен интегралу по α от f(e(x)).

LaTeX

$$$$\int y, f(y) \partial(Measure.map e \mu) = \int x, f(e(x)) \partial\mu.$$$$

Lean4

theorem integral_map_equiv {β} [MeasurableSpace β] (e : α ≃ᵐ β) (f : β → G) :
    ∫ y, f y ∂Measure.map e μ = ∫ x, f (e x) ∂μ :=
  e.measurableEmbedding.integral_map f

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