OAI/NumberTheory/TwoPoint/Fourier/ModFiveCenterBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform lower bounds on Re s = 2, from the exact Möbius inverse. Together with the Abel upper bound these give the polynomial bound for a normalized analytic disk used in the fixed-modulus zero-free argument.

  1. def OAI.TwoPointCorrelations.modFiveInverseConstant line 15

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveCenterBounds.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFiveInverseConstant_pos line 18

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

  3. lemma OAI.TwoPointCorrelations.modFive_twisted_moebius_norm line 24

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveCenterBounds.lean:24 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFive_inverse_series_norm_le line 32

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveCenterBounds.lean:32 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.modFive_LFunction_inv_norm line 53

    Source documentation

    Uniform reciprocal bound, independent of the imaginary part and character.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveCenterBounds.lean:53 (same declaration text).

    theorem modFive_LFunction_inv_norm (χ : DirichletCharacter ℂ 5)
    {s : ℂ} (hs : s.re = 2) :
    ‖(DirichletCharacter.LFunction χ s)⁻¹‖ ≤ modFiveInverseConstant := by
…

    Mentions: OAI.TwoPointCorrelations.modFiveInverseConstant

  6. def OAI.TwoPointCorrelations.modFiveNormalizedLFunction line 66

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveCenterBounds.lean:66 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.modFiveNormalizedLFunction_zero line 71

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

  8. lemma OAI.TwoPointCorrelations.modFiveNormalizedLFunction_differentiable line 77

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveCenterBounds.lean:77 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.modFiveNormalizedLFunction_norm line 85

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveCenterBounds.lean:85 (same declaration text).