setLIntegral_restrict — Mathlib

English

Let s be a measurable subset of β. For any a and measurable f, the L-integral over t with κ|s at a equals the L-integral over t ∩ s with κ at a.

Русский

Пусть s ⊆ β измеримо. При любом a и измеримой f интеграл по t ограниченного ядра κ|s равен интегралу по t ∩ s относительно κ.

LaTeX

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

Lean4

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

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