lintegral_map_equiv — Mathlib

English

For a measurable equivalence g : α ≃ᵐ β, the lintegral with respect to map g μ equals the lintegral of f under μ composed with g, i.e., the same as above under EquivLike.toFunLike.coe.

Русский

Для измеримого эквивалентности g : α ≃ᵐ β тождественный переход линеграла сохраняется: ∫ f d(map g μ) = ∫ f∘g dμ.

LaTeX

$$$$ \int⁻ a, f a ∂map g μ = \int⁻ a, f (g a) ∂μ, $$$$

Lean4

/-- The `lintegral` transforms appropriately under a measurable equivalence `g : α ≃ᵐ β`.
(Compare `lintegral_map`, which applies to a wider class of functions `g : α → β`, but requires
measurability of the function being integrated.) -/
theorem lintegral_map_equiv (f : β → ℝ≥0∞) (g : α ≃ᵐ β) : ∫⁻ a, f a ∂map g μ = ∫⁻ a, f (g a) ∂μ :=
  g.measurableEmbedding.lintegral_map f

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