OAI/NumberTheory/Jacobsthal/Renewal/MarkedCycleCompletion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.continueMarkUpdate line 16
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.continueMarkUpdate_measurable line 18
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markContinuation line 21
4. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.markContinuation_isMarkovKernel line 24
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markContinuation_apply line 27
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markContinuation_forget line 34
7. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedMarkedKernel line 40
8. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedMarkedKernel_isMarkovKernel line 43
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedMarked_forget line 47
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedMarked_regeneration line 62
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markContinuation_preserves_mark line 68
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedMarked_mark_eq line 74
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedMarked_mark_mass line 88
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedMarked_cost_lower line 92
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markContinuation_translation line 98
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.completedMarked_translation line 110