OAI/NumberTheory/JointDickman/Arithmetic/PrimePhaseDivergence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.principalDistance_eq_cosine line 11
2. theorem OAI.JointDickman.prime_cosine_defect_diverges line 28

   Source documentation

   The full frequency range needs only qualitative divergence here; no numerical Vinogradov--Korobov rate is asserted.

   theorem prime_cosine_defect_diverges (R : ℝ) :
       ∀ᶠ X : ℝ in atTop, ∀ t : ℝ, 1 ≤ |t| → |t| ≤ 2*X →
         R ≤ ∑ p ∈ (Icc 2 ⌊X⌋₊).filter Nat.Prime,
           (1 - Real.cos (t * Real.log (p : ℝ))) / (p : ℝ) := by
   …

3. lemma OAI.JointDickman.cosine_defect_le_four_abs_defect line 54
4. theorem OAI.JointDickman.prime_abs_cosine_defect_diverges line 63

   Source documentation

   This is the qualitative two-twist repulsion needed for short averages. It includes the range up to twice the cutoff and has no analytic hypothesis.

   theorem prime_abs_cosine_defect_diverges (R : ℝ) :
       ∀ᶠ X : ℝ in atTop, ∀ t : ℝ, 1 ≤ |t| → |t| ≤ 2*X →
         R ≤ ∑ p ∈ (Icc 2 ⌊X⌋₊).filter Nat.Prime,
           (1 - |Real.cos (t * Real.log (p : ℝ) / 2)|) / (p : ℝ) := by
   …