The batch 10 to 11

Sendov.R_le_batch bounds every R n α for 10 ≤ n ≤ 11 by the elementary part and moment at n₀ = 10 together with the prefactor at n₁ = 11, so one moment and one certificate serve all 2 degrees. The certificate has degree 8, set by n₀ rather than n₁.

Feasibility at n₀ is proved rather than assumed: for n ≥ 36 it follows from 0 ≤ α ≤ 17, since A - c² increases with n. This matters because feasibility propagates upward in n, so it could not be inherited from the hypothesis at n.

The moment numerator Nmomc is checked against the packed recurrence (Sendov.pev_wsum_eq_of_packed), and the numerator Sendov.batchP 10 11 3 Lc Nmomc of 1 - bound is certified positive on [0, 5] by its Bernstein coefficients Bc (Sendov.pev_pos_of_bern). Every closed computation is evaluated by the kernel.

def Sendov.Batch10To11.Lc : ℤ

The common denominator L of the moment weights: j + 4 ∣ L for every j < 2k + 1.

Equations

• Sendov.Batch10To11.Lc = 2520

def Sendov.Batch10To11.betac : ℤ

The base β at which polynomials in α are packed: it exceeds twice the absolute value of every coefficient of Nmomc and of the weighted row sum wsum Lc 0 (qrow …).

Equations

• Sendov.Batch10To11.betac = 82590802561

def Sendov.Batch10To11.tauc : ℤ

The base τ at which the recurrence rows, evaluated at betac, are packed into a single integer exponentiation: it exceeds twice the absolute value of every row entry.

Equations

• Sendov.Batch10To11.tauc = Sendov.big [81496854475499965300896802417388157646295122586173254149900368313668004057389423899346929, 484002949944962611058313401]

def Sendov.Batch10To11.Nmomc : List ℤ

The moment numerator at n₀ = 10, k = 3.

Equations

• Sendov.Batch10To11.Nmomc = [472392, 1312200, 1971216, 3407184, 294192, 12096, 192]

def Sendov.Batch10To11.Bc : List ℤ

Bernstein coefficients of 5 ^ 8 * batchP 10 11 3 Lc Nmomc on [0, 5].

Equations

• Sendov.Batch10To11.Bc = [7546462200000, 106071372072000, 590024221488000, 1022404934016000, 1176704065080000, 2736859476600000, 4242813219072000, 2642855620608000, 483084435456000]

theorem Sendov.Batch10To11.c_lo {α : ℝ} (hα : 0 ≤ α) : c 10 α = (54 + 3 * α - 2 * α ^ 2) / (18 * (3 + α))

theorem Sendov.Batch10To11.c_lo_nonneg {α : ℝ} (hα : 0 ≤ α) (hU : α ≤ 5) : 0 ≤ c 10 α

c is nonnegative at n₀ on the batch's α-range. This replaces feasibility at n₀, which for n₀ < 36 does not follow from α ≤ 17.

theorem Sendov.Batch10To11.pev_Nmomc (α : ℝ) : pev Nmomc α = pev (wsum Lc 0 (qrow (gg0 10) (gg1 10) (gg2 10) 3)) α

theorem Sendov.Batch10To11.integral_lo (α : ℝ) (hα : 0 ≤ α) : ∫ (t : ℝ) in 0..1, t ^ 3 * Q 10 α t ^ 3 = pev Nmomc α / (↑Lc * (2 * M 10 * (3 + α)) ^ 3)

theorem Sendov.Batch10To11.P_pos {α : ℝ} (hα : 0 ≤ α) (hU : 1 * α ≤ 5) : 0 < pev (batchP 10 11 3 Lc Nmomc) α

The certificate: batchP 10 11 3 Lc Nmomc is positive on [0, 5].

theorem Sendov.Batch10To11.finite_range {n : ℕ} (h0 : 10 ≤ n) (h1 : n ≤ 11) {α : ℝ} (hα : 0 ≤ α) (_hα' : α ≤ 17) (hfeas : c n α ^ 2 ≤ A n α) : R n α < 1

The batch 10 ≤ n ≤ 11.