OAI/NumberTheory/TwoPoint/Fourier/ModFivePrimeNumberTheorem.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The fixed modulus-five prime number theorem follows from the three nonprincipal contour estimates, the zeta prime number theorem, and finite character orthogonality.

  1. lemma OAI.TwoPointCorrelations.modFive_character_card line 18
  2. lemma OAI.TwoPointCorrelations.modFive_rate_mono line 24
  3. theorem OAI.TwoPointCorrelations.modFive_all_character_error line 29
  4. lemma OAI.TwoPointCorrelations.modFive_selected_psi_error line 58
  5. theorem OAI.TwoPointCorrelations.modFive_eventual_psi line 83
  6. theorem OAI.TwoPointCorrelations.modFiveThetaInput line 116

    Source documentation

    The logarithmically weighted prime estimate in the two selected modulus-five classes, obtained by contour integration and orthogonality.

    theorem modFiveThetaInput : ModFiveThetaInput := by
…

    Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput