Spectral parameters from a zeta numerator

This file records the elementary factorization needed after rationality of a curve zeta function has produced a numerator polynomial. A complex polynomial whose constant coefficient is one is uniquely the product of the factors 1 - alpha * X, where the parameters alpha are the inverses of its roots, counted with multiplicity.

The substantive arithmetic input remains the construction of the zeta numerator and its logarithmic-derivative point-count identity. No spectral norm estimate is used here.

noncomputable def BGS.HasseWeil.reciprocalRootParameter (P : Polynomial ℂ) (i : Fin P.natDegree) : ℂ

The reciprocal root parameter attached to the i-th root of P, with roots enumerated by the canonical sorted list underlying their multiset.

Equations

• BGS.HasseWeil.reciprocalRootParameter P i = (P.roots.toList.get (Fin.cast ⋯ i))⁻¹

theorem BGS.HasseWeil.sum_reciprocalRootParameter_pow (P : Polynomial ℂ) (m : ℕ) : ∑ i : Fin P.natDegree, reciprocalRootParameter P i ^ m = (Multiset.map (fun (r : ℂ) => r⁻¹ ^ m) P.roots).sum

Summing powers of the indexed reciprocal-root family agrees with the multiset power sum, including root multiplicities.

theorem BGS.HasseWeil.polynomial_eq_prod_one_sub_C_mul_X_of_coeff_zero_eq_one (P : Polynomial ℂ) (hP0 : P.coeff 0 = 1) : P = (Multiset.map (fun (r : ℂ) => 1 - Polynomial.C r⁻¹ * Polynomial.X) P.roots).prod

A complex polynomial normalized by P(0) = 1 factors into reciprocal linear factors, with one factor for every root counted with multiplicity.

theorem BGS.HasseWeil.polynomial_eq_prod_reciprocalRootParameter (P : Polynomial ℂ) (hP0 : P.coeff 0 = 1) : P = ∏ i : Fin P.natDegree, (1 - Polynomial.C (reciprocalRootParameter P i) * Polynomial.X)

The reciprocal-root factorization with the parameters indexed by Fin P.natDegree, ready for the finite power sums used in the spectral point-count formula.