integral_restrict

Mathlib.Probability.Kernel.Integral

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.integral_restrict

English

The integral with respect to κ.restrict hs equals the integral over s with κ a.

Русский

Интеграл по κ.restrict hs равен интегралу по s с κ a.

LaTeX

$$$\\int x, f(x) \\, d\\kappa.restrict hs (a) = \\int x, f(x) \\, d\\kappa(a)$$$

Lean4

@[simp]
theorem integral_restrict (hs : MeasurableSet s) : ∫ x, f x ∂κ.restrict hs a = ∫ x in s, f x ∂κ a := by
  rw [restrict_apply]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru