measure_sum_seq

Mathlib.Probability.Kernel.Defs

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

← MathLib Explorer

English

For IsSFiniteKernel κ and a ∈ α, (Measure.sum (λ n, seq κ n a)) = κ a.

Русский

Для κ конечного по seq и любого a ∈ α сумма мер seq κ n a равна κ a.

LaTeX

$$$\\mathrm{Measure.sum}\\, (fun n => \\mathrm{seq}\\\\ κ\\\\ n \\\\ a) = κ a$$$

Lean4

theorem measure_sum_seq (κ : Kernel α β) [h : IsSFiniteKernel κ] (a : α) : (Measure.sum fun n => seq κ n a) = κ a := by
  rw [← Kernel.sum_apply, kernel_sum_seq κ]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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