OAI/NumberTheory/Ostmann/QuadraticCenter/InverseWeylPhase.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.QuadraticCenter.weylPhase line 8
  2. theorem OAI.Ostmann.QuadraticCenter.weylPhase_norm line 10
  3. theorem OAI.Ostmann.QuadraticCenter.weylPhase_zero line 11
  4. theorem OAI.Ostmann.QuadraticCenter.weylPhase_add line 12
  5. theorem OAI.Ostmann.QuadraticCenter.weylPhase_sub line 14
  6. theorem OAI.Ostmann.QuadraticCenter.weylPhase_int line 16
  7. theorem OAI.Ostmann.QuadraticCenter.weylPhase_sub_int line 19
  8. theorem OAI.Ostmann.QuadraticCenter.weylPhase_nat_mul line 21
  9. def OAI.Ostmann.QuadraticCenter.integerDistance line 24
  10. theorem OAI.Ostmann.QuadraticCenter.integerDistance_nonneg line 25
  11. theorem OAI.Ostmann.QuadraticCenter.integerDistance_le_half line 26
  12. theorem OAI.Ostmann.QuadraticCenter.integerDistance_le line 27
  13. theorem OAI.Ostmann.QuadraticCenter.phase_sub_one_lower line 29
  14. theorem OAI.Ostmann.QuadraticCenter.linear_weyl_bound line 50