OAI/NumberTheory/Jacobsthal/Estimates/CanonicalPairCylinders.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairSurvivingHistory line 13
2. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairStoppedHistory line 16
3. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairSurvivingHistory_isFiniteKernel line 19
4. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairStoppedHistory_isFiniteKernel line 23
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairSurvivingHistory_zero line 27
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairStoppedHistory_zero line 32
7. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairSurvivingHistory_succ line 39
8. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairStoppedHistory_factor line 51