OAI/NumberTheory/Jacobsthal/Renewal/SourceCycleDuration.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.durationHitOrReturn line 16
2. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.durationHitOrReturn_isMarkovKernel line 21
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.durationHitOrReturn_forget line 25
4. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.FirstPairWitness line 34
5. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.SourceCycleWitness line 35
6. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairWitnessUpdate line 37
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairWitnessUpdate_measurable line 40
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairWitnessKernel line 43
9. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairWitnessKernel_isMarkovKernel line 46
10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstPairProjection line 49
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstPairProjection_measurable line 51
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairWitness_projection line 54
13. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.continueWitnessUpdate line 61
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.continueWitnessUpdate_measurable line 64
15. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation line 68
16. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation_isMarkovKernel line 71
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation_apply line 74
18. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceWitnessProjection line 81
19. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceWitnessProjection_measurable line 84
20. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation_projection line 87
21. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleWitnessKernel line 99
22. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleWitnessKernel_isMarkovKernel line 102
23. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleWitness_projection line 106
24. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleWitness_duration_ge_two line 121
25. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceWitness_mark_iff line 132
26. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.addPairDuration line 148
27. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.addPairDuration_measurable line 150
28. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.durationHit_comp_captured line 153
29. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.durationHit_comp_killed line 170
30. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstMarkedReturn_succ line 181
31. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedReturnLaw_first_step_duration line 191
32. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.duration_forced_first_pair line 202
33. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pairWitness_forget line 219
34. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation_duration line 225
35. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleWitness_duration_law line 232