The two factorizations

A polynomial p of degree n over ℂ splits, so it factors over its roots, and so does p'. The blog post writes these as

p(z) = (z-a) ∏ⱼ (z - zⱼ), p'(z) = n ∏ⱼ (z - a + 1/qⱼ),

where a is the distinguished root, the zⱼ are the others, and the critical points are written as a - 1/qⱼ — possible exactly because each lies at distance at least 1 from a, which puts each qⱼ in the closed unit disk.

Everything here is deliberately hypothesis-light. Nothing is assumed about a beyond its being a root: not that it is real, not that |a| < 1, not that a ≠ 0. The boundary case |a| = 1 of Rubinstein's theorem needs these same two factorizations, and would not be able to use them if |a| < 1 were baked in here. The stronger hypotheses enter one layer up.

Roots are kept as multisets throughout, which is how Mathlib produces them and what allows repeated roots without comment.

A note on the proofs: the root multisets are extracted with obtain ⟨z, hz⟩ : ∃ z, … := ⟨_, rfl⟩ rather than named with set. Rewriting p = C p.leadingCoeff * (p.roots.map …).prod into a goal that still mentions p.roots otherwise loops, and set leaves a local definition that rewriting unfolds again. An opaque local is what is wanted.

Main statements

• Sendov.exists_root_multiset: the factorization of p over a and the other roots;
• Sendov.exists_crit_multiset: the factorization of p' over the reciprocal coordinates q.

theorem Sendov.exists_root_multiset {n : ℕ} (hn : 1 ≤ n) {p : Polynomial ℂ} (hdeg : p.natDegree = n) (hroots : ∀ w ∈ p.roots, ‖w‖ ≤ 1) {a : ℂ} (hpa : Polynomial.eval a p = 0) : ∃ (z : Multiset ℂ), z.card = n - 1 ∧ (∀ w ∈ z, ‖w‖ ≤ 1) ∧ p = Polynomial.C p.leadingCoeff * ((Polynomial.X - Polynomial.C a) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) z).prod)

The factorization of p over its roots, with the distinguished root a split off.

theorem Sendov.exists_crit_multiset {n : ℕ} (hn : 2 ≤ n) {p : Polynomial ℂ} (hdeg : p.natDegree = n) {a : ℂ} (hcrit : ∀ (w : ℂ), Polynomial.eval w (Polynomial.derivative p) = 0 → 1 ≤ ‖w - a‖) : ∃ (q : Multiset ℂ), q.card = n - 1 ∧ (∀ v ∈ q, ‖v‖ ≤ 1) ∧ (∀ v ∈ q, v ≠ 0) ∧ Polynomial.derivative p = Polynomial.C (↑n * p.leadingCoeff) * (Multiset.map (fun (v : ℂ) => Polynomial.X - Polynomial.C (a - v⁻¹)) q).prod

The factorization of p'. Each critical point w lies at distance at least 1 from a, so (a - w)⁻¹ lies in the closed unit disk and w = a - ((a-w)⁻¹)⁻¹.