edist_eq_zero_of_const_eq_zero — Mathlib

English

Let X be an IsKolmogorovProcess with parameters p, q and 0. Then for every s,t in T, the inequality edist(X_s(ω), X_t(ω)) = 0 holds almost surely with respect to P.

Русский

Пусть X — процесс IsKolmogorov с параметрами p, q и 0. Тогда для любых s,t ∈ T выполняется, что edist(X_s(ω), X_t(ω)) = 0 почти наверняка по мере P.

LaTeX

$$$$ \forall s,t : T, \ \forall^\omega \partial P, \ edist(X_s(\omega), X_t(\omega)) = 0. $$$$

Lean4

theorem edist_eq_zero_of_const_eq_zero (hX : IsKolmogorovProcess X P p q 0) (s t : T) :
    ∀ᵐ ω ∂P, edist (X s ω) (X t ω) = 0 :=
  hX.IsAEKolmogorovProcess.edist_eq_zero_of_const_eq_zero s t

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