theorem HexRootsMathlib.logDeriv_eq_sum (p : Polynomial ℂ) {z : ℂ} (hz : Polynomial.eval z p ≠ 0) : Polynomial.eval z (Polynomial.derivative p) / Polynomial.eval z p = (Multiset.map (fun (a : ℂ) => (z - a)⁻¹) p.roots).sum

The logarithmic derivative of a complex polynomial is the sum of its reciprocal linear factors, counted over the root multiset.

theorem HexRootsMathlib.subInv_circleIntegrable {c a : ℂ} {R : ℝ} (ha : a ∉ Metric.sphere c |R|) : CircleIntegrable (fun (z : ℂ) => (z - a)⁻¹) c R

A reciprocal linear factor is circle integrable exactly when its pole is not on the circle (apart from the degenerate zero-radius case).

theorem HexRootsMathlib.integral_subInv_inside {c a : ℂ} {R : ℝ} (ha : a ∈ Metric.ball c R) : ∮ (z : ℂ) in C(c, R), (z - a)⁻¹ = 2 * ↑Real.pi * Complex.I

A pole strictly inside a positive-radius circle contributes 2πi.

theorem HexRootsMathlib.integral_subInv_outside {c a : ℂ} {R : ℝ} (hR : 0 ≤ R) (ha : a ∉ Metric.closedBall c R) : ∮ (z : ℂ) in C(c, R), (z - a)⁻¹ = 0

A pole outside the closed disc contributes zero.

theorem HexRootsMathlib.integral_sum_subInv {roots : Multiset ℂ} {c : ℂ} {R : ℝ} (hroots : ∀ a ∈ roots, a ∉ Metric.sphere c |R|) : ∮ (z : ℂ) in C(c, R), (Multiset.map (fun (a : ℂ) => (z - a)⁻¹) roots).sum = (Multiset.map (fun (a : ℂ) => ∮ (z : ℂ) in C(c, R), (z - a)⁻¹) roots).sum

Circle integration commutes with a finite multiset sum of reciprocal linear factors when none of the poles lies on the circle.

theorem HexRootsMathlib.logDeriv_circleIntegrable {p : Polynomial ℂ} (hp : p ≠ 0) {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hboundary : ∀ z ∈ Metric.sphere c R, Polynomial.eval z p ≠ 0) : CircleIntegrable (fun (z : ℂ) => Polynomial.eval z (Polynomial.derivative p) / Polynomial.eval z p) c R

If a polynomial has no root on a nonnegative-radius circle, then its logarithmic derivative is circle integrable.

theorem HexRootsMathlib.integral_logDeriv_eq_sum {p : Polynomial ℂ} (hp : p ≠ 0) {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hboundary : ∀ z ∈ Metric.sphere c R, Polynomial.eval z p ≠ 0) : ∮ (z : ℂ) in C(c, R), Polynomial.eval z (Polynomial.derivative p) / Polynomial.eval z p = (Multiset.map (fun (a : ℂ) => ∮ (z : ℂ) in C(c, R), (z - a)⁻¹) p.roots).sum

The circle integral of a polynomial logarithmic derivative is the multiset sum of its reciprocal-factor integrals.