Dedekind sums through the sawtooth function

DedekindSum.saw k n = ((n/k)) for n : ℤ, 0 < k (0 when k ∣ n, otherwise (n mod k)/k − 1/2), and DedekindSum.ded h k = s(h, k) = ∑_{r mod k} ((r/k)) ((hr/k)). Mathlib has neither (checked at the pinned commit).

Main results

• DedekindSum.ded_congr: s(h, k) depends only on h mod k.
• DedekindSum.ded_neg: s(−h, k) = −s(h, k).
• DedekindSum.ded_reciprocity: s(h, k) + s(k, h) = (h² + k² + 1)/(12hk) − 1/4 for coprime h, k ≥ 1 (elementary proof: the permutation r ↦ hr mod k and a lattice-point count of ∑ ⌊hr/k⌋²).
• DedekindSum.ded_inv: s(h⁻¹, k) = s(h, k).
• DedekindSum.saw_dist: the distribution relation ∑_{j<q} (((n + jm)/(qm))) = ((n/m)).
• DedekindSum.ded_scale: s(qy, qm) = s(y, m).
• DedekindSum.petersson_knopp_prime: for q prime, ∑_{l<q} s(x + lm, qm) = (q + 1) s(x, m) − s(qx, m).
• DedekindSum.petersson_knopp_coprime_lifts: the version for q ∤ m, qy ≡ x (mod m).

References

• S. R. Louboutin and M. Munsch, Canad. J. Math. 75 (2023), 1711–1743, arXiv:2205.01024 (its Conjecture 5.7 is the motivation).

def DedekindSum.saw (k : ℕ) (n : ℤ) : ℚ

The sawtooth ((n/k)).

Equations

• DedekindSum.saw k n = if n % ↑k = 0 then 0 else ↑(n % ↑k) / ↑k - 1 / 2

def DedekindSum.ded (h : ℤ) (k : ℕ) : ℚ

The Dedekind sum s(h,k) = Σ_{r=0}^{k-1} ((r/k)) ((hr/k)).

Equations

• DedekindSum.ded h k = ∑ r ∈ Finset.range k, DedekindSum.saw k ↑r * DedekindSum.saw k (h * ↑r)

theorem DedekindSum.saw_emod (k : ℕ) (n : ℤ) : saw k (n % ↑k) = saw k n

theorem DedekindSum.saw_congr {k : ℕ} {n n' : ℤ} (h : n ≡ n' [ZMOD ↑k]) : saw k n = saw k n'

theorem DedekindSum.ded_congr {h h' : ℤ} {k : ℕ} (hh : h ≡ h' [ZMOD ↑k]) : ded h k = ded h' k

(a) s(h,k) depends only on h mod k.

theorem DedekindSum.saw_neg {k : ℕ} (hk : 0 < k) (n : ℤ) : saw k (-n) = -saw k n

theorem DedekindSum.ded_neg (h : ℤ) (k : ℕ) : ded (-h) k = -ded h k

(b) s(−h,k) = −s(h,k).

Two-term reciprocity (and the inverse symmetry of (F2))

theorem DedekindSum.perm_sum {h k : ℕ} (hc : h.Coprime k) (F : ℕ → ℚ) : ∑ r ∈ Finset.range k, F (h * r % k) = ∑ r ∈ Finset.range k, F r

Multiplication by a unit permutes the residues 0, …, k-1.

theorem DedekindSum.ded_inv {h h' k : ℕ} (hinv : h * h' ≡ 1 [MOD k]) : ded (↑h') k = ded (↑h) k

(F2) s(h⁻¹,k) = s(h,k): if h h' ≡ 1 (mod k) then s(h',k) = s(h,k).

theorem DedekindSum.sum_id (k : ℕ) : ∑ r ∈ Finset.range k, ↑r = ↑k * (↑k - 1) / 2

theorem DedekindSum.sum_sq (k : ℕ) : ∑ r ∈ Finset.range k, ↑r ^ 2 = (↑k - 1) * ↑k * (2 * ↑k - 1) / 6

theorem DedekindSum.sum_odd (n : ℕ) : ∑ i ∈ Finset.Ico 1 (n + 1), (2 * ↑i - 1) = ↑n ^ 2

theorem DedekindSum.rho_cast (h k r : ℕ) : ↑(h * r % k) = ↑h * ↑r - ↑k * ↑(h * r / k)

def DedekindSum.P (h k : ℕ) : ℚ

P h k = Σ r ⌊hr/k⌋, Q h k = Σ ⌊hr/k⌋², M h k = Σ ⌊hr/k⌋ (r over range k).

Equations

• DedekindSum.P h k = ∑ r ∈ Finset.range k, ↑r * ↑(h * r / k)

def DedekindSum.Q (h k : ℕ) : ℚ

Equations

• DedekindSum.Q h k = ∑ r ∈ Finset.range k, ↑(h * r / k) ^ 2

def DedekindSum.M (h k : ℕ) : ℚ

Equations

• DedekindSum.M h k = ∑ r ∈ Finset.range k, ↑(h * r / k)

theorem DedekindSum.eqn1 {h k : ℕ} (hc : h.Coprime k) : ↑h * (↑k * (↑k - 1) / 2) - ↑k * M h k = ↑k * (↑k - 1) / 2

Σ (hr mod k) = Σ r.

theorem DedekindSum.eqn2 {h k : ℕ} (hc : h.Coprime k) : ↑h ^ 2 * ((↑k - 1) * ↑k * (2 * ↑k - 1) / 6) - 2 * ↑h * ↑k * P h k + ↑k ^ 2 * Q h k = (↑k - 1) * ↑k * (2 * ↑k - 1) / 6

Σ (hr mod k)² = Σ r².

theorem DedekindSum.ded_formula {h k : ℕ} (hc : h.Coprime k) (hk : 0 < k) : ded (↑h) k = ↑h * ((↑k - 1) * ↑k * (2 * ↑k - 1) / 6) / ↑k ^ 2 - P h k / ↑k - ↑k * (↑k - 1) / 2 / (2 * ↑k) - ↑h * (↑k * (↑k - 1) / 2) / (2 * ↑k) + M h k / 2 + ↑k / 4 - 1 / 4

s(h,k) through P and M.

theorem DedekindSum.sq_as_sum {h k r : ℕ} (hh : 0 < h) (hk : 0 < k) (hr : r < k) : ↑(h * r / k) ^ 2 = ∑ i ∈ Finset.Ico 1 h, if k * i ≤ h * r then 2 * ↑i - 1 else 0

For r < k: ⌊hr/k⌋² = Σ_{1 ≤ i < h, ki ≤ hr} (2i − 1).

theorem DedekindSum.count_as_sum {h k i : ℕ} (hh : 0 < h) (hk : 0 < k) (hi : i < h) : ↑(k * i / h) + 1 = ∑ r ∈ Finset.range k, if h * r ≤ k * i then 1 else 0

For 1 ≤ i < h: #{r < k : hr ≤ ki} = ⌊ki/h⌋ + 1.

theorem DedekindSum.eqn3 {h k : ℕ} (hc : h.Coprime k) (hh : 0 < h) (hk : 0 < k) : Q h k + 2 * P k h - M k h + (↑h - 1) ^ 2 = ↑k * (↑h - 1) ^ 2

Lattice-point double count: Q h k + 2 P k h − M k h + (h−1)² = k (h−1)².

theorem DedekindSum.ded_reciprocity {h k : ℕ} (hc : h.Coprime k) (hh : 0 < h) (hk : 0 < k) : ded (↑h) k + ded (↑k) h = (↑h ^ 2 + ↑k ^ 2 + 1) / (12 * ↑h * ↑k) - 1 / 4

(c) Dedekind reciprocity. For coprime positive integers h, k, s(h,k) + s(k,h) = (h² + k² + 1)/(12hk) − 1/4.

(d) Distribution relation (F3)

theorem DedekindSum.saw_scale {q m : ℕ} (hq : 0 < q) (hm : 0 < m) (n : ℤ) : saw (q * m) (↑q * n) = saw m n

((qn/(qm))) = ((n/m)).

theorem DedekindSum.saw_of_lt {k : ℕ} {n : ℤ} (h0 : 0 ≤ n) (hlt : n < ↑k) : saw k n = ↑n / ↑k - 1 / 2 + if n = 0 then 1 / 2 else 0

theorem DedekindSum.shift_sum (q : ℕ) (H : ℤ → ℚ) (hH : ∀ (t : ℤ), H (t + ↑q) = H t) (a : ℤ) : ∑ j ∈ Finset.range q, H (a + ↑j) = ∑ j ∈ Finset.range q, H ↑j

A q-periodic function has the same sum over any q consecutive integers.

theorem DedekindSum.saw_dist {q m : ℕ} (hq : 0 < q) (hm : 0 < m) (n : ℤ) : ∑ j ∈ Finset.range q, saw (q * m) (n + ↑j * ↑m) = saw m n

(F3) Discrete distribution relation: Σ_{j<q} (((n + jm)/(qm))) = ((n/m)).

(d) Lemma 1: the prime case of the Petersson–Knopp identity

theorem DedekindSum.sum_range_mul (q m : ℕ) (f : ℕ → ℚ) : ∑ r ∈ Finset.range (q * m), f r = ∑ j ∈ Finset.range q, ∑ i ∈ Finset.range m, f (j * m + i)

theorem DedekindSum.inner_value {q m : ℕ} (hq : Nat.Prime q) (hm : 0 < m) (x : ℤ) (r : ℕ) : ∑ l ∈ Finset.range q, saw (q * m) ((x + ↑l * ↑m) * ↑r) = saw m (x * ↑r) + if q ∣ r then ↑q * saw m (x * ↑(r / q)) - saw m (x * ↑r) else 0

The inner sum over l in Lemma 1.

theorem DedekindSum.lift_sum {q m : ℕ} (hq0 : 0 < q) (hm : 0 < m) (x : ℤ) : ∑ r ∈ Finset.range (q * m), saw (q * m) ↑r * saw m (x * ↑r) = ∑ r ∈ Finset.range m, saw m ↑r * saw m (x * ↑r)

Σ_{r<qm} ((r/(qm))) ((xr/m)) = s(x,m) (split r = jm + i, then (F3)).

theorem DedekindSum.ded_scale {q m : ℕ} (hq0 : 0 < q) (hm : 0 < m) (y : ℤ) : ded (↑q * y) (q * m) = ded y m

(F4), the instance used in Corollary 1′: s(qy, qm) = s(y, m).

theorem DedekindSum.petersson_knopp_prime {q m : ℕ} (hq : Nat.Prime q) (hm : 0 < m) (x : ℤ) : ∑ l ∈ Finset.range q, ded (x + ↑l * ↑m) (q * m) = (↑q + 1) * ded x m - ded (↑q * x) m

Lemma 1 (prime case of Petersson–Knopp): for a prime q, m ≥ 1, x ∈ ℤ, Σ_{l<q} s(x + lm, qm) = (q+1) s(x,m) − s(qx,m).

theorem DedekindSum.petersson_knopp_coprime_lifts {q m : ℕ} (hq : Nat.Prime q) (hm : 0 < m) (hqm : ¬q ∣ m) (x y : ℤ) (hy : ↑q * y ≡ x [ZMOD ↑m]) : (∑ l ∈ Finset.range q, if ↑q ∣ x + ↑l * ↑m then 0 else ded (x + ↑l * ↑m) (q * m)) = (↑q + 1) * ded x m - ded (↑q * x) m - ded y m

Corollary 1′ (coprime lifts). For a prime q ∤ m and y with q y ≡ x (mod m) (i.e. y = q⁻¹x mod m): the sum over the l < q with q ∤ x + lm equals (q+1) s(x,m) − s(qx,m) − s(q⁻¹x,m).