# mathlibdocumentation

ring_theory.polynomial.chebyshev.defs

# Chebyshev polynomials

The Chebyshev polynomials are two families of polynomials indexed by ℕ, with integral coefficients. In this file, we only consider Chebyshev polynomials of the first kind.

See the file ring_theory.polynomial.chebyshev.basic for more properties.

## Main declarations

• polynomial.chebyshev₁: the Chebyshev polynomials of the first kind.
• polynomial.lambdashev: a variant on the Chebyshev polynomials that define a Lambda structure on polynomial ℤ.

## Implementation details

In this file we only give definitions and some very elementary simp-lemmas. This way, we can import this file in analysis.special_functions.trigonometric, and import that file in turn, in ring_theory.polynomial.chebyshev.basic.

## TODO

Add Chebyshev polynomials of the second kind.

def polynomial.chebyshev₁ (R : Type u_1) [comm_ring R] :

chebyshev₁ n is the n-th Chebyshev polynomial of the first kind

Equations
@[simp]
theorem polynomial.chebyshev₁_zero (R : Type u_1) [comm_ring R] :

@[simp]
theorem polynomial.chebyshev₁_one (R : Type u_1) [comm_ring R] :

theorem polynomial.chebyshev₁_two (R : Type u_1) [comm_ring R] :
= 2 * - 1

@[simp]
theorem polynomial.chebyshev₁_add_two (R : Type u_1) [comm_ring R] (n : ) :
(n + 2) = * (n + 1) -

theorem polynomial.chebyshev₁_of_two_le (R : Type u_1) [comm_ring R] (n : ) (h : 2 n) :
= * (n - 1) - (n - 2)

theorem polynomial.map_chebyshev₁ {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (n : ) :

def polynomial.lambdashev (R : Type u_1) [comm_ring R] :

lambdashev R n is equal to 2 * (chebyshev₁ R n).comp (X / 2). It is a family of polynomials that satisfies lambdashev (zmod p) p = X ^ p, and therefore defines a Lambda structure on polynomial ℤ.

Equations
• (n + 2) =
@[simp]
theorem polynomial.lambdashev_zero (R : Type u_1) [comm_ring R] :

@[simp]
theorem polynomial.lambdashev_one (R : Type u_1) [comm_ring R] :

theorem polynomial.lambdashev_two (R : Type u_1) [comm_ring R] :
= - 2

@[simp]
theorem polynomial.lambdashev_add_two (R : Type u_1) [comm_ring R] (n : ) :
(n + 2) = polynomial.X * (n + 1) -

theorem polynomial.lambdashev_eq_two_le (R : Type u_1) [comm_ring R] (n : ) (h : 2 n) :
= polynomial.X * (n - 1) - (n - 2)

theorem polynomial.map_lambdashev {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (n : ) :