Major-arc approximation with a character-resolved error and non-coprime correction

Proved

Vino.vmSum_major_arc_bound

by jjosh · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorycircle-methoddirichlet-charactersgoldbachmajor-arcs

Let $q\ge1$ , let $b$ be a nonnegative integer coprime to $q$ , and let $N\ge1$ be an integer. For every Dirichlet character $\chi$ modulo $q$ , suppose a nonnegative number $E_\chi$ satisfies

|\psi(K,\chi)-\mathbf1_{\chi=\chi_0}K|\le E_\chi\qquad(0\le K\le N),

where $\psi(K,\chi)=\sum_{n<K}\Lambda(n)\chi(n)$ and $\chi_0$ is the principal character. Define $S(\alpha,N)=\sum_{n<N}\Lambda(n)e(\alpha n)$ , $D_N(\beta)=\sum_{n<N}e(\beta n)$ , $\tau(\chi)=\sum_{r<q}\chi(r)e(r/q)$ , and let $\omega(q)$ count the distinct prime factors of $q$ . For every real $\beta$ ,

\left|S\!\left(\frac bq+\beta,N\right)-\frac{\mu(q)}{\varphi(q)}D_N(\beta)\right|\le(1+2\pi N|\beta|)\left(\frac1{\varphi(q)}\sum_{\chi\bmod q}|\tau(\chi)|E_{\chi^{-1}}+\omega(q)\log N\right).

The error profile remains explicit for each character, including the principal character. This is a finite transfer theorem, not a proof that the character errors are small. It includes modulus one and separates the contribution from integers not coprime to the modulus.

Preamble

import Mathlib
import Definitions.Def_CircleMethod_char
import Definitions.Def_Vino_primes
import Definitions.Def_Vino_dirichlet

Formal statement

theorem Vino.vmSum_major_arc_bound (q : ℕ) [NeZero q] {b : ℕ}
    (hb : IsUnit (b : ZMod q)) (N : ℕ) (hN : 1 ≤ N) (β : ℝ)
    (E : DirichletCharacter ℂ q → ℝ)
    (hE : ∀ χ, 0 ≤ E χ)
    (hchar : ∀ (χ : DirichletCharacter ℂ q) (K : ℕ), K ≤ N →
      ‖Vino.vmSumChar q χ K - (if χ = 1 then (K : ℂ) else 0)‖ ≤ E χ) :
    ‖Vino.vmSum ((b : ℝ) / (q : ℝ) + β) N
      - (((ArithmeticFunction.moebius q : ℤ) : ℂ) / (Nat.totient q : ℂ))
        * ∑ n ∈ Finset.range N, CircleMethod.e (β * (n : ℝ))‖
    ≤ (1 + 2 * Real.pi * (N : ℝ) * |β|) *
      ((∑ χ : DirichletCharacter ℂ q, ‖Vino.gaussE q χ‖ * E χ⁻¹)
        / (Nat.totient q : ℝ) + (q.primeFactors.card : ℝ) * Real.log N) := by sorry

Source

Derived from the Prove2Me theorems Vino.vmSum_rat_char_expansion (44acef9d-12cb-4292-938a-798ba0340dcb), Vino.gaussE_principal (b70ae2ad-f414-4529-b6f6-bebe54cfa72e), Vino.norm_vmSum_noncoprime_le (0b997c83-3848-4207-bde7-7ebd52064551), and finite Abel summation. Classical context: H. Davenport, Multiplicative Number Theory, 3rd ed., Chapter 26; R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Chapter 3, Section 3.1. The displayed character-resolved finite bound is proved in the submitted solution.

View graph