OAI/NumberTheory/Ostmann/Quadratic/QuadraticRowNorm.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The least constant for an actual finite set of quadratic rows

  1. def OAI.Ostmann.quadraticRowEnergy line 11
  2. def OAI.Ostmann.QuadraticRowBound line 14
  3. def OAI.Ostmann.quadraticRowNorm line 17
  4. theorem OAI.Ostmann.quadraticRowEnergy_nonneg line 20
  5. theorem OAI.Ostmann.quadraticRowEnergy_trivial line 23
  6. theorem OAI.Ostmann.quadraticRow_ratios_bounded line 30
  7. theorem OAI.Ostmann.quadraticRowNorm_nonneg line 41
  8. theorem OAI.Ostmann.quadraticRowNorm_bound line 48
  9. theorem OAI.Ostmann.quadraticRowNorm_le line 58
  10. theorem OAI.Ostmann.QuadraticRowBound.mono_constant line 67