Chen 1973, Lemma 6: source spine for the M₂ bound

This file follows printed pp. 119--123, equations (12)--(21). It freezes the actual M₂ from Chen1973Lemma5SwitchedTripleSource, the literal prime-pair and conductor dyadic carriers, and the finite reindexing behind (13).

The analytic estimates are deliberately not hidden in a conclusion-shaped record. The terminal theorem takes separately named hypotheses with the exact roles of displayed equations (12), (19), (20), and (21), plus the final logarithmic absorption. All finite carrier identities are proved here.

The source's finite Dirichlet polynomial is represented by Finset.Icc 1 H (in natural order). This matters on the β = 1/2 + 1/log x line: no conditionally convergent infinite reordering is introduced.

Source ledger (verified directly on printed pp. 119--123):

• (12) is M₂ ≪ (log x)^6 max_{1<m≤x^(1/2)} N_m.
• (13) uses 0≤l≤I₁, 0≤k≤I₂, low conductors 1<d≤(log x)^100, high cells 2^(l-1)(log x)^100<d≤2^l(log x)^100, and pair cells x^(13/30)2^k<p₁p₂≤x^(13/30)2^(k+1).
• (14) is the second moment for 1-LS; (15) is the fourth moment of the natural-order polynomial S(H,β+iv,χ); (16) is the algebraic L'/L split; (17) has the printed second prefactor x^(1/2).
• (18) bounds 3^ν(d) on squarefree conductors. Equations (19) and (20) give N_m^(l,k) ≪ x/(log x)^20; in the second case the printed choice is H=max(2^(2l-k)x^(-13/30)(log x)^400 I_{l,x}, x^(1/2-ε)).
• (21) treats the low-conductor l=0 cells using the primitive-character zero-free line. Finally (12), (13), and (19)--(21) yield the printed M₂ ≪ x/(log x)^2.01.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6MobiusPartialSum {d : ℕ} (H : ℕ) (s : ℂ) (χ : PrimitiveCharacter d) : ℂ

The p. 120 polynomial S(H,s,χ)=∑_{n=1}^H μ(n)χ(n)n⁻ˢ, with the natural-number order made literal.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6MobiusPartialSum H s χ = ∑ n ∈ Finset.Icc 1 H, ↑(ArithmeticFunction.moebius n) * ↑χ ↑n / ↑n ^ s

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_mobiusPartialSum_sq {d H : ℕ} (s : ℂ) (χ : PrimitiveCharacter d) : chen1973Lemma6MobiusPartialSum H s χ ^ 2 = ∑ a ∈ Finset.Icc 1 H, ∑ b ∈ Finset.Icc 1 H, ↑(ArithmeticFunction.moebius a) * ↑χ ↑a / ↑a ^ s * (↑(ArithmeticFunction.moebius b) * ↑χ ↑b / ↑b ^ s)

The exact finite square before collecting equal products into the source's coefficient j(n). Both indices are natural-order finite partial sums, so this identity is valid equally on the Re(s)≤1 line used in (15).

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6DyadicShell {α : Type u_1} [DecidableEq α] (S : Finset α) (size : α → ℕ) (B k : ℕ) : Finset α

A dyadic shell with the source convention B·2^k < size ≤ B·2^(k+1).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6DyadicShell S size B k = {a ∈ S | B * 2 ^ k < size a ∧ size a ≤ B * 2 ^ (k + 1)}

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6DyadicHull {α : Type u_1} [DecidableEq α] (S : Finset α) (size : α → ℕ) (B K : ℕ) : Finset α

The complete dyadic hull covered by levels 0,…,K.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6DyadicHull S size B K = {a ∈ S | B < size a ∧ size a ≤ B * 2 ^ (K + 1)}

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_biUnion_dyadicShell_eq_hull {α : Type u_1} [DecidableEq α] (S : Finset α) (size : α → ℕ) {B K : ℕ} (hB : 0 < B) : (Finset.range (K + 1)).biUnion (chen1973Lemma6DyadicShell S size B) = chen1973Lemma6DyadicHull S size B K

Exact finite union of the printed dyadic shells.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_dyadicShell_pairwiseDisjoint {α : Type u_1} [DecidableEq α] (S : Finset α) (size : α → ℕ) {B K : ℕ} (hB : 0 < B) : (↑(Finset.range (K + 1))).PairwiseDisjoint (chen1973Lemma6DyadicShell S size B)

The printed shells are pairwise disjoint; hence finite sums may be reindexed without multiplicity.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_sum_dyadicShell {α : Type u_1} [DecidableEq α] (S : Finset α) (size : α → ℕ) {B K : ℕ} (hB : 0 < B) (f : α → ℝ) : ∑ a ∈ chen1973Lemma6DyadicHull S size B K, f a = ∑ k ∈ Finset.range (K + 1), ∑ a ∈ chen1973Lemma6DyadicShell S size B k, f a

Exact sum reindexing over the source dyadic hull.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell (x B k m : ℕ) : Finset (ℕ × ℕ)

The literal p. 119 prime-pair shell x^(13/30)2^k < p₁p₂ ≤ x^(13/30)2^(k+1), represented by an honest natural base cutoff B; the real-power correspondence is stated separately below.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m = AnalyticNumberTheory.LargeSieve.chen1973Lemma6DyadicShell ({pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x | (pp.1 * pp.2).Coprime m}) (fun (pp : ℕ × ℕ) => pp.1 * pp.2) B k

def AnalyticNumberTheory.LargeSieve.Chen1973ThirteenThirtiethCutoff (x B : ℕ) : Prop

Honest cutoff bridge for the printed x^(13/30) boundary.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973ThirteenThirtiethCutoff x B = ∀ (n : ℕ), B < n ↔ ↑x ^ (13 / 30) < ↑n

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock (x L level : ℕ) : Finset ℕ

The conductor blocks in (13): level zero is 1<d≤L; level l+1 is 2^l L<d≤2^(l+1)L.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level = if level = 0 then {d ∈ Finset.Ioc 1 L | d.Coprime x ∧ Squarefree d} else {d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6DyadicShell (Finset.Ioc 1 (L * 2 ^ level)) id L (level - 1) | d.Coprime x ∧ Squarefree d}

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlock (x L level B k m : ℕ) (Phi : (d : ℕ) → PrimitiveCharacter d → ℝ → ℂ) : ℝ

The exact p. 119 summand of N_m, with Chen's Möbius/3^ν weight, primitive-character sum, reciprocal logarithm, and actual semiprime carrier. Phi d χ y is the displayed contour kernel Φ(y,χ) defined at the start of Lemma 6; it is not an arbitrary coefficient sequence on integers.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlock x L level B k m Phi = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, |↑(ArithmeticFunction.moebius d)| * 3 ^ d.primeFactors.card / ↑d * ‖∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, star (↑χ ↑x) * ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * Phi d χ (↑x / (↑pp.1 * ↑pp.2)) * ↑χ ↑(pp.1 * pp.2)‖

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6DyadicMajorant (x L I1 B I2 m : ℕ) (Phi : (d : ℕ) → PrimitiveCharacter d → ℝ → ℂ) : ℝ

The complete right side of source equation (13).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6DyadicMajorant x L I1 B I2 m Phi = ∑ level ∈ Finset.range (I1 + 1), ∑ k ∈ Finset.range (I2 + 1), AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlock x L level B k m Phi

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19Cell (_x L B D level k : ℕ) : Prop

1≤l≤I₁ cells in the first two ranges treated by source equation (19).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19Cell _x L B D level k = (1 ≤ level ∧ (D < B * 2 ^ k ∨ B * 2 ^ k ≤ D ∧ L * 2 ^ level < B * 2 ^ k))

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20Cell (_x L B D level k : ℕ) : Prop

1≤l≤I₁ cells in the complementary range treated by source equation (20).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20Cell _x L B D level k = (1 ≤ level ∧ B * 2 ^ k ≤ L * 2 ^ level ∧ L * 2 ^ level ≤ 2 * D)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_or_eq20 {x L B D level k : ℕ} (hlevel : 1 ≤ level) (hLast : L * 2 ^ level ≤ 2 * D) : chen1973Lemma6Eq19Cell x L B D level k ∨ chen1973Lemma6Eq20Cell x L B D level k

Every positive-level cell is assigned to (19) or (20), under the printed last-shell relation D < 2^I₁L ≤ 2D.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6M2_le_twoPointZeroOne (x D L I1 B I2 m : ℕ) (Phi : (d : ℕ) → PrimitiveCharacter d → ℝ → ℂ) (h12 : chen1973Lemma5M2 x D ≤ Real.log ↑x ^ 6 * chen1973Lemma6DyadicMajorant x L I1 B I2 m Phi) (h19 : ∀ level ∈ Finset.Icc 1 I1, ∀ k ∈ Finset.range (I2 + 1), chen1973Lemma6Eq19Cell x L B D level k → chen1973Lemma6NmBlock x L level B k m Phi ≤ ↑x / Real.log ↑x ^ 20) (h20 : ∀ level ∈ Finset.Icc 1 I1, ∀ k ∈ Finset.range (I2 + 1), chen1973Lemma6Eq20Cell x L B D level k → chen1973Lemma6NmBlock x L level B k m Phi ≤ ↑x / Real.log ↑x ^ 20) (h21 : ∀ k ∈ Finset.range (I2 + 1), chen1973Lemma6NmBlock x L 0 B k m Phi ≤ ↑x / Real.log ↑x ^ 20) (hLast : ∀ level ∈ Finset.Icc 1 I1, L * 2 ^ level ≤ 2 * D) (hAbsorb : Real.log ↑x ^ 6 * (↑(I1 + 1) * ↑(I2 + 1) * (↑x / Real.log ↑x ^ 20)) ≤ ↑x / Real.log ↑x ^ 2.01) : chen1973Lemma5M2 x D ≤ ↑x / Real.log ↑x ^ 2.01

Transparent source chain (12), (13), (19)--(21) to Lemma 6's terminal 2.01 bound. Each analytic input is a concrete inequality about the displayed quantity; there is no Prop wrapper carrying the conclusion.