OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterPositivity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The de la Vallée Poussin positivity inequality for arbitrary positive modulus. 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. def OAI.TwoPointCorrelations.mrtCharacterMangoldtTwist line 17
  2. lemma OAI.TwoPointCorrelations.mrtCharacter_three_four_one_nonneg line 20
  3. lemma OAI.TwoPointCorrelations.mrtCharacter_phase_norm line 29
  4. lemma OAI.TwoPointCorrelations.mrtCharacter_twisted_phase_norm line 34
  5. lemma OAI.TwoPointCorrelations.mrtCharacter_real_mangoldt_term line 40
  6. lemma OAI.TwoPointCorrelations.mrtCharacter_twisted_mangoldt_term line 47
  7. lemma OAI.TwoPointCorrelations.mrtCharacter_double_phase line 59
  8. lemma OAI.TwoPointCorrelations.mrtCharacter_mangoldt_term_positivity line 67
  9. theorem OAI.TwoPointCorrelations.mrtCharacter_mangoldt_series_positivity line 88

    Source documentation

    Positivity of the three actual, absolutely convergent Mangoldt series.

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

    Mentions: OAI.TwoPointCorrelations.mrtCharacterMangoldtTwist

  10. lemma OAI.TwoPointCorrelations.mrtCharacter_twisted_series_logderiv line 103
  11. theorem OAI.TwoPointCorrelations.mrtCharacter_logderiv_positivity line 113

    Source documentation

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

    theorem mrtCharacter_logderiv_positivity [NeZero q] (χ : DirichletCharacter ℂ q)
    {σ : ℝ} (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
…