Chen 1973, Lemma 6, equation (21): zero-free-to-contour bridge

The corrected transcription of the printed exponent is 1/300. The left-line comparison is 1 / sqrt (log x) ≤ c / d^(1/300). For fixed positive c and d ≤ (log x)^100 this is eventually true; the former 3/100 obstruction was a transcription error, not a defect of the printed conductor scale.

def AnalyticNumberTheory.LargeSieve.Chen1973Lemma6Eq21ZeroFreeContourBridge (x L : ℕ) (c : ℝ) : Prop

The exact comparison putting the line of (21) inside the printed d^(-1/300) strip. A sufficiently-large-x theorem can discharge this comparison for each fixed positive c; zero-freeness is a separate input.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Lemma6Eq21ZeroFreeContourBridge x L c = ∀ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L 0, 1 / √(Real.log ↑x) ≤ c / ↑d ^ (1 / 300)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_sigma_ge_zeroFreeBoundary {x L d : ℕ} {c : ℝ} (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0) : 1 - c / ↑d ^ (1 / 300) ≤ chen1973Lemma6Eq21Sigma x

The bridge comparison is exactly the inclusion of the printed left line in the printed zero-free half-plane.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_leftLine_nonvanishing {x L d : ℕ} {c : ℝ} (hzero : Chen1973Lemma6Eq21ZeroFreeInput x L c) (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0) (χ : PrimitiveCharacter d) (t : ℝ) : chen1973Lemma6PrimitiveLValue d (chen1973Lemma6Eq21Line x t) χ ≠ 0

Consequently every point on the equation-(21) line is nonzero.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_rectangle_nonvanishing {x L d : ℕ} {c : ℝ} (hzero : Chen1973Lemma6Eq21ZeroFreeInput x L c) (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0) (χ : PrimitiveCharacter d) {s : ℂ} (hs : chen1973Lemma6Eq21Sigma x ≤ s.re ∧ s.re ≤ chen1973Lemma6Alpha x) : chen1973Lemma6PrimitiveLValue d s χ ≠ 0

Nonvanishing on the whole closed vertical strip from the printed left line to the source Bromwich line α = 1 + 1 / log x.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_sigma_pos {x : ℕ} (hx : 3 ≤ x) : 0 < chen1973Lemma6Eq21Sigma x

For the literal source range x ≥ 3, the printed left edge remains in the open right half-plane.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_sigma_le_one (x : ℕ) : chen1973Lemma6Eq21Sigma x ≤ 1

The printed left edge is bounded above by 1.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_sigma_le_alpha {x : ℕ} (hx : 3 ≤ x) : chen1973Lemma6Eq21Sigma x ≤ chen1973Lemma6Alpha x

The printed left edge lies to the left of the source Bromwich line α = 1 + 1 / log x. The weaker comparison with 1 remains available as a separate elementary lemma.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21ShiftIntegrand (x d : ℕ) (χ : PrimitiveCharacter d) (y : ℝ) (s : ℂ) : ℂ

The literal logarithmic-derivative integrand shifted in equation (21), with y = x/(p₁p₂) supplied separately so positivity is visible to the analytic API.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21ShiftIntegrand x d χ y s = ↑y ^ s * AnalyticNumberTheory.LargeSieve.chen1973MellinKernel (↑x) s * (AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv d s χ / AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue d s χ)

theorem AnalyticNumberTheory.LargeSieve.eq21_mellinKernel_differentiableAt {x : ℕ} (hx : 3 ≤ x) {s : ℂ} (hs : 0 < s.re) : DifferentiableAt ℂ (chen1973MellinKernel ↑x) s

Chen's Mellin kernel is differentiable in the open right half-plane.

theorem AnalyticNumberTheory.LargeSieve.differentiableOn_chen1973Lemma6Eq21ShiftIntegrand_strip {x L B k m l₂ d : ℕ} {c y : ℝ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) (hzero : Chen1973Lemma6Eq21ZeroFreeInput x L c) (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0) (χ : PrimitiveCharacter d) (hy : 0 < y) : DifferentiableOn ℂ (chen1973Lemma6Eq21ShiftIntegrand x d χ y) {s : ℂ | chen1973Lemma6Eq21Sigma x ≤ s.re ∧ s.re ≤ chen1973Lemma6Alpha x}

Under the explicit bridge, the actual logarithmic-derivative integrand is holomorphic on the full closed strip between the equation-(21) line and the source Bromwich line α = 1 + 1 / log x. No zero-free statement stronger than the printed input is assumed.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_finite_contour_shift {x L B k m l₂ d : ℕ} {c y T : ℝ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) (hzero : Chen1973Lemma6Eq21ZeroFreeInput x L c) (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0) (χ : PrimitiveCharacter d) (hy : 0 < y) : (∫ (t : ℝ) in -T..T, chen1973VerticalSection (chen1973Lemma6Eq21ShiftIntegrand x d χ y) (chen1973Lemma6Alpha x) t) - ∫ (t : ℝ) in -T..T, chen1973VerticalSection (chen1973Lemma6Eq21ShiftIntegrand x d χ y) (chen1973Lemma6Eq21Sigma x) t = Complex.I * chen1973HorizontalSection (chen1973Lemma6Eq21ShiftIntegrand x d χ y) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T

The finite equation-(21) contour shift on the actual rectangle. This is a Cauchy--Goursat equality, not an assumed contour-majorization inequality.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_full_contour_shift {x L B k m l₂ d : ℕ} {c y C : ℝ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) (hzero : Chen1973Lemma6Eq21ZeroFreeInput x L c) (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0) (χ : PrimitiveCharacter d) (hy : 0 < y) (hC : 0 ≤ C) (hleft : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq21ShiftIntegrand x d χ y) (chen1973Lemma6Eq21Sigma x)) MeasureTheory.volume) (hright : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq21ShiftIntegrand x d χ y) (chen1973Lemma6Alpha x)) MeasureTheory.volume) (hhoriz : ∀ (T : ℝ), 0 ≤ T → ‖chen1973HorizontalSection (chen1973Lemma6Eq21ShiftIntegrand x d χ y) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T‖ ≤ C / (1 + T ^ 2)) : ∫ (t : ℝ), chen1973VerticalSection (chen1973Lemma6Eq21ShiftIntegrand x d χ y) (chen1973Lemma6Alpha x) t = ∫ (t : ℝ), chen1973VerticalSection (chen1973Lemma6Eq21ShiftIntegrand x d χ y) (chen1973Lemma6Eq21Sigma x) t

Passing to infinite vertical lines using the existing contour infrastructure. Integrability of the two vertical sections and the explicit horizontal-edge decay are the precise remaining analytic limit inputs.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21TermShiftIntegrand (x d : ℕ) (χ : PrimitiveCharacter d) (pp : ℕ × ℕ) (s : ℂ) : ℂ

The literal term integrand inside chen1973Lemma6Eq21VerticalIntegral. The finite character value is retained, rather than factored out before the contour deformation.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21TermShiftIntegrand x d χ pp s = ↑χ ↑(pp.1 * pp.2) * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21ShiftIntegrand x d χ (↑x / (↑pp.1 * ↑pp.2)) s

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_verticalIntegral_eq_termShift (x d : ℕ) (χ : PrimitiveCharacter d) (pp : ℕ × ℕ) : chen1973Lemma6Eq21VerticalIntegral x d χ pp = ↑(1 / (2 * Real.pi)) * ∫ (t : ℝ), chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) t

The source vertical integral is exactly the left-line integral of the literal shifted term.

theorem AnalyticNumberTheory.LargeSieve.differentiableOn_chen1973Lemma6Eq21TermShiftIntegrand_strip {x L B k m l₂ d : ℕ} {c : ℝ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) (hzero : Chen1973Lemma6Eq21ZeroFreeInput x L c) (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) : DifferentiableOn ℂ (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) {s : ℂ | chen1973Lemma6Eq21Sigma x ≤ s.re ∧ s.re ≤ chen1973Lemma6Alpha x}

The literal term is holomorphic on the same strip.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_term_finite_contour_shift {x L B k m l₂ d : ℕ} {c T : ℝ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) (hzero : Chen1973Lemma6Eq21ZeroFreeInput x L c) (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) : (∫ (t : ℝ) in -T..T, chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Alpha x) t) - ∫ (t : ℝ) in -T..T, chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) t = Complex.I * chen1973HorizontalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T

Actual finite contour-shift equality for one literal equation-(21) term.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_term_full_contour_shift {x L B k m l₂ d : ℕ} {c C : ℝ} (P : Chen1973Lemma6Eq21SourceParameters x L B k m l₂) (hzero : Chen1973Lemma6Eq21ZeroFreeInput x L c) (hbridge : Chen1973Lemma6Eq21ZeroFreeContourBridge x L c) (hd : d ∈ chen1973Lemma6ConductorBlock x L 0) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) (hC : 0 ≤ C) (hleft : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x)) MeasureTheory.volume) (hright : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Alpha x)) MeasureTheory.volume) (hhoriz : ∀ (T : ℝ), 0 ≤ T → ‖chen1973HorizontalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T‖ ≤ C / (1 + T ^ 2)) : ∫ (t : ℝ), chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Alpha x) t = ∫ (t : ℝ), chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) t

Full-line contour shift for the literal term. The horizontal limit is paid through the existing C/(1+T²) infrastructure.