Documentation

Verification.BernsteinProducts

← Mathematical handbook
source
theorem Verification.bernstein_product (m n : ℕ) (i : Fin (m + 1)) (j : Fin (n + 1)) (u : ↑unitInterval) :
(bernstein m ↑i) u * (bernstein n ↑j) u = ↑(m.choose ↑i) * ↑(n.choose ↑j) / ↑((m + n).choose (↑i + ↑j)) * (bernstein (m + n) (↑i + ↑j)) u

Product of Bernstein basis functions, including endpoint indices.

source
theorem Verification.integral_bernstein_product (m n : ℕ) (i : Fin (m + 1)) (j : Fin (n + 1)) :
∫ (u : ↑unitInterval), (bernstein m ↑i) u * (bernstein n ↑j) u = ↑(m.choose ↑i) * ↑(n.choose ↑j) / ((↑m + ↑n + 1) * ↑((m + n).choose (↑i + ↑j)))

Exact Gram matrix entry for Bernstein bases of arbitrary degrees.

source
theorem Verification.integral_bernstein_product_nat (m n i j : ℕ) :
∫ (u : ↑unitInterval), (bernstein m i) u * (bernstein n j) u = ↑(m.choose i) * ↑(n.choose j) / ((↑m + ↑n + 1) * ↑((m + n).choose (i + j)))

The same formula also handles indices outside the basis, where the basis vanishes.