OAI/NumberTheory/TotientAsymptotic/RowCutoffModel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The size of the explicit residual cutoff for Ford's exponential row slack.

  1. def OAI.TotientAsymptotic.rowModelDecay line 9
  2. def OAI.TotientAsymptotic.rowModelConstant line 12
  3. lemma OAI.TotientAsymptotic.row_model_decay_bounds line 16
  4. lemma OAI.TotientAsymptotic.row_model_decay_log line 29
  5. lemma OAI.TotientAsymptotic.row_model_constant_nonneg line 38
  6. lemma OAI.TotientAsymptotic.row_model_cutoff_log_bound line 48
  7. lemma OAI.TotientAsymptotic.row_model_mass_exponent_bound line 66