Mathlib Map

Theorems · Inductive type · probability

ProbabilityTheory.IsPreBrownianReal

{Ω : Type u_1} →
  {mΩ : MeasurableSpace Ω} →
    (NNReal → Ω → ℝ) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsPreBrownianReal._auto_1 → Prop

A stochastic process is called pre-Brownian if its finite-dimensional laws are those of the Brownian motion, see projectiveFamily. Note: we name the constructor mk' so as to define later IsPreBrownianReal.mk, which to pre-Brownian motion will associate a continuous modification, in a way similar to AEMeasurable.mk.

Defined in
Mathlib.Probability.BrownianMotion.Basic
Cited by
23 results in Mathlib
Foundations
Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ProbabilityTheory.IsPreBrownianReal.isGaussianProcess · cited by 7IsPreBrownianReal.isGauss…ProbabilityTheory.IsPreBrownianReal.covariance_eval · cited by 5IsPreBrownianReal.covaria…ProbabilityTheory.IsPreBrownianReal.hasLaw · cited by 5IsPreBrownianReal.hasLawProbabilityTheory.IsBrownianReal.toIsPreBrownianReal · cited by 4IsBrownianReal.toIsPreBro…ProbabilityTheory.IsGaussianProcess.isPreBrownianReal_of_covariance · cited by 4IsGaussianProcess.isPreBr…ProbabilityTheory.IsPreBrownianReal.hasLaw_eval · cited by 3IsPreBrownianReal.hasLaw_…ProbabilityTheory.IsPreBrownianReal.integral_eval · cited by 3IsPreBrownianReal.integra…ProbabilityTheory.HasIndepIncrements.isPreBrownianReal_of_hasLaw · cited by 1HasIndepIncrements.isPreB…ProbabilityTheory.IsPreBrownianReal.aemeasurable · cited by 1IsPreBrownianReal.aemeasu…ProbabilityTheory.IsPreBrownianReal.covariance_fun_eval · cited by 1IsPreBrownianReal.covaria…ProbabilityTheory.IsPreBrownianReal.eval_zero_ae_eq_zero · cited by 1IsPreBrownianReal.eval_ze…ProbabilityTheory.IsPreBrownianReal.hasIndepIncrements · cited by 1IsPreBrownianReal.hasInde…ProbabilityTheory.IsPreBrownianReal.neg · cited by 1IsPreBrownianReal.negProbabilityTheory.IsPreBrownianReal.shift · cited by 1IsPreBrownianReal.shiftProbabilityTheory.IsPreBrownianReal.smul · cited by 1IsPreBrownianReal.smulReal · cited by 25697RealMeasurableSpace · cited by 13106MeasurableSpaceMeasureTheory.Measure · cited by 10939MeasureTheory.MeasureNNReal · cited by 4310NNRealProbabilityTheory.IsPreBrowni…CITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by27

Results whose statement or proof uses this declaration.