Explicit Constant c(N, θ)
StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.Core
Statement
The constant $c(N,\theta)$ is given explicitly by $$c(N,\theta) = 2^{N-1} \cdot (-1)^N \cdot \prod_{k=0}^{N-1} \cos\!\left(\theta + \frac{2\pi k}{N}\right) - T_N(0).$$ This is the only $\theta$-dependent part of the relationship $S_N(x;\theta) = T_N(x) + c(N,\theta)$.
def explicitConstant (N : ℕ) (θ : ℝ) : ℝ :=
constantTermFormula N θ - chebyshevConstantTerm N
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