OAI/NumberTheory/Jacobsthal/Probability/RawMarkedVisitGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastRawCycle line 16
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastRawCycle_measurable line 21
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastRawCycle_anchor_ge line 34
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastRawCycle_record line 41
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenFinalCycle line 48
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenFinalCycle_measurable line 53
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenFinalCycle_anchor_gt line 65
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenFinalCycle_record line 70
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHit_actual_visit line 74
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.gapAt_add_cost line 108
11. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.physical_record_slack line 115
12. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHit_ae_geometric line 136