Theorems · Theorem · probability
ProbabilityTheory.BrownianReal.measurePreserving_eval_projectiveFamily
∀ {I : Finset NNReal} (s : ↥I),
MeasureTheory.MeasurePreserving (fun x => x s) (ProbabilityTheory.BrownianReal.projectiveFamily I)
(ProbabilityTheory.gaussianReal 0 ↑s)The distribution of finite-dimensional marginals of the real Brownian motion at time s
is the centered Gaussian with variance s.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 321 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Finsetstatement and proof · cited by 13,712
- MeasureTheory.Measureproof · cited by 10,939
- NNRealstatement and proof · cited by 4,310
- Real.toNNRealproof · cited by 267
- MeasureTheory.MeasurePreservingstatement · cited by 259
- ProbabilityTheory.varianceproof · cited by 104
- ProbabilityTheory.gaussianRealstatement and proof · cited by 77
- measurable_pi_applyproof · cited by 77
- Real.toNNReal_coeproof · cited by 36
- ProbabilityTheory.BrownianReal.projectiveFamilystatement and proof · cited by 19
- ProbabilityTheory.HasGaussianLaw.evalproof · cited by 6
Cited by1
Results whose statement or proof uses this declaration.
- ProbabilityTheory.IsPreBrownianReal.hasLaw_evalproof · cited by 3