The degree of Δ_K and F_K — formula (2.9) of the paper

The entries of G_K(X) are affine in X; the coefficient of X^h in Δ_K = det G_K is the determinant of the matrix of X-coefficients, which is Vᵀ diag(w) V for the Vandermonde matrix V of the nodes -j², N < j ≤ K, with nonzero weights w. Hence deg Δ_K = h.

theorem Zeta5Irrational.coeff_det_of_natDegree_le_one {R : Type u_1} [CommRing R] {n : ℕ} (M : Matrix (Fin n) (Fin n) (Polynomial R)) (hM : ∀ (i j : Fin n), (M i j).natDegree ≤ 1) : M.det.coeff n = (Matrix.of fun (i j : Fin n) => (M i j).coeff 1).det ∧ M.det.natDegree ≤ n

noncomputable def Zeta5Irrational.res (K : ℕ) (P : Polynomial ℚ) (j : ℕ) : ℚ

Residue coefficient at the pole -j² of P / D K, for 1 ≤ j ≤ K.

Equations

• Zeta5Irrational.res K P j = Polynomial.eval (-↑j ^ 2) P / Polynomial.eval (-↑j ^ 2) (Polynomial.derivative (Zeta5Irrational.D K))

theorem Zeta5Irrational.poleValue_eq (j : ℕ) : poleValue j = Polynomial.C (↑j ^ 4) * Polynomial.X + Polynomial.C (-↑j ^ 4 * H5 j - 1 / 4 + 1 / (2 * ↑j))

theorem Zeta5Irrational.μX_eq (K : ℕ) (P : Polynomial ℚ) : μX K P = Polynomial.C (∑ j ∈ Finset.Icc 1 K, res K P j * ↑j ^ 4) * Polynomial.X + Polynomial.C (μpoly (P /ₘ D K) + ∑ j ∈ Finset.Icc 1 K, res K P j * (-↑j ^ 4 * H5 j - 1 / 4 + 1 / (2 * ↑j)))

theorem Zeta5Irrational.natDegree_μX_le (K : ℕ) (P : Polynomial ℚ) : (μX K P).natDegree ≤ 1

theorem Zeta5Irrational.coeff_μX_one (K : ℕ) (P : Polynomial ℚ) : (μX K P).coeff 1 = ∑ j ∈ Finset.Icc 1 K, res K P j * ↑j ^ 4

theorem Zeta5Irrational.eval_D (m : ℕ) (x : ℚ) : Polynomial.eval x (D m) = ∏ j ∈ Finset.Icc 1 m, (x + ↑j ^ 2)

theorem Zeta5Irrational.eval_D_eq_zero {m j : ℕ} (hj : j ∈ Finset.Icc 1 m) : Polynomial.eval (-↑j ^ 2) (D m) = 0

theorem Zeta5Irrational.eval_D_ne_zero {m j : ℕ} (hj : m < j) : Polynomial.eval (-↑j ^ 2) (D m) ≠ 0

theorem Zeta5Irrational.eval_derivative_D {K j : ℕ} (hj : j ∈ Finset.Icc 1 K) : Polynomial.eval (-↑j ^ 2) (Polynomial.derivative (D K)) = ∏ i ∈ (Finset.Icc 1 K).erase j, (↑i ^ 2 - ↑j ^ 2)

theorem Zeta5Irrational.eval_derivative_D_ne_zero {K j : ℕ} (hj : j ∈ Finset.Icc 1 K) : Polynomial.eval (-↑j ^ 2) (Polynomial.derivative (D K)) ≠ 0

theorem Zeta5Irrational.sum_Icc_eq_sum_fin (N K : ℕ) (hNK : N ≤ K) (f : ℕ → ℚ) (hf : ∀ j ∈ Finset.Icc 1 N, f j = 0) : ∑ j ∈ Finset.Icc 1 K, f j = ∑ k : Fin (K - N), f (N + 1 + ↑k)

Reindexing: a sum over Icc 1 K whose terms vanish on Icc 1 N is a sum over k : Fin (K - N) of the terms at N + 1 + k.

noncomputable def Zeta5Irrational.node (n : ℕ) (k : Fin (37 * n)) : ℚ

The nodes x_k = -(N + 1 + k)², k < h.

Equations

• Zeta5Irrational.node n k = -↑(3 * n + 1 + ↑k) ^ 2

noncomputable def Zeta5Irrational.weight (n : ℕ) (k : Fin (37 * n)) : ℚ

The weights w_k = D_N(x_k)^6 (N + 1 + k)^4 / D_K'(x_k).

Equations

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

theorem Zeta5Irrational.natDegree_G_le (n : ℕ) (i j : Fin (37 * n)) : (G n i j).natDegree ≤ 1

theorem Zeta5Irrational.coeff_G_one (n : ℕ) : (Matrix.of fun (i j : Fin (37 * n)) => (G n i j).coeff 1) = (Matrix.vandermonde (node n)).transpose * Matrix.diagonal (weight n) * Matrix.vandermonde (node n)

The matrix of X-coefficients of G_K(X) is Vᵀ diag(w) V with V the Vandermonde matrix of the nodes.

theorem Zeta5Irrational.node_injective (n : ℕ) : Function.Injective (node n)

theorem Zeta5Irrational.weight_ne_zero (n : ℕ) (k : Fin (37 * n)) : weight n k ≠ 0

theorem Zeta5Irrational.det_coeff_G_one_ne_zero (n : ℕ) : (Matrix.of fun (i j : Fin (37 * n)) => (G n i j).coeff 1).det ≠ 0

theorem Zeta5Irrational.natDegree_Δ (n : ℕ) : (Δ n).natDegree = 37 * n

(2.9): Δ_K has degree exactly h = 37 n.

theorem Zeta5Irrational.S_pos (n : ℕ) : 0 < S n

theorem Zeta5Irrational.natDegree_F (n : ℕ) : (F n).natDegree = 37 * n

(2.9): F_K has degree exactly h = 37 n.