Chebyshev Root
StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.ChebyshevRoots
Statement
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))
Dependencies (uses)
NoneNeighborhood
Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms