measurable

Mathlib.Probability.Process.Kolmogorov

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.IsKolmogorovProcess.measurable

← MathLib Explorer

English

If edist(s,t) = 0, then edist(X_s ω, X_t ω) = 0 for almost every ω.

Русский

Если edist(s,t) = 0, то edist(X_s ω, X_t ω) = 0 почти наверняка по ω.

LaTeX

$$$\\text{If }\\ and\\ edist(s,t)=0,\\ then\\ edist(X_s\\omega, X_t\\omega)=0\\;\\text{a.e.}$$$

Lean4

theorem measurable (hX : IsKolmogorovProcess X P p q M) (s : T) : Measurable (X s) :=
  (measurable_fst.mono prod_le_borel_prod le_rfl).comp (hX.measurablePair s s)

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

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

Разделы

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

Аффилиация

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