Rotated Roots of Unity

StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.Core

Statement

The Chebyshev polynomial construction begins with the $N$-th roots of unity on the complex unit circle. These form a regular $N$-gon inscribed in the unit circle, with vertices equally spaced at angular intervals of $2\pi/N$.
Definition 1.1
[blueprint]

When the $N$-th roots of unity are rotated by an angle $\theta$ (equivalently, multiplied by $e^{i\theta}$), we obtain the $N$ complex numbers $e^{i(\theta + 2\pi k/N)}$ for $k = 0, 1, \ldots, N-1$. The rotation angle $\theta$ controls the orientation of the $N$-gon.

def rotatedRootsOfUnityList (N : ℕ) (θ : ℝ) : List ℂ :=
  List.range N |>.map (fun k => exp (I * (θ + 2 * π * k / N)))
As $\theta$ varies from $0$ to $2\pi$, the rotated roots sweep through all possible configurations of $N$ equally-spaced points on the unit circle. Projecting these onto the real axis yields the inputs to the polynomial construction.

Dependencies (uses)

None

Dependents (used by)

None

Neighborhood

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