OAI/NumberTheory/Jacobsthal/Probability/CompletedMarkEvents.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.CanonicalMarkSlack.firstArrivalMark_bounds line 16
2. theorem OAI.Erdos970.NumberTheoryLean.CanonicalMarkSlack.pair_hit_slack line 25
3. theorem OAI.Erdos970.NumberTheoryLean.CanonicalMarkSlack.canonical_all_marks_slack line 54
4. def OAI.Erdos970.NumberTheoryLean.CompletedMarkEvents.strongMark line 86
5. theorem OAI.Erdos970.NumberTheoryLean.CompletedMarkEvents.strongMark_measurable line 90
6. def OAI.Erdos970.NumberTheoryLean.CompletedMarkEvents.markedPoint line 97
7. def OAI.Erdos970.NumberTheoryLean.CompletedMarkEvents.compactPoint line 100
8. theorem OAI.Erdos970.NumberTheoryLean.CompletedMarkEvents.markedPoint_measurable line 103
9. theorem OAI.Erdos970.NumberTheoryLean.CompletedMarkEvents.compactPoint_measurable line 106
10. def OAI.Erdos970.NumberTheoryLean.CompletedMarkEvents.noStrongBefore line 109
11. theorem OAI.Erdos970.NumberTheoryLean.CompletedMarkEvents.noStrongBefore_measurable line 112
12. def OAI.Erdos970.NumberTheoryLean.CompletedMarkEvents.badCompactPath line 121
13. theorem OAI.Erdos970.NumberTheoryLean.CompletedMarkEvents.badCompactPath_measurable line 124