OAI/NumberTheory/TotientAsymptotic/BandUnionCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sum the actual normal-preimage count over a finite family of cutoff vectors.

  1. def OAI.TotientAsymptotic.NormalBandWitness line 10
  2. theorem OAI.TotientAsymptotic.normal_band_union_count line 17