Chebyshev Roots Power Sum Value

  -- Apply binomial expansion from ChebyshevOrthogonality.lean
  have h_bound : j < 2 * N := by omega
  rw [ChebyshevCircles.sum_cos_pow_chebyshev_binomial N j hN hj h_bound]

  -- All non-constant terms vanish by binomial_terms_vanish_chebyshev
  by_cases h_even : Even j
  · -- j is even: only the middle term (r = j/2) contributes
    rw [if_pos h_even]
    obtain ⟨m, hm⟩ := h_even

    -- Show that only the term where r = j/2 is non-zero
    have sum_eq : ∑ r ∈ Finset.range (j + 1), (j.choose r : ℝ) *
        ∑ k ∈ Finset.range N, Real.cos ((2 * r - j : ℤ) * (2 * k + 1 : ℝ) * π / (2 * N)) =
      (j.choose (j / 2) : ℝ) * N := by
      -- Apply binomial_terms_vanish_chebyshev to show all terms except r = j/2 vanish
      have hj_2_dvd : 2 ∣ j := by
        use m
        rw [hm]
        ring
      have hj_div : j / 2 = m := by omega

      have : ∑ r ∈ Finset.range (j + 1), (j.choose r : ℝ) *
          ∑ k ∈ Finset.range N,
            Real.cos ((2 * r - j : ℤ) * (2 * k + 1 : ℝ) * π / (2 * 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: cos(0 * ...) = 1, 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: apply binomial_terms_vanish_chebyshev
          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
          have h_vanish := ChebyshevCircles.binomial_terms_vanish_chebyshev N j r hN hj' hr h_neq
          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
    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 + 1 : ℝ) * π / (2 * N)) = 0 := by
      -- All terms vanish: (2r - j) is odd when j is odd, apply binomial_terms_vanish_chebyshev
      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
      -- Apply binomial_terms_vanish_chebyshev
      have h_vanish := ChebyshevCircles.binomial_terms_vanish_chebyshev N j r hN hj' hr h_neq
      rw [h_vanish]
      ring
    rw [sum_zero]
    ring