Pre-Brownian motion as a projective limit

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

def ProbabilityTheory.brownianCovMatrix (I : Finset NNReal) : Matrix { x : NNReal // x ∈ I } { x : NNReal // x ∈ I } ℝ

Equations

• ProbabilityTheory.brownianCovMatrix I = Matrix.of fun (s t : { x : NNReal // x ∈ I }) => min ↑↑s ↑↑t

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

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

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

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.

theorem ProbabilityTheory.measurePreserving_equiv_multivariateGaussian (I : Finset NNReal) : MeasureTheory.MeasurePreserving (⇑(EuclideanSpace.measurableEquiv { x : NNReal // x ∈ I })) (multivariateGaussian 0 (brownianCovMatrix I) ⋯) (gaussianProjectiveFamily I)

theorem ProbabilityTheory.measurePreserving_equiv_gaussianProjectiveFamily (I : Finset NNReal) : MeasureTheory.MeasurePreserving (⇑(EuclideanSpace.measurableEquiv { x : NNReal // x ∈ I }).symm) (gaussianProjectiveFamily I) (multivariateGaussian 0 (brownianCovMatrix I) ⋯)

theorem ProbabilityTheory.integral_gaussianProjectiveFamily {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (I : Finset NNReal) (f : ({ x : NNReal // x ∈ I } → ℝ) → E) : ∫ (x : { x : NNReal // x ∈ I } → ℝ), f x ∂gaussianProjectiveFamily I = ∫ (x : EuclideanSpace ℝ { x : NNReal // x ∈ I }), f ((EuclideanSpace.equiv { x : NNReal // x ∈ 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 : { x : NNReal // x ∈ I } → ℝ), x ∂gaussianProjectiveFamily I = 0

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

theorem ProbabilityTheory.covariance_eval_gaussianProjectiveFamily {I : Finset NNReal} (s t : { x : NNReal // x ∈ I }) : covariance (fun (x : { x : NNReal // x ∈ I } → ℝ) => x s) (fun (x : { x : NNReal // x ∈ I } → ℝ) => x t) (gaussianProjectiveFamily I) = ↑(min ↑s ↑t)

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

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

theorem ProbabilityTheory.hasLaw_eval_sub_eval_gaussianProjectiveFamily {I : Finset NNReal} {s t : { x : NNReal // x ∈ I }} : HasLaw (fun (x : { x : NNReal // 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 : { x : ι // x ∈ 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