ae_eq_mk

Mathlib.Probability.Process.Kolmogorov

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

English

For AE Kolmogorov process h, for every t, X_t equals almost surely h.mk X t.

Русский

Для AE Kolmogorov-процесса h, для каждого t, X_t =_{a.e.} h.mk X t.

LaTeX

$$$\\forall t,\\ X_t =_{a.e.} h.mk X_t$$$

Lean4

theorem ae_eq_mk (h : IsAEKolmogorovProcess X P p q M) : ∀ t, X t =ᵐ[P] h.mk X t :=
  (Classical.choose_spec h).2

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

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

Разделы

Аффилиация

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