Chebyshev Constant Term

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.MainTheoremSupport

Statement

Theorem Chebyshev Constant Term
[blueprint]

$[x^0]\, T_N(x) = \texttt{chebyshevConstantTerm}(N)$. This is a definitional equality that exposes the constant term for use in the explicit constant formula.

theorem chebyshev_T_constantTerm (N : ℕ) :
    (Polynomial.Chebyshev.T ℝ N).coeff 0 = chebyshevConstantTerm N :=
Proof ▼ 

 rfl

Dependencies (uses)

Dependents (used by)

Neighborhood

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