# Verso file for the Brownian motion process #

This file is used to generate the Verso manual page about Brownian motion.

source
@[reducible, inline]
abbrev Ω :
Type
Equations

- Ω = (NNReal → ℝ)

Instances For

source
instance instMeasureSpaceΩ :
MeasureTheory.MeasureSpace Ω
Equations

- instMeasureSpaceΩ = { toMeasurableSpace := MeasurableSpace.pi, volume := ProbabilityTheory.gaussianLimit }

source
def B :
NNReal → Ω → ℝ
Equations

- B = ProbabilityTheory.brownian

Instances For