derivative_succ — Mathlib

English

The derivative of Bernstein(n)(ν+1) equals n times the difference Bernstein(n-1, ν) and Bernstein(n-1, ν+1).

Русский

Производная Bernstein(n)(ν+1) равна n умножить на разность Bernstein(n-1, ν) и Bernstein(n-1, ν+1).

LaTeX

$$$\mathrm{derivative}(\bernsteinPolynomial R n (\nu+1)) = n \big(\bernsteinPolynomial R (n-1) \nu - \bernsteinPolynomial R (n-1) (\nu+1)\big)$$$

Lean4

theorem derivative_succ (n ν : ℕ) :
    Polynomial.derivative (bernsteinPolynomial R n (ν + 1)) =
      n * (bernsteinPolynomial R (n - 1) ν - bernsteinPolynomial R (n - 1) (ν + 1)) :=
  by
  cases n
  · simp [bernsteinPolynomial]
  · rw [Nat.cast_succ]; apply derivative_succ_aux

Похожие утверждения