theorem
Verification.bernsteinDerivative_product_moments
(k i r : ℕ)
(hi : i ≤ k)
(hr : r ≤ k)
:
∫ (u : ↑unitInterval), bernsteinDerivative (k + 2) (i + 1) u * bernsteinDerivative (k + 2) (r + 1) u = ↑((k + 2).choose (i + 1)) * ↑((k + 2).choose (r + 1)) * ((↑i + 1) * (↑r + 1) * betaMoment (i + r) (k - i + (k - r)) - (↑k + 2) * (↑i + ↑r + 2) * betaMoment (i + r + 1) (k - i + (k - r)) + (↑k + 2) ^ 2 * betaMoment (i + r + 2) (k - i + (k - r)))
theorem
Verification.bernstein_upsilon_interior
(k i r : ℕ)
(hi : i ≤ k)
(hr : r ≤ k)
:
∫ (u : ↑unitInterval), bernsteinDerivative (k + 2) (i + 1) u * bernsteinDerivative (k + 2) (r + 1) u = ↑((k + 2).choose (i + 1)) * ↑((k + 2).choose (r + 1)) / ((2 * ↑k + 1) * ↑((2 * k).choose (i + r))) * ((↑i + 1) * (↑r + 1) - 2 * (↑k + 2) * (↑k + 1) * ↑((i + r + 2).choose 2) / ((2 * ↑k + 3) * (2 * ↑k + 2)))
The printed interior case of Upsilon, for every degree k+2 and source indices i+1,r+1.