Explicit floor-sum control of the quadratic Siegel convolution discrepancy

This file opens the divisor double sum and records the exact floor-sum form. The cutoff error is then separated into a short floor error and a genuinely oscillatory long tail. In particular, the floor error costs only the cutoff m, rather than the ambient length X.

theorem DirichletCharacter.abs_sum_range_mul_le_of_prefix (f w : ℕ → ℝ) (n : ℕ) (B : ℝ) (hB : 0 ≤ B) (hpref : ∀ k ≤ n, |∑ i ∈ Finset.range k, f i| ≤ B) (hw0 : ∀ (i : ℕ), 0 ≤ w i) (hwmono : ∀ (i : ℕ), i + 1 < n → w (i + 1) ≤ w i) : |∑ i ∈ Finset.range n, w i * f i| ≤ B * w 0

Finite Abel summation with a nonnegative decreasing weight. This is the form used below for w(d)=⌊X/d⌋; only interval-prefix cancellation is paid.

theorem DirichletCharacter.quadraticDivisorDoubleSum_eq_floorSum {q : ℕ} (χ : DirichletCharacter ℂ q) (X : ℕ) : ∑ n ∈ Finset.Icc 1 X, ∑ d ∈ n.divisors, (χ ↑d).re = ∑ d ∈ Finset.Icc 1 X, ↑(X / d) * (χ ↑d).re

Reindex the divisor double sum by the divisor. The multiplicity of d is exactly ⌊X/d⌋.

theorem DirichletCharacter.quadraticHarmonicTruncation_eq_Ico {q : ℕ} (χ : DirichletCharacter ℂ q) (m : ℕ) : χ.quadraticHarmonicTruncation m = ∑ d ∈ Finset.Ico 1 m, (χ ↑d).re / ↑d

At s=1, the real harmonic truncation is the ordinary finite sum ∑_{1≤d<m} Re χ(d)/d.

theorem DirichletCharacter.IsPrimitive.abs_sum_Ico_character_re_le_eight_mul_sqrt_q_mul_one_add_log {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ.IsPrimitive) (hq : 1 < q) (a b : ℕ) : |∑ n ∈ Finset.Ico a b, (χ ↑n).re| ≤ 8 * √↑q * (1 + Real.log ↑q)

Pólya--Vinogradov controls every real character interval, not merely prefixes.

theorem DirichletCharacter.IsPrimitive.abs_floorWeighted_character_tail_le {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ.IsPrimitive) (hq : 1 < q) {m X : ℕ} (hm : 1 ≤ m) (_hmX : m ≤ X) : |∑ d ∈ Finset.Icc m X, ↑(X / d) * (χ ↑d).re| ≤ 8 * √↑q * (1 + Real.log ↑q) * ↑(X / m)

The long floor-weighted tail is controlled by interval prefixes through finite Abel summation. This is the cancellation step which prevents a termwise O(X) bound.

theorem DirichletCharacter.quadraticSiegelConvolutionDiscrepancy_eq_floorSum_sub {q : ℕ} (χ : DirichletCharacter ℂ q) (X m : ℕ) : χ.quadraticSiegelConvolutionDiscrepancy X m = ∑ d ∈ Finset.Icc 1 X, ↑(X / d) * (χ ↑d).re - ↑X * ∑ d ∈ Finset.Ico 1 m, (χ ↑d).re / ↑d

Exact floor-sum expansion of the production discrepancy.