OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimeSupply.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An elementary supply of primes in a fixed multiplicative interval. Chebyshev's bounds suffice; no prime number theorem is needed here.

  1. lemma OAI.TwoPointCorrelations.halasz_theta_eventually_lower line 14
  2. lemma OAI.TwoPointCorrelations.halasz_theta_upper line 45
  3. def OAI.TwoPointCorrelations.halaszPrimeSupply line 57
  4. lemma OAI.TwoPointCorrelations.halasz_prime_supply_mem line 59
  5. lemma OAI.TwoPointCorrelations.halasz_prime_supply_mass line 66
  6. theorem OAI.TwoPointCorrelations.halasz_prime_supply_card line 75