OAI/NumberTheory/Ostmann/Characters/SparseKernelEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.rawAdditiveKernelAction line 11
2. theorem OAI.Ostmann.rawAdditiveKernelAction_fourier line 14
3. theorem OAI.Ostmann.rawAdditiveKernelAction_energy_le line 27
4. theorem OAI.Ostmann.sparseAdditiveKernel_square_fourier line 38
5. theorem OAI.Ostmann.sparseAdditiveKernel_square_multiplier_le line 58

   Source documentation

   Equation (5.8): the square kernel has raw operator norm at most t^2 epsilon. The estimate retains the actual convolution multiplicities.

   theorem sparseAdditiveKernel_square_multiplier_le {p : ℕ} [NeZero p]
       (E : Finset (ZMod p)) (t ε : ℝ) (hE : (E.card : ℝ) ≤ ε * p) (a : ZMod p) :
       ‖(p : ℂ) * additiveFourier
         (fun x => sparseAdditiveKernel E t x * sparseAdditiveKernel E t x) a‖ ≤ t ^ 2 * ε := by
   …

   Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.sparseAdditiveKernel

6. theorem OAI.Ostmann.sparseAdditiveKernel_square_energy_le line 77