OAI/NumberTheory/Ostmann/Characters/AffineFourier.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The affine action in the Fourier basis

On nonzero additive frequencies the affine action is a matrix whose entries are additive character sums. Parseval bounds its squared matrix norm by p times the coefficient energy. This is the finite matrix estimate in the proof of the uniform Mellin bound in Section 6.

  1. def OAI.Ostmann.additiveCharacterSum line 19
  2. theorem OAI.Ostmann.additiveCharacterSum_eq line 23
  3. theorem OAI.Ostmann.additiveCharacterSum_energy line 30
  4. theorem OAI.Ostmann.additiveCharacterSum_unit_energy_le line 42
  5. def OAI.Ostmann.affineFourierMatrix line 53

    Source documentation

    The input frequency is ξ and the output frequency is η.

    noncomputable def affineFourierMatrix {p : ℕ} [Fact p.Prime]
    (c : (ZMod p)ˣ × ZMod p → ℂ) (η ξ : (ZMod p)ˣ) : ℂ :=
…
  6. theorem OAI.Ostmann.affineFourierMatrix_energy_le line 57
  7. theorem OAI.Ostmann.complex_sum_mul_sq line 75
  8. theorem OAI.Ostmann.finite_matrix_energy_bound line 85
  9. theorem OAI.Ostmann.affineFourier_action_energy_bound line 92
  10. theorem OAI.Ostmann.affineFourier_collected_energy_bound line 101