Chen 1973, Lemma 5: the actual switched triple source

This file freezes the opening of Lemma 5 on pp. 116--119 of Chen's original scan. It keeps the actual von Mangoldt coefficient, Chen's finite Perron kernel Φ(x/(p₁p₂n)), and the reciprocal logarithmic weight. In particular it does not replace the source by an arbitrary coefficient sequence.

The analytic estimates in Lemmas 5--6 are not asserted here. The first layer is the exact finite bookkeeping used before those estimates: the prime-triple carrier, the Selberg-square expansion, the principal/nonprincipal partition, and the resulting M₁-M₃+M₄ identity.

def AnalyticNumberTheory.LargeSieve.chen1973Lemma5Q (z4 : ℕ) : ℕ

A natural cutoff version of Chen's Q=∏_{2≤p<x^(1/4)}p. The relation to the real fourth root is carried separately, so the finite product never uses a fake real-indexed finset.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5Q z4 = ∏ p ∈ Finset.range z4 with 2 ≤ p ∧ Nat.Prime p, p

def AnalyticNumberTheory.LargeSieve.Chen1973FourthRootCutoff (x z4 : ℕ) : Prop

An honest natural cutoff realizes the source's strict real fourth-root cutoff when these membership predicates agree.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973FourthRootCutoff x z4 = ∀ (p : ℕ), Nat.Prime p → (p < z4 ↔ ↑p < ↑x ^ (1 / 4))

theorem AnalyticNumberTheory.LargeSieve.mem_chen1973Lemma5QCarrier_iff {x z4 p : ℕ} (hz : Chen1973FourthRootCutoff x z4) (hp : Nat.Prime p) : p ∈ {q ∈ Finset.range z4 | 2 ≤ q ∧ Nat.Prime q} ↔ 2 ≤ p ∧ ↑p < ↑x ^ (1 / 4)

Under the explicit cutoff bridge, membership in the finite Q carrier is exactly the source condition 2 ≤ p < x^(1/4).

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs (x : ℕ) : Finset (ℕ × ℕ)

The finite pair carrier printed at the start of Lemma 5: x^(1/10)<p₁≤x^(1/3)<p₂≤(x/p₁)^(1/2).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x = {pp ∈ (Finset.range (x + 1)).product (Finset.range (x + 1)) | Nat.Prime pp.1 ∧ Nat.Prime pp.2 ∧ ↑x ^ (1 / 10) < ↑pp.1 ∧ ↑pp.1 ≤ ↑x ^ (1 / 3) ∧ ↑x ^ (1 / 3) < ↑pp.2 ∧ ↑pp.2 ≤ (↑x / ↑pp.1) ^ (1 / 2)}

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimeTriples (x : ℕ) : Finset ((ℕ × ℕ) × ℕ)

The actual finite triple carrier counted by Ω, before the coprimality sieve is imposed.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimeTriples x = {t ∈ (AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x).product (Finset.range (x + 1)) | Nat.Prime t.2 ∧ t.2 ≤ x / (t.1.1 * t.1.2)}

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5OmegaCarrier (x z4 : ℕ) : Finset ((ℕ × ℕ) × ℕ)

Chen's Ω: prime triples in the printed carrier for which (x-p₁p₂p₃,Q)=1.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5OmegaCarrier x z4 = {t ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimeTriples x | (x - t.1.1 * t.1.2 * t.2).Coprime (AnalyticNumberTheory.LargeSieve.chen1973Lemma5Q z4)}

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5Omega (x z4 : ℕ) : ℕ

The integer counted by the source symbol Ω.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5Omega x z4 = (AnalyticNumberTheory.LargeSieve.chen1973Lemma5OmegaCarrier x z4).card

theorem AnalyticNumberTheory.LargeSieve.mem_chen1973Lemma5OmegaCarrier_iff {x z4 : ℕ} {t : (ℕ × ℕ) × ℕ} : t ∈ chen1973Lemma5OmegaCarrier x z4 ↔ t.1 ∈ chen1973Lemma5PrimePairs x ∧ t.2 < x + 1 ∧ Nat.Prime t.2 ∧ t.2 ≤ x / (t.1.1 * t.1.2) ∧ (x - t.1.1 * t.1.2 * t.2).Coprime (chen1973Lemma5Q z4)

Literal membership conditions for the finite Ω carrier.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergF (k : ℕ) : ℝ

Chen p. 115: f(k)=φ(k)∏_{p∣k}(p-2)/(p-1).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergF k = ↑k.totient * ∏ p ∈ k.primeFactors, (↑p - 2) / (↑p - 1)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergDenominator (x R : ℕ) : ℝ

The normalized finite denominator in Chen's literal Selberg coefficient.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergDenominator x R = ∑ k ∈ Finset.range (R + 1) with 1 ≤ k ∧ k.Coprime x, ↑(ArithmeticFunction.moebius k) ^ 2 / AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergF k

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergLambda (x R d : ℕ) : ℝ

The actual coefficient λ_d defined immediately before Lemma 5 (p. 115). R is the honest natural version of x^(1/4-ε/2).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergLambda x R d = if d = 1 then 1 else if R < d then 0 else (↑(ArithmeticFunction.moebius d) / (AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergF d * (↑d.totient)⁻¹) * ∑ k ∈ Finset.range (R / d + 1) with 1 ≤ k ∧ k.Coprime (x * d), ↑(ArithmeticFunction.moebius k) ^ 2 / AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergF k) * (AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergDenominator x R)⁻¹

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergLambda_one (x R : ℕ) : chen1973Lemma5SelbergLambda x R 1 = 1

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergLambda_eq_zero_of_cutoff {x R d : ℕ} (hR : 1 ≤ R) (hd : R < d) : chen1973Lemma5SelbergLambda x R d = 0

def AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier (x : ℕ) (pp : ℕ × ℕ) : Finset ℕ

The finite n≤x/(p₁p₂) carrier used after switching p₃ to Λ(n).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp = {n ∈ Finset.range (x + 1) | n ≤ x / (pp.1 * pp.2)}

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight (x : ℕ) (pp : ℕ × ℕ) (n : ℕ) : ℝ

The literal source weight Λ(n) Φ(x/(p₁p₂n)) / log(x/(p₁p₂)). The value at a zero denominator is totalized by Lean's field operations; on the prime-pair carrier the later analytic development proves the required positivity separately.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight x pp n = ArithmeticFunction.vonMangoldt n * AnalyticNumberTheory.LargeSieve.chen1973PerronKernelFinite (↑x) (↑x / (↑pp.1 * ↑pp.2 * ↑n)) / Real.log (↑x / (↑pp.1 * ↑pp.2))

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M (x z4 : ℕ) : ℝ

The unsmoothed switched main sum M printed on p. 116.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M x z4 = ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x, 1 / Real.log (↑x / (↑pp.1 * ↑pp.2)) * ∑ n ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp, if (x - pp.1 * pp.2 * n).Coprime (AnalyticNumberTheory.LargeSieve.chen1973Lemma5Q z4) then ArithmeticFunction.vonMangoldt n else 0

def AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorCarrier (x z4 : ℕ) : Finset ℕ

The divisor support in the Selberg square: d∣Q, (d,x)=1.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorCarrier x z4 = {d ∈ (AnalyticNumberTheory.LargeSieve.chen1973Lemma5Q z4).divisors | d.Coprime x}

def AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorSum (x z4 : ℕ) (lambda : ℕ → ℝ) (pp : ℕ × ℕ) (n : ℕ) : ℝ

The finite Selberg divisor sum appearing inside the square in (5).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorSum x z4 lambda pp n = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorCarrier x z4, if d ∣ x - pp.1 * pp.2 * n then lambda d else 0

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergSquare (x z4 : ℕ) (lambda : ℕ → ℝ) : ℝ

The exact smoothed Selberg square before expanding in d₁,d₂.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergSquare x z4 lambda = ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x, ∑ n ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp, AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight x pp n * AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorSum x z4 lambda pp n ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5OmegaSmoothed (x z4 : ℕ) : ℝ

The literal switched Λ·Φ/log mass on the Ω carrier. Keeping this quantity separate avoids silently replacing Chen's smoothed source by a bare cardinality.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5OmegaSmoothed x z4 = ∑ t ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5OmegaCarrier x z4, AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight x t.1 t.2

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight_nonneg {x : ℕ} (hx : 1 < x) {pp : ℕ × ℕ} {n : ℕ} (hlog : 0 ≤ Real.log (↑x / (↑pp.1 * ↑pp.2))) : 0 ≤ chen1973Lemma5SmoothedWeight x pp n

The source weight is nonnegative once its (printed) logarithmic denominator is known to be nonnegative. The nonnegativity of Λ and of Chen's finite Perron kernel are discharged internally.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5Q_ne_zero (z4 : ℕ) : chen1973Lemma5Q z4 ≠ 0

The finite product defining Q is nonzero.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorSum_eq_one_of_coprime {x z4 : ℕ} {lambda : ℕ → ℝ} (hlambda : lambda 1 = 1) {pp : ℕ × ℕ} {n : ℕ} (hcop : (x - pp.1 * pp.2 * n).Coprime (chen1973Lemma5Q z4)) : chen1973Lemma5DivisorSum x z4 lambda pp n = 1

On an Ω residue, every divisor of Q which divides the residue is one; therefore a Selberg divisor sum normalized by λ₁=1 is exactly one.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5OmegaSmoothed_eq_switched (x z4 : ℕ) : chen1973Lemma5OmegaSmoothed x z4 = ∑ pp ∈ chen1973Lemma5PrimePairs x, ∑ n ∈ chen1973Lemma5NCarrier x pp, if Nat.Prime n ∧ (x - pp.1 * pp.2 * n).Coprime (chen1973Lemma5Q z4) then chen1973Lemma5SmoothedWeight x pp n else 0

Exact reindexing of the smoothed Ω source into the switched pair/n coordinates used by the Selberg square.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5OmegaSmoothed_le_SelbergSquare {x z4 : ℕ} {lambda : ℕ → ℝ} (hlambda : lambda 1 = 1) (hw : ∀ pp ∈ chen1973Lemma5PrimePairs x, ∀ n ∈ chen1973Lemma5NCarrier x pp, 0 ≤ chen1973Lemma5SmoothedWeight x pp n) : chen1973Lemma5OmegaSmoothed x z4 ≤ chen1973Lemma5SelbergSquare x z4 lambda

The actual smoothed Ω mass is bounded by the actual Selberg square. The only hypotheses are λ₁=1 and nonnegativity of the source weights; the latter is supplied by chen1973Lemma5SmoothedWeight_nonneg from the genuine Λ·Φ/log definition.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5Omega_le_OmegaSmoothed {x z4 : ℕ} (hw1 : ∀ t ∈ chen1973Lemma5OmegaCarrier x z4, 1 ≤ chen1973Lemma5SmoothedWeight x t.1 t.2) : ↑(chen1973Lemma5Omega x z4) ≤ chen1973Lemma5OmegaSmoothed x z4

A separate, honest cardinal bridge. It applies when the retained smoothed weight is pointwise at least one; this condition is deliberately explicit and is not conflated with mere nonnegativity of the Perron weight.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5Omega_le_SelbergSquare {x z4 : ℕ} {lambda : ℕ → ℝ} (hlambda : lambda 1 = 1) (hw0 : ∀ pp ∈ chen1973Lemma5PrimePairs x, ∀ n ∈ chen1973Lemma5NCarrier x pp, 0 ≤ chen1973Lemma5SmoothedWeight x pp n) (hw1 : ∀ t ∈ chen1973Lemma5OmegaCarrier x z4, 1 ≤ chen1973Lemma5SmoothedWeight x t.1 t.2) : ↑(chen1973Lemma5Omega x z4) ≤ chen1973Lemma5SelbergSquare x z4 lambda

Cardinal form of the Ω--Selberg-square bridge, with the genuinely stronger pointwise lower bound isolated from the internally proved sign condition.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5ProgressionTerm (x d1 d2 : ℕ) : ℝ

The progression sum denoted N_[d₁,d₂] in (5).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5ProgressionTerm x d1 d2 = ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x, ∑ n ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp, if d1.lcm d2 ∣ x - pp.1 * pp.2 * n then AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight x pp n else 0

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergSquare_eq_expanded (x z4 : ℕ) (lambda : ℕ → ℝ) : chen1973Lemma5SelbergSquare x z4 lambda = ∑ d1 ∈ chen1973Lemma5DivisorCarrier x z4, ∑ d2 ∈ chen1973Lemma5DivisorCarrier x z4, lambda d1 * lambda d2 * chen1973Lemma5ProgressionTerm x d1 d2

Expansion of Chen's Selberg square into the two divisor variables.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrincipalAll (x d1 d2 : ℕ) : ℝ

Principal-character sum with no coprimality deletion.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrincipalAll x d1 d2 = (↑(d1.lcm d2).totient)⁻¹ * ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x, ∑ n ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp, AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight x pp n

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrincipalGood (x d1 d2 : ℕ) : ℝ

The part of the principal sum satisfying (p₁p₂n,d₁d₂)=1.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrincipalGood x d1 d2 = (↑(d1.lcm d2).totient)⁻¹ * ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x, ∑ n ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp, if (pp.1 * pp.2 * n).Coprime (d1 * d2) then AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight x pp n else 0

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrincipalBad (x d1 d2 : ℕ) : ℝ

The complementary principal contribution (p₁p₂n,d₁d₂)>1, source M₃.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrincipalBad x d1 d2 = (↑(d1.lcm d2).totient)⁻¹ * ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x, ∑ n ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp, if (pp.1 * pp.2 * n).Coprime (d1 * d2) then 0 else AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight x pp n

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrincipalAll_eq_good_add_bad (x d1 d2 : ℕ) : chen1973Lemma5PrincipalAll x d1 d2 = chen1973Lemma5PrincipalGood x d1 d2 + chen1973Lemma5PrincipalBad x d1 d2

Pure finite partition of the principal sum into good and bad gcd lanes.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M1 (x z4 : ℕ) (lambda : ℕ → ℝ) : ℝ

Source M₁: the unrestricted principal-character main term.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M1 x z4 lambda = ∑ d1 ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorCarrier x z4, ∑ d2 ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorCarrier x z4, lambda d1 * lambda d2 * AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrincipalAll x d1 d2

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M3 (x z4 : ℕ) (lambda : ℕ → ℝ) : ℝ

Source M₃: the non-coprime correction removed from M₁.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M3 x z4 lambda = ∑ d1 ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorCarrier x z4, ∑ d2 ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorCarrier x z4, lambda d1 * lambda d2 * AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrincipalBad x d1 d2

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M4 (x z4 : ℕ) (lambda : ℕ → ℝ) : ℝ

Source M₄ at the finite pre-contour level: the exact progression remainder after subtracting the coprime principal-character term.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M4 x z4 lambda = ∑ d1 ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorCarrier x z4, ∑ d2 ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5DivisorCarrier x z4, lambda d1 * lambda d2 * (AnalyticNumberTheory.LargeSieve.chen1973Lemma5ProgressionTerm x d1 d2 - AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrincipalGood x d1 d2)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimitiveTwist (x q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The actual twisted switched source at modulus q; the coefficient remains literally Λ(n) Φ(x/(p₁p₂n)) / log(x/(p₁p₂)).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimitiveTwist x q χ = star (↑χ ↑x) * ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x, ∑ n ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp, ↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight x pp n) * ↑χ ↑(pp.1 * pp.2 * n)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5_character_orthogonality {q x a : ℕ} [NeZero q] (hxq : x.Coprime q) : ∑ χ : DirichletCharacter ℂ q, star (χ ↑x) * χ ↑a = if ↑x = ↑a then ↑q.totient else 0

The pointwise Dirichlet-character orthogonality relation needed to turn a progression condition into a character sum. Unlike a black-box source premise, this finite step is proved directly from Mathlib's orthogonality API.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2Signed (x D : ℕ) : ℝ

The old one-conductor signed ledger. It is useful as the inner character majorant, but it is not Chen's p. 117--119 source M₂: that source still has an outer squarefree d-sum and the restriction (p₁p₂,d)=1.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2Signed x D = ∑ l ∈ Finset.range (D + 1) with l.Coprime x ∧ Squarefree l, ↑(ArithmeticFunction.moebius l) ^ 2 * 3 ^ l.primeFactors.card / ↑l.totient * (∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter l, if ↑χ = 1 then 0 else AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimitiveTwist x l χ).re

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2InnerMajorant (x D : ℕ) : ℝ

Compatibility name for the old one-conductor norm ledger. This is only an inner majorant (the shape later denoted N_m after inserting a prime-pair filter), not the source M₂ of Lemma 5. The source-faithful object is chen1973Lemma5M2Source below.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2InnerMajorant x D = ∑ l ∈ Finset.range (D + 1) with l.Coprime x ∧ Squarefree l, ↑(ArithmeticFunction.moebius l) ^ 2 * 3 ^ l.primeFactors.card / ↑l.totient * ‖∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter l, if ↑χ = 1 then 0 else AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimitiveTwist x l χ‖

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2 (x D : ℕ) : ℝ

Legacy API retained for downstream files. Semantically this is the one-conductor inner majorant, not source M₂.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2 x D = AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2InnerMajorant x D

def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2OuterDivisors (x D : ℕ) : Finset ℕ

The p. 119 outer squarefree-divisor carrier.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2OuterDivisors x D = {d ∈ Finset.Icc 2 D | d.Coprime x ∧ Squarefree d}

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2OuterWeight (d : ℕ) : ℝ

The p. 119 outer weight 3^ν(d)|μ(d)|/φ(d).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2OuterWeight d = 3 ^ d.primeFactors.card * |↑(ArithmeticFunction.moebius d)| / ↑d.totient

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimitiveTwistCoprime (x l d : ℕ) (χ : PrimitiveCharacter l) : ℂ

The literal primitive twist after retaining the source condition (p₁p₂,d)=1. The character conductor is the independent inner variable l.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimitiveTwistCoprime x l d χ = star (↑χ ↑x) * ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimePairs x with (pp.1 * pp.2).Coprime d, ∑ n ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp, ↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma5SmoothedWeight x pp n) * ↑χ ↑(pp.1 * pp.2 * n)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2SourceInner (x D d : ℕ) : ℝ

The inner conductor sum at a fixed outer divisor d.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2SourceInner x D d = ∑ l ∈ Finset.range (D + 1) with l.Coprime x ∧ Squarefree l, ↑(ArithmeticFunction.moebius l) ^ 2 * 3 ^ l.primeFactors.card / ↑l.totient * ‖∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter l, if ↑χ = 1 then 0 else AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimitiveTwistCoprime x l d χ‖

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2Source (x D : ℕ) : ℝ

Source-faithful M₂ on pp. 117--119: first the outer d weight, then the independent inner conductor l primitive-character sum, with (p₁p₂,d)=1 inside the prime-pair carrier.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2Source x D = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2OuterDivisors x D, AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2OuterWeight d * AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2SourceInner x D d

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2SourceSigned (x D : ℕ) : ℝ

Signed pre-norm form of the same two-layer source. This is the exact finite target for the Selberg/character expansion of the actual M₄ remainder.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2SourceSigned x D = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2OuterDivisors x D, AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2OuterWeight d * ∑ l ∈ Finset.range (D + 1) with l.Coprime x ∧ Squarefree l, ↑(ArithmeticFunction.moebius l) ^ 2 * 3 ^ l.primeFactors.card / ↑l.totient * (∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter l, if ↑χ = 1 then 0 else AnalyticNumberTheory.LargeSieve.chen1973Lemma5PrimitiveTwistCoprime x l d χ).re

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2Signed_le_M2 (x D : ℕ) : chen1973Lemma5M2Signed x D ≤ chen1973Lemma5M2 x D

The old one-conductor real-part ledger is bounded by its norm ledger.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5M2SourceSigned_le_source (x D : ℕ) : chen1973Lemma5M2SourceSigned x D ≤ chen1973Lemma5M2Source x D

Taking norms conductor-by-conductor bounds the signed two-layer source.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5M4_le_M2_of_conductor_grouping {x z4 D : ℕ} {lambda : ℕ → ℝ} (hgroup : chen1973Lemma5M4 x z4 lambda ≤ chen1973Lemma5M2SourceSigned x D) : chen1973Lemma5M4 x z4 lambda ≤ chen1973Lemma5M2Source x D

Finite M₄ ≤ M₂ connector with the correct source object. The premise is exactly the still-separate Selberg-coefficient/imprimitive-character expansion; the norm step itself is proved here.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5ActualM4_le_M2Source_of_character_expansion {x z4 R D : ℕ} (hexpand : chen1973Lemma5M4 x z4 (chen1973Lemma5SelbergLambda x R) ≤ chen1973Lemma5M2SourceSigned x D) : chen1973Lemma5M4 x z4 (chen1973Lemma5SelbergLambda x R) ≤ chen1973Lemma5M2Source x D

The preceding connector specialized to Chen's actual p. 115 Selberg coefficient, making the link to the concrete M₄ remainder explicit.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5_expanded_eq_M1_sub_M3_add_M4 (x z4 : ℕ) (lambda : ℕ → ℝ) : ∑ d1 ∈ chen1973Lemma5DivisorCarrier x z4, ∑ d2 ∈ chen1973Lemma5DivisorCarrier x z4, lambda d1 * lambda d2 * chen1973Lemma5ProgressionTerm x d1 d2 = chen1973Lemma5M1 x z4 lambda - chen1973Lemma5M3 x z4 lambda + chen1973Lemma5M4 x z4 lambda

Exact finite M₁-M₃+M₄ decomposition of the expanded Selberg square.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5SelbergSquare_eq_M1_sub_M3_add_M4 (x z4 : ℕ) (lambda : ℕ → ℝ) : chen1973Lemma5SelbergSquare x z4 lambda = chen1973Lemma5M1 x z4 lambda - chen1973Lemma5M3 x z4 lambda + chen1973Lemma5M4 x z4 lambda

Equation (5), now as a kernel-checked finite identity.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma5ActualSelbergSquare_eq_M1_sub_M3_add_M4 (x z4 R : ℕ) : chen1973Lemma5SelbergSquare x z4 (chen1973Lemma5SelbergLambda x R) = chen1973Lemma5M1 x z4 (chen1973Lemma5SelbergLambda x R) - chen1973Lemma5M3 x z4 (chen1973Lemma5SelbergLambda x R) + chen1973Lemma5M4 x z4 (chen1973Lemma5SelbergLambda x R)

Equation (5) specialized to Chen's actual p. 115 Selberg coefficient.