English
For every integer n, derivative(T_R n) = n * U_R (n-1).
Русский
Для каждого целого n производная T_R(n) равна n · U_R(n-1).
LaTeX
$$$ derivative\ (T_R\ n) = n \cdot U_R(n-1) $$$
Lean4
theorem T_derivative_eq_U (n : ℤ) : derivative (T R n) = n * U R (n - 1) := by
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
have h₁ := congr_arg derivative (T_add_two R n)
have h₂ := U_sub_one R n
have h₃ := T_eq_U_sub_X_mul_U R (n + 1)
simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁
linear_combination (norm := (push_cast; ring_nf)) h₁ - ih2 + 2 * (X : R[X]) * ih1 + 2 * h₃ - n * h₂
| neg_add_one n ih1 ih2 =>
have h₁ := congr_arg derivative (T_sub_one R (-n))
have h₂ := U_sub_two R (-n)
have h₃ := T_eq_U_sub_X_mul_U R (-n)
simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁
linear_combination (norm := (push_cast; ring_nf)) -ih2 + 2 * (X : R[X]) * ih1 + h₁ + 2 * h₃ + (n + 1) * h₂
