OAI/NumberTheory/Jacobsthal/Probability/OrdinaryMarkedWindow.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.potential_factor_right line 16
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.kernel_middle_power line 20
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.potential_exchange line 23
4. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.potential_denesting line 30
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.compose_mono_right_general line 35
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.potential_mono_step_general line 43
7. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.stateFilter line 63
8. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.stateFilter_isFiniteKernel line 65
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.stateFilter_apply line 69
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.stateFilter_mass line 74
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.stateFilter_output line 80
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.stateFilter_input line 84
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.stateFilter_mono line 96
14. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.stateFilter_stopping_isMarkov line 105
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.capturePotential_mass_le_one line 114
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.currentHit_outside line 143
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.currentHit_inside line 151
18. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.restricted_crossing_le_current_hit line 156
19. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.cycleBranch_mass_partition line 179
20. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.nextMarkWeight_le_one line 184
21. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markInputWeightKernel line 190
22. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.markInputWeightKernel_isFiniteKernel line 193
23. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markInputWeightKernel_apply line 197
24. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryCostWindow line 202
25. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryCostWindow_measurable line 204
26. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryWindowCapture line 207
27. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryWindowContinue line 210
28. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryWindowCapture_isFiniteKernel line 213
29. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryWindowContinue_isFiniteKernel line 217
30. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryWindowCapture_mass line 221
31. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryWindow_stop_isMarkov line 228
32. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryMarkedHit line 241
33. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryMarkedHit_mass_le_one line 244
34. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedStar line 247
35. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedStar_isSFiniteKernel line 249
36. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBeginning_unmarkedStar line 251
37. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryMarkedHit_denested line 257