OAI/NumberTheory/JointDickman/Arithmetic/PrimePairSieveCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Applying the proved finite-event sieve to prime pairs

  1. def OAI.JointDickman.primePairCount line 12
  2. theorem OAI.JointDickman.primePair_count_sieve_bound line 18

    Source documentation

    A finite cutoff bound with the exact pair density and a polynomial error. The primes 2 and 3 are omitted so that every local density is at most 1/2.

    theorem primePair_count_sieve_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ Q Z h : ℕ, 3 ≤ Z → 0 < h →
      (primePairCount Q h:ℝ) ≤
        C*(Q+1:ℝ)*((h:ℝ)/h.totient)*
          (∏ p ∈ (Nat.primesLE Z).filter (fun p => 3 < p), (1-1/(p:ℝ)))^2 +
        2*(Z+1:ℝ)*(Z:ℝ)^2+(Z+1:ℝ) := by
…

    Mentions: OAI.JointDickman.primePairCount