measurable_edist

Mathlib.Probability.Process.Kolmogorov

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

← MathLib Explorer

English

For a KolmogorovProcess X, the map ω ↦ edist(X_s ω, X_t ω) is measurable.

Русский

Для Kolmogorov-процесса X отображение ω ↦ edist(X_s ω, X_t ω) измеримо.

LaTeX

$$$\\text{Measurable}(\\lambda \\omega. edist(X_s\\omega, X_t\\omega))$$$

Lean4

theorem measurable_edist (hX : IsKolmogorovProcess X P p q M) {s t : T} : Measurable (fun ω ↦ edist (X s ω) (X t ω)) :=
  hX.stronglyMeasurable_edist.measurable

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

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

Разделы

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

Аффилиация

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