Sendov's conjecture

Reference: Wikipedia

Tags: Sendov Conjecture, Ilieff's Conjecture.

theorem Sendov.sendov_conjecture (n : ℕ) (hn : 2 ≤ n) : Sendov.Nat.SatisfiesSendovConjecture✝ n

Sendov's conjecture states that for a polynomial $$f(z)=(z-r_{1})\cdots (z-r_{n}),\qquad (n\geq 2)$$ with all roots $r_1, ..., r_n$ inside the closed unit disk $|z| ≤ 1$, each of the $n$ roots is at a distance no more than $1$ from at least one critical point.

theorem Sendov.sendov_conjecture.variants.le_nine (n : ℕ) (hn : n ∈ Set.Icc 2 9) : Sendov.Nat.SatisfiesSendovConjecture✝ n

Sendov's conjecture states that for a polynomial $$f(z)=(z-r_{1})\cdots (z-r_{n}),\qquad (n\geq 2)$$ with all roots $r_1, ..., r_n$ inside the closed unit disk $|z| ≤ 1$, each of the $n$ roots is at a distance no more than $1$ from at least one critical point.

It has been shown that Sendov's conjecture holds when the degree of $n$ is at most $9$.

theorem Sendov.sendov_conjecture.variants.eventually_true : ∀ᶠ (n : ℕ) in Filter.atTop, Sendov.Nat.SatisfiesSendovConjecture✝ n

Sendov's conjecture states that for a polynomial $$f(z)=(z-r_{1})\cdots (z-r_{n}),\qquad (n\geq 2)$$ with all roots $r_1, ..., r_n$ inside the closed unit disk $|z| ≤ 1$, each of the $n$ roots is at a distance no more than $1$ from at least one critical point.

It has been shown that Sendov's conjecture holds for polynomials of sufficiently large degree.