Gaussian processes

In this file we define a Gaussian process as a stochastic process whose finite dimensional distributions are Gaussian.

Main definition

• IsGaussianProcess X P: The stochastic process X is Gaussian under the measure P.

Tags

Gaussian process

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

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

• hasGaussianLaw (I : Finset T) : HasGaussianLaw (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P