OAI/NumberTheory/JointDickman/Arithmetic/TotientProductTruncation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A mean approximation of the totient ratio by finitely many prime factors

  1. def OAI.JointDickman.totientLocalProduct line 10
  2. theorem OAI.JointDickman.prime_totient_increment_bound line 13
  3. theorem OAI.JointDickman.prime_totient_increment_sum line 24
  4. theorem OAI.JointDickman.prime_totient_increment_tail line 36
  5. theorem OAI.JointDickman.totientLocalProduct_eq_ratio line 47
  6. theorem OAI.JointDickman.totientLocalProduct_mono line 70
  7. theorem OAI.JointDickman.totientLocalProduct_mean_error line 89