OAI/NumberTheory/TwoPoint/Halasz/HalaszSmallPrimeSamples.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The small additional-prime branch, using the proved integer kernel.

  1. lemma OAI.TwoPointCorrelations.halasz_sparse_cofactor_bounded line 13
  2. theorem OAI.TwoPointCorrelations.halasz_small_prime_samples line 30
  3. theorem OAI.TwoPointCorrelations.halasz_small_prime_integral line 54