Class sums and their continuous limits

For p = 2m + 1 and 0 ≤ v, v' < p put, for 1 ≤ c ≤ m, a_c = [c ≤ v] + [p - v ≤ c] and a'_c = [c ≤ v'] + [p - v' ≤ c]. Every function h of (a_c, a'_c) is a combination of the products of the interval indicators 1 = [1 ≤ c ≤ m], A = [c ≤ v], E = [p - v ≤ c], so ∑_c h(a_c, a'_c) is a combination of nine interval counts. Each count is within 5/2 of p times its continuous analogue, where v/p = f, v'/p = g.

We also prove SX p X c = 2 ⌊X/p⌋ + a_c(X mod p).

def Zeta5Irrational.ivLo (p v : ℕ) : Fin 3 → ℕ

The interval [lo i, hi i] of the indicator i ∈ {1, A, E}.

Equations

• Zeta5Irrational.ivLo p v = ![1, 1, p - v]

def Zeta5Irrational.ivHi (m v : ℕ) : Fin 3 → ℕ

Upper endpoints of the three discrete intervals used in the class-count expansion.

Equations

• Zeta5Irrational.ivHi m v = ![m, v, m]

noncomputable def Zeta5Irrational.cvLo (f : ℝ) : Fin 3 → ℝ

The continuous intervals.

Equations

• Zeta5Irrational.cvLo f = ![0, 0, 1 - f]

noncomputable def Zeta5Irrational.cvHi (f : ℝ) : Fin 3 → ℝ

Upper endpoints of the continuous intervals corresponding to ivHi.

Equations

• Zeta5Irrational.cvHi f = ![1 / 2, f, 1 / 2]

def Zeta5Irrational.bcoef (h : ℕ → ℝ) : Fin 3 → ℝ

The coefficients of h in the basis 1, A, E.

Equations

• Zeta5Irrational.bcoef h = ![h 0, h 1 - h 0, h 2 - h 1]

def Zeta5Irrational.aCnt (p v c : ℕ) : ℕ

a(c) = [c ≤ v] + [p - v ≤ c].

Equations

• Zeta5Irrational.aCnt p v c = (if c ≤ v then 1 else 0) + if p - v ≤ c then 1 else 0

def Zeta5Irrational.ivInd (p m v : ℕ) (i : Fin 3) (c : ℕ) : ℝ

The interval indicator.

Equations

• Zeta5Irrational.ivInd p m v i c = if Zeta5Irrational.ivLo p v i ≤ c ∧ c ≤ Zeta5Irrational.ivHi m v i then 1 else 0

theorem Zeta5Irrational.expand_one {p m v c : ℕ} (hm : 2 * m + 1 = p) (hv : v < p) (hc1 : 1 ≤ c) (hcm : c ≤ m) (h : ℕ → ℝ) : h (aCnt p v c) = ∑ i : Fin 3, bcoef h i * ivInd p m v i c

theorem Zeta5Irrational.expand_two {p m v v' c : ℕ} (hm : 2 * m + 1 = p) (hv : v < p) (hv' : v' < p) (hc1 : 1 ≤ c) (hcm : c ≤ m) (h : ℕ → ℕ → ℝ) : h (aCnt p v c) (aCnt p v' c) = ∑ i : Fin 3, ∑ j : Fin 3, bcoef (fun (a : ℕ) => bcoef (fun (b : ℕ) => h a b) j) i * (ivInd p m v i c * ivInd p m v' j c)

theorem Zeta5Irrational.card_two_intervals (m lo hi lo' hi' : ℕ) : {c ∈ Finset.Icc 1 m | (lo ≤ c ∧ c ≤ hi) ∧ lo' ≤ c ∧ c ≤ hi'}.card = min (min hi hi') m + 1 - max (max lo lo') 1

The discrete count of an intersection of two intervals within [1, m].

theorem Zeta5Irrational.class_sum {p m v v' : ℕ} (hm : 2 * m + 1 = p) (hv : v < p) (hv' : v' < p) (h : ℕ → ℕ → ℝ) : ∑ c ∈ Finset.Icc 1 m, h (aCnt p v c) (aCnt p v' c) = ∑ i : Fin 3, ∑ j : Fin 3, bcoef (fun (a : ℕ) => bcoef (fun (b : ℕ) => h a b) j) i * ↑(min (min (ivHi m v i) (ivHi m v' j)) m + 1 - max (max (ivLo p v i) (ivLo p v' j)) 1)

Class sums as interval counts.

noncomputable def Zeta5Irrational.ccount (f g : ℝ) (i j : Fin 3) : ℝ

The continuous analogue of an interval count.

Equations

• Zeta5Irrational.ccount f g i j = max 0 (min (min (Zeta5Irrational.cvHi f i) (Zeta5Irrational.cvHi g j)) (1 / 2) - max (max (Zeta5Irrational.cvLo f i) (Zeta5Irrational.cvLo g j)) 0)

theorem Zeta5Irrational.cast_trunc_sub (a b : ℕ) : ↑(a - b) = max 0 (↑a - ↑b)

theorem Zeta5Irrational.abs_max0_sub (u w : ℝ) : |max 0 u - max 0 w| ≤ |u - w|

theorem Zeta5Irrational.hi_approx {p m v : ℕ} (hm : 2 * m + 1 = p) (_hv : v < p) (i : Fin 3) : |↑(ivHi m v i) - ↑p * cvHi (↑v / ↑p) i| ≤ 1 / 2

theorem Zeta5Irrational.lo_approx {p v : ℕ} (hv : v < p) (i : Fin 3) : |↑(ivLo p v i) - ↑p * cvLo (↑v / ↑p) i| ≤ 1

theorem Zeta5Irrational.count_approx {p m v v' : ℕ} (hm : 2 * m + 1 = p) (hv : v < p) (hv' : v' < p) (i j : Fin 3) : |↑(min (min (ivHi m v i) (ivHi m v' j)) m + 1 - max (max (ivLo p v i) (ivLo p v' j)) 1) - ↑p * ccount (↑v / ↑p) (↑v' / ↑p) i j| ≤ 5 / 2

Each interval count is within 5/2 of p times its continuous analogue.

theorem Zeta5Irrational.class_sum_approx {p m v v' : ℕ} (hm : 2 * m + 1 = p) (hv : v < p) (hv' : v' < p) (h : ℕ → ℕ → ℝ) : |∑ c ∈ Finset.Icc 1 m, h (aCnt p v c) (aCnt p v' c) - ↑p * ∑ i : Fin 3, ∑ j : Fin 3, bcoef (fun (a : ℕ) => bcoef (fun (b : ℕ) => h a b) j) i * ccount (↑v / ↑p) (↑v' / ↑p) i j| ≤ 5 / 2 * ∑ i : Fin 3, ∑ j : Fin 3, |bcoef (fun (a : ℕ) => bcoef (fun (b : ℕ) => h a b) j) i|

Class sums versus their continuous limit.