← Mathematical handbook

theorem Verification.bernsteinDerivative_factor (k i : ℕ) (hi : i ≤ k) (u : ↑unitInterval) : bernsteinDerivative (k + 2) (i + 1) u = ↑((k + 2).choose (i + 1)) * ↑u ^ i * (1 - ↑u) ^ (k - i) * (↑i + 1 - (↑k + 2) * ↑u)

Interior-index Bernstein derivatives factor into a beta monomial and a linear polynomial.

theorem Verification.bernsteinDerivative_last (k : ℕ) (u : ↑unitInterval) : bernsteinDerivative (k + 1) (k + 1) u = (↑k + 1) * ↑u ^ k