Documentation

LeanPool.MarkovProcess.MarkovProcess.Kernel.KolmogorovMoments

Intrinsic Kolmogorov moment bounds for a transition semigroup #

Kolmogorov's continuity criterion is usually imposed on an already constructed coordinate process. This file states the same criterion directly on the transition semigroup: the p-th moment of the displacement accumulated over a time step h is at most M * h ^ q, uniformly in the starting point.

The predicate is purely a moment bound on the transition kernels. It makes no path-space, continuity, or stochastic-process claim; the transport of this bound to the canonical dense-time coordinate process is proved elsewhere.

source
def MarkovProcess.SubMarkovKernelSemigroup.HasKolmogorovMoments {alpha : Type u_1} [PseudoEMetricSpace alpha] [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (p q : ℝ) (M : NNReal) :
Prop

A uniform p-th moment bound on the displacement of P over time h, of order h ^ q.

The exponents are constrained by 0 < p and 1 < q, exactly the range in which the Kolmogorov--Chentsov threshold (q - 1) / p is a positive Hölder exponent. The bound is demanded for every time h ≥ 0, not only for small h; this is stronger than the local criterion the Kolmogorov--Chentsov theorem needs, and it is what the bridge to KolmogorovRegular consumes.

Equations
Instances For
    source
    theorem MarkovProcess.SubMarkovKernelSemigroup.HasKolmogorovMoments.p_pos {alpha : Type u_1} [PseudoEMetricSpace alpha] [MeasurableSpace alpha] {P : SubMarkovKernelSemigroup alpha} {p q : ℝ} {M : NNReal} (hmom : P.HasKolmogorovMoments p q M) :
    0 < p

    The moment exponent of a Kolmogorov moment bound is positive.

    source
    theorem MarkovProcess.SubMarkovKernelSemigroup.HasKolmogorovMoments.one_lt_q {alpha : Type u_1} [PseudoEMetricSpace alpha] [MeasurableSpace alpha] {P : SubMarkovKernelSemigroup alpha} {p q : ℝ} {M : NNReal} (hmom : P.HasKolmogorovMoments p q M) :
    1 < q

    The time exponent of a Kolmogorov moment bound is strictly larger than one.

    source
    theorem MarkovProcess.SubMarkovKernelSemigroup.HasKolmogorovMoments.q_pos {alpha : Type u_1} [PseudoEMetricSpace alpha] [MeasurableSpace alpha] {P : SubMarkovKernelSemigroup alpha} {p q : ℝ} {M : NNReal} (hmom : P.HasKolmogorovMoments p q M) :
    0 < q

    The time exponent of a Kolmogorov moment bound is positive.

    source
    theorem MarkovProcess.SubMarkovKernelSemigroup.HasKolmogorovMoments.lintegral_edist_le {alpha : Type u_1} [PseudoEMetricSpace alpha] [MeasurableSpace alpha] {P : SubMarkovKernelSemigroup alpha} {p q : ℝ} {M : NNReal} (hmom : P.HasKolmogorovMoments p q M) (h : NNReal) (y : alpha) :
    ∫⁻ (z : alpha), edist z y ^ p ∂(P.kernel h) y ≤ ↑M * ↑h ^ q

    The displacement moment estimate carried by a Kolmogorov moment bound.

    source
    theorem MarkovProcess.SubMarkovKernelSemigroup.HasKolmogorovMoments.exists_holderExponent {alpha : Type u_1} [PseudoEMetricSpace alpha] [MeasurableSpace alpha] {P : SubMarkovKernelSemigroup alpha} {p q : ℝ} {M : NNReal} (hmom : P.HasKolmogorovMoments p q M) :
    ∃ (gamma : ℝ), 0 < gamma ∧ gamma < (q - 1) / p

    A Kolmogorov moment bound admits a strictly positive Hölder exponent below the Kolmogorov--Chentsov threshold (q - 1) / p; the witness (q - 1) / (2 * p) is used.