Chen 1973, Lemma 6, equation (17): alpha-line log-derivative bridge

This module moves the exact finite ActualPhi identity from the unconditional Re s = 2 Bromwich representation to Chen's line Re s = alpha = 1 + 1 / log x, identifies the von Mangoldt series with -L'/L, and lifts the identity through the finite pair, primitive-character, and conductor-block sums. It does not assume an equation-(17) majorization or any later assembly conclusion.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock_one_lt {x L level d : ℕ} (hlevel : 1 ≤ level) (hd : d ∈ chen1973Lemma6ConductorBlock x L level) : 1 < d

Conductors in a positive-level Chen block are greater than one.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi_eq_negLogDerivIntegral_alpha {x d : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (_hχ : ↑χ ≠ 1) (hx : 3 ≤ x) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) : chen1973Lemma6ActualPhi x d χ pp = ↑(1 / (2 * Real.pi)) * ∫ (t : ℝ), -deriv (DirichletCharacter.LFunction ↑χ) (↑(chen1973Lemma6Alpha x) + ↑t * Complex.I) / DirichletCharacter.LFunction (↑χ) (↑(chen1973Lemma6Alpha x) + ↑t * Complex.I) * ((↑↑x / (↑↑pp.1 * ↑pp.2)) ^ (↑(chen1973Lemma6Alpha x) + ↑t * Complex.I) * chen1973MellinKernel (↑x) (↑(chen1973Lemma6Alpha x) + ↑t * Complex.I))

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivIntegrand (x d : ℕ) (χ : PrimitiveCharacter d) (pp : ℕ × ℕ) (t : ℝ) : ℂ

The totalized alpha-line -L'/L integrand. On the conductor range 1 < d, the totalized values reduce definitionally to the primitive Dirichlet L-function and its derivative.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivIntegrand x d χ pp t = -AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv d (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑t * Complex.I) χ / AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue d (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑t * Complex.I) χ * ((↑↑x / (↑↑pp.1 * ↑pp.2)) ^ (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑t * Complex.I) * AnalyticNumberTheory.LargeSieve.chen1973MellinKernel (↑x) (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑t * Complex.I))

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

The normalized full alpha-line transform for one primitive character and one prime pair. The factor is exactly 1/(2π) and the logarithmic derivative has the source sign -L'/L.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivIntegral x d χ pp = ↑(1 / (2 * Real.pi)) * ∫ (t : ℝ), AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivIntegrand x d χ pp t

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi_eq_alphaNegLogDerivIntegral {x d : ℕ} (χ : PrimitiveCharacter d) (hd : 1 < d) (hx : 3 ≤ x) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) : chen1973Lemma6ActualPhi x d χ pp = chen1973Lemma6AlphaNegLogDerivIntegral x d χ pp

Totalized form of the exact alpha-line bridge, suitable for finite sums.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivPrimePairSum (x d B k m : ℕ) (χ : PrimitiveCharacter d) : ℂ

Finite prime-pair lift of the alpha-line bridge.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivPrimePairSum x d B k m χ = ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivIntegral x d χ pp * ↑χ ↑(pp.1 * pp.2)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairSum_eq_alphaNegLogDeriv {x d B k m : ℕ} (χ : PrimitiveCharacter d) (hd : 1 < d) (hx : 3 ≤ x) : ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2) = chen1973Lemma6AlphaNegLogDerivPrimePairSum x d B k m χ

The actual finite pair sum is exactly its alpha-line -L'/L lift.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivCharacterSum (x d B k m : ℕ) : ℂ

The finite primitive-character lift on one conductor.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivCharacterSum x d B k m = ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, star (↑χ ↑x) * AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivPrimePairSum x d B k m χ

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6CharacterSum_eq_alphaNegLogDeriv {x d B k m : ℕ} (hd : 1 < d) (hx : 3 ≤ x) : ∑ χ : PrimitiveCharacter d, star (↑χ ↑x) * ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2) = chen1973Lemma6AlphaNegLogDerivCharacterSum x d B k m

The actual finite primitive-character sum is exactly its alpha-line -L'/L lift.

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

The conductor-block alpha-line expression, with the exact equation-(17) weight and norm retained.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlockAlphaNegLogDeriv x L level B k m = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, |↑(ArithmeticFunction.moebius d)| * 3 ^ d.primeFactors.card / ↑d * ‖AnalyticNumberTheory.LargeSieve.chen1973Lemma6AlphaNegLogDerivCharacterSum x d B k m‖

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlockActual_eq_alphaNegLogDeriv {x L level B k m : ℕ} (hlevel : 1 ≤ level) (hx : 3 ≤ x) : chen1973Lemma6NmBlockActual x L level B k m = chen1973Lemma6NmBlockAlphaNegLogDeriv x L level B k m

Exact conductor-block lift. The positive level hypothesis is used only to show that each conductor in the block is greater than one, hence every primitive character in the block is nonprincipal.