IsKolmogorovProcess_mk

Mathlib.Probability.Process.Kolmogorov

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.IsAEKolmogorovProcess.IsKolmogorovProcess_mk

English

If X is an AE KolmogorovProcess, then IsKolmogorovProcess (h.mk X) P p q M.

Русский

Если X является AE Kolmogorov-процессом, то IsKolmogorovProcess (h.mk X) с теми же параметрами выполняется.

LaTeX

$$$IsKolmogorovProcess\\ (h.mk X)\\ P\\ p\\ q\\ M$$$

Lean4

theorem IsKolmogorovProcess_mk (h : IsAEKolmogorovProcess X P p q M) : IsKolmogorovProcess (h.mk X) P p q M :=
  (Classical.choose_spec h).1

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

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

Разделы

Аффилиация

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