English
Let R be a commutative ring of characteristic zero. For all natural numbers n and ν with ν ≤ n, the ν-th derivative of the Bernstein polynomial bernsteinPolynomial R n ν, evaluated at 0, is nonzero.
Русский
Пусть R — коммутативное кольцо характеристикой ноль. Для всех n, ν ∈ ℕ с ν ≤ n, ν-ая производная Bernstein-полиномa bernsteinPolynomial R n ν, вычисленная в 0, не равна нулю.
LaTeX
$$$ (Polynomial.derivative^{\nu} (bernsteinPolynomial R n ν)).eval 0 \neq 0 $$$
Lean4
theorem iterate_derivative_at_0_ne_zero [CharZero R] (n ν : ℕ) (h : ν ≤ n) :
(Polynomial.derivative^[ν] (bernsteinPolynomial R n ν)).eval 0 ≠ 0 :=
by
simp only [bernsteinPolynomial.iterate_derivative_at_0, Ne]
simp only [← ascPochhammer_eval_cast]
norm_cast
apply ne_of_gt
obtain rfl | h' := Nat.eq_zero_or_pos ν
· simp
· rw [← Nat.succ_pred_eq_of_pos h'] at h
exact ascPochhammer_pos _ _ (tsub_pos_of_lt (Nat.lt_of_succ_le h))
