OAI/NumberTheory/Jacobsthal/Paths/BranchWordEndpoint.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.wordSignatureEnd line 15
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.wordSignatureEnd_measurable line 19
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.branchWordKernel line 24
4. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.branchWordKernel_isFiniteKernel line 28
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.branchWordKernel_replicate line 33
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.branchWordKernel_first_replicate line 39
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceMarkedWord_endpoint line 43
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawWordReturnedOdd line 70
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawWordReturnedOdd_measurable line 73
10. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawMarkedWord_endpoint line 76