Theorems · Theorem · probability

ProbabilityTheory.IsGaussianProcess.isPreBrownianReal_of_covariance

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsGaussianProcess X P →
    (∀ (t : NNReal), ∫ (x : Ω), X t x ∂P = 0) →
      (∀ (s t : NNReal), s ≤ t → ProbabilityTheory.covariance (X s) (X t) P = ↑s) →
        ProbabilityTheory.IsPreBrownianReal X P

A centered Gaussian process with the right covariance is a pre-Brownian motion.

Defined in

Mathlib.Probability.BrownianMotion.Basic

Cited by

4 results in Mathlib

Foundations

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