The distribution formula on one simple pole D_{5n} / (t + j).

• dl_near : on the disc b = j mod p the pole is near: dl = p^{-1} V^loc(1/(u + ⌊j/p⌋));
• dl_far : on the other discs it is far: dl = V^loc(trunc (near(u) / ((j - b) + p u)));
• VG_far : the far value is p-integral (Tate coefficients v ≥ e, von Staudt).

noncomputable def Zeta32.PrimeEdge.Ej (M : Finset ℕ) (j : ℕ) : Polynomial ℚ

D_S / (t + j).

Equations

• Zeta32.PrimeEdge.Ej M j = ∏ m' ∈ M.erase j, (Polynomial.X + Polynomial.C ↑m')

theorem Zeta32.PrimeEdge.Ej_mul {M : Finset ℕ} {j : ℕ} (hj : j ∈ M) : Ej M j * (Polynomial.X + Polynomial.C ↑j) = mprod M

theorem Zeta32.PrimeEdge.natDegree_Ej (M : Finset ℕ) (j : ℕ) : (Ej M j).natDegree = (M.erase j).card

theorem Zeta32.PrimeEdge.sum_ite_Ej (M : Finset ℕ) {j : ℕ} (hj : j ∈ M) : ∑ m ∈ M, Polynomial.C (if m = j then 1 else 0) * ∏ m' ∈ M.erase m, (Polynomial.X + Polynomial.C ↑m') = Ej M j

theorem Zeta32.PrimeEdge.locValue_Ej (s : ℚ) {M : Finset ℕ} {j : ℕ} (hj : j ∈ M) : locValue s (Ej M j) M = locPole s j

theorem Zeta32.PrimeEdge.Ej_comp_mul {M : Finset ℕ} {j : ℕ} (hj : j ∈ M) (p b : ℕ) : (Ej M j).comp (Polynomial.C ↑p * Polynomial.X - Polynomial.C ↑b) * (Polynomial.C (↑j - ↑b) + Polynomial.C ↑p * Polynomial.X) = (mprod M).comp (Polynomial.C ↑p * Polynomial.X - Polynomial.C ↑b)

theorem Zeta32.PrimeEdge.inv_lin (w q : ℚ) (hw : w ≠ 0) : (↑(Polynomial.C w + Polynomial.C q * Polynomial.X))⁻¹ = PowerSeries.mk fun (e : ℕ) => (-q) ^ e / w ^ (e + 1)

The inverse of w + q u in ℚ[[u]].

theorem Zeta32.PrimeEdge.dl_far {p : ℕ} (hp : 0 < p) (r : ℚ) (n b : ℕ) (hb : b < p) {j : ℕ} (hj : j ∈ Finset.Icc 1 (5 * n)) (hjb : j % p ≠ b) : dl r n p b (Ej (Finset.Icc 1 (5 * n)) j) = locValue (r * ↑p) ((PowerSeries.trunc (truncOrder n)) (↑(mprod (nearSet n p b)) * (↑(Polynomial.C (↑j - ↑b) + Polynomial.C ↑p * Polynomial.X))⁻¹)) (nearSet n p b)

Far pole on the disc b.

theorem Zeta32.PrimeEdge.dl_near {p : ℕ} (hp : 0 < p) (r : ℚ) (n : ℕ) {j : ℕ} (hj : j ∈ Finset.Icc 1 (5 * n)) : dl r n p (j % p) (Ej (Finset.Icc 1 (5 * n)) j) = (↑p)⁻¹ * locPole (r * ↑p) (j / p)

Near pole on the disc j mod p.

theorem Zeta32.PrimeEdge.VG_far {p : ℕ} [hp : Fact (Nat.Prime p)] {s : ℚ} (hs : Zeta5Irrational.VG p s 1) (near : Finset ℕ) (hnear : ∀ m ∈ near, m < p) (N : ℕ) (hN : near.card + 1 ≤ N) {w : ℚ} (hw0 : w ≠ 0) (hw : Zeta5Irrational.VG p w⁻¹ 0) : Zeta5Irrational.VG p (locValue s ((PowerSeries.trunc N) (↑(mprod near) * (↑(Polynomial.C w + Polynomial.C ↑p * Polynomial.X))⁻¹)) near) 0

Far values are integral.