Sendov's conjecture

Reference: Wikipedia

Tags: Sendov Conjecture, Ilieff's Conjecture.

def Sendov.Polynomial.IsSendov (f : Polynomial ℂ) : Prop

The predicate that a polynomial satisfies the hypotheses of Sendov's conjecture.

f.IsSendov holds if f has degree at least 2 and all roots of f lie in the unit disc of the complex plane.

Equations

• Sendov.Polynomial.IsSendov f = (2 ≤ f.natDegree ∧ f.rootSet ℂ ⊆ Metric.closedBall 0 1)

def Sendov.Nat.SatisfiesSendovConjecture (n : ℕ) : Prop

SatisfiesSendovConjecture n states that Sendov's conjecture is true for every polynomial of degree n.

Equations

• One or more equations did not get rendered due to their size.

theorem Sendov.sendov_conjecture (n : ℕ) (hn : 2 ≤ n) : 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) : 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, 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.