Gaussian processes #
class
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.
- hasGaussianLaw (I : Finset T) : HasGaussianLaw (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P
Instances
theorem
ProbabilityTheory.IsGaussianProcess.aemeasurable
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[hX : IsGaussianProcess X P]
(t : T)
:
AEMeasurable (X t) P
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]
[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)
instance
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_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]
[IsGaussianProcess X P]
{t : T}
:
HasGaussianLaw (X t) P
instance
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_sub
{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]
[SecondCountableTopology E]
[IsGaussianProcess X P]
{s t : T}
:
HasGaussianLaw (X s - X t) P