Valuations of the pole values μ_X(1/(t + j²)) = j⁴(X - H⁽⁵⁾_j) - 1/4 + 1/(2j)

theorem Zeta5Irrational.VG_inv_nat_le {p : ℕ} [hp : Fact (Nat.Prime p)] {u : ℕ} (hu : u ≠ 0) {e : ℕ} (he : padicValNat p u ≤ e) : VG p (↑u)⁻¹ (-↑e)

v_p(1/u) ≥ -e if v_p(u) ≤ e.

theorem Zeta5Irrational.padicValNat_lt_p {p u : ℕ} (hu : 1 ≤ u) (hup : u < p) : padicValNat p u = 0

theorem Zeta5Irrational.padicValNat_lt_sq {p : ℕ} [hp : Fact (Nat.Prime p)] {u : ℕ} (hu : 1 ≤ u) (hup : u < p ^ 2) : padicValNat p u ≤ 1

theorem Zeta5Irrational.VG_H5_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {j : ℕ} (hj : j < p) : VG p (H5 j) 0

theorem Zeta5Irrational.VG_quarter {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) : VG p (1 / 4) 0

theorem Zeta5Irrational.VG_inv_2j {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {j e : ℕ} (hj : 1 ≤ j) (he : padicValNat p j ≤ e) : VG p (1 / (2 * ↑j)) (-↑e)

theorem Zeta5Irrational.GV_poleValue_lt {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {j : ℕ} (hj : 1 ≤ j) (hjp : j < p) : GV p (poleValue j) 0

Integral pole values for 1 ≤ j < p.

theorem Zeta5Irrational.GV_poleValue_sq {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {j : ℕ} (hj : 1 ≤ j) (hjp : j < p ^ 2) : GV p (poleValue j) (-5)

Pole values ≥ -5 for 1 ≤ j < p².

theorem Zeta5Irrational.GV_poleValue_mul {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {k : ℕ} (hk : 1 ≤ k) (hkp : k < p) : GV p (poleValue (p * k)) (-1)

Pole values ≥ -1 for j = p k, 1 ≤ k < p.

theorem Zeta5Irrational.VG_int_dvd_one {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ} (h : ↑p ∣ z) : VG p (↑z) 1

theorem Zeta5Irrational.VG_pair {p : ℕ} [hp : Fact (Nat.Prime p)] (_hp3 : 3 ≤ p) {u : ℕ} (hu : 1 ≤ u) (hup : u < p) : VG p (1 / (↑p - ↑u) ^ 5 + 1 / ↑u ^ 5) 1

1/(p-u)⁵ + 1/u⁵ ≡ 0 (mod p).

theorem Zeta5Irrational.VG_H5_pm1 {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) : VG p (H5 (p - 1)) 1

H⁽⁵⁾_{p-1} ≡ 0 (mod p).

theorem Zeta5Irrational.H5_succ' {j : ℕ} (hj : 1 ≤ j) : H5 j = H5 (j - 1) + 1 / ↑j ^ 5

theorem Zeta5Irrational.H5_split {p c : ℕ} (hc : 1 ≤ c) (hcp : c < p) : H5 (p - 1) = H5 (p - c) + ∑ u ∈ Finset.Icc 1 (c - 1), 1 / (↑p - ↑u) ^ 5

theorem Zeta5Irrational.GV_poleValue_congr {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {c : ℕ} (hc : 1 ≤ c) (hcp : c < p) : GV p (poleValue (p - c) - poleValue c) 1

The congruence poleValue (p - c) ≡ poleValue c (mod p) for 1 ≤ c < p.