OAI/NumberTheory/TwoPoint/Halasz/HalaszAvoidPrimes.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A small family of primes contains a prime preserving distinctness of both long tuples. Only the prime supply is analytic.

  1. lemma OAI.TwoPointCorrelations.halasz_large_prime_divisors line 14
  2. lemma OAI.TwoPointCorrelations.halasz_congruent_prime_count line 35
  3. theorem OAI.TwoPointCorrelations.halasz_bad_residue_prime_count line 56
  4. theorem OAI.TwoPointCorrelations.halasz_exists_good_prime line 81