AnalyticNumberTheory.LargeSieve.Additive

Additive large sieve (Montgomery 1971)

For a δ-well-spaced set of points {x_r} modulo 1 and any finitely supported complex sequence a_n,

Σ_r |Σ_{M<n≤M+N} a_n e(n x_r)|² ≤ (N + 1/δ) · Σ_{M<n≤M+N} |a_n|²,

where e(x) = exp(2πix). This is a basic analytic input to the Bombieri--Vinogradov theorem and the weighted Pan mean-value theorem (PanMeanValueUniform); the multiplicative and arithmetic large sieves are consequences of it.

This module has three parts:

1. Representation: the standard additive character unitChar x = exp(2πix) on AddCircle 1 (mathlib's AddCircle.toCircle), the interval exponential sum circleCharSum, and wellSpaced (δ-separation in the distance modulo 1).
2. Target statements: MontgomeryLargeSievePrimal and MontgomeryLargeSieveDual are quantified propositions. This module defines these targets rather than proving either large-sieve bound.
3. Duality lemma: for any finite matrix A and constant C ≥ 0, the primal bound (for every a) is equivalent to the dual bound (for every b) (largeSieveDuality). This is the algebraic foundation of the large-sieve argument: Montgomery's original proof starts with the dual form (geometric-sum bounds and the Schur test), and duality preserves the constant. The dual form uses the conjugate transpose (star (A i j)); the classical e(nx) formulation follows equivalently by conjugating b and reversing the sign of n.

References:

• Montgomery, H.L. (1971), "Topics in Multiplicative Number Theory"
• Iwaniec & Kowalski, "Analytic Number Theory" (2004), Ch. 7
• Halberstam & Richert, "Sieve Methods" (1974), Ch. 9-10

1. Additive characters and exponential sums on the circle modulo 1

noncomputable def AnalyticNumberTheory.LargeSieve.unitChar (x : AddCircle 1) : Circle

e(x) = exp(2πix): the standard additive character on AddCircle 1 (mathlib's AddCircle.toCircle; see AddCircle.toCircle_apply_mk).

Equations

• AnalyticNumberTheory.LargeSieve.unitChar x = x.toCircle

noncomputable def AnalyticNumberTheory.LargeSieve.charPow (n : ℤ) (x : AddCircle 1) : Circle

e(nx) = e(x)^n (n : ℤ): compatibility of the character with integer multiplication (AddCircle.toCircle_zsmul).

Equations

• AnalyticNumberTheory.LargeSieve.charPow n x = AnalyticNumberTheory.LargeSieve.unitChar (n • x)

noncomputable def AnalyticNumberTheory.LargeSieve.circleCharSum (M : ℤ) (N : ℕ) (a : ℤ → ℂ) (x : AddCircle 1) : ℂ

The weighted exponential sum Σ_{M<n≤M+N} a_n e(nx) on (M, M+N].

Equations

• AnalyticNumberTheory.LargeSieve.circleCharSum M N a x = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * ↑(AnalyticNumberTheory.LargeSieve.charPow n x)

noncomputable def AnalyticNumberTheory.LargeSieve.wellSpaced (X : Finset (AddCircle 1)) (δ : ℝ) : Prop

X ⊆ AddCircle 1 is δ-well-spaced: any two distinct points have distance modulo 1 at least δ.

Equations

• AnalyticNumberTheory.LargeSieve.wellSpaced X δ = ∀ ⦃x : AddCircle 1⦄, x ∈ X → ∀ ⦃y : AddCircle 1⦄, y ∈ X → x ≠ y → δ ≤ dist x y

2. Additive large-sieve target statements

def AnalyticNumberTheory.LargeSieve.MontgomeryLargeSievePrimal (M : ℤ) (N : ℕ) : Prop

Additive large sieve (Montgomery, primal form): for a δ-well-spaced set X and any finitely supported complex sequence a : ℤ → ℂ,

Σ_{x∈X} |Σ_{M<n≤M+N} a_n e(nx)|² ≤ (N + 1/δ) · Σ_{M<n≤M+N} |a_n|².

This is a target proposition, not a bound proved here. The classical proof uses the dual form, a geometric-sum bound, and the Schur test.

Equations

• AnalyticNumberTheory.LargeSieve.MontgomeryLargeSievePrimal M N = ∀ (δ : ℝ), 0 < δ → ∀ (X : Finset (AddCircle 1)), AnalyticNumberTheory.LargeSieve.wellSpaced X δ → ∀ (a : ℤ → ℂ), ∑ x ∈ X, ‖AnalyticNumberTheory.LargeSieve.circleCharSum M N a x‖ ^ 2 ≤ (↑N + 1 / δ) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖a n‖ ^ 2

def AnalyticNumberTheory.LargeSieve.MontgomeryLargeSieveDual (M : ℤ) (N : ℕ) : Prop

Dual additive large sieve (defined using the conjugate transpose):

Σ_{M<n≤M+N} |Σ_{x∈X} conj(e(nx))·b_x|² ≤ (N + 1/δ) · Σ_{x∈X} |b_x|².

In the classical formulation, conj(e(nx)) is written as e(-nx); conjugating b gives the equivalent form with the opposite sign in the exponential.

Equations

• AnalyticNumberTheory.LargeSieve.MontgomeryLargeSieveDual M N = ∀ (δ : ℝ), 0 < δ → ∀ (X : Finset (AddCircle 1)), AnalyticNumberTheory.LargeSieve.wellSpaced X δ → ∀ (b : AddCircle 1 → ℂ), ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖∑ x ∈ X, star ↑(AnalyticNumberTheory.LargeSieve.charPow n x) * b x‖ ^ 2 ≤ (↑N + 1 / δ) * ∑ x ∈ X, ‖b x‖ ^ 2

3. Duality lemma (the algebraic foundation of the large sieve)

theorem AnalyticNumberTheory.LargeSieve.realCauchySchwarz {ι : Type u_1} (s : Finset ι) (a b : ι → ℝ) : (∑ i ∈ s, a i * b i) ^ 2 ≤ (∑ i ∈ s, a i ^ 2) * ∑ i ∈ s, b i ^ 2

Real Cauchy--Schwarz (Finset): (Σ aᵢbᵢ)² ≤ (Σ aᵢ²)(Σ bᵢ²). This is Mathlib's finite-sum Cauchy--Schwarz inequality.

theorem AnalyticNumberTheory.LargeSieve.complexCauchySchwarz {ι : Type u_1} (s : Finset ι) (x y : ι → ℂ) : ‖∑ i ∈ s, x i * star (y i)‖ ≤ √(∑ i ∈ s, ‖x i‖ ^ 2) * √(∑ i ∈ s, ‖y i‖ ^ 2)

Complex Cauchy--Schwarz (Finset): |Σᵢ xᵢ·conj(yᵢ)| ≤ √(Σ‖xᵢ‖²)·√(Σ‖yᵢ‖²), proved using the triangle inequality and real Cauchy--Schwarz.

theorem AnalyticNumberTheory.LargeSieve.largeSieveDuality_primalToDual {ι : Type u_1} {κ : Type u_2} (s : Finset ι) (t : Finset κ) (A : ι → κ → ℂ) {C : ℝ} (hC : 0 ≤ C) (hPrimal : ∀ (a : κ → ℂ), ∑ i ∈ s, ‖∑ j ∈ t, A i j * a j‖ ^ 2 ≤ C * ∑ j ∈ t, ‖a j‖ ^ 2) (b : ι → ℂ) : ∑ j ∈ t, ‖∑ i ∈ s, star (A i j) * b i‖ ^ 2 ≤ C * ∑ i ∈ s, ‖b i‖ ^ 2

Large-sieve duality lemma (finite matrices): for any A : ι → κ → ℂ and C ≥ 0, the primal bound Σᵢ |Σⱼ Aᵢⱼ aⱼ|² ≤ C·Σⱼ |aⱼ|² (∀a) is equivalent to the conjugate-transpose dual bound Σⱼ |Σᵢ conj(Aᵢⱼ) bᵢ|² ≤ C·Σᵢ |bᵢ|² (∀b).

Proof (Montgomery's classical argument): put v = A*b (bStar). Then ‖A*b‖² = |⟨b, A A*b⟩| ≤ ‖A A*b‖·‖b‖ ≤ √C·‖A*b‖·‖b‖. The primal bound applied to v and complex Cauchy--Schwarz give ‖A*b‖ ≤ √C·‖b‖. The converse follows symmetrically from A** = A (star (star A) = A).

theorem AnalyticNumberTheory.LargeSieve.largeSieveDuality {ι : Type u_1} {κ : Type u_2} (s : Finset ι) (t : Finset κ) (A : ι → κ → ℂ) {C : ℝ} (hC : 0 ≤ C) : (∀ (a : κ → ℂ), ∑ i ∈ s, ‖∑ j ∈ t, A i j * a j‖ ^ 2 ≤ C * ∑ j ∈ t, ‖a j‖ ^ 2) ↔ ∀ (b : ι → ℂ), ∑ j ∈ t, ‖∑ i ∈ s, star (A i j) * b i‖ ^ 2 ≤ C * ∑ i ∈ s, ‖b i‖ ^ 2

Large-sieve duality lemma: equivalence of the primal and dual forms. For the converse, replace A by its conjugate transpose and use star (star x) = x to recover the primal form.

theorem AnalyticNumberTheory.LargeSieve.montgomeryDuality (M : ℤ) (N : ℕ) : MontgomeryLargeSievePrimal M N ↔ MontgomeryLargeSieveDual M N

Additive large sieve: primal ⟺ dual. Apply the general duality lemma to the character matrix A x n = e(nx) with C = N + 1/δ. Thus the two target statements are equivalent: proving either one gives the other.