OAI/NumberTheory/TotientAsymptotic/NormalRemainderLayer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Ford normality applied to each actual positive-index witness layer.

  1. def OAI.TotientAsymptotic.nonNormalRemainders line 16
  2. lemma OAI.TotientAsymptotic.primeFinal_remainder line 20
  3. lemma OAI.TotientAsymptotic.basic_suffix_discard_bound line 26
  4. theorem OAI.TotientAsymptotic.normal_remainder_layer_mass line 50