Power Sum Equality

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PowerSumEquality

Statement

This theorem is the key algebraic identity connecting the two root systems. Both power sums reduce to the same closed-form expression via independent binomial expansion arguments, one using primitive root orthogonality and the other using Chebyshev angle orthogonality. The matching power sums, combined with Newton's identities, force the polynomial coefficients to agree.
Theorem 6.2.2
[blueprint]

For $1 \leq j < N$, $\sum_{k=0}^{N-1} \cos^j\!\left(\theta + \frac{2\pi k}{N}\right) = \sum_{k=0}^{N-1} \cos^j\!\left(\frac{(2k+1)\pi}{2N}\right)$.

theorem general_powersum_equality (N j : ℕ) (hN : 0 < N) (hj : 0 < j) (hj' : j < N) :
    ∑ k ∈ Finset.range N, (Real.cos (2 * π * k / N)) ^ j =
    ∑ k ∈ Finset.range N, (Real.cos ((2 * k + 1 : ℝ) * π / (2 * N))) ^ j := by
Proof ▼

Both sums are evaluated in closed form by the rotated roots and Chebyshev roots power sum value lemmas. The closed forms are identical, establishing equality.


  -- Both sums equal the same closed-form expression
  rw [rotated_roots_powersum_value N j hN hj hj']
  rw [chebyshev_roots_powersum_value N j hN hj hj']
By Newton's identities, matching power sums for $1 \leq j < N$ imply matching elementary symmetric polynomials, and hence matching polynomial coefficients for degrees $1$ through $N$. This is how the main theorem follows.

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