Transport of a von Mangoldt partial-sum approximation to a neighboring frequency

Proved

Vino.vmSum_arc_error_bound

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

analytic-number-theorycircle-methodexponential-sumsgoldbach

Write $S(\alpha,K)=\sum_{n<K}\Lambda(n)e(\alpha n)$ and $D_N(\beta)=\sum_{n<N}e(\beta n)$ , with $e(t)=\exp(2\pi i t)$ . Let $\alpha,\beta\in\mathbb R$ , $c\in\mathbb C$ , $N\ge0$ an integer, and $E\ge0$ . If

|S(\alpha,K)-cK|\le E\qquad(0\le K\le N),

then

|S(\alpha+\beta,N)-cD_N(\beta)|\le(1+2\pi N|\beta|)E.

In particular, taking $\alpha=a/q$ and $c=\mu(q)/\varphi(q)$ converts a rational-point approximation valid at every initial length into a major-arc approximation. The theorem does not assume that such an error bound is small, and it also applies to arbitrary real base frequencies and complex coefficients $c$ .

Preamble

import Mathlib
import Definitions.Def_CircleMethod_char
import Definitions.Def_Vino_primes

Formal statement

theorem Vino.vmSum_arc_error_bound (α β : ℝ) (c : ℂ) (N : ℕ) (E : ℝ)
    (hE : 0 ≤ E)
    (hpartial : ∀ K : ℕ, K ≤ N → ‖Vino.vmSum α K - c * (K : ℂ)‖ ≤ E) :
    ‖Vino.vmSum (α + β) N
        - c * ∑ n ∈ Finset.range N, CircleMethod.e (β * (n : ℝ))‖
      ≤ (1 + 2 * Real.pi * (N : ℝ) * |β|) * E := by sorry

Source

Finite Abel-summation corollary proved in the submitted solution, using Mathlib Finset.sum_range_by_parts and the elementary variation bound for exp(2*pi*i*t). Circle-method context: R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Chapter 3, Section 3.1. The explicit interface is an original formalization, not an assertion of an effective prime-number-theorem error estimate.

View graph