OAI/NumberTheory/TwoPointCorrelations/ModFiveRightBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence bounds on the right Perron line. The twisted series is dominated term by term by the untwisted Mangoldt series, whose pole bound controls the series uniformly.

  1. lemma OAI.TwoPointCorrelations.modFive_mangoldt_norm line 15

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

  2. lemma OAI.TwoPointCorrelations.modFive_logderiv_right_domination line 22

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveRightBound.lean:22 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.modFive_logderiv_right_bound line 55

    Source documentation

    A uniform right-line bound, valid for every character, with only the explicit simple-pole dependence on the distance from one.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveRightBound.lean:55 (same declaration text).

    theorem modFive_logderiv_right_bound : ∃ C : ℝ, 0 < C ∧
    ∀ (χ : DirichletCharacter ℂ 5) (δ t : ℝ), 0 < δ →
      ‖-deriv (DirichletCharacter.LFunction χ) (((1 + δ : ℝ) : ℂ) + (t : ℂ) * Complex.I) /
        DirichletCharacter.LFunction χ (((1 + δ : ℝ) : ℂ) + (t : ℂ) * Complex.I)‖ ≤
          1 / δ + C := by
…