OAI/NumberTheory/TotientAsymptotic/BootstrapMajorant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A concrete logarithmic majorant for the counting recurrence.

  1. def OAI.TotientAsymptotic.bootstrapHeight line 11
  2. def OAI.TotientAsymptotic.bootstrapMajorant line 12
  3. lemma OAI.TotientAsymptotic.bootstrapHeight_one_le line 14
  4. lemma OAI.TotientAsymptotic.bootstrapHeight_mono line 19
  5. lemma OAI.TotientAsymptotic.bootstrapMajorant_one_le line 27
  6. lemma OAI.TotientAsymptotic.bootstrapMajorant_mono line 29
  7. lemma OAI.TotientAsymptotic.bootstrapHeight_tendsto line 36
  8. lemma OAI.TotientAsymptotic.majorant_real_drop line 45
  9. lemma OAI.TotientAsymptotic.bootstrap_majorant_contraction line 63