Gaussian processes #
In this file we define a Gaussian process as a stochastic process whose finite dimensional ditributions are Gaussian.
Main definition #
IsGaussianProcess X P: The stochastic processXis Gaussian under the measureP.
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)
:
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