OAI/NumberTheory/Ostmann/Quadratic/QuadraticPairPoisson.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact Poisson summation for a pair of quadratic coefficients

The squarefree kernel is primitive. The common-divisor coprimality factor remains in the Fourier transform as the principal character modulo the gcd. No prime or squarefree terms are discarded.

  1. theorem OAI.Ostmann.principal_character_intCast line 18
  2. theorem OAI.Ostmann.jacobi_pair_complex line 27
  3. theorem OAI.Ostmann.quadratic_pair_poisson line 36