Prove2Me

Local factors are close to 11 at large primes

Proved
CircleMethod.norm_localFactor_sub_one_le

by tabbott · Sep 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodnumber-theorysingular-serieswaring

A quantitative form of "almost all local factors are harmless". Suppose the local densities obey the uniform decay bound ∣A(q,n)∣≤Cq−(1+δ)|A(q,n)|\le C q^{-(1+\delta)} for all q≥1q\ge1 and all nn, with C,δ>0C,\delta>0, and that ∑q∣A(q,n)∣\sum_q|A(q,n)| converges. Then for every prime p≥2p\ge2,

∣σp(n)−1∣ ≤ 2C p−(1+δ).\bigl|\sigma_p(n)-1\bigr|\ \le\ 2C\,p^{-(1+\delta)} .

The point is the exponent 1+δ>11+\delta>1: summing over pp gives a convergent series, so all but finitely many local factors lie within a fixed small distance of 11 and the Euler product cannot vanish through its tail. Only the finitely many small primes need separate treatment.

Preamble
/-
# Positivity of the singular series in Waring's problem

`singSeries k s n = ∑' q, locDens k s q n` is the singular series `𝔖(n)`.  This file
establishes its Euler product `𝔖(n) = ∏_p σ_p(n)`, `σ_p(n) = ∑_j A(p^j, n)`, bounds the
tail of the product, and assembles a uniform lower bound `𝔖(n) ≥ c(k,s) > 0` from the
local-solubility statement `LocalSolubility k s` (Vaughan, Lemmas 2.13–2.15).
-/
import Definitions.Def_CircleMethod_singpos
import Theorems.Thm_CircleMethod_locDens_mul
import Theorems.Thm_CircleMethod_locDens_one
import Theorems.Thm_CircleMethod_locDens_zero_modulus
import Theorems.Thm_CircleMethod_locDens_bound
import Theorems.Thm_CircleMethod_locDens_exponent_lt_neg_one
import Theorems.Thm_CircleMethod_sing_series_summable_norm
import Theorems.Thm_CircleMethod_e_zero
import Theorems.Thm_CircleMethod_e_add
import Theorems.Thm_CircleMethod_sum_e_div_orthogonality
import Theorems.Thm_Vino_e_div_congr
import Mathlib.NumberTheory.EulerProduct.Basic
import Mathlib.NumberTheory.SumPrimeReciprocals
import Mathlib.NumberTheory.Padics.Hensel
import Mathlib.NumberTheory.Padics.RingHoms
import Mathlib.Combinatorics.Additive.CauchyDavenport

open Finset Filter Topology

open Finset Filter Topology
Formal statement
namespace CircleMethod

theorem norm_localFactor_sub_one_le {k s : ℕ} {C δ : ℝ} (hC : 0 < C) (hδ : 0 < δ)
    (hbd : ∀ (q : ℕ) (n : ℤ), 0 < q → ‖locDens k s q n‖ ≤ C * (q : ℝ) ^ (-(1 + δ)))
    (hsum : ∀ n : ℤ, Summable (fun q : ℕ => ‖locDens k s q n‖))
    {p : ℕ} (hp : 2 ≤ p) (n : ℤ) :
    ‖localFactor k s p n - 1‖ ≤ 2 * C * (p : ℝ) ^ (-(1 + δ)) := by sorry

end CircleMethod
Source
R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Section 2.6, proof of Theorem 2.4 (eq. 2.33)

View graph