is_probability_measure'

Mathlib.Probability.Kernel.Defs

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.IsMarkovKernel.is_probability_measure'

English

Same as above, alternative view of isFiniteKernel from ≤ relation.

Русский

То же самое взглядом на измеенение через отношение ≤.

LaTeX

$$$\text{IsFiniteKernel}(\kappa) \iff \text{IsFiniteKernel}(\kappa) \text{ через } \le$$$

Lean4

instance is_probability_measure' [IsMarkovKernel κ] (a : α) : IsProbabilityMeasure (κ a) :=
  IsMarkovKernel.isProbabilityMeasure a

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

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

Разделы

Аффилиация

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