OAI/NumberTheory/TotientAsymptotic/FiniteCandidateRatio.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded totient ratio for the actual finite geometric candidate family.

  1. lemma OAI.TotientAsymptotic.finite_reverse_geometric_sum line 10
  2. lemma OAI.TotientAsymptotic.finite_geometric_prime_reciprocals line 28
  3. lemma OAI.TotientAsymptotic.prime_factor_ratio_exp line 44
  4. theorem OAI.TotientAsymptotic.finite_candidate_ratio_bound line 57