← Mathematical handbook

noncomputable def Verification.bernsteinGram (m n i j : ℕ) : ℝ

Explicit Bernstein Gram entry, with natural-number binomial coefficients.

Equations

• Verification.bernsteinGram m n i j = ↑(m.choose i) * ↑(n.choose j) / ((↑m + ↑n + 1) * ↑((m + n).choose (i + j)))

noncomputable def Verification.bernsteinDerivativeGram (m i r : ℕ) : ℝ

Derivative Gram entry in a uniform finite-difference form, including the last row.

Equations

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

theorem Verification.bernsteinDerivative_succ (m i : ℕ) (u : ↑unitInterval) : bernsteinDerivative m (i + 1) u = ↑m * ((bernstein (m - 1) i) u - (bernstein (m - 1) (i + 1)) u)

theorem Verification.integral_bernsteinDerivative_product (m i r : ℕ) : ∫ (u : ↑unitInterval), bernsteinDerivative m (i + 1) u * bernsteinDerivative m (r + 1) u = bernsteinDerivativeGram m i r