Polynomial.Chebyshev.mul_T
theorem Polynomial.Chebyshev.mul_T :
∀ (R : Type u_1) [inst : CommRing R] (m k : ℕ),
2 * Polynomial.Chebyshev.T R m * Polynomial.Chebyshev.T R (m + k) =
Polynomial.Chebyshev.T R (2 * m + k) + Polynomial.Chebyshev.T R k
The theorem `Polynomial.Chebyshev.mul_T` states that for any commutative ring `R` and any natural numbers `m` and `k`, the product of the `m`-th and the `(m + k)`-th Chebyshev polynomials of the first kind (multiplied by 2) is equal to the sum of the `(2*m + k)`-th and the `k`-th Chebyshev polynomials of the first kind. In other words, this theorem is a specific relationship between different Chebyshev polynomials of the first kind.
More concisely: For any commutative ring R and natural numbers m and k, the product of the m-th and (m + k)-th Chebyshev polynomials of the first kind, multiplied by 2, equals the (2m + k)-th Chebyshev polynomial of the first kind plus the k-th Chebyshev polynomial of the first kind.
|
Polynomial.Chebyshev.T_add_two
theorem Polynomial.Chebyshev.T_add_two :
∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
Polynomial.Chebyshev.T R (n + 2) =
2 * Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - Polynomial.Chebyshev.T R n
The theorem `Polynomial.Chebyshev.T_add_two` states that for any commutative ring `R` and any natural number `n`, the `(n + 2)`-th Chebyshev polynomial of the first kind can be calculated from the `(n + 1)`-th and `n`-th Chebyshev polynomials. More precisely, it is twice the polynomial variable times the `(n + 1)`-th Chebyshev polynomial minus the `n`-th Chebyshev polynomial. This is a recursive definition of Chebyshev polynomials, a sequence of orthogonal polynomials which often arise in numerical analysis and approximation theory.
More concisely: For any commutative ring R and natural number n, the (n + 2)-th Chebyshev polynomial of the first kind is given recursively as T_(n+2)(x) = 2x*T_(n+1)(x) - T\_n(x).
|
Polynomial.Chebyshev.T_mul
theorem Polynomial.Chebyshev.T_mul :
∀ (R : Type u_1) [inst : CommRing R] (m n : ℕ),
Polynomial.Chebyshev.T R (m * n) = (Polynomial.Chebyshev.T R m).comp (Polynomial.Chebyshev.T R n)
The theorem `Polynomial.Chebyshev.T_mul` states that for any commutative ring `R` and for any natural numbers `m` and `n`, the `(m * n)`-th Chebyshev polynomial of the first kind is equal to the composition of the `m`-th and `n`-th Chebyshev polynomials of the first kind. In mathematical terms, we have `T_{m*n}(x) = T_m(T_n(x))`, where `T_n(x)` denotes the `n`-th Chebyshev polynomial of the first kind.
More concisely: The `(m * n)`-th Chebyshev polynomial of the first kind equals the composition of the `m`-th and `n`-th Chebyshev polynomials of the first kind: `T_{m*n}(x) = T_m(T_n(x))`.
|