OAI/NumberTheory/Jacobsthal/Renewal/MarkedCycleWords.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranchKernel line 14
2. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranchKernel_isFiniteKernel line 17
3. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranch_pow_isFiniteKernel line 21
4. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.branchCostLaw line 29
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.branchCostLaw_true line 32
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.false_mark_set line 34
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.branchCostLaw_false line 38
8. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.branchCostLaw_isFiniteMeasure line 42
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranch_sum line 46
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranch_ae_regeneration line 60
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranch_increment_integral line 66
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranch_cost_lintegral line 90
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranch_mass line 109
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranch_true_mass line 113
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranch_pow_ae_regeneration line 117
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.branch_cumulative_cost_lintegral line 128
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.branch_cumulative_cost_law line 162
18. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.branch_word_ae_regeneration line 171
19. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.branch_word_cost_lintegral line 177
20. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.branch_word_cost_law line 203