The pullback identity (3.1): μ_X(R) = τ_X(x⁵ R(-x²))

With PlK K = {±1, …, ±K} and pull K P = (-1)^K x⁵ P(-x²) we have μX K P = tauX (pull K P) (PlK K) (μX_eq_tauX), since x⁵ P(-x²) / D_K(-x²) = pull K P / ∏_{r ∈ PlK K} (x - r).

Linearity of τ

theorem Zeta5Irrational.tau_add (P Q : Polynomial ℚ) : tau (P + Q) = tau P + tau Q

theorem Zeta5Irrational.tau_C_mul (c : ℚ) (P : Polynomial ℚ) : tau (Polynomial.C c * P) = c * tau P

theorem Zeta5Irrational.tau_neg (P : Polynomial ℚ) : tau (-P) = -tau P

theorem Zeta5Irrational.tau_sum {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℚ) : tau (∑ i ∈ s, f i) = ∑ i ∈ s, tau (f i)

theorem Zeta5Irrational.tau_X_pow (n : ℕ) : tau (Polynomial.X ^ n) = ↑(n.descFactorial 3) * bernoulli (n - 3) / 24

theorem Zeta5Irrational.tau_X_pow_odd (e : ℕ) : tau (Polynomial.C ((-1) ^ e) * Polynomial.X ^ (2 * e + 5)) = μmono e

theorem Zeta5Irrational.tau_pull_poly (Q : Polynomial ℚ) : tau (Polynomial.X ^ 5 * Q.comp (-Polynomial.X ^ 2)) = μpoly Q

τ(x⁵ Q(-x²)) = μ(Q).

theorem Zeta5Irrational.tau_cubic (a : ℚ) : tau (-Polynomial.X ^ 3 - Polynomial.C a * Polynomial.X) = -1 / 4

The pole set {±1, …, ±K}

def Zeta5Irrational.PlK (K : ℕ) : Finset ℤ

The poles ±1, …, ±K in the variable x.

Equations

• Zeta5Irrational.PlK K = Finset.image (fun (j : ℕ) => ↑j) (Finset.Icc 1 K) ∪ Finset.image (fun (j : ℕ) => -↑j) (Finset.Icc 1 K)

theorem Zeta5Irrational.PlK_disjoint (K : ℕ) : Disjoint (Finset.image (fun (j : ℕ) => ↑j) (Finset.Icc 1 K)) (Finset.image (fun (j : ℕ) => -↑j) (Finset.Icc 1 K))

theorem Zeta5Irrational.sum_PlK {M : Type u_1} [AddCommMonoid M] (K : ℕ) (f : ℤ → M) : ∑ r ∈ PlK K, f r = ∑ j ∈ Finset.Icc 1 K, (f ↑j + f (-↑j))

theorem Zeta5Irrational.prod_PlK {M : Type u_1} [CommMonoid M] (K : ℕ) (f : ℤ → M) : ∏ r ∈ PlK K, f r = ∏ j ∈ Finset.Icc 1 K, f ↑j * f (-↑j)

theorem Zeta5Irrational.X_add_C_comp_neg_sq (a : ℚ) : (Polynomial.X + Polynomial.C a).comp (-Polynomial.X ^ 2) = -Polynomial.X ^ 2 + Polynomial.C a

theorem Zeta5Irrational.piPl_PlK (K : ℕ) : piPl (PlK K) = Polynomial.C ((-1) ^ K) * (D K).comp (-Polynomial.X ^ 2)

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

pull K P = (-1)^K x⁵ P(-x²).

Equations

• Zeta5Irrational.pull K P = Polynomial.C ((-1) ^ K) * Polynomial.X ^ 5 * P.comp (-Polynomial.X ^ 2)

theorem Zeta5Irrational.card_PlK (K : ℕ) : (PlK K).card = 2 * K

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

The cofactor B_j = (-1)^K ∏_{i ≠ j} (i² - x²).

Equations

• Zeta5Irrational.Bj K j = Polynomial.C ((-1) ^ K) * (∏ i ∈ (Finset.Icc 1 K).erase j, (Polynomial.X + Polynomial.C (↑i ^ 2))).comp (-Polynomial.X ^ 2)

theorem Zeta5Irrational.piPl_eq_Bj {K j : ℕ} (hj : j ∈ Finset.Icc 1 K) : piPl (PlK K) = (-Polynomial.X ^ 2 + Polynomial.C (↑j ^ 2)) * Bj K j

theorem Zeta5Irrational.natDegree_Bj_le {K j : ℕ} (hj : j ∈ Finset.Icc 1 K) : (Bj K j).natDegree ≤ 2 * (K - 1)

theorem Zeta5Irrational.polyPart_pull (K : ℕ) (P : Polynomial ℚ) : polyPart (pull K P) (PlK K) = Polynomial.X ^ 5 * (P /ₘ D K).comp (-Polynomial.X ^ 2) + ∑ j ∈ Finset.Icc 1 K, Polynomial.C (res K P j) * (-Polynomial.X ^ 3 - Polynomial.C (↑j ^ 2) * Polynomial.X)

The polynomial part of the pulled-back function.

theorem Zeta5Irrational.prod_erase_eq_derivative (Pl : Finset ℤ) {r : ℤ} (hr : r ∈ Pl) : ∏ s ∈ Pl.erase r, (↑r - ↑s) = Polynomial.eval (↑r) (Polynomial.derivative (piPl Pl))

theorem Zeta5Irrational.resP_pull (K : ℕ) (P : Polynomial ℚ) {r : ℤ} (hr : r ∈ PlK K) (hr0 : r ≠ 0) : resP (pull K P) (PlK K) r = -(↑r ^ 4 / 2) * (Polynomial.eval (-↑r ^ 2) P / Polynomial.eval (-↑r ^ 2) (Polynomial.derivative (D K)))

theorem Zeta5Irrational.dd_nat (j : ℕ) : dd ↑j = j

theorem Zeta5Irrational.dd_neg {j : ℕ} (hj : 1 ≤ j) : dd (-↑j) = j - 1

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

theorem Zeta5Irrational.μX_eq_tauX (K : ℕ) (P : Polynomial ℚ) : μX K P = tauX (pull K P) (PlK K)

The pullback identity (3.1): μ_X(P / D_K) = τ_X((-1)^K x⁵ P(-x²) / ∏_{r ∈ PlK} (x - r)).