Pre-Brownian motion as a projective limit

def ProbabilityTheory.brownianCovMatrix {ι : Type u_1} (I : ι → NNReal) : Matrix ι ι ℝ

Equations

• ProbabilityTheory.brownianCovMatrix I = Matrix.of fun (i j : ι) => min ↑(I i) ↑(I j)

theorem ProbabilityTheory.posSemidef_brownianCovMatrix {ι : Type u_1} [Fintype ι] (I : ι → NNReal) : (brownianCovMatrix I).PosSemidef

noncomputable def ProbabilityTheory.gaussianProjectiveFamilyAux {d : ℕ} (I : Fin d → NNReal) : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))

Equations

• ProbabilityTheory.gaussianProjectiveFamilyAux I = ProbabilityTheory.multivariateGaussian 0 (ProbabilityTheory.brownianCovMatrix I) ⋯

instance ProbabilityTheory.isGaussian_gaussianProjectiveFamilyAux {d : ℕ} (I : Fin d → NNReal) : IsGaussian (gaussianProjectiveFamilyAux I)

noncomputable def ProbabilityTheory.gaussianProjectiveFamily (I : Finset NNReal) : MeasureTheory.Measure ({ x : NNReal // x ∈ I } → ℝ)

Equations

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

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

theorem ProbabilityTheory.isProjectiveMeasureFamily_gaussianProjectiveFamily : MeasureTheory.IsProjectiveMeasureFamily gaussianProjectiveFamily

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

Equations

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

theorem ProbabilityTheory.isProjectiveLimit_gaussianLimit : MeasureTheory.IsProjectiveLimit gaussianLimit gaussianProjectiveFamily