OAI/NumberTheory/JointDickman/Arithmetic/PrimePairCorrelations.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.even_kernel_pair_sum line 9
2. lemma OAI.JointDickman.prime_positive_difference_sum_le line 43
3. theorem OAI.JointDickman.prime_even_kernel_bound line 90

   Source documentation

   An even nonnegative prime correlation kernel is bounded by its diagonal and the explicit totient-weighted sum over positive differences.

   theorem prime_even_kernel_bound : ∃ C : ℝ, 0 < C ∧
       ∀ (Q X : ℕ) (P : Finset ℕ), 2 ≤ Q →
       (∀ p ∈ P, p.Prime ∧ p ≤ Q) →
       (∀ p ∈ P, ∀ r ∈ P, r-p ≤ X) → ∀ K : ℤ → ℝ,
       (∀ h, 0 ≤ K h) → (∀ h, K (-h) = K h) →
       (∑ p ∈ P, ∑ r ∈ P, K ((r:ℤ)-p)) ≤
         (P.card:ℝ)*K 0 + 2*C*(Q:ℝ)/(Real.log Q)^2 *
           ∑ h ∈ Icc 1 X, ((h:ℝ)/h.totient)*K h := by
   …