Partial fractions for P / D_K

For a polynomial P and t ≥ 0, P(t) / D_K(t) = (P /ₘ D_K)(t) + ∑_j res_j / (t + j²) with res_j = P(-j²) / D_K'(-j²), the residues used in the definition of μ_X (Zeta5Irrational.res).

theorem Zeta5Irrational.D_monic (K : ℕ) : (D K).Monic

theorem Zeta5Irrational.natDegree_D (K : ℕ) : (D K).natDegree = K

theorem Zeta5Irrational.modByMonic_eq_sum_res (K : ℕ) (P : Polynomial ℚ) : P %ₘ D K = ∑ j ∈ Finset.Icc 1 K, Polynomial.C (res K P j) * ∏ i ∈ (Finset.Icc 1 K).erase j, (Polynomial.X + Polynomial.C (↑i ^ 2))

The polynomial identity behind the partial fractions: the remainder P %ₘ D_K equals ∑_j res_j ∏_{i ≠ j} (X + i²).

theorem Zeta5Irrational.aeval_D_pos (m : ℕ) {t : ℝ} (ht : 0 ≤ t) : 0 < (Polynomial.aeval t) (D m)

theorem Zeta5Irrational.partial_fractions (K : ℕ) (P : Polynomial ℚ) {t : ℝ} (ht : 0 ≤ t) : (Polynomial.aeval t) P / (Polynomial.aeval t) (D K) = (Polynomial.aeval t) (P /ₘ D K) + ∑ j ∈ Finset.Icc 1 K, ↑(res K P j) / (t + ↑j ^ 2)

Partial fractions as real functions, for t ≥ 0.