OAI/NumberTheory/TotientAsymptotic/PrimeBandProducts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative and nested-truncation identities for actual collision bands.

  1. lemma OAI.TotientAsymptotic.partBetween_support line 11
  2. lemma OAI.TotientAsymptotic.partBetween_prod line 16
  3. lemma OAI.TotientAsymptotic.partBetween_eq_one_of_largest_le line 28
  4. lemma OAI.TotientAsymptotic.partBelow_all_of_largest_le line 35
  5. lemma OAI.TotientAsymptotic.partBelow_nested line 44
  6. lemma OAI.TotientAsymptotic.partBetween_below line 57
  7. lemma OAI.TotientAsymptotic.common_band_product line 72