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.

def AnalyticNumberTheory.LargeSieve.Chen1973Lemma3Domain (s : ℂ) (σ t : ℝ) : Prop

The literal domain sentence s = σ + it, σ ≥ 1/2 on p. 114.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Lemma3Domain s σ t = (s = ↑σ + ↑t * Complex.I ∧ 1 / 2 ≤ σ)

theorem AnalyticNumberTheory.LargeSieve.Chen1973Lemma3Domain.re_eq {s : ℂ} {σ t : ℝ} (hs : Chen1973Lemma3Domain s σ t) : s.re = σ

theorem AnalyticNumberTheory.LargeSieve.Chen1973Lemma3Domain.re_pos {s : ℂ} {σ t : ℝ} (hs : Chen1973Lemma3Domain s σ t) : 0 < s.re

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLValue (q : ℕ) (s : ℂ) (χ : PrimitiveCharacter q) : ℂ

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

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma3FourthMoment (Q : ℕ) (s : ℂ) : ℝ

Chen's literal sum ∑_{q≤Q} ∑*_{χ_q} |L(s,χ_q)|⁴.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma3FourthMoment Q s = ∑ q ∈ Finset.Icc 1 Q, ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLValue q s χ‖ ^ 4

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma3Cutoff (Q : ℕ) (s : ℂ) : ℕ

The integer [Q |s|] selected in the proof on p. 115.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma3Cutoff Q s = ⌊↑Q * ‖s‖⌋₊

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3Cutoff_lt_succ (Q : ℕ) (s : ℂ) : ↑Q * ‖s‖ < ↑(chen1973Lemma3Cutoff Q s) + 1

The strict floor endpoint needed in the truncation-error scalar ledger; unlike 1 ≤ Q‖s‖, this is valid without a small-height assumption.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3Cutoff_le (Q : ℕ) (s : ℂ) : ↑(chen1973Lemma3Cutoff Q s) ≤ ↑Q * ‖s‖

The companion non-strict floor inequality.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973DirichletPolynomial (N : ℕ) (s : ℂ) {q : ℕ} (χ : PrimitiveCharacter q) : ℂ

The finite Dirichlet polynomial ∑_{n=1}^N χ(n)/n^s.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973DirichletPolynomial N s χ = ∑ n ∈ Finset.Icc 1 N, ↑n ^ (-s) * ↑χ ↑n

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973PairCoefficient (N : ℕ) (s : ℂ) (m : ℤ) : ℂ

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

theorem AnalyticNumberTheory.LargeSieve.chen1973DirichletPolynomial_sq_eq_pair_sum (N : ℕ) (s : ℂ) {q : ℕ} (χ : PrimitiveCharacter q) : chen1973DirichletPolynomial N s χ ^ 2 = ∑ ab ∈ (Finset.Icc 1 N).product (Finset.Icc 1 N), ↑ab.1 ^ (-s) * ↑ab.2 ^ (-s) * ↑χ ↑(ab.1 * ab.2)

The first finite algebraic step in the fourfold expansion: squaring the Dirichlet polynomial and collecting the two numerator variables.

theorem AnalyticNumberTheory.LargeSieve.chen1973_pair_product_mem {N a b : ℕ} (ha : a ∈ Finset.Icc 1 N) (hb : b ∈ Finset.Icc 1 N) : ↑a * ↑b ∈ Finset.Icc 1 ↑(N * N)

Every product of two integers in [1,N] lies in [1,N²].

theorem AnalyticNumberTheory.LargeSieve.chen1973_pairCoefficient_character_sum_eq (N : ℕ) (s : ℂ) {q : ℕ} (χ : PrimitiveCharacter q) : ∑ m ∈ Finset.Icc 1 ↑(N * N), chen1973PairCoefficient N s m * ↑χ ↑m = ∑ ab ∈ (Finset.Icc 1 N).product (Finset.Icc 1 N), ↑ab.1 ^ (-s) * ↑ab.2 ^ (-s) * ↑χ ↑(ab.1 * ab.2)

Collecting equal products is an exact finite reindexing.

theorem AnalyticNumberTheory.LargeSieve.chen1973DirichletPolynomial_norm_four_eq_pair_norm_sq (N : ℕ) (s : ℂ) {q : ℕ} (χ : PrimitiveCharacter q) : ‖chen1973DirichletPolynomial N s χ‖ ^ 4 = ‖∑ m ∈ Finset.Icc 1 ↑(N * N), chen1973PairCoefficient N s m * ↑χ ↑m‖ ^ 2

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

theorem AnalyticNumberTheory.LargeSieve.chen1973_primitive_ne_one {q : ℕ} [NeZero q] (hq : 1 < q) (χ : PrimitiveCharacter q) : ↑χ ≠ 1

A primitive character of modulus q>1 is not principal.

theorem AnalyticNumberTheory.LargeSieve.chen1973DirichletPolynomial_eq_sum_range {q : ℕ} [NeZero q] (hq : 1 < q) (χ : PrimitiveCharacter q) (N : ℕ) (s : ℂ) : chen1973DirichletPolynomial N s χ = ∑ n ∈ Finset.range (N + 1), DirichletLAbelWeightVariation.cpowWeight s ↑n * ↑χ ↑n

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.

theorem AnalyticNumberTheory.LargeSieve.chen1973_LFunction_sub_polynomial_coarse {q : ℕ} [NeZero q] (hq : 1 < q) (χ : PrimitiveCharacter q) (N : ℕ) (s : ℂ) (hs : 0 < s.re) : ‖DirichletCharacter.LFunction (↑χ) s - chen1973DirichletPolynomial N s χ‖ ≤ ↑q * (↑(N + 1) ^ (-s.re) + ‖s‖ / s.re * ↑(N + 1) ^ (-s.re))

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.

theorem AnalyticNumberTheory.LargeSieve.chen1973_LFunction_sub_polynomial_polyaVinogradov {q : ℕ} [NeZero q] (hq : 1 < q) (χ : PrimitiveCharacter q) (N : ℕ) (s : ℂ) (hs : 0 < s.re) : ‖DirichletCharacter.LFunction (↑χ) s - chen1973DirichletPolynomial N s χ‖ ≤ 4 * √↑q * (1 + Real.log ↑q) * (↑(N + 1) ^ (-s.re) + ‖s‖ / s.re * ↑(N + 1) ^ (-s.re))

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.

theorem AnalyticNumberTheory.LargeSieve.chen1973_LFunction_sub_polynomial_le_forty {q : ℕ} [NeZero q] (hq : 1 < q) (χ : PrimitiveCharacter q) (N : ℕ) (s : ℂ) (hs : Chen1973Lemma3Domain s s.re s.im) : ‖DirichletCharacter.LFunction (↑χ) s - chen1973DirichletPolynomial N s χ‖ ≤ 40 * ‖s‖ * √↑q * Real.log ↑q * ↑(N + 1) ^ (-s.re)

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

def AnalyticNumberTheory.LargeSieve.chen1973PairFiber (N : ℕ) (m : ℤ) : Finset (ℕ × ℕ)

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}

theorem AnalyticNumberTheory.LargeSieve.chen1973PairFiber_card_le_divisors {N : ℕ} {m : ℤ} (hm : m ∈ Finset.Icc 1 ↑(N * N)) : (chen1973PairFiber N m).card ≤ m.toNat.divisors.card

theorem AnalyticNumberTheory.LargeSieve.chen1973_pairCoefficient_norm_le {N : ℕ} {s : ℂ} {m : ℤ} (hs : Chen1973Lemma3Domain s s.re s.im) (hm : m ∈ Finset.Icc 1 ↑(N * N)) : ‖chen1973PairCoefficient N s m‖ ≤ ↑m.toNat.divisors.card * ↑m.toNat ^ (-(1 / 2))

theorem AnalyticNumberTheory.LargeSieve.chen1973_pairCoefficient_energy_le_harmonic_four (N : ℕ) (s : ℂ) (hs : Chen1973Lemma3Domain s s.re s.im) : ∑ m ∈ Finset.Icc 1 ↑(N * N), ‖chen1973PairCoefficient N s m‖ ^ 2 ≤ MathlibNt.SieveTheory.LiuWeight.liuHarmonic (N * N) ^ 4

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

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma2_source_call_on_pairCoefficient (h2 : Chen1973Lemma2EquationTwo) (N Q : ℕ) (s : ℂ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖chen1973DirichletPolynomial N s χ‖ ^ 4 ≤ 2 * ((↑Q ^ 2 + Real.pi * ↑(N * N)) * ∑ m ∈ Finset.Icc 1 ↑(N * N), ‖chen1973PairCoefficient N s m‖ ^ 2)

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.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma2_call_on_pairCoefficient (N Q : ℕ) (s : ℂ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖chen1973DirichletPolynomial N s χ‖ ^ 4 ≤ primitiveLargeSieveConstant (N * N) Q * ∑ m ∈ Finset.Icc 1 ↑(N * N), ‖chen1973PairCoefficient N s m‖ ^ 2

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

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLValue_one (s : ℂ) (χ : PrimitiveCharacter 1) : chen1973PrimitiveLValue 1 s χ = 0

The value at modulus one is zero under the source convention used here.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973PrimitivePolynomialValue (q N : ℕ) (s : ℂ) (χ : PrimitiveCharacter q) : ℂ

The matching source-family convention for the truncating polynomial.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973PrimitivePolynomialValue q N s χ = if 1 < q then AnalyticNumberTheory.LargeSieve.chen1973DirichletPolynomial N s χ else 0

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chen1973PrimitivePolynomialValue_one (N : ℕ) (s : ℂ) (χ : PrimitiveCharacter 1) : chen1973PrimitivePolynomialValue 1 N s χ = 0

theorem AnalyticNumberTheory.LargeSieve.chen1973DirichletPolynomial_fourthMoment_le (h2 : Chen1973Lemma2EquationTwo) (N Q : ℕ) (s : ℂ) (hs : Chen1973Lemma3Domain s s.re s.im) : ∑ q ∈ Finset.Icc 1 Q, ∑ χ : PrimitiveCharacter q, ‖chen1973DirichletPolynomial N s χ‖ ^ 4 ≤ 2 * ((↑Q ^ 2 + Real.pi * ↑(N * N)) * MathlibNt.SieveTheory.LiuWeight.liuHarmonic (N * N) ^ 4)

Removing the harmless weight q / φ(q) from the polynomial fourth moment. This is the exact finite-polynomial contribution in Chen's final display.

theorem AnalyticNumberTheory.LargeSieve.chen1973_truncation_error_fourth_sum_le (N Q : ℕ) (s : ℂ) (hs : Chen1973Lemma3Domain s s.re s.im) : ∑ q ∈ Finset.Icc 1 Q, ∑ χ : PrimitiveCharacter q, ‖chen1973PrimitiveLValue q s χ - chen1973PrimitivePolynomialValue q N s χ‖ ^ 4 ≤ ∑ q ∈ Finset.Icc 1 Q, ↑(Fintype.card (PrimitiveCharacter q)) * (40 * ‖s‖ * √↑q * Real.log ↑q * ↑(N + 1) ^ (-s.re)) ^ 4

The PV--Abel errors aggregated over the complete finite starred family. The modulus-one lane vanishes by the explicit source convention.

theorem AnalyticNumberTheory.LargeSieve.norm_four_le_eight_add_norm_sub_four (z w : ℂ) : ‖z‖ ^ 4 ≤ 8 * (‖w‖ ^ 4 + ‖z - w‖ ^ 4)

A pointwise fourth-power split used to aggregate the truncation errors.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_fourthMoment_finite_assembly (h2 : Chen1973Lemma2EquationTwo) (N Q : ℕ) (s : ℂ) (hs : Chen1973Lemma3Domain s s.re s.im) : chen1973Lemma3FourthMoment Q s ≤ 16 * ((↑Q ^ 2 + Real.pi * ↑(N * N)) * MathlibNt.SieveTheory.LiuWeight.liuHarmonic (N * N) ^ 4) + 8 * ∑ q ∈ Finset.Icc 1 Q, ∑ χ : PrimitiveCharacter q, ‖chen1973PrimitiveLValue q s χ - chen1973PrimitivePolynomialValue q N s χ‖ ^ 4

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.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma3LogScale (Q : ℕ) (s : ℂ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma3LogScale Q s = Real.log (↑Q * (1 + ‖s‖))

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_norm_half {s : ℂ} (hs : Chen1973Lemma3Domain s s.re s.im) : 1 / 2 ≤ ‖s‖

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_logScale_pos {Q : ℕ} {s : ℂ} (hQ : 2 ≤ Q) : 0 < chen1973Lemma3LogScale Q s

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_cutoff_square_add_one_le {Q : ℕ} {s : ℂ} (hQ : 2 ≤ Q) : ↑(chen1973Lemma3Cutoff Q s * chen1973Lemma3Cutoff Q s + 1) ≤ (↑Q * (1 + ‖s‖)) ^ 2

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_harmonic_le_logScale {Q : ℕ} {s : ℂ} (hQ : 2 ≤ Q) : MathlibNt.SieveTheory.LiuWeight.liuHarmonic (chen1973Lemma3Cutoff Q s * chen1973Lemma3Cutoff Q s) ≤ 6 * chen1973Lemma3LogScale Q s

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_cutoff_decay_four {Q : ℕ} {s : ℂ} (hQ : 2 ≤ Q) (hs : Chen1973Lemma3Domain s s.re s.im) : (↑(chen1973Lemma3Cutoff Q s + 1) ^ (-s.re)) ^ 4 ≤ (↑Q * ‖s‖)⁻¹ ^ 2

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_truncation_pointwise_scalar {Q q : ℕ} {s : ℂ} (hQ : 2 ≤ Q) (hq0 : 1 ≤ q) (hq : q ≤ Q) (hs : Chen1973Lemma3Domain s s.re s.im) : (40 * ‖s‖ * √↑q * Real.log ↑q * ↑(chen1973Lemma3Cutoff Q s + 1) ^ (-s.re)) ^ 4 ≤ 2560000 * ‖s‖ ^ 2 * ↑q ^ 2 / ↑Q ^ 2 * chen1973Lemma3LogScale Q s ^ 4

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_truncation_error_sum_scalar {Q : ℕ} {s : ℂ} (hQ : 2 ≤ Q) (hs : Chen1973Lemma3Domain s s.re s.im) : ∑ q ∈ Finset.Icc 1 Q, ∑ χ : PrimitiveCharacter q, ‖chen1973PrimitiveLValue q s χ - chen1973PrimitivePolynomialValue q (chen1973Lemma3Cutoff Q s) s χ‖ ^ 4 ≤ 2560000 * ↑Q ^ 2 * ‖s‖ ^ 2 * chen1973Lemma3LogScale Q s ^ 4

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_corrected_endpoint (h2 : Chen1973Lemma2EquationTwo) {Q : ℕ} (s : ℂ) (hQ : 2 ≤ Q) (hs : Chen1973Lemma3Domain s s.re s.im) : chen1973Lemma3FourthMoment Q s ≤ 21000000 * ↑Q ^ 2 * ‖s‖ ^ 2 * Real.log (↑Q * (1 + ‖s‖)) ^ 4

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‖⌋₊.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_logScale_le_bounded_height {Q A : ℕ} {s : ℂ} (hQ : 2 ≤ Q) (hheight : ‖s‖ ≤ ↑Q ^ A) : chen1973Lemma3LogScale Q s ≤ ↑(A + 2) * Real.log ↑Q

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_bounded_height_specialization (h2 : Chen1973Lemma2EquationTwo) {Q A : ℕ} (s : ℂ) (hQ : 2 ≤ Q) (hs : Chen1973Lemma3Domain s s.re s.im) (hheight : ‖s‖ ≤ ↑Q ^ A) : chen1973Lemma3FourthMoment Q s ≤ 21000000 * ↑(A + 2) ^ 4 * ↑Q ^ 2 * ‖s‖ ^ 2 * Real.log ↑Q ^ 4

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.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_corrected_endpoint_unconditional {Q : ℕ} (s : ℂ) (hQ : 2 ≤ Q) (hs : Chen1973Lemma3Domain s s.re s.im) : chen1973Lemma3FourthMoment Q s ≤ 21000000 * ↑Q ^ 2 * ‖s‖ ^ 2 * Real.log (↑Q * (1 + ‖s‖)) ^ 4

The corrected unrestricted-height endpoint with Chen's Lemma 2 discharged by the now-proved exact Farey formula (4).

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma3_bounded_height_specialization_unconditional {Q A : ℕ} (s : ℂ) (hQ : 2 ≤ Q) (hs : Chen1973Lemma3Domain s s.re s.im) (hheight : ‖s‖ ≤ ↑Q ^ A) : chen1973Lemma3FourthMoment Q s ≤ 21000000 * ↑(A + 2) ^ 4 * ↑Q ^ 2 * ‖s‖ ^ 2 * Real.log ↑Q ^ 4

The bounded-height specialization with the exact source Lemma 2 input discharged unconditionally.

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.