OAI/NumberTheory/TotientAsymptotic/FailedRowCutoff.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit residual cutoffs satisfying every first-failed-row mass budget.

  1. def OAI.TotientAsymptotic.failedRowCutoff line 9
  2. lemma OAI.TotientAsymptotic.failed_row_cutoff_loglog line 12
  3. lemma OAI.TotientAsymptotic.failed_row_cutoff_budget line 16