Pan--Wang--Ding (1975), early source reductions

This module records the first literal finite objects in the proof of Theorem 2 on pp. 600--602. In particular, the absolute value in (2.7), (2.10), (2.11), and (2.14) surrounds the complete a-sum. No termwise absolute majorant is introduced here.

The paper's Theorem A (2.1) has the sharper classical factor Q + N / P (up to an absolute constant). The first theorem below only connects its literal left side to the unconditional reduced-Farey large-sieve factor currently proved in production; it does not rename that weaker factor as the paper's source estimate.

Theorem A, equation (2.1): literal left side

noncomputable def AnalyticNumberTheory.LargeSieve.panTheoremALeft (b : ℤ → ℂ) (M : ℤ) (N P Q : ℕ) : ℝ

The literal primitive-character square ledger on P < q ≤ Q occurring on the left of Pan--Wang--Ding Theorem A (2.1).

Equations

• AnalyticNumberTheory.LargeSieve.panTheoremALeft b M N P Q = ∑ q ∈ Finset.Ioc P Q, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.primitiveIntervalAmplitude b M N χ‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.panTheoremALeft_le_productionFareyBound (b : ℤ → ℂ) (M : ℤ) (N P Q : ℕ) (hP : 0 < P) (hPQ : P < Q) : panTheoremALeft b M N P Q ≤ largeSieveBound N (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

Exact production bridge for the literal (2.1) ledger. The source weight 1 / φ(q) is first increased to q / φ(q) and only then is the proved primitive Gauss--Farey large sieve invoked.

Equations (2.7), (2.9)--(2.11), and the literal (2.14) cell

noncomputable def AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude {q : ℕ} (g d : ℕ → ℂ) (y A₁ A₂ : ℕ) (χ : PrimitiveCharacter q) : ℂ

The complete source/product character amplitude inside the absolute value in (2.7). The inner cutoff depends on a, and cancellation across the whole outer a-sum is retained.

Equations

• AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude g d y A₁ A₂ χ = ∑ a ∈ Finset.Ioc A₁ A₂, g a * ↑χ ↑a * ∑ n ∈ Finset.Icc 1 (y / a), d n * ↑χ ↑n

noncomputable def AnalyticNumberTheory.LargeSieve.panIym (g d : ℕ → ℂ) (y A₁ A₂ D : ℕ) : ℝ

Pan--Wang--Ding (2.7), with the absolute value outside the complete a-sum.

Equations

• AnalyticNumberTheory.LargeSieve.panIym g d y A₁ A₂ D = ∑ q ∈ Finset.Icc 1 D, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude g d y A₁ A₂ χ‖

noncomputable def AnalyticNumberTheory.LargeSieve.panIymLow (g d : ℕ → ℂ) (y A₁ A₂ D₁ : ℕ) : ℝ

The low-conductor term (2.10).

Equations

• AnalyticNumberTheory.LargeSieve.panIymLow g d y A₁ A₂ D₁ = ∑ q ∈ Finset.Icc 1 D₁, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude g d y A₁ A₂ χ‖

noncomputable def AnalyticNumberTheory.LargeSieve.panIymHigh (g d : ℕ → ℂ) (y A₁ A₂ D₁ D : ℕ) : ℝ

The high-conductor term (2.11).

Equations

• AnalyticNumberTheory.LargeSieve.panIymHigh g d y A₁ A₂ D₁ D = ∑ q ∈ Finset.Ioc D₁ D, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude g d y A₁ A₂ χ‖

theorem AnalyticNumberTheory.LargeSieve.panIym_eq_low_add_high (g d : ℕ → ℂ) (y A₁ A₂ D₁ D : ℕ) (hD : D₁ ≤ D) : panIym g d y A₁ A₂ D = panIymLow g d y A₁ A₂ D₁ + panIymHigh g d y A₁ A₂ D₁ D

Exact low/high conductor partition (2.9).

noncomputable def AnalyticNumberTheory.LargeSieve.panIymDyadicBlock (g d : ℕ → ℂ) (y D₁ A₁ j k : ℕ) : ℝ

Literal dyadic block (2.14). Both the modulus cell and source cell are left explicit, and the norm still surrounds the complete source sum.

Equations

• AnalyticNumberTheory.LargeSieve.panIymDyadicBlock g d y D₁ A₁ j k = ∑ q ∈ Finset.Ioc (2 ^ j * D₁) (2 ^ (j + 1) * D₁), (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude g d y (2 ^ k * A₁) (2 ^ (k + 1) * A₁) χ‖