OAI/NumberTheory/TotientAsymptotic/BootstrapExceptionalCount.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Explicit, rather than merely vanishing, preliminary exceptional-value bounds.

  1. def OAI.TotientAsymptotic.bootstrapErrorWeight line 13
  2. lemma OAI.TotientAsymptotic.bootstrap_error_weight_pos line 16
  3. lemma OAI.TotientAsymptotic.bootstrap_error_weight_dominates line 19
  4. lemma OAI.TotientAsymptotic.bootstrap_non_normal_nat_count line 32
  5. lemma OAI.TotientAsymptotic.bootstrap_error_weight_mul line 91
  6. lemma OAI.TotientAsymptotic.bootstrap_regularity_nat_count line 99
  7. lemma OAI.TotientAsymptotic.bootstrap_good_nat_count line 176
  8. theorem OAI.TotientAsymptotic.bootstrap_good_nat_gaussian line 233