OAI/NumberTheory/Jacobsthal/Renewal/RegenerationBandBounds.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.Erdos970Dependency.CycleMeanCost.capturedAge line 19
  2. def OAI.Erdos970.Erdos970Dependency.CycleMeanCost.blockIncrement line 22
  3. theorem OAI.Erdos970.Erdos970Dependency.CycleMeanCost.residualAge_zero line 25
  4. theorem OAI.Erdos970.Erdos970Dependency.CycleMeanCost.age_balance line 30
  5. theorem OAI.Erdos970.Erdos970Dependency.CycleMeanCost.finite_cost_balance line 43
  6. theorem OAI.Erdos970.Erdos970Dependency.CycleMeanCost.capturedAge_sum line 56
  7. theorem OAI.Erdos970.Erdos970Dependency.CycleMeanCost.blockIncrement_sum line 62
  8. theorem OAI.Erdos970.Erdos970Dependency.CycleMeanCost.cycle_cost_lintegral_eq_increments line 67
  9. theorem OAI.Erdos970.Erdos970Dependency.CycleMeanCost.cycle_cost_integrable line 80
  10. theorem OAI.Erdos970.Erdos970Dependency.CycleMeanCost.cycle_mean_eq line 89
  11. def OAI.Erdos970.NumberTheoryLean.InitialRegeneration.hitOrReturn line 115
  12. instance OAI.Erdos970.NumberTheoryLean.InitialRegeneration.hitOrReturn_isMarkovKernel line 119
  13. theorem OAI.Erdos970.NumberTheoryLean.InitialRegeneration.hitOrReturn_ae_regeneration line 121
  14. theorem OAI.Erdos970.NumberTheoryLean.InitialRegeneration.hitOrReturn_cost_monotone line 129
  15. def OAI.Erdos970.NumberTheoryLean.InitialRegeneration.delayedRegeneration line 139
  16. instance OAI.Erdos970.NumberTheoryLean.InitialRegeneration.delayedRegeneration_isMarkovKernel line 141
  17. theorem OAI.Erdos970.NumberTheoryLean.InitialRegeneration.delayedRegeneration_ae_regeneration line 145
  18. theorem OAI.Erdos970.NumberTheoryLean.InitialRegeneration.delayedRegeneration_cost_nonneg line 150
  19. theorem OAI.Erdos970.NumberTheoryLean.InitialRegeneration.exponential_total_eq line 158
  20. theorem OAI.Erdos970.NumberTheoryLean.InitialRegeneration.delayedRegeneration_uniform_exponential line 170
  21. def OAI.Erdos970.NumberTheoryLean.InitialRegeneration.delayedCostLaw line 214
  22. instance OAI.Erdos970.NumberTheoryLean.InitialRegeneration.delayedCostLaw_isProbabilityMeasure line 216
  23. theorem OAI.Erdos970.NumberTheoryLean.InitialRegeneration.delayedCostLaw_uniform_exponential line 220
  24. def OAI.Erdos970.NumberTheoryLean.InitialOccupation.beforeRegeneration line 244
  25. instance OAI.Erdos970.NumberTheoryLean.InitialOccupation.beforeRegeneration_isSFiniteKernel line 248
  26. def OAI.Erdos970.NumberTheoryLean.InitialOccupation.initialOccupation line 252
  27. instance OAI.Erdos970.NumberTheoryLean.InitialOccupation.initialOccupation_isSFiniteKernel line 255
  28. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupation.pairedOccupation_unfold_cycles line 259
  29. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupation.pairedOccupation_first_hit_split line 267
  30. def OAI.Erdos970.NumberTheoryLean.InitialOccupation.evenEmbeddingKernel line 281
  31. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupation.firstOdd_intertwines line 284
  32. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupation.fullOccupation_eq_potential line 292
  33. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupation.fullOccupation_unfold line 298
  34. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupation.fullOccupation_odd_kernel line 302
  35. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupation.fullOccupation_even_first_draw line 308
  36. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupation.initial_occupation_decomposition line 317
  37. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupation.initial_occupation_decomposition_apply line 325
  38. instance OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.fullOccupation_isSFiniteKernel line 345
  39. theorem OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.shifts_commute_fullOccupation line 349
  40. theorem OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.fullOccupation_translation line 356
  41. theorem OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.fullOccupation_regeneration line 363
  42. theorem OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.fullOccupation_regeneration_law line 374
  43. def OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.fullResponse line 382
  44. theorem OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.fullResponse_measurable line 385
  45. theorem OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.fullResponse_uniform_bound line 389
  46. theorem OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.fullResponse_limit line 393
  47. theorem OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.fullOccupation_regeneration_integral line 397
  48. theorem OAI.Erdos970.NumberTheoryLean.FullOccupationCovariance.fullOccupation_regeneration_integrable line 408
  49. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupationMoments.occupation_cost_monotone line 434
  50. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupationMoments.beforeRegeneration_cost_monotone line 439
  51. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupationMoments.initialOccupation_cost_nonneg line 446
  52. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupationMoments.initialOccupation_uniform_exponential line 457
  53. instance OAI.Erdos970.NumberTheoryLean.InitialOccupationMoments.initialOccupation_isFiniteMeasure line 507
  54. theorem OAI.Erdos970.NumberTheoryLean.InitialOccupationMoments.initialOccupation_test_decay line 519
  55. theorem OAI.Erdos970.NumberTheoryLean.UniformDelayedLimit.exponential_integrable_of_bound line 568
  56. theorem OAI.Erdos970.NumberTheoryLean.UniformDelayedLimit.uniform_shift_limit line 578
  57. theorem OAI.Erdos970.NumberTheoryLean.UniformDelayedLimit.actual_delayed_response_limit line 635
  58. theorem OAI.Erdos970.NumberTheoryLean.EvenStartOccupation.compactBound_norm line 659
  59. theorem OAI.Erdos970.NumberTheoryLean.EvenStartOccupation.initial_test_integrable line 668
  60. theorem OAI.Erdos970.NumberTheoryLean.EvenStartOccupation.future_after_delay_integrable line 675
  61. theorem OAI.Erdos970.NumberTheoryLean.EvenStartOccupation.even_full_test_integrable line 690
  62. theorem OAI.Erdos970.NumberTheoryLean.EvenStartOccupation.even_full_signed_decomposition line 696
  63. def OAI.Erdos970.NumberTheoryLean.EvenStartOccupation.evenResponse line 711
  64. theorem OAI.Erdos970.NumberTheoryLean.EvenStartOccupation.uniform_even_occupation_limit line 714
  65. theorem OAI.Erdos970.NumberTheoryLean.EvenStartOccupation.source_start_occupation_limit line 744
  66. def OAI.Erdos970.NumberTheoryLean.NormalizedOccupationLimit.invariantAverage line 767
  67. theorem OAI.Erdos970.NumberTheoryLean.NormalizedOccupationLimit.occupation_constant_eq line 770
  68. theorem OAI.Erdos970.NumberTheoryLean.NormalizedOccupationLimit.normalized_regeneration_occupation_limit line 775
  69. theorem OAI.Erdos970.NumberTheoryLean.NormalizedOccupationLimit.normalized_uniform_even_occupation_limit line 780
  70. theorem OAI.Erdos970.NumberTheoryLean.NormalizedOccupationLimit.source_compact_occupation_limit line 786
  71. instance OAI.Erdos970.NumberTheoryLean.RegenerationBandBounds.cycleRenewal_sFinite line 809
  72. def OAI.Erdos970.NumberTheoryLean.RegenerationBandBounds.stateBandReward line 813
  73. theorem OAI.Erdos970.NumberTheoryLean.RegenerationBandBounds.sub_mem_band_iff line 816
  74. theorem OAI.Erdos970.NumberTheoryLean.RegenerationBandBounds.regeneration_band_identity line 820
  75. theorem OAI.Erdos970.NumberTheoryLean.RegenerationBandBounds.regeneration_uniform_band line 848