OAI/NumberTheory/Jacobsthal/Probability/CanonicalPairHitEvents.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawWord_first_prefix_law line 15
2. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairHitTest line 65
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairHitTest_measurable line 70
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairHitTest_prefix line 76
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.noPairHits line 79
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.noPairHits_measurable line 82
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.noPairHits_prefix line 90
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.noPairHits_zero line 93
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.noPairHits_succ line 98
10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstPairHitEvent line 115
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstPairHitEvent_measurable line 118
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstPairHitEvent_prefix line 122
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstPairHitEvent_disjoint line 125