Basic properties of the quantities in the finite-range claim

Elementary facts about Sendov.M, Sendov.A, Sendov.c and Sendov.Q, used by every degree-specific argument. The two facts that matter are:

• Sendov.Q_nonneg: the feasibility constraint c ^ 2 ≤ A says exactly that Q is a sum of squares, hence nonnegative. This is what makes the real power Q ^ ((n-4)/2) appearing in Sendov.R behave, and in particular avoids the junk values of Real.rpow at negative bases.
• Sendov.Q_one: Q n α 1 = α / (3 + α), the value B prescribed by the simplified polar inequality of the blog post. Since Q n α 1 = 1 - 2 * c n α + A n α, this pins down A - 2 * c = B - 1 < 0, which is what gives Sendov.Q_le_one.

theorem Sendov.M_pos {n : ℕ} (hn : 2 ≤ n) : 0 < M n

theorem Sendov.three_add_pos {α : ℝ} (hα : 0 ≤ α) : 0 < 3 + α

theorem Sendov.Q_eq (n : ℕ) (α t : ℝ) : Q n α t = (1 - c n α * t) ^ 2 + (A n α - c n α ^ 2) * t ^ 2

Q written as a sum of squares. Compare β(t) = (1 - a x t) ^ 2 + a² t² (1 - x²) in the blog post.

theorem Sendov.A_nonneg {n : ℕ} {α : ℝ} (hfeas : c n α ^ 2 ≤ A n α) : 0 ≤ A n α

Feasibility forces a² ≥ 0.

theorem Sendov.alpha_le_half_M {n : ℕ} {α : ℝ} (hn : 2 ≤ n) (hfeas : c n α ^ 2 ≤ A n α) : α ≤ M n / 2

Feasibility bounds α by (n-1)/2, simply because it forces A = 1 - 2α/(n-1) ≥ 0.

This crude consequence is all that the numerical step of any degree needs: on 0 ≤ α ≤ min 17 ((n-1)/2) the upper bounds for R n α used in this development stay below 0.856 for every 5 ≤ n ≤ 97. The exact shape of the feasible region, which is cut out by a quartic in α, is therefore never required by the polynomial certificates.

This must not be read as saying that A ≥ 0 replaces feasibility everywhere. It does not: the odd-degree bound needs 0 ≤ Q n α t on [0,1], which is Sendov.Q_nonneg and uses the full constraint c ^ 2 ≤ A — it does not follow from A ≥ 0. Accordingly Sendov.integral_rpow_le takes hfeas itself, and only the passage from the resulting rational function to a polynomial positivity statement is weakened to α ≤ M n / 2. For even degrees the moment identity Sendov.integral_moment needs no hypothesis at all.

theorem Sendov.Q_nonneg {n : ℕ} {α : ℝ} (hfeas : c n α ^ 2 ≤ A n α) (t : ℝ) : 0 ≤ Q n α t

theorem Sendov.Q_one {n : ℕ} {α : ℝ} (hn : 2 ≤ n) (hα : 0 ≤ α) : Q n α 1 = α / (3 + α)

Q n α 1 = B = α / (3 + α): the substituted quadratic takes at t = 1 the value that the simplified polar inequality β(1) < α / (3 + α) prescribes.

theorem Sendov.Q_le_one {n : ℕ} {α t : ℝ} (hn : 2 ≤ n) (hα : 0 ≤ α) (hc : 0 ≤ c n α) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : Q n α t ≤ 1

Q is convex with Q 0 = 1 and Q 1 = B ≤ 1, hence bounded by 1 on [0,1].

Only 0 ≤ c is needed, not 0 ≤ A: writing Q t - 1 = t (A t - 2c), the identity Q 1 = B < 1 gives A ≤ 2c outright, and then A t ≤ 2c holds whether A is nonnegative (as A t ≤ A) or negative (as A t ≤ 0 ≤ 2c). That matters for batches of degrees whose α-range reaches past (n₀-1)/2, where A n₀ α can be negative.

theorem Sendov.c_pos_of_le_half_M {n : ℕ} {α : ℝ} (hn : 2 ≤ n) (hα : 0 ≤ α) (hhalf : α ≤ M n / 2) : 0 < c n α

Feasibility gives α ≤ (n-1)/2, and hence c ≥ (1-B)/2 > 0.

theorem Sendov.R_le_of_integral_le {n : ℕ} {α : ℝ} (hn : 2 ≤ n) (hα : 0 ≤ α) {J : ℝ} (hJ : ∫ (t : ℝ) in 0..1, t ^ 3 * Q n α t ^ ((↑n - 4) / 2) ≤ J) : R n α ≤ 1 / 6 + 1 / (4 * (3 + α)) + 1 / (2 * M n) + 1 / (4 * M n * (3 + α)) + A n α ^ 2 * ↑n * M n * (↑n - 2) / (4 * (3 + α)) * J

The coefficient multiplying the integral in Sendov.R is nonnegative, so any upper bound for the integral yields an upper bound for R. This is how each degree replaces its integral by an explicit rational function.