OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimeRecurrence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The classical mean-value recurrence from a finite supply of primes. All analytic prime-supply requirements appear as elementary bounds on P.

  1. lemma OAI.TwoPointCorrelations.halasz_distinct_moment_total line 12
  2. theorem OAI.TwoPointCorrelations.halasz_vinogradov_prime_sum line 23