English
For all n and ν, the ν-th iterate of the derivative of Bernstein(n, ν) evaluated at 0 equals ascPochhammer(ν) evaluated at n − (ν − 1).
Русский
Для всех n и ν, ν-я итерация производной Bernstein(n, ν) в точке 0 равна ascPochhammer(ν) в точке n − (ν − 1).
LaTeX
$$$(\mathrm{derivative}^{\nu}(\bernsteinPolynomial R n \nu))(0) = (\ascPochhammer R \nu)(n - (\nu - 1))$$$
Lean4
@[simp]
theorem iterate_derivative_at_0 (n ν : ℕ) :
(Polynomial.derivative^[ν] (bernsteinPolynomial R n ν)).eval 0 = (ascPochhammer R ν).eval ((n - (ν - 1) : ℕ) : R) :=
by
by_cases h : ν ≤ n
·
induction ν generalizing n with
| zero => simp [eval_at_0]
| succ ν ih =>
have h' : ν ≤ n - 1 := le_tsub_of_add_le_right h
simp only [derivative_succ, ih (n - 1) h', iterate_derivative_succ_at_0_eq_zero, Nat.succ_sub_succ_eq_sub,
tsub_zero, sub_zero, iterate_derivative_sub, iterate_derivative_natCast_mul, eval_one, eval_mul, eval_add,
eval_sub, eval_X, eval_comp, eval_natCast, Function.comp_apply, Function.iterate_succ, ascPochhammer_succ_left]
obtain rfl | h'' := ν.eq_zero_or_pos
· simp
· have : n - 1 - (ν - 1) = n - ν := by omega
rw [this, ascPochhammer_eval_succ]
rw_mod_cast [tsub_add_cancel_of_le (h'.trans n.pred_le)]
· simp only [not_le] at h
rw [tsub_eq_zero_iff_le.mpr (Nat.le_sub_one_of_lt h), eq_zero_of_lt R h]
simp [pos_iff_ne_zero.mp (pos_of_gt h)]
