Full Root Characterization of Chebyshev Polynomials

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.ChebyshevRoots

Statement

This is the definitive root characterization for Chebyshev polynomials. It combines the backward direction (each $\xi_k$ is a root) with the forward direction (every root is some $\xi_k$) into a single biconditional.

Theorem Full Root Characterization of Chebyshev Polynomials

[blueprint]

For $N \geq 1$ and $x \in \mathbb{R}$, $T_N(x) = 0 \iff \exists\, k < N,\; x = \cos\!\left(\frac{(2k+1)\pi}{2N}\right)$.

theorem chebyshev_T_eval_eq_zero_iff (N : ℕ) (hN : 0 < N) (x : ℝ) :
    (Polynomial.Chebyshev.T ℝ N).eval x = 0 ↔ ∃ k < N, x = chebyshevRoot N k := by

Proof ▼

The forward direction uses the degree-counting argument; the backward direction uses the defining identity $T_N(\cos\theta) = \cos(N\theta)$.


  constructor
  · exact chebyshev_T_eval_eq_zero_forward N hN x
  · intro ⟨k, hk, h_eq⟩
    rw [h_eq]
    exact chebyshev_T_eval_chebyshevRoot N k hN hk

This characterization is essential for the main theorem: it identifies the Chebyshev roots whose power sums must match those of the rotated roots of unity.

Dependencies (uses)

Forward Direction: Roots of T_N Are Chebyshev Roots

Dependents (used by)

None

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms