AnalyticNumberTheory.LargeSieve.Multiplicative

Multiplicative large sieve

The multiplicative step in the Pan mean-value argument starts from the additive large sieve (LargeSieve/WellSpaced.lean) and uses Dirichlet-character orthogonality and finite Fourier Parseval to obtain:

• The additive large sieve on the rational point set X_Q = {r/q : 1 ≤ q ≤ Q, 0 ≤ r < q} (the Farey fractions after removing duplicates): Σ_{x∈X_Q} |Σ_n a_n·e(nx)|² ≤ C(N, 1/Q²)·Σ_n |a_n|² (largeSieveRationalPoints).
• The character large-sieve inequality for each modulus q: (q/φ(q))·Σ_{χ mod q} |Σ_n a_n·χ(n)|² ≤ Σ_{r<q} |Σ_n a_n·e(nr/q)|² (characterSieveModulus_le).

Proof structure (Montgomery's classical route):

1. Character orthogonality: summing over all characters modulo q, Σ_χ |S(χ)|² = φ(q)·Σ_{(a,q)=1} |Σ_{n≡a (q)} a_n|². Use mathlib's DirichletCharacter.sum_char_inv_mul_char_eq; χ(n) = 0 for (n,q) > 1 handles the coprimality restriction.
2. Finite Fourier Parseval: Σ_{a mod q} |Σ_{n≡a (q)} a_n|² = (1/q)·Σ_{r mod q} |S(r/q)|² (zmodParseval_inv/zmodParseval_character), using the geometric-series kernel Σ_a e(a(r−s)/q) = q·1_{r=s}.
3. Spacing of rational points: X_Q is 1/Q²-well-spaced, since the numerator-denominator difference gives a lower bound ≥ 1/(q₁q₂) (rationalPoints_wellSpaced).
4. Additive large sieve: apply largeSievePrimal_wellSpaced to X_Q to obtain largeSieveRationalPoints, with the weaker additive large-sieve constant C(N, 1/Q²) (largeSieveBound).

Scope and limitations. The classical Bombieri--Davenport bound Σ_{q≤Q} (q/φ(q))·Σ*_{χ mod q} |S(χ)|² ≤ (Q²+N−1)·Σ_n |a_n|² restricts Σ* to primitive characters. Its derivation needs (i) primitive-character theory and Gauss sums (|τ(χ)|² = q) to write (q/φ(q))·|S(χ)|² as (1/φ(q))·|Σ_{(a,q)=1} conj(χ(a))·S(a/q)|², and (ii) an explicit sum over reduced fraction pairs, with a bijection to the deduplicated rationalPoints set. These additional steps belong to BombieriDavenport.lean, not to the per-modulus argument here.

One cannot simply sum the Parseval bounds over all characters or over the point multiset Σ_{q≤Q} Σ_{r<q} |S(r/q)|². For example, with a_n ≡ 1, Q = 2, and sufficiently large N, Σ_q (q/φ(q))Σ_χ |S(χ)|² ≈ 3N²/2, whereas C(N,1/4)·N = (N+64)·N. The primitive-character restriction is therefore essential. The constant C(N,δ) comes from the additive estimate; the sharp N + δ⁻¹ bound is not supplied by this argument.

References: Montgomery, "Topics in Multiplicative Number Theory" (1971), Ch. 1; Iwaniec & Kowalski, "Analytic Number Theory" (2004), Ch. 7; Kedlaya, "Notes on Analytic Number Theory", Ch. 16 (Bombieri--Davenport).

1. Complex roots of unity and conjugation of character values

theorem AnalyticNumberTheory.LargeSieve.complexHasEnoughRootsOfUnity (n : ℕ) (hn : n ≠ 0) : HasEnoughRootsOfUnity ℂ n

ℂ has enough nth roots of unity for n ≠ 0: exp(2πi/n) is primitive and the group of roots of unity is cyclic. This supplies the complex instance needed by the DirichletCharacter orthogonality theorem, in addition to mathlib's instances for Circle and algebraic closures.

theorem AnalyticNumberTheory.LargeSieve.conj_eq_inv_of_norm_eq_one {z : ℂ} (hz : ‖z‖ = 1) : star z = z⁻¹

The conjugate of a complex number of norm 1 equals its inverse.

theorem AnalyticNumberTheory.LargeSieve.char_conj_inv {q : ℕ} (χ : DirichletCharacter ℂ q) {a : ZMod q} (ha : IsUnit a) : star (χ a) = χ⁻¹ a

Conjugation equals evaluation of the inverse character: conj(χ(a)) = χ⁻¹(a) for a unit a. The nonunit case is handled separately in the orthogonality lemma, where both sides are zero.

2. Geometric-series kernel and Parseval modulo q

theorem AnalyticNumberTheory.LargeSieve.charReal_int_eq_one (k : ℤ) : charReal ↑k = 1

e(x) is 1 at integers: e(k) = 1 (k : ℤ).

theorem AnalyticNumberTheory.LargeSieve.charReal_periodic_int (x : ℝ) (k : ℤ) : charReal (x + ↑k) = charReal x

Every integer is a period of e: e(x + k) = e(x) (k : ℤ).

theorem AnalyticNumberTheory.LargeSieve.geomSum_zmod_charReal {q : ℕ} (hq : 0 < q) (k : ℤ) : ∑ r ∈ Finset.range q, charReal (↑k * ↑r / ↑q) = if ↑q ∣ k then ↑q else 0

Geometric-series kernel modulo q: Σ_{r<q} e(r·k/q) = q·1_{q|k} for integer k. If q | k, each term is 1; otherwise use the geometric-series formula with e(k) = 1.

theorem AnalyticNumberTheory.LargeSieve.zmodParseval {q : ℕ} (hq : 0 < q) (z : ℕ → ℂ) : ∑ a ∈ Finset.range q, ↑‖∑ r ∈ Finset.range q, charReal (↑a * ↑r / ↑q) * z r‖ ^ 2 = ↑q * ∑ r ∈ Finset.range q, ↑‖z r‖ ^ 2

Finite Fourier Parseval modulo q: for any z : ℕ → ℂ, Σ_{a<q} |Σ_{r<q} e(ar/q)·z_r|² = q·Σ_{r<q} |z_r|².

3. Character orthogonality

theorem AnalyticNumberTheory.LargeSieve.charOrthSum {q : ℕ} (hq : 0 < q) (m n : ZMod q) : ∑ χ : DirichletCharacter ℂ q, χ m * star (χ n) = if IsUnit m ∧ IsUnit n ∧ m = n then ↑q.totient else 0

Pointwise character orthogonality: for m, n : ZMod q, Σ_χ χ(m)·conj(χ(n)) = φ(q)·1_{IsUnit m ∧ IsUnit n ∧ m = n}.

theorem AnalyticNumberTheory.LargeSieve.unitClassSum {q : ℕ} [NeZero q] (a : ℤ → ℂ) (M : ℤ) (N : ℕ) : ∑ m ∈ Finset.Icc (M + 1) (M + ↑N), (if IsUnit ↑m then 1 else 0) * a m * star (∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * if ↑n = ↑m then 1 else 0) = ∑ x : ZMod q, (if IsUnit x then 1 else 0) * ↑‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * if ↑n = x then 1 else 0‖ ^ 2

Grouping by residue class: for any a, Σ_{m ∈ Icc} [IsUnit m]·a_m·star(Σ_{n≡m} a_n) = Σ_{x mod q} [IsUnit x]·|Σ_{n≡x} a_n|².

theorem AnalyticNumberTheory.LargeSieve.charInnerReduce {q : ℕ} [NeZero q] (a : ℤ → ℂ) (M : ℤ) (N : ℕ) : (∑ m ∈ Finset.Icc (M + 1) (M + ↑N), ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ((a m * star (a n) * ↑q.totient * if IsUnit ↑m then 1 else 0) * if IsUnit ↑n then 1 else 0) * if ↑m = ↑n then 1 else 0) = ↑q.totient * ∑ m ∈ Finset.Icc (M + 1) (M + ↑N), (if IsUnit ↑m then 1 else 0) * a m * star (∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * if ↑n = ↑m then 1 else 0)

Inner reduction: Σ_m Σ_n a_m·star(a_n)·φ(q)·[unit m][unit n][m≡n] = φ(q)·Σ_m [unit m]·a_m·star(Σ_{n≡m} a_n).

theorem AnalyticNumberTheory.LargeSieve.charOrthogonality_le {q : ℕ} [NeZero q] (a : ℤ → ℂ) (M : ℤ) (N : ℕ) : ∑ χ : DirichletCharacter ℂ q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * χ ↑n‖ ^ 2 ≤ ↑q.totient * ∑ x : ZMod q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * if ↑n = x then 1 else 0‖ ^ 2

Character orthogonality inequality: for any a, Σ_χ |Σ_{n∈Icc} a_n·χ(n)|² ≤ φ(q)·Σ_{x mod q} |Σ_{n≡x} a_n|² as a real-valued inequality.

4. Well-spaced rational points and the multiplicative large sieve

noncomputable def AnalyticNumberTheory.LargeSieve.rationalPoints (Q : ℕ) : Finset ℝ

The rational point set X_Q = {r/q : 1 ≤ q ≤ Q, 0 ≤ r < q} ⊆ [0,1).

Equations

• AnalyticNumberTheory.LargeSieve.rationalPoints Q = (Finset.Icc 1 Q).biUnion fun (q : ℕ) => Finset.image (fun (r : ℕ) => ↑r / ↑q) (Finset.range q)

theorem AnalyticNumberTheory.LargeSieve.rationals_distToInt_ge {q₁ r₁ q₂ r₂ : ℕ} (hq₁ : 0 < q₁) (hq₂ : 0 < q₂) (hr₁ : r₁ < q₁) (hr₂ : r₂ < q₂) (hne : ↑r₁ / ↑q₁ ≠ ↑r₂ / ↑q₂) : 1 / (↑q₁ * ↑q₂) ≤ distToInt (↑r₁ / ↑q₁ - ↑r₂ / ↑q₂)

Two distinct rational points modulo 1 have distance at least 1/(q₁q₂).

theorem AnalyticNumberTheory.LargeSieve.rationalPoints_wellSpaced (Q : ℕ) (hQ : 0 < Q) : wellSpacedReal (rationalPoints Q) (1 / ↑Q ^ 2)

The rational point set X_Q = {r/q : 1 ≤ q ≤ Q, 0 ≤ r < q} is 1/Q²-well-spaced.

5. Multiplicative large-sieve assembly: inverse Parseval, characters, and Farey points

theorem AnalyticNumberTheory.LargeSieve.zmod_sum_range {q : ℕ} [NeZero q] {M : Type u_1} [AddCommMonoid M] (f : ZMod q → M) : ∑ x : ZMod q, f x = ∑ a ∈ Finset.range q, f ↑a

Summation along the bijection between residue classes modulo q and 0..q−1: Σ_{x : ZMod q} f x = Σ_{a < q} f ↑a.

theorem AnalyticNumberTheory.LargeSieve.zmod_dvd_add_iff {q a b : ℕ} (hq : 0 < q) (ha : a < q) (hb : b < q) : ↑q ∣ ↑a + ↑b ↔ b = (q - a) % q

For 0 ≤ a,b < q, q | a+b if and only if b = (q−a) mod q.

theorem AnalyticNumberTheory.LargeSieve.zmod_dvd_sub_iff {q a b : ℕ} (_hq : 0 < q) (ha : a < q) (hb : b < q) : ↑q ∣ ↑a - ↑b ↔ a = b

For 0 ≤ a,b < q, q | a−b if and only if a = b.

theorem AnalyticNumberTheory.LargeSieve.zmodCharKernel {q : ℕ} (hq : 0 < q) (a b : ℕ) (ha : a < q) (hb : b < q) : ∑ r ∈ Finset.range q, charReal (↑a * ↑r / ↑q) * star (charReal (↑b * ↑r / ↑q)) = if a = b then ↑q else 0

Kernel modulo q: Σ_{r<q} e(ar/q)·conj(e(br/q)) = q·1_{a=b} for 0 ≤ a,b < q.

theorem AnalyticNumberTheory.LargeSieve.zmodParseval_inv {q : ℕ} (hq : 0 < q) (c : ℕ → ℂ) : ∑ a ∈ Finset.range q, ‖c a‖ ^ 2 = 1 / ↑q * ∑ r ∈ Finset.range q, ‖∑ a ∈ Finset.range q, c a * charReal (↑a * ↑r / ↑q)‖ ^ 2

Inverse Parseval: Σ_{a<q} |c a|² = (1/q)·Σ_{r<q} |Σ_{a<q} c a e(ar/q)|². Expand Σ_r |ĉ r|² directly and use Σ_r e((a−b)r/q) = q·1_{a=b} (zmodCharKernel), avoiding Fourier inversion and conjugation-sign bookkeeping.

theorem AnalyticNumberTheory.LargeSieve.charReal_zmod_eq {q : ℕ} (hq : 0 < q) {m : ℤ} {n : ℕ} (hmn : ↑m = ↑n) (r : ℕ) : charReal (↑m * ↑r / ↑q) = charReal (↑n * ↑r / ↑q)

Congruence periodicity modulo q: for an integer m and natural n, (m : ZMod q) = (n : ZMod q) implies e(mr/q) = e(nr/q).

theorem AnalyticNumberTheory.LargeSieve.zmodParseval_character {q : ℕ} [NeZero q] (a : ℤ → ℂ) (M : ℤ) (N : ℕ) : ∑ x : ZMod q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * if ↑n = x then 1 else 0‖ ^ 2 = 1 / ↑q * ∑ r ∈ Finset.range q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), charReal (↑n * ↑r / ↑q) * a n‖ ^ 2

Character form of Parseval: Σ_{x mod q} |Σ_{n≡x (q)} a_n|² = (1/q)·Σ_{r<q} |S(r/q)|², where S(r/q) = Σ_n a_n·e(nr/q). This follows directly from zmodParseval_inv with c a = Σ_{n≡a (q)} a_n.

theorem AnalyticNumberTheory.LargeSieve.largeSieveRationalPoints (M : ℤ) (N Q : ℕ) (hQ : 0 < Q) (a : ℤ → ℂ) : ∑ x ∈ rationalPoints Q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), charReal (↑n * x) * a n‖ ^ 2 ≤ largeSieveBound N (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖a n‖ ^ 2

Additive large sieve on rational points: for the Farey point set X_Q = {r/q : 1 ≤ q ≤ Q, 0 ≤ r < q} (the reduced fractions after deduplication, hence 1/Q²-well-spaced), Σ_{x∈X_Q} |Σ_{M<n≤M+N} a_n·e(nx)|² ≤ C(N, 1/Q²)·Σ_n |a_n|², where C(N,δ) = largeSieveBound N δ is the weaker additive large-sieve constant from the additive estimate.

theorem AnalyticNumberTheory.LargeSieve.characterSieveModulus_le {q : ℕ} [NeZero q] (a : ℤ → ℂ) (M : ℤ) (N : ℕ) : ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * χ ↑n‖ ^ 2 ≤ ∑ r ∈ Finset.range q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), charReal (↑n * ↑r / ↑q) * a n‖ ^ 2

Character large-sieve inequality for each modulus q: character orthogonality (charOrthogonality_le) and character Parseval (zmodParseval_character) give (q/φ(q))·Σ_{χ mod q} |Σ_n a_n·χ(n)|² ≤ Σ_{r<q} |Σ_n a_n·e(nr/q)|². Summing this over q ≤ Q does not give an all-character large sieve (see the counterexample in the module overview). The classical Bombieri--Davenport argument instead requires primitive characters and Gauss sums, treated separately in BombieriDavenport.lean.