Documentation

BrownianMotion.Gaussian.GaussianProcess

Gaussian processes #

def ProbabilityTheory.IsGaussianProcess {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} [MeasurableSpace E] [TopologicalSpace E] [AddCommMonoid E] [Module E] (X : TΩE) (P : MeasureTheory.Measure Ω := by volume_tac) :

A stochastic process is a Gaussian process if all its finite dimensional distributions are Gaussian.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem ProbabilityTheory.IsGaussianProcess.version {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : TΩE} [MeasurableSpace E] [TopologicalSpace E] [AddCommMonoid E] [Module E] (hX : IsGaussianProcess X P) (hXY : ∀ (t : T), X t =ᵐ[P] Y t) :