noncomputable def HexRootsTheory.rootsInDisc (p : Polynomial ℂ) (c : ℂ) (R : ℝ) : ℕ

Number of roots of p in the open disc, counted with multiplicity.

Equations

• HexRootsTheory.rootsInDisc p c R = Multiset.countP (fun (a : ℂ) => a ∈ Metric.ball c R) p.roots

theorem HexRootsTheory.integral_subInv_outside_of_not_mem {c a : ℂ} {R : ℝ} (hR : 0 ≤ R) (haSphere : a ∉ Metric.sphere c R) (haBall : a ∉ Metric.ball c R) : ∮ (z : ℂ) in C(c, R), (z - a)⁻¹ = 0

A reciprocal factor whose pole is neither inside nor on a nonnegative- radius circle has integral zero.

theorem HexRootsTheory.integral_logDeriv_eq_rootCount {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 = ↑(rootsInDisc p c R) * (2 * ↑Real.pi * Complex.I)

The unnormalized logarithmic-derivative integral is 2πi times the number of roots in the open disc, counted with multiplicity.

theorem HexRootsTheory.argumentPrinciple {p : Polynomial ℂ} (hp : p ≠ 0) {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hboundary : ∀ z ∈ Metric.sphere c R, Polynomial.eval z p ≠ 0) : (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(c, R), Polynomial.eval z (Polynomial.derivative p) / Polynomial.eval z p = ↑(rootsInDisc p c R)

Polynomial argument principle on a nonnegative-radius circle: the normalized logarithmic-derivative integral is the number of roots in the open disc, counted with multiplicity. The admitted case R = 0 is degenerate and both sides vanish.

theorem HexRootsTheory.rootsInDisc_eq_iff {p q : Polynomial ℂ} (hp : p ≠ 0) (hq : q ≠ 0) {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hpBoundary : ∀ z ∈ Metric.sphere c R, Polynomial.eval z p ≠ 0) (hqBoundary : ∀ z ∈ Metric.sphere c R, Polynomial.eval z q ≠ 0) : rootsInDisc p c R = rootsInDisc q c R ↔ (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(c, R), Polynomial.eval z (Polynomial.derivative p) / Polynomial.eval z p = (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(c, R), Polynomial.eval z (Polynomial.derivative q) / Polynomial.eval z q

Under the argument-principle hypotheses, equality of two normalized logarithmic-derivative integrals is equivalent to equality of their natural root counts.