kolmogorovCondition — Mathlib

English

If X is an AE KolmogorovProcess, then for all s,t we have the Kolmogorov integral bound: ∫ edist(...)^p dP ≤ M edist(s,t)^q.

Русский

Если X — AE Kolmogorov-процесс, то для всех s,t выполняется неравенство Колмогорового интеграла: ∫ edist(...)^p dP ≤ M edist(s,t)^q.

LaTeX

$$$\\forall s,t,\\ \\int^-\\omega\\ edist(X_s\\omega,X_t\\omega)^p\\ dP \\le M\\, edist(s,t)^q$$$

Lean4

theorem kolmogorovCondition (hX : IsAEKolmogorovProcess X P p q M) (s t : T) :
    ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P ≤ M * edist s t ^ q :=
  by
  convert hX.IsKolmogorovProcess_mk.kolmogorovCondition s t using 1
  refine lintegral_congr_ae ?_
  filter_upwards [hX.ae_eq_mk s, hX.ae_eq_mk t] with ω hω₁ hω₂
  simp_rw [hω₁, hω₂]

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