Partial fractions for rational polynomials with simple integer poles

This generic API is shared by the Zeta5 and Zeta32 arithmetic and contour proofs.

noncomputable def Zeta5Irrational.piPl (Pl : Finset ℤ) : Polynomial ℚ

∏_{r ∈ Pl} (x - r).

Equations

• Zeta5Irrational.piPl Pl = ∏ r ∈ Pl, (Polynomial.X - Polynomial.C ↑r)

theorem Zeta5Irrational.piPl_monic (Pl : Finset ℤ) : (piPl Pl).Monic

theorem Zeta5Irrational.natDegree_piPl (Pl : Finset ℤ) : (piPl Pl).natDegree = Pl.card

noncomputable def Zeta5Irrational.polyPart (A : Polynomial ℚ) (Pl : Finset ℤ) : Polynomial ℚ

The polynomial part.

Equations

• Zeta5Irrational.polyPart A Pl = A /ₘ Zeta5Irrational.piPl Pl

noncomputable def Zeta5Irrational.resP (A : Polynomial ℚ) (Pl : Finset ℤ) (r : ℤ) : ℚ

The residue at r.

Equations

• Zeta5Irrational.resP A Pl r = Polynomial.eval (↑r) A / ∏ s ∈ Pl.erase r, (↑r - ↑s)

theorem Zeta5Irrational.lagrange_basis_eq (Pl : Finset ℤ) (r : ℤ) : Lagrange.basis Pl (fun (s : ℤ) => ↑s) r = Polynomial.C (∏ s ∈ Pl.erase r, (↑r - ↑s))⁻¹ * ∏ s ∈ Pl.erase r, (Polynomial.X - Polynomial.C ↑s)

theorem Zeta5Irrational.partial_fractionsP (A : Polynomial ℚ) (Pl : Finset ℤ) : A = polyPart A Pl * piPl Pl + ∑ r ∈ Pl, Polynomial.C (resP A Pl r) * ∏ s ∈ Pl.erase r, (Polynomial.X - Polynomial.C ↑s)

Partial fractions.

theorem Zeta5Irrational.natDegree_polyPart_le (A : Polynomial ℚ) (Pl : Finset ℤ) : (polyPart A Pl).natDegree ≤ A.natDegree - Pl.card