OAI/NumberTheory/Jacobsthal/Paths/ConsecutivePairStop.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.boundedPairCylinder line 13
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.boundedPairCylinder_measurable line 16
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.boundedPairCylinder_disjoint line 22
4. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.anyPairHit line 30
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.anyPairHit_measurable line 33
6. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstPairHit_union_eq_any line 42
7. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonical_first_hit_measure line 64
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedPairHit line 81
9. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedPairHit_isFiniteKernel line 84
10. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedPairHit_eq_extension line 88
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedPairHit_le line 103
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.boundedPairCylinder_empty line 108
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstPairHit_iUnion_eq_any line 112
14. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedPairHit_sum line 127
15. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedPairHit_sum_le line 140
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedPairHit_sum_mass_le_one line 145
17. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.regenerativeCostWindow line 161
18. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.regenerativeCostWindow_measurable line 164
19. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedArrival line 167
20. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedArrival_measurable line 168
21. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutiveCapture line 170
22. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutiveFirstContinue line 173
23. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutiveContinue line 177
24. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutiveCapture_isFiniteKernel line 180
25. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutiveFirstContinue_isFiniteKernel line 184
26. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutiveContinue_isFiniteKernel line 188
27. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutive_first_partition line 192
28. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutive_stop_isMarkov line 203
29. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutiveMarkedHit line 213
30. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutiveMarkedHit_mass_le_one line 216