Chebyshev Evaluation at Cosine

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.PolynomialProperties

Statement

Theorem Chebyshev Evaluation at Cosine

For all $N \in \mathbb{N}$ and $\theta \in \mathbb{R}$, $T_N(\cos\theta) = \cos(N\theta)$. This is the fundamental identity characterizing Chebyshev polynomials of the first kind.

theorem chebyshev_eval_cos (N : ℕ) (θ : ℝ) :
    (Polynomial.Chebyshev.T ℝ N).eval (Real.cos θ) = Real.cos (N * θ) := by

Proof ▼


  exact Polynomial.Chebyshev.T_real_cos θ N

Dependencies (uses)

None

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