Gaussian processes #
class
ProbabilityTheory.IsGaussianProcess
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{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.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.modification
{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]
[IsGaussianProcess X P]
(hXY : ∀ (t : T), X t =ᵐ[P] Y t)
:
instance
ProbabilityTheory.instBorelSpaceForallOfSubsingleton_brownianMotion
{E : Type u_6}
{ι : Type u_7}
[TopologicalSpace E]
[MeasurableSpace E]
[BorelSpace E]
[Subsingleton ι]
:
BorelSpace (ι → E)
instance
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]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[IsGaussianProcess X P]
(t : T)
:
HasGaussianLaw (X t) P
instance
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]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[IsGaussianProcess X P]
{s t : T}
:
HasGaussianLaw (X s - X t) P
instance
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]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[IsGaussianProcess X P]
{s t : T}
:
HasGaussianLaw (fun (ω : Ω) => X s ω - X t ω) P
instance
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]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[IsGaussianProcess X P]
{n : ℕ}
{t : Fin (n + 1) → T}
:
HasGaussianLaw (fun (ω : Ω) (i : Fin n) => X (t i.succ) ω - X (t i.castSucc) ω) P
theorem
ProbabilityTheory.IsGaussianProcess.indepFun
{S : Type u_1}
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
{X : S → Ω → E}
{Y : T → Ω → E}
(h : IsGaussianProcess (Sum.elim X Y) P)
(hX : ∀ (s : S), Measurable (X s))
(hY : ∀ (t : T), Measurable (Y t))
(h' : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), covariance (⇑L₁ ∘ X s) (⇑L₂ ∘ Y t) P = 0)
:
IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P
theorem
ProbabilityTheory.IsGaussianProcess.iIndepFun
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
{S : T → Type u_6}
{X : (t : T) → S t → Ω → E}
(h : IsGaussianProcess (fun (p : (t : T) × S t) (ω : Ω) => X p.fst p.snd ω) P)
(hX : ∀ (t : T) (s : S t), Measurable (X t s))
(h' :
∀ (t₁ t₂ : T),
t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), covariance (⇑L₁ ∘ X t₁ s₁) (⇑L₂ ∘ X t₂ s₂) P = 0)
:
ProbabilityTheory.iIndepFun (fun (t : T) (ω : Ω) (s : S t) => X t s ω) P
theorem
ProbabilityTheory.IsGaussianProcess.indepFun'
{S : Type u_1}
{T : Type u_2}
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_6}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
{X : S → Ω → E}
{Y : T → Ω → E}
(h : IsGaussianProcess (Sum.elim X Y) P)
(hX : ∀ (s : S), Measurable (X s))
(hY : ∀ (t : T), Measurable (Y t))
(h' :
∀ (s : S) (t : T) (x y : E), covariance (fun (ω : Ω) => inner ℝ x (X s ω)) (fun (ω : Ω) => inner ℝ y (Y t ω)) P = 0)
:
IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P
theorem
ProbabilityTheory.IsGaussianProcess.iIndepFun'
{T : Type u_2}
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_6}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
{S : T → Type u_7}
{X : (t : T) → S t → Ω → E}
(h : IsGaussianProcess (fun (p : (t : T) × S t) (ω : Ω) => X p.fst p.snd ω) P)
(hX : ∀ (t : T) (s : S t), Measurable (X t s))
(h' :
∀ (t₁ t₂ : T),
t₁ ≠ t₂ →
∀ (s₁ : S t₁) (s₂ : S t₂) (x y : E),
covariance (fun (ω : Ω) => inner ℝ x (X t₁ s₁ ω)) (fun (ω : Ω) => inner ℝ y (X t₂ s₂ ω)) P = 0)
:
ProbabilityTheory.iIndepFun (fun (t : T) (ω : Ω) (s : S t) => X t s ω) P
theorem
ProbabilityTheory.IsGaussianProcess.indepFun''
{S : Type u_1}
{T : Type u_2}
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : S → Ω → ℝ}
{Y : T → Ω → ℝ}
(h : IsGaussianProcess (Sum.elim X Y) P)
(hX : ∀ (s : S), Measurable (X s))
(hY : ∀ (t : T), Measurable (Y t))
(h' : ∀ (s : S) (t : T), covariance (X s) (Y t) P = 0)
:
IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P
theorem
ProbabilityTheory.IsGaussianProcess.iIndepFun''
{T : Type u_2}
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{S : T → Type u_6}
{X : (t : T) → S t → Ω → ℝ}
(h : IsGaussianProcess (fun (p : (t : T) × S t) (ω : Ω) => X p.fst p.snd ω) P)
(hX : ∀ (t : T) (s : S t), Measurable (X t s))
(h' : ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂), covariance (X t₁ s₁) (X t₂ s₂) P = 0)
:
ProbabilityTheory.iIndepFun (fun (t : T) (ω : Ω) (s : S t) => X t s ω) P
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]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[IsGaussianProcess X P]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
[SecondCountableTopology F]
{Y : S → Ω → F}
(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 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]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace 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]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace 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
instance
ProbabilityTheory.IsGaussianProcess.smul
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
(c : T → ℝ)
[IsGaussianProcess X P]
:
IsGaussianProcess (fun (t : T) (ω : Ω) => c t • X t ω) P
instance
ProbabilityTheory.IsGaussianProcess.shift
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[Add T]
[h : IsGaussianProcess X P]
(t₀ : T)
:
IsGaussianProcess (fun (t : T) (ω : Ω) => X (t₀ + t) ω - X t₀ ω) P
instance
ProbabilityTheory.IsGaussianProcess.restrict
{T : Type u_2}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[h : IsGaussianProcess X P]
(s : Set T)
:
IsGaussianProcess (fun (t : ↑s) => X ↑t) P