OAI/NumberTheory/TotientAsymptotic/NormalPrimeBands.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Largest-factor bands derived from normality, including the small-prime case.

  1. lemma OAI.TotientAsymptotic.largestPrimeFactor_le_self line 12
  2. lemma OAI.TotientAsymptotic.normality_total_uniform line 17
  3. lemma OAI.TotientAsymptotic.shifted_doubleLog_lower line 32
  4. lemma OAI.TotientAsymptotic.normal_prime_largest_band line 49