edist_eq_zero — Mathlib

English

Repeated statement: under IsKolmogorovProcess, if edist s t = 0 then edist(X_s ω, X_t ω) = 0 a.e.

Русский

Повторно: при IsKolmogorovProcess, если edist(s,t)=0, то edist(X_s ω, X_t ω) = 0 почти surely.

LaTeX

$$$\\forall s,t,\\ edist(s,t)=0 \\Rightarrow \\ edist(X_s, X_t)=0\\; \\text{a.e.}$$$

Lean4

theorem edist_eq_zero (hX : IsAEKolmogorovProcess X P p q M) {s t : T} (h : edist s t = 0) :
    ∀ᵐ ω ∂P, edist (X s ω) (X t ω) = 0 :=
  by
  suffices ∀ᵐ ω ∂P, edist (X s ω) (X t ω) ^ p = 0
    by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω
  refine (lintegral_eq_zero_iff' (hX.aemeasurable_edist.pow_const p)).mp ?_
  refine le_antisymm ?_ zero_le'
  calc
    ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P
    _ ≤ M * edist s t ^ q := (hX.kolmogorovCondition s t)
    _ = 0 := by simp [h, hX.q_pos]

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