aemeasurable_edist — Mathlib

English

For a KolmogorovProcess X, the edist function between X_s and X_t is AE-measurable in ω.

Русский

Для Kolmogorov-процесса X функция edist(X_s, X_t) измерима почти всюду по ω.

LaTeX

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

Lean4

theorem aemeasurable_edist (hX : IsAEKolmogorovProcess X P p q M) {s t : T} :
    AEMeasurable (fun ω ↦ edist (X s ω) (X t ω)) P :=
  hX.aestronglyMeasurable_edist.aemeasurable

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