The outer-range basis

For p = 2m + 1 and the tail poles j ∈ (N, K], grouped by class jc j (j ≡ ±c): row (c, i) (i < Lo c) is tpol (rootsO c i) with rootsO c i = {tail poles of other classes} + (i < nb c ? i·{c} : big c + (i - nb c)·{c}), where big c are the tail poles of class c above p.

def Zeta5Irrational.jc {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (j : ℕ) : Fin (m + 1)

The class of a natural number.

Equations

• Zeta5Irrational.jc hm j = Zeta5Irrational.ccls hm ↑↑j

theorem Zeta5Irrational.sq_eq_iff_ccls {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (x y : ZMod p) : x ^ 2 = y ^ 2 ↔ ccls hm x = ccls hm y

def Zeta5Irrational.tailO (n : ℕ) : Finset ℕ

Tail poles N < j ≤ K.

Equations

• Zeta5Irrational.tailO n = Finset.Icc (3 * n + 1) (40 * n)

def Zeta5Irrational.tailC {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) : Finset ℕ

Outer pole indices belonging to the residue class c.

Equations

• Zeta5Irrational.tailC hm n c = {j ∈ Zeta5Irrational.tailO n | Zeta5Irrational.jc hm j = c}

def Zeta5Irrational.LoC {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) : ℕ

Number of rows allocated to the outer residue class c.

Equations

• Zeta5Irrational.LoC hm n c = (Zeta5Irrational.tailC hm n c).card

def Zeta5Irrational.bigC {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) : Finset ℕ

Outer pole indices in class c that exceed the prime p.

Equations

• Zeta5Irrational.bigC hm n c = {j ∈ Zeta5Irrational.tailC hm n c | p < j}

def Zeta5Irrational.nbC {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) : ℕ

Number of outer poles in class c that exceed p.

Equations

• Zeta5Irrational.nbC hm n c = (Zeta5Irrational.bigC hm n c).card

def Zeta5Irrational.rootsO {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) (i : ℕ) : Multiset ℤ

The roots of the outer row (c, i).

Equations

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

theorem Zeta5Irrational.sum_LoC {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) : ∑ c : Fin (m + 1), LoC hm n c = 37 * n

theorem Zeta5Irrational.card_rootsO {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) {i : ℕ} (hi : i < LoC hm n c) : (rootsO hm n c i).card < 37 * n

theorem Zeta5Irrational.ccls_self {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (c : Fin (m + 1)) : ccls hm ↑↑↑c = c

The class of a class representative is itself.

theorem Zeta5Irrational.sq_jc {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (j : ℕ) : ↑↑j ^ 2 = ↑↑↑(jc hm j) ^ 2

def Zeta5Irrational.γO {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (c : Fin (m + 1)) : ZMod p

γ_c = -c² in 𝔽_p.

Equations

• Zeta5Irrational.γO c = -↑↑↑c ^ 2

theorem Zeta5Irrational.map_factor {p : ℕ} [hp : Fact (Nat.Prime p)] (γ : ℤ) : Polynomial.map (Int.castRingHom (ZMod p)) (Polynomial.X + Polynomial.C (γ ^ 2)) = Polynomial.X - Polynomial.C (-↑γ ^ 2)

theorem Zeta5Irrational.prod_map_const_pow {p : ℕ} [hp : Fact (Nat.Prime p)] {s : Finset ℕ} {f : ℕ → Polynomial (ZMod p)} {q : Polynomial (ZMod p)} (h : ∀ j ∈ s, f j = q) : ∏ j ∈ s, f j = q ^ s.card

theorem Zeta5Irrational.rootsO_map_ZMod {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : 2 * m + 1 = p) (n : ℕ) (c : Fin (m + 1)) (i : ℕ) : Polynomial.map (Int.castRingHom (ZMod p)) (tpolZ (rootsO hm n c i)) = (∏ c' ∈ Finset.univ.erase c, (Polynomial.X - Polynomial.C (γO c')) ^ LoC hm n c') * (Polynomial.X - Polynomial.C (γO c)) ^ i

Reduction of the outer rows mod p.