OAI/NumberTheory/TotientAsymptotic/TotientCountingEnvelope.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite dyadic counting envelope used to bootstrap the global upper bound.

  1. def OAI.TotientAsymptotic.dyadicTotientEnvelope line 11
  2. lemma OAI.TotientAsymptotic.dyadicTotientEnvelope_one_le line 15
  3. lemma OAI.TotientAsymptotic.dyadicTotientEnvelope_mono line 17
  4. lemma OAI.TotientAsymptotic.dyadicTotientEnvelope_term_le line 25
  5. lemma OAI.TotientAsymptotic.dyadic_totient_count_le line 32
  6. lemma OAI.TotientAsymptotic.totient_values_subset line 40
  7. lemma OAI.TotientAsymptotic.V_monotone line 47
  8. lemma OAI.TotientAsymptotic.dyadic_totient_reciprocal_mass line 51