Linear algebra of the local functional locValue (for S2b-1).

• dist_locValue_add, dist_locValue_C_mul, dist_locValue_sum : locValue s · M is linear;
• locPoly_eq : locPoly s Q = Lbp Q' + 2 s Lbp Q;
• pf_nat : partial fractions over the nodes -m, m ∈ M;
• locValue_pf : value of locValue on a partial-fraction form.

noncomputable def Zeta32.PrimeEdge.mprod (M : Finset ℕ) : Polynomial ℚ

∏_{m ∈ M} (X + m).

Equations

• Zeta32.PrimeEdge.mprod M = ∏ m ∈ M, (Polynomial.X + Polynomial.C ↑m)

theorem Zeta32.PrimeEdge.mprod_monic (M : Finset ℕ) : (mprod M).Monic

theorem Zeta32.PrimeEdge.natDegree_mprod (M : Finset ℕ) : (mprod M).natDegree = M.card

theorem Zeta32.PrimeEdge.dist_locPoly_add (s : ℚ) (P Q : Polynomial ℚ) : locPoly s (P + Q) = locPoly s P + locPoly s Q

theorem Zeta32.PrimeEdge.locPoly_C_mul (s c : ℚ) (P : Polynomial ℚ) : locPoly s (Polynomial.C c * P) = c * locPoly s P

theorem Zeta32.PrimeEdge.dist_locPoly_zero (s : ℚ) : locPoly s 0 = 0

theorem Zeta32.PrimeEdge.locPoly_monomial (s : ℚ) (e : ℕ) (a : ℚ) : locPoly s ((Polynomial.monomial e) a) = a * locMoment s e

theorem Zeta32.PrimeEdge.locPoly_eq (s : ℚ) (Q : Polynomial ℚ) : locPoly s Q = Arith.Local.Lbp (Polynomial.derivative Q) + 2 * s * Arith.Local.Lbp Q

locPoly s Q = Lbp Q' + 2 s Lbp Q.

theorem Zeta32.PrimeEdge.dist_locValue_add (s : ℚ) (S T : Polynomial ℚ) (M : Finset ℕ) : locValue s (S + T) M = locValue s S M + locValue s T M

theorem Zeta32.PrimeEdge.dist_locValue_C_mul (s c : ℚ) (S : Polynomial ℚ) (M : Finset ℕ) : locValue s (Polynomial.C c * S) M = c * locValue s S M

theorem Zeta32.PrimeEdge.locValue_zero (s : ℚ) (M : Finset ℕ) : locValue s 0 M = 0

theorem Zeta32.PrimeEdge.dist_locValue_sum {ι : Type u_1} (s : ℚ) (t : Finset ι) (S : ι → Polynomial ℚ) (M : Finset ℕ) : locValue s (∑ i ∈ t, S i) M = ∑ i ∈ t, locValue s (S i) M

def Zeta32.PrimeEdge.resN (S : Polynomial ℚ) (M : Finset ℕ) (m : ℕ) : ℚ

Residue of S / mprod M at -m.

Equations

• Zeta32.PrimeEdge.resN S M m = Polynomial.eval (-↑m) S / ∏ m' ∈ M.erase m, (↑m' - ↑m)

theorem Zeta32.PrimeEdge.lagrange_basis_eq_nat (M : Finset ℕ) (m : ℕ) : Lagrange.basis M (fun (m : ℕ) => -↑m) m = Polynomial.C (∏ m' ∈ M.erase m, (↑m' - ↑m))⁻¹ * ∏ m' ∈ M.erase m, (Polynomial.X + Polynomial.C ↑m')

theorem Zeta32.PrimeEdge.pf_nat (S : Polynomial ℚ) (M : Finset ℕ) : S = S /ₘ mprod M * mprod M + ∑ m ∈ M, Polynomial.C (resN S M m) * ∏ m' ∈ M.erase m, (Polynomial.X + Polynomial.C ↑m')

Partial fractions over the nodes -m, m ∈ M.

theorem Zeta32.PrimeEdge.locValue_pf (s : ℚ) (M : Finset ℕ) (P : Polynomial ℚ) (a : ℕ → ℚ) : locValue s (P * mprod M + ∑ m ∈ M, Polynomial.C (a m) * ∏ m' ∈ M.erase m, (Polynomial.X + Polynomial.C ↑m')) M = locPoly s P + ∑ m ∈ M, a m * locPole s m

locValue on a partial-fraction form.