OAI/NumberTheory/TwoPoint/Fourier/ModFiveZetaPsi.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The principal twisted Mangoldt estimate from the already proved zeta prime number theorem, with the elementary five-power correction retained.

  1. lemma OAI.TwoPointCorrelations.modFive_constant_absorption line 12
  2. theorem OAI.TwoPointCorrelations.modFive_zeta_psi_decay line 27
  3. theorem OAI.TwoPointCorrelations.modFive_principal_psi_decay line 47