Chen 1973, Lemma 6, equation (17): the L' S contour shift

This file isolates the honest complex-analytic deformation used in (17). The integrand is the actual product L'(s,χ) S(H,s,χ) y^s K_x(s), with K_x Chen's rational Mellin kernel. The proof never divides by L on the beta line.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17ShiftIntegrand {d : ℕ} [NeZero d] (x H : ℕ) (y : ℝ) (χ : PrimitiveCharacter d) (s : ℂ) : ℂ

The actual holomorphic factor shifted in the second term of (16).

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17ShiftIntegrand x H y χ s = deriv (DirichletCharacter.LFunction ↑χ) s * AnalyticNumberTheory.LargeSieve.chen1973Lemma6MobiusPartialSum H s χ * (↑y ^ s * AnalyticNumberTheory.LargeSieve.chen1973MellinKernel (↑x) s)

theorem AnalyticNumberTheory.LargeSieve.differentiableOn_chen1973Lemma6Eq17ShiftIntegrand_strip {d x H : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (hχ : ↑χ ≠ 1) (hx : 1 < x) {y : ℝ} (hy : 0 < y) : DifferentiableOn ℂ (chen1973Lemma6Eq17ShiftIntegrand x H y χ) {s : ℂ | chen1973Lemma6Beta x ≤ s.re ∧ s.re ≤ chen1973Lemma6Alpha x}

For a nonprincipal primitive character, the actual L' S integrand is holomorphic throughout Chen's closed strip. Primitivity is part of the type; nonprincipality is used only to make L entire. No beta-line nonvanishing assumption occurs.

def AnalyticNumberTheory.LargeSieve.chen1973VerticalSection (f : ℂ → ℂ) (σ t : ℝ) : ℂ

A vertical section of a complex integrand.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973VerticalSection f σ t = f (↑σ + ↑t * Complex.I)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973HorizontalSection (f : ℂ → ℂ) (β α T : ℝ) : ℂ

The two horizontal sides of the rectangle, oriented from beta to alpha.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973HorizontalSection f β α T = (∫ (u : ℝ) in β..α, f (↑u + -↑T * Complex.I)) - ∫ (u : ℝ) in β..α, f (↑u + ↑T * Complex.I)

theorem AnalyticNumberTheory.LargeSieve.chen1973_finite_rectangle_vertical_identity {f : ℂ → ℂ} {β α T : ℝ} (hβα : β ≤ α) (hf : DifferentiableOn ℂ f {s : ℂ | β ≤ s.re ∧ s.re ≤ α}) : (∫ (t : ℝ) in -T..T, chen1973VerticalSection f α t) - ∫ (t : ℝ) in -T..T, chen1973VerticalSection f β t = Complex.I * chen1973HorizontalSection f β α T

Cauchy--Goursat on the finite rectangle, rewritten as a vertical-line identity.

theorem AnalyticNumberTheory.LargeSieve.chen1973_full_vertical_integral_shift {f : ℂ → ℂ} {β α C : ℝ} (hβα : β ≤ α) (hC : 0 ≤ C) (hhol : DifferentiableOn ℂ f {s : ℂ | β ≤ s.re ∧ s.re ≤ α}) (hβint : MeasureTheory.Integrable (chen1973VerticalSection f β) MeasureTheory.volume) (hαint : MeasureTheory.Integrable (chen1973VerticalSection f α) MeasureTheory.volume) (hhoriz : ∀ (T : ℝ), 0 ≤ T → ‖chen1973HorizontalSection f β α T‖ ≤ C / (1 + T ^ 2)) : ∫ (t : ℝ), chen1973VerticalSection f α t = ∫ (t : ℝ), chen1973VerticalSection f β t

Full Bochner contour shift. The only quantitative hypotheses are the two explicit horizontal-side estimates produced from Chen's rational kernel. They are strictly weaker than the desired integral equality and expose the exact remaining growth estimate for L' S; no conclusion-equivalent premise is accepted.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_LDerivS_contour_shift {d x H : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (hχ : ↑χ ≠ 1) (hx : 1 < x) {y C : ℝ} (hy : 0 < y) (hC : 0 ≤ C) (hβint : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq17ShiftIntegrand x H y χ) (chen1973Lemma6Beta x)) MeasureTheory.volume) (hαint : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq17ShiftIntegrand x H y χ) (chen1973Lemma6Alpha x)) MeasureTheory.volume) (hhoriz : ∀ (T : ℝ), 0 ≤ T → ‖chen1973HorizontalSection (chen1973Lemma6Eq17ShiftIntegrand x H y χ) (chen1973Lemma6Beta x) (chen1973Lemma6Alpha x) T‖ ≤ C / (1 + T ^ 2)) : ∫ (t : ℝ), chen1973VerticalSection (chen1973Lemma6Eq17ShiftIntegrand x H y χ) (chen1973Lemma6Alpha x) t = ∫ (t : ℝ), chen1973VerticalSection (chen1973Lemma6Eq17ShiftIntegrand x H y χ) (chen1973Lemma6Beta x) t

Equation-(17)'s actual L' S contour shift, from Chen's alpha line to his beta line. Holomorphy is discharged internally from nonprincipality; callers supply only Bochner integrability and the horizontal kernel-decay estimate.