AnalyticNumberTheory.Sieve.PanV3SquareMean

Type II square-sum bounds and per-modulus large-sieve reduction

This module proves two components relevant to panTypeIICharMeanSieveBound and PanTypeIICharacterMeanValue (PanMeanValueBody.lean §§5, 5.2), parallel to PanV1SquareMean.lean:

1. Elementary square-sum bound: Σ_{n≤N} vaughanThird(n,u,v)² ≤ N·(1+log(N+1))⁵. The bilinear inner sum satisfies Σ_{e|n/d, v<e} Λ(e) ≤ Σ_{e|n/d} Λ(e) = log(n/d), by ArithmeticFunction.vonMangoldt_sum and Λ ≥ 0. With |μ(d)| ≤ 1 and τ(n) = n.divisors.card, this gives |vaughanThird(n,u,v)| ≤ τ(n)·log(n+1). Double counting and the lcm reduction yield Σ_{n≤N} τ(n)² ≤ N·(1+log(N+1))³.
2. Per-modulus character square-sum bound: Σ_χ ‖V_χ(m)‖² ≤ (φ(q)/q)·largeSieveBound(m+1,1/q²)·Σ_{n≤m} vaughanThird(n,u,v)², where V_χ(m) = Σ_{n≤m} vaughanThird(n,u,v)·χ(n) is panTypeIIV3CharSum. Combine characterSieveModulus_le with largeSieveRationalPoints, then replace the maximum by a sum to obtain panTypeIICharSqrtMeanMaxY_le_sieveSqrtSum.

This does not prove the all-character panTypeIICharSquareMeanBound over q ≤ Q. The classical Bombieri--Davenport theorem uses primitive characters and Gauss sums |τ(χ)|² = q; the all-character version requires additional control and has a principal-character obstruction at u = v = 1 (see PanTypeIIBoundAudit.lean). The final per-modulus reduction here leaves only the sieve constant, the V3 L² sum, and outer (y,a) weights.

1. Elementary pointwise bound for vaughanThird

theorem AnalyticNumberTheory.Sieve.v3_moebius_abs_le_one (d : ℕ) : |↑(ArithmeticFunction.moebius d)| ≤ 1

μ(d) ∈ {-1, 0, 1}: |μ d| ≤ 1.

theorem AnalyticNumberTheory.Sieve.vaughanThird_zero (u v : ℕ) : vaughanThird 0 u v = 0

vaughanThird 0 u v = 0: the filtered divisor set of 0 is empty.

theorem AnalyticNumberTheory.Sieve.v3_vonMangoldt_nonneg (e : ℕ) : 0 ≤ ArithmeticFunction.vonMangoldt e

Nonnegativity of von Mangoldt, an alias for mathlib's ArithmeticFunction.vonMangoldt_nonneg.

theorem AnalyticNumberTheory.Sieve.vaughanThird_abs_le (n u v : ℕ) : |vaughanThird n u v| ≤ ↑n.divisors.card * Real.log (↑n + 1)

Pointwise V3 bound: |vaughanThird(n,u,v)| ≤ τ(n)·log(n+1), where τ(n) = n.divisors.card. The bilinear inner sum is bounded by Σ_{e|n/d} Λ(e) = log(n/d) using vonMangoldt_sum and Λ ≥ 0; the outer coefficients satisfy |μ(d)| ≤ 1. At n = 0, use vaughanThird 0 u v = 0.

2. Harmonic sums and multiple counts for the τ² estimate

theorem AnalyticNumberTheory.Sieve.v3_harmonic_Icc_le (M : ℕ) : ∑ k ∈ Finset.Icc 1 M, 1 / ↑k ≤ 1 + Real.log (↑M + 1)

Harmonic bound Σ_{k=1}^{M} 1/k ≤ 1+log(M+1), a consequence of mathlib's harmonic-sum estimates.

theorem AnalyticNumberTheory.Sieve.v3_card_multiples_Icc (N m : ℕ) (hm : 1 ≤ m) : {n ∈ Finset.Icc 1 N | m ∣ n}.card = N / m

Multiple count: #{n ∈ Icc 1 N : m | n} = N/m for m ≥ 1.

3. Reciprocal-lcm sums and Σ_{n≤N} τ(n)² ≤ N·(1+log(N+1))³

theorem AnalyticNumberTheory.Sieve.v3_lcm_inv_sum_le (N : ℕ) : ∑ d ∈ Finset.Icc 1 N, ∑ e ∈ Finset.Icc 1 N, 1 / ↑(d.lcm e) ≤ (1 + Real.log (↑N + 1)) ^ 3

Double reciprocal-lcm sum: Σ_{d,e≤N} 1/lcm(d,e) ≤ (1+log(N+1))³. Use lcm = de/gcd and gcd(d,e) = Σ_{g|d, g|e} φ(g) to write Σ_{d,e} 1/lcm(d,e) = Σ_{g≤N} (φ(g)/g²)·(Σ_{d'≤N/g} 1/d')². This is at most (1+log(N+1))²·Σ_{g≤N} φ(g)/g² ≤ (1+log(N+1))²·Σ_{g≤N} 1/g ≤ (1+log(N+1))³.

4. Summing τ(n)² up to N

theorem AnalyticNumberTheory.Sieve.v3_divisorCountSq_sum_le (N : ℕ) : ∑ n ∈ Finset.Icc 1 N, ↑n.divisors.card ^ 2 ≤ ↑N * (1 + Real.log (↑N + 1)) ^ 3

Divisor square-sum bound: Σ_{n≤N} τ(n)² ≤ N·(1+log(N+1))³. Double count τ(n)² = #{(d,e) : d|n, e|n} and exchange sums: Σ_{n≤N} τ(n)² = Σ_{d,e≤N} ⌊N/lcm(d,e)⌋.

5. Square-sum bound for vaughanThird

theorem AnalyticNumberTheory.Sieve.vaughanThird_l2_sum_le (u v : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ), ∑ n ∈ Finset.range (N + 1), vaughanThird n u v ^ 2 ≤ C * ↑N * (1 + Real.log (↑N + 1)) ^ 5

Vaughan V3 square-sum bound: Σ_{n≤N} vaughanThird(n,u,v)² ≤ N·(1+log(N+1))⁵, using the elementary pointwise bound |vaughanThird| ≤ τ·log and the divisor square-sum bound.

6. Per-modulus large-sieve reduction of character square sums

theorem AnalyticNumberTheory.Sieve.panTypeIICharSqSum_le_additiveSieve (q m u v : ℕ) (hq : 0 < q) : panTypeIICharSqSum q m u v ≤ ↑q.totient / ↑q * LargeSieve.largeSieveBound (m + 1) (1 / ↑q ^ 2) * ∑ n ∈ Finset.range (m + 1), vaughanThird n u v ^ 2

Per-modulus character square-sum bound: for q ≥ 1, Σ_χ ‖V_χ(m)‖² ≤ (φ(q)/q)·largeSieveBound(m+1,1/q²)·Σ_{n≤m} vaughanThird(n,u,v)². Combine characterSieveModulus_le and largeSieveRationalPoints. This is only a per-modulus estimate; it does not establish panTypeIICharSquareMeanBound over q ≤ Q. Primitive-character and Gauss-sum analysis, with additional all-character control, is needed for that separate mean-value question.

7. Replacing panTypeIICharSqrtMeanMaxY by a sum over y

theorem AnalyticNumberTheory.Sieve.panTypeIICharSqrtMeanMaxY_le_sum (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : panTypeIICharSqrtMeanMaxY X q x f u v ≤ ∑ y ∈ Finset.range (x + 1), panTypeIICharSqrtMean y X q f u v

Maximum-to-sum bound: panTypeIICharSqrtMeanMaxY ≤ Σ_{y≤x} panTypeIICharSqrtMean y, since the summands are nonnegative.

8. Character square sums bounded by the sieve constant and the V3 square sum

theorem AnalyticNumberTheory.Sieve.panTypeIICharSqrtMeanMaxY_le_sieveSqrtSum (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hq : 0 < q) : panTypeIICharSqrtMeanMaxY X q x f u v ≤ ∑ y ∈ Finset.range (x + 1), ∑ a ∈ Finset.Icc 1 X, |f a| / |Real.log ↑(y / a)| * √(↑q.totient / ↑q * LargeSieve.largeSieveBound (y / a + 1) (1 / ↑q ^ 2)) * √(∑ n ∈ Finset.range (y / a + 1), vaughanThird n u v ^ 2)

Expanded per-modulus reduction: after removing the maximum, bound panTypeIICharSqrtMeanMaxY by elementary quantities. For each y ≤ x, a ≤ X, √(Σ_χ‖V_χ(y/a)‖²) ≤ √((φ(q)/q)·largeSieveBound(y/a+1,1/q²)) ·√(Σ_{n≤y/a} vaughanThird(n,u,v)²). Only the sieve constant, V3 square sum, and outer weights remain. A mean over moduli is a separate step involving Gauss-sum and primitive-character analysis.