OAI/Probability/SKValue/Processes/UnitMomentMartingale.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SKValue.UnitMomentMartingale line 26
2. lemma OAI.SKValue.UnitMomentMartingale.integrable line 35
3. lemma OAI.SKValue.UnitMomentMartingale.integrable_mul line 40
4. lemma OAI.SKValue.UnitMomentMartingale.integral_past_mul line 49
5. lemma OAI.SKValue.UnitMomentMartingale.sampled_gap_martingale line 62
6. lemma OAI.SKValue.UnitMomentMartingale.sampled_gap_nonneg line 88
7. lemma OAI.SKValue.UnitMomentMartingale.sampled_gap_integral line 99
8. lemma OAI.SKValue.UnitMomentMartingale.finite_gap_maximal line 107
9. lemma OAI.SKValue.UnitMomentMartingale.rational_gap_maximal line 156
10. def OAI.SKValue.terminalTime line 194
11. lemma OAI.SKValue.terminalTime_mem line 196
12. lemma OAI.SKValue.terminalTime_monotone line 206
13. lemma OAI.SKValue.terminalTime_tendsto line 213
14. lemma OAI.SKValue.UnitMomentMartingale.ae_exists_rational_gap_bound line 219
15. lemma OAI.SKValue.continuous_gap_bound_of_rat line 250
16. lemma OAI.SKValue.UnitMomentMartingale.exists_sequence_terminal line 265
17. lemma OAI.SKValue.UnitMomentMartingale.exists_continuous_terminal line 288
18. lemma OAI.SKValue.UnitMomentMartingale.terminal_square line 335
19. lemma OAI.SKValue.UnitMomentMartingale.terminal_mean_square line 370