OAI/NumberTheory/Jacobsthal/Probability/MarkedVisitGeometry.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos970.NumberTheoryLean.PairedCostProcess.OddCost line 16
2. def OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairedDraws line 18
3. instance OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairedDraws_isMarkovKernel line 21
4. def OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairUpdate line 23
5. theorem OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairUpdate_measurable line 26
6. def OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairedCostKernel line 32
7. instance OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairedCostKernel_isMarkovKernel line 35
8. theorem OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairedCostKernel_apply line 38
9. theorem OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairedCost_map_state line 45
10. theorem OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairedCost_map_ratio_cost line 51
11. theorem OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairedDraws_regeneration line 64
12. theorem OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairedCost_regeneration line 74
13. def OAI.Erdos970.NumberTheoryLean.PairedCostProcess.shiftCost line 81
14. theorem OAI.Erdos970.NumberTheoryLean.PairedCostProcess.shiftCost_measurable line 83
15. theorem OAI.Erdos970.NumberTheoryLean.PairedCostProcess.pairedCost_translation line 86
16. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceMark line 110
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceMark_measurable line 112
18. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.MarkedOddCost line 116
19. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedPairUpdate line 118
20. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedPairUpdate_measurable line 121
21. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedPairKernel line 124
22. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedPairKernel_isMarkovKernel line 127
23. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedPairKernel_apply line 130
24. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedPair_forget line 138
25. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedPair_regeneration line 144
26. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedShift line 149
27. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedShift_measurable line 151
28. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedPair_translation line 154
29. def OAI.Erdos970.NumberTheoryLean.CostReturnLaw.returnSet line 177
30. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.returnSet_measurable line 179
31. def OAI.Erdos970.NumberTheoryLean.CostReturnLaw.costKilled line 182
32. def OAI.Erdos970.NumberTheoryLean.CostReturnLaw.costCaptured line 183
33. instance OAI.Erdos970.NumberTheoryLean.CostReturnLaw.costKilled_isFiniteKernel line 185
34. instance OAI.Erdos970.NumberTheoryLean.CostReturnLaw.costCaptured_isFiniteKernel line 186
35. instance OAI.Erdos970.NumberTheoryLean.CostReturnLaw.costKilled_pow_isFiniteKernel line 188
36. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.costKilled_map_state line 196
37. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.costKilled_pow_map_state line 203
38. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.costKilled_mass line 225
39. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.cost_survival_tendsto_zero line 230
40. def OAI.Erdos970.NumberTheoryLean.CostReturnLaw.firstReturn line 236
41. instance OAI.Erdos970.NumberTheoryLean.CostReturnLaw.firstReturn_isFiniteKernel line 238
42. def OAI.Erdos970.NumberTheoryLean.CostReturnLaw.returnLaw line 240
43. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.costCaptured_add_costKilled line 242
44. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.return_mass_step line 247
45. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.return_finite_mass line 257
46. instance OAI.Erdos970.NumberTheoryLean.CostReturnLaw.returnLaw_isMarkovKernel line 271
47. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.costCaptured_off_returnSet line 280
48. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.firstReturn_off_returnSet line 283
49. theorem OAI.Erdos970.NumberTheoryLean.CostReturnLaw.returnLaw_off_returnSet line 287
50. def OAI.Erdos970.NumberTheoryLean.CostReturnLaw.cycleCostLaw line 291
51. instance OAI.Erdos970.NumberTheoryLean.CostReturnLaw.cycleCostLaw_isProbabilityMeasure line 293
52. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.regeneration_density_eq line 311
53. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.regeneration_interval_positive line 315
54. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.markProbability line 338
55. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markProbability_pos line 341
56. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markProbability_lt_one line 344
57. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceMark_true line 357
58. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.markedPair_mark_mass line 360
59. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.gapAt line 392
60. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.gapAt_pathCost line 394
61. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.nextExponent_scale line 398
62. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.nextGap_scale line 402
63. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.marked_draw_slack line 406
64. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.gapAt_le_iff line 433
65. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.le_gapAt_iff line 439
66. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.marked_cost_window line 445
67. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.proportional_window_width line 454
68. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.moving_window_cost_threshold line 459