mathlib3
3091b91e - feat(probability/stopping): if a filtration is sigma finite, then the measure restricted to the sigma algebra generated by a stopping time is sigma finite (#14752)

Commit

3 years ago

feat(probability/stopping): if a filtration is sigma finite, then the measure restricted to the sigma algebra generated by a stopping time is sigma finite (#14752) Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Author

RemyDegenne

Parents

72fbe5c3

mathlib3 3091b91e - feat(probability/stopping): if a filtration is sigma finite, then the measure restricted to the sigma algebra generated by a stopping time is sigma finite (#14752)

mathlib3
3091b91e - feat(probability/stopping): if a filtration is sigma finite, then the measure restricted to the sigma algebra generated by a stopping time is sigma finite (#14752)