add_one_mul_T_eq_poly_in_U — Mathlib

English

A relation expressing (n+1) factor of T in terms of U and derivative of U.

Русский

Связь, выражающая (n+1) фактор T через U и производную U.

LaTeX

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

Lean4

theorem add_one_mul_T_eq_poly_in_U (n : ℤ) :
    ((n : R[X]) + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * derivative (U R n) :=
  by
  have h₁ := congr_arg derivative <| T_eq_X_mul_T_sub_pol_U R n
  simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow, T_derivative_eq_U,
    C_eq_natCast] at h₁
  have h₂ := T_eq_U_sub_X_mul_U R (n + 1)
  linear_combination (norm := (push_cast; ring_nf)) h₁ + (n + 2) * h₂

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