Sendov's conjecture and the Phelps–Rodriguez conjecture

Let n ≥ 2 and let p be a degree n polynomial with all zeroes in the closed unit disk. Then for every zero a of p there is a critical point ζ of p with ‖ζ - a‖ ≤ 1 (Sendov), and in fact with ‖ζ - a‖ < 1 unless ‖a‖ = 1 and p is a scalar multiple of zⁿ - aⁿ (Phelps–Rodriguez).

Everything mathematical is already done: this file only removes the normalization a ∈ [0,1) by rotating the variable. Writing a = ω r with ‖ω‖ = 1 and r = ‖a‖, the polynomial p(ωz) has the same degree, still has all its zeroes in the closed unit disk, and vanishes at the real point r. Its critical points are the ω⁻¹ζ, and ‖ω⁻¹ζ - r‖ = ‖ζ - a‖, so the conclusion transports back unchanged.

Three cases, by the position of a:

• a = 0: Sendov.sendov_center;
• 0 < ‖a‖ < 1: Sendov.sendov_interior_real after rotating;
• ‖a‖ = 1: Sendov.rubinstein_one after rotating, whose extremal polynomial c(zⁿ - 1) rotates back to c ω⁻ⁿ (zⁿ - aⁿ).

Main statements

• Sendov.phelps_rodriguez: the Phelps–Rodriguez conjecture;
• Sendov.sendov: Sendov's conjecture.

Rotating the variable

noncomputable def Sendov.rotate (ω : ℂ) (p : Polynomial ℂ) : Polynomial ℂ

p(ωz).

Equations

• Sendov.rotate ω p = p.comp (Polynomial.C ω * Polynomial.X)

@[simp]

theorem Sendov.eval_rotate (ω : ℂ) (p : Polynomial ℂ) (x : ℂ) : Polynomial.eval x (rotate ω p) = Polynomial.eval (ω * x) p

theorem Sendov.natDegree_rotate {ω : ℂ} (hω : ω ≠ 0) (p : Polynomial ℂ) : (rotate ω p).natDegree = p.natDegree

theorem Sendov.derivative_rotate (ω : ℂ) (p : Polynomial ℂ) : Polynomial.derivative (rotate ω p) = Polynomial.C ω * rotate ω (Polynomial.derivative p)

theorem Sendov.eval_derivative_rotate (ω : ℂ) (p : Polynomial ℂ) (x : ℂ) : Polynomial.eval x (Polynomial.derivative (rotate ω p)) = ω * Polynomial.eval (ω * x) (Polynomial.derivative p)

theorem Sendov.rotate_rotate_inv {ω : ℂ} (hω : ω ≠ 0) (p : Polynomial ℂ) : rotate ω⁻¹ (rotate ω p) = p

Rotating is undone by rotating back.

theorem Sendov.roots_rotate {ω : ℂ} (hω : ‖ω‖ = 1) {p : Polynomial ℂ} (hp : p ≠ 0) (hroots : ∀ w ∈ p.roots, ‖w‖ ≤ 1) (w : ℂ) : w ∈ (rotate ω p).roots → ‖w‖ ≤ 1

The Phelps–Rodriguez conjecture

theorem Sendov.phelps_rodriguez {n : ℕ} (hn : 2 ≤ n) {p : Polynomial ℂ} (hdeg : p.natDegree = n) (hroots : ∀ w ∈ p.roots, ‖w‖ ≤ 1) {a : ℂ} (hpa : Polynomial.eval a p = 0) : (∃ (ζ : ℂ), Polynomial.eval ζ (Polynomial.derivative p) = 0 ∧ ‖ζ - a‖ < 1) ∨ ‖a‖ = 1 ∧ ∃ (c : ℂ), c ≠ 0 ∧ p = Polynomial.C c * (Polynomial.X ^ n - Polynomial.C (a ^ n))

The Phelps–Rodriguez conjecture. Every zero a of a degree n ≥ 2 polynomial with all zeroes in the closed unit disk has a critical point strictly within distance 1, unless a is on the unit circle and p is a scalar multiple of zⁿ - aⁿ.

Sendov's conjecture

theorem Sendov.sendov {n : ℕ} (hn : 2 ≤ n) {p : Polynomial ℂ} (hdeg : p.natDegree = n) (hroots : ∀ w ∈ p.roots, ‖w‖ ≤ 1) {a : ℂ} (hpa : Polynomial.eval a p = 0) : ∃ (ζ : ℂ), Polynomial.eval ζ (Polynomial.derivative p) = 0 ∧ ‖ζ - a‖ ≤ 1

Sendov's conjecture. Every zero of a degree n ≥ 2 polynomial with all zeroes in the closed unit disk has a critical point within distance 1.

The statements of record

Upstream states both theorems a second time, in the Mathlib-only form that its comparator configuration checks: the degree hypothesis is 2 ≤ p.natDegree rather than a separate n, and the disk hypothesis quantifies over all of ℂ rather than over Polynomial.roots. Each is a thin bridge to the theorem above; both differences are bookkeeping only, and the hypotheses here are the weaker pair, so these conclusions are the stronger claims.

theorem SendovConjecture.sendov {p : Polynomial ℂ} (hdeg : 2 ≤ p.natDegree) (hzeroes : ∀ (w : ℂ), Polynomial.eval w p = 0 → ‖w‖ ≤ 1) {a : ℂ} (hpa : Polynomial.eval a p = 0) : ∃ (ζ : ℂ), Polynomial.eval ζ (Polynomial.derivative p) = 0 ∧ ‖ζ - a‖ ≤ 1

Sendov's conjecture, in the Mathlib-only form of the upstream statement of record: proved by Sendov.sendov.

theorem SendovConjecture.phelps_rodriguez {p : Polynomial ℂ} (hdeg : 2 ≤ p.natDegree) (hzeroes : ∀ (w : ℂ), Polynomial.eval w p = 0 → ‖w‖ ≤ 1) {a : ℂ} (hpa : Polynomial.eval a p = 0) : (∃ (ζ : ℂ), Polynomial.eval ζ (Polynomial.derivative p) = 0 ∧ ‖ζ - a‖ < 1) ∨ ‖a‖ = 1 ∧ ∃ (c : ℂ), c ≠ 0 ∧ p = Polynomial.C c * (Polynomial.X ^ p.natDegree - Polynomial.C (a ^ p.natDegree))

The Phelps–Rodriguez conjecture, in the Mathlib-only form of the upstream statement of record: proved by Sendov.phelps_rodriguez.