Kolmogorov Process Increment Tail Bound

This statement gives the Markov–Chebyshev tail estimate associated with a Kolmogorov process.

Let $\Omega$ be a measurable space, let $P$ be a probability measure on $\Omega$, and let $X : \mathbb{R} \to \Omega \to \mathbb{R}$ be a real-valued process. Let $p,q \in \mathbb{R}$ and $M \in [0,\infty)$, and assume the process satisfies ProbabilityTheory.IsKolmogorovProcess X P p q M. For arbitrary times $s,t \in \mathbb{R}$, let $\lambda \in [0,\infty]$ satisfy:

1. $0 < \lambda$;
2. $\lambda \ne \infty$.

Writing edist for the extended distance, the probability of an increment exceeding the threshold $\lambda$ is bounded by

Here the right-hand side is interpreted in $[0,\infty]$, with $M$ coerced from $[0,\infty)$ to ENNReal; the powers are extended-real powers. This is a per-pair increment tail estimate that can be reused in convergence-in-measure and summability arguments for continuous modifications of stochastic processes.

Formalization Note The measure-valued quantity and all arithmetic in the conclusion use ENNReal; the hypotheses require the threshold to be strictly positive and not equal to ⊤.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Continuity. Shown in its original module context. Proof omitted.

lemma kolmogorov_markov_bound
    (P : Measure Ω) [IsProbabilityMeasure P]
    (X : ℝ → Ω → ℝ) {p q : ℝ} {M : ℝ≥0}
    (hX : ProbabilityTheory.IsKolmogorovProcess X P p q M)
    (s t : ℝ) {lam : ℝ≥0∞} (hlam_pos : 0 < lam) (hlam_top : lam ≠ ⊤) :
    P {ω | lam ≤ edist (X s ω) (X t ω)}
      ≤ (M : ℝ≥0∞) * edist s t ^ q / lam ^ p

Module navigation

Module: LevyStochCalc/Brownian/ContinuityKolmogorovBounds.

Next: kc_level_bad_measure.

Source excerpt, lines 42–48 · Frozen source 408915f.