← Mathematical handbook

theorem Verification.bernsteinDerivative_boundary_moments (k i : ℕ) (hi : i ≤ k) : ∫ (u : ↑unitInterval), bernsteinDerivative (k + 2) (i + 1) u * bernsteinDerivative (k + 2) (k + 2) u = (↑k + 2) * ↑((k + 2).choose (i + 1)) * ((↑i + 1) * betaMoment (k + i + 1) (k - i) - (↑k + 2) * betaMoment (k + i + 2) (k - i))

theorem Verification.bernstein_upsilon_boundary (k i : ℕ) (hi : i ≤ k) : ∫ (u : ↑unitInterval), bernsteinDerivative (k + 2) (i + 1) u * bernsteinDerivative (k + 2) (k + 2) u = (↑k + 2) * (↑k + 1) * (↑i - ↑k - 1) * ↑((k + 2).choose (i + 1)) / ((2 * ↑k + 3) * (2 * ↑k + 2) * ↑((2 * k + 1).choose (k + i + 1)))

The printed last-column case of Upsilon, away from the last diagonal entry.

theorem Verification.bernstein_upsilon_corner (k : ℕ) : ∫ (u : ↑unitInterval), bernsteinDerivative (k + 1) (k + 1) u * bernsteinDerivative (k + 1) (k + 1) u = (↑k + 1) ^ 2 / (2 * ↑k + 1)

The printed last diagonal entry, also valid for degree one.