Chen 1973, Lemma 6, equations (14) and (15)

This file freezes the finite algebra on p. 120. All Dirichlet polynomials use natural order. In particular, no conditionally convergent tsum is used. Equation (14) is separated into its finite large-sieve term and the literal truncation remainder. Equation (15) is the fourth moment of the finite Möbius polynomial. The final two results record the actual unconditional Lemma 3 calls needed on the adjacent Cauchy circle.

@[reducible, inline]

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

Chen's natural-order polynomial S(H,s,χ).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6NaturalMobiusPolynomial H s χ = AnalyticNumberTheory.LargeSieve.chen1973Lemma6MobiusPartialSum H s χ

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

The natural-order truncation of L(s,χ) used on p. 120.

Equations

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

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

The actual expression 1-L(s,χ)S(H,s,χ).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6OneSubLS H s χ = 1 - AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLValue d s χ * AnalyticNumberTheory.LargeSieve.chen1973Lemma6NaturalMobiusPolynomial H s χ

def AnalyticNumberTheory.LargeSieve.chen1973Lemma6ProductCoefficient (H : ℕ) (A B : ℕ → ℂ) (m : ℤ) : ℂ

A generic finite product coefficient. Keeping the two cpow factors here avoids any appeal to an infinite Dirichlet-series product.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6ProductCoefficient H A B m = ∑ ab ∈ (Finset.Icc 1 H).product (Finset.Icc 1 H), if ↑ab.1 * ↑ab.2 = m then A ab.1 * B ab.2 else 0

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_product_sum_eq_collected (H : ℕ) (A B : ℕ → ℂ) {d : ℕ} (χ : PrimitiveCharacter d) : (∑ a ∈ Finset.Icc 1 H, A a * ↑χ ↑a) * ∑ b ∈ Finset.Icc 1 H, B b * ↑χ ↑b = ∑ m ∈ Finset.Icc 1 ↑(H * H), chen1973Lemma6ProductCoefficient H A B m * ↑χ ↑m

Exact collection of a product of two natural-order finite polynomials.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6CHWeightedCoefficient (H : ℕ) (s : ℂ) (m : ℤ) : ℂ

The finite coefficient C_H(n)/n^s in the product approximation to 1-LS. It is deliberately a finite convolution.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6CHWeightedCoefficient H s m = (if m = 1 then 1 else 0) - AnalyticNumberTheory.LargeSieve.chen1973Lemma6ProductCoefficient H (fun (n : ℕ) => ↑n ^ (-s)) (fun (n : ℕ) => ↑(ArithmeticFunction.moebius n) / ↑n ^ s) m

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_one_sub_finiteLS_eq_CH {H d : ℕ} (hH : 0 < H) (s : ℂ) (χ : PrimitiveCharacter d) : 1 - chen1973Lemma6NaturalLPolynomial H s χ * chen1973Lemma6NaturalMobiusPolynomial H s χ = ∑ m ∈ Finset.Icc 1 ↑(H * H), chen1973Lemma6CHWeightedCoefficient H s m * ↑χ ↑m

The p. 120 finite convolution identity.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_oneSubLS_eq_CH_sub_remainder {H d : ℕ} (hH : 0 < H) (s : ℂ) (χ : PrimitiveCharacter d) : chen1973Lemma6OneSubLS H s χ = ∑ m ∈ Finset.Icc 1 ↑(H * H), chen1973Lemma6CHWeightedCoefficient H s m * ↑χ ↑m - (chen1973PrimitiveLValue d s χ - chen1973Lemma6NaturalLPolynomial H s χ) * chen1973Lemma6NaturalMobiusPolynomial H s χ

Exact decomposition of the actual 1-LS: finite convolution minus the literal finite-truncation remainder.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6MobiusSquareCoefficient (H : ℕ) (s : ℂ) (m : ℤ) : ℂ

The coefficient j(n)/n^s in S(H,s,χ)^2.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6MobiusSquareCoefficient H s m = AnalyticNumberTheory.LargeSieve.chen1973Lemma6ProductCoefficient H (fun (n : ℕ) => ↑(ArithmeticFunction.moebius n) / ↑n ^ s) (fun (n : ℕ) => ↑(ArithmeticFunction.moebius n) / ↑n ^ s) m

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_mobiusPolynomial_sq_eq_collected (H : ℕ) (s : ℂ) {d : ℕ} (χ : PrimitiveCharacter d) : chen1973Lemma6NaturalMobiusPolynomial H s χ ^ 2 = ∑ m ∈ Finset.Icc 1 ↑(H * H), chen1973Lemma6MobiusSquareCoefficient H s m * ↑χ ↑m

Exact finite j-coefficient expansion used in (15).

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma2_equationThree_complex_unconditional (c : ℤ → ℂ) (M : ℤ) (N D Q : ℕ) (hD : 0 < D) : ∃ (C : ℝ), 0 < C ∧ ∑ q ∈ Finset.Ioc D Q, 1 / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), c n * ↑χ ↑n‖ ^ 2 ≤ 2 * C * (↑Q + ↑N / ↑D) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖c n‖ ^ 2

Complex-coefficient form of Chen's equation (3). The factor 2 is the explicit cost of applying the real sharp large sieve to real and imaginary parts.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation14_finite_second_moment (H D Q : ℕ) (s : ℂ) (hD : 0 < D) (_hs : 1 ≤ s.re) : ∃ (C : ℝ), 0 < C ∧ ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖∑ m ∈ Finset.Icc 1 ↑(H * H), chen1973Lemma6CHWeightedCoefficient H s m * ↑χ ↑m‖ ^ 2 ≤ 2 * C * (↑Q + ↑(H * H) / ↑D) * ∑ m ∈ Finset.Icc 1 ↑(H * H), ‖chen1973Lemma6CHWeightedCoefficient H s m‖ ^ 2

Equation (14), finite large-sieve term. This is an unconditional call to Chen's sharp Lemma 2; Re(s)≥1 is retained because it is the source range in which the adjacent truncation theorem is used.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation14RemainderMoment (H D Q : ℕ) (s : ℂ) : ℝ

The literal truncation-remainder ledger in (14). This is not an Eq. (14)-shaped assumption: it is the concrete error (L-P_H) S(H) appearing in the exact convolution identity.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation14RemainderMoment H D Q s = ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, ‖(AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLValue d s χ - AnalyticNumberTheory.LargeSieve.chen1973Lemma6NaturalLPolynomial H s χ) * AnalyticNumberTheory.LargeSieve.chen1973Lemma6NaturalMobiusPolynomial H s χ‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation14_weighted_second_moment (H D Q : ℕ) (s : ℂ) (hH : 0 < H) (hD : 0 < D) (hs : 1 ≤ s.re) : ∃ (C : ℝ), 0 < C ∧ ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖chen1973Lemma6OneSubLS H s χ‖ ^ 2 ≤ 4 * C * (↑Q + ↑(H * H) / ↑D) * ∑ m ∈ Finset.Icc 1 ↑(H * H), ‖chen1973Lemma6CHWeightedCoefficient H s m‖ ^ 2 + 2 * chen1973Lemma6Equation14RemainderMoment H D Q s

Equation (14) with the actual 1-L(s,χ)S(H,s,χ) on the left. The sharp Lemma 2 payment is internal; only the literal Abel-truncation remainder remains visible for the subsequent p. 120 scalar estimate.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation15_fourth_moment (H D Q : ℕ) (s : ℂ) (hD : 0 < D) (_hs : 1 / 2 ≤ s.re) : ∃ (C : ℝ), 0 < C ∧ ∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖chen1973Lemma6NaturalMobiusPolynomial H s χ‖ ^ 4 ≤ 2 * C * (↑Q + ↑(H * H) / ↑D) * ∑ m ∈ Finset.Icc 1 ↑(H * H), ‖chen1973Lemma6MobiusSquareCoefficient H s m‖ ^ 2

Equation (15): the actual fourth moment of the natural-order Möbius polynomial, before the elementary |j(n)|≤τ(n) scalar simplification.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_L_fourth_moment_corrected {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 Lemma 3 input used after (15).

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_L_fourth_moment_bounded_height {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 Lemma 3 specialization used uniformly on Chen's small Cauchy circle. The concrete height inequality is retained, not hidden in an Eq. (15)-shaped premise.