OAI/NumberTheory/JointDickman/Arithmetic/PrimePairUpperBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform upper bound for pairs of primes at a prescribed difference

  1. theorem OAI.JointDickman.primePair_count_log_bound line 12

    Source documentation

    The upper-sieve bound is uniform in the positive difference, including all prime divisors of that difference through the exact totient factor.

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

    Mentions: OAI.JointDickman.primePairCount