[Merged by Bors] - feat(probability/martingale): optional sampling theorem

[RemyDegenne]

We prove the optional sampling theorem: if τ is a bounded stopping time and σ is another stopping time, then the value of a martingale f at the stopping time min τ σ is almost everywhere equal to μ[stopped_value f τ | hσ.measurable_space].

---

• depends on: [Merged by Bors] - chore(measure_theory/function/conditional_expectation): change the definition of condexp and its notation #14010
• depends on: [Merged by Bors] - feat(measure_theory/function/conditional_expectation): Conditional expectation of an indicator #14058
• depends on: [Merged by Bors] - feat(probability/stopping): measurability of comparisons of stopping times #14061
• depends on: [Merged by Bors] - feat(probability/stopping): prove measurability of the stopped value #14062
• depends on: [Merged by Bors] - feat(probability/stopping): measurability of sets related to stopping times, under countable/encodable assumptions #14750
• depends on: [Merged by Bors] - feat(measure_theory/function/conditional_expectation): conditional expectation w.r.t. the restriction of a measure to a set #14751
• depends on: [Merged by Bors] - 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
• depends on: [Merged by Bors] - feat(probability/stopping): generalize mem_ℒp_stopped_value #16369
• depends on: [Merged by Bors] - feat(measure_theory/measure/measure_space): add variants of ae_restrict_Union_eq #16370
• depends on: [Merged by Bors] - feat(order/succ_pred/linear_locally_finite): there is an order_iso between a linear locally finite order and a subset of Z #16832

[RemyDegenne]

Thanks for the review, and sorry for all the useless assumptions! That code changed a lot over time and I did not catch all the simplifications.

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests