Prove2Me

Major-arc decomposition: principal-character main term μ(q)ψ(⋅,q)=1(N)\mu(q)\psi_{(\cdot,q)=1}(N)

Proved
Vino.vmSum_rat_principal_extraction

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

circle-methoddirichlet-charactersgoldbachmajor-arcsnumber-theory

At a reduced fraction b/qb/q, the von Mangoldt exponential sum splits as

φ(q) S(b/q,N)=μ(q) ⁣∑n<N(n,q)=1Λ(n)  +  ∑χ≠χ0χˉ(b) τ(χ) ψ(N,χˉ)  +  φ(q) ⁣∑n<N(n,q)>1Λ(n)e(bn/q).\varphi(q)\,S(b/q,N)=\mu(q)\!\sum_{\substack{n<N\\(n,q)=1}}\Lambda(n)\;+\;\sum_{\chi\ne\chi_0}\bar\chi(b)\,\tau(\chi)\,\psi(N,\bar\chi)\;+\;\varphi(q)\!\sum_{\substack{n<N\\(n,q)>1}}\Lambda(n)e(bn/q).

The first term is the main term of the major-arc analysis: ψ(N,χ0)=∑(n,q)=1Λ(n)≈N\psi(N,\chi_0)=\sum_{(n,q)=1}\Lambda(n)\approx N, and τ(χ0)=μ(q)\tau(\chi_0)=\mu(q). The middle sum over non-principal characters is exactly where the prime-number-theorem-in-progressions (Siegel–Walfisz type) input is required. The last term is the coprime defect, which is small (≪ω(q)log⁡qlog⁡N\ll\omega(q)\log q\log N) by the published bound norm_vmSum_noncoprime_le.

Preamble
import Mathlib
import Definitions.Def_Vino_dirichlet
import Definitions.Def_Vino_primes
import Theorems.Thm_Vino_vmSum_rat_char_expansion
import Theorems.Thm_Vino_ramanujan_eq_kluyver
import Mathlib.NumberTheory.DirichletCharacter.Basic
import Mathlib.NumberTheory.DirichletCharacter.Orthogonality
open Finset
Formal statement
namespace Vino

theorem vmSum_rat_principal_extraction (q : ℕ) [NeZero q] {b : ℕ}
    (hb : IsUnit ((b : ℕ) : ZMod q)) (N : ℕ) :
    (Nat.totient q : ℂ) * vmSum ((b : ℝ) / (q : ℝ)) N
      = ((ArithmeticFunction.moebius q : ℤ) : ℂ)
          * ∑ n ∈ Finset.range N, (if Nat.Coprime n q then 1 else 0 : ℂ)
              * ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ)
        + ∑ χ ∈ Finset.univ.filter (· ≠ (1 : DirichletCharacter ℂ q)),
            χ⁻¹ ((b : ℕ) : ZMod q) * gaussE q χ * vmSumChar q χ⁻¹ N
        + (Nat.totient q : ℂ)
            * ∑ n ∈ (Finset.range N).filter (fun n => ¬ Nat.Coprime n q),
                ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ)
                  * CircleMethod.e ((b : ℝ) / (q : ℝ) * (n : ℝ)) := by
  sorry

end Vino
Source
extraction of the χ0\chi_0 term of `vmSum_rat_char_expansion`; Davenport Ch. 26

View graph