Coefficient Matching at theta = 0

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.MainTheoremSupport

Statement

This result establishes the concrete coefficient matching at the reference angle $\theta = 0$. Combined with the coefficient independence theorem, it implies that $S_N(x;\theta)$ and $T_N(x)$ agree in all non-constant coefficients for every $\theta$.
Theorem Coefficient Matching at theta = 0
[blueprint]

For $N \geq 1$ and $k \geq 1$, $[x^k]\, S_N(x; 0) = [x^k]\, T_N(x)$. The proof proceeds by case analysis: $N = 1, 2, 3$ are verified by explicit computation, and $N \geq 4$ uses the power sum equality and Newton's identities to match elementary symmetric polynomials.

theorem scaledPolynomial_matches_chebyshev_at_zero (N : ℕ) (k : ℕ) (hN : 0 < N) (hk : 0 < k) :
    (scaledPolynomial N 0).coeff k = (Polynomial.Chebyshev.T ℝ N).coeff k := by
Proof ▼

Case split on $N$: small cases ($N = 1, 2, 3$) by direct computation of polynomial coefficients; general case ($N \geq 4$) by constructing both root multisets, verifying power sum equality via $\texttt{general\_powersum\_equality}$, lifting to elementary symmetric polynomial equality via Newton's identities, and concluding coefficient equality via Vieta.


  match N with
  | 1 => exact scaledPolynomial_matches_chebyshev_N_eq_1 k hk
  | 2 => exact scaledPolynomial_matches_chebyshev_N_eq_2 k hk
  | 3 => exact scaledPolynomial_matches_chebyshev_N_eq_3 k hk
  | n + 4 => exact scaledPolynomial_matches_chebyshev_N_ge_4 (n + 4) k (by omega) hk
This is the technical core of the main theorem proof. The constant term is handled separately by the explicit constant term formula.

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