Theorems · Theorem · probability

ProbabilityTheory.IsPreBrownianReal.hasLaw_eval

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P →
    ∀ (t : NNReal), ProbabilityTheory.HasLaw (B t) (ProbabilityTheory.gaussianReal 0 t) P

Defined in: Mathlib.Probability.BrownianMotion.Basic
Cited by: 3 results in Mathlib
Foundations: Depth 322 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
NNRealstatement and proof · cited by 4,310
ProbabilityTheory.gaussianRealstatement · cited by 77
ProbabilityTheory.HasLawstatement · cited by 69
ProbabilityTheory.IsPreBrownianRealstatement and proof · cited by 23
ProbabilityTheory.HasLaw.compproof · cited by 12
ProbabilityTheory.IsPreBrownianReal.hasLawproof · cited by 5
MeasureTheory.MeasurePreserving.hasLawproof · cited by 4
ProbabilityTheory.BrownianReal.measurePreserving_eval_projectiveFamilyproof · cited by 1

Cited by3

Results whose statement or proof uses this declaration.

ProbabilityTheory.IsPreBrownianReal.integral_evalproof · cited by 3
ProbabilityTheory.IsPreBrownianReal.eval_zero_ae_eq_zeroproof · cited by 1
ProbabilityTheory.IsPreBrownianReal.negproof · cited by 1