Rotated Roots Power Sum Value

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PowerSumEquality

Statement

Theorem Rotated Roots Power Sum Value
[blueprint]

For $1 \leq j < N$, $\sum_{k=0}^{N-1} \cos^j(2\pi k/N) = \begin{cases} N \cdot 2^{-j} \binom{j}{j/2} & j \text{ even} \\ 0 & j \text{ odd} \end{cases}$. The proof applies the binomial expansion and uses primitive root orthogonality to show that all non-constant frequency terms vanish, leaving only the middle binomial coefficient when $j$ is even.

theorem rotated_roots_powersum_value (N j : ℕ) (hN : 0 < N) (hj : 0 < j) (hj' : j < N) :
    ∑ k ∈ Finset.range N, (Real.cos (2 * π * k / N)) ^ j =
    if Even j then N * (2 : ℝ) ^ (-(j : ℤ)) * (j.choose (j / 2)) else 0 := by
Proof ▼

Expand via the binomial formula from PowerSums.lean with $\theta = 0$. For each term, the inner sum $\sum \cos((2r-j) \cdot 2\pi k/N)$ vanishes unless $2r - j = 0$ (by discrete orthogonality). When $j$ is odd no such $r$ exists; when $j$ is even only $r = j/2$ contributes.


  -- Apply binomial expansion from PowerSums.lean with θ=0
  have h_expand := sum_cos_pow_eq_sum_binomial N j 0 hN hj'
  simp only [zero_add] at h_expand
  rw [h_expand]

  -- All non-constant terms vanish, only r = j/2 survives when j is even
  by_cases h_even : Even j
  · -- j is even: only the middle term (r = j/2) contributes
    rw [if_pos h_even]
    -- When 2r - j = 0 (i.e., r = j/2), the sum is N (constant term)
    -- All other terms vanish by sum_cos_int_multiple_vanishes
    have sum_eq : ∑ r ∈ Finset.range (j + 1), (j.choose r : ℝ) *
        ∑ k ∈ Finset.range N, Real.cos (((2 * r - j) : ℤ) * (2 * π * k / N)) =
      (j.choose (j / 2) : ℝ) * N := by
      -- Only the term where 2*r - j = 0 contributes
      -- For even j, this happens when r = j/2
      obtain ⟨m, hm⟩ := h_even
      have hj_2_dvd : 2 ∣ j := by
        use m
        rw [hm]
        ring
      have hj_div : j / 2 = m := by omega

      -- Show the sum equals the single term at r = j/2
      have : ∑ r ∈ Finset.range (j + 1), (j.choose r : ℝ) *
          ∑ k ∈ Finset.range N, Real.cos (((2 * r - j) : ℤ) * (2 * π * k / N)) =
        ∑ r ∈ Finset.range (j + 1),
          if r = j / 2 then (j.choose r : ℝ) * N else 0 := by
        apply Finset.sum_congr rfl
        intro r hr
        by_cases h_mid : r = j / 2
        · -- r = j/2: the coefficient (2r - j) = 0, so cos(0) = 1 and sum = N
          rw [if_pos h_mid, h_mid]
          have h_zero : (2 * (j / 2) - j : ℤ) = 0 := by
            -- We have j = m + m, and j / 2 = m
            have h1 : (j / 2 : ℤ) = (m : ℤ) := by exact_mod_cast hj_div
            have h2 : (j : ℤ) = (m : ℤ) + (m : ℤ) := by omega
            rw [h1, h2]; ring
          simp [h_zero]
        · -- r ≠ j/2: the coefficient is non-zero, sum vanishes
          rw [if_neg h_mid]
          have h_neq : (2 * r - j : ℤ) ≠ 0 := by
            intro h_eq
            have h_eq_nat : 2 * r = j := by omega
            have : r = j / 2 := by
              have : j = 2 * r := by omega
              rw [this, Nat.mul_div_cancel_left r (by omega : 0 < 2)]
            contradiction
          -- Need to show |2*r - j| < N
          have h_bound : |(2 * r - j : ℤ)| < N := by
            have hr_le : r ≤ j := by
              simp only [Finset.mem_range] at hr
              omega
            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 the vanishing lemma
          have h_vanish := sum_cos_int_multiple_vanishes N (2 * r - j) 0 hN h_neq h_bound
          simp only [zero_add] at h_vanish
          rw [h_vanish]
          ring
      rw [this]
      simp [Finset.sum_ite_eq', Finset.mem_range]
      omega
    rw [sum_eq]
    ring
  · -- j is odd: all terms vanish (2r - j is never 0 for integer r when j is odd)
    rw [if_neg h_even]
    have sum_zero : ∑ r ∈ Finset.range (j + 1), (j.choose r : ℝ) *
        ∑ k ∈ Finset.range N, Real.cos (((2 * r - j) : ℤ) * (2 * π * k / N)) = 0 := by
      -- All terms vanish: (2r - j) is never 0 when j is odd
      apply Finset.sum_eq_zero
      intro r hr
      -- Show (2*r - j) ≠ 0
      have h_neq : (2 * r - j : ℤ) ≠ 0 := by
        intro h_eq
        have h_eq_nat : 2 * r = j := by omega
        -- This contradicts j being odd (2*r is even)
        have : Even j := ⟨r, by omega⟩
        contradiction
      -- Show |2*r - j| < N
      have h_bound : |(2 * r - j : ℤ)| < N := by
        have hr_le : r ≤ j := by
          simp only [Finset.mem_range] at hr
          omega
        by_cases hr_case : 2 * r ≥ j
        · 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
        · 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 vanishing lemma
      have h_vanish := sum_cos_int_multiple_vanishes N (2 * r - j) 0 hN h_neq h_bound
      simp only [zero_add] at h_vanish
      rw [h_vanish]
      ring
    rw [sum_zero]
    ring

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