Monotonicity of the elementary bound in the degree

Sendov.U bounds Sendov.R for every n ≥ 5. Here it is reduced to a single inequality in α alone, by showing that U n α is essentially decreasing in n on n ≥ 101.

Two features of the bound make this cheaper than it looks.

First, the sharp Beta constant collapses. The exponent is r = (n-4)/2, so

(r+1)(r+2)(r+3)(r+4) = (n-2) n (n+2) (n+4) / 16,

and the n (n-2) in it cancels the n (n-2) in the prefactor of Sendov.R exactly. The first tail term is therefore the rational function

T1 n α = 24 (n-1-2α)² / ((3+α) c⁴ (n-1)(n+2)(n+4)),

with no factorial-like growth left to control. (Had the cruder constant 6/r⁴ of the informal write-up been used, no such cancellation would occur and the corresponding step would need the degree-8 positivity certificate recorded there.)

Second, the surviving real power is a square: writing b = √B, the second tail term is T2 n α = A² n (n-1)(n-2)/(16(3+α)) · b ^ (n-4) with a natural exponent, so the geometric decay can be run as an ordinary induction on n rather than as an estimate on rpow.

The two certificates

T1 is not monotone in n by itself — at α = 17 the factor (n-1-2α)²/((n-1)(n+2)(n+4)) increases up to n ≈ 108 — so it is bounded by its value at n = 101 only after a 1% allowance, which the c⁴ in the denominator more than pays for. That allowance is Sendov.tail1_poly, a Bernstein certificate on 0 ≤ α ≤ 17. Its top coefficient is the only one in this development that is not a positive combination of powers of the degree offset; it is handled by completing the square, its quadratic part having negative discriminant.

Sendov.tail2_poly is the geometric step, and is an ordinary all-positive certificate.

Main statements

• Sendov.U_eq: U in closed form, T1 + T2 plus four elementary terms;
• Sendov.T1_le, Sendov.T2_le: the two tail bounds at n = 101;
• Sendov.U_le_Ut: U n α ≤ Ut α for n ≥ 101, where Ut involves no n and no rpow.

noncomputable def Sendov.T1 (n : ℕ) (α : ℝ) : ℝ

The first tail term of Sendov.U, in closed form.

Equations

• Sendov.T1 n α = 24 * (↑n - 1 - 2 * α) ^ 2 / ((3 + α) * Sendov.c n α ^ 4 * (↑n - 1) * (↑n + 2) * (↑n + 4))

noncomputable def Sendov.T2 (n : ℕ) (α : ℝ) : ℝ

The second tail term of Sendov.U, with the real power of B replaced by a natural power of √B.

Equations

• Sendov.T2 n α = Sendov.A n α ^ 2 * ↑n * Sendov.M n * (↑n - 2) / (16 * (3 + α)) * √(α / (3 + α)) ^ (n - 4)

The two polynomial certificates

theorem Sendov.tail1_poly {j α : ℝ} (hj : 0 ≤ j) (hα : 0 ≤ α) (hα' : α ≤ 17) : 108150000 * (100 + j - 2 * α) ^ 2 ≤ 101 * (100 - 2 * α) ^ 2 * ((100 + j) * (103 + j) * (105 + j))

The allowance for the first tail term: on 0 ≤ α ≤ 17 and N = 100 + j ≥ 100,

(N-2α)² / (N (N+3)(N+5)) ≤ (101/100) (100-2α)² / (100 · 103 · 105).

A Bernstein certificate in α on [0,17], whose coefficients are polynomials in j. The top one, 439956 j³ + 27356448 j² - 366591060 j + 4711014000, has a negative linear coefficient; it is nonnegative because its quadratic part has negative discriminant.

theorem Sendov.tail2_poly {k α : ℝ} (hk : 0 ≤ k) (hα : 0 ≤ α) (hα' : α ≤ 17) : 12 * (101 + k - 2 * α) ^ 2 * (102 + k) * (100 + k) ^ 2 ≤ 13 * (100 + k - 2 * α) ^ 2 * (99 + k) * (101 + k) ^ 2

The geometric step for the second tail term: on 0 ≤ α ≤ 17 and n = 101 + k ≥ 101,

12 A_{n+1}² (n+1) n (n-1) ≤ 13 A_n² n (n-1)(n-2),

after clearing the denominators n² and (n-1)² of A_{n+1} and A_n. Together with √B ≤ 12/13 this makes the step ratio less than one. A Bernstein certificate in α on [0,17] with all coefficients positive combinations of powers of k.

The closed form of U

theorem Sendov.c_mono {α : ℝ} {m n : ℕ} (hm : 2 ≤ m) (h : m ≤ n) (hα : 0 ≤ α) : c m α ≤ c n α

c increases with n: raising the degree moves c towards 1 - B/2.

theorem Sendov.rpow_B_eq {n : ℕ} {α : ℝ} (hn : 4 ≤ n) (hα : 0 ≤ α) : (α / (3 + α)) ^ ((↑n - 4) / 2) = √(α / (3 + α)) ^ (n - 4)

The real power of B in Sendov.U is a natural power of √B.

theorem Sendov.beta_prod (n : ℕ) : ((↑n - 4) / 2 + 1) * ((↑n - 4) / 2 + 2) * ((↑n - 4) / 2 + 3) * ((↑n - 4) / 2 + 4) = (↑n - 2) * ↑n * (↑n + 2) * (↑n + 4) / 16

The sharp Beta constant, factored. This is the cancellation that makes T1 rational: (r+1)(r+2)(r+3)(r+4) = (n-2) n (n+2)(n+4)/16 at r = (n-4)/2.

theorem Sendov.U_eq {n : ℕ} {α : ℝ} (hn : 5 ≤ n) (hα : 0 ≤ α) (hc : c n α ≠ 0) : U n α = 1 / 6 + 1 / (4 * (3 + α)) + 1 / (2 * M n) + 1 / (4 * M n * (3 + α)) + T1 n α + T2 n α

U in closed form. The n (n-2) of the prefactor cancels against the same factor in the sharp Beta constant, leaving a rational function plus a natural power of √B.

The first tail term

theorem Sendov.T1_le {n : ℕ} {α : ℝ} (hn : 101 ≤ n) (hα : 0 ≤ α) (hα' : α ≤ 17) : T1 n α ≤ 101 / 100 * T1 101 α

T1 is bounded by its value at n = 101, up to 1%.

The second tail term

theorem Sendov.sqrtB_le {α : ℝ} (hα : 0 ≤ α) (hα' : α ≤ 17) : √(α / (3 + α)) ≤ 12 / 13

√B ≤ 12/13 on 0 ≤ α ≤ 17, since B ≤ 17/20 ≤ (12/13)². A rational bound is enough here, and avoids carrying a square root into the step ratio.

theorem Sendov.T2_step {n : ℕ} {α : ℝ} (hn : 101 ≤ n) (hα : 0 ≤ α) (hα' : α ≤ 17) : T2 (n + 1) α ≤ T2 n α

One step of the geometric decay: T2 decreases with n on n ≥ 101.

theorem Sendov.T2_le {n : ℕ} {α : ℝ} (hn : 101 ≤ n) (hα : 0 ≤ α) (hα' : α ≤ 17) : T2 n α ≤ T2 101 α

T2 is bounded by its value at n = 101.

The bound with no degree left in it

noncomputable def Sendov.Ut (α : ℝ) : ℝ

The elementary bound at n = 101, with √B removed and α the only variable.

Equations

• Sendov.Ut α = 1 / 6 + 1 / (4 * (3 + α)) + 1 / 200 + 1 / (400 * (3 + α)) + 101 / 100 * Sendov.T1 101 α + (100 - 2 * α) ^ 2 / 100 * 101 * 99 / (16 * (3 + α)) * (α / (3 + α)) ^ 48

theorem Sendov.U_le_Ut {n : ℕ} {α : ℝ} (hn : 101 ≤ n) (hα : 0 ≤ α) (hα' : α ≤ 17) : U n α ≤ Ut α

U is bounded by an expression in α alone, for every n ≥ 101. This is where the degree leaves the argument.