OAI/NumberTheory/Jacobsthal/Primes/AdjacentPrimeRecovery.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.PrimeHistoryPrefixOrder.prefixRel line 20
2. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryPrefixOrder.prefixRel_refl line 25
3. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryPrefixOrder.prefixRel_trans line 30
4. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryPrefixOrder.actual_row_prefixRel line 45
5. def OAI.Erdos970.NumberTheoryLean.PrimeHistoryPrefixOrder.orderedPast line 59
6. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryPrefixOrder.orderedPast_measurable line 62
7. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryPrefixOrder.orderedPast_extend line 66
8. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryPrefixOrder.actual_history_ordered line 96
9. def OAI.Erdos970.NumberTheoryLean.PriorPrimeWindow.hasPrimeWindow line 122
10. theorem OAI.Erdos970.NumberTheoryLean.PriorPrimeWindow.sourceHistory_ordered line 130
11. theorem OAI.Erdos970.NumberTheoryLean.PriorPrimeWindow.sourceHistory_prior_live line 140
12. theorem OAI.Erdos970.NumberTheoryLean.PriorPrimeWindow.sourceHistory_prior_mark line 156
13. theorem OAI.Erdos970.NumberTheoryLean.PrimePrefixRecovery.sourceHistory_stages line 193
14. theorem OAI.Erdos970.NumberTheoryLean.PrimePrefixRecovery.sourceHistory_recovers_prefix line 209
15. def OAI.Erdos970.NumberTheoryLean.PrimePrefixRecovery.hasNearThresholdPrefix line 235
16. theorem OAI.Erdos970.NumberTheoryLean.PrimePrefixRecovery.recovered_near_prefix_occurs line 238
17. theorem OAI.Erdos970.NumberTheoryLean.AdjacentPrimeRecovery.sourceHistory_recovers_adjacent line 274