Power Sum Invariance

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.PowerSums

Statement

We now prove that the power sums of the rotated projections $r_k(\theta) = \cos(\theta + 2\pi k/N)$ are independent of $\theta$. This remarkable invariance is the heart of our main theorem: it shows that rotating the configuration does not change the polynomial (except for the constant term).

Theorem 4.3.1

[blueprint]

For any integers $N \ge 1$, $j$ with $1 \le j < N$, and any $\theta \in \mathbb{R}$, $\sum_{k=0}^{N-1} \cos^j\!\bigl(\theta + \frac{2\pi k}{N}\bigr)$ is independent of $\theta$.

theorem powerSumCos_invariant (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 / N)) ^ j := by

Proof ▼

For $j = 1$ this is the vanishing cosine sum. For $j \ge 2$, apply the binomial expansion strategy: expand $\cos^j$ via Euler's formula, sum over the roots of unity, and observe that discrete orthogonality kills every $\theta$-dependent term.


  match j with
  | 0 => omega  -- Contradicts hj
  | 1 =>
    -- j = 1: sum of cosines at N equally spaced angles = 0
    simp only [pow_one]
    have hN2 : 2 ≤ N := by omega
    rw [sum_cos_roots_of_unity N θ₁ hN2, sum_cos_roots_of_unity N θ₂ hN2]
  | j' + 2 =>
    -- j ≥ 2: use the general binomial expansion theorem
    exact sum_cos_pow_theta_independent N (j' + 2) θ₁ θ₂ hN (by omega) hj'

The formalization establishes this for small values of $j$ explicitly ($j = 2, 3, 4, 5, 6$) and then proves the general case using the binomial argument above.

Dependencies (uses)

Dependents (used by)

Elementary Symmetric Functions of Rotated Roots Are Invariant

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