kernel_sum_seq

Mathlib.Probability.Kernel.Defs

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

English

Kernel.sum (seq κ) = κ.

Русский

Сумма последовательности seq κ восстанавливает κ.

LaTeX

$$$ Kernel.sum( seq κ ) = κ $$$

Lean4

theorem kernel_sum_seq (κ : Kernel α β) [h : IsSFiniteKernel κ] : Kernel.sum (seq κ) = κ :=
  h.tsum_finite.choose_spec.2.symm

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

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

Разделы

Аффилиация

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