OAI/NumberTheory/JointDickman/Analysis/CharacterDistanceInput.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The published Dirichlet-character distance estimate

Only the fixed-modulus consequence of Klurman--Mangerel--Teräväinen, Multiplicative functions in short arithmetic progressions, Proc. London Math. Soc. 127 (2023), 366--446, Lemma 7.8, is assumed here. That lemma bounds the infimum over |t| ≤ 10X by (1/4) log (log X / log (2 conductor χ)) + O(1). For a fixed character the conductor term is absorbed in the constant. The primes dividing the modulus only add nonnegative terms to our distance. No modified character, bin label, or short average occurs in this input. Source: https://doi.org/10.1112/plms.12546, arXiv:1909.12280, Lemma 7.8.

  1. def OAI.JointDickman.characterArithmetic line 21
  2. theorem OAI.JointDickman.characterArithmetic_prime line 25
  3. theorem OAI.JointDickman.characterArithmetic_norm_le_one line 29
  4. theorem OAI.JointDickman.characterArithmetic_multiplicative line 35
  5. def OAI.JointDickman.PublishedInputs.CharacterDistanceInput line 45
  6. def OAI.JointDickman.CharacterDistanceDivergence line 54
  7. theorem OAI.JointDickman.characterDistanceDivergence_of_published line 60

    Source documentation

    The quantitative character-distance bound implies qualitative divergence.

    theorem characterDistanceDivergence_of_published (hKMT : CharacterDistanceInput) :
    CharacterDistanceDivergence := by
…

    Mentions: OAI.JointDickman.CharacterDistanceDivergence