Chen 1973, Lemma 6, equation (19): moment transport

This leaf pays the change from the squarefree equation-(17) weight |μ(d)| 3^ω(d) / d to the reciprocal-totient weight used in (14), (15), and Lemma 2. It also applies the sharp, unconditional Lemma 2 to the literal prime-pair polynomial. The bounds stop at scalar moments and do not assume the final cell estimate.

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

Public copy of the equation-(17) conductor weight.

Equations

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

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairCoefficient (x B k m : ℕ) (s : ℂ) (n : ℤ) : ℂ

The coefficient obtained by collecting equal products in the literal pair polynomial of equation (19).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19PairCoefficient x B k m s n = ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m, if ↑pp.1 * ↑pp.2 = n then 1 / ((↑pp.1 * ↑pp.2) ^ s * ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))) else 0

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19Weight_nonneg (d : ℕ) : 0 ≤ chen1973Lemma6Eq19Weight d

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19Weight_le_I_div_totient {x L level d : ℕ} (hd : d ∈ chen1973Lemma6ConductorBlock x L level) : chen1973Lemma6Eq19Weight d ≤ chen1973Lemma6Eq19I x L level / ↑d.totient

Squarefreeness removes the Möbius absolute value, and φ(d) ≤ d changes 1/d to 1/φ(d). This is the pointwise weight transport used in (19).

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_weight_transport {x L level : ℕ} (F : ℕ → ℝ) (hF : ∀ (d : ℕ), 0 ≤ F d) : ∑ d ∈ chen1973Lemma6ConductorBlock x L level, chen1973Lemma6Eq19Weight d * F d ≤ chen1973Lemma6Eq19I x L level * ∑ d ∈ chen1973Lemma6ConductorBlock x L level, 1 / ↑d.totient * F d

Transport any nonnegative cell ledger to reciprocal-totient normalization.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_pairPolynomial_eq_collected (x B k m : ℕ) (s : ℂ) {d : ℕ} (χ : PrimitiveCharacter d) : ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ↑χ ↑(pp.1 * pp.2) / ((↑pp.1 * ↑pp.2) ^ s * ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))) = ∑ n ∈ Finset.Icc 1 ↑(x * x), chen1973Lemma6Eq19PairCoefficient x B k m s n * ↑χ ↑n

Exact collection identity for the literal pair polynomial.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_pair_second_moment (x L level B k m D Q : ℕ) (s : ℂ) (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : ∃ (C : ℝ), 0 < C ∧ chen1973Lemma6Eq19PairSecondMoment x L level B k m s ≤ chen1973Lemma6Eq19I x L level * (2 * C * (↑Q + ↑(x * x) / ↑D) * ∑ n ∈ Finset.Icc 1 ↑(x * x), ‖chen1973Lemma6Eq19PairCoefficient x B k m s n‖ ^ 2)

The actual pair-polynomial second moment on any source cell contained in (D,Q]. The constant comes from the proved sharp Lemma 2; no cell-bound premise is accepted.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_oneSub_second_moment (x L level H D Q : ℕ) (s : ℂ) (hH : 0 < H) (hD : 0 < D) (hDQ : D < Q) (hs : 1 ≤ s.re) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : ∃ (C : ℝ), 0 < C ∧ chen1973Lemma6Eq19OneSubSecondMoment x L level H s ≤ chen1973Lemma6Eq19I x L level * (4 * C * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4 + 2 * ↑Q * (40 * ‖s‖ * √↑Q * Real.log ↑Q * ↑(H + 1) ^ (-s.re) * (1 + Real.log ↑H)) ^ 2)

Equation (14) transported to the literal equation-(19) weight and paid by its unconditional explicit scalar endpoint.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_mobius_fourth_moment (x L level H D Q : ℕ) (s : ℂ) (hD : 0 < D) (hs : Chen1973Lemma3Domain s s.re s.im) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : ∃ (C : ℝ), 0 < C ∧ chen1973Lemma6Eq19MobiusFourthMoment x L level H s ≤ chen1973Lemma6Eq19I x L level * (2 * C * (↑Q + ↑(H * H) / ↑D) * (1 + Real.log ↑(H * H)) ^ 4)

Equation (15) transported to the literal equation-(19) weight and paid by its unconditional divisor-energy scalar endpoint.

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

A nonnegative scalar envelope for the corrected Lemma 3 fourth moment on the Cauchy circle of radius r about s.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq19CircleFourthEnvelope Q s r = 21000000 * ↑Q ^ 2 * (‖s‖ + r) ^ 2 * Real.log (↑Q * (1 + (‖s‖ + r))) ^ 4

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_LDeriv_fourth_moment_cauchy (x L level Q : ℕ) (s : ℂ) (r : ℝ) (hQ : 2 ≤ Q) (hr : 0 < r) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Icc 2 Q) (hsphere : ∀ z ∈ Metric.sphere s r, Chen1973Lemma3Domain z z.re z.im) : chen1973Lemma6Eq19LDerivFourthMoment x L level s ≤ chen1973Lemma6Eq19I x L level * ↑Q * ((chen1973Lemma6Eq19CircleFourthEnvelope Q s r + 1) / r) ^ 4

The actual L' fourth moment on an equation-(17) cell, obtained by Cauchy's circle estimate from the unconditional corrected Lemma 3. The deliberately coarse extra factor Q only counts reciprocal-totient-normalized character families; all constants and the circle range are explicit.