lintegral_map_equiv — Mathlib

English

If g is a MeasurableEmbedding, then for every f we have ∫ f ∘ g dμ = ∫ f d(map g μ).

Русский

Если g — измеримое вложение, то для любой функции f выполняется ∫ f ∘ g dμ = ∫ f d(map g μ).

LaTeX

$$$$ \int (f\circ g)\, dμ = \int f\, d(map\ g\ μ). $$$$

Lean4

protected theorem lintegral_map_equiv (f : β → ℝ≥0∞) (g : α ≃ᵐ β) (hg : MeasurePreserving g μ ν) :
    ∫⁻ a, f a ∂ν = ∫⁻ a, f (g a) ∂μ := by rw [← MeasureTheory.lintegral_map_equiv f g, hg.map_eq]

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