# Pre-Brownian motion as a projective limit #

source
theorem L2.posSemidef_interMatrix {ι : Type u_1} [Fintype ι] {α : Type u_2} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {v : ι → Set α} (hv₁ : ∀ (j : ι), MeasurableSet (v j)) (hv₂ : ∀ (j : ι), μ (v j) ≠ ⊤ := by finiteness) :
(Matrix.of fun (i j : ι) => μ.real (v i ∩ v j)).PosSemidef
source
def ProbabilityTheory.brownianCovMatrix (I : Finset NNReal) :
Matrix ↥I ↥I ℝ
Equations

- ProbabilityTheory.brownianCovMatrix I = Matrix.of fun (s t : ↥I) => min ↑↑s ↑↑t

Instances For

source
theorem ProbabilityTheory.brownianCovMatrix_apply {I : Finset NNReal} (s t : ↥I) :
brownianCovMatrix I s t = ↑(min ↑s ↑t)
source
theorem ProbabilityTheory.brownianCovMatrix_submatrix {I J : Finset NNReal} (hJI : J ⊆ I) :
((brownianCovMatrix I).submatrix (fun (i : ↥J) => ⟨↑i, ⋯⟩) fun (i : ↥J) => ⟨↑i, ⋯⟩) = brownianCovMatrix J
source
theorem ProbabilityTheory.posSemidef_brownianCovMatrix (I : Finset NNReal) :
(brownianCovMatrix I).PosSemidef
source
noncomputable def ProbabilityTheory.gaussianProjectiveFamily (I : Finset NNReal) :
MeasureTheory.Measure (↥I → ℝ)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem ProbabilityTheory.measurePreserving_equiv_multivariateGaussian (I : Finset NNReal) :
MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) (multivariateGaussian 0 (brownianCovMatrix I)) (gaussianProjectiveFamily I)
source
theorem ProbabilityTheory.measurePreserving_equiv_gaussianProjectiveFamily (I : Finset NNReal) :
MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm.symm) (gaussianProjectiveFamily I) (multivariateGaussian 0 (brownianCovMatrix I))
source
theorem ProbabilityTheory.integral_gaussianProjectiveFamily {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (I : Finset NNReal) (f : (↥I → ℝ) → E) :
∫ (x : ↥I → ℝ), f x ∂gaussianProjectiveFamily I = ∫ (x : EuclideanSpace ℝ ↥I), f ((EuclideanSpace.equiv ↥I ℝ) x) ∂multivariateGaussian 0 (brownianCovMatrix I)
source
instance ProbabilityTheory.isGaussian_gaussianProjectiveFamily (I : Finset NNReal) :
IsGaussian (gaussianProjectiveFamily I)
source
@[simp]
theorem ProbabilityTheory.integral_id_gaussianProjectiveFamily (I : Finset NNReal) :
∫ (x : ↥I → ℝ), x ∂gaussianProjectiveFamily I = 0
source
theorem ProbabilityTheory.integral_id_gaussianProjectiveFamily' (I : Finset NNReal) :
∫ (x : ↥I → ℝ), id x ∂gaussianProjectiveFamily I = 0
source
theorem ProbabilityTheory.covariance_eval_gaussianProjectiveFamily (I : Finset NNReal) (s t : ↥I) :
covariance (fun (x : ↥I → ℝ) => x s) (fun (x : ↥I → ℝ) => x t) (gaussianProjectiveFamily I) = ↑(min ↑s ↑t)
source
theorem ProbabilityTheory.variance_eval_gaussianProjectiveFamily {I : Finset NNReal} (s : ↥I) :
variance (fun (x : ↥I → ℝ) => x s) (gaussianProjectiveFamily I) = ↑↑s
source
theorem ProbabilityTheory.hasLaw_eval_gaussianProjectiveFamily {I : Finset NNReal} (s : ↥I) :
HasLaw (fun (x : ↥I → ℝ) => x s) (gaussianReal 0 ↑s) (gaussianProjectiveFamily I)
source
theorem ProbabilityTheory.hasLaw_eval_sub_eval_gaussianProjectiveFamily (I : Finset NNReal) (s t : ↥I) :
HasLaw (fun (x : ↥I → ℝ) => x s - x t) (gaussianReal 0 (max (↑s - ↑t) (↑t - ↑s))) (gaussianProjectiveFamily I)
source
theorem ProbabilityTheory.isProjectiveMeasureFamily_gaussianProjectiveFamily :
MeasureTheory.IsProjectiveMeasureFamily gaussianProjectiveFamily
source
theorem ProbabilityTheory.measurePreserving_restrict_gaussianProjectiveFamily {I J : Finset NNReal} (hIJ : I ⊆ J) :
MeasureTheory.MeasurePreserving (Finset.restrict₂ hIJ) (gaussianProjectiveFamily J) (gaussianProjectiveFamily I)
source
noncomputable def ProbabilityTheory.gaussianLimit :
MeasureTheory.Measure (NNReal → ℝ)
Equations

- ProbabilityTheory.gaussianLimit = MeasureTheory.projectiveLimit ProbabilityTheory.gaussianProjectiveFamily ProbabilityTheory.isProjectiveMeasureFamily_gaussianProjectiveFamily

Instances For

source
instance ProbabilityTheory.IsProbabilityMeasure_gaussianLimit :
MeasureTheory.IsProbabilityMeasure gaussianLimit
source
theorem ProbabilityTheory.isProjectiveLimit_gaussianLimit :
MeasureTheory.IsProjectiveLimit gaussianLimit gaussianProjectiveFamily
source
theorem MeasureTheory.IsProjectiveLimit.hasLaw_restrict {ι : Type u_2} {X : ι → Type u_3} {mX : (i : ι) → MeasurableSpace (X i)} {μ : Measure ((i : ι) → X i)} {P : (I : Finset ι) → Measure ((i : ↥I) → X ↑i)} (h : IsProjectiveLimit μ P) {I : Finset ι} :
ProbabilityTheory.HasLaw I.restrict (P I) μ
source
theorem ProbabilityTheory.hasLaw_restrict_gaussianLimit {I : Finset NNReal} :
HasLaw I.restrict (gaussianProjectiveFamily I) gaussianLimit
source
theorem ProbabilityTheory.hasLaw_eval_gaussianLimit {t : NNReal} :
HasLaw (fun (x : NNReal → ℝ) => x t) (gaussianReal 0 t) gaussianLimit
source
theorem ProbabilityTheory.covariance_eval_gaussianLimit {s t : NNReal} :
covariance (fun (x : NNReal → ℝ) => x s) (fun (x : NNReal → ℝ) => x t) gaussianLimit = ↑(min s t)