Pre-Brownian motion as a projective limit

theorem L2.posSemidef_interMatrix {ι : Type u_1} [Finite ι] {α : 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

def ProbabilityTheory.brownianCovMatrix (I : Finset NNReal) : Matrix ↥I ↥I ℝ

Equations

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

theorem ProbabilityTheory.brownianCovMatrix_apply {I : Finset NNReal} (s t : ↥I) : brownianCovMatrix I s t = ↑(min ↑s ↑t)

theorem ProbabilityTheory.brownianCovMatrix_submatrix {I J : Finset NNReal} (hJI : J ⊆ I) : ((brownianCovMatrix I).submatrix (fun (i : ↥J) => ⟨↑i, ⋯⟩) fun (i : ↥J) => ⟨↑i, ⋯⟩) = brownianCovMatrix J

theorem ProbabilityTheory.posSemidef_brownianCovMatrix (I : Finset NNReal) : (brownianCovMatrix I).PosSemidef

noncomputable def ProbabilityTheory.gaussianProjectiveFamily (I : Finset NNReal) : MeasureTheory.Measure (↥I → ℝ)

Equations

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

theorem ProbabilityTheory.measurePreserving_equiv_multivariateGaussian (I : Finset NNReal) : MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) (multivariateGaussian 0 (brownianCovMatrix I)) (gaussianProjectiveFamily I)

theorem ProbabilityTheory.measurePreserving_equiv_gaussianProjectiveFamily (I : Finset NNReal) : MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm.symm) (gaussianProjectiveFamily I) (multivariateGaussian 0 (brownianCovMatrix I))

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)

instance ProbabilityTheory.isGaussian_gaussianProjectiveFamily (I : Finset NNReal) : IsGaussian (gaussianProjectiveFamily I)

@[simp]

theorem ProbabilityTheory.integral_id_gaussianProjectiveFamily (I : Finset NNReal) : ∫ (x : ↥I → ℝ), x ∂gaussianProjectiveFamily I = 0

theorem ProbabilityTheory.integral_id_gaussianProjectiveFamily' (I : Finset NNReal) : ∫ (x : ↥I → ℝ), id x ∂gaussianProjectiveFamily I = 0

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)

theorem ProbabilityTheory.variance_eval_gaussianProjectiveFamily {I : Finset NNReal} (s : ↥I) : variance (fun (x : ↥I → ℝ) => x s) (gaussianProjectiveFamily I) = ↑↑s

theorem ProbabilityTheory.hasLaw_eval_gaussianProjectiveFamily {I : Finset NNReal} (s : ↥I) : HasLaw (fun (x : ↥I → ℝ) => x s) (gaussianReal 0 ↑s) (gaussianProjectiveFamily I)

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)

theorem ProbabilityTheory.isProjectiveMeasureFamily_gaussianProjectiveFamily : MeasureTheory.IsProjectiveMeasureFamily gaussianProjectiveFamily

theorem ProbabilityTheory.measurePreserving_restrict_gaussianProjectiveFamily {I J : Finset NNReal} (hIJ : I ⊆ J) : MeasureTheory.MeasurePreserving (Finset.restrict₂ hIJ) (gaussianProjectiveFamily J) (gaussianProjectiveFamily I)

noncomputable def ProbabilityTheory.gaussianLimit : MeasureTheory.Measure (NNReal → ℝ)

Equations

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

instance ProbabilityTheory.IsProbabilityMeasure_gaussianLimit : MeasureTheory.IsProbabilityMeasure gaussianLimit

theorem ProbabilityTheory.isProjectiveLimit_gaussianLimit : MeasureTheory.IsProjectiveLimit gaussianLimit gaussianProjectiveFamily

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) μ

theorem ProbabilityTheory.hasLaw_restrict_gaussianLimit {I : Finset NNReal} : HasLaw I.restrict (gaussianProjectiveFamily I) gaussianLimit

theorem ProbabilityTheory.hasLaw_eval_gaussianLimit {t : NNReal} : HasLaw (fun (x : NNReal → ℝ) => x t) (gaussianReal 0 t) gaussianLimit

theorem ProbabilityTheory.covariance_eval_gaussianLimit {s t : NNReal} : covariance (fun (x : NNReal → ℝ) => x s) (fun (x : NNReal → ℝ) => x t) gaussianLimit = ↑(min s t)