Constant Term Formula
StatusFully Proven
TypeDefinition
ModuleChebyshevCircles.Definitions.Core
Statement
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
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