OAI/NumberTheory/TotientAsymptotic/UniformPrimePairBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform elementary upper-bound sieve for q and bq+1.

  1. lemma OAI.TotientAsymptotic.allShiftedPrimePairs_large_bound line 11
  2. theorem OAI.TotientAsymptotic.uniform_prime_pair_bound line 48

    Source documentation

    Uniform in the positive coefficient b; no analytic input is assumed.

    theorem uniform_prime_pair_bound : ∃ C : ℝ, 0<C ∧ ∀ b : ℕ, 0<b →
    ∀ X : ℕ, 2≤X → ((allShiftedPrimePairs b X).card:ℝ) ≤
      C*X*((b:ℝ)/b.totient)/(Real.log X)^2 := by
…

    Mentions: OAI.TotientAsymptotic.allShiftedPrimePairs