OAI/NumberTheory/Ostmann/Quadratic/QuadraticSignedInfiniteSum.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact infinite signed-frequency coordinates for the first transform

  1. abbrev OAI.Ostmann.QuadraticOddKernel line 12
  2. abbrev OAI.Ostmann.QuadraticFrequencyIndex line 13
  3. def OAI.Ostmann.quadraticFrequencyValue line 15
  4. theorem OAI.Ostmann.quadraticFrequencyValue_injective line 18
  5. theorem OAI.Ostmann.quadraticFrequencyValue_range line 28
  6. theorem OAI.Ostmann.quadratic_signed_tsum line 48
  7. theorem OAI.Ostmann.quadratic_signed_summable line 57
  8. theorem OAI.Ostmann.quadratic_signed_tsum_iterated line 61