OAI/NumberTheory/TotientAsymptotic/CollisionBandData.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A single interval's collision data and its left-right symmetry.

  1. structure OAI.TotientAsymptotic.CollisionBandConditions line 11
  2. lemma OAI.TotientAsymptotic.CollisionBandConditions.common line 28
  3. lemma OAI.TotientAsymptotic.CollisionBandConditions.distinct line 35
  4. lemma OAI.TotientAsymptotic.CollisionBandConditions.swap line 42
  5. lemma OAI.TotientAsymptotic.collision_swap_sum line 53