The power saving for A_1(D) from the mean square over sixth-power rows
DisprovedQRH.prime_extractionAssume the coefficient sequence is bounded by one on the elements prime to S, and the mean-square estimate: there is k with msSum over the rows of norm at most D^(1+theta) bounded by k D^(2+theta+eps) for all D >= 2. Then there is k with |A_1(D)| <= k D^(11/12 + 5 theta / 12 + eps) for all D >= 2. The extraction averages the mean square over the rows u = p^6: the sixth-power identity chi_n(p^6) = 1 when p does not divide n makes A_{p^6}(D) equal A_1(D) up to the terms divisible by p, which the divisor-count bound controls; Landau's prime ideal theorem supplies on the order of Y / log Y rows with Y = D^((1+theta)/6), and their sixth powers are distinct.
import Mathlib import Definitions.Def_QRH_arith import Definitions.Def_QRH_sums import Definitions.Def_QRH_lfun
universe u
namespace QRH
/-- The prime-extraction step of section 3 of the source: the power
saving for the smoothed Möbius sums A₁(D) follows from the mean-square
estimate for the family. For the rows u = p⁶ with p a primary prime of
norm in (Y/2, Y], the identity χ_n(p⁶) = 1_{p ∤ n} makes A_{p⁶}(D) equal
A₁(D) up to the terms divisible by p, which the divisor-count bound of
the interface controls by D / N p; Landau's prime ideal theorem supplies
≍ Y / log Y such primes, and their sixth powers are distinct rows of
norm at most D^(1+θ) with Y = D^((1+θ)/6). Averaging the mean square
over these rows bounds |A₁(D)|² by D^(11/6+5θ/6+ε), that is, |A₁(D)| by
D^(11/12+5θ/12+ε). -/
theorem prime_extraction (W : QRHWorld.{u}) (S : QRHSums W)
(c : W.E → ℂ) (Wt : ℝ → ℂ)
(hcb : ∀ n : W.E, W.Sgood n → ‖c n‖ ≤ 1)
(θ ε : ℝ) (hθ : 0 < θ) (hθ₁ : θ ≤ 1 / 10) (hε : 0 < ε)
(hms : ∃ k : ℝ, ∀ D : ℝ, 2 ≤ D →
msSum W S c Wt (D ^ (1 + θ)) D (2 * D) ≤ k * D ^ (2 + θ + ε)) :
∃ k : ℝ, ∀ D : ℝ, 2 ≤ D →
‖A1sum W S c Wt D (2 * D)‖
≤ k * D ^ (11 / 12 + 5 * θ / 12 + ε) := by
sorry
end QRH
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Read-back (self-check authored by the same model that produced the statement): the formal theorem takes the bound hcb (the coefficient c has norm at most 1 on elements prime to S), 0 < theta <= 1/10, eps > 0, and the mean-square hypothesis hms, and produces a constant k with norm(A1sum W S c Wt D (2 * D)) <= k * D ^ (11/12 + 5 * theta / 12 + eps) for all D >= 2. The proof shape: the rows p^6 for p in primeRange Y with Y = D^((1 + theta)/6) lie in the row range by pow6_inj and the norm axiom N_wpow; the difference A_1(D) - A_{p^6}(D) is controlled by count_divisor and hcb; Landau's theorem landau lower-bounds the number of rows; averaging the mean square hms over these rows gives the exponent 11/12 + 5 theta / 12 + eps.