OAI/NumberTheory/TwoPoint/Fourier/ModFivePrincipalCorrection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The principal modulus-five logarithmic derivative differs from the ordinary zeta logarithmic derivative by a single, uniformly bounded Euler factor. This is proved directly from the existing change-of-level identity.

  1. def OAI.TwoPointCorrelations.modFiveEulerFactor line 16

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePrincipalCorrection.lean:16 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFive_principal_eq line 18

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePrincipalCorrection.lean:18 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFiveEulerFactor_cpow_norm line 26

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePrincipalCorrection.lean:26 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFiveEulerFactor_norm_ge line 35

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePrincipalCorrection.lean:35 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.modFiveEulerFactor_ne_zero line 43

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePrincipalCorrection.lean:43 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.modFiveEulerFactor_hasDeriv line 50

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePrincipalCorrection.lean:50 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.modFiveEulerFactor_logderiv_norm line 56

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePrincipalCorrection.lean:56 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.modFive_principal_logderiv line 71

    Source documentation

    Exact principal-character correction, in logarithmic-derivative form.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePrincipalCorrection.lean:71 (same declaration text).

    theorem modFive_principal_logderiv {s : ℂ} (hs : 1 < s.re) :
    deriv (DirichletCharacter.LFunction (1 : DirichletCharacter ℂ 5)) s /
        DirichletCharacter.LFunction (1 : DirichletCharacter ℂ 5) s =
      deriv modFiveEulerFactor s / modFiveEulerFactor s +
        deriv riemannZeta s / riemannZeta s := by
…

    Mentions: OAI.TwoPointCorrelations.modFiveEulerFactor

  9. theorem OAI.TwoPointCorrelations.modFive_principal_logderiv_error line 89

    Source documentation

    The correction at the exceptional prime has an absolute bound.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePrincipalCorrection.lean:89 (same declaration text).

    theorem modFive_principal_logderiv_error {s : ℂ} (hs : 1 < s.re) :
    ‖(-deriv (DirichletCharacter.LFunction (1 : DirichletCharacter ℂ 5)) s /
        DirichletCharacter.LFunction (1 : DirichletCharacter ℂ 5) s) -
      (-deriv riemannZeta s / riemannZeta s)‖ ≤ Real.log 5 / 4 := by
…