AnalyticNumberTheory.LargeSieve.BombieriDavenport

Primitive characters + Gauss sums, and the Bombieri-Davenport large sieve

This module proves the classical Bombieri-Davenport multiplicative large sieve lemma (Montgomery 1971 Ch.1; Iwaniec-Kowalski 2004 Thm 7.18 type):

sum_{1 <= q <= Q} (q/phi(q)) * sum_{chi primitive mod q} ||sum_n a_n chi(n)||^2 <= largeSieveBound(N, 1/Q^2) * sum_n ||a_n||^2

The construction consists of:

1. The standard additive character e_q(x) = e(x.val/q) on ZMod q (from AddChar.zmodChar and the repo's charReal), its primitivity, and the Gauss sum bridge gaussSum chi (e_q.mulShift n) = sum_x chi(x) * e(n * x.val / q).
2. |tau(chi)|^2 = q for primitive chi mod q (zmodParseval + mathlib's gaussSum_mulShift_of_isPrimitive).
3. Gauss-sum Fourier inversion for primitive chi: ||S_chi||^2 = (1/q) * ||sum_{r<q} chi(r) * T(r/q)||^2.
4. The Bombieri-Davenport stacking: unit Parseval (charOrthSum) + the Farey point additive sieve (largeSieveRationalPoints).

Limitation of panTypeICharSquareMeanBound: the literal target sum_{q <= Q} mu^2(q) 3^omega(q) * sum_{chi mod q} ||V_chi(m)||^2 <= C * (m + Q^2) * sum_{n <= m} vaughanFirst(n,u)^2 is FALSE as stated: take u = 1 (then vaughanFirst(n,1) = log n) and m = Q^2; the smooth part of the class sums gives LHS >= sum_{q <= Q} mu^2(q) 3^omega(q) phi(q)^2 m^2 (log m)^2 / q^2 which already exceeds C (m + Q^2) S(m) for every constant C (primes alone contribute sum_{p <= Q} 3 (p-1)^2 / p^2 ~ 3 Q / log Q). See check_target.py for the numerics (LHS/RHS grows without bound as Q -> oo). The correct analytic input is the primitive-character version with the (q/phi(q)) weight, proved below as bombieriDavenport_le; see the file trailer for the explicit corrected sub-steps of the type-I assembly.

1. The standard additive character e_q and Gauss sum bridge

noncomputable def AnalyticNumberTheory.LargeSieve.zetaRoot (q : ℕ) : ℂ

Standard q-th root of unity: zeta = e(1/q) = exp(2pii/q).

Equations

• AnalyticNumberTheory.LargeSieve.zetaRoot q = AnalyticNumberTheory.LargeSieve.charReal (1 / ↑q)

theorem AnalyticNumberTheory.LargeSieve.zetaRoot_isPrimitiveRoot (q : ℕ) (hq : q ≠ 0) : IsPrimitiveRoot (zetaRoot q) q

zeta is a primitive q-th root of unity (q != 0).

theorem AnalyticNumberTheory.LargeSieve.zetaRoot_pow (q : ℕ) (hq : q ≠ 0) : zetaRoot q ^ q = 1

zeta^q = 1 (q != 0).

noncomputable def AnalyticNumberTheory.LargeSieve.zmodCharStd (q : ℕ) [NeZero q] : AddChar (ZMod q) ℂ

The standard additive character e_q(a) = e(a.val/q) = zeta^(a.val).

Equations

• AnalyticNumberTheory.LargeSieve.zmodCharStd q = AddChar.zmodChar q ⋯

theorem AnalyticNumberTheory.LargeSieve.zmodCharStd_apply (q : ℕ) [NeZero q] (a : ZMod q) : (zmodCharStd q) a = charReal (↑a.val / ↑q)

e_q(a) = e(a.val/q).

theorem AnalyticNumberTheory.LargeSieve.zmodCharStd_isPrimitive (q : ℕ) [NeZero q] : (zmodCharStd q).IsPrimitive

e_q is a primitive additive character (q != 0).

theorem AnalyticNumberTheory.LargeSieve.charReal_periodic_zmod {q : ℕ} (hq : 0 < q) {m n : ℤ} (hmn : m ≡ n [ZMOD ↑q]) : charReal (↑m / ↑q) = charReal (↑n / ↑q)

charReal is periodic modulo integers: e((m + q t)/q) = e(m/q).

theorem AnalyticNumberTheory.LargeSieve.zmodCharStd_mulShift_apply (q : ℕ) [NeZero q] (n : ℤ) (x : ZMod q) : ((zmodCharStd q).mulShift ↑n) x = charReal (↑n * ↑x.val / ↑q)

e_q(n * x) = e(n * x.val / q) for n : ℤ: the Gauss-sum bridge.

2. The Gauss-sum magnitude: |tau(chi)|^2 = q for primitive chi

theorem AnalyticNumberTheory.LargeSieve.cast_mul_sum {α : Type u_1} (s : Finset α) (c : ℝ) (f : α → ℝ) : ↑c * ∑ x ∈ s, ↑(f x) = (algebraMap ℝ ℂ) (c * ∑ x ∈ s, f x)

(c : ℂ) * sum of casts = cast of (c * sum).

theorem AnalyticNumberTheory.LargeSieve.gaussSum_mulShift_apply {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (n : ℤ) : gaussSum χ ((zmodCharStd q).mulShift ↑n) = ∑ x : ZMod q, χ x * charReal (↑n * ↑x.val / ↑q)

Gauss sum of chi against a shifted additive character, in charReal form: gaussSum chi (e_q.mulShift n) = sum_{x mod q} chi(x) * e(n * x.val / q).

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

The sum over ZMod q equals the sum over representatives r < q.

theorem AnalyticNumberTheory.LargeSieve.zmodParseval_zmod {q : ℕ} [NeZero q] (z : ZMod q → ℂ) : ∑ a : ZMod q, ‖∑ x : ZMod q, charReal (↑a.val * ↑x.val / ↑q) * z x‖ ^ 2 = ↑q * ∑ x : ZMod q, ‖z x‖ ^ 2

Parseval (ZMod version): sum_{a mod q} |sum_{x mod q} e(a*x.val/q) z x|^2 = q * sum_x |z x|^2.

3. |tau(chi)|^2 = q for primitive chi

theorem AnalyticNumberTheory.LargeSieve.dirichletChar_norm_unit {q : ℕ} (χ : DirichletCharacter ℂ q) {a : ZMod q} (ha : IsUnit a) : ‖χ a‖ = 1

|chi(a)| = 1 for unit a.

theorem AnalyticNumberTheory.LargeSieve.dirichletChar_norm_le_one (q : ℕ) (χ : DirichletCharacter ℂ q) (a : ZMod q) : ‖χ a‖ ≤ 1

The norm of a Dirichlet character is at most one, for every modulus.

theorem AnalyticNumberTheory.LargeSieve.charNormSq_sum {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) : ∑ a : ZMod q, ‖χ a‖ ^ 2 = ↑q.totient

The L2 mass of |chi| over all residues is phi(q).

theorem AnalyticNumberTheory.LargeSieve.char_inv_eq_star {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (a : ZMod q) : χ⁻¹ a = star (χ a)

chi^{-1} a = star (chi a) for all a (complex characters).

theorem AnalyticNumberTheory.LargeSieve.gaussSumSq_eq_conductor {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ.IsPrimitive) : ‖gaussSum χ (zmodCharStd q)‖ ^ 2 = ↑q

Gauss-sum magnitude: |tau(chi)|^2 = q for primitive chi mod q. Via Parseval (zmodParseval_zmod with z = chi) and mathlib's gaussSum_mulShift_of_isPrimitive.

4. Gauss-sum Fourier inversion for primitive characters

theorem AnalyticNumberTheory.LargeSieve.star_factorsThrough {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (d : ℕ) : (star χ).FactorsThrough d ↔ χ.FactorsThrough d

star preserves FactorsThrough: (star chi).FactorsThrough d iff chi.FactorsThrough d.

theorem AnalyticNumberTheory.LargeSieve.star_conductor {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) : (star χ).conductor = χ.conductor

The conductor is preserved by star.

theorem AnalyticNumberTheory.LargeSieve.star_isPrimitive {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ.IsPrimitive) : (star χ).IsPrimitive

star preserves primitivity.

noncomputable def AnalyticNumberTheory.LargeSieve.charAddSum (a : ℤ → ℂ) (M : ℤ) (N q : ℕ) (x : ZMod q) : ℂ

The additive sum T(x) = sum_n a_n * e(n * x.val / q) for x : ZMod q.

Equations

• AnalyticNumberTheory.LargeSieve.charAddSum a M N q x = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * AnalyticNumberTheory.LargeSieve.charReal (↑n * (↑x.val / ↑q))

theorem AnalyticNumberTheory.LargeSieve.charReal_mul_div {q : ℕ} [NeZero q] (n : ℤ) (x : ZMod q) : charReal (↑n * (↑x.val / ↑q)) = charReal (↑n * ↑x.val / ↑q)

e(n·x/q) written with the single quotient x/q: argument-form bridge.

theorem AnalyticNumberTheory.LargeSieve.primitiveFourier {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ.IsPrimitive) (n : ℤ) : ∑ x : ZMod q, star (χ x) * charReal (↑n * (↑x.val / ↑q)) = χ ↑n * gaussSum (star χ) (zmodCharStd q)

The Fourier transform of a primitive character: for all n, sum_{x mod q} star(chi x) * e(n x / q) = chi n * tau(star chi).

theorem AnalyticNumberTheory.LargeSieve.primitiveInversion {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ.IsPrimitive) (a : ℤ → ℂ) (M : ℤ) (N : ℕ) : ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * χ ↑n‖ ^ 2 = 1 / ↑q * ‖∑ x : ZMod q, star (χ x) * charAddSum a M N q x‖ ^ 2

Primitive inversion: for primitive chi mod q, |S_chi|^2 = (1/q) * |sum_{x mod q} star(chi x) * T(x)|^2 where S_chi = sum_n a_n chi(n) and T(x) = sum_n a_n e(n x.val / q).

5. Unit Parseval and the Bombieri-Davenport stacking

theorem AnalyticNumberTheory.LargeSieve.charOrthSum_star {q : ℕ} [NeZero q] (a b : ZMod q) : ∑ χ : DirichletCharacter ℂ q, star (χ a) * χ b = if IsUnit a ∧ IsUnit b ∧ a = b then ↑q.totient else 0

Orthogonality with star: sum_chi star(chi a) * chi b = phi(q) * [a = b and a unit].

theorem AnalyticNumberTheory.LargeSieve.charParseval_units {q : ℕ} [NeZero q] (T : ZMod q → ℂ) : ∑ χ : DirichletCharacter ℂ q, ‖∑ x : ZMod q, star (χ x) * T x‖ ^ 2 = ↑q.totient * ∑ x : ZMod q, if IsUnit x then ‖T x‖ ^ 2 else 0

Unit Parseval: sum_chi ||sum_x star(chi x) T x||^2 = phi(q) * sum over units |T x|^2.

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

The set of reduced fractions {r/q : 1 <= q <= Q, 0 < r < q, (r, q) = 1}.

Equations

• AnalyticNumberTheory.LargeSieve.reducedFracs Q = (Finset.Icc 1 Q).biUnion fun (q : ℕ) => Finset.image (fun (r : ℕ) => ↑r / ↑q) ({r ∈ Finset.range q | r.Coprime q})

theorem AnalyticNumberTheory.LargeSieve.reducedFracs_subset_rationalPoints (Q : ℕ) : reducedFracs Q ⊆ rationalPoints Q

reducedFracs is contained in rationalPoints (each reduced fraction is a rational point).

theorem AnalyticNumberTheory.LargeSieve.reducedFracs_sum {Q : ℕ} {β : Type u_1} [AddCommMonoid β] (T : ℝ → β) : ∑ q ∈ Finset.Icc 1 Q, ∑ r ∈ Finset.range q with r.Coprime q, T (↑r / ↑q) = ∑ x ∈ reducedFracs Q, T x

The double sum over reduced pairs equals the sum over reducedFracs (the map is injective).

6. The Bombieri-Davenport lemma

theorem AnalyticNumberTheory.LargeSieve.charAddSum_natCast {q : ℕ} [NeZero q] (a : ℤ → ℂ) (M : ℤ) (N : ℕ) {r : ℕ} (hr : r < q) : charAddSum a M N q ↑r = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * charReal (↑n * (↑r / ↑q))

charAddSum at the representative (r : ZMod q) equals the range-sum for r < q.

theorem AnalyticNumberTheory.LargeSieve.unitsSum_eq_reducedFracs {q : ℕ} [NeZero q] (T : ZMod q → ℂ) : (∑ x : ZMod q, if IsUnit x then ‖T x‖ ^ 2 else 0) = ∑ r ∈ Finset.range q with r.Coprime q, ‖T ↑r‖ ^ 2

The unit-class sum of |T|^2 equals the sum over reduced residues r < q.

theorem AnalyticNumberTheory.LargeSieve.bombieriDavenport_le (Q : ℕ) (hQ : 0 < Q) (a : ℤ → ℂ) (M : ℤ) (N : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), a n * χ ↑n‖ ^ 2 ≤ largeSieveBound N (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖a n‖ ^ 2

Bombieri-Davenport lemma: sum_{1 <= q <= Q} (q/phi(q)) * sum over primitive chi of |sum_n a_n chi(n)|^2 is bounded by the additive large sieve on the Farey set X_Q = {r/q : 1 <= q <= Q, 0 <= r < q, gcd(r,q)=1}.

7. Application to Type I coefficients and limitations

theorem AnalyticNumberTheory.LargeSieve.vaughanFirst_Icc_charSum {q m u : ℕ} (χ : DirichletCharacter ℂ q) : ∑ n ∈ Finset.Icc 0 ↑m, (if 0 ≤ n then ↑(Sieve.vaughanFirst n.toNat u) else 0) * χ ↑n = ∑ n ∈ Finset.range (m + 1), ↑(Sieve.vaughanFirst n u) * χ ↑n

The Icc (0 : ℤ) (m : ℤ) sum of the vaughanFirst coefficients equals the character sum over range (m + 1) (bridge between the BD lemma and panTypeIV1CharSum).

theorem AnalyticNumberTheory.LargeSieve.vaughanFirst_Icc_normSq (m u : ℕ) : ∑ n ∈ Finset.Icc 0 ↑m, ‖if 0 ≤ n then ↑(Sieve.vaughanFirst n.toNat u) else 0‖ ^ 2 = ∑ n ∈ Finset.range (m + 1), Sieve.vaughanFirst n u ^ 2

The norm-square of the interval coefficients equals the range sum of vaughanFirst(n,u)^2.

theorem AnalyticNumberTheory.LargeSieve.bombieriDavenport_vaughanFirst (Q m u : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ‖Sieve.panTypeIV1CharSum q m u χ‖ ^ 2 ≤ largeSieveBound (m + 1) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.range (m + 1), Sieve.vaughanFirst n u ^ 2

Bombieri-Davenport for the type-I coefficients: the primitive-character (q/phi(q))-weighted mean bound for vaughanFirst(n,u), i.e. the corrected analytic input for the type-I mean value. The literal panTypeICharSquareMeanBound (all characters, weight mu^2 3^omega, constant C) is FALSE as stated; see the module header.

7b. Application to the type-II assembly (panTypeIIV3CharSum)

The mirror of section 7 for the type-II coefficients: Bombieri-Davenport for vaughanThird(n,u,v) with the (q/phi(q)) primitive-character weight, bombieriDavenport_vaughanThird, the corrected analytic input for the type-II mean value.

theorem AnalyticNumberTheory.LargeSieve.vaughanThird_Icc_charSum {q m u v : ℕ} (χ : DirichletCharacter ℂ q) : ∑ n ∈ Finset.Icc 0 ↑m, (if 0 ≤ n then ↑(Sieve.vaughanThird n.toNat u v) else 0) * χ ↑n = ∑ n ∈ Finset.range (m + 1), ↑(Sieve.vaughanThird n u v) * χ ↑n

The Icc (0 : ℤ) (m : ℤ) sum of the vaughanThird coefficients equals the character sum over range (m + 1) (bridge between the BD lemma and panTypeIIV3CharSum).

theorem AnalyticNumberTheory.LargeSieve.vaughanThird_Icc_normSq (m u v : ℕ) : ∑ n ∈ Finset.Icc 0 ↑m, ‖if 0 ≤ n then ↑(Sieve.vaughanThird n.toNat u v) else 0‖ ^ 2 = ∑ n ∈ Finset.range (m + 1), Sieve.vaughanThird n u v ^ 2

The norm-square of the interval coefficients equals the range sum of vaughanThird(n,u,v)^2.

theorem AnalyticNumberTheory.LargeSieve.bombieriDavenport_vaughanThird (Q m u v : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ‖Sieve.panTypeIIV3CharSum q m u v χ‖ ^ 2 ≤ largeSieveBound (m + 1) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.range (m + 1), Sieve.vaughanThird n u v ^ 2

Bombieri-Davenport for the type-II coefficients: the primitive-character (q/phi(q))-weighted mean bound for vaughanThird(n,u,v), i.e. the corrected analytic input for the type-II mean value (mirror of bombieriDavenport_vaughanFirst).

8. The per-q assembly analysis: regrouping by reduced fractions

theorem AnalyticNumberTheory.LargeSieve.gcd_mul_right' (a b c : ℕ) : (a * c).gcd (b * c) = c * a.gcd b

gcd multiplication: gcd(ac, bc) = c * gcd(a, b).

theorem AnalyticNumberTheory.LargeSieve.coprime_div_gcd {q r : ℕ} (hq : 0 < q) : (q / q.gcd r).Coprime (r / q.gcd r)

Dividing by the gcd gives a coprime pair.

theorem AnalyticNumberTheory.LargeSieve.perModulus_regroup {Q : ℕ} (w : ℕ → ℝ) (f : ℝ → ℂ) : ∑ q ∈ Finset.Icc 1 Q, ↑(w q) * ∑ r ∈ Finset.range q, f (↑r / ↑q) = ∑ q' ∈ Finset.Icc 1 Q, ↑(∑ d ∈ Finset.Icc 1 (Q / q'), w (q' * d)) * ∑ r' ∈ Finset.range q' with r'.Coprime q', f (↑r' / ↑q')

Per-modulus regrouping (the exact content of assembly for each q): for weights w(q), sum_{q <= Q} w(q) * sum_{r < q} f(r/q) = sum_{q' <= Q} W(q') * sum_{red r'} f(r'/q') with W(q') = sum_{d <= Q/q'} w(q'*d); the reduced fractions r'/q' (coprime) carry the regrouped weight. For w(q) = mu^2 3^omega phi(q)/q, W(1) ~ (log Q)^3 is unbounded — the per-q stacking cannot produce the (m + Q^2) shape.

9. Per-modulus bounds versus the Type I mean-value target

Setup. The actual consumer of the mean-value input is panTypeICharMeanSieveBound in PanMeanValueBody, via PanTypeICharacterMeanValue.of_sieveBound. Its L^2 intermediate panTypeICharSquareMeanBound asks for sum_{q<=Q} mu^2 3^omega * sum_{chi mod q} ||V_chi(m)||^2 <= C (m + Q^2) S(m). The per-modulus material already proved is characterSieveModulus_le sum_chi ||S_chi||^2 <= (phi(q)/q) * sum_{r<q} |T(r/q)|^2 (one q at a time) together with the additive sieve largeSieveBound(m+1, 1/q^2) = m + O(q^2 log q).

(a) Can the q-summation be done from the per-q material + polylog? NO. The per-q bound gives the q-sum with weight mu^2 3^omega (phi(q)/q) times (m + q^2 log q). The regrouping lemma perModulus_regroup shows this is exactly sum_{q'<=Q} W(q') * sum_{red r'} |T(r'/q')|^2, W(q') = sum_{d<=Q/q'} mu^2 3^omega phi(q'd)/(q'd), and the effective weight W(1) = sum_{d<=Q} mu^2 3^omega phi(d)/d is unbounded; primes alone contribute order Q/log Q, so this is not merely log-cubed growth (numerics in check_perq.py: W(1) = 94, 211, 473, 1098 at Q = 40, 80, 160, 320). Equivalently, sum_{q<=Q} mu^2 3^omega (phi/q) (m + q^2 log q) m Q (log Q)^2 + Q^3 (log Q)^3, which is Q (log Q)^3 times bigger than (m + Q^2) at m = Q^2 (ratio 704, 1664, 3844, 9777). So the per-q stacking cannot produce the (m + Q^2) shape; moreover panTypeICharSquareMeanBound itself is false (u = 1, m = Q^2; see section 7).

(b) The real Bombieri-Davenport (all q simultaneously) is needed — and proved. characterSieveModulus_le is per-modulus (fixed q). The all-q version must apply the additive sieve to the WHOLE Farey set X_Q = {r/q : 1 <= q <= Q, 0 <= r < q, gcd(r,q)=1} (which is 1/Q^2-well-spaced) with largeSieveRationalPoints — that is exactly bombieriDavenport_le / bombieriDavenport_vaughanFirst (sum over primitive chi with the (q/phi(q)) weight; the Gauss-sum inversion converts the weighted primitive sum to the UNWEIGHTED reduced-fraction sum, and the additive sieve is applied once, on X_Q). This gives the m + Q^2 shape (up to the weak sieve constant).

(c) The direct-Parseval-stacking counterexample is avoided. The per-modulus counterexample discussed in PanMeanValueBody shows that stacking the per-q Parseval over ALL characters (or with multiplicities on the rational points) fails. The BD proof never does that: it (i) restricts to primitive characters, (ii) uses the Gauss-sum inversion |S_chi|^2 = (1/q) |sum_a star(chi a) T(a/q)|^2, (iii) applies the unit-group Parseval to get the sum over REDUCED fractions with weight 1, and (iv) applies the additive sieve once on the Farey set. No per-q Parseval stacking occurs.

Additional requirements for a mean-value assembly. The proved BD lemma carries the (q/phi(q)) weight over primitive characters; the target carries mu^2 3^omega over all characters. Bridging the two needs the conductor decomposition (each chi mod q lifts a unique primitive chi' mod q' | q) with the non-coprime part controlled by density estimates, and then the mu^2 3^omega weight assembly (sub-steps S2-S3 of section 7). The sharp (m + Q^2) constant additionally needs the N + delta^{-1} additive-sieve constant (sub-step S4).