lintegral_restrict — Mathlib

English

For a measurable set s, a point a, and a nonnegative function f, the lintegral of f with respect to the restricted kernel κ|s at a equals the lintegral of f over s with respect to κ at a.

Русский

Пусть s — измеримое множество, a — точка, f ≥ 0. Линтеграл по ограниченному ядру κ|s равен линtegrалу по области s относительно κ.

LaTeX

$$$\\int^{\\! -}_{b} f(b) \\; d(\\kappa|_{s})(a)(b) \\\\ = \\int^{\\! -}_{b \\in s} f(b) \\\\ d\\kappa(a)(b)$$$

Lean4

@[simp]
theorem lintegral_restrict (κ : Kernel α β) (hs : MeasurableSet s) (a : α) (f : β → ℝ≥0∞) :
    ∫⁻ b, f b ∂κ.restrict hs a = ∫⁻ b in s, f b ∂κ a := by rw [restrict_apply]

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