The exponent inequality behind the minor-arc bound

Proved

CircleMethod.weyl_hua_exponent_lt

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorycircle-methodnumber-theorywaring-problem

The arithmetic that makes the minor arcs negligible. Interpolating the pointwise Weyl saving $N^{1-\delta 2^{1-k}+\varepsilon}$ against Hua's inequality $N^{2^{k}-k+\varepsilon}$ gives a minor-arc contribution of order $N^{E}$ with

E=\left(1-\delta 2^{1-k}+\varepsilon\right)\left(s-2^{k}\right)+\left(2^{k}-k+\varepsilon\right),

while the main term has order $N^{\,s-k}$ . This lemma is the statement that $E<s-k$ , so the minor arcs really are of smaller order.

The difference is exactly

E-(s-k)=\varepsilon\left(s-2^{k}+1\right)-\delta 2^{1-k}\left(s-2^{k}\right),

so the inequality is strict precisely when $\varepsilon<\dfrac{\delta 2^{1-k}(s-2^{k})}{s-2^{k}+1}$ . Two things are visible in that formula. First, some $\varepsilon$ always works, for every $\delta>0$ — no smallness of the Farey parameter is needed here. Second, the requirement $s>2^{k}$ is not an artefact: at $s=2^{k}$ the saving term vanishes and no positive $\varepsilon$ can be chosen. That is the precise sense in which the Hardy--Littlewood method needs more than $2^{k}$ variables.

Preamble

import Definitions.Def_CircleMethod_char
import Mathlib.Analysis.SpecialFunctions.Pow.Real

Formal statement

namespace CircleMethod

theorem weyl_hua_exponent_lt (k s : ℕ) {δ ε : ℝ}
    (hε : ε * ((s : ℝ) - (2 : ℝ) ^ k + 1) < δ * (2 : ℝ) ^ (1 - (k : ℝ)) * ((s : ℝ) - (2 : ℝ) ^ k)) :
    (1 - δ * (2 : ℝ) ^ (1 - (k : ℝ)) + ε) * ((s : ℝ) - (2 : ℝ) ^ k)
        + ((2 : ℝ) ^ k - (k : ℝ) + ε) < (s : ℝ) - (k : ℝ) := by sorry

end CircleMethod

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 2 and Chapter 4 (the minor-arc treatment, where the pointwise Weyl bound and Hua's mean value estimate are interpolated).

View graph