OAI/NumberTheory/TotientAsymptotic/DyadicLogGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Elementary log-log comparisons at dyadic endpoints.

  1. lemma OAI.TotientAsymptotic.dyadic_B_tendsto line 11
  2. lemma OAI.TotientAsymptotic.double_log_double_le line 14
  3. lemma OAI.TotientAsymptotic.dyadic_log_index_le line 28
  4. lemma OAI.TotientAsymptotic.dyadic_normality_polynomial line 38