Pan--Wang--Ding Theorem A and the dyadic cover in (2.13)

This leaf isolates two finite deductions used on pp. 600--604 of Pan--Wang-- Ding (1975). First, the usual q / φ(q) primitive large sieve implies the sharp Theorem A scale Q + N / P on a dyadic conductor interval. Second, the two open-left, closed-right dyadic partitions used in (2.13) really cover the whole conductor and source rectangles. The triangle inequality is applied only after each complete source block has been summed; it is never pushed inside the a-sum.

The sharp dyadic form of Theorem A

def AnalyticNumberTheory.LargeSieve.PanWeightedPrimitiveLargeSieve (C : ℝ) : Prop

A convenient explicit form of the standard weighted primitive large-sieve input. The constant C is absolute; this definition merely records the exact N + Q² scale needed below.

Equations

• AnalyticNumberTheory.LargeSieve.PanWeightedPrimitiveLargeSieve C = (0 ≤ C ∧ ∀ (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ), 0 < Q → ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.primitiveIntervalAmplitude b M N χ‖ ^ 2 ≤ C * (↑N + ↑Q ^ 2) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2)

theorem AnalyticNumberTheory.LargeSieve.panTheoremALeft_le_sharp_dyadic {C : ℝ} (hLS : PanWeightedPrimitiveLargeSieve C) (b : ℤ → ℂ) (M : ℤ) (N P Q : ℕ) (hP : 0 < P) (hPQ : P < Q) (hQP : Q ≤ 2 * P) : panTheoremALeft b M N P Q ≤ 2 * C * (↑Q + ↑N / ↑P) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

Pan--Wang--Ding Theorem A, sharp dyadic scale.

On P < q ≤ Q ≤ 2P, write 1/φ(q) = (1/q)(q/φ(q)) and use 1/q ≤ 1/P. Thus the standard N + Q² weighted primitive large sieve gives an absolute multiple of N/P + Q; the displayed constant is 2C.

The complete dyadic cover used in (2.13)

def AnalyticNumberTheory.LargeSieve.panDyadicDepth (R Q : ℕ) : ℕ

Number of open-left dyadic cells required to cover (R,Q].

Equations

• AnalyticNumberTheory.LargeSieve.panDyadicDepth R Q = Nat.log 2 (Q / R) + 1

def AnalyticNumberTheory.LargeSieve.panDyadicCell (R Q j : ℕ) : Finset ℕ

The j-th open-left, closed-right dyadic cell, clipped only at the final paper endpoint.

Equations

• AnalyticNumberTheory.LargeSieve.panDyadicCell R Q j = Finset.Ioc (R * 2 ^ j) (min (2 * (R * 2 ^ j)) Q)

theorem AnalyticNumberTheory.LargeSieve.mem_panDyadicCell_of_mem_Ioc {R Q x : ℕ} (hR : 0 < R) (hx : x ∈ Finset.Ioc R Q) : ∃ j ∈ Finset.range (panDyadicDepth R Q), x ∈ panDyadicCell R Q j

Every point of (R,Q] lies in one of the advertised dyadic cells.

theorem AnalyticNumberTheory.LargeSieve.panDyadicCells_cover (R Q : ℕ) (hR : 0 < R) : (Finset.range (panDyadicDepth R Q)).biUnion (panDyadicCell R Q) = Finset.Ioc R Q

The cells cover the whole interval, including the last clipped cell.

theorem AnalyticNumberTheory.LargeSieve.panDyadicCells_pairwise (R Q : ℕ) (_hR : 0 < R) : (↑(Finset.range (panDyadicDepth R Q))).PairwiseDisjoint (panDyadicCell R Q)

Distinct dyadic cells are disjoint.

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

The clipped (j,k) block used to state the exact finite form of (2.13). The norm remains outside the complete source sum in its k-cell.

Equations

• AnalyticNumberTheory.LargeSieve.panIymDyadicCoveredBlock g d y D₁ D A₁ A₂ j k = ∑ q ∈ AnalyticNumberTheory.LargeSieve.panDyadicCell D₁ D j, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude g d y (A₁ * 2 ^ k) (min (2 * (A₁ * 2 ^ k)) A₂) χ‖

theorem AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude_eq_sum_dyadicCells (g d : ℕ → ℂ) (y A₁ A₂ : ℕ) (hA₁ : 0 < A₁) {q : ℕ} (χ : PrimitiveCharacter q) : panSourceCharacterAmplitude g d y A₁ A₂ χ = ∑ k ∈ Finset.range (panDyadicDepth A₁ A₂), panSourceCharacterAmplitude g d y (A₁ * 2 ^ k) (min (2 * (A₁ * 2 ^ k)) A₂) χ

The complete a-sum is the sum of its dyadic source blocks.

theorem AnalyticNumberTheory.LargeSieve.panIymHigh_le_sum_dyadicCoveredBlocks (g d : ℕ → ℂ) (y A₁ A₂ D₁ D : ℕ) (hA₁ : 0 < A₁) (hD₁ : 0 < D₁) : panIymHigh g d y A₁ A₂ D₁ D ≤ ∑ j ∈ Finset.range (panDyadicDepth D₁ D), ∑ k ∈ Finset.range (panDyadicDepth A₁ A₂), panIymDyadicCoveredBlock g d y D₁ D A₁ A₂ j k

Equation (2.13), complete finite dyadic block inequality.

The conductor cells are disjoint, while the source decomposition uses one triangle inequality per character after summing every a in a full source cell. This is exactly the absolute-value level in the paper.