Chebyshev Roots Are Roots of T_N

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.ChebyshevRoots

Statement

Theorem Chebyshev Roots Are Roots of T_N

For $N \geq 1$ and $0 \leq k < N$, $T_N(\cos((2k+1)\pi/(2N))) = 0$. The proof uses the defining identity $T_N(\cos\theta) = \cos(N\theta)$ and shows $N \cdot (2k+1)\pi/(2N) = (2k+1)\pi/2$, at which cosine vanishes.

theorem chebyshev_T_eval_chebyshevRoot (N k : ℕ) (hN : 0 < N) (_hk : k < N) :
    (Polynomial.Chebyshev.T ℝ N).eval (chebyshevRoot N k) = 0 := by

Proof ▼

Apply $T_N(\cos\theta) = \cos(N\theta)$, simplify the argument to $(2k+1)\pi/2$, then use $\cos((2k+1)\pi/2) = 0$ from the characterization of cosine zeros.


  unfold chebyshevRoot
  -- Use T_real_cos: T_n(cos θ) = cos(nθ)
  rw [Polynomial.Chebyshev.T_real_cos]
  -- Need to show: cos(N * ((2k+1)π/(2N))) = 0
  -- Simplify the argument using field_simp and show it equals (2k+1)π/2
  suffices Real.cos ((2 * k + 1) * π / 2) = 0 by
    convert this using 2
    push_cast
    field_simp [show (N : ℝ) ≠ 0 by positivity]
  -- Now we need: cos((2k+1)π/2) = 0
  -- Use Real.cos_eq_zero_iff: cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1) * π / 2
  rw [Real.cos_eq_zero_iff]
  use k
  push_cast
  rfl

Dependencies (uses)

Chebyshev Root

Dependents (used by)

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