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.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.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.measurePreserving_gaussianProjectiveFamily {I : Finset NNReal} {s : { x : NNReal // x ∈ I }} : MeasureTheory.MeasurePreserving (fun (x : { x : NNReal // x ∈ I } → ℝ) => x s) (gaussianProjectiveFamily I) (gaussianReal 0 ↑s)

theorem ProbabilityTheory.measurePreserving_gaussianProjectiveFamily₂ {I : Finset NNReal} {s t : { x : NNReal // x ∈ I }} : MeasureTheory.MeasurePreserving ((fun (x : { x : NNReal // x ∈ I } → ℝ) => x s) - fun (x : { x : NNReal // x ∈ I } → ℝ) => x t) (gaussianProjectiveFamily I) (gaussianReal 0 (max (↑s - ↑t) (↑t - ↑s)))

theorem ProbabilityTheory.isProjectiveMeasureFamily_gaussianProjectiveFamily : MeasureTheory.IsProjectiveMeasureFamily gaussianProjectiveFamily

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.measurePreserving_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 ι} : MeasurePreserving I.restrict μ (P I)

theorem ProbabilityTheory.measurePreserving_gaussianLimit {I : Finset NNReal} : MeasureTheory.MeasurePreserving I.restrict gaussianLimit (gaussianProjectiveFamily I)