OAI/NumberTheory/Jacobsthal/Estimates/FullReturnCylinders.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.avoidOddReturns line 14
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.avoidOddReturns_measurable line 17
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastRegeneration line 25
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastRegeneration_measurable line 28
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.survivingHistory line 31
6. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory line 34
7. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.survivingHistory_isFiniteKernel line 38
8. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory_isFiniteKernel line 42
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.avoidOddReturns_prefix line 46
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.avoidOddReturns_succ line 50
11. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.survivingHistory_succ line 70
12. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory_eq_capture_after_survival line 82
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory_ae_cylinder line 92
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory_retains_past line 99
15. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistoryWithFirst line 104
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistoryWithFirst_apply line 109