OAI/NumberTheory/Ostmann/Characters/CharacterEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Energy and the principal-character correction

All characters, including the principal one, vanish at zero. Multiplying by a character cannot increase Fourier energy, and the principal twist subtracts the zero-point contribution from every Fourier coefficient.

  1. theorem OAI.Ostmann.norm_mulChar_le_one line 17
  2. theorem OAI.Ostmann.additiveFourier_character_energy_le line 23
  3. theorem OAI.Ostmann.additiveFourier_principal_twist line 35