Gaussian processes #
This file contains basic properties of Gaussian processes. In particular,
in IsGaussianProcess.of_isGaussianProcess, we show that if a stochastic
process Y : S → Ω → F is such that for each s : S, Y s can be written as a linear map
applied to finitely many values of a certain Gaussian process,
then Y is itself a Gaussian process.
Main statement #
IsGaussianProcess.of_isGaussianProcess: If a stochastic processY : S → Ω → Fis such that for eachs : S,Y scan be written as a linear map applied to finitely many values of a certain Gaussian process, thenYis itself a Gaussian process.
Tags #
Gaussian process
Basic facts #
theorem
ProbabilityTheory.IsGaussianProcess.isProbabilityMeasure
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
(hX : IsGaussianProcess X P)
:
theorem
ProbabilityTheory.IsGaussianProcess.aemeasurable
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{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.congr
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{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)
:
A modification of a Gaussian process is a Gaussian process.
Gaussian Marginals #
theorem
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_eval
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
(hX : IsGaussianProcess X P)
(t : T)
:
HasGaussianLaw (X t) P
theorem
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_prodMk
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(hX : IsGaussianProcess X P)
{s t : T}
:
HasGaussianLaw (fun (ω : Ω) => (X s ω, X t ω)) P
theorem
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_add
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(hX : IsGaussianProcess X P)
{s t : T}
:
HasGaussianLaw (X s + X t) P
theorem
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_fun_add
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(hX : IsGaussianProcess X P)
{s t : T}
:
HasGaussianLaw (fun (ω : Ω) => X s ω + X t ω) P
theorem
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_sub
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(hX : IsGaussianProcess X P)
{s t : T}
:
HasGaussianLaw (X s - X t) P
theorem
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_fun_sub
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(hX : IsGaussianProcess X P)
{s t : T}
:
HasGaussianLaw (fun (ω : Ω) => X s ω - X t ω) P
theorem
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_sum
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(hX : IsGaussianProcess X P)
{I : Finset T}
:
HasGaussianLaw (∑ i ∈ I, X i) P
theorem
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_fun_sum
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(hX : IsGaussianProcess X P)
{I : Finset T}
:
HasGaussianLaw (fun (ω : Ω) => ∑ i ∈ I, X i ω) P
theorem
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_increments
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(hX : IsGaussianProcess X P)
{n : ℕ}
{t : Fin (n + 1) → T}
:
HasGaussianLaw (fun (ω : Ω) (i : Fin n) => X (t i.succ) ω - X (t i.castSucc) ω) P
The increments of a Gaussian process are Gaussian.
Operations that preserve Gaussianity #
theorem
ProbabilityTheory.IsGaussianProcess.of_isGaussianProcess
{S : Type u_1}
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
[SecondCountableTopology F]
{Y : S → Ω → F}
(hX : IsGaussianProcess X P)
(h : ∀ (s : S), ∃ (I : Finset T) (L : (↥I → E) →L[ℝ] F), ∀ (ω : Ω), Y s ω = L (I.restrict fun (x : T) => X x ω))
:
If a stochastic process Y is such that for each s, Y s can be written as a linear
combination of finitely many values of a Gaussian process, then Y is a Gaussian process.
theorem
ProbabilityTheory.IsGaussianProcess.comp_right
{S : Type u_1}
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(h : IsGaussianProcess X P)
(f : S → T)
:
IsGaussianProcess (X ∘ f) P
theorem
ProbabilityTheory.IsGaussianProcess.comp_left
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
[SecondCountableTopology F]
(L : T → E →L[ℝ] F)
(h : IsGaussianProcess X P)
:
IsGaussianProcess (fun (t : T) (ω : Ω) => (L t) (X t ω)) P
theorem
ProbabilityTheory.IsGaussianProcess.smul
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(c : T → ℝ)
(hX : IsGaussianProcess X P)
:
IsGaussianProcess (fun (t : T) (ω : Ω) => c t • X t ω) P
theorem
ProbabilityTheory.IsGaussianProcess.shift
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
[Add T]
(h : IsGaussianProcess X P)
(t₀ : T)
:
IsGaussianProcess (fun (t : T) (ω : Ω) => X (t₀ + t) ω - X t₀ ω) P
theorem
ProbabilityTheory.IsGaussianProcess.restrict
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
(h : IsGaussianProcess X P)
(s : Set T)
:
IsGaussianProcess (fun (t : ↑s) => X ↑t) P