wikipedia flavored stochastic_process

Stream: Is there code for X?

[Lars Ericson]

For the Wikipedia definition of stochastic process, is the following rendition reasonable, and in terms of mathlib style guide, how would you touch it up:

import measure_theory.lebesgue_measure
import measure_theory.measurable_space

open measure_theory

-- https://en.wikipedia.org/wiki/Probability_space

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure:  probability_measure volume)

-- https://en.wikipedia.org/wiki/Random_variable#Definition

def random_variable (α β: Type*) (PS: probability_space α) (MS: measurable_space β):=
  @measurable α β PS.to_measure_space.to_measurable_space MS

--https://en.wikipedia.org/wiki/Stochastic_process#Stochastic_process

def stochastic_process (α β T: Type*) (PS: probability_space α) (MS: measurable_space β) (X: T → α → β) (t: T) :=
  random_variable α β PS MS (X t)

-- https://en.wikipedia.org/wiki/Stochastic_process#Index_set

def index_set (α β T: Type*) (X: T → α → β) := T

-- https://en.wikipedia.org/wiki/Stochastic_process#State_space

def state_space (α β T: Type*) (X: T → α → β) := β

-- https://en.wikipedia.org/wiki/Stochastic_process#Sample_function

def sample_function (α β T: Type*) (X: T → α → β) := λ (ω: α), λ (t: T), X t ω

-- https://en.wikipedia.org/wiki/Stochastic_process#Law
def law (α β T: Type*)
        (PS: probability_space α)
        (MS: measurable_space β)
        (X: T → α → β)
        (t: T)
        (SP: stochastic_process α β T PS MS X t)
        (HM: has_mem β β)
        (Y: set β):=
  PS.volume.to_outer_measure.measure_of {ω : α | ∃ y:β, X t ω ∈ y}