Power Sum Theta-Independence

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PowerSums

Statement

Theorem Power Sum Theta-Independence
[blueprint]

For $0 < j < N$ and any $\theta_1, \theta_2 \in \mathbb{R}$, $\sum_{k=0}^{N-1} \cos^j\!\bigl(\theta_1 + \frac{2\pi k}{N}\bigr) = \sum_{k=0}^{N-1} \cos^j\!\bigl(\theta_2 + \frac{2\pi k}{N}\bigr).$

theorem sum_cos_pow_theta_independent (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 ▼

Expand both sides via the binomial identity. Each inner cosine sum with $2r - j \ne 0$ vanishes by discrete orthogonality; the surviving term (when $j$ is even, $r = j/2$) contributes $N\binom{j}{j/2}/2^j$, which is $\theta$-independent.


  -- Use binomial expansion to show all non-constant terms vanish
  rw [sum_cos_pow_eq_sum_binomial N j θ₁ hN hj', sum_cos_pow_eq_sum_binomial N j θ₂ hN hj']
  congr 1
  -- The sum over r contains terms that depend on θ via cos((2r-j) * (θ + 2πk/N))
  -- We need to show these sums are equal for θ₁ and θ₂
  apply Finset.sum_congr rfl
  intro r hr
  congr 1
  -- For each r, the inner sum ∑_k cos((2r-j) * (θ + 2πk/N)) is either:
  -- 1. Zero if 2r-j ≠ 0 (by sum_cos_int_multiple_vanishes), or
  -- 2. N if 2r-j = 0 (constant term)
  -- In both cases, it's independent of θ
  by_cases h_zero : (2 * r - j : ℤ) = 0
  · -- When 2r = j, the sum is constant (= N)
    simp only [h_zero]
    norm_num
  · -- When 2r ≠ j, apply sum_cos_int_multiple_vanishes
    have h_abs : |(2 * r - j : ℤ)| < N := by
      -- Need to bound |2r - j| < N given j < N and r ≤ j
      have hr_le : r ∈ Finset.range (j + 1) := hr
      simp only [Finset.mem_range] at hr_le
      -- r < j + 1 means r ≤ j
      have : r ≤ j := Nat.lt_succ_iff.mp hr_le
      -- So 2r ≤ 2j, and |2r - j| ≤ j < N
      by_cases hr_case : 2 * r ≥ j
      · -- 2r ≥ j: |2r - j| = 2r - j ≤ 2j - j = j < N
        rw [abs_of_nonneg (Int.sub_nonneg_of_le (by omega : (j : ℤ) ≤ (2 * r : ℤ)))]
        calc (2 * r - j : ℤ)
          _ ≤ (2 * j - j : ℤ) := by omega
          _ = (j : ℤ) := by ring
          _ < (N : ℤ) := by omega
      · -- 2r < j: |2r - j| = j - 2r ≤ j < N
        push_neg at hr_case
        rw [abs_of_neg (Int.sub_neg_of_lt (by omega : (2 * r : ℤ) < (j : ℤ)))]
        calc -(2 * r - j : ℤ)
          _ = (j - 2 * r : ℤ) := by ring
          _ ≤ (j : ℤ) := by omega
          _ < (N : ℤ) := by omega
    -- Apply sum_cos_int_multiple_vanishes to both sums
    rw [sum_cos_int_multiple_vanishes N (2 * r - j) θ₁ hN h_zero h_abs,
        sum_cos_int_multiple_vanishes N (2 * r - j) θ₂ hN h_zero h_abs]

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