noncomputable def ResidueSum.residueAtPole {k : Type u_1} [Field k] (P Q : Polynomial k) (a : k) : k

The residue of P/Q at a simple pole a: P(a) / Q'(a), the standard formula valid when Q has a simple root at a.

noncomputable def ResidueSum.poleProd {k : Type u_1} [Field k] {n : ℕ} (a : Fin n → k) : Polynomial k

The product ∏ (X − a_i) whose roots are the chosen poles, the denominator of the partial fraction decomposition.

noncomputable def ResidueSum.partialFracNumer {k : Type u_1} [Field k] {n : ℕ} (c a : Fin n → k) : Polynomial k

The numerator polynomial Σ_i c_i · ∏_{j ≠ i}(X − a_j) of a partial-fraction expression with residues c_i at the poles a_i.

noncomputable def ResidueSum.residuePartialFrac {k : Type u_1} [Field k] {n : ℕ} (c a : Fin n → k) (i : Fin n) : k

The residue at the pole a_i of the partial-fraction differential partialFracNumer c a / poleProd a.

noncomputable def ResidueSum.residueAtInfPartialFrac {k : Type u_1} [Field k] {n : ℕ} (c a : Fin n → k) : k

The residue at infinity of the partial-fraction differential: the negative of the leading coefficient of the numerator polynomial.

theorem ResidueSum.prod_erase_eval_zero {k : Type u_1} [Field k] {n : ℕ} (a : Fin n → k) (i j : Fin n) (hij : i ≠ j) : Polynomial.eval (a j) (∏ l ∈ Finset.univ.erase i, (Polynomial.X - Polynomial.C (a l))) = 0

For distinct indices, the product ∏_{l ≠ i}(X − a_l) evaluated at a_j vanishes (one factor a_j − a_j appears).

theorem ResidueSum.coeff_summand {k : Type u_1} [Field k] {n : ℕ} (c a : Fin n → k) (i : Fin n) : (Polynomial.C (c i) * ∏ j ∈ Finset.univ.erase i, (Polynomial.X - Polynomial.C (a j))).coeff (n - 1) = c i

The leading coefficient of the i-th summand c_i · ∏_{j ≠ i}(X − a_j) is exactly c_i.

theorem ResidueSum.residue_of_simple_pole {k : Type u_1} [Field k] (c a : k) : residueAtPole (Polynomial.C c) (Polynomial.X - Polynomial.C a) a = c

Single-pole identity: the residue of c / (X − a) at a equals c.

theorem ResidueSum.partialFracNumer_eval {k : Type u_1} [Field k] {n : ℕ} (c a : Fin n → k) (j : Fin n) : Polynomial.eval (a j) (partialFracNumer c a) = c j * ∏ l ∈ Finset.univ.erase j, (a j - a l)

Evaluation of the partial-fraction numerator at a pole a_j: only the j-th summand survives and equals c_j · ∏_{l ≠ j}(a_j − a_l).

theorem ResidueSum.poleProd_derivative_eval {k : Type u_1} [Field k] {n : ℕ} (a : Fin n → k) (j : Fin n) : Polynomial.eval (a j) (Polynomial.derivative (poleProd a)) = ∏ i ∈ Finset.univ.erase j, (a j - a i)

Logarithmic derivative formula: at a pole a_j of the denominator ∏(X − a_i), the derivative evaluates to ∏_{i ≠ j}(a_j − a_i).

theorem ResidueSum.partialFracNumer_coeff_top {k : Type u_1} [Field k] {n : ℕ} (c a : Fin n → k) : (partialFracNumer c a).coeff (n - 1) = ∑ i : Fin n, c i

The leading (degree n−1) coefficient of the partial-fraction numerator equals the sum of the residues Σ c_i.

theorem ResidueSum.derivative_at_simple_root {k : Type u_1} [Field k] (a : k) (R : Polynomial k) : Polynomial.eval a (Polynomial.derivative ((Polynomial.X - Polynomial.C a) * R)) = Polynomial.eval a R

Derivative of (X − a) · R at a is simply R(a) (the product rule specialised to a simple linear factor).

theorem ResidueSum.residue_eq_eval_div_cofactor {k : Type u_1} [Field k] (P R : Polynomial k) (a : k) (_hR : Polynomial.eval a R ≠ 0) : residueAtPole P ((Polynomial.X - Polynomial.C a) * R) a = Polynomial.eval a P / Polynomial.eval a R

Residue formula in factored form: the residue of P / ((X − a) · R) at a equals P(a) / R(a) when R(a) ≠ 0.

theorem ResidueSum.residue_partial_frac_eq_coeff {k : Type u_1} [Field k] {n : ℕ} (c a : Fin n → k) (j : Fin n) (hdist : Function.Injective a) : residuePartialFrac c a j = c j

The residue at the pole a_j of the canonical partial-fraction differential returns the input coefficient c_j.

theorem ResidueSum.residueAtInf_eq_neg_sum {k : Type u_1} [Field k] {n : ℕ} (c a : Fin n → k) : residueAtInfPartialFrac c a = -∑ i : Fin n, c i

The residue at infinity of the partial-fraction differential equals −Σ c_i, the negative of the sum of finite residues.

theorem ResidueSum.residue_sum_partial_frac {k : Type u_1} [Field k] {n : ℕ} (c a : Fin n → k) (hdist : Function.Injective a) : ∑ i : Fin n, residuePartialFrac c a i + residueAtInfPartialFrac c a = 0

Residue theorem for ℙ¹ in partial-fraction form: the sum of all residues (finite poles plus infinity) of a rational differential is zero.

theorem ResidueSum.residue_sum_const_over_two_linear {k : Type u_1} [Field k] (a b c : k) (hab : a ≠ b) : residueAtPole (Polynomial.C c) ((Polynomial.X - Polynomial.C a) * (Polynomial.X - Polynomial.C b)) a + residueAtPole (Polynomial.C c) ((Polynomial.X - Polynomial.C a) * (Polynomial.X - Polynomial.C b)) b = 0

Worked example with two simple poles: residues of c / ((X − a)(X − b)) at a and b cancel to zero (no pole at infinity).

theorem ResidueSum.residue_sum_poly_two_poles {k : Type u_1} [Field k] {P : Polynomial k} (a b : k) (hab : a ≠ b) (hP : P.natDegree ≤ 1) : residueAtPole P ((Polynomial.X - Polynomial.C a) * (Polynomial.X - Polynomial.C b)) a + residueAtPole P ((Polynomial.X - Polynomial.C a) * (Polynomial.X - Polynomial.C b)) b + -P.coeff 1 = 0

Residue identity with a degree-one numerator: Σ res P/((X−a)(X−b)) + (−[X]P) = 0, where the last term is the residue at infinity.

theorem ResidueSum.residue_sum_linear_over_two_poles {k : Type u_1} [Field k] (a b d e : k) (hab : a ≠ b) : (d * a + e) / (a - b) + (d * b + e) / (b - a) + -d = 0

Pure-algebra check for the two-pole identity: a fraction identity that underpins the residue cancellation in residue_sum_poly_two_poles.

theorem ResidueSum.residue_sum_logarithmic_form {k : Type u_1} [Field k] {n m : ℕ} (_zeros : Fin n → k) (_poles : Fin m → k) : ∑ _i : Fin n, 1 + ∑ _j : Fin m, -1 + (↑m - ↑n) = 0

Combinatorial form of the residue theorem for a logarithmic differential d log(f): zeros contribute +1, poles contribute −1, and infinity contributes (deg poles) − (deg zeros). The total is zero.