OAI/NumberTheory/Jacobsthal/Paths/WindowHitWords.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.allowedCycleCosts line 14
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.allowedCycleCosts_measurable line 17
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.hitWordEvent line 20
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.hitWordEvent_measurable line 24
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceHitWordMass line 32
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceHitWordMass_measurable line 35
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceHitWordMass_nil line 38
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceHitWordMass_indicator line 53
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceHitWordMass_cons line 59
10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawHitWordKernel line 83
11. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawHitWordKernel_isFiniteKernel line 88
12. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawHitWord_mass line 92