Zulip Chat Archive

Stream: Is there code for X?

Topic: wikipedia flavored stochastic_process

view this post on Zulip Lars Ericson (Jan 20 2021 at 20:25):

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


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}

Last updated: May 16 2021 at 05:21 UTC