Gaussian processes #
def
ProbabilityTheory.IsGaussianProcess
{T : Type u_1}
{Ω : Type u_2}
{E : 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.
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}
{mΩ : 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)
: