OAI/NumberTheory/JointDickman/Arithmetic/PrimePairAllCutoffs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Extending the prime-pair sieve estimate to every cutoff

  1. theorem OAI.JointDickman.primePair_count_le line 9
  2. theorem OAI.JointDickman.primePair_upper_sieve line 14

    Source documentation

    The uniform prime-pair upper sieve, at every integer cutoff at least two.

    theorem primePair_upper_sieve : ∃ C : ℝ, 0 < C ∧
    ∀ Q h : ℕ, 2 ≤ Q → 0 < h →
      (primePairCount Q h:ℝ) ≤ C*((h:ℝ)/h.totient)*(Q:ℝ)/(Real.log Q)^2 := by
…

    Mentions: OAI.JointDickman.primePairCount