Explicit Constant c(N, θ)

StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.Core

Statement

Definition Explicit Constant c(N, θ)

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

Neighborhood

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