OAI/NumberTheory/Jacobsthal/Renewal/UniformCycleMoments.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.OccupationBoundaries.stateRatio_pos line 20
  2. theorem OAI.Erdos970.NumberTheoryLean.OccupationBoundaries.stateKernel_ratio_null line 25
  3. theorem OAI.Erdos970.NumberTheoryLean.OccupationBoundaries.costKernel_level_null line 32
  4. theorem OAI.Erdos970.NumberTheoryLean.OccupationBoundaries.occupation_null_of_transition_null line 48
  5. theorem OAI.Erdos970.NumberTheoryLean.OccupationBoundaries.occupation_level_null line 63
  6. theorem OAI.Erdos970.NumberTheoryLean.OccupationBoundaries.occupation_age_level_null line 70
  7. theorem OAI.Erdos970.NumberTheoryLean.OccupationBoundaries.cost_add_log line 75
  8. theorem OAI.Erdos970.NumberTheoryLean.OccupationBoundaries.occupation_age_log_ratio_level_null line 80
  9. theorem OAI.Erdos970.NumberTheoryLean.OccupationBoundaries.occupation_arrival_boundary_null line 91
  10. instance OAI.Erdos970.NumberTheoryLean.CycleConvolutionLaw.returnLaw_pow_isMarkovKernel line 113
  11. theorem OAI.Erdos970.NumberTheoryLean.CycleConvolutionLaw.cumulative_cost_lintegral line 121
  12. theorem OAI.Erdos970.NumberTheoryLean.CycleConvolutionLaw.cumulative_cost_law line 154
  13. def OAI.Erdos970.NumberTheoryLean.CycleConvolutionLaw.actualArrivalLaw line 165
  14. theorem OAI.Erdos970.NumberTheoryLean.CycleConvolutionLaw.actualArrivalLaw_eq_convPow line 168
  15. theorem OAI.Erdos970.NumberTheoryLean.CycleConvolutionLaw.actualArrival_sum_eq_renewal line 176
  16. theorem OAI.Erdos970.NumberTheoryLean.CycleConvolutionLaw.actual_cycle_key_renewal line 182
  17. abbrev OAI.Erdos970.NumberTheoryLean.CycleResponse.Test line 200
  18. def OAI.Erdos970.NumberTheoryLean.CycleResponse.response line 202
  19. theorem OAI.Erdos970.NumberTheoryLean.CycleResponse.shiftedTest_measurable line 205
  20. theorem OAI.Erdos970.NumberTheoryLean.CycleResponse.shiftedTest_integrable line 209
  21. theorem OAI.Erdos970.NumberTheoryLean.CycleResponse.response_bound line 215
  22. theorem OAI.Erdos970.NumberTheoryLean.CycleResponse.response_zero_left line 219
  23. theorem OAI.Erdos970.NumberTheoryLean.CycleResponse.occupation_age_all_moments line 225
  24. theorem OAI.Erdos970.NumberTheoryLean.CycleResponse.response_continuous_of_ae line 236
  25. theorem OAI.Erdos970.NumberTheoryLean.CycleResponse.response_reciprocal_square_bound line 247
  26. theorem OAI.Erdos970.NumberTheoryLean.CycleResponse.driNorm_le_of_reciprocal_square line 278
  27. theorem OAI.Erdos970.NumberTheoryLean.CycleResponse.response_driNorm line 295
  28. def OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.mask line 311
  29. def OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.HasCompactBound line 313
  30. def OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.ShiftContinuous line 316
  31. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.HasCompactBound.mask line 319
  32. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.HasCompactBound.add line 331
  33. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.HasCompactBound.scale line 342
  34. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.continuousAt_cut_lt line 353
  35. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.continuousAt_cut_le line 364
  36. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.ShiftContinuous.upper line 375
  37. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.ShiftContinuous.upperOpen line 384
  38. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.ShiftContinuous.state line 393
  39. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.ShiftContinuous.arrival line 410
  40. inductive OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible line 420
  41. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.lower line 432
  42. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.lowerOpen line 441
  43. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.intervalIcc line 450
  44. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.intervalIco line 457
  45. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.intervalIoc line 464
  46. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.intervalIoo line 471
  47. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.measurable line 478
  48. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.compactBound line 490
  49. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.shiftContinuous line 500
  50. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.response_continuous line 518
  51. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.Admissible.response_driNorm line 522
  52. theorem OAI.Erdos970.NumberTheoryLean.AdmissibleCycleTests.admissible_cycle_response_renewal line 527
  53. def OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.pairedOccupation line 543
  54. instance OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.pairedOccupation_isSFiniteKernel line 545
  55. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.returnLaw_eq_potential line 549
  56. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.occupationKernel_eq_potential line 551
  57. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.pairedOccupation_cycle_decomposition line 553
  58. def OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.oddEmbeddingKernel line 561
  59. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.oddEmbedding_intertwines line 564
  60. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.oddEmbedding_intertwines_pow line 571
  61. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.pairedCost_pow_full_grouping line 584
  62. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.pairVisits_as_full_kernel line 591
  63. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.pairedVisits_full_grouping line 598
  64. def OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.fullOccupation line 614
  65. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.pairedOccupation_eq_full line 617
  66. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.fullOccupation_cycle_decomposition line 626
  67. theorem OAI.Erdos970.NumberTheoryLean.OccupationDecomposition.fullOccupation_cycle_lintegral line 631
  68. def OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.shiftFullCost line 651
  69. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.shiftFullCost_measurable line 653
  70. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.costKernel_translation line 656
  71. def OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.shiftFullKernel line 667
  72. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.shiftFull_commutes line 670
  73. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.costKernel_pow_translation line 677
  74. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.pairVisits_translation line 685
  75. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.shifts_intertwine_pairVisits line 691
  76. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.shifts_intertwine_occupation line 698
  77. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.occupation_translation line 709
  78. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.pairVisits_regeneration line 716
  79. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.visitBlock_regeneration line 724
  80. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.occupation_regeneration line 738
  81. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.occupation_regeneration_law line 746
  82. def OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.positiveResponse line 752
  83. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.positiveResponse_measurable line 755
  84. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.occupation_response_lintegral line 760
  85. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.occupation_response_integral line 773
  86. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.returnLaw_pow_ae_regeneration line 784
  87. theorem OAI.Erdos970.NumberTheoryLean.OccupationRegeneration.fullOccupation_positive_convolution line 796
  88. theorem OAI.Erdos970.NumberTheoryLean.SignedCycleOccupation.positiveResponse_norm_eq line 823
  89. theorem OAI.Erdos970.NumberTheoryLean.SignedCycleOccupation.positiveResponse_norm_driNorm line 833
  90. theorem OAI.Erdos970.NumberTheoryLean.SignedCycleOccupation.fullOccupation_norm_lintegral_bound line 845
  91. theorem OAI.Erdos970.NumberTheoryLean.SignedCycleOccupation.fullOccupation_test_integrable line 857
  92. theorem OAI.Erdos970.NumberTheoryLean.SignedCycleOccupation.fullOccupation_test_uniform_bound line 864
  93. theorem OAI.Erdos970.NumberTheoryLean.SignedCycleOccupation.fullOccupation_signed_convolution line 876
  94. theorem OAI.Erdos970.NumberTheoryLean.SignedCycleOccupation.fullOccupation_regeneration_limit line 892
  95. def OAI.Erdos970.NumberTheoryLean.CycleResponseFubini.ageShear line 908
  96. theorem OAI.Erdos970.NumberTheoryLean.CycleResponseFubini.ageShear_measurable line 910
  97. theorem OAI.Erdos970.NumberTheoryLean.CycleResponseFubini.ageShear_measurePreserving line 913
  98. theorem OAI.Erdos970.NumberTheoryLean.CycleResponseFubini.unshifted_test_product_integrable line 921
  99. theorem OAI.Erdos970.NumberTheoryLean.CycleResponseFubini.shifted_test_product_integrable line 940
  100. theorem OAI.Erdos970.NumberTheoryLean.CycleResponseFubini.response_integrable line 945
  101. theorem OAI.Erdos970.NumberTheoryLean.CycleResponseFubini.integrated_test_occupation_integrable line 949
  102. theorem OAI.Erdos970.NumberTheoryLean.CycleResponseFubini.integral_response_eq_occupation line 954
  103. def OAI.Erdos970.NumberTheoryLean.OccupationConstant.integratedStateTest line 977
  104. theorem OAI.Erdos970.NumberTheoryLean.OccupationConstant.integratedStateTest_measurable line 979
  105. theorem OAI.Erdos970.NumberTheoryLean.OccupationConstant.response_integral_eq_invariant line 982
  106. theorem OAI.Erdos970.NumberTheoryLean.UniformCycleMoments.geometric_exponential_budget line 1002
  107. theorem OAI.Erdos970.NumberTheoryLean.UniformCycleMoments.return_increment_uniform_exponential line 1034
  108. theorem OAI.Erdos970.NumberTheoryLean.UniformCycleMoments.occupation_increment_uniform_exponential line 1061