The bound α ≤ 17

This is (beta-bound) + (origin-exact) ⟹ (17), the last link of the chain. Suppose α > 17. Feasibility gives n - 1 ≥ 2α > 34, so n ≥ 36, and after discarding ax > 0 and bounding 1 - x² ≤ 1, (origin-exact) reads

2α ≤ 1/(2(n-1)) + a² n (n-1) ∫₀¹ t β(t)^((n-2)/2) dt.

The integral is split by Sendov.integral_le_tail_lin — the k = 1 instance of the chord bound — into a Beta value plus β(1)^((n-2)/2)/2. Both halves of (beta-bound) are then used, and this is the only place where the logarithmic half is needed:

• x² ≥ 1 - β(1) ≥ log α / α turns the Beta term into 4α/log α;
• β(1) ≤ e^{β(1)-1} ≤ α^{-1/α} makes the second term decay geometrically.

Dividing by α leaves 2 ≤ 1/(2(n-1)α) + 4/log α + T, and the substitution v := (n-1)/(2α) - 1 (the write-up's u = a²/(1-a²)) turns T into v(2(v+1) + 1/α) α^{-v} · α^{1/(2α)}, which is bounded by an ordinary polynomial inequality after four terms of the exponential series. The three pieces come to 0.0009 + 1.4135 + 0.5054 = 1.920 < 2.

The write-up uses ∫₀^∞ t e^{-ct} dt here and reaches 1.948; the Beta route used instead reaches 1.817, and the extra room is what pays for the crude constants below.

Main statements

• Sendov.log_seventeen_ge, Sendov.log_le_div_exp_one: the two facts about log needed;
• Sendov.alpha_le_seventeen: (beta-bound) + (origin-exact) ⟹ α ≤ 17.

Elementary estimates

theorem Sendov.quartic_le_exp {z : ℝ} (hz : 0 ≤ z) : 1 + z + z ^ 2 / 2 + z ^ 3 / 6 ≤ Real.exp z

Four terms of the exponential series.

theorem Sendov.log_le_div_exp_one {t : ℝ} (ht : 0 < t) : Real.log t ≤ t / Real.exp 1

log t ≤ t / e, the tangent bound at t = e.

theorem Sendov.exp_le_one_div_one_sub {z : ℝ} (hz : z < 1) : Real.exp z ≤ 1 / (1 - z)

exp z ≤ 1/(1-z) for z < 1, from 1 - z ≤ e^{-z}.

theorem Sendov.log_seventeen_ge : 2.83 ≤ Real.log 17

2.83 ≤ log 17, via log 16 + log(17/16) ≥ 4 log 2 + 1/17.

theorem Sendov.tail_poly_bound {v : ℝ} (hv : 0 ≤ v) : v * (2 * (v + 1) + 1 / 17) * Real.exp (-(2.83 * v)) ≤ 0.4118

The polynomial bound behind the geometric term: v(2v + 2 + 1/17) e^{-2.83 v} ≤ 0.4118 for v ≥ 0. Four terms of the exponential series suffice; the true maximum is 0.3722.

The bound

theorem Sendov.alpha_le_seventeen {n : ℕ} {a x α : ℝ} (hn : 5 ≤ n) (ha : 0 < a) (ha1 : a < 1) (hx : x ^ 2 ≤ 1) (hα : α = M n * (1 - a ^ 2) / 2) (hbeta : QQ (a * x) (a ^ 2) 1 ≤ α / (3 + α)) (hlogb : Real.log α ≤ α * (1 - QQ (a * x) (a ^ 2) 1)) (horigin : 2 * α + a * x ≤ (1 - x ^ 2) / (2 * M n) + a ^ 2 * ↑n * M n * ∫ (t : ℝ) in 0..1, t * QQ (a * x) (a ^ 2) t ^ ((↑n - 2) / 2)) : α ≤ 17

(beta-bound) + (origin-exact) ⟹ α ≤ 17.