Chebyshev Roots List
StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.ChebyshevRoots
Statement
The complete list of Chebyshev roots $[\xi_0, \xi_1, \ldots, \xi_{N-1}]$ where $\xi_k = \cos\!\left(\frac{(2k+1)\pi}{2N}\right)$. These roots are used to compute the power sums that must equal those of the rotated root projections.
def chebyshevRootsList (N : ℕ) : List ℝ :=
List.ofFn (fun k : Fin N => chebyshevRoot N k)
Dependencies (uses)
Dependents (used by)
Neighborhood
Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms