mathlib3
c41e1712 - chore(probability/process): split `probability/stopping.lean` into three files, create `process` folder (#16521)

Commit
3 years ago
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 Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Author
Parents
Loading