Power Sum as Binomial Cosine Sum

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PowerSums

Statement

Theorem Power Sum as Binomial Cosine Sum
[blueprint]

For $j < N$, $\sum_{k=0}^{N-1} \cos^j\!\bigl(\theta + \frac{2\pi k}{N}\bigr) = 2^{-j} \sum_{r=0}^{j} \binom{j}{r} \sum_{k=0}^{N-1} \cos\!\bigl((2r-j)(\theta + \frac{2\pi k}{N})\bigr).$

theorem sum_cos_pow_eq_sum_binomial (N j : ℕ) (θ : ℝ) (_hN : 0 < N) (_hj : j < N) :
    ∑ k ∈ Finset.range N, (Real.cos (θ + 2 * π * k / N)) ^ j =
    (2 : ℝ) ^ (-(j : ℤ)) * ∑ r ∈ Finset.range (j + 1), (j.choose r : ℝ) *
    ∑ k ∈ Finset.range N, Real.cos (((2 * r - j) : ℤ) * (θ + 2 * π * k / N)) := by
Proof ▼ 


  -- Use the fact that cos(x) = Re((e^{ix} + e^{-ix})/2)
  -- and apply binomial theorem
  simp only [cos_as_exp]
  -- Pull power inside re: (z.re)^j = (z^j).re when z is real
  have h_re_pow : ∀ k, ((Complex.exp (↑(θ + 2 * π * k / N) * Complex.I) +
      Complex.exp (-(↑(θ + 2 * π * k / N) * Complex.I))) / 2).re ^ j =
    (((Complex.exp (↑(θ + 2 * π * k / N) * Complex.I) +
      Complex.exp (-(↑(θ + 2 * π * k / N) * Complex.I))) / 2) ^ j).re := by
    intro k
    -- The sum e^{ix} + e^{-ix} is real (it equals 2cos(x))
    set z := (Complex.exp (↑(θ + 2 * π * k / N) * Complex.I) +
        Complex.exp (-(↑(θ + 2 * π * k / N) * Complex.I))) / 2 with z_def
    have h_real : z.im = 0 := by
      rw [z_def]
      have h1 : (Complex.exp (↑(θ + 2 * π * k / N) * Complex.I) +
          Complex.exp (-(↑(θ + 2 * π * k / N) * Complex.I))).im = 0 := by
        rw [Complex.add_im, Complex.exp_ofReal_mul_I_im]
        have : (Complex.exp (-(↑(θ + 2 * π * k / N) * Complex.I))).im =
          Real.sin (-(θ + 2 * π * k / N)) := by
          rw [show -(↑(θ + 2 * π * k / N) * Complex.I) =
            (↑(-(θ + 2 * π * k / N)) : ℂ) * Complex.I by
            apply Complex.ext <;> simp]
          exact Complex.exp_ofReal_mul_I_im _
        rw [this, Real.sin_neg]
        ring
      rw [Complex.div_im, h1]
      simp
    -- Since z is real, z.re^j = (z^j).re
    have h_eq : z = (z.re : ℂ) := Complex.ext rfl h_real
    calc z.re ^ j
      _ = (z.re : ℂ).re ^ j := by simp
      _ = ((z.re : ℂ) ^ j).re := by simp [← Complex.ofReal_pow]
      _ = (z ^ j).re := by rw [← h_eq]
  conv_lhs =>
    arg 2
    ext k
    rw [h_re_pow k]
  rw [← Complex.re_sum]
  -- Now work with the sum of complex powers
  -- Apply binomial expansion to each term, then manipulate
  simp only [div_pow]
  -- Apply binomial expansion inside the sum and factor out 2^j
  rw [show ∑ x ∈ Finset.range N,
        (Complex.exp (↑(θ + 2 * π * ↑x / ↑N) * Complex.I) +
          Complex.exp (-(↑(θ + 2 * π * ↑x / ↑N) * Complex.I))) ^ j / (2 : ℂ) ^ j =
      ∑ x ∈ Finset.range N,
        (∑ r ∈ Finset.range (j + 1), (j.choose r : ℂ) *
          Complex.exp ((2 * r - j : ℤ) * ↑(θ + 2 * π * ↑x / ↑N) * Complex.I)) /
        (2 : ℂ) ^ j by
    apply Finset.sum_congr rfl
    intro i _
    rw [exp_add_exp_pow (↑(θ + 2 * π * ↑i / ↑N)) j]]
  rw [← Finset.sum_div]
  -- Rewrite division as multiplication by inverse
  rw [div_eq_mul_inv, mul_comm]
  -- Simplify: (2^j)⁻¹ = 2^(-j)
  rw [show ((2 : ℂ) ^ j)⁻¹ = (2 : ℂ) ^ (-(j : ℤ)) by
    rw [← zpow_natCast, ← zpow_neg_one, ← zpow_mul]
    norm_num]
  -- Move .re inside and commute sums
  rw [Complex.mul_re]
  -- Simplify: Re(2^(-j)) = 2^(-j) and Im(2^(-j)) = 0
  have h_re : ((2 : ℂ) ^ (-(j : ℤ))).re = (2 : ℝ) ^ (-(j : ℤ)) := by
    have : (2 : ℂ) = (↑(2 : ℝ) : ℂ) := rfl
    rw [this, ← Complex.ofReal_zpow, Complex.ofReal_re]
  have h_im : ((2 : ℂ) ^ (-(j : ℤ))).im = 0 := by
    have : (2 : ℂ) = (↑(2 : ℝ) : ℂ) := rfl
    rw [this, ← Complex.ofReal_zpow, Complex.ofReal_im]
  rw [h_re, h_im]
  simp
  -- Now commute the sums and simplify the RHS
  rw [Finset.sum_comm]
  apply Finset.sum_congr rfl
  intro r hr
  rw [← Finset.mul_sum]
  congr 1
  -- Show (∑ exp(...)).re = ∑ (exp(...).re + exp(-...).re) / 2
  rw [← Complex.re_sum]
  -- Now show ∑ exp(...).re = ∑ (exp(...).re + exp(-...).re) / 2
  -- First move .re inside the left sum
  rw [Complex.re_sum]
  -- Each term: exp(ix).re = (exp(ix).re + exp(-ix).re) / 2
  -- This holds because exp(ix).re = cos(x) and exp(-ix).re = cos(-x) = cos(x)
  apply Finset.sum_congr rfl
  intro k _
  -- Show exp(...).re = (exp(...).re + exp(-...).re) / 2
  -- Use that exp(ix).re = cos(x) and exp(-ix).re = cos(-x) = cos(x)
  have h1 :
      (Complex.exp ((2 * ↑r - ↑j) * (↑θ + 2 * ↑π * ↑k / ↑N) * Complex.I)).re =
        Real.cos ((2 * ↑r - ↑j) * (θ + 2 * π * ↑k / ↑N)) := by
    have : (2 * ↑r - ↑j) * (↑θ + 2 * ↑π * ↑k / ↑N) * Complex.I =
      ↑((2 * ↑r - ↑j) * (θ + 2 * π * ↑k / ↑N)) * Complex.I := by
      push_cast
      ring
    rw [this, Complex.exp_ofReal_mul_I_re]
  have h2 :
      (Complex.exp (-((2 * ↑r - ↑j) * (↑θ + 2 * ↑π * ↑k / ↑N) * Complex.I))).re =
        Real.cos ((2 * ↑r - ↑j) * (θ + 2 * π * ↑k / ↑N)) := by
    have : -((2 * ↑r - ↑j) * (↑θ + 2 * ↑π * ↑k / ↑N) * Complex.I) =
      ↑(-((2 * ↑r - ↑j) * (θ + 2 * π * ↑k / ↑N))) * Complex.I := by
      push_cast
      ring
    rw [this, Complex.exp_ofReal_mul_I_re, Real.cos_neg]
  rw [h1, h2]
  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