QuadraticWeylBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A concrete quadratic Weyl bound from one differencing step

theorem OAI.Ostmann.quadratic_weyl_bound line 14

Source documentation

The bound is uniform in the linear coefficient. It is derived from the finite block-packing argument, with no external exponential-sum hypothesis.

theorem quadratic_weyl_bound (α β : ℝ) (a : ℤ) (r N : ℕ)
    (hr : 2 ≤ r) (hcop : a.natAbs.Coprime r)
    (happrox : |2 * α - (a : ℝ) / r| ≤ 1 / (r : ℝ) ^ 2) :
    ‖∑ j ∈ Finset.range N, realQuadraticPhase α β j‖ ^ 2 ≤
      64 * ((N : ℝ) / r + 1) * ((N : ℝ) + r * (1 + Real.log r)) := by
…