← Mathematical handbook

noncomputable def Verification.bernsteinUpsilonMatrix (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

The source's piecewise Upsilon matrix for degree n+1, with source indices i+1,r+1.

Equations

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

theorem Verification.bernsteinUpsilonMatrix_integral (n : ℕ) (i r : Fin (n + 1)) : ∫ (u : ↑unitInterval), bernsteinDerivative (n + 1) (↑i + 1) u * bernsteinDerivative (n + 1) (↑r + 1) u = bernsteinUpsilonMatrix n i r