Coefficient Independence Theorem

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.PolynomialProperties

Statement

This theorem is the algebraic heart of the main result. It establishes that rotating the $N$-th roots of unity before projecting onto the real axis does not change the polynomial coefficients of degree $\geq 1$. The proof uses Vieta's formulas and the $\theta$-invariance of elementary symmetric polynomials.

Theorem 5.1.1

[blueprint]

For any $N \geq 1$ and any $k \geq 1$, the coefficient $[x^k] S_N(x;\theta_1) = [x^k] S_N(x;\theta_2)$ for all $\theta_1, \theta_2 \in \mathbb{R}$.

theorem constant_term_only_varies (N : ℕ) (θ₁ θ₂ : ℝ) (k : ℕ) (hN : 0 < N)
    (hk : 0 < k) : (scaledPolynomial N θ₁).coeff k = (scaledPolynomial N θ₂).coeff k := by

Proof ▼

Unfold the scaled and unscaled polynomial definitions, convert to multiset form via Vieta's formula, and show the elementary symmetric polynomials are $\theta$-independent for all non-constant coefficients. For $k > N$, both coefficients are zero by degree bounds.


  unfold scaledPolynomial unscaledPolynomial polynomialFromRealRoots
  simp only [coeff_C_mul]
  congr 1
  -- Convert to multiset form
  rw [list_foldr_eq_multiset_prod, list_foldr_eq_multiset_prod]
  -- Factor out the card lemma
  have h_card (θ : ℝ) : ((realProjectionsList N θ : Multiset ℝ)).card = N := by
    rw [Multiset.coe_card, card_realProjectionsList]
  -- Split cases
  by_cases hk_le : k ≤ N
  · -- k ≤ N: use Vieta's formula
    rw [Multiset.prod_X_sub_C_coeff (realProjectionsList N θ₁ : Multiset ℝ) (by rwa [h_card]),
        Multiset.prod_X_sub_C_coeff (realProjectionsList N θ₂ : Multiset ℝ) (by rwa [h_card])]
    congr 1
    · rw [h_card, h_card]
    · by_cases hk_eq : k = N
      · rw [hk_eq, h_card, h_card]; norm_num [Multiset.esymm, Multiset.powersetCard_zero_left]
      · rw [h_card, h_card]
        exact esymm_rotated_roots_invariant N (N - k) θ₁ θ₂ hN (by omega) (by omega)
  · -- k > N: both coefficients are 0
    have deg (θ : ℝ) : (Multiset.map (fun r => X - C r)
        (realProjectionsList N θ : Multiset ℝ)).prod.natDegree = N := by
      rw [Polynomial.natDegree_multiset_prod_X_sub_C_eq_card, h_card]
    rw [Polynomial.coeff_eq_zero_of_natDegree_lt, Polynomial.coeff_eq_zero_of_natDegree_lt]
    · rw [deg]; omega
    · rw [deg]; omega

Combined with the explicit constant term formula, this implies the main theorem: $S_N(x;\theta) = T_N(x) + c(\theta)$ where only $c(\theta)$ depends on the rotation angle.

Dependencies (uses)

Dependents (used by)

Proof of Main Theorem

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms