From (1le) to stat

This is (1le) + (beta-bound) ⟹ stat. The right-hand side of (1le),

β(1)/(2α(1-β(1))) + β(1)/(4α) + 1/(2(n-1)) + β(1)/(4α(n-1)) + a⁴ n(n-1)(n-2) β(1)/(4α) ∫₀¹ t³ β(t)^((n-4)/2) dt,

is monotone increasing in β(1), so (beta-bound) lets β(1) be replaced throughout by α/(3+α). Under that substitution every term becomes the corresponding term of Sendov.R: β(1)/(2α(1-β(1))) becomes 1/6, β(1)/(4α) becomes 1/(4(3+α)), and ax, which is 1 - β(1)/2 - α/(n-1), becomes exactly Sendov.c n α.

Monotonicity of the integral term is the only part that is not immediate. ax decreases as β(1) grows, and Sendov.QQ decreases in its first argument on [0,1], so the integrand grows — Sendov.integral_QQ_anti. Nonnegativity of β(t) is needed only at the actual value ax, where it is (ax)² ≤ a², i.e. x² ≤ 1; at the substituted value it comes free from the pointwise comparison, the same way Sendov.integral_anti gets it in the batching argument.

Main statements

• Sendov.mul_eq_c: ax = 1 - β(1)/2 - α/(n-1), and hence c n α ≤ ax under (beta-bound);
• Sendov.stat_of_one_le: (1le) + (beta-bound) ⟹ 1 ≤ R n α.

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

ax = 1 - β(1)/2 - α/(n-1): the blog post's rearrangement of β(1) = 1 - 2ax + a².

theorem Sendov.c_le_mul {n : ℕ} {a x α : ℝ} (hn : 2 ≤ n) (hα : α = M n * (1 - a ^ 2) / 2) (hα0 : 0 < α) (hbeta : QQ (a * x) (a ^ 2) 1 ≤ α / (3 + α)) : c n α ≤ a * x

Under (beta-bound), Sendov.c n α ≤ ax: the substitution only ever lowers ax.

theorem Sendov.feasible_of_beta {n : ℕ} {a x α : ℝ} (hn : 2 ≤ n) (hx : x ^ 2 ≤ 1) (hα : α = M n * (1 - a ^ 2) / 2) (hα0 : 0 < α) (hbeta : QQ (a * x) (a ^ 2) 1 ≤ α / (3 + α)) : c n α ^ 2 ≤ A n α

(beta-bound) supplies the feasibility constraint c² ≤ A that Sendov.stat_lt_one requires. It is c ≤ ax squared, together with x² ≤ 1: the substitution can only lower ax, and ax is already at most a.

theorem Sendov.stat_of_one_le {n : ℕ} {a x α : ℝ} (hn : 5 ≤ n) (hx : x ^ 2 ≤ 1) (hα : α = M n * (1 - a ^ 2) / 2) (hα0 : 0 < α) (hbeta : QQ (a * x) (a ^ 2) 1 ≤ α / (3 + α)) (h1le : 1 ≤ QQ (a * x) (a ^ 2) 1 / (2 * α * (1 - QQ (a * x) (a ^ 2) 1)) + QQ (a * x) (a ^ 2) 1 / (4 * α) + 1 / (2 * M n) + QQ (a * x) (a ^ 2) 1 / (4 * α * M n) + (a ^ 2) ^ 2 * ↑n * M n * (↑n - 2) * QQ (a * x) (a ^ 2) 1 / (4 * α) * ∫ (t : ℝ) in 0..1, t ^ 3 * QQ (a * x) (a ^ 2) t ^ ((↑n - 4) / 2)) : 1 ≤ R n α

(1le) + (beta-bound) ⟹ stat.