The σ-algebra of cylinder sets of Brownian trajectories

Stream: new members

[Lars Ericson]

We have a set Ω of all continuous real functions from nnreal to ℝ:

@[derive [topological_space, has_coe_to_fun]]
def Brownian_event_space := C(nnreal, ℝ)
local notation `Ω` := Brownian_event_space

noncomputable instance : measurable_space Ω := borel _
instance : borel_space Ω := ⟨rfl⟩

We define the cylinder sets C T I on Ω as describedf by Zeev Schuss:
Screenshot-from-2020-12-20-23-12-42.png

[Lars Ericson]

so

def interval (n : ℕ ) (I : (fin n) → ℝ × ℝ) (k: (fin n)) := set.Ioo (I k).1 (I k).2

def cylinder_set (n : ℕ) (t : fin n → nnreal)
                 (I : (fin n) → ℝ × ℝ ) :=
  {ω : Brownian_event_space | ∀ k : fin n, (ω (t k) ∈ (interval n I k))}

#check cylinder_set -- : Π (n : ℕ), (fin n → nnreal) → (fin n → ℝ × ℝ) → set Ω

[Lars Ericson]

The space of Brownian Events is the σ-algebra of the cylinder sets, so:
Screenshot-from-2020-12-20-23-13-28.png

[Lars Ericson]

The enumeration here is over all possible time grids T of size n and all possible real intervals of size n. So countable for the size and then doubly uncountable for the, for each size, to enumerate all possible cylinder bounds. The sample space is all members of C(nnreal, ℝ).

So for probability space, instead of a setting (Ω, A, P), where the event space is A=B(Ω), i.e. the Borel sets of Ω, here we've got the σ-algebra generated by the countable/double uncountable family of cylinder sets of Ω.

So I guess I can do that with measurable_space.generate_from on the cylinder sets, if I can figure out how to enumerate all the t and I.

No specific question here....just if this rings a bell and you have any thoughts, please say a few words.

All I'm trying to do here is give the construction of the probability space for Brownian motion, in Lean.

This is not much discussed but is pretty explicitly described in the Zeev Schuss book linked above. I've Googled a lot and most discussions don't quite come right out and build the space, but Zeev does. I like descriptions like that that are more constructive and hands-on. In this case it seems a bit tricky though because of the uncountables.

[Reid Barton]

It looks like the Brownian events are intended to make up the sigma-algebra on Ω, so you don't want the Borel one--you can just delete the last two lines of your very first code block, and you probably don't use the topological space structure at all.

[Reid Barton]

(It's not clear to me whether in the end you do get the same sigma-algebra after all.)