OAI/NumberTheory/Jacobsthal/Partitions/BeginningWindowTransport.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costProjection_comp line 18
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costProjection_power line 28
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costProjection_potential line 39
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costProjection_restrict line 48
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.relativeBeginningCost line 54
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.relativeBeginningCost_measurable line 56
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginning_relative_cost_projection line 59
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningBelow line 75
9. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningWindow line 79
10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningOver line 83
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningBelow_projection line 87
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningWindow_projection line 93
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningOver_projection line 99
14. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningWindowHit line 105
15. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningOvershoot line 108
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningWindowHit_eq_clock line 111
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningOvershoot_eq_clock line 119
18. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningWindow_partition line 127
19. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningWindow_exponential line 132