Theorems · Definition · probability

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.

Defined in

Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Cited by

19 results in Mathlib

Foundations

Depth 267 from the axioms · uses propext, Classical.choice, Quot.sound