OAI/NumberTheory/Jacobsthal/Renewal/ClockWindowPassage.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockAtOrAbove line 14
2. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockAtOrAbove_isFiniteKernel line 17
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockAtOrAbove_add_below line 20
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockBelow_increment_lower line 25
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockBelow_pow_lower line 30
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockBelow_mass_eq_zero line 45
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockBelow_survival_tendsto_zero line 52
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockExit_mass_step line 62
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockExit_finite_mass line 72
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockExit_mass_one line 84
11. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockWindow line 92
12. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockWindow_isFiniteKernel line 95
13. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockWindowHit line 98
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockWindow_add_over line 101
15. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockWindowHit_add_overshoot line 121
16. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.clockWindowHit_exponential line 127