OAI/NumberTheory/JointDickman/Arithmetic/PrimePhaseRepulsion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Qualitative separation of two pretentious twists

  1. lemma OAI.JointDickman.phase_sum_norm line 10
  2. lemma OAI.JointDickman.two_twist_distance_lower line 30
  3. theorem OAI.JointDickman.two_twist_distance_diverges line 58

    Source documentation

    For any desired distance, two bounded-frequency twists separated by at least one cannot both stay close to the same bounded multiplicative data. The bound is uniform in the coefficient function.

    theorem two_twist_distance_diverges (R : ℝ) :
    ∀ᶠ X : ℝ in atTop, ∀ (f : ArithmeticFunction ℂ), (∀ n, ‖f n‖ ≤ 1) →
      ∀ t s : ℝ, |t| ≤ X → |s| ≤ X → 1 ≤ |t-s| →
        2*R ≤ primeDistanceSquared f X t + primeDistanceSquared f X s := by
…