Chebyshev Roots List

StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.ChebyshevRoots

Statement

Definition Chebyshev Roots List

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