← Mathematical handbook

theorem Verification.bernstein_theta_off_corner (k i r : ℕ) (hi : i ≤ k) (_hr : r ≤ k) (hir : i + r < 2 * k) : 2 * bernsteinMixedGram (k + 1) i r = (↑i - ↑r) * ↑((k + 1).choose (i + 1)) * ↑((k + 1).choose (r + 1)) / ((2 * ↑k - ↑i - ↑r) * ↑((2 * k + 1).choose (i + r + 1)))

Off-corner entries of the paper's Theta matrix equal twice the mixed derivative Gram entry.

theorem Verification.bernstein_theta_corner (k : ℕ) : 2 * bernsteinMixedGram (k + 1) k k = 1

noncomputable def Verification.bernsteinTheta (k : ℕ) (i r : Fin (k + 1)) : ℝ

The source Theta matrix, with its special 0/0=1 convention at the last diagonal entry. The degree is k+1 and indices are source indices i+1,r+1.

Equations

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

theorem Verification.bernsteinTheta_eq_mixedGram (k : ℕ) (i r : Fin (k + 1)) : bernsteinTheta k i r = 2 * bernsteinMixedGram (k + 1) ↑i ↑r

theorem Verification.bernsteinTheta_add_transpose (k : ℕ) (i r : Fin (k + 1)) : bernsteinTheta k i r + bernsteinTheta k r i = if i = Fin.last k ∧ r = Fin.last k then 2 else 0