sum

Mathlib.Probability.Kernel.Defs

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

Lean4

/-- Sum of an indexed family of kernels. -/
protected noncomputable def sum [Countable ι] (κ : ι → Kernel α β) : Kernel α β
    where
  toFun a := Measure.sum fun n => κ n a
  measurable' := by
    refine Measure.measurable_of_measurable_coe _ fun s hs => ?_
    simp_rw [Measure.sum_apply _ hs]
    exact Measurable.ennreal_tsum fun n => Kernel.measurable_coe (κ n) hs

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

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

Разделы

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

Аффилиация

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