The tail bound

The large-degree argument replaces the integral in Sendov.R by an elementary expression:

∫₀¹ t³ Q^r dt ≤ 6 / (c⁴ (r+1)(r+2)(r+3)(r+4)) + Bʳ / 4.

This is the only part of the large-degree argument that touches integration; everything after it is elementary inequalities in α and n.

The work is done by Sendov.integral_le_tail_cube in Sendov.Common.Chord, which proves the same split for the general quadratic QQ c A and an arbitrary weight t^k — the α ≤ 17 argument needs the k = 1 instance of it. All that is left here is to read that bound through Q n α t = QQ (c n α) (A n α) t and Q n α 1 = α/(3+α).

Main statements

• Sendov.c_le_one: c ≤ 1, so the chord's zero 1/c is at least 1;
• Sendov.integral_le_tail: the bound above.

theorem Sendov.c_le_one {n : ℕ} {α : ℝ} (hn : 2 ≤ n) (hα : 0 ≤ α) : c n α ≤ 1

c ≤ 1, so the chord's zero 1/c is at least 1.

theorem Sendov.integral_le_tail {n : ℕ} {α : ℝ} (hn : 2 ≤ n) (hα : 0 ≤ α) (hfeas : c n α ^ 2 ≤ A n α) (hc : 0 < c n α) {r : ℝ} (hr : 0 < r) : ∫ (t : ℝ) in 0..1, t ^ 3 * Q n α t ^ r ≤ 6 / (c n α ^ 4 * ((r + 1) * (r + 2) * (r + 3) * (r + 4))) + (α / (3 + α)) ^ r / 4

The tail bound, read off from Sendov.integral_le_tail_cube.

The elementary upper bound U

Everything after this point in the large-degree argument is an inequality in α and n alone; no integral survives.

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

The elementary bound replacing Sendov.R: (11) of the informal write-up, but with the sharper Beta constant 6/((r+1)(r+2)(r+3)(r+4)) in place of 6/r⁴.

Equations

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

theorem Sendov.c_ge_of_large {n : ℕ} {α : ℝ} (hn : 101 ≤ n) (hα : 0 ≤ α) (hα' : α ≤ 17) : 81 / 200 ≤ c n α

On the large-degree range c is bounded below, hence positive. For n ≥ 101 and α ≤ 17 this gives c ≥ 81/200, which is (3) of the write-up.

theorem Sendov.R_le_U {n : ℕ} {α : ℝ} (hn : 5 ≤ n) (hα : 0 ≤ α) (hfeas : c n α ^ 2 ≤ A n α) (hc : 0 < c n α) : R n α ≤ U n α

R is bounded by the elementary expression U. This is the bridge out of integration: from here the large-degree argument is elementary.