Chen 1973, Lemma 6, equations (16) and (17)

This module records the two displayed formulae on pp. 120--121 with the actual finite S(H,s,χ) and the actual switched Φ from equation (12). In particular, there is no free function named Phi.

The second prefactor in (17) is the printed x^(1/2) (p.121).

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha (x : ℕ) : ℝ

Chen's two vertical lines in (17).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x = 1 + 1 / Real.log ↑x

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta (x : ℕ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x = 1 / 2 + 1 / Real.log ↑x

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue (q : ℕ) (s : ℂ) (χ : PrimitiveCharacter q) : ℂ

Totalized L(s,χ) on the primitive range.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue q s χ = if hq : 1 < q then DirichletCharacter.LFunction (↑χ) s else 0

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv (q : ℕ) (s : ℂ) (χ : PrimitiveCharacter q) : ℂ

The totalized derivative used in the finite starred-character sums.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv q s χ = if hq : 1 < q then deriv (DirichletCharacter.LFunction ↑χ) s else 0

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi_termwise_bromwich {x d n : ℕ} {pp : ℕ × ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) (hn : 0 < n) (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) : ↑(ArithmeticFunction.vonMangoldt n) * ↑(chen1973PerronKernelFinite (↑x) (↑x / (↑pp.1 * ↑pp.2 * ↑n))) * ↑χ ↑n = ↑(ArithmeticFunction.vonMangoldt n) * (↑(1 / (2 * Real.pi)) * ∫ (t : ℝ), chen1973BromwichIntegrand (↑x) (↑x / (↑pp.1 * ↑pp.2 * ↑n)) t) * ↑χ ↑n

Termwise actual-Φ interface to the already closed Mellin--Bromwich identity. The finite sum is left finite here; hence no conditional tsum reordering is involved. This is the exact analytic kernel consumed before (16).

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation16 {d H : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (s : ℂ) (hL : DirichletCharacter.LFunction (↑χ) s ≠ 0) : deriv (DirichletCharacter.LFunction ↑χ) s / DirichletCharacter.LFunction (↑χ) s = deriv (DirichletCharacter.LFunction ↑χ) s / DirichletCharacter.LFunction (↑χ) s * (1 - DirichletCharacter.LFunction (↑χ) s * chen1973Lemma6MobiusPartialSum H s χ) + deriv (DirichletCharacter.LFunction ↑χ) s * chen1973Lemma6MobiusPartialSum H s χ

The exact algebraic decomposition (16). The only analytic fact needed is the pointwise nonvanishing required to divide by L.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation16_on_alpha {d H : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (hχ : ↑χ ≠ 1) (x : ℕ) (hx : 1 < x) (v : ℝ) : deriv (DirichletCharacter.LFunction ↑χ) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) / DirichletCharacter.LFunction (↑χ) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) = deriv (DirichletCharacter.LFunction ↑χ) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) / DirichletCharacter.LFunction (↑χ) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) * (1 - DirichletCharacter.LFunction (↑χ) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) * chen1973Lemma6MobiusPartialSum H (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) χ) + deriv (DirichletCharacter.LFunction ↑χ) (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) * chen1973Lemma6MobiusPartialSum H (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) χ

On the printed right line, (16) needs no additional zero-free hypothesis: nonprincipal Dirichlet L-functions do not vanish for Re s ≥ 1.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17Kernel (x : ℕ) (s : ℂ) : ℝ

The literal high-power radial denominator printed in (17). Its scale is (log x)^(11/10) and its exponent is [log x] + 1; in particular it has no conductor-level dependence.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17Kernel x s = ‖s‖ * (1 + ‖s‖ / AnalyticNumberTheory.LargeSieve.chen1973PerronScale ↑x) ^ (AnalyticNumberTheory.LargeSieve.chen1973PerronOrder ↑x + 1)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6A (x L level B k m H : ℕ) (s : ℂ) : ℝ

The actual A(l,k,s,m,H) of p. 121. The source has already paid the alpha-line logarithmic derivative pointwise into the exterior (log x)^2 prefactor, so A contains only the pair polynomial and 1-LS.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6A x L level B k m H s = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, |↑(ArithmeticFunction.moebius d)| * 3 ^ d.primeFactors.card / ↑d * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, ‖∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m, ↑χ ↑(pp.1 * pp.2) / ((↑pp.1 * ↑pp.2) ^ s * ↑(Real.log (↑x / (↑pp.1 * ↑pp.2))))‖ * ‖1 - AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue d s χ * AnalyticNumberTheory.LargeSieve.chen1973Lemma6MobiusPartialSum H s χ‖

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6B (x L level B k m H : ℕ) (s : ℂ) : ℝ

The actual B(l,k,s,m,H) of p. 121.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6B x L level B k m H s = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, |↑(ArithmeticFunction.moebius d)| * 3 ^ d.primeFactors.card / ↑d * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, ‖∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m, ↑χ ↑(pp.1 * pp.2) / ((↑pp.1 * ↑pp.2) ^ s * ↑(Real.log (↑x / (↑pp.1 * ↑pp.2))))‖ * ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv d s χ * AnalyticNumberTheory.LargeSieve.chen1973Lemma6MobiusPartialSum H s χ‖

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17FirstIntegral (x L level B k m H : ℕ) : ℝ

First actual vertical-line integral in (17), on Re s = α.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17FirstIntegral x L level B k m H = ∫ (v : ℝ) in Set.Ioi 0, AnalyticNumberTheory.LargeSieve.chen1973Lemma6A x L level B k m H (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑v * Complex.I) / AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17Kernel x (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑v * Complex.I)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17SecondIntegral (x L level B k m H : ℕ) : ℝ

Second actual vertical-line integral in (17), on Re s = β.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17SecondIntegral x L level B k m H = ∫ (v : ℝ) in Set.Ioi 0, AnalyticNumberTheory.LargeSieve.chen1973Lemma6B x L level B k m H (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) + ↑v * Complex.I) / AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17Kernel x (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) + ↑v * Complex.I)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation17RHS (x L level B k m H : ℕ) : ℝ

The literal right side of (17), with the original beta prefactor x^(1/2).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation17RHS x L level B k m H = 2 * ↑x * Real.log ↑x ^ 2 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17FirstIntegral x L level B k m H + 2 * ↑x ^ (1 / 2) * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17SecondIntegral x L level B k m H

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlockActual (x L level B k m : ℕ) : ℝ

The actual equation-(17) left side, with the pair-dependent Φ from equation (12) inserted directly (rather than passed as a free parameter).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlockActual x L level B k m = ∑ 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)))⁻¹ * AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2)‖

def AnalyticNumberTheory.LargeSieve.Chen1973Equation17ContourMajorization (x L level B k m H : ℕ) : Prop

Compatibility boundary for the still-unformalized contour deformation in (17). This is not a beta-line zero-free hypothesis: on the source range level ≥ 1, every conductor is greater than one, hence the primitive character is nonprincipal and L'·S continues entire to the beta line. The remaining work is the quantitative deformation from the unconditional Bromwich line, including the whole-line to half-line symmetry and Bochner integrability/Fubini argument.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Equation17ContourMajorization x L level B k m H = (AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlockActual x L level B k m ≤ AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation17RHS x L level B k m H)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation17_of_contourMajorization {x L level B k m H : ℕ} (h17 : Chen1973Equation17ContourMajorization x L level B k m H) : chen1973Lemma6NmBlockActual x L level B k m ≤ 2 * ↑x * Real.log ↑x ^ 2 * chen1973Lemma6Eq17FirstIntegral x L level B k m H + 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq17SecondIntegral x L level B k m H

Compatibility consumer for a supplied contour majorization. The premise-free publication theorem is proved in the equation-(17) assembly module.