Batching adjacent degrees

Every term of Sendov.R is monotone in n, and the directions cooperate: the elementary part decreases, the prefactor increases, and the moment decreases. So for a whole range of degrees n₀ ≤ n ≤ n₁ one bound suffices,

R n α ≤ base n₀ α + pref n₁ α * I n₀ α,

needing one moment and one certificate for the batch rather than one per degree.

The key identity is

Q (n+1) α t = Q n α t - (2α / (n(n-1))) * t * (1-t),

so Q decreases with n on [0,1]; combined with Q ≤ 1 and the exponent (n-4)/2 increasing, the moment decreases too.

This pays most where it costs most. Batch sizes track the slack in R n α, which is smallest near its maximum at n = 53 and grows away from it, so the expensive high degrees batch into the largest groups: measured, n ∈ [62,97] costs 12.5× less batched, against 2.8× in the tight middle. Note also that the certificate's degree is set by n₀, the smallest member, so a batch is cheaper than any single degree it covers except the first.

Main statements

• Sendov.Q_succ_sub: the identity above;
• Sendov.Q_anti: Q decreases with n on [0,1];
• Sendov.A_mono: A increases with n.

theorem Sendov.M_mono {m n : ℕ} (h : m ≤ n) : M m ≤ M n

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

A increases with n: raising the degree moves a² towards 1.

theorem Sendov.Q_succ_sub {α : ℝ} (n : ℕ) (hn : 2 ≤ n) (hα : 0 ≤ α) (t : ℝ) : Q (n + 1) α t = Q n α t - 2 * α / (↑n * (↑n - 1)) * t * (1 - t)

The degree step. Raising n by one lowers Q by a multiple of t(1-t).

theorem Sendov.Q_anti {α t : ℝ} {m n : ℕ} (hm : 2 ≤ m) (h : m ≤ n) (hα : 0 ≤ α) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : Q n α t ≤ Q m α t

Q decreases with n on [0,1].

The batch bound

theorem Sendov.rpow_le_rpow_exponent_ge' {x y z : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hz : 0 < z) (hzy : z ≤ y) : x ^ y ≤ x ^ z

x ^ y ≤ x ^ z for 0 ≤ x ≤ 1 and 0 < z ≤ y, allowing x = 0.

theorem Sendov.integral_anti {α : ℝ} {m n : ℕ} (hm : 5 ≤ m) (h : m ≤ n) (hα : 0 ≤ α) (hcm : 0 ≤ c m α) (hfn : c n α ^ 2 ≤ A n α) : ∫ (t : ℝ) in 0..1, t ^ 3 * Q n α t ^ ((↑n - 4) / 2) ≤ ∫ (t : ℝ) in 0..1, t ^ 3 * Q m α t ^ ((↑m - 4) / 2)

The moment decreases with the degree: Q falls and the exponent rises.

theorem Sendov.R_le_batch {α : ℝ} {n₀ n n₁ : ℕ} (h0 : 5 ≤ n₀) (h1 : n₀ ≤ n) (h2 : n ≤ n₁) (hα : 0 ≤ α) (hc0 : 0 ≤ c n₀ α) (hfn : c n α ^ 2 ≤ A n α) : R n α ≤ 1 / 6 + 1 / (4 * (3 + α)) + 1 / (2 * M n₀) + 1 / (4 * M n₀ * (3 + α)) + A n₁ α ^ 2 * ↑n₁ * M n₁ * (↑n₁ - 2) / (4 * (3 + α)) * ∫ (t : ℝ) in 0..1, t ^ 3 * Q n₀ α t ^ ((↑n₀ - 4) / 2)

The batch bound. One evaluation covers every degree in [n₀, n₁]: the elementary part and the moment at n₀, the prefactor at n₁.

Only 0 ≤ c n₀ α is required at n₀, not feasibility. That matters: feasibility propagates upward in n, so it could not be inherited from the hypothesis at n, and for n₀ < 36 it does not follow from α ≤ 17 either. Nonnegativity of Q at n₀ instead comes free from Q_anti, since Q n₀ ≥ Q n ≥ 0.