OAI/NumberTheory/JointDickman/Analysis/CharacterDistanceEuler.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Euler logarithm lower bound for character distance

  1. theorem OAI.JointDickman.characterDistance_ge_log_sub_L line 11

    Source documentation

    The error is absolute and independent of the modulus, character and frequency. This bridge uses only Mertens' estimates and absolute Euler tails.

    theorem characterDistance_ge_log_sub_L : ∃ C : ℝ,
    ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q)
      (X : ℝ), max 2 (Real.exp 1) ≤ X → ∀ t : ℝ,
      Real.log (Real.log X) -
        Real.log ‖χ.LFunction ((1+1/Real.log X:ℝ)+(t:ℂ)*I)‖ - C ≤
        PublishedInputs.primeDistanceSquared (characterArithmetic χ) X t := by
…

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