← Mathematical handbook

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

Equations

• Verification.bernsteinMixedGram m i r = ↑m * (Verification.bernsteinGram (m - 1) m i (r + 1) - Verification.bernsteinGram (m - 1) m (i + 1) (r + 1))

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