English
If k < ν, then the k-th iterate of the derivative applied to Bernstein(n, ν) evaluated at 0 is 0.
Русский
Если k < ν, то k-й итерационный применив производную к Bernstein(n, ν) в точке 0 равен 0.
LaTeX
$$$k < \nu \Rightarrow (\mathrm{derivative}^k (\bernsteinPolynomial R n \nu)).eval 0 = 0$$$
Lean4
theorem iterate_derivative_at_0_eq_zero_of_lt (n : ℕ) {ν k : ℕ} :
k < ν → (Polynomial.derivative^[k] (bernsteinPolynomial R n ν)).eval 0 = 0 :=
by
rcases ν with - | ν
· rintro ⟨⟩
· rw [Nat.lt_succ_iff]
induction k generalizing n ν with
| zero => simp [eval_at_0]
| succ k
ih =>
simp only [derivative_succ, Function.comp_apply, Function.iterate_succ, Polynomial.iterate_derivative_sub,
Polynomial.iterate_derivative_natCast_mul, Polynomial.eval_mul, Polynomial.eval_natCast, Polynomial.eval_sub]
intro h
apply mul_eq_zero_of_right
rw [ih _ _ (Nat.le_of_succ_le h), sub_zero]
convert ih _ _ (Nat.pred_le_pred h)
exact (Nat.succ_pred_eq_of_pos (k.succ_pos.trans_le h)).symm
