Brownian motion

def ProbabilityTheory.preBrownian : NNReal → (NNReal → ℝ) → ℝ

Equations

• ProbabilityTheory.preBrownian t ω = ω t

theorem ProbabilityTheory.isGaussianProcess_preBrownian : IsGaussianProcess preBrownian gaussianLimit