Partial fractions for t^k R_n(t) = X^k D_n^4 / D_{5n} with the polynomialPart and residue of Zeta32/Family.lean.

The generic part (piPl, polyPart, resP, partial_fractionsP) is -- adapted from dtq1997/li2-half-irrationality@d5d8206:Li2Unified/Modular/Base/SimplePoles.lean (itself extracted from Apery/Arith/PoleFun.lean in mo271/Zeta5 by Moritz Firsching, Apache-2.0); the specialization to D (5*n) follows Li2 OriginalPartialFractions.lean.

def Zeta32.Analytic.Contour.negativePoles (m : ℕ) : Finset ℤ

The poles -1, …, -m as integers.

Equations

• Zeta32.Analytic.Contour.negativePoles m = Finset.image (fun (j : ℕ) => -↑j) (Finset.Icc 1 m)

theorem Zeta32.Analytic.Contour.negative_nat_injective : Function.Injective fun (j : ℕ) => -↑j

theorem Zeta32.Analytic.Contour.negativePoles_product (m : ℕ) : Zeta5Irrational.piPl (negativePoles m) = D m

theorem Zeta32.Analytic.Contour.numerator_partial_fractions (n k : ℕ) : numerator n k = polynomialPart n k * D (5 * n) + ∑ j ∈ Finset.Icc 1 (5 * n), Polynomial.C (residue n k j) * ∏ l ∈ (Finset.Icc 1 (5 * n)).erase j, (Polynomial.X + Polynomial.C ↑l)

Partial fractions for the entries of the family: X^k D_n^4 = q D_{5n} + Σ c_j ∏_{l≠j}(X+l).

theorem Zeta32.Analytic.Contour.aeval_D (m : ℕ) (z : ℂ) : (Polynomial.aeval z) (D m) = ∏ j ∈ Finset.Icc 1 m, (z + ↑j)

theorem Zeta32.Analytic.Contour.prod_add_nat_ne_zero (m : ℕ) {z : ℂ} (hz : 0 < z.re) : ∏ j ∈ Finset.Icc 1 m, (z + ↑j) ≠ 0

theorem Zeta32.Analytic.Contour.pow_mul_Rfun_eq (n k : ℕ) {z : ℂ} (hz : 0 < z.re) : z ^ k * Rfun n z = (Polynomial.aeval z) (polynomialPart n k) + ∑ j ∈ Finset.Icc 1 (5 * n), ↑(residue n k j) / (z + ↑j)

Complex form of the partial fractions: z^k R_n(z) = q(z) + Σ_j c_j/(z+j) for Re z > 0.