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
Instances For
    theorem ProbabilityTheory.IsGaussianProcess.modification {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) :
    theorem ProbabilityTheory.IsGaussianProcess.isGaussian_eval {T : Type u_1} {Ω : Type u_2} {E : Type u_3} { : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : TΩE} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] (hX : IsGaussianProcess X P) (t : T) (hX' : AEMeasurable (X t) P) :