OAI/NumberTheory/TotientAsymptotic/ShiftedSieveCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact translation of simultaneous shifted primes into the Selberg sieve.

  1. def OAI.TotientAsymptotic.shiftedPrimePairs line 11
  2. lemma OAI.TotientAsymptotic.shiftedPrimePair_coprime line 14
  3. lemma OAI.TotientAsymptotic.shiftedPrimePairs_le_sifted line 27
  4. lemma OAI.TotientAsymptotic.shiftedPrimeSieve_multSum line 51
  5. theorem OAI.TotientAsymptotic.shiftedPrimePairs_selberg line 61

    Source documentation

    A genuine sieve bound for the actual prime pairs, with the exact local remainders still visible for the next arithmetic estimate.

    theorem shiftedPrimePairs_selberg (b X z : ℕ) (y : ℝ) (hy : 1 ≤ y) :
    let s := shiftedPrimeSieve b X z y hy
…

    Mentions: OAI.TotientAsymptotic.shiftedPrimeSieve