Commit 2022-09-19 20:38 c41e1712
View on Github →chore(probability/process): split probability/stopping.lean into three files, create process folder (#16521)
Split the content of stopping.lean into the following three files:
- filtration.lean: definition and properties of filtrations
- adapted.lean: adapted and progressively measurable processes (and soon predictable as well)
- stopping.lean: stopping times, stopped values and stopped processes