OAI/NumberTheory/Jacobsthal/Renewal/OccupationAge.lean

GitHub source file

137 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.CycleCostAtomless.positive_second_cost_level_null line 22
  2. theorem OAI.Erdos970.NumberTheoryLean.CycleCostAtomless.oddTwoStep_second_positive line 40
  3. theorem OAI.Erdos970.NumberTheoryLean.CycleCostAtomless.oddTwoStep_cost_level line 47
  4. theorem OAI.Erdos970.NumberTheoryLean.CycleCostAtomless.pairedCost_cost_level line 56
  5. theorem OAI.Erdos970.NumberTheoryLean.CycleCostAtomless.captured_cost_level line 68
  6. theorem OAI.Erdos970.NumberTheoryLean.CycleCostAtomless.firstReturn_cost_level line 72
  7. theorem OAI.Erdos970.NumberTheoryLean.CycleCostAtomless.returnLaw_cost_level line 77
  8. instance OAI.Erdos970.NumberTheoryLean.CycleCostAtomless.cycleCostLaw_nullSingletonClass line 81
  9. theorem OAI.Erdos970.NumberTheoryLean.CycleCostAtomless.cycleCostLaw_countable_null line 87
  10. theorem OAI.Erdos970.NumberTheoryLean.CycleCostAtomless.cycleCostLaw_lattice_null line 90
  11. theorem OAI.Erdos970.NumberTheoryLean.CycleCostLower.pairedCost_cost_monotone line 111
  12. theorem OAI.Erdos970.NumberTheoryLean.CycleCostLower.costKilled_cost_monotone line 125
  13. theorem OAI.Erdos970.NumberTheoryLean.CycleCostLower.costKilled_pow_cost_monotone line 128
  14. theorem OAI.Erdos970.NumberTheoryLean.CycleCostLower.captured_cost_lower line 142
  15. theorem OAI.Erdos970.NumberTheoryLean.CycleCostLower.firstReturn_cost_lower line 163
  16. theorem OAI.Erdos970.NumberTheoryLean.CycleCostLower.returnLaw_cost_lower line 171
  17. theorem OAI.Erdos970.NumberTheoryLean.CycleCostLower.cost_three line 175
  18. theorem OAI.Erdos970.NumberTheoryLean.CycleCostLower.cycleCostLaw_lower line 180
  19. theorem OAI.Erdos970.NumberTheoryLean.CycleCostLower.cycleCostLaw_positive line 186
  20. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.costKilled_regeneration line 202
  21. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.costCaptured_regeneration line 206
  22. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.firstReturn_regeneration line 210
  23. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.returnLaw_regeneration line 224
  24. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.costKilled_translation line 232
  25. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.costCaptured_translation line 240
  26. def OAI.Erdos970.NumberTheoryLean.CycleRegeneration.shiftKernel line 248
  27. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.shift_commutes_killed line 251
  28. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.shift_commutes_captured line 258
  29. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.shift_commutes_firstReturn line 265
  30. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.shift_commutes_returnLaw line 268
  31. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.returnLaw_translation line 275
  32. def OAI.Erdos970.NumberTheoryLean.CycleRegeneration.cycleJointLaw line 283
  33. instance OAI.Erdos970.NumberTheoryLean.CycleRegeneration.cycleJointLaw_isProbabilityMeasure line 285
  34. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.return_increment_law line 289
  35. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.returnLaw_ae_regeneration line 302
  36. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.cycle_increment_integral line 306
  37. def OAI.Erdos970.NumberTheoryLean.CycleRegeneration.cycleProductExpectation line 314
  38. theorem OAI.Erdos970.NumberTheoryLean.CycleRegeneration.finite_cycle_cost_factorization line 318
  39. abbrev OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.MarkedReturn line 349
  40. def OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.markReturn line 351
  41. theorem OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.markReturn_measurable line 353
  42. def OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.firstMarkedReturn line 356
  43. instance OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.firstMarkedReturn_isFiniteKernel line 359
  44. def OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.markedReturnLaw line 363
  45. instance OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.markedReturnLaw_isMarkovKernel line 365
  46. theorem OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.markedReturnLaw_forget line 378
  47. theorem OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.markedReturnLaw_duration_ge_two line 387
  48. theorem OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.markedReturnLaw_ae_regeneration line 395
  49. def OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.markedCycleLaw line 401
  50. instance OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.markedCycleLaw_isProbabilityMeasure line 404
  51. def OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.durationLaw line 408
  52. instance OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.durationLaw_isProbabilityMeasure line 410
  53. theorem OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.durationLaw_ge_two line 414
  54. theorem OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.durationLaw_positive line 418
  55. theorem OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.markedCycleLaw_cost_projection line 422
  56. theorem OAI.Erdos970.NumberTheoryLean.MarkedCycleLaw.durationLaw_lintegral line 429
  57. def OAI.Erdos970.NumberTheoryLean.CycleDurationMoments.durationFrom line 455
  58. instance OAI.Erdos970.NumberTheoryLean.CycleDurationMoments.durationFrom_isProbabilityMeasure line 457
  59. theorem OAI.Erdos970.NumberTheoryLean.CycleDurationMoments.durationFrom_lintegral line 461
  60. theorem OAI.Erdos970.NumberTheoryLean.CycleDurationMoments.firstReturn_geometric line 472
  61. theorem OAI.Erdos970.NumberTheoryLean.CycleDurationMoments.weighted_geometric_bound line 484
  62. theorem OAI.Erdos970.NumberTheoryLean.CycleDurationMoments.return_duration_exponential_moment line 504
  63. theorem OAI.Erdos970.NumberTheoryLean.CycleDurationMoments.return_duration_exponential_integrable line 535
  64. theorem OAI.Erdos970.NumberTheoryLean.CycleDurationMoments.cycle_duration_exponential_integrable line 543
  65. theorem OAI.Erdos970.NumberTheoryLean.CycleCostMoments.draw_cost_le_log_three line 561
  66. theorem OAI.Erdos970.NumberTheoryLean.CycleCostMoments.pairedCost_cost_upper line 567
  67. theorem OAI.Erdos970.NumberTheoryLean.CycleCostMoments.costKilled_cost_upper line 583
  68. theorem OAI.Erdos970.NumberTheoryLean.CycleCostMoments.costKilled_pow_cost_upper line 586
  69. theorem OAI.Erdos970.NumberTheoryLean.CycleCostMoments.captured_cost_upper line 602
  70. theorem OAI.Erdos970.NumberTheoryLean.CycleCostMoments.firstReturn_cost_upper line 605
  71. theorem OAI.Erdos970.NumberTheoryLean.CycleCostMoments.markedReturn_cost_upper line 614
  72. theorem OAI.Erdos970.NumberTheoryLean.CycleCostMoments.markedCycle_cost_upper line 627
  73. theorem OAI.Erdos970.NumberTheoryLean.CycleCostMoments.cycle_cost_exponential_moment line 632
  74. theorem OAI.Erdos970.NumberTheoryLean.CycleCostMoments.cycle_cost_exponential_integrable line 656
  75. def OAI.Erdos970.NumberTheoryLean.CycleOccupation.pairSampling line 675
  76. instance OAI.Erdos970.NumberTheoryLean.CycleOccupation.pairSampling_isMarkovKernel line 678
  77. def OAI.Erdos970.NumberTheoryLean.CycleOccupation.evenVisitMap line 680
  78. def OAI.Erdos970.NumberTheoryLean.CycleOccupation.oddVisitMap line 683
  79. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.evenVisitMap_measurable line 686
  80. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.oddVisitMap_measurable line 691
  81. def OAI.Erdos970.NumberTheoryLean.CycleOccupation.evenVisit line 697
  82. def OAI.Erdos970.NumberTheoryLean.CycleOccupation.oddVisit line 698
  83. instance OAI.Erdos970.NumberTheoryLean.CycleOccupation.evenVisit_isMarkovKernel line 700
  84. instance OAI.Erdos970.NumberTheoryLean.CycleOccupation.oddVisit_isMarkovKernel line 701
  85. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.sampling_map_measure line 703
  86. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.evenVisit_eq_full_step line 713
  87. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.oddVisit_eq_paired line 725
  88. def OAI.Erdos970.NumberTheoryLean.CycleOccupation.pairVisits line 731
  89. instance OAI.Erdos970.NumberTheoryLean.CycleOccupation.pairVisits_isFiniteKernel line 733
  90. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.pairVisits_full_steps line 735
  91. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.pairVisits_mass line 739
  92. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.evenVisit_age_bounds line 744
  93. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.oddVisit_age_bounds line 757
  94. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.pairVisits_age_bounds line 772
  95. def OAI.Erdos970.NumberTheoryLean.CycleOccupation.visitBlock line 777
  96. instance OAI.Erdos970.NumberTheoryLean.CycleOccupation.visitBlock_isFiniteKernel line 779
  97. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.visitBlock_mass line 781
  98. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.visitBlock_age_bounds line 785
  99. def OAI.Erdos970.NumberTheoryLean.CycleOccupation.occupationKernel line 799
  100. instance OAI.Erdos970.NumberTheoryLean.CycleOccupation.occupationKernel_isSFiniteKernel line 801
  101. def OAI.Erdos970.NumberTheoryLean.CycleOccupation.occupationMeasure line 803
  102. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.occupation_age_nonneg line 805
  103. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.occupationFrom_exponential_moment line 810
  104. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.occupation_exponential_moment line 860
  105. instance OAI.Erdos970.NumberTheoryLean.CycleOccupation.occupationMeasure_isFiniteMeasure line 865
  106. theorem OAI.Erdos970.NumberTheoryLean.CycleOccupation.occupation_exponential_integrable line 876
  107. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_negative_exponential_integrable line 896
  108. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_all_moments line 904
  109. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_integrable_id line 910
  110. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_memLp_two line 915
  111. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_mean_lower line 919
  112. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_mean_pos line 923
  113. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_nonlattice line 926
  114. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_expTransform_le line 931
  115. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_expTransform_lt_one line 944
  116. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_key_renewal line 947
  117. theorem OAI.Erdos970.NumberTheoryLean.CycleRenewalInputs.cycle_renewal_cell_bound line 954
  118. theorem OAI.Erdos970.Erdos970Dependency.ActualCycleOccupation.costKernel_map_state line 974
  119. theorem OAI.Erdos970.Erdos970Dependency.ActualCycleOccupation.evenVisit_map_state line 981
  120. theorem OAI.Erdos970.Erdos970Dependency.ActualCycleOccupation.oddVisit_map_state line 987
  121. theorem OAI.Erdos970.Erdos970Dependency.ActualCycleOccupation.pairVisits_map_state line 993
  122. theorem OAI.Erdos970.Erdos970Dependency.ActualCycleOccupation.visitBlock_map_state line 997
  123. theorem OAI.Erdos970.Erdos970Dependency.ActualCycleOccupation.occupation_map_ratioOccupation line 1011
  124. theorem OAI.Erdos970.Erdos970Dependency.ActualCycleOccupation.occupation_map_stateMeasure line 1016
  125. theorem OAI.Erdos970.Erdos970Dependency.ActualCycleOccupation.lintegral_state_occupation line 1020
  126. theorem OAI.Erdos970.Erdos970Dependency.ActualCycleOccupation.integrable_state_occupation_iff line 1025
  127. theorem OAI.Erdos970.Erdos970Dependency.ActualCycleOccupation.integral_state_occupation line 1033
  128. theorem OAI.Erdos970.Erdos970Dependency.OccupationAge.oddAge_measurable line 1054
  129. theorem OAI.Erdos970.Erdos970Dependency.OccupationAge.stateAge_measurable line 1057
  130. theorem OAI.Erdos970.Erdos970Dependency.OccupationAge.occupation_age_integrable line 1060
  131. def OAI.Erdos970.Erdos970Dependency.OccupationAge.blockAge line 1070
  132. def OAI.Erdos970.Erdos970Dependency.OccupationAge.residualAge line 1073
  133. theorem OAI.Erdos970.Erdos970Dependency.OccupationAge.blockAge_sum_finite line 1076
  134. theorem OAI.Erdos970.Erdos970Dependency.OccupationAge.blockAge_tendsto_zero line 1083
  135. theorem OAI.Erdos970.Erdos970Dependency.OccupationAge.killed_age_le_pair line 1086
  136. theorem OAI.Erdos970.Erdos970Dependency.OccupationAge.residualAge_succ_le line 1102
  137. theorem OAI.Erdos970.Erdos970Dependency.OccupationAge.residualAge_tendsto_zero line 1110