OAI/NumberTheory/Ostmann/QuadraticCenter/PositiveQuadraticUniformBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform bound for the positive quadratic series at every kernel

  1. theorem OAI.Ostmann.positiveQuadraticSum_uniform_bound line 11
  2. theorem OAI.Ostmann.positiveQuadraticSum_energy_uniform_bound line 49