OAI/NumberTheory/TotientAsymptotic/SmallValueGaussian.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Values below the three-quarter power are negligible at every Ford dimension.

  1. lemma OAI.TotientAsymptotic.small_value_gaussian_scale line 11
  2. lemma OAI.TotientAsymptotic.small_value_gaussian_count line 54