aestronglyMeasurable_edist — Mathlib

English

If X is a KolmogorovProcess, then ω ↦ edist(X_s ω, X_t ω) is AES strongly measurable (ae-almost everywhere).

Русский

Если X — Kolmogorov-процесс, то функция ω ↦ edist(X_s ω, X_t ω) является AES сильно измеримой (на почти всюм меры).

LaTeX

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

Lean4

theorem aestronglyMeasurable_edist (hX : IsAEKolmogorovProcess X P p q M) {s t : T} :
    AEStronglyMeasurable (fun ω ↦ edist (X s ω) (X t ω)) P :=
  by
  refine ⟨(fun ω ↦ edist (hX.mk X s ω) (hX.mk X t ω)), hX.IsKolmogorovProcess_mk.stronglyMeasurable_edist, ?_⟩
  filter_upwards [hX.ae_eq_mk s, hX.ae_eq_mk t] with ω hω₁ hω₂ using by simp [hω₁, hω₂]

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