OAI/NumberTheory/JointDickman/Amplification/PretentiousFrequencySeparation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.primeDistanceSquared_continuous line 10
2. lemma OAI.JointDickman.primeDistance_minimizing_twist line 15
3. theorem OAI.JointDickman.primeDistance_separated_from_minimizer line 26

   Source documentation

   Outside a unit neighborhood of a minimizing twist, the distance tends to infinity uniformly in all bounded coefficient functions. This asserts qualitative separation only, not the numerical rate of MRT Lemma A.4.

   theorem primeDistance_separated_from_minimizer (R : ℝ) :
       ∀ᶠ X : ℝ in atTop, ∀ f : ArithmeticFunction ℂ, (∀ n, ‖f n‖ ≤ 1) →
         ∃ t₀ : ℝ, |t₀| ≤ X ∧
           (∀ t : ℝ, |t| ≤ X → primeDistanceSquared f X t₀ ≤ primeDistanceSquared f X t) ∧
           ∀ t : ℝ, |t| ≤ X → 1 ≤ |t-t₀| → R ≤ primeDistanceSquared f X t := by
   …