The raw inequalities, and the dictionary between them and Sendov.R

Sendov.stat_lt_one refutes equation stat of the blog post. stat is itself deduced there from two inequalities that come out of the complex-analytic part of the argument:

• the raw polar inequality (1Q), 1 ≤ ∫₀¹ P(t)^((n-1)/2) dt with P(t) = a² + 2atx(1-a²) + t²(1-a²)²;
• the raw origin inequality (origin-exact), 2α + ax ≤ (1-x²)/(2(n-1)) + a²n(n-1) ∫₀¹ t β(t)^((n-2)/2) dt.

Both are statements about two real numbers a ∈ (0,1) and x ∈ [-1,1] and a degree n; no polynomial, no complex number and no q_j survives into them. That is what makes the next target — that the two are not simultaneously satisfiable for n ≥ 5 — a self-contained real-variable statement.

This file fixes P and records the dictionary. The key entry is that α and a determine each other: with α = (n-1)(1-a²)/2 one has A n α = a² exactly, so the A of Sendov.Defs and the a² of the blog post are the same thing, and β(t) is Sendov.QQ (a*x) (a^2) t while Q n α t is Sendov.QQ (c n α) (A n α) t.

Main statements

• Sendov.Ppolar_eq: P as a sum of squares, hence nonnegative for |x| ≤ 1;
• Sendov.A_eq_sq: A n α = a²;
• Sendov.alpha_pos, Sendov.alpha_le_half: the range of α.

noncomputable def Sendov.Ppolar (a x t : ℝ) : ℝ

The integrand of the raw polar inequality (1Q).

Equations

• Sendov.Ppolar a x t = a ^ 2 + 2 * a * t * x * (1 - a ^ 2) + t ^ 2 * (1 - a ^ 2) ^ 2

theorem Sendov.Ppolar_eq (a x t : ℝ) : Ppolar a x t = (a + t * (1 - a ^ 2) * x) ^ 2 + t ^ 2 * (1 - a ^ 2) ^ 2 * (1 - x ^ 2)

P is a sum of squares once |x| ≤ 1; this is the same computation that makes Sendov.QQ_nonneg work.

theorem Sendov.Ppolar_nonneg {x : ℝ} (hx : x ^ 2 ≤ 1) (a t : ℝ) : 0 ≤ Ppolar a x t

theorem Sendov.continuous_Ppolar (a x : ℝ) : Continuous fun (t : ℝ) => Ppolar a x t

theorem Sendov.A_eq_sq {n : ℕ} {a α : ℝ} (hn : 2 ≤ n) (hα : α = M n * (1 - a ^ 2) / 2) : A n α = a ^ 2

With α = (n-1)(1-a²)/2, the A of Sendov.Defs is exactly a².

theorem Sendov.alpha_pos {n : ℕ} {a α : ℝ} (hn : 2 ≤ n) (ha1 : a < 1) (_ha0 : 0 ≤ a) (hα : α = M n * (1 - a ^ 2) / 2) : 0 < α

theorem Sendov.alpha_le_half {n : ℕ} {a α : ℝ} (hn : 2 ≤ n) (hα : α = M n * (1 - a ^ 2) / 2) : α ≤ M n / 2