Constant Term Formula

StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.Core

Statement

Definition Constant Term Formula

The constant term of $P_N(x;\theta)$ is $(-1)^N \prod_{k=0}^{N-1} r_k(\theta)$. After scaling by $2^{N-1}$, the constant term of $S_N$ is $$2^{N-1} \cdot (-1)^N \cdot \prod_{k=0}^{N-1} \cos\!\left(\theta + \frac{2\pi k}{N}\right).$$ This product of roots varies with $\theta$, reflecting the fact that Newton's identities only constrain $e_N$ using $p_N$, which may depend on $\theta$ when $j = N$.

def constantTermFormula (N : ) (θ : ) :  :=
  (2 : ) ^ (N - 1) * (-1) ^ N * (realProjectionsList N θ).prod

Neighborhood

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