Chen 1973, Lemma 6, equation (17): kernel and scalar payments

This independent leaf records the literal 11/10 Perron scale, pointwise Cauchy decay of the denominator on both source lines, its half-line integral, and the elementary alpha/beta, reciprocal-log, and conductor-weight payments. All cutoffs and constants are explicit; no finite computation is used.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_perronScale_pos {x : ℕ} (hx : 1 < x) : 0 < chen1973PerronScale ↑x

The source scale is positive as soon as x > 1.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_one_le_norm_one_add_div {A : ℝ} (hA : 0 < A) {s : ℂ} (hs : 0 ≤ s.re) : 1 ≤ ‖1 + s / ↑A‖

On the closed right half-plane, the complex Mellin factor has norm at least one. This is the step that permits decreasing the exact exponent n+1 to the first power.

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

Since n+1 ≥ 1, the exact Mellin power dominates its first factor on the closed right half-plane.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_radial_le_sqrt_two_mul_complex {A : ℝ} (hA : 0 < A) {s : ℂ} (hs : 0 ≤ s.re) : 1 + ‖s‖ / A ≤ √2 * ‖1 + s / ↑A‖

Exact Euclidean comparison between the first radial factor and the complex factor. Squaring reduces the claim to (A - ‖s‖)^2 + 4 A re(s) ≥ 0.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_mellinKernel_norm_le_radial {x : ℕ} (hx : 1 < x) {s : ℂ} (hs : 0 ≤ s.re) : ‖chen1973MellinKernel (↑x) s‖ ≤ √2 ^ (chen1973PerronOrder ↑x + 1) / chen1973Lemma6Eq17Kernel x s

Comparison of the exact complex Mellin denominator with the literal source radial denominator. The factor sqrt 2 ^ N is the honest cost of replacing ‖1+s/A‖ by 1+‖s‖/A at the full source exponent N.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_one_le_log_and_order {x : ℕ} (hx : 3 ≤ x) : 1 ≤ Real.log ↑x ∧ 1 ≤ chen1973PerronOrder ↑x

The completely explicit cutoff x ≥ 3 gives both one logarithm and one unit of Perron order.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_perronScale_le_log_sq {x : ℕ} (hx : 3 ≤ x) : chen1973PerronScale ↑x ≤ Real.log ↑x ^ 2

At x ≥ 3, the literal scale (log x)^(11/10) is paid by (log x)^2.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_vertical_norm_sq (σ v : ℝ) : ‖↑σ + ↑v * Complex.I‖ ^ 2 = σ ^ 2 + v ^ 2

Exact Euclidean norm on a real vertical line.

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

The source denominator is strictly positive on every positive vertical line.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_cauchy_le_kernel {x : ℕ} (hx : 3 ≤ x) {σ v : ℝ} (_hσ : 0 < σ) (hσupper : σ ≤ 2) : 1 / 2 * σ * (1 + (v / chen1973PerronScale ↑x) ^ 2) ≤ chen1973Lemma6Eq17Kernel x (↑σ + ↑v * Complex.I)

Pointwise Cauchy decay furnished by the radial equation-(17) denominator. The harmless factor 2 covers both source lines (σ ≤ 2) at the explicit cutoff x ≥ 3.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_fixed_power_le_kernel {x p : ℕ} {s : ℂ} (hx : 1 < x) (hs : 1 / 2 ≤ ‖s‖) (hp0 : p ≠ 0) (hp : p ≤ chen1973PerronOrder ↑x + 1) : 1 / 2 * (1 + (‖s‖ / chen1973PerronScale ↑x) ^ p) ≤ chen1973Lemma6Eq17Kernel x s

Every fixed natural radial power up to the source order is retained by the exact equation-(17) kernel once ‖s‖ ≥ 1/2. This is the reusable tail weakening; unlike the old definition it does not discard the source power.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_rpow_21_div_10_le_kernel {x : ℕ} {s : ℂ} (hx : 1 < x) (hs : 1 / 2 ≤ ‖s‖) (horder : 3 ≤ chen1973PerronOrder ↑x + 1) : 1 / 4 * (1 + (‖s‖ / chen1973PerronScale ↑x) ^ (21 / 10)) ≤ chen1973Lemma6Eq17Kernel x s

The fixed v^(21/10) tail weakening needed after the equation-(19) second-moment bound. The explicit order threshold is exactly 3 ≤ N.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_fourth_power_le_kernel {x : ℕ} {s : ℂ} (hx : 1 < x) (hs : 1 / 2 ≤ ‖s‖) (horder : 4 ≤ chen1973PerronOrder ↑x + 1) : 1 / 2 * (1 + (‖s‖ / chen1973PerronScale ↑x) ^ 4) ≤ chen1973Lemma6Eq17Kernel x s

The fixed fourth-power tail weakening needed for the equation-(20) fourth moments, under the explicit threshold 4 ≤ N.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_kernel_inv_le_cauchy {x : ℕ} (hx : 3 ≤ x) {σ v : ℝ} (hσ : 0 < σ) (hσupper : σ ≤ 2) : (chen1973Lemma6Eq17Kernel x (↑σ + ↑v * Complex.I))⁻¹ ≤ 2 * σ⁻¹ * (1 + (v / chen1973PerronScale ↑x) ^ 2)⁻¹

Reciprocal form of the pointwise Cauchy majorant.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_integral_cauchy_envelope {a σ : ℝ} (ha : 0 < a) (hσ : 0 < σ) : ∫ (v : ℝ) in Set.Ioi 0, σ⁻¹ * (1 + (v / a) ^ 2)⁻¹ = Real.pi / 2 * a / σ

Exact half-line mass of the scalar Cauchy envelope.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_rpow_alpha {x : ℕ} (hx : 1 < x) : ↑x ^ chen1973Lemma6Alpha x = Real.exp 1 * ↑x

Exact source alpha exponent: x^alpha = e*x.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_rpow_beta {x : ℕ} (hx : 1 < x) : ↑x ^ chen1973Lemma6Beta x = Real.exp 1 * √↑x

Exact source beta exponent: x^beta = e*sqrt x.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_alpha_scalar_payment {x : ℕ} (hx : 3 ≤ x) : Real.pi / 2 * chen1973PerronScale ↑x / chen1973Lemma6Alpha x * ↑x ^ chen1973Lemma6Alpha x ≤ 6 * ↑x * Real.log ↑x ^ 2

The alpha-line Cauchy mass is paid by the printed x (log x)^2 coefficient, with the explicit constant 6.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_beta_scalar_payment {x : ℕ} (hx : 3 ≤ x) : Real.pi / 2 * chen1973PerronScale ↑x / chen1973Lemma6Beta x * ↑x ^ chen1973Lemma6Beta x ≤ 48 * ↑x ^ (3 / 2)

At the same explicit cutoff, the beta-line Cauchy mass (including the literal 11/10 scale) has the coarse auxiliary bound x^(3/2). This is not the printed x^(1/2) prefactor; the sharp beta comparison is proved in Equation17CorrectedAssembly. The constant 48 comes from pi/2<2, beta≥1/2, e<3, and log x ≤ 2 sqrt x; no finite scan is used.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_norm_reciprocal_log {y : ℝ} (hy : 1 < y) : ‖↑(Real.log y)⁻¹‖ = (Real.log y)⁻¹

The reciprocal logarithm appearing in the pair polynomial has exactly the expected complex norm when its source argument exceeds one.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_conductorWeight_nonneg (d : ℕ) : 0 ≤ |↑(ArithmeticFunction.moebius d)| * 3 ^ d.primeFactors.card / ↑d

Every literal conductor coefficient in (17) is nonnegative.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_conductorWeight_le_divisorSquare {d : ℕ} (hd : Squarefree d) : |↑(ArithmeticFunction.moebius d)| * 3 ^ d.primeFactors.card / ↑d ≤ ↑d.divisors.card ^ 2 / ↑d

Squarefree conductor weights are paid pointwise by the divisor-square weight.