OAI/NumberTheory/Jacobsthal/Probability/MarkedBeginningKernel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBeginningKernel line 14
2. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBeginningKernel_isSFiniteKernel line 17
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBeginning_ae_regeneration line 21
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBeginning_project_actual line 26
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBeginning_cost_law line 35
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBeginning_mass line 39
7. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.RegCost line 45
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningDomainKernel line 47
9. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningDomainKernel_isMarkovKernel line 50
10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedBeginningKernel line 57
11. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedBeginningKernel_isMarkovKernel line 60
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedBeginning_map_state line 74
13. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningCost line 82
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningCost_measurable line 84
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedBeginning_increment_law line 87
16. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedClockKernel line 95
17. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedClockKernel_isMarkovKernel line 98
18. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedClockKernel_apply line 101
19. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedBeginning_cost_kernel_link line 109