OAI/NumberTheory/TotientAsymptotic/FordInputs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Totient asymptotics from structural, sieve, prime-counting, and renewal estimates.

  1. theorem OAI.TotientAsymptotic.main_from_ford_inputs line 21
  2. theorem OAI.TotientAsymptotic.companion_from_ford_inputs line 32
  3. theorem OAI.TotientAsymptotic.companion_one_two_from_ford_inputs line 46