OAI/NumberTheory/TwoPoint/Fourier/ModFivePrincipalPsi.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The principal character only removes powers of five. For the required error bound it is enough to charge the prime 5 once, and all remaining terms to the already proved elementary prime-power error.

  1. lemma OAI.TwoPointCorrelations.modFive_principal_term_bound line 17
  2. lemma OAI.TwoPointCorrelations.modFive_principal_psi_error line 45
  3. lemma OAI.TwoPointCorrelations.modFive_chebyshevPsi_eq line 72