OAI/NumberTheory/Jacobsthal/Paths/RawWordSpaces.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstArrivalMark line 16
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstArrivalMark_measurable line 18
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnSignatureMark line 21
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnSignatureMark_measurable line 23
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnMark line 26
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnMark_measurable line 28
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceReturnSignature_mark line 31
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBranchReturnKernel line 34
9. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBranchReturnKernel_isFiniteKernel line 37
10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceBranchWitnessKernel line 41
11. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceBranchWitnessKernel_isFiniteKernel line 44
12. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBranchReturn_signature line 48
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceBranchWitness_markCost line 62
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceBranchWitness_endpoint line 71
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBranchReturn_endpoint line 80
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBranchReturn_mass_le_one line 95
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTrace_ae_regeneration line 100
18. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBranchReturn_ae_regeneration line 111
19. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.RawCycleWordTrace line 127
20. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawCycleWordMeasurable line 131
21. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.(instance at line 138) line 138
22. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.CycleInputSignature line 140
23. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.CycleWordSignature line 142
24. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleWordSignatureMeasurable line 146
25. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.(instance at line 152) line 152
26. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnInputCost line 154
27. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnInputCost_measurable line 157
28. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnInputSignature line 163
29. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnInputSignature_measurable line 166
30. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawCycleWordSignature line 169
31. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawCycleWordSignature_measurable line 174