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

Assembly-facing alias for the rigorous corrected-source kernel. The conductor level is retained only to keep the equation-(17) integral API aligned with the surrounding block notation.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialKernel x _level s = AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedKernel x s

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

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialFirstIntegral 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.chen1973Lemma6Eq17CorrectedRadialKernel x level (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑v * Complex.I)

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

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialSecondIntegral 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.chen1973Lemma6Eq17CorrectedRadialKernel x level (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) + ↑v * Complex.I)

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

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialFirstFullIntegral x L level B k m H = ∫ (v : ℝ), AnalyticNumberTheory.LargeSieve.chen1973Lemma6A x L level B k m H (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑v * Complex.I) / AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialKernel x level (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑v * Complex.I)

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

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialSecondFullIntegral x L level B k m H = ∫ (v : ℝ), AnalyticNumberTheory.LargeSieve.chen1973Lemma6B x L level B k m H (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) + ↑v * Complex.I) / AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialKernel x level (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) + ↑v * Complex.I)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialFirstFullIntegral_eq_two_mul_half {x L level B k m H : ℕ} (hlevel : 1 ≤ level) (hx : 1 < x) : chen1973Lemma6Eq17CorrectedRadialFirstFullIntegral x L level B k m H = 2 * chen1973Lemma6Eq17CorrectedRadialFirstIntegral x L level B k m H

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialSecondFullIntegral_eq_two_mul_half {x L level B k m H : ℕ} (hlevel : 1 ≤ level) (hx : 1 < x) : chen1973Lemma6Eq17CorrectedRadialSecondFullIntegral x L level B k m H = 2 * chen1973Lemma6Eq17CorrectedRadialSecondIntegral x L level B k m H

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

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Equation17CorrectedRadialRHS x L level B k m H = 12 * ↑x * Real.log ↑x ^ 2 * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialFirstIntegral x L level B k m H + 2 * ↑x ^ (1 / 2) * AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17CorrectedRadialSecondIntegral x L level B k m H

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

Equations

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

def AnalyticNumberTheory.LargeSieve.Chen1973Equation17AlphaLogDerivativePayment (x L level : ℕ) : Prop

The pointwise alpha-line logarithmic-derivative estimate paid by the external (log x)^2 factor in the corrected equation-(17) assembly. The explicit absolute constant 6 comes from the absolute twisted von Mangoldt series; the current source quantity A remains free of L'/L.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Equation17AlphaLogDerivativePayment x L level = ∀ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d) (t : ℝ), ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv d (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑t * Complex.I) χ / AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue d (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑t * Complex.I) χ‖ ≤ 6 * Real.log ↑x ^ 2

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_scaledKernel_beta_le_source {x level : ℕ} (hx : 3 ≤ x) (t : ℝ) : ‖↑(1 / (2 * Real.pi)) * ↑x ^ (↑(chen1973Lemma6Beta x) + ↑t * Complex.I) * chen1973MellinKernel (↑x) (↑(chen1973Lemma6Beta x) + ↑t * Complex.I)‖ ≤ ↑x ^ (1 / 2) / chen1973Lemma6Eq17CorrectedRadialKernel x level (↑(chen1973Lemma6Beta x) + ↑t * Complex.I)

The original beta-line prefactor is sqrt x (Chen p.121).

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_alphaLogDerivative_le_six_mul_log_sq {x d : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (hd : 1 < d) (hx : 3 ≤ x) (t : ℝ) : ‖chen1973PrimitiveLDeriv d (↑(chen1973Lemma6Alpha x) + ↑t * Complex.I) χ / chen1973Lemma6PrimitiveLValue d (↑(chen1973Lemma6Alpha x) + ↑t * Complex.I) χ‖ ≤ 6 * Real.log ↑x ^ 2

On Chen's alpha line, the absolute twisted von Mangoldt series pays the logarithmic derivative with the explicit universal constant 6.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_corrected_radial_contourMajorization {x L level B k m H : ℕ} (hx : 3 ≤ x) (hlevel : 1 ≤ level) (hAlpha : Chen1973Equation17AlphaLogDerivativePayment x L level) : Chen1973Equation17CorrectedRadialContourMajorization x L level B k m H

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation17_corrected_radial {x L level B k m H : ℕ} (hx : 3 ≤ x) (hlevel : 1 ≤ level) (hAlpha : Chen1973Equation17AlphaLogDerivativePayment x L level) : chen1973Lemma6NmBlockActual x L level B k m ≤ 12 * ↑x * Real.log ↑x ^ 2 * chen1973Lemma6Eq17CorrectedRadialFirstIntegral x L level B k m H + 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq17CorrectedRadialSecondIntegral x L level B k m H

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation17_alphaLogDerivativePayment_unconditional {x L level : ℕ} (hx : 3 ≤ x) (hlevel : 1 ≤ level) : Chen1973Equation17AlphaLogDerivativePayment x L level

The alpha-line payment is unconditional: absolute convergence of the -L'/L von Mangoldt series supplies the explicit coefficient 6.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation17_corrected_radial_unconditional {x L level B k m H : ℕ} (hx : 3 ≤ x) (hlevel : 1 ≤ level) : chen1973Lemma6NmBlockActual x L level B k m ≤ 12 * ↑x * Real.log ↑x ^ 2 * chen1973Lemma6Eq17CorrectedRadialFirstIntegral x L level B k m H + 2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq17CorrectedRadialSecondIntegral x L level B k m H

Unconditional corrected equation-(17) assembly. The source A remains unchanged; the absolute alpha-line logarithmic derivative is paid only in the first displayed coefficient.