AnalyticNumberTheory.Sieve.PanV1SquareMean

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

This module proves two components relevant to panTypeICharMeanSieveBound and PanTypeICharacterMeanValue (PanMeanValueBody.lean §§5--5.1):

1. Elementary square-sum bound: Σ_{n≤N} vaughanFirst(n,u)² ≤ N·(1+log(N+1))⁵. First use |vaughanFirst(n,u)| ≤ τ(n)·log(n+1), where τ(n) = n.divisors.card and |μ(d)| ≤ 1. Double counting gives Σ_{n≤N} τ(n)² = Σ_{d,e≤N} ⌊N/lcm(d,e)⌋. Then gcd·lcm = de and gcd = Σ_{g|gcd} φ(g) reduce the reciprocal-lcm sum to Σ_g (φ(g)/g²)·H(N/g)² ≤ (1+log(N+1))³. Harmonic estimates come from Mathlib.NumberTheory.Harmonic.
2. Per-modulus character square-sum bound: Σ_χ ‖V_χ(m)‖² ≤ (φ(q)/q)·largeSieveBound(m+1,1/q²)·Σ_{n≤m} vaughanFirst(n,u)². Combine characterSieveModulus_le with largeSieveRationalPoints, then replace the y-maximum by a sum to obtain panTypeICharSqrtMeanMaxY_le_sieveSqrtSum.

These are per-modulus bounds, not a proof of the all-character panTypeICharSquareMeanBound summed over q ≤ Q. The classical Bombieri--Davenport argument uses primitive characters and Gauss sums |τ(χ)|² = q; an all-character extension requires additional control. The final bound here leaves only the additive large-sieve constant, the vaughanFirst L² sum, and the outer (y,a) weights.

1. Elementary pointwise bound for vaughanFirst

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

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

theorem AnalyticNumberTheory.Sieve.vaughanFirst_zero (u : ℕ) : vaughanFirst 0 u = 0

vaughanFirst 0 u = 0 (0.divisors = ∅).

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

Pointwise bound: |vaughanFirst(n,u)| ≤ τ(n)·log(n+1), with τ(n) = n.divisors.card. The case n = 0 is trivial because vaughanFirst 0 u = 0.

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

theorem AnalyticNumberTheory.Sieve.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.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.pan_lcm_inv_eq_gcd_div {d e : ℕ} (hd : 1 ≤ d) (he : 1 ≤ e) : 1 / ↑(d.lcm e) = ↑(d.gcd e) / (↑d * ↑e)

1/lcm(d,e) = gcd(d,e)/(d·e) in ℝ, for d,e ≥ 1.

theorem AnalyticNumberTheory.Sieve.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.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 vaughanFirst

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

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

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

theorem AnalyticNumberTheory.Sieve.pan_sum_range_to_Icc_int {m : ℕ} {β : Type u_1} [AddCommMonoid β] (f : ℕ → β) (g : ℤ → β) (hfg : ∀ (n : ℕ), f n = g ↑n) : ∑ n ∈ Finset.range (m + 1), f n = ∑ n ∈ Finset.Icc 0 ↑m, g n

Reindex an ℕ range sum as an ℤ interval sum using the natural embedding n ↦ n.

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

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

7. Replacing panTypeICharSqrtMeanMaxY by a sum over y

theorem AnalyticNumberTheory.Sieve.panTypeICharSqrtMeanMaxY_le_sum (X q x : ℕ) (f : ℕ → ℝ) (u : ℕ) : panTypeICharSqrtMeanMaxY X q x f u ≤ ∑ y ∈ Finset.range (x + 1), panTypeICharSqrtMean y X q f u

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

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

theorem AnalyticNumberTheory.Sieve.panTypeICharSqrtMeanMaxY_le_sieveSqrtSum (X q x : ℕ) (f : ℕ → ℝ) (u : ℕ) (hq : 0 < q) : panTypeICharSqrtMeanMaxY X q x f u ≤ ∑ 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), vaughanFirst n u ^ 2)

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