OAI/NumberTheory/Ostmann/QuadraticCenter/SmallKernelQuadraticSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.small_kernel_quadratic_sum_bound line 14

   Source documentation

   The cutoff may include a complex quadratic phase. Only its absolute bound enters this estimate, while the interval covers at least one period.

   theorem small_kernel_quadratic_sum_bound (q W : ℕ) [NeZero q]
       (g : ZMod q → ℂ) (hg : ∀ x, ¬IsUnit x → g x = 0)
       (henergy : (∑ x : ZMod q, ‖g x‖ ^ 2) ≤ q)
       (a : ZMod q) (weight : ℕ → ℂ) (B C N : ℝ)
       (hB : 0 ≤ B) (hN : 0 < N)
       (hq : (q : ℝ) ≤ N) (hW : (W : ℝ) ≤ C * N)
       (hw : ∀ w ∈ Finset.Ioc 0 W, ‖weight w‖ ≤ B) :
       ‖(N : ℂ)⁻¹ * ∑ w ∈ Finset.Ioc 0 W, g (a * (w : ZMod q) ^ 2) * weight w‖ ≤
         B * (C + 1) * Real.sqrt ((2 : ℝ) ^ (q.primeFactors.card + 1)) := by
   …