Chen 1973, Lemma 6, equation (17): finite Bromwich sums

This module closes the finite-sum part of the passage to (17). It proves that Chen's actual finite Φ is a Bochner integral over the full real Bromwich line, exchanges that integral with the finite von-Mangoldt, prime-pair, and primitive character sums, and then records the resulting exact conductor-block identity. No equation-(17) majorization or contour-deformation conclusion is assumed.

theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973BromwichIntegrand {x y : ℝ} (hx : 1 < x) (hy : 0 < y) : MeasureTheory.Integrable (fun (t : ℝ) => chen1973BromwichIntegrand x y t) MeasureTheory.volume

The Bromwich integrand is Bochner integrable for every positive argument.

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

The literal finite von-Mangoldt/character integrand whose full-line integral is chen1973Lemma6ActualPhi. The normalization 1/(2π) is inside the integrand, so the result is a single Bochner integral.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6BromwichVonMangoldtIntegrand x d χ pp t = ∑ n ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma5NCarrier x pp, ↑(ArithmeticFunction.vonMangoldt n) * (↑(1 / (2 * Real.pi)) * AnalyticNumberTheory.LargeSieve.chen1973BromwichIntegrand (↑x) (↑x / (↑pp.1 * ↑pp.2 * ↑n)) t) * ↑χ ↑n

theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973Lemma6BromwichVonMangoldtTerm {x d n : ℕ} {pp : ℕ × ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) : MeasureTheory.Integrable (fun (t : ℝ) => ↑(ArithmeticFunction.vonMangoldt n) * (↑(1 / (2 * Real.pi)) * chen1973BromwichIntegrand (↑x) (↑x / (↑pp.1 * ↑pp.2 * ↑n)) t) * ↑χ ↑n) MeasureTheory.volume

Every summand in the finite von-Mangoldt Bromwich sum is Bochner integrable. The n=0 term vanishes; positive n use the closed Mellin integrability theorem.

theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973Lemma6BromwichVonMangoldtIntegrand {x d : ℕ} {pp : ℕ × ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) : MeasureTheory.Integrable (chen1973Lemma6BromwichVonMangoldtIntegrand x d χ pp) MeasureTheory.volume

The complete finite von-Mangoldt Bromwich integrand is Bochner integrable.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi_eq_integral_bromwichSum {x d : ℕ} {pp : ℕ × ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) : chen1973Lemma6ActualPhi x d χ pp = ∫ (t : ℝ), chen1973Lemma6BromwichVonMangoldtIntegrand x d χ pp t

chen1973Lemma6ActualPhi is exactly the full real-line integral of its finite von-Mangoldt twisted sum.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell_pos {x B k m : ℕ} {pp : ℕ × ℕ} (hpp : pp ∈ chen1973Lemma6PrimePairShell x B k m) : 0 < pp.1 ∧ 0 < pp.2

Membership in a source prime-pair shell forces both coordinates positive.

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

The prime-pair sum after moving its finite sum inside the Bromwich integral.

Equations

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

theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973Lemma6BromwichPrimePairIntegrand {x d B k m : ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) : MeasureTheory.Integrable (chen1973Lemma6BromwichPrimePairIntegrand x d B k m χ) MeasureTheory.volume

Every prime-pair integrand is Bochner integrable.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairSum_eq_integral_bromwichSum {x d B k m : ℕ} (χ : PrimitiveCharacter d) (hx : 1 < x) : ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))⁻¹ * chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2) = ∫ (t : ℝ), chen1973Lemma6BromwichPrimePairIntegrand x d B k m χ t

Exact finite prime-pair/integral exchange.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6BromwichCharacterIntegrand (x d B k m : ℕ) (t : ℝ) : ℂ

The complete primitive-character integrand for one conductor.

Equations

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

theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973Lemma6BromwichCharacterIntegrand {x d B k m : ℕ} (hx : 1 < x) : MeasureTheory.Integrable (chen1973Lemma6BromwichCharacterIntegrand x d B k m) MeasureTheory.volume

The finite primitive-character integrand is Bochner integrable.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6CharacterSum_eq_integral_bromwichSum {x d B k m : ℕ} (hx : 1 < 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) = ∫ (t : ℝ), chen1973Lemma6BromwichCharacterIntegrand x d B k m t

Exact exchange of the primitive-character sum with the full-line Bromwich integral.

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

The exact conductor-block expression after all finite sums have been moved inside their full-line Bromwich integrals. The conductor sum and norm remain outside, exactly as in the definition of N_m.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlockBromwich x L level B k m = ∑ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L level, |↑(ArithmeticFunction.moebius d)| * 3 ^ d.primeFactors.card / ↑d * ‖∫ (t : ℝ), AnalyticNumberTheory.LargeSieve.chen1973Lemma6BromwichCharacterIntegrand x d B k m t‖

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6NmBlockActual_eq_bromwich {x L level B k m : ℕ} (hx : 1 < x) : chen1973Lemma6NmBlockActual x L level B k m = chen1973Lemma6NmBlockBromwich x L level B k m

Exact conductor-block lift of the finite Bromwich identity. This is the finite-sum closure needed before any contour deformation toward equation (17), and it has no equation-(17) conclusion premise.