Real Projections List
StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.Core
Statement
The rotated roots of unity live on the complex unit circle. Projecting them
onto the real axis extracts the cosine of each angle, yielding a multiset of real
values in $[-1, 1]$ that serve as roots for the polynomial construction.
The real projections of the rotated $N$-th roots of unity are the $N$ real numbers $$r_k(\theta) = \cos\!\left(\theta + \frac{2\pi k}{N}\right), \quad k = 0, 1, \ldots, N-1.$$
def realProjectionsList (N : ℕ) (θ : ℝ) : List ℝ :=
(List.range N).map (fun (k : ℕ) => Real.cos (θ + 2 * π * k / N))
These projected roots are the inputs to the monic polynomial construction
$P_N(x;\theta) = \prod_{k=0}^{N-1}(x - r_k(\theta))$, which after scaling yields
the Chebyshev polynomial plus a constant.
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