Chebyshev Root

StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.ChebyshevRoots

Statement

Definition Chebyshev Root

The roots of the Chebyshev polynomial $T_N(x)$ are $$\xi_k = \cos\!\left(\frac{(2k+1)\pi}{2N}\right), \quad k = 0, 1, \ldots, N-1.$$ These are $N$ distinct real numbers in the interval $(-1, 1)$. They satisfy $T_N(\xi_k) = 0$ by the defining relation $T_N(\cos\theta) = \cos(N\theta)$.

def chebyshevRoot (N k : ) :  := Real.cos ((2 * k + 1 : ) * π / (2 * N))

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms