Kernel-checked Bernstein certificates

Each batch file Sendov.FiniteRange.Degree<n₀>_<n₁> proves R n α < 1 for n₀ ≤ n ≤ n₁ by bounding R n α through Sendov.R_le_batch by a rational function of α, and certifying that the numerator of 1 - bound is positive on the batch's α-range. Upstream, each certificate was an explicit polynomial identity closed by ring under a raised heartbeat budget, and the rational bound was cleared by field_simp in every batch. Here the same data are checked by the kernel instead:

• Sendov.bern p q d b expands ∑ⱼ bⱼ Xʲ (p - q X)^(d-j) into a coefficient list, so the statement "p ^ d • P has Bernstein coefficients b on [0, p/q]" is a decidable equality of lists, and Sendov.pev_pos_of_bern turns positive coefficients into positivity of P;
• Sendov.batchP n₀ n₁ k L Nmom computes the numerator polynomial directly from the batch parameters and the moment numerator, and Sendov.batch_lt_one proves once, for symbolic n₀, n₁, k, that positivity of this polynomial gives the batch bound < 1.

Numerals beyond 90 digits cannot sit on one line; Sendov.big assembles them from decimal chunks.

def Sendov.big (chunks : List ℕ) : ℤ

A large natural number assembled from little-endian chunks of at most 90 decimal digits, as an integer.

Equations

• Sendov.big chunks = ↑(Sendov.npev chunks (10 ^ 90))

Polynomial arithmetic on coefficient lists

def Sendov.pscale (c : ℤ) (p : List ℤ) : List ℤ

Scalar multiple of a dense integer polynomial.

Equations

• Sendov.pscale c p = List.map (fun (a : ℤ) => c * a) p

theorem Sendov.pev_pscale (c : ℤ) (p : List ℤ) (x : ℝ) : pev (pscale c p) x = ↑c * pev p x

def Sendov.psub (p q : List ℤ) : List ℤ

Difference of dense integer polynomials.

Equations

• Sendov.psub p q = Sendov.padd p (Sendov.pscale (-1) q)

theorem Sendov.pev_psub (p q : List ℤ) (x : ℝ) : pev (psub p q) x = pev p x - pev q x

def Sendov.ppow (p : List ℤ) : ℕ → List ℤ

Power of a dense integer polynomial.

Equations

• Sendov.ppow p 0 = [1]
• Sendov.ppow p k.succ = Sendov.pmul p (Sendov.ppow p k)

theorem Sendov.pev_ppow (p : List ℤ) (k : ℕ) (x : ℝ) : pev (ppow p k) x = pev p x ^ k

theorem Sendov.pev_lin (p q : ℤ) (x : ℝ) : pev [p, -q] x = ↑p - ↑q * x

theorem Sendov.pev_three_add (x : ℝ) : pev [3, 1] x = 3 + x

theorem Sendov.pev_X (x : ℝ) : pev [0, 1] x = x

Bernstein expansion

def Sendov.bern (p q : ℤ) : ℕ → List ℤ → List ℤ

bern p q d b is ∑ⱼ bⱼ Xʲ (p - q X)^(d-j) as a coefficient list, the entries of b being listed from j = 0.

Equations

• Sendov.bern p q x✝ [] = []
• Sendov.bern p q x✝ (a :: rest) = Sendov.padd (Sendov.pscale a (Sendov.ppow [p, -q] x✝)) (0 :: Sendov.bern p q (x✝ - 1) rest)

theorem Sendov.pev_bern_cons (p q : ℤ) (d : ℕ) (a : ℤ) (rest : List ℤ) (x : ℝ) : pev (bern p q d (a :: rest)) x = ↑a * (↑p - ↑q * x) ^ d + x * pev (bern p q (d - 1) rest) x

theorem Sendov.bern_nonneg {p q : ℤ} {x : ℝ} (hx : 0 ≤ x) (hxp : ↑q * x ≤ ↑p) (d : ℕ) (b : List ℤ) : (∀ a ∈ b, 0 ≤ a) → 0 ≤ pev (bern p q d b) x

theorem Sendov.bern_pos {p q : ℤ} (hp : 0 < p) {x : ℝ} (hx : 0 ≤ x) (hxp : ↑q * x ≤ ↑p) (d : ℕ) (b : List ℤ) : b.length = d + 1 → (∀ a ∈ b, 0 < a) → 0 < pev (bern p q d b) x

theorem Sendov.pev_pos_of_bern (P B : List ℤ) (p q : ℤ) (d : ℕ) (hp : 0 < p) (_hq : 0 < q) (hlen : B.length = d + 1) (hpos : ∀ a ∈ B, 0 < a) (hcert : bern p q d B = pscale (p ^ d) P) {x : ℝ} (hx : 0 ≤ x) (hxp : ↑q * x ≤ ↑p) : 0 < pev P x

Positivity from a Bernstein certificate: if bern p q d B = pscale (p ^ d) P and every entry of B is positive, then P is positive on [0, p/q]. All closed hypotheses are decidable and are discharged by the kernel in the batch files.

The batch bound as a rational function

def Sendov.batchD (n₀ n₁ k : ℕ) (L : ℤ) : List ℤ

The denominator of the batch bound of Sendov.R_le_batch, after the moment substitution, as a polynomial in α: with m₀ = n₀ - 1 and m₁ = n₁ - 1, 12 m₀ m₁² L (2m₀)^k (3+α)^(k+1).

Equations

• Sendov.batchD n₀ n₁ k L = Sendov.pscale (12 * (↑n₀ - 1) * (↑n₁ - 1) ^ 2 * L * (2 * (↑n₀ - 1)) ^ k) (Sendov.ppow [3, 1] (k + 1))

def Sendov.batchN (n₀ n₁ k : ℕ) (L : ℤ) (Nmom : List ℤ) : List ℤ

The numerator of the batch bound over the denominator Sendov.batchD.

Equations

• One or more equations did not get rendered due to their size.

def Sendov.batchP (n₀ n₁ k : ℕ) (L : ℤ) (Nmom : List ℤ) : List ℤ

The numerator of 1 - bound: the polynomial that each batch certifies positive.

Equations

• Sendov.batchP n₀ n₁ k L Nmom = Sendov.psub (Sendov.batchD n₀ n₁ k L) (Sendov.batchN n₀ n₁ k L Nmom)

theorem Sendov.two_alpha_le_of_le {n n₁ : ℕ} {α : ℝ} (hn : 2 ≤ n) (h1 : n ≤ n₁) (hfeas : c n α ^ 2 ≤ A n α) : 2 * α ≤ ↑n₁ - 1

theorem Sendov.batch_lt_one {n₀ n₁ k : ℕ} (hn₀ : 5 ≤ n₀) (hk : n₀ = 2 * k + 4) (h01 : n₀ ≤ n₁) (L : ℤ) (hL : 0 < L) (Nmom : List ℤ) {α : ℝ} (hα : 0 ≤ α) (hint : ∫ (t : ℝ) in 0..1, t ^ 3 * Q n₀ α t ^ k = pev Nmom α / (↑L * (2 * M n₀ * (3 + α)) ^ k)) (hP : 0 < pev (batchP n₀ n₁ k L Nmom) α) : 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) < 1

The batch bound is below 1 once its numerator Sendov.batchP is positive. The hypothesis hint is the packed moment identity of the batch (Sendov.integral_moment_packed), and the conclusion is exactly the right-hand side of Sendov.R_le_batch.