OAI/NumberTheory/TotientAsymptotic/BandStates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite factor states for the successive cutoffs in Ford's iteration.

  1. def OAI.TotientAsymptotic.factorProduct line 10
  2. def OAI.TotientAsymptotic.lowerState line 12
  3. def OAI.TotientAsymptotic.stateBand line 17
  4. lemma OAI.TotientAsymptotic.fin_prod_initial line 21
  5. lemma OAI.TotientAsymptotic.stateBand_product line 37
  6. lemma OAI.TotientAsymptotic.lowerState_recover line 44