OAI/NumberTheory/TwoPointCorrelations/ModFiveMangoldt.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Exact finite reductions for the fixed modulus-five prime input.

The only primes-versus-prime-powers loss is the existing elementary Chebyshev bound. These identities isolate the quantitative Dirichlet L-function estimate still needed to discharge ModFiveThetaInput.

  1. def OAI.TwoPointCorrelations.modFiveResidue line 21

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:21 (same declaration text).

  2. def OAI.TwoPointCorrelations.modFiveMangoldtWeight line 24

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:24 (same declaration text).

  3. def OAI.TwoPointCorrelations.modFivePsi line 27

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:27 (same declaration text).

  4. def OAI.TwoPointCorrelations.modFiveTwistedPsi line 30

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:30 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.modFivePrime_iff line 34

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:34 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.modFive_logWeight_eq line 38

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:38 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.modFive_weight_difference line 44

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:44 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.modFive_weight_difference_nonneg line 52

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:52 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.modFive_weight_difference_le line 59

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:59 (same declaration text).

  10. theorem OAI.TwoPointCorrelations.modFivePsi_sub_theta_bounds line 71

    Source documentation

    Restricting the prime-power error to either selection cannot increase it.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:71 (same declaration text).

    theorem modFivePsi_sub_theta_bounds (one : Bool) (x : ℝ) :
    0 ≤ modFivePsi one x - modFiveTheta one x ∧
      modFivePsi one x - modFiveTheta one x ≤ Chebyshev.psi x - Chebyshev.theta x := by
…

    Mentions: OAI.TwoPointCorrelations.modFivePsi, OAI.TwoPointCorrelations.modFiveTheta

  11. theorem OAI.TwoPointCorrelations.modFivePsi_sub_theta_abs_le line 86

    Source documentation

    The elementary loss in passing from a von Mangoldt estimate to primes.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:86 (same declaration text).

    theorem modFivePsi_sub_theta_abs_le (one : Bool) {x : ℝ} (hx : 1 ≤ x) :
    |modFivePsi one x - modFiveTheta one x| ≤ 2 * Real.sqrt x * Real.log x := by
…

    Mentions: OAI.TwoPointCorrelations.modFivePsi, OAI.TwoPointCorrelations.modFiveTheta

  12. lemma OAI.TwoPointCorrelations.modFiveMangoldtWeight_complement line 91

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:91 (same declaration text).

  13. lemma OAI.TwoPointCorrelations.modFivePsi_complement line 96

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:96 (same declaration text).

  14. lemma OAI.TwoPointCorrelations.modFive_character_sum line 101

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:101 (same declaration text).

  15. theorem OAI.TwoPointCorrelations.modFivePsi_true_character_sum line 111

    Source documentation

    Exact character expansion; no asymptotic input is used here.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:111 (same declaration text).

    theorem modFivePsi_true_character_sum (x : ℝ) :
    (4 : ℂ) * (modFivePsi true x : ℂ) =
      ∑ χ : DirichletCharacter ℂ 5, modFiveTwistedPsi χ x := by
…

    Mentions: OAI.TwoPointCorrelations.modFivePsi, OAI.TwoPointCorrelations.modFiveTwistedPsi

  16. lemma OAI.TwoPointCorrelations.sqrt_mul_log_le_exp_sqrt line 122

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:122 (same declaration text).

  17. theorem OAI.TwoPointCorrelations.modFiveThetaInput_of_psi line 158

    Source documentation

    A quantitative estimate for the selected von Mangoldt sums gives the exact prime estimate used by the application, with unchanged exponent.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveMangoldt.lean:158 (same declaration text).

    theorem modFiveThetaInput_of_psi (c C : ℝ) (hc : 0 < c) (hC : 0 ≤ C)
    (hpsi : ∀ (one : Bool) (x : ℝ), 2 ≤ x →
      |modFivePsi one x - modFiveDensity one * x| ≤
        C * x * Real.exp (-c * Real.sqrt (Real.log x))) :
    ModFiveThetaInput := by
…

    Mentions: OAI.TwoPointCorrelations.modFivePsi, OAI.TwoPointCorrelations.modFiveDensity, OAI.TwoPointCorrelations.ModFiveThetaInput