OAI/NumberTheory/Ostmann/Characters/ReciprocalTwist.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The reciprocal twist used in the uniform Mellin estimate

Inversion preserves the finite-field squared norm. The mean of the reciprocal twist is exactly an additive Fourier coefficient of the original multiplicatively twisted test.

  1. def OAI.Ostmann.reciprocalTwist line 17
  2. theorem OAI.Ostmann.reciprocalTwist_zero line 21
  3. theorem OAI.Ostmann.norm_reciprocalTwist line 26
  4. theorem OAI.Ostmann.reciprocalTwist_energy line 36
  5. theorem OAI.Ostmann.reciprocalTwist_mean line 42