English
Let R be a commutative ring with CharZero. For all n, ν ∈ ℕ with ν ≤ n, the value of the (n−ν)-th derivative of Bernstein polynomial B_{n,ν} at x=1 equals (-1)^{n−ν} times ascPochhammer evaluated at (n−ν) and ν+1.
Русский
Пусть R — коммутативное кольцо характеристики ноль. Для всех n, ν ∈ ℕ с ν ≤ n, значение (n−ν)-й производной Bernstein-полиномa B_{n,ν} в x=1 равно (-1)^{n−ν} умножить на ascPochhammer_R(n−ν) в точке (ν+1).
LaTeX
$$$ (Polynomial.derivative^{n-\nu} (bernsteinPolynomial R n ν)).eval 1 = (-1)^{(n-\nu)} \cdot (ascPochhammer R (n-\nu)).eval (\nu + 1 : R) $$$
Lean4
@[simp]
theorem iterate_derivative_at_1 (n ν : ℕ) (h : ν ≤ n) :
(Polynomial.derivative^[n - ν] (bernsteinPolynomial R n ν)).eval 1 =
(-1) ^ (n - ν) * (ascPochhammer R (n - ν)).eval (ν + 1 : R) :=
by
rw [flip' _ _ _ h]
simp only [iterate_derivative_comp_one_sub_X, eval_mul, eval_pow, eval_neg, eval_one, eval_comp, eval_sub, eval_X,
sub_self, iterate_derivative_at_0]
obtain rfl | h' := h.eq_or_lt
· simp
· norm_cast
congr
cutsat
