the proof notes, §7: the unitriangular change t^i ↦ i!·binom(t,i) gives Q_n/F_n = det[U_r(binom(t,a) binom(t,b) R_n)], and with one factor S_n per row, Qtilde r n = det[U_r(S_n D_n^4 binom(t,a) binom(t,b) / D_{5n})].

noncomputable def Zeta32.Arith.Small.Ufun (r : ℚ) (n : ℕ) (F : Polynomial ℚ) : Polynomial ℚ

The functional U_r on F / D_{5n}: polynomial part plus simple poles `U_r(1/(t+j)) = 2jX

• β_j`.

Equations

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

theorem Zeta32.Arith.Small.divByMonic_add {q : Polynomial ℚ} (hq : q.Monic) (F G : Polynomial ℚ) : (F + G) /ₘ q = F /ₘ q + G /ₘ q

theorem Zeta32.Arith.Small.divByMonic_C_mul {q : Polynomial ℚ} (hq : q.Monic) (c : ℚ) (F : Polynomial ℚ) : Polynomial.C c * F /ₘ q = Polynomial.C c * (F /ₘ q)

theorem Zeta32.Arith.Small.Ufun_add (r : ℚ) (n : ℕ) (F G : Polynomial ℚ) : Ufun r n (F + G) = Ufun r n F + Ufun r n G

theorem Zeta32.Arith.Small.Ufun_C_mul (r : ℚ) (n : ℕ) (c : ℚ) (F : Polynomial ℚ) : Ufun r n (Polynomial.C c * F) = Polynomial.C c * Ufun r n F

theorem Zeta32.Arith.Small.Ufun_sum {ι : Type u_1} (r : ℚ) (n : ℕ) (s : Finset ι) (F : ι → Polynomial ℚ) : Ufun r n (∑ i ∈ s, F i) = ∑ i ∈ s, Ufun r n (F i)

theorem Zeta32.Arith.Small.Ufun_entry (r : ℚ) (n k : ℕ) : Ufun r n (numerator n k) = Polynomial.X * Polynomial.C (slope n k) + Polynomial.C (intercept r n k)

Gram basis change

@[reducible, inline]

noncomputable abbrev Zeta32.Arith.Small.coeffMat {h : ℕ} (E : Fin h → Polynomial ℚ) : Matrix (Fin h) (Fin h) ℚ

Coefficient matrix of a finite family of polynomials.

Equations

• Zeta32.Arith.Small.coeffMat E = Zeta5Irrational.coeffMat E

theorem Zeta32.Arith.Small.sum_coeffMat {h : ℕ} (E : Fin h → Polynomial ℚ) (hE : ∀ (a : Fin h), (E a).natDegree < h) (a : Fin h) : E a = ∑ k : Fin h, Polynomial.C (coeffMat E a k) * Polynomial.X ^ ↑k

noncomputable def Zeta32.Arith.Small.hankelFor (r : ℚ) (n h : ℕ) (R : Polynomial ℚ) : Matrix (Fin h) (Fin h) (Polynomial ℚ)

Hankel matrix obtained by applying Ufun to shifted copies of R.

Equations

• Zeta32.Arith.Small.hankelFor r n h R i j = Zeta32.Arith.Small.Ufun r n (R * Polynomial.X ^ (↑i + ↑j))

theorem Zeta32.Arith.Small.gram_basis_change (r : ℚ) (n h : ℕ) (R : Polynomial ℚ) (E : Fin h → Polynomial ℚ) (hE : ∀ (a : Fin h), (E a).natDegree < h) : (Matrix.of fun (a b : Fin h) => Ufun r n (R * E a * E b)).det = Polynomial.C ((coeffMat E).det ^ 2) * (hankelFor r n h R).det

theorem Zeta32.Arith.Small.hankelFor_original (r : ℚ) (n : ℕ) : hankelFor r n (3 * n) (D n ^ 4) = Polynomial.X • (B n).map ⇑Polynomial.C + (A r n).map ⇑Polynomial.C

theorem Zeta32.Arith.Small.original_gram_basis_change (r : ℚ) (n : ℕ) (E : Fin (3 * n) → Polynomial ℚ) (hE : ∀ (a : Fin (3 * n)), (E a).natDegree < 3 * n) : (Matrix.of fun (a b : Fin (3 * n)) => Ufun r n (D n ^ 4 * E a * E b)).det = Polynomial.C ((coeffMat E).det ^ 2) * Q r n

Binomial normalization

theorem Zeta32.Arith.Small.coeffMat_binom_lowerTriangular (h : ℕ) : (coeffMat fun (a : Fin h) => binomPoly ↑a).BlockTriangular ⇑OrderDual.toDual

theorem Zeta32.Arith.Small.coeffMat_binom_det (h : ℕ) : (coeffMat fun (a : Fin h) => binomPoly ↑a).det = ∏ i ∈ Finset.range h, (↑i.factorial)⁻¹

theorem Zeta32.Arith.Small.coeffMat_binom_det_sq (n : ℕ) : (coeffMat fun (a : Fin (3 * n)) => binomPoly ↑a).det ^ 2 = (Fn n)⁻¹

noncomputable def Zeta32.Arith.Small.binomGram (r : ℚ) (n : ℕ) : Matrix (Fin (3 * n)) (Fin (3 * n)) (Polynomial ℚ)

The binomial Gram matrix with the scalar S_n inside every entry.

Equations

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

theorem Zeta32.Arith.Small.Qtilde_eq_binomGram_det (r : ℚ) (n : ℕ) : Qtilde r n = (binomGram r n).det