OAI/NumberTheory/JointDickman/Analysis/CharacterLogFrequency.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Character distance on polynomial logarithmic frequency ranges

This proves the small-frequency part of KMT Lemma 7.8 directly from the classical Dirichlet-series growth estimate. The full input has a larger frequency range and is not asserted here.

  1. lemma OAI.JointDickman.character_log_frequency_norm line 15
  2. theorem OAI.JointDickman.characterDistance_log_frequency line 70

    Source documentation

    This is an unconditional bound on every fixed polynomial logarithmic frequency range. It does not replace the full KMT range |t| ≤ X.

    theorem characterDistance_log_frequency {A : ℝ} (hA : 0 ≤ A)
    {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) :
    ∃ C : ℝ, ∀ X : ℝ, max 2 (Real.exp 1) ≤ X → ∀ t : ℝ,
      |t| ≤ (Real.log X)^A →
      (3/4:ℝ)*Real.log (Real.log X)-C ≤
        PublishedInputs.primeDistanceSquared (characterArithmetic χ) X t := by
…

    Mentions: OAI.JointDickman.PublishedInputs.primeDistanceSquared, OAI.JointDickman.characterArithmetic