OAI/NumberTheory/Jacobsthal/Estimates/ConsecutivePowerProjection.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.historyGoodInput line 14
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.historyGoodInput_measurable line 17
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairHitTest_first_eq line 20
4. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairStoppedHistory_zero_input_filter line 31
5. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonical_capture_projection line 47
6. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstNoHitHistory line 58
7. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstNoHitHistory_isFiniteKernel line 61
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstHistory_partition line 65
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonical_first_continue_projection line 72
10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.noHitPairHistory line 96
11. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.noHitPairHistory_isFiniteKernel line 99
12. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.noHitPairHistory_factor line 103
13. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonical_pair_continue_projection line 119
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.shifted_pair_continue_projection line 133
15. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairSurvivingHistory_projection line 152
16. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairStoppedHistory_projection line 179