lintegral_comp_emb — Mathlib

English

For a measure-preserving embedding hge and f, ∫ f(g a) dμ = ∫ f b dν; i.e., the lintegral is preserved under embedding.

Русский

Для отображения с сохранением меры и вложением hge линеграл сохраняется: ∫ f(g a) dμ = ∫ f(b) dν.

LaTeX

$$$$ \int f(g a)\, dμ = \int f(b)\, dν, $$$$

Lean4

theorem lintegral_comp_emb (hge : MeasurableEmbedding g) (f : β → ℝ≥0∞) : ∫⁻ a, f (g a) ∂μ = ∫⁻ b, f b ∂ν := by
  rw [← hg.map_eq, hge.lintegral_map]

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