OAI/NumberTheory/Jacobsthal/Probability/MarkedCostHitReduction.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.allowedCycleInputs line 15
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.allowedCycleInputs_measurable line 18
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.permittedCycleBranch line 21
4. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.permittedCycleBranch_isFiniteKernel line 24
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.permittedCycleBranch_false line 28
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.permittedCycleBranch_true line 33
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.permittedCycleBranch_sum line 36
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceHitWordKernel line 39
9. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceHitWordKernel_isFiniteKernel line 43
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceHitWordKernel_mass line 48
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.kernel_comp_finset_sum_left line 62
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.kernel_comp_finset_sum_right line 70
13. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceHitWordKernel_sum_length line 78
14. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.RawMarkedHitTrace line 107
15. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.packRawMarkedHitTrace line 110
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.packRawMarkedHitTrace_measurable line 115
17. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawMarkedFirstHitKernel line 120
18. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawMarkedFirstHitKernel_isSFiniteKernel line 124
19. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawMarkedFirstHit_mass line 128
20. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawMarkedHitEvent line 146
21. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawMarkedHitEvent_measurable line 149
22. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawMarkedFirstHit_ae_event line 156
23. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawRegMarkedFirstHitKernel line 167
24. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawRegMarkedFirstHit_mass_le_one line 170
25. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawRegMarkedFirstHitKernel_isFiniteKernel line 181
26. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.kernel_power_sfinite line 197
27. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.kernel_power_support line 202
28. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.supported_projection_power line 213
29. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.supported_projection_potential line 235
30. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.kernelScale line 257
31. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.kernelScale_apply line 260
32. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.kernelScale_isSFinite line 264
33. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.potential_scale_base line 267
34. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.costWindowFilter line 293
35. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.costOutsideFilter line 296
36. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.costWindowFilter_isFiniteKernel line 299
37. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.costOutsideFilter_isFiniteKernel line 302
38. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.costMarkedLoop line 306
39. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.costMarkedLoop_isFiniteKernel line 307
40. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.costCurrentHit line 311
41. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.costCurrentHit_isSFiniteKernel line 313
42. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.costWindow_stopping_isMarkov line 317
43. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costCurrentHit_mass_le_one line 321
44. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryMarkedLoop line 324
45. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryMarkedLoop_isSFiniteKernel line 326
46. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBeginning_total_cost line 330
47. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryMarkedLoop_support line 342
48. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryMarkedLoop_cost line 349
49. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.cost_filter_projection line 359
50. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryWindowCapture_on_regeneration line 366
51. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryWindowCapture_cost line 372
52. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryMarkedPotential_cost line 376
53. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.unmarkedStar_support line 401
54. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryMarkedPotential_mass line 408
55. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryMarkedHit_first_mark_reduction line 415
56. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryInitialHitMass line 432
57. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryInitialHitMass_le_one line 435
58. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.ordinaryInitialHit_cost_law line 440