Commit 2021-12-02 12:47 17c22094

View on Github →

feat(probability_theory/stopping): define filtration and stopping time (#10553) This PR defines filtrations and stopping times which are used in stochastic processes. This is the first step towards creating a theory of martingales in lean.

Estimated changes

Modified src/measure_theory/measurable_space_def.lean

added theorem measurable.le

Created src/probability_theory/stopping.lean

added theorem measure_theory.adapted.add

added theorem measure_theory.adapted.neg

added theorem measure_theory.adapted.smul

added def measure_theory.adapted

added theorem measure_theory.adapted_zero

added def measure_theory.const_filtration

added theorem measure_theory.filtration.adapted_natural

added def measure_theory.filtration.natural

added structure measure_theory.filtration

added theorem measure_theory.is_stopping_time.add_const

added theorem measure_theory.is_stopping_time.max

added theorem measure_theory.is_stopping_time.measurable

added theorem measure_theory.is_stopping_time.measurable_set

added theorem measure_theory.is_stopping_time.measurable_set_eq

added theorem measure_theory.is_stopping_time.measurable_set_eq_const

added theorem measure_theory.is_stopping_time.measurable_set_eq_le

added def measure_theory.is_stopping_time.measurable_space

added theorem measure_theory.is_stopping_time.measurable_space_le

added theorem measure_theory.is_stopping_time.measurable_space_mono

added theorem measure_theory.is_stopping_time.min

added def measure_theory.is_stopping_time

added theorem measure_theory.is_stopping_time_const

added theorem measure_theory.is_stopping_time_of_measurable_set_eq

added theorem measure_theory.measurable_set_of_filtration