OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterCenterBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The Mobius inverse bounds the reciprocal L-function on Re(s)=2 uniformly in the modulus. Combining this with the q-dependent Abel bound gives growth of the normalized nonprincipal character L-function on a fixed disk. No zero-free region is asserted here.

  1. def OAI.TwoPointCorrelations.mrtCharacterInverseConstant line 17
  2. lemma OAI.TwoPointCorrelations.mrtCharacterInverseConstant_pos line 20
  3. lemma OAI.TwoPointCorrelations.mrtCharacter_twisted_moebius_norm line 27
  4. lemma OAI.TwoPointCorrelations.mrtCharacter_inverse_series_norm_le line 36
  5. theorem OAI.TwoPointCorrelations.mrtCharacter_LFunction_inv_norm line 57

    Source documentation

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

    theorem mrtCharacter_LFunction_inv_norm (χ : DirichletCharacter ℂ q)
    {s : ℂ} (hs : s.re = 2) :
    ‖(DirichletCharacter.LFunction χ s)⁻¹‖ ≤ mrtCharacterInverseConstant := by
…

    Mentions: OAI.TwoPointCorrelations.mrtCharacterInverseConstant

  6. def OAI.TwoPointCorrelations.mrtCharacterNormalizedLFunction line 70
  7. lemma OAI.TwoPointCorrelations.mrtCharacterNormalizedLFunction_zero line 75
  8. lemma OAI.TwoPointCorrelations.mrtCharacterNormalizedLFunction_differentiable line 81
  9. lemma OAI.TwoPointCorrelations.mrtCharacterNormalizedLFunction_norm line 89