OAI/NumberTheory/Jacobsthal/Probability/MovingMarkedWindow.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstMarkedBeginning line 18
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.nextMarkWeight_ne_top line 21
3. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstMarkedBeginning_isSFiniteKernel line 24
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstMarkedBeginning_apply line 28
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstMarkedBeginning_increment line 36
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstMarkedBeginning_mass line 44
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstMarkedBeginning_ae_regeneration line 50
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstMarkedBeginning_cost_integral line 56
9. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedBeginning line 67
10. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedBeginning_isMarkovKernel line 70
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedBeginning_ae_regeneration line 81
12. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedCostLaw line 88
13. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedCostLaw_isProbabilityMeasure line 91
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedCostLaw_eq line 94
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstMarkWaiting_nonneg line 107
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedCost_nonneg line 112
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costTransform_mono line 119
18. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedCost_uniform_exponential line 125
19. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialBeginningReg line 156
20. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialBeginningReg_isMarkovKernel line 159
21. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialBeginningReg_map_state line 170
22. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialBeginningReg_cost_law line 178
23. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningBelow_shift line 184
24. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningOver_shift line 191
25. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.beginningWindow_shift line 198
26. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.absoluteBeginningOvershoot_eq line 205
27. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.absoluteBeginningWindowHit_eq line 210
28. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedWindowSuccess line 215
29. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedWindowFailure line 219
30. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedWindowSuccess_measurable line 223
31. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedWindowFailure_measurable line 229
32. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedWindow_partition line 235
33. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedWindowSuccess line 244
34. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedWindowFailure line 247
35. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedWindow_partition line 250
36. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.cost_tail_le_transform line 256
37. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedWindowFailure_le line 273
38. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialMarkedWindow_exponential line 297
39. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.exponential_decay_tendsto line 327
40. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.moving_marked_window_capture line 334