OAI/NumberTheory/TwoPointCorrelations/ModFivePositivity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The de la Vallée Poussin positivity inequality for modulus five. The proof is termwise and uses the actual Mangoldt Dirichlet series. It does not assume a zero-free region or a prime-number estimate.

  1. lemma OAI.TwoPointCorrelations.modFive_three_four_one_nonneg line 15

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePositivity.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFive_phase_norm line 24

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

  3. lemma OAI.TwoPointCorrelations.modFive_twisted_phase_norm line 29

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePositivity.lean:29 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFive_real_mangoldt_term line 35

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePositivity.lean:35 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.modFive_twisted_mangoldt_term line 42

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePositivity.lean:42 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.modFive_double_phase line 54

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePositivity.lean:54 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.modFive_mangoldt_term_positivity line 62

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePositivity.lean:62 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.modFive_mangoldt_series_positivity line 83

    Source documentation

    Positivity of the three actual, absolutely convergent Mangoldt series.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePositivity.lean:83 (same declaration text).

    theorem modFive_mangoldt_series_positivity (χ : DirichletCharacter ℂ 5)
    {σ : ℝ} (hσ : 1 < σ) (t : ℝ) :
    0 ≤ 3 * (LSeries (fun m => (vonMangoldt m : ℂ)) (σ : ℂ)).re +
      4 * (LSeries (modFiveMangoldtTwist χ) ((σ : ℂ) + Complex.I * (t : ℂ))).re +
      (LSeries (modFiveMangoldtTwist (χ ^ 2))
        ((σ : ℂ) + Complex.I * ((2 * t : ℝ) : ℂ))).re := by
…

    Mentions: OAI.TwoPointCorrelations.modFiveMangoldtTwist

  9. lemma OAI.TwoPointCorrelations.modFive_twisted_series_logderiv line 98

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePositivity.lean:98 (same declaration text).

  10. theorem OAI.TwoPointCorrelations.modFive_logderiv_positivity line 108

    Source documentation

    The fixed-character logarithmic-derivative inequality needed by the quantitative zero-free-region proof.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePositivity.lean:108 (same declaration text).

    theorem modFive_logderiv_positivity (χ : DirichletCharacter ℂ 5)
    {σ : ℝ} (hσ : 1 < σ) (t : ℝ) :
    0 ≤ 3 * (-deriv riemannZeta (σ : ℂ) / riemannZeta (σ : ℂ)).re +
      4 * (-deriv (DirichletCharacter.LFunction χ)
        ((σ : ℂ) + Complex.I * (t : ℂ)) /
        DirichletCharacter.LFunction χ ((σ : ℂ) + Complex.I * (t : ℂ))).re +
      (-deriv (DirichletCharacter.LFunction (χ ^ 2))
        ((σ : ℂ) + Complex.I * ((2 * t : ℝ) : ℂ)) /
        DirichletCharacter.LFunction (χ ^ 2)
          ((σ : ℂ) + Complex.I * ((2 * t : ℝ) : ℂ))).re := by
…