OAI/NumberTheory/TotientAsymptotic/BootstrapNormalityDecay.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The normality parameter chosen for the bootstrap gives exponential decay in the log-log scale.

  1. lemma OAI.TotientAsymptotic.loglogCutoff_ge_four line 13
  2. lemma OAI.TotientAsymptotic.bootstrap_normality_factor line 20
  3. lemma OAI.TotientAsymptotic.shifted_sixth_exp_decay line 40