instIsMarkovKernelForallValNatMemFinsetIicForallTraj

Mathlib.Probability.Kernel.IonescuTulcea.Traj

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

English

For every a, traj κ a is a Markov kernel on the full trajectory space; i.e., IsMarkovKernel (traj κ a).

Русский

Для каждого a ядро traj κ a является марковским ядром в пространстве траектории; IsMarkovKernel (traj κ a).

LaTeX

$$$\\forall a:\\mathbb{N},\\ IsMarkovKernel (traj\\ κ\\ a)$$$

Lean4

instance (a : ℕ) : IsMarkovKernel (traj κ a) :=
  ⟨fun _ ↦ isProbabilityMeasure_trajFun ..⟩

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

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

Разделы

Аффилиация

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