OAI/NumberTheory/Ostmann/Quadratic/QuadraticSupportCount.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The support-size and scaling bounds for the expanded quadratic sums

  1. theorem OAI.Ostmann.quadratic_support_count_le line 12
  2. theorem OAI.Ostmann.quadratic_support_pair_count line 22
  3. theorem OAI.Ostmann.quadratic_support_scale line 40