OAI/NumberTheory/TotientAsymptotic/FordStateIteration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite iteration on images of the actual Ford cutoff states.

  1. def OAI.TotientAsymptotic.fordBandCost line 11
  2. lemma OAI.TotientAsymptotic.fordBandCost_nonneg line 15
  3. lemma OAI.TotientAsymptotic.state_mass_iteration line 20
  4. theorem OAI.TotientAsymptotic.ford_state_iteration line 38