Verso file for the Brownian motion process

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

@[reducible, inline]

abbrev Ω : Type

Equations

• Ω = (NNReal → ℝ)

instance instMeasureSpaceΩ : MeasureTheory.MeasureSpace Ω

Equations

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

def B : NNReal → Ω → ℝ

Equations

• B = ProbabilityTheory.brownian