OAI/NumberTheory/Jacobsthal/Primes/PrimeGridGeometry.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltMonotone.multiplier_measurable line 23
  2. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltMonotone.minRatio_pos line 30
  3. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltMonotone.multiplier_antitone line 33
  4. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltMonotone.ratioMeasure_ae_above line 64
  5. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltMonotone.multiplier_nonnegative_ae line 67
  6. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltMonotone.weighted_ratio_density_eq line 71
  7. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltMonotone.transitionDensity_mass line 86
  8. theorem OAI.Erdos970.NumberTheoryLean.PrimeTiltMonotone.multiplier_ratio_integral line 100
  9. def OAI.Erdos970.NumberTheoryLean.PrimeRatioMeasure.primeAtoms line 121
  10. def OAI.Erdos970.NumberTheoryLean.PrimeRatioMeasure.finitePrimeMeasure line 125
  11. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioMeasure.finitePrimeMeasure_apply line 128
  12. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioMeasure.finitePrimeMeasure_support line 136
  13. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioMeasure.primeAtoms_above line 147
  14. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioMeasure.finitePrimeMeasure_Icc line 154
  15. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioMeasure.finitePrimeMeasure_tilt line 166
  16. theorem OAI.Erdos970.NumberTheoryLean.PrimeRatioMeasure.ratioMeasure_Icc line 178
  17. def OAI.Erdos970.NumberTheoryLean.PrimeCumulativeBound.closedBin line 211
  18. def OAI.Erdos970.NumberTheoryLean.PrimeCumulativeBound.closedMass line 215
  19. theorem OAI.Erdos970.NumberTheoryLean.PrimeCumulativeBound.closed_interval_iff line 217
  20. theorem OAI.Erdos970.NumberTheoryLean.PrimeCumulativeBound.closedMass_eq_harmonic line 239
  21. theorem OAI.Erdos970.NumberTheoryLean.PrimeCumulativeBound.cumulative_subset_closed line 249
  22. theorem OAI.Erdos970.NumberTheoryLean.PrimeCumulativeBound.cumulative_sum_le_closed line 265
  23. theorem OAI.Erdos970.NumberTheoryLean.PrimeCumulativeBound.actual_cumulative_error line 273
  24. theorem OAI.Erdos970.NumberTheoryLean.PrimeRowMass.retained_row_mass line 326
  25. theorem OAI.Erdos970.NumberTheoryLean.PrimeRowNormalization.polynomial_absorption line 376
  26. theorem OAI.Erdos970.NumberTheoryLean.PrimeRowNormalization.retained_row_mass_one_add line 421
  27. def OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.normalizationRate line 444
  28. def OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.normalizationThreshold line 445
  29. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.normalizationRate_pos line 447
  30. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.normalizationThreshold_gt_one line 450
  31. def OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.epsilon line 453
  32. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.epsilon_pos line 455
  33. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.normalizer_pos line 456
  34. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.actual_row_bound line 458
  35. abbrev OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.ChainState line 465
  36. instance OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.(instance at line 467) line 467
  37. instance OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.(instance at line 468) line 468
  38. def OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.childProbability line 470
  39. def OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.liveMass line 473
  40. def OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.liveLaw line 476
  41. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.liveLaw_univ line 480
  42. def OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.completedLaw line 484
  43. def OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.chain line 487
  44. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.chain_none line 493
  45. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.chain_some line 494
  46. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.liveMass_le_one line 498
  47. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.chain_isMarkov line 518
  48. instance OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.chain_pow_markov line 532
  49. def OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.pathLaw line 542
  50. theorem OAI.Erdos970.NumberTheoryLean.PrimeKilledChain.pathLaw_isProbability line 545
  51. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainProbabilities.history_append_eq_iff line 566
  52. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainProbabilities.liveLaw_at_append line 577
  53. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainProbabilities.chain_at_append line 594
  54. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainProbabilities.pathLaw_append line 605
  55. def OAI.Erdos970.NumberTheoryLean.PrimeChainProbabilities.nodeProduct line 618
  56. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainProbabilities.nodeProduct_append line 621
  57. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainProbabilities.nodeProduct_nonnegative line 631
  58. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainProbabilities.pathLaw_singleton_weight line 640
  59. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainProbabilities.source_prime_weight_identity line 673
  60. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainProbabilities.normalized_source_prime_weight line 682
  61. def OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.potential line 705
  62. def OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.visit line 709
  63. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.visit_nonneg line 713
  64. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.potential_nonneg line 718
  65. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.potential_le line 727
  66. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.visit_le_potential line 733
  67. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.child_potential_drift line 745
  68. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.actual_row_drift_ae line 766
  69. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.actual_row_drift line 782
  70. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.finite_compact_potential line 798
  71. theorem OAI.Erdos970.NumberTheoryLean.PrimeCompactVisits.finite_compact_visits line 821
  72. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryHorizon.valid_ratio_lower line 838
  73. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryHorizon.prime_cost_lower line 841
  74. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryHorizon.prime_gap_cost line 858
  75. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryHorizon.prime_final_gap_lower line 864
  76. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryHorizon.prime_source_horizon line 889
  77. theorem OAI.Erdos970.NumberTheoryLean.PrimeHistoryHorizon.history_length_lt line 924
  78. def OAI.Erdos970.NumberTheoryLean.PrimeChainHorizon.stage line 943
  79. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainHorizon.stage_measurable line 947
  80. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainHorizon.next_stage line 949
  81. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainHorizon.pathLaw_stage line 961
  82. theorem OAI.Erdos970.NumberTheoryLean.PrimeChainHorizon.pathLaw_eq_cemetery line 974
  83. def OAI.Erdos970.NumberTheoryLean.PrimeCorrectionFactor.correctionBudget line 1006
  84. theorem OAI.Erdos970.NumberTheoryLean.PrimeCorrectionFactor.correctionBudget_tendsto_zero line 1009
  85. theorem OAI.Erdos970.NumberTheoryLean.PrimeCorrectionFactor.correction_le_budget line 1025
  86. theorem OAI.Erdos970.NumberTheoryLean.PrimeCorrectionFactor.history_correction line 1041
  87. def OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.sideAfter line 1061
  88. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.sideAfter_flip line 1065
  89. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.sideAfter_even line 1070
  90. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.sideAfter_odd line 1077
  91. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.terminal_side_after line 1081
  92. def OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.regularLower line 1089
  93. def OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.weakLower line 1090
  94. def OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.Regular line 1092
  95. def OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.WeakRegular line 1093
  96. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.regular_step line 1095
  97. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.two_step_regular line 1115
  98. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.terminal_regular_of_regular line 1135
  99. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.terminal_regular line 1143
  100. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.weak_step line 1156
  101. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.terminal_weak line 1173
  102. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.pathLaw_regular line 1184
  103. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.pathLaw_weak line 1195
  104. theorem OAI.Erdos970.NumberTheoryLean.PrimeSideSupport.pathLaw_side line 1210
  105. def OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.width line 1231
  106. def OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.point line 1232
  107. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.width_nonneg line 1234
  108. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.width_pos line 1236
  109. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.point_succ line 1240
  110. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.point_nonneg line 1243
  111. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.threshold_le_point line 1245
  112. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.index_from_upper line 1251
  113. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.finite_grid_cover line 1259
  114. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.incoming_grid_end line 1278
  115. def OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.lowerIndex line 1285
  116. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.regular_bin_domain line 1287
  117. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.weak_bin_domain line 1306
  118. theorem OAI.Erdos970.NumberTheoryLean.PrimeGridGeometry.child_bin_domain line 1325