English
The property AE KolmogorovProcess(X, P, p, q, M) holds if there exists a process Y that satisfies IsKolmogorovProcess with the same P, p, q, M and X t equals Y t almost everywhere for every t.
Русский
Свойство AE KolmogorovProcess(X, P, p, q, M) выполняется, если существует процесс Y, удовлетворяющий IsKolmogorovProcess с тем же P, p, q, M, и X t равно Y t почти нигде для каждого t.
LaTeX
$$$IsAEKolmogorovProcess\\ X\\ P\\ p\\ q\\ M := \\exists Y, IsKolmogorovProcess\\ Y\\ P\\ p\\ q\\ M \\land \\forall t,\\ X_t =\\!\\!\\mathrm{ae} P\\, Y_t$$$
Lean4
/-- Property of being a modification of a stochastic process that satisfies the Kolmogorov
condition (`IsKolmogorovProcess`). -/
def IsAEKolmogorovProcess (X : T → Ω → E) (P : Measure Ω) (p q : ℝ) (M : ℝ≥0) : Prop :=
∃ Y, IsKolmogorovProcess Y P p q M ∧ ∀ t, X t =ᵐ[P] Y t
