Finite dimensional distributions of Brownian motion

In this file we define projectiveFamily : (I : Finset ℝ≥0) → Measure (I → ℝ). Each projectiveFamily I is the centered Gaussian measure over I → ℝ with covariance matrix given by covMatrix I s t := min s t. Note that we build a measure over I → ℝ rather than EuclideanSpace I ℝ. This is because we want to extend this family to a measure over ℝ≥0 → ℝ through the Kolmogorov's extension theorem, which is phrased in this language.

We prove that these measures satisfy IsProjectiveMeasureFamily, which means that they can be extended into a measure over ℝ≥0 → ℝ thanks to the Kolmogorov's extension theorem (not in Mathlib yet). The obtained measure is a measure over the set of real processes indexed by ℝ≥0 and is the law of the Brownian motion.

Main definition

• BrownianReal.projectiveFamily I: The centered Gaussian measure over I → ℝ with covariance matrix given by covMatrix I s t := min s t.

Main statement

• BrownianReal.isProjectiveMeasureFamily_projectiveFamily: BrownianReal.projectiveFamily satisfies IsProjectiveMeasureFamily, which means it can be extended into a measure over ℝ≥0 → ℝ.

Tags

Brownian motion, covariance matrix, projective family

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

The covariance matrix of the finite dimensional distribution of the Brownian motion indexed by I.

Equations

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

@[simp]

theorem ProbabilityTheory.BrownianReal.covMatrix_apply {I : Finset NNReal} (s t : ↥I) : covMatrix I s t = ↑(min ↑s ↑t)

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

theorem ProbabilityTheory.BrownianReal.posSemidef_covMatrix (I : Finset NNReal) : (covMatrix I).PosSemidef

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

Each projectiveFamily I is the centered Gaussian measure with covariance matrix given by covMatrix I s t := min s t.

Note that we build a measure over I → ℝ rather than EuclideanSpace I ℝ. This is because we want to extend this family to a measure over ℝ≥0 → ℝ through the Kolmogorov's extension theorem, which is phrased in this language.

Equations

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

theorem ProbabilityTheory.BrownianReal.measurePreserving_ofLp_multivariateGaussian (I : Finset NNReal) : MeasureTheory.MeasurePreserving WithLp.ofLp (multivariateGaussian 0 (covMatrix I)) (projectiveFamily I)

Up to a measurable equivalence, projectiveFamily I is the centered multivariate Gaussian with covariance matrix covMatrix I.

theorem ProbabilityTheory.BrownianReal.measurePreserving_toLp_projectiveFamily (I : Finset NNReal) : MeasureTheory.MeasurePreserving (WithLp.toLp 2) (projectiveFamily I) (multivariateGaussian 0 (covMatrix I))

Up to a measurable equivalence, projectiveFamily I is the centered multivariate Gaussian with covariance matrix covMatrix I.

theorem ProbabilityTheory.BrownianReal.integral_projectiveFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (I : Finset NNReal) (f : (↥I → ℝ) → E) : ∫ (x : ↥I → ℝ), f x ∂projectiveFamily I = ∫ (x : EuclideanSpace ℝ ↥I), f x.ofLp ∂multivariateGaussian 0 (covMatrix I)

theorem ProbabilityTheory.BrownianReal.covariance_projectiveFamily (I : Finset NNReal) (f g : (↥I → ℝ) → ℝ) : covariance f g (projectiveFamily I) = covariance (f ∘ WithLp.ofLp) (g ∘ WithLp.ofLp) (multivariateGaussian 0 (covMatrix I))

theorem ProbabilityTheory.BrownianReal.covariance_fun_projectiveFamily (I : Finset NNReal) (f g : (↥I → ℝ) → ℝ) : covariance f g (projectiveFamily I) = covariance (fun (x : WithLp 2 (↥I → ℝ)) => f x.ofLp) (fun (x : WithLp 2 (↥I → ℝ)) => g x.ofLp) (multivariateGaussian 0 (covMatrix I))

Eta-expanded form of ProbabilityTheory.BrownianReal.covariance_projectiveFamily

theorem ProbabilityTheory.BrownianReal.variance_projectiveFamily (I : Finset NNReal) (f : (↥I → ℝ) → ℝ) : variance f (projectiveFamily I) = variance (f ∘ WithLp.ofLp) (multivariateGaussian 0 (covMatrix I))

theorem ProbabilityTheory.BrownianReal.variance_fun_projectiveFamily (I : Finset NNReal) (f : (↥I → ℝ) → ℝ) : variance f (projectiveFamily I) = variance (fun (x : WithLp 2 (↥I → ℝ)) => f x.ofLp) (multivariateGaussian 0 (covMatrix I))

Eta-expanded form of ProbabilityTheory.BrownianReal.variance_projectiveFamily

instance ProbabilityTheory.BrownianReal.isGaussian_projectiveFamily (I : Finset NNReal) : IsGaussian (projectiveFamily I)

@[simp]

theorem ProbabilityTheory.BrownianReal.integral_id_projectiveFamily (I : Finset NNReal) : ∫ (x : ↥I → ℝ), x ∂projectiveFamily I = 0

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

@[simp]

theorem ProbabilityTheory.BrownianReal.integral_eval_projectiveFamily (I : Finset NNReal) (s : ↥I) : ∫ (x : ↥I → ℝ), x s ∂projectiveFamily I = 0

theorem ProbabilityTheory.BrownianReal.covariance_eval_projectiveFamily (I : Finset NNReal) (s t : ↥I) : covariance (fun (x : ↥I → ℝ) => x s) (fun (x : ↥I → ℝ) => x t) (projectiveFamily I) = ↑(min ↑s ↑t)

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

theorem ProbabilityTheory.BrownianReal.measurePreserving_eval_projectiveFamily {I : Finset NNReal} (s : ↥I) : MeasureTheory.MeasurePreserving (fun (x : ↥I → ℝ) => x s) (projectiveFamily I) (gaussianReal 0 ↑s)

The distribution of finite-dimensional marginals of the real Brownian motion at time s is the centered Gaussian with variance s.

theorem ProbabilityTheory.BrownianReal.measurePreserving_eval_sub_eval_projectiveFamily (I : Finset NNReal) (s t : ↥I) : MeasureTheory.MeasurePreserving (fun (x : ↥I → ℝ) => x s - x t) (projectiveFamily I) (gaussianReal 0 (nndist ↑s ↑t))

The distribution of the increment of the real Brownian motion from time s to time t is the centered Gaussian with variance t - s.

theorem ProbabilityTheory.BrownianReal.isProjectiveMeasureFamily_projectiveFamily : MeasureTheory.IsProjectiveMeasureFamily projectiveFamily

theorem ProbabilityTheory.BrownianReal.measurePreserving_restrict_projectiveFamily {I J : Finset NNReal} (hIJ : I ⊆ J) : MeasureTheory.MeasurePreserving (Finset.restrict₂ hIJ) (projectiveFamily J) (projectiveFamily I)

If one restricts the finite-dimensional distribution of the real Brownian motion over a finset J to a smaller finset I, one obtains the finite-dimensional distribution of the real Brownian motion over I.