OAI/NumberTheory/TotientAsymptotic/ShiftedSieveModel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The concrete two-linear-form sieve used for shifted primes.

  1. def OAI.TotientAsymptotic.shiftedSievePolynomial line 11
  2. lemma OAI.TotientAsymptotic.shiftedSievePolynomial_strictMono line 13
  3. def OAI.TotientAsymptotic.oddSievePrimes line 20
  4. lemma OAI.TotientAsymptotic.mem_oddSievePrimes line 23
  5. lemma OAI.TotientAsymptotic.oddSievePrimes_prod_squarefree line 26
  6. lemma OAI.TotientAsymptotic.mem_oddSievePrimes_of_dvd line 36
  7. def OAI.TotientAsymptotic.shiftedSieveDensity line 42
  8. lemma OAI.TotientAsymptotic.shiftedSieveDensity_prime line 45
  9. lemma OAI.TotientAsymptotic.shiftedSieveDensity_positive line 49
  10. lemma OAI.TotientAsymptotic.shiftedSieveDensity_lt_one line 54
  11. def OAI.TotientAsymptotic.shiftedPrimeSieve line 64

    Source documentation

    Every density and support here is concrete; only the local discrepancy and bounding sum remain to be estimated in the subsequent counting argument.

    def shiftedPrimeSieve (b X z : ℕ) (y : ℝ) (hy : 1 ≤ y) : SelbergSieve where
…