one_sub_X_sq_mul_derivative_T_eq_poly_in_T

English

A relation between derivative of T and U involving 1 - X^2

Русский

Связь производной T с U через 1 - X^2

LaTeX

$$$ (1 - X^2) \cdot derivative(T_R(n+1)) = (n+1) \cdot (T_R(n) - X\, T_R(n+1)) $$$

Lean4

theorem one_sub_X_sq_mul_derivative_T_eq_poly_in_T (n : ℤ) :
    (1 - X ^ 2) * derivative (T R (n + 1)) = (n + 1 : R[X]) * (T R n - X * T R (n + 1)) :=
  by
  have H₁ := one_sub_X_sq_mul_U_eq_pol_in_T R n
  have H₂ := T_derivative_eq_U (R := R) (n + 1)
  have h₁ := T_add_two R n
  linear_combination (norm := (push_cast; ring_nf)) (-n - 1) * h₁ + (-(X : R[X]) ^ 2 + 1) * H₂ + (n + 1) * H₁

Похожие утверждения