lintegral_map — Mathlib

English

For measurable f and g' measurable, the lintegral over map κ f a of g' equals the lintegral over κ a of g'(f a).

Русский

Для измеримого f и g' измеримого выполняется линтеграл: ∫ g' d(map κ f a) = ∫ g'(f(a)) dκ a.

LaTeX

$$$$ \\int g' \\, d(\\kappa.map f \\, a) = \\int g'(f(a)) \\, d\\kappa a. $$$$

Lean4

nonrec theorem lintegral_map (κ : Kernel α β) (hf : Measurable f) (a : α) {g' : γ → ℝ≥0∞} (hg : Measurable g') :
    ∫⁻ b, g' b ∂map κ f a = ∫⁻ a, g' (f a) ∂κ a := by rw [map_apply _ hf, lintegral_map hg hf]

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