A stochastic process with independent increments and Gaussian marginals is Gaussian

We prove that a stochastic process with independent increments and Gaussian marginals is Gaussian. To do so, we first define I.orderEmbOfFinWithBot : Fin (#I + 1) → T, which is the map (⊥, t₁, ..., tₙ), where t₁ < ... < tₙ are the elements of I and ⊥ is the smallest element of T.

Assume then that X is a stochastic process with independent increments and Gaussian marginals, and such that X ⊥ = 0 almost surely. Then X tᵢ = ∑ j ≤ i-1, (X tⱼ₊₁ - X tⱼ). Therefore the vector (X t₁, ..., X tₙ) can be obtained from the vector of the increments by a linear map. It remains to show that the vector of the increments is Gaussian. Because increments are independent, it is enough to show that each increment is Gaussian. This follows from the fact that X tᵢ and X tᵢ₊₁ are Gaussian, and X tᵢ and X tᵢ₊₁ - X tᵢ are independent (see IndepFun.hasGaussianLaw_sub_of_sub).

Main statement

• HasIndepIncrements.isGaussianProcess: A stochastic process X with independent increments, such that X t is Gaussian for all t and such that X ⊥ = 0 almost surely is a Gaussian process.

Tags

independent increments, Gaussian process

theorem ProbabilityTheory.HasIndepIncrements.isGaussianProcess {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder T] [OrderBot T] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {X : T → Ω → E} (law : ∀ (t : T), HasGaussianLaw (X t) P) (h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0) (incr : HasIndepIncrements X P) : IsGaussianProcess X P

A stochastic process X with independent increments, such that X t is Gaussian for all t and such that X ⊥ = 0 almost surely is a Gaussian process.