OAI/NumberTheory/Ostmann/QuadraticCenter/FullCoefficientMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial absolute mass for the full coefficient family

  1. theorem OAI.Ostmann.fullQuadraticCoefficient_norm_le line 12
  2. theorem OAI.Ostmann.eventual_full_coefficient_point_bound line 31
  3. theorem OAI.Ostmann.eventual_arithmetic_coefficient_mass line 69
  4. theorem OAI.Ostmann.eventual_fixed_quadratic_family_mass line 87