OAI/NumberTheory/Jacobsthal/Primes/HighPrimeRemoval.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosPrimeInputs.StrongChebyshev.errorScale line 19
  2. theorem OAI.Erdos970.ErdosPrimeInputs.StrongChebyshev.errorScale_nonneg line 22
  3. theorem OAI.Erdos970.ErdosPrimeInputs.StrongChebyshev.psi_eq_original line 25
  4. theorem OAI.Erdos970.ErdosPrimeInputs.StrongChebyshev.sqrt_le_errorScale line 29
  5. theorem OAI.Erdos970.ErdosPrimeInputs.StrongChebyshev.sqrt_isBigO_errorScale line 49
  6. theorem OAI.Erdos970.ErdosPrimeInputs.StrongChebyshev.psi_strong line 56
  7. theorem OAI.Erdos970.ErdosPrimeInputs.StrongChebyshev.theta_strong line 65
  8. def OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.primeLogWeight line 83
  9. def OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.reciprocalPrimes line 84
  10. def OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.invLogWeight line 86
  11. def OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.errorKernel line 87
  12. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.prefix_primeLogWeight line 89
  13. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.reciprocal_eq_weighted line 94
  14. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.hasDerivAt_invLogWeight line 106
  15. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.deriv_invLogWeight line 116
  16. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.invLogWeight_continuousOn line 119
  17. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.deriv_invLogWeight_continuousOn line 124
  18. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.abel_theta line 138
  19. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.error_identity line 147
  20. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.hasDerivAt_loglog line 179
  21. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeAbel.integral_invLogWeight line 186
  22. def OAI.Erdos970.ErdosPrimeInputs.PrimeEndpoints.intervalGuard line 205
  23. def OAI.Erdos970.ErdosPrimeInputs.PrimeEndpoints.intervalSum line 208
  24. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeEndpoints.reciprocal_eq_core line 213
  25. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeEndpoints.selection_difference_bound line 222
  26. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeEndpoints.fiber_sum_le line 226
  27. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeEndpoints.endpoint_difference line 238
  28. def OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.decay line 284
  29. def OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.tailKernel line 285
  30. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.decay_pos line 287
  31. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.decay_antitone line 289
  32. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.hasDerivAt_decay line 295
  33. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.tailKernel_continuousOn line 305
  34. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.hasDerivAt_tailPrimitive line 315
  35. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.tailIntegral line 320
  36. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.tailIntegral_le line 333
  37. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.kernel_comparison line 338
  38. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.endpoint_error_bound line 357
  39. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.integral_error_bound line 369
  40. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeErrorDecay.uniform_prime_interval_error line 398
  41. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrimeMeasure.reciprocal_le_decay line 447
  42. theorem OAI.Erdos970.ErdosPrimeInputs.HarmonicPrimeMeasure.uniform_all_endpoints line 456
  43. def OAI.Erdos970.ErdosPrimeInputs.HarmonicPrimeMeasure.primeExponent line 474
  44. def OAI.Erdos970.ErdosPrimeInputs.HarmonicPrimeMeasure.harmonicMass line 476
  45. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrimeMeasure.exponent_le_iff line 481
  46. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrimeMeasure.exponent_lt_iff line 486
  47. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrimeMeasure.le_exponent_iff line 491
  48. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrimeMeasure.lt_exponent_iff line 496
  49. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrimeMeasure.harmonicMass_eq_intervalSum line 501
  50. theorem OAI.Erdos970.ErdosPrimeInputs.HarmonicPrimeMeasure.harmonic_prime_measure line 515
  51. lemma OAI.Erdos970.ErdosPrimeInputs.MertensStrong.second_error_difference line 556
  52. theorem OAI.Erdos970.ErdosPrimeInputs.MertensStrong.second_error_strong line 565
  53. lemma OAI.Erdos970.ErdosPrimeInputs.MertensStrong.reciprocal_le_decay line 578
  54. lemma OAI.Erdos970.ErdosPrimeInputs.MertensStrong.third_error_identity line 588
  55. theorem OAI.Erdos970.ErdosPrimeInputs.MertensStrong.third_error_strong line 600
  56. def OAI.Erdos970.ErdosPrimeInputs.MertensStrong.primeProduct line 634
  57. theorem OAI.Erdos970.ErdosPrimeInputs.MertensStrong.prime_product_strong line 637
  58. theorem OAI.Erdos970.ErdosInversePrimeBin.prime_bin_theta_error line 672
  59. theorem OAI.Erdos970.ErdosInversePrimeBin.decay_tendsto_zero line 703
  60. theorem OAI.Erdos970.ErdosInversePrimeBin.uniform_bin_theta_error line 710
  61. def OAI.Erdos970.ErdosPrimeInputs.PrimePrefixMass.primesBetween line 736
  62. def OAI.Erdos970.ErdosPrimeInputs.PrimePrefixMass.decreasingPrefixes line 739
  63. def OAI.Erdos970.ErdosPrimeInputs.PrimePrefixMass.prefixWeight line 742
  64. lemma OAI.Erdos970.ErdosPrimeInputs.PrimePrefixMass.mem_decreasingPrefixes line 744
  65. lemma OAI.Erdos970.ErdosPrimeInputs.PrimePrefixMass.prefixWeight_sort line 761
  66. lemma OAI.Erdos970.ErdosPrimeInputs.PrimePrefixMass.sum_prefixWeights line 766
  67. lemma OAI.Erdos970.ErdosPrimeInputs.PrimePrefixMass.prefix_mass_le_exp line 775
  68. lemma OAI.Erdos970.ErdosPrimeInputs.PrimePrefixMass.sum_primesBetween line 784
  69. lemma OAI.Erdos970.ErdosPrimeInputs.PrimePrefixMass.interval_open_closed line 789
  70. theorem OAI.Erdos970.ErdosPrimeInputs.PrimePrefixMass.total_prime_prefix_mass line 798
  71. def OAI.Erdos970.ErdosPrimeInputs.PrimePrefixTail.longPrefixMass line 836
  72. lemma OAI.Erdos970.ErdosPrimeInputs.PrimePrefixTail.prefixWeight_nonneg line 839
  73. lemma OAI.Erdos970.ErdosPrimeInputs.PrimePrefixTail.tilted_weight line 846
  74. lemma OAI.Erdos970.ErdosPrimeInputs.PrimePrefixTail.sum_sorted_products line 852
  75. lemma OAI.Erdos970.ErdosPrimeInputs.PrimePrefixTail.sum_tilted_weights line 862
  76. theorem OAI.Erdos970.ErdosPrimeInputs.PrimePrefixTail.longPrefixMass_le line 868
  77. lemma OAI.Erdos970.ErdosPrimeInputs.LongPrimePaths.fixed_tilt_tail line 902
  78. theorem OAI.Erdos970.ErdosPrimeInputs.LongPrimePaths.long_prime_paths_superpolynomial line 924
  79. def OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.remainingGap line 962
  80. def OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.cutoff line 965
  81. def OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.primeCutoff line 969
  82. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.cutoff_append line 971
  83. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.cutoff_eq_lastD line 977
  84. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.remainingGap_append line 986
  85. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.exponent_monotone line 991
  86. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.cutoff_lower line 1001
  87. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.suffix_le_cutoff line 1008
  88. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.sum_exponents_le line 1020
  89. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.prime_exponent_bounds line 1030
  90. def OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.hasHighState line 1039
  91. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.high_short_gap line 1043
  92. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrimeGeometry.high_small_gap_long line 1070
  93. def OAI.Erdos970.ErdosPrimeInputs.HighPrimeMass.lowGapHighMass line 1088
  94. def OAI.Erdos970.ErdosPrimeInputs.HighPrimeMass.rewardedHighMass line 1093
  95. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrimeMass.lowGapHighMass_le_long line 1099
  96. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrimeMass.rewardedHighMass_le line 1113
  97. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeRemoval.lowGapHighMass_nonneg line 1156
  98. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeRemoval.rewardedHighMass_nonneg line 1161
  99. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrimeRemoval.large_gap_saving line 1166
  100. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrimeRemoval.low_gap_high_removal line 1182
  101. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrimeRemoval.rewarded_high_removal line 1200