The finite-range claim in degree seven

The first odd degree, and the prototype for the general odd-degree argument. Here the exponent (n-4)/2 is 1 + 1/2, so Sendov.integral_rpow_le replaces the square root by the average of the moments of Q and Q ^ 2, after which the argument runs exactly as in degree six.

With M 7 = 6, A 7 α = 1 - α/3 and c 7 α = (18 - α²)/(6(3+α)):

• ∫ t in 0..1, t³ (Q + Q²)/2 dt = 1/4 - 3c/5 + (4c² + 3A)/12 - 2cA/7 + A²/16;
• the resulting upper bound for R 7 α is 1 - P α / (2592 (3+α)³) with P α = -5α⁶ - 222α⁵ - 2619α⁴ + 17388α³ + 19413α² - 5022α + 33291;
• feasibility enters only through Sendov.alpha_le_half_M, which gives α ≤ 3.

P is positive up to α = 5.338, so once again there is ample room. The exact feasible range is α ≤ 2.710, cut out by -α⁴ - 12α³ + 108α ≥ 0, but that is not needed. Since the odd-degree bound is an inequality rather than an identity, the loss it incurs is real but small: the exact maximum of R 7 α over the feasible range is about 0.598, against 0.664 for this upper bound.

theorem Sendov.M_seven : M 7 = 6

theorem Sendov.A_seven (α : ℝ) : A 7 α = 1 - α / 3

theorem Sendov.c_seven (α : ℝ) : c 7 α = 1 - α / 6 - α / (2 * (3 + α))

theorem Sendov.c_seven' {α : ℝ} (hα : 0 ≤ α) : c 7 α = (18 - α ^ 2) / (6 * (3 + α))

theorem Sendov.integral_seven {α : ℝ} (hfeas : c 7 α ^ 2 ≤ A 7 α) : ∫ (t : ℝ) in 0..1, t ^ 3 * Q 7 α t ^ ((↑7 - 4) / 2) ≤ 1 / 4 - 3 * c 7 α / 5 + (4 * c 7 α ^ 2 + 3 * A 7 α) / 12 - 2 * c 7 α * A 7 α / 7 + A 7 α ^ 2 / 16

The odd-degree bound in degree seven: the exponent is 1 + 1/2, so the integral is bounded by the average of the first two moments, which is computed exactly.

theorem Sendov.R_seven_le {α : ℝ} (hα : 0 ≤ α) (hfeas : c 7 α ^ 2 ≤ A 7 α) : R 7 α ≤ 1 / 6 + 1 / (4 * (3 + α)) + 1 / 12 + 1 / (24 * (3 + α)) + 210 * A 7 α ^ 2 / (4 * (3 + α)) * (1 / 4 - 3 * c 7 α / 5 + (4 * c 7 α ^ 2 + 3 * A 7 α) / 12 - 2 * c 7 α * A 7 α / 7 + A 7 α ^ 2 / 16)

The upper bound for R 7 α obtained from Sendov.integral_seven.

theorem Sendov.finite_range_seven {α : ℝ} (hα : 0 ≤ α) (hfeas : c 7 α ^ 2 ≤ A 7 α) : R 7 α < 1

The finite-range claim in degree seven.