Chen 1973, equation (17): rigorous corrected-source kernel

The denominator printed in (17) remains |s| (1 + |s| / A)^N. The exact Mellin denominator does not dominate that printed expression with an absolute constant: the direct comparison costs (sqrt 2)^N.

This separate module therefore introduces the rigorous corrected-source denominator

|s| (1 + (|s| / A)^N).

For Re s ≥ 0 and N ≥ 2, the exact complex Mellin denominator dominates this corrected denominator with constant one. The fixed-power estimates below are coarse downstream weakenings and are not transcriptions of printed (17).

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

The rigorous corrected-source radial denominator. Unlike the printed kernel, the high power applies only to |s| / A. It has no conductor-level parameter.

Equations

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

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_one_add_radial_pow_le_complex_pow {A : ℝ} (hA : 0 < A) {s : ℂ} (hs : 0 ≤ s.re) {N : ℕ} (hN : 2 ≤ N) : 1 + (‖s‖ / A) ^ N ≤ ‖1 + s / ↑A‖ ^ N

On the right half-plane, the exact complex power dominates the corrected-source radial power once the integer exponent is at least two.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_mellinKernel_norm_le_correctedKernel {x : ℕ} (hx : 1 < x) {s : ℂ} (hs : 0 ≤ s.re) (horder : 2 ≤ chen1973PerronOrder ↑x + 1) : ‖chen1973MellinKernel (↑x) s‖ ≤ (chen1973Lemma6Eq17CorrectedKernel x s)⁻¹

The exact Mellin norm is bounded by the reciprocal corrected-source denominator with explicit constant one.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_correctedKernel_nonneg {x : ℕ} (hx : 1 < x) (s : ℂ) : 0 ≤ chen1973Lemma6Eq17CorrectedKernel x s

The corrected-source denominator is nonnegative everywhere.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_correctedKernel_pos {x : ℕ} (hx : 1 < x) {σ v : ℝ} (hσ : 0 < σ) : 0 < chen1973Lemma6Eq17CorrectedKernel x (↑σ + ↑v * Complex.I)

The corrected-source denominator is positive on every positive vertical line.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedKernel_reflection (x : ℕ) (a v : ℝ) : chen1973Lemma6Eq17CorrectedKernel x (↑a + -↑v * Complex.I) = chen1973Lemma6Eq17CorrectedKernel x (↑a + ↑v * Complex.I)

Reflection symmetry of the corrected-source denominator on vertical lines.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_correctedFactor_inv_le_rpow_21_div_10 {u : ℝ} (hu : 0 ≤ u) {N : ℕ} (hN : 3 ≤ N) : (1 + u ^ N)⁻¹ ≤ 2 / (1 + u ^ (21 / 10))

A normalized 21/10 weakening of the corrected high-power factor.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_correctedFactor_inv_le_fourth_power {u : ℝ} (hu : 0 ≤ u) {N : ℕ} (hN : 4 ≤ N) : (1 + u ^ N)⁻¹ ≤ 2 / (1 + u ^ 4)

A normalized fourth-power weakening of the corrected high-power factor.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_correctedFactor_vertical_inv_le_21_div_10 {x : ℕ} (hx : 3 ≤ x) (σ v : ℝ) (horder : 3 ≤ chen1973PerronOrder ↑x + 1) : (1 + (‖↑σ + ↑v * Complex.I‖ / chen1973PerronScale ↑x) ^ (chen1973PerronOrder ↑x + 1))⁻¹ ≤ 2 * Real.log ↑x ^ (231 / 100) / (1 + |v| ^ (21 / 10))

On a vertical line, the corrected factor weakens to the printed downstream 21/10 weight. The scale payment is kept explicitly as A^(21/10) = (log x)^(231/100).

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_correctedFactor_vertical_inv_le_fourth_power {x : ℕ} (hx : 3 ≤ x) (σ v : ℝ) (horder : 4 ≤ chen1973PerronOrder ↑x + 1) : (1 + (‖↑σ + ↑v * Complex.I‖ / chen1973PerronScale ↑x) ^ (chen1973PerronOrder ↑x + 1))⁻¹ ≤ 2 * Real.log ↑x ^ (22 / 5) / (1 + |v| ^ 4)

On a vertical line, the corrected factor weakens to the printed downstream fourth-power weight, with the explicit payment A^4 = (log x)^(22/5).