OAI/NumberTheory/Ostmann/Characters/GaussFourthMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Fourth moments after a nonprincipal multiplicative twist

Gauss convolution transfers the weighted character fourth moment to Fourier coefficients. The character inversion merely permutes the nonprincipal characters.

  1. theorem OAI.Ostmann.normalizedGauss_norm_sq line 23
  2. theorem OAI.Ostmann.additiveFourier_character_norm_four line 30
  3. theorem OAI.Ostmann.nonprincipal_fourier_fourth_bound line 57