Chen 1973, Lemma 3: source-order fourth-moment reductions #
This file follows pp. 114--115 of Chen's original paper sentence by sentence. It defines the literal half-plane, primitive-character fourth moment, truncating Dirichlet polynomial, its collected two-factor coefficients, and the exact fourfold expansion used in Chen's invocation of Lemma 2.
The source's final analytic estimate is not packaged as a Prop. The first
unproved printed step is recorded at the end of this file after the proved
finite identities and the actual Lemma 2 call.
L(s,χ) on the nonprincipal primitive range q > 1. The source's
starred family excludes the exceptional principal character at modulus 1; we
therefore set that term to zero explicitly (and also totalize modulus 0).
Equations
- AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLValue q s χ = if hq : 1 < q then DirichletCharacter.LFunction (↑χ) s else 0
Instances For
Chen's literal sum ∑_{q≤Q} ∑*_{χ_q} |L(s,χ_q)|⁴.
Equations
Instances For
The strict floor endpoint needed in the truncation-error scalar ledger; unlike
1 ≤ Q‖s‖, this is valid without a small-height assumption.
The companion non-strict floor inequality.
The finite Dirichlet polynomial ∑_{n=1}^N χ(n)/n^s.
Equations
- AnalyticNumberTheory.LargeSieve.chen1973DirichletPolynomial N s χ = ∑ n ∈ Finset.Icc 1 N, ↑n ^ (-s) * ↑χ ↑n
Instances For
A single coefficient after squaring and collecting equal products.
Equations
- AnalyticNumberTheory.LargeSieve.chen1973PairCoefficient N s m = ∑ ab ∈ (Finset.Icc 1 N).product (Finset.Icc 1 N), if ↑ab.1 * ↑ab.2 = m then ↑ab.1 ^ (-s) * ↑ab.2 ^ (-s) else 0
Instances For
The first finite algebraic step in the fourfold expansion: squaring the Dirichlet polynomial and collecting the two numerator variables.
Every product of two integers in [1,N] lies in [1,N²].
Collecting equal products is an exact finite reindexing.
Chen's finite fourfold expansion, in the collected form to which Lemma 2 is applied: the fourth power of the original norm is the square norm of the pair-coefficient character polynomial.
The printed truncation sentence #
A primitive character of modulus q>1 is not principal.
On the source range q>1, the finite polynomial is the natural partial
sum used by the already formalized conditional Dirichlet series. The extra
index 0 vanishes.
The exact, already closed Abel-truncation inequality in the order used on
p. 115. This proves the finite truncation mechanism and its |s|/σ decay,
but has the elementary prefix constant q, not yet Chen's sharper
q^(1/2) log q constant.
Chen p. 115, first printed estimate before suppressing constants: combine
primitive Pólya--Vinogradov with the general-s Abel tail. The same numerical
prefix constant works for every primitive χ, every N, and every s in the
right half-plane.
The literal Vinogradov form of the preceding estimate. The constant 40
is absolute and uniform; σ ≥ 1/2 absorbs both the Abel endpoint and the
factor 1/σ, while q>1 absorbs 1 + log q into log q.
Pair-coefficient energy #
The bounded factorization fibre collected by chen1973PairCoefficient.
Equations
- AnalyticNumberTheory.LargeSieve.chen1973PairFiber N m = {ab ∈ (Finset.Icc 1 N).product (Finset.Icc 1 N) | ↑ab.1 * ↑ab.2 = m}
Instances For
Chen's collected coefficients have divisor-square energy bounded by four
harmonic factors. This is the ∑ d(n)²/n step on p. 115.
The fourfold expansion followed by the literal Lemma 2 call #
The literal call to Chen's source equation (2). Since the current source
module states (2) for real coefficient sequences, we apply it to real and
imaginary parts; the elementary complex split costs the absolute factor 2.
No modern large-sieve constant is substituted.
The actual large-sieve inequality obtained by applying Chen's Lemma 2 to the collected coefficient sequence from the fourfold expansion. No asymptotic or divisor-square energy estimate is assumed here.
Modulus one and the final finite fourth-moment assembly #
The value at modulus one is zero under the source convention used here.
The matching source-family convention for the truncating polynomial.
Equations
Instances For
Removing the harmless weight q / φ(q) from the polynomial fourth moment.
This is the exact finite-polynomial contribution in Chen's final display.
The PV--Abel errors aggregated over the complete finite starred family. The modulus-one lane vanishes by the explicit source convention.
The exact final finite assembly before Chen's last scalar simplification. It keeps the truncation-error fourth powers explicit, so no endpoint or family cardinality convention is hidden.
Corrected unrestricted-height endpoint and bounded-height specialization #
The source calculation naturally yields log (Q * (1 + ‖s‖)) ^ 4. The
log Q ^ 4 form below is therefore stated only under the explicit additional
hypothesis ‖s‖ ≤ Q ^ A. Both endpoints retain the preceding finite assembly.
The corrected unrestricted-height form of Chen's Lemma 3. Unlike the
printed final line, the fourth logarithm retains the conductor-height scale
forced by the cutoff ⌊Q‖s‖⌋₊.
Chen's printed log Q fourth power is valid after adding the explicit
bounded-height hypothesis ‖s‖ ≤ Q^A; it is not an unconditional source claim.
The corrected unrestricted-height endpoint with Chen's Lemma 2 discharged by the now-proved exact Farey formula (4).
Source-strength audit of the last displayed line #
The scan defines ∑* only as a primitive-character sum; it does not explicitly
say that modulus 1 is omitted. Nevertheless the proof uses the nonprincipal
Dirichlet series and the factor log q, so its displayed argument necessarily
uses the classical convention that this starred family starts at q = 2.
Mathlib's PrimitiveCharacter 1 is nonempty and its LFunction is zeta, which
has a pole at s = 1; including it would make the stated uniform half-plane
lemma false. The explicit zero above therefore records a mathematically forced
source convention rather than changing Mathlib's primitive-character type.
There is a second, independent issue in the last scalar step. The proved energy
is liuHarmonic (⌊Q‖s‖⌋²)^4, naturally of size
log(Q‖s‖)^4. The printed lemma has no restriction on t or ‖s‖, but replaces
this by log Q^4. That replacement is not uniform for unrestricted height and
does not follow from the displayed argument. Accordingly the theorem above is
the complete source-faithful finite assembly; no false Q²‖s‖²(log Q)^4
wrapper is introduced.