OAI/NumberTheory/Ostmann/Characters/SparseMellinCoefficients.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sum_units_eq_sum_nonzero line 13
2. theorem OAI.Ostmann.sparseAdditiveKernel_total_energy line 26
3. theorem OAI.Ostmann.mellinCoefficient_sq_le_energy line 45
4. theorem OAI.Ostmann.sparse_power_mellin_sq_le line 54

   Source documentation

   Both powers used by the squared truncation have the same square-root coefficient bound. The proof uses exact Parseval and |b|<=1.

   theorem sparse_power_mellin_sq_le {p : ℕ} [Fact p.Prime]
       (E : Finset (ZMod p)) (t : ℝ) (ht : 0 ≤ t) (ht1 : t ≤ 1)
       (j : ℕ) (hj : j = 1 ∨ j = 2) (χ : MulChar (ZMod p) ℂ) :
       ‖mellinCoefficient (fun x : (ZMod p)ˣ => sparseAdditiveKernel E t x ^ j) χ‖ ^ 2 ≤
         2 / p := by
   …

   Mentions: OAI.Ostmann.mellinCoefficient, OAI.Ostmann.sparseAdditiveKernel

5. theorem OAI.Ostmann.sparse_power_mellin_le line 109

   Source documentation

   A convenient non-squared bound for the two local powers.

   theorem sparse_power_mellin_le {p : ℕ} [Fact p.Prime]
       (E : Finset (ZMod p)) (t : ℝ) (ht : 0 ≤ t) (ht1 : t ≤ 1)
       (j : ℕ) (hj : j = 1 ∨ j = 2) (χ : MulChar (ZMod p) ℂ) :
       ‖mellinCoefficient (fun x : (ZMod p)ˣ => sparseAdditiveKernel E t x ^ j) χ‖ ≤
         2 / Real.sqrt (p : ℝ) := by
   …

   Mentions: OAI.Ostmann.mellinCoefficient, OAI.Ostmann.sparseAdditiveKernel