Zeta32 — Family.

noncomputable def Zeta32.D (m : ℕ) : Polynomial ℚ

The rational polynomial with roots -1, …, -m.

Equations

• Zeta32.D m = ∏ j ∈ Finset.Icc 1 m, (Polynomial.X + Polynomial.C ↑j)

noncomputable def Zeta32.numerator (n k : ℕ) : Polynomial ℚ

Numerator of the rational function used to construct the polynomial family.

Equations

• Zeta32.numerator n k = Polynomial.X ^ k * Zeta32.D n ^ 4

noncomputable def Zeta32.polynomialPart (n k : ℕ) : Polynomial ℚ

Polynomial quotient of the numerator by the denominator polynomial.

Equations

• Zeta32.polynomialPart n k = Zeta32.numerator n k /ₘ Zeta32.D (5 * n)

noncomputable def Zeta32.residue (n k j : ℕ) : ℚ

Residue coefficient at the simple pole indexed by j.

Equations

• Zeta32.residue n k j = Polynomial.eval (-↑j) (Zeta32.numerator n k) / ∏ l ∈ (Finset.Icc 1 (5 * n)).erase j, (↑l - ↑j)

def Zeta32.moment (r : ℚ) (e : ℕ) : ℚ

Bernoulli moment of the polynomial functional at rational parameter r.

Equations

• Zeta32.moment r e = ↑(e + 1) * bernoulli' e + 2 * r * bernoulli' (e + 1)

def Zeta32.H (e j : ℕ) : ℚ

Finite generalized harmonic sum of order e through index j.

Equations

• Zeta32.H e j = ∑ a ∈ Finset.Icc 1 j, 1 / ↑a ^ e

def Zeta32.beta (r : ℚ) (j : ℕ) : ℚ

Constant contribution of the pole indexed by j to the moment functional.

Equations

• Zeta32.beta r j = 2 * r - 2 * ↑j * Zeta32.H 3 j + 2 * r * ↑j * Zeta32.H 2 j

def Zeta32.polynomialMoment (r : ℚ) (p : Polynomial ℚ) : ℚ

Linear extension of the Bernoulli moments to a polynomial.

Equations

• Zeta32.polynomialMoment r p = p.sum fun (e : ℕ) (a : ℚ) => a * Zeta32.moment r e

noncomputable def Zeta32.slope (n k : ℕ) : ℚ

Coefficient of the target zeta value in the rational-function moment.

Equations

• Zeta32.slope n k = ∑ j ∈ Finset.Icc 1 (5 * n), Zeta32.residue n k j * (2 * ↑j)

noncomputable def Zeta32.intercept (r : ℚ) (n k : ℕ) : ℚ

Constant coefficient in the rational-function moment.

Equations

• Zeta32.intercept r n k = Zeta32.polynomialMoment r (Zeta32.polynomialPart n k) + ∑ j ∈ Finset.Icc 1 (5 * n), Zeta32.residue n k j * Zeta32.beta r j

noncomputable def Zeta32.A (r : ℚ) (n : ℕ) : Matrix (Fin (3 * n)) (Fin (3 * n)) ℚ

Hankel matrix of the constant moment coefficients.

Equations

• Zeta32.A r n i k = Zeta32.intercept r n (↑i + ↑k)

noncomputable def Zeta32.B (n : ℕ) : Matrix (Fin (3 * n)) (Fin (3 * n)) ℚ

Hankel matrix of the target-value moment coefficients.

Equations

• Zeta32.B n i k = Zeta32.slope n (↑i + ↑k)

noncomputable def Zeta32.Q (r : ℚ) (n : ℕ) : Polynomial ℚ

Determinant polynomial of the moment pencil X • B + A.

Equations

• Zeta32.Q r n = (Polynomial.X • (Zeta32.B n).map ⇑Polynomial.C + (Zeta32.A r n).map ⇑Polynomial.C).det

theorem Zeta32.Q_natDegree_le (r : ℚ) (n : ℕ) : (Q r n).natDegree ≤ 3 * n

noncomputable def Zeta32.primitiveQ (r : ℚ) (n : ℕ) : Polynomial ℤ

Primitive integral normalization of the determinant polynomial, with zero preserved.

Equations

• Zeta32.primitiveQ r n = if Zeta32.Q r n = 0 then 0 else (IsLocalization.integerNormalization (nonZeroDivisors ℤ) (Zeta32.Q r n)).primPart

theorem Zeta32.primitiveQ_isPrimitive (r : ℚ) (n : ℕ) (hn : Q r n ≠ 0) : (primitiveQ r n).IsPrimitive

theorem Zeta32.primitiveQ_natDegree_le (r : ℚ) (n : ℕ) : (primitiveQ r n).natDegree ≤ 3 * n

theorem Zeta32.primitiveQ_proportional (r : ℚ) (n : ℕ) : ∃ (a : ℚ), a ≠ 0 ∧ Polynomial.map (algebraMap ℤ ℚ) (primitiveQ r n) = Polynomial.C a * Q r n

def Zeta32.Sn (n : ℕ) : ℚ

Factorial quotient used to normalize the rational-function determinant.

Equations

• Zeta32.Sn n = ↑(5 * n).factorial / ↑n.factorial ^ 4

def Zeta32.Fn (n : ℕ) : ℚ

Product of squared factorials used to normalize the Hankel determinant.

Equations

• Zeta32.Fn n = ∏ i ∈ Finset.range (3 * n), ↑i.factorial ^ 2

def Zeta32.scale (n : ℕ) : ℚ

Positive scalar converting the determinant to its arithmetic normalization.

Equations

• Zeta32.scale n = Zeta32.Sn n ^ (3 * n) / Zeta32.Fn n

noncomputable def Zeta32.Qtilde (r : ℚ) (n : ℕ) : Polynomial ℚ

The determinant polynomial after multiplication by the arithmetic normalization.

Equations

• Zeta32.Qtilde r n = Polynomial.C (Zeta32.scale n) * Zeta32.Q r n

theorem Zeta32.Sn_pos (n : ℕ) : 0 < Sn n

theorem Zeta32.Fn_pos (n : ℕ) : 0 < Fn n

theorem Zeta32.scale_pos (n : ℕ) : 0 < scale n

noncomputable def Zeta32.cost (r : ℚ) (n p : ℕ) : ℝ

Negative minimum valuation among the nonzero coefficients of the normalized polynomial.

Equations

• Zeta32.cost r n p = -sInf {v : ℝ | ∃ (k : ℕ), (Zeta32.Qtilde r n).coeff k ≠ 0 ∧ v = ↑(padicValRat p ((Zeta32.Qtilde r n).coeff k))}

noncomputable def Zeta32.primitiveScale (r : ℚ) (n : ℕ) : ℚ

A nonzero proportionality factor for the primitive integral normalization.

Equations

• Zeta32.primitiveScale r n = ⋯.choose

theorem Zeta32.primitiveScale_ne_zero (r : ℚ) (n : ℕ) : primitiveScale r n ≠ 0

theorem Zeta32.primitiveScale_spec (r : ℚ) (n : ℕ) : Polynomial.map (algebraMap ℤ ℚ) (primitiveQ r n) = Polynomial.C (primitiveScale r n) * Q r n

noncomputable def Zeta32.P (r : ℚ) (n : ℕ) : Polynomial ℤ

Primitive integral determinant polynomial with a positive proportionality factor.

Equations

• Zeta32.P r n = if 0 < Zeta32.primitiveScale r n then Zeta32.primitiveQ r n else -Zeta32.primitiveQ r n

theorem Zeta32.P_natDegree_le (r : ℚ) (n : ℕ) : (P r n).natDegree ≤ 3 * n

noncomputable def Zeta32.d (r : ℚ) (n : ℕ) : ℚ

Positive proportionality factor for the primitive determinant polynomial.

Equations

• Zeta32.d r n = |Zeta32.primitiveScale r n|

noncomputable def Zeta32.dtilde (r : ℚ) (n : ℕ) : ℚ

Positive proportionality factor relative to the arithmetically normalized polynomial.

Equations

• Zeta32.dtilde r n = Zeta32.d r n / Zeta32.scale n

theorem Zeta32.d_pos (r : ℚ) (n : ℕ) : 0 < d r n

theorem Zeta32.dtilde_pos (r : ℚ) (n : ℕ) : 0 < dtilde r n

theorem Zeta32.P_eq_dtilde_Qtilde (r : ℚ) (n : ℕ) : Polynomial.map (algebraMap ℤ ℚ) (P r n) = Polynomial.C (dtilde r n) * Qtilde r n

noncomputable def Zeta32.zeta3val : ℝ

Real zeta value at three, expressed as a convergent series.

Equations

• Zeta32.zeta3val = ∑' (k : ℕ), 1 / (↑k + 1) ^ 3

noncomputable def Zeta32.zeta2val : ℝ

Real zeta value at two, expressed as a convergent series.

Equations

• Zeta32.zeta2val = ∑' (k : ℕ), 1 / (↑k + 1) ^ 2

noncomputable def Zeta32.Cr (r : ℚ) : ℝ

The real target value ζ(3) - r * ζ(2).

Equations

• Zeta32.Cr r = Zeta32.zeta3val - ↑r * Zeta32.zeta2val