Chapter 5: From Power Sums to Polynomial Coefficients

Having established that the power sums are \(\theta\)-independent, we now apply Newton's identities to deduce that the polynomial coefficients (except the constant term) are also \(\theta\)-independent.

Newton's identities: the algebraic bridge

Recall that for roots \(\alpha_1, \ldots, \alpha_N\), Newton's identities recursively determine the elementary symmetric polynomials \(e_k\) from the power sums \(p_j = \sum \alpha_i^j\):

\begin{equation}...\end{equation}

Since this is a recursive formula starting from \(e_0 = 1\), if the power sums \(p_1, \ldots, p_N\) are independent of \(\theta\), then so are all elementary symmetric polynomials \(e_1, \ldots, e_N\). By Vieta's formulas, these determine the polynomial coefficients (the coefficient of \(x^{N-k}\) is \((-1)^k e_k\) in the monic polynomial).

Lemma

Let \(r_k(\theta) = \cos(\theta + 2\pi k/N)\) for \(k = 0, \ldots, N-1\). Then for any \(m\) with \(1 \leq m \leq N\), the elementary symmetric polynomial

\begin{equation}...\end{equation}

is independent of \(\theta\).

Proof.

By Theorem~lem:power_sum_invariance, the power sums \(p_j = \sum_{k=0}^{N-1} r_k(\theta)^j\) are independent of \(\theta\) for \(1 \leq j < N\). For \(j = N\), the power sum may depend on \(\theta\), but Newton's identities for \(e_m\) with \(m \leq N\) only involve \(p_1, \ldots, p_m \leq p_N\). Since \(m \leq N\), we use \(p_j\) for \(j < N\), which are all invariant. Thus by induction on \(m\), each \(e_m\) is independent of \(\theta\). esymm_eq_of_psum_eq

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.

Why the constant term varies

The constant term of \(P_N(x; \theta)\) is \((-1)^N e_N = (-1)^N \prod_{k=0}^{N-1} r_k(\theta)\). While the product of roots can vary with \(\theta\), Newton's identities only constrain \(e_N\) using \(p_1, \ldots, p_N\). Since \(p_N\) (the sum of \(N\)-th powers) may depend on \(\theta\) when \(j = N \geq N\), there is no contradiction. Indeed, explicit calculation shows the constant term does vary. scaledPolynomial_constantTerm_varies

5.1 Newton's identities: the algebraic bridge

Recall that for roots \(\alpha_1, \ldots, \alpha_N\), Newton's identities recursively determine the elementary symmetric polynomials \(e_k\) from the power sums \(p_j = \sum \alpha_i^j\):

\begin{equation}...\end{equation}

Since this is a recursive formula starting from \(e_0 = 1\), if the power sums \(p_1, \ldots, p_N\) are independent of \(\theta\), then so are all elementary symmetric polynomials \(e_1, \ldots, e_N\). By Vieta's formulas, these determine the polynomial coefficients (the coefficient of \(x^{N-k}\) is \((-1)^k e_k\) in the monic polynomial).

Lemma

Let \(r_k(\theta) = \cos(\theta + 2\pi k/N)\) for \(k = 0, \ldots, N-1\). Then for any \(m\) with \(1 \leq m \leq N\), the elementary symmetric polynomial

\begin{equation}...\end{equation}

is independent of \(\theta\).

Proof.

By Theorem~lem:power_sum_invariance, the power sums \(p_j = \sum_{k=0}^{N-1} r_k(\theta)^j\) are independent of \(\theta\) for \(1 \leq j < N\). For \(j = N\), the power sum may depend on \(\theta\), but Newton's identities for \(e_m\) with \(m \leq N\) only involve \(p_1, \ldots, p_m \leq p_N\). Since \(m \leq N\), we use \(p_j\) for \(j < N\), which are all invariant. Thus by induction on \(m\), each \(e_m\) is independent of \(\theta\). esymm_eq_of_psum_eq

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.

5.2 Why the constant term varies

The constant term of \(P_N(x; \theta)\) is \((-1)^N e_N = (-1)^N \prod_{k=0}^{N-1} r_k(\theta)\). While the product of roots can vary with \(\theta\), Newton's identities only constrain \(e_N\) using \(p_1, \ldots, p_N\). Since \(p_N\) (the sum of \(N\)-th powers) may depend on \(\theta\) when \(j = N \geq N\), there is no contradiction. Indeed, explicit calculation shows the constant term does vary. scaledPolynomial_constantTerm_varies