Chebyshev Constant Term
StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.Core
Statement
The value $T_N(0)$, i.e.\ the coefficient of $x^0$ in $T_N(x)$. This is subtracted from the scaled polynomial's constant term to obtain the explicit constant $c(N,\theta)$.
def chebyshevConstantTerm (N : ℕ) : ℝ :=
(Polynomial.Chebyshev.T ℝ N).coeff 0
Dependencies (uses)
NoneDependents (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