Theorems · Inductive type · probability

ProbabilityTheory.IsKolmogorovProcess

{T : Type u_1} →
  {Ω : Type u_2} →
    {E : Type u_3} →
      [PseudoEMetricSpace T] →
        {mΩ : MeasurableSpace Ω} →
          [PseudoEMetricSpace E] → (T → Ω → E) → MeasureTheory.Measure Ω → ℝ → ℝ → NNReal → Prop

A stochastic process X : T → Ω → E on an index space T and a measurable space Ω with measure P is said to satisfy the Kolmogorov condition with exponents p, q and constant M if for all s, t : T, the pair (X s, X t) is measurable for the Borel sigma-algebra on E × E and the following condition holds: ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P ≤ M * edist s t ^ q.

Defined in

Mathlib.Probability.Process.Kolmogorov

Cited by

12 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpacePseudoEMetricSpace