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
- ProbabilityTheory.IsGaussianProcess X P = ∀ (I : Finset T), ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P)
Instances For
theorem
ProbabilityTheory.IsGaussianProcess.modification
{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)
:
instance
ProbabilityTheory.instBorelSpaceForallOfSubsingleton_brownianMotion
{E : Type u_4}
{ι : Type u_5}
[TopologicalSpace E]
[MeasurableSpace E]
[BorelSpace E]
[Subsingleton ι]
:
BorelSpace (ι → E)
theorem
ProbabilityTheory.IsGaussianProcess.isGaussian_eval
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : 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)
:
IsGaussian (MeasureTheory.Measure.map (X t) P)