English
The derivative of Bernstein(n+1)(ν+1) equals (n+1) times the difference Bernstein(n, ν) and Bernstein(n, ν+1).
Русский
Производная Bernstein(n+1)(ν+1) равна (n+1) умножить на разность Bernstein(n, ν) и Bernstein(n, ν+1).
LaTeX
$$$\mathrm{derivative}(\bernsteinPolynomial R (n+1) (\nu+1)) = (n+1) \cdot (\bernsteinPolynomial R n \nu - \bernsteinPolynomial R n (\nu+1))$$$
Lean4
theorem derivative_succ_aux (n ν : ℕ) :
Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) =
(n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1)) :=
by
rw [bernsteinPolynomial]
suffices
((n + 1).choose (ν + 1) : R[X]) * ((↑(ν + 1 : ℕ) : R[X]) * X ^ ν) * (1 - X) ^ (n - ν) -
((n + 1).choose (ν + 1) : R[X]) * X ^ (ν + 1) * ((↑(n - ν) : R[X]) * (1 - X) ^ (n - ν - 1)) =
(↑(n + 1) : R[X]) *
((n.choose ν : R[X]) * X ^ ν * (1 - X) ^ (n - ν) -
(n.choose (ν + 1) : R[X]) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
by
simpa [Polynomial.derivative_pow, ← sub_eq_add_neg, Nat.succ_sub_succ_eq_sub, Polynomial.derivative_mul,
Polynomial.derivative_natCast, zero_mul, Nat.cast_add, algebraMap.coe_one, Polynomial.derivative_X, mul_one,
zero_add, Polynomial.derivative_sub, Polynomial.derivative_one, zero_sub, mul_neg, Nat.sub_zero,
bernsteinPolynomial, map_add, map_natCast, Nat.cast_one]
conv_rhs =>
rw [mul_sub]
-- We'll prove the two terms match up separately.
refine congr (congr_arg Sub.sub ?_) ?_
· simp only [← mul_assoc]
apply congr (congr_arg (· * ·) (congr (congr_arg (· * ·) _) rfl)) rfl
exact mod_cast congr_arg (fun m : ℕ => (m : R[X])) (Nat.succ_mul_choose_eq n ν).symm
· rw [← tsub_add_eq_tsub_tsub, ← mul_assoc, ← mul_assoc]; congr 1
rw [mul_comm, ← mul_assoc, ← mul_assoc]; congr 1
norm_cast
congr 1
convert (Nat.choose_mul_succ_eq n (ν + 1)).symm using 1
· convert mul_comm _ _ using 2
simp
· apply mul_comm
