mathlib
17c22094 - feat(probability_theory/stopping): define filtration and stopping time (#10553)

Commit
4 years ago
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.
Author
Parents
Loading