OAI/NumberTheory/Ostmann/Quadratic/QuadraticMainCoefficientBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The divisor bound for the actual main-term difference coefficients

  1. theorem OAI.Ostmann.abs_moebius_index_sum line 11
  2. theorem OAI.Ostmann.common_divisor_count_le line 37
  3. theorem OAI.Ostmann.quadraticMainAlpha_abs_le line 45
  4. theorem OAI.Ostmann.quadraticMainBeta_abs_le line 55
  5. theorem OAI.Ostmann.quadraticMainGamma_abs_le line 66