OAI/NumberTheory/TotientAsymptotic/FordTupleFactors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Basic integer and band-product bounds for tuples satisfying Ford's published conditions.

  1. lemma OAI.TotientAsymptotic.ford_shift_pos line 10
  2. lemma OAI.TotientAsymptotic.ford_left_product_pos line 17
  3. lemma OAI.TotientAsymptotic.ford_right_product_pos line 21
  4. lemma OAI.TotientAsymptotic.ford_product_le_y line 25
  5. lemma OAI.TotientAsymptotic.ford_left_shift_le_y line 37
  6. lemma OAI.TotientAsymptotic.ford_right_product_le_y line 44
  7. lemma OAI.TotientAsymptotic.ford_right_shift_le_y line 61
  8. lemma OAI.TotientAsymptotic.ford_common_band line 68