Documentation

MathlibNt.AnalyticNumberTheory.Chen1973.Chen1973Lemma6Equations14And15ScalarPayments

Chen 1973, Lemma 6, equations (14) and (15): scalar payments #

This file pays the elementary scalar estimates left after the exact finite expansions in Chen1973Lemma6Equations14And15. Each payment is a separate result. The coefficient estimates apply only to Chen's literal coefficients; there is no arbitrary-coefficient strengthening.

Trivial harmonic majorant for Chen's literal Möbius polynomial on the Re(s) ≥ 1 line used in equation (14).

Pointwise Abel--Pólya--Vinogradov payment for the literal remainder in (14). The source range Re(s) ≥ 1 is explicit.

The equation-(14) remainder moment is paid by the explicit finite PV--Abel scalar sum; no remainder-shaped premise is retained.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation14_remainderMoment_le_log_explicit (H D Q : ) (s : ) (hH : 0 < H) (hD : 0 < D) (hs : 1 s.re) :
chen1973Lemma6Equation14RemainderMoment H D Q s dFinset.Ioc D Q, (40 * s * d * Real.log d * ↑(H + 1) ^ (-s.re) * (1 + Real.log H)) ^ 2

Logarithmic form of the Abel--PV remainder payment. Positivity of H is stated because it is exactly what makes 1 + log H a nonnegative majorant for the finite harmonic factor.

The finite convolution coefficient C_H(m)/mˢ in (14) has the same weighted divisor majorant as the source uses. The hypothesis Re(s) ≥ 1 is the literal equation-(14) range.

The C_H divisor-energy payment in equation (14).

Explicit log⁴ version of the C_H energy payment.

The literal coefficient j(m) in (15), including its m⁻ˢ weight, is bounded by τ(m)m⁻¹/² on Chen's half-plane.

Weighted divisor-square payment for the literal j(m) coefficients in (15). This is the finite form of |j(m)| ≤ τ(m) followed by ∑ τ(m)²/m ≪ log⁴.

Explicit logarithmic version of the (15) coefficient energy.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation15_scalar_paid (H D Q : ) (s : ) (hD : 0 < D) (hs : Chen1973Lemma3Domain s s.re s.im) :
∃ (C : ), 0 < C dFinset.Ioc D Q, 1 / d.totient * χ : PrimitiveCharacter d, chen1973Lemma6NaturalMobiusPolynomial H s χ ^ 4 2 * C * (Q + ↑(H * H) / D) * (1 + Real.log ↑(H * H)) ^ 4

Equation (15) after paying its literal weighted divisor-square energy.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation14_remainderMoment_final_scalar (H D Q : ) (s : ) (hH : 0 < H) (hD : 0 < D) (hDQ : D < Q) (hs : 1 s.re) :
chen1973Lemma6Equation14RemainderMoment H D Q s Q * (40 * s * Q * Real.log Q * ↑(H + 1) ^ (-s.re) * (1 + Real.log H)) ^ 2

The finite Abel--PV remainder summed over Chen's literal conductor interval D < d ≤ Q. The hypotheses 0 < H, 0 < D, and D < Q are exactly the nonempty source regime; the constant 40 and every height factor remain visible.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation14_final_scalar_paid (H D Q : ) (s : ) (hH : 0 < H) (hD : 0 < D) (hDQ : D < Q) (hs : 1 s.re) :
∃ (C : ), 0 < C dFinset.Ioc D Q, 1 / d.totient * χ : PrimitiveCharacter d, chen1973Lemma6OneSubLS H s χ ^ 2 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

Final scalar form of equation (14). It combines the sharp finite second moment, the literal C_H divisor energy, and the summed Abel--PV remainder. No equation-(14)-shaped hypothesis is retained.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation15_final_log_power (H D Q : ) (s : ) (hD : 0 < D) (hs : Chen1973Lemma3Domain s s.re s.im) :
∃ (C : ), 0 < C dFinset.Ioc D Q, 1 / d.totient * χ : PrimitiveCharacter d, chen1973Lemma6NaturalMobiusPolynomial H s χ ^ 4 2 * C * (Q + ↑(H * H) / D) * (1 + Real.log ↑(H * H)) ^ 4

Final log⁴ endpoint for equation (15), with Chen's actual half-plane encoded by Chen1973Lemma3Domain and the literal H,D,Q ranges unchanged.