AnalyticNumberTheory.LargeSieve.Duality

Dual quadratic-form identity

The central Parseval/tensor-product step in Montgomery's additive large-sieve proof expands the square sum of T(n) = Σ_{x∈X} star(e(nx))·b_x into a quadratic form with coefficients b_x·star(b_y) and kernel Σ_n star(e(n(x−y))):

Σ_n |T(n)|² = Σ_x Σ_y b_x·star(b_y)·Σ_n star(e(n(x−y))).

The module proves three levels of this identity:

1. Finite-matrix expansion (dualExpansion): a purely algebraic identity for arbitrary φ : ι → κ → ℂ and b : κ → ℂ, with no character hypotheses.
2. Real additive-character version (dualQuadraticIdentity): take φ n x = e(nx) and use star(e(nx))·e(ny) = star(e(n(x−y))) to reduce the kernel to Σ_n star(e(n(x−y))).
3. Shifted-interval version (dualQuadraticIdentity_Icc) for n ∈ (M, M+N], and circle version (dualQuadraticIdentity_circle) for charPow n x = e(nx) on AddCircle 1, matching MontgomeryLargeSieveDual.

The subsequent geometric-sum and Schur-test argument estimates the off-diagonal kernel entries by min(N, 1/(2·dist x y)). These are the kernel estimates used in the dual large-sieve argument; this module supplies the identities, not the sharp Montgomery bound.

References: Montgomery, "Topics in Multiplicative Number Theory" (1971), Ch. 1; Iwaniec & Kowalski, "Analytic Number Theory" (2004), Ch. 7.

1. Finite-matrix expansion

theorem AnalyticNumberTheory.LargeSieve.normSq_sum_eq_sum_mul_star {ι : Type u_1} (s : Finset ι) (c : ι → ℂ) : ↑‖∑ x ∈ s, c x‖ ^ 2 = ∑ x ∈ s, ∑ y ∈ s, c x * star (c y)

Expansion of |Σ_x c_x|² as Σ_x Σ_y c_x·star(c_y).

theorem AnalyticNumberTheory.LargeSieve.dualExpansion {ι : Type u_1} {κ : Type u_2} (s : Finset ι) (t : Finset κ) (φ : ι → κ → ℂ) (b : κ → ℂ) : ↑(∑ n ∈ s, ‖∑ x ∈ t, star (φ n x) * b x‖ ^ 2) = ∑ x ∈ t, ∑ y ∈ t, b x * star (b y) * ∑ n ∈ s, star (φ n x) * φ n y

Dual quadratic-form expansion (finite matrices): for arbitrary φ : ι → κ → ℂ and b : κ → ℂ,

Σ_n |Σ_x star(φ n x)·b_x|² = Σ_x Σ_y b_x·star(b_y)·(Σ_n star(φ n x)·φ n y).

This is the algebraic foundation of Montgomery's dual large-sieve argument: the left side sums over n, while the right side is regrouped by x, y. The kernel Σ_n star(φ n x)·φ n y is the object to be estimated.

2. Real additive-character version

theorem AnalyticNumberTheory.LargeSieve.charReal_cross (n : ℤ) (x y : ℝ) : star (charReal (↑n * x)) * charReal (↑n * y) = star (charReal (↑n * (x - y)))

Character cross-product identity: star(e(nx))·e(ny) = star(e(n(x−y))) (n : ℤ).

theorem AnalyticNumberTheory.LargeSieve.dualQuadraticIdentity (s : Finset ℤ) (t : Finset ℝ) (b : ℝ → ℂ) : ↑(∑ n ∈ s, ‖∑ x ∈ t, star (charReal (↑n * x)) * b x‖ ^ 2) = ∑ x ∈ t, ∑ y ∈ t, b x * star (b y) * ∑ n ∈ s, star (charReal (↑n * (x - y)))

Dual quadratic-form identity (real additive characters): take φ n x = e(nx).

Σ_n |Σ_x star(e(nx))·b_x|² = Σ_x Σ_y b_x·star(b_y)·Σ_n star(e(n(x−y))).

theorem AnalyticNumberTheory.LargeSieve.dualQuadraticIdentity_Icc (M : ℤ) (N : ℕ) (t : Finset ℝ) (b : ℝ → ℂ) : ↑(∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖∑ x ∈ t, star (charReal (↑n * x)) * b x‖ ^ 2) = ∑ x ∈ t, ∑ y ∈ t, b x * star (b y) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), star (charReal (↑n * (x - y)))

Dual quadratic-form identity (shifted interval): expand the dual form for n ∈ (M, M+N].

3. Circle version (AddCircle 1)

theorem AnalyticNumberTheory.LargeSieve.charPow_star (n : ℤ) (x : AddCircle 1) : star ↑(charPow n x) = ↑(charPow (-n) x)

Conjugation of a circle character: star(e(nx)) = e(−nx) (n : ℤ, x : AddCircle 1).

theorem AnalyticNumberTheory.LargeSieve.unitChar_add (a b : AddCircle 1) : ↑(unitChar (a + b)) = ↑(unitChar a) * ↑(unitChar b)

Circle-character product: (unitChar (a + b) : ℂ) = (unitChar a : ℂ) * (unitChar b : ℂ).

theorem AnalyticNumberTheory.LargeSieve.charPow_cross (n : ℤ) (x y : AddCircle 1) : star ↑(charPow n x) * ↑(charPow n y) = star ↑(charPow n (x - y))

Circle-character cross-product identity: star(e(nx))·e(ny) = star(e(n(x−y))) (n : ℤ, x y : AddCircle 1).

theorem AnalyticNumberTheory.LargeSieve.dualQuadraticIdentity_circle (M : ℤ) (N : ℕ) (X : Finset (AddCircle 1)) (b : AddCircle 1 → ℂ) : ↑(∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖∑ x ∈ X, star ↑(charPow n x) * b x‖ ^ 2) = ∑ x ∈ X, ∑ y ∈ X, b x * star (b y) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), star ↑(charPow n (x - y))

Dual quadratic-form identity (circle): the Parseval expansion matching MontgomeryLargeSieveDual, with kernel Σ_n star(e(n(x−y))).