the proof notes, §1 (Corollary 2): the local functional on a disc, in a finite rational form.

For 0 ≤ b < p put t = p u - b (the variable u is written X). For f = A / D_{5n} the dissected function g_b(u) = (t f)(p u - b) is g_b = p^{-|near_b|} · dissectNum(u) / (nearProd(u) · farProd(u)), where

• nearSet n p b = {m = (j - b)/p : j ∈ [1, 5n], j ≡ b (mod p)} (near poles u = -m),
• nearProd = ∏_{m ∈ nearSet} (u + m),
• farProd = ∏_{j ∈ [1,5n], j ≢ b} ((j - b) + p u) (constant term a p-unit),
• dissectNum = (t · A)(p u - b). seriesPart is the power series dissectNum / farProd ∈ ℚ[[u]] truncated to degree < 10n + 2.

The local functional (the X-free part of V_Y, Corollary 2) on S / ∏_{m ∈ M} (u + m): V(u^e) = e B_{e-1} + 2 s B_e (B = bernoulli', B_1 = +1/2), and V((u+m)^{-1}) = 2 H_m^{(3)} - 2 s H_m^{(2)} (the -2Y part is dropped; Y ∈ p³ ℤ_p[X]). s = r p gives V_Y without Y; s = 0 gives V⁰.

def Zeta32.PrimeEdge.nearSet (n p b : ℕ) : Finset ℕ

Near poles on the disc b.

Equations

• Zeta32.PrimeEdge.nearSet n p b = Finset.image (fun (j : ℕ) => (j - b) / p) ({j ∈ Finset.Icc 1 (5 * n) | j % p = b})

noncomputable def Zeta32.PrimeEdge.nearProd (n p b : ℕ) : Polynomial ℚ

Denominator factors in the residue class selected by b.

Equations

• Zeta32.PrimeEdge.nearProd n p b = ∏ m ∈ Zeta32.PrimeEdge.nearSet n p b, (Polynomial.X + Polynomial.C ↑m)

noncomputable def Zeta32.PrimeEdge.farProd (n p b : ℕ) : Polynomial ℚ

Transformed denominator factors outside the residue class selected by b.

Equations

• Zeta32.PrimeEdge.farProd n p b = ∏ j ∈ Finset.Icc 1 (5 * n) with j % p ≠ b, (Polynomial.C (↑j - ↑b) + Polynomial.C ↑p * Polynomial.X)

noncomputable def Zeta32.PrimeEdge.dissectNum (p b : ℕ) (A : Polynomial ℚ) : Polynomial ℚ

(t · A)(p u - b) as a polynomial in u.

Equations

• Zeta32.PrimeEdge.dissectNum p b A = (Polynomial.X * A).comp (Polynomial.C ↑p * Polynomial.X - Polynomial.C ↑b)

def Zeta32.PrimeEdge.truncOrder (n : ℕ) : ℕ

Truncation order of the far-pole expansions.

Equations

• Zeta32.PrimeEdge.truncOrder n = 10 * n + 2

noncomputable def Zeta32.PrimeEdge.seriesPart (n p b : ℕ) (A : Polynomial ℚ) : Polynomial ℚ

dissectNum / farProd, expanded in ℚ[[u]] and truncated to degree < truncOrder n.

Equations

• Zeta32.PrimeEdge.seriesPart n p b A = (PowerSeries.trunc (Zeta32.PrimeEdge.truncOrder n)) (↑(Zeta32.PrimeEdge.dissectNum p b A) * (↑(Zeta32.PrimeEdge.farProd n p b))⁻¹)

def Zeta32.PrimeEdge.locMoment (s : ℚ) (e : ℕ) : ℚ

V(u^e) = e B_{e-1} + 2 s B_e.

Equations

• Zeta32.PrimeEdge.locMoment s e = ↑e * bernoulli' (e - 1) + 2 * s * bernoulli' e

def Zeta32.PrimeEdge.locPoly (s : ℚ) (P : Polynomial ℚ) : ℚ

Linear extension of the local moments to a polynomial.

Equations

• Zeta32.PrimeEdge.locPoly s P = P.sum fun (e : ℕ) (a : ℚ) => a * Zeta32.PrimeEdge.locMoment s e

def Zeta32.PrimeEdge.locPole (s : ℚ) (m : ℕ) : ℚ

V((u+m)^{-1}) without the -2Y part.

Equations

• Zeta32.PrimeEdge.locPole s m = 2 * Zeta32.H 3 m - 2 * s * Zeta32.H 2 m

noncomputable def Zeta32.PrimeEdge.locValue (s : ℚ) (S : Polynomial ℚ) (M : Finset ℕ) : ℚ

The local functional on S / ∏_{m ∈ M} (u + m) (polynomial part plus Lagrange residues).

Equations

• One or more equations did not get rendered due to their size.

theorem Zeta32.PrimeEdge.locPoly_add_linear (s : ℚ) (P Q : Polynomial ℚ) : locPoly s (P + Q) = locPoly s P + locPoly s Q

theorem Zeta32.PrimeEdge.locPoly_C_mul_linear (s c : ℚ) (P : Polynomial ℚ) : locPoly s (Polynomial.C c * P) = c * locPoly s P

theorem Zeta32.PrimeEdge.locPoly_zero_linear (s : ℚ) : locPoly s 0 = 0

theorem Zeta32.PrimeEdge.locValue_add_linear (s : ℚ) (S T : Polynomial ℚ) (M : Finset ℕ) : locValue s (S + T) M = locValue s S M + locValue s T M

theorem Zeta32.PrimeEdge.locValue_C_mul_linear (s c : ℚ) (S : Polynomial ℚ) (M : Finset ℕ) : locValue s (Polynomial.C c * S) M = c * locValue s S M

theorem Zeta32.PrimeEdge.locValue_zero_linear (s : ℚ) (M : Finset ℕ) : locValue s 0 M = 0

theorem Zeta32.PrimeEdge.locValue_sum_linear {ι : Type u_1} (s : ℚ) (t : Finset ι) (S : ι → Polynomial ℚ) (M : Finset ℕ) : locValue s (∑ i ∈ t, S i) M = ∑ i ∈ t, locValue s (S i) M

noncomputable def Zeta32.PrimeEdge.discLocal (r : ℚ) (n p b : ℕ) (A : Polynomial ℚ) : ℚ

V_Y(g_b) without the Y part, with far poles truncated: p^{-|near|} V(seriesPart / nearProd).

Equations

• Zeta32.PrimeEdge.discLocal r n p b A = ↑p ^ (-↑(Zeta32.PrimeEdge.nearSet n p b).card) * Zeta32.PrimeEdge.locValue (r * ↑p) (Zeta32.PrimeEdge.seriesPart n p b A) (Zeta32.PrimeEdge.nearSet n p b)

noncomputable def Zeta32.PrimeEdge.blockMoment (p b e : ℕ) : ℚ

V⁰(u^e r_type) for the three class types of §6: zero r_0 = u/((u+1)…(u+4)), low r_L = u³/((u+1)…(u+4)), high r_H = u³/((u+1)(u+2)(u+3)).

Equations

• One or more equations did not get rendered due to their size.