OAI/NumberTheory/TotientAsymptotic/TripleEulerProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The dimension-three lower bound for the collision sieve's Euler product.

  1. lemma OAI.TotientAsymptotic.tripleEulerProduct_eq line 11
  2. lemma OAI.TotientAsymptotic.tripleEulerProduct_log_lower line 28
  3. lemma OAI.TotientAsymptotic.triple_exceptional_product_le_totient line 34
  4. lemma OAI.TotientAsymptotic.tripleSieveEulerProduct_lower line 61