OAI/NumberTheory/Jacobsthal/Renewal/ClockTailReward.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedClock_pow_isMarkovKernel line 15
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedClock_cumulative_lintegral line 23
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedClock_cumulative_law line 46
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedClock_zero_law line 53
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedClock_renewal line 58
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedClock_increment_lower line 65
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedClock_minimum_pos line 73
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockBelow line 87
9. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockOver line 88
10. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockBelow_isFiniteKernel line 90
11. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockOver_isFiniteKernel line 91
12. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockBelow_pow_isFiniteKernel line 93
13. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockOverReward line 98
14. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockOverReward_isFiniteKernel line 102
15. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockOvershoot line 107
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockBelow_le line 109
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockBelow_ae_lt line 114
18. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockBelow_pow_ae_lt line 118
19. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockOver_mass line 126
20. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockOverReward_mass line 135
21. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clock_compose_mono_right line 141
22. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clock_potential_mono_step line 149
23. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockOvershoot_guarded line 156
24. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockReward_potential_integral line 170
25. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockOvershoot_le_reward line 178
26. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockTailPiece line 195
27. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockTailPiece_measurable line 198
28. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockReward_le_tail_pieces line 201
29. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockTailPiece_integral line 221
30. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.clock_renewal_reward_tail_bound line 227