Chebyshev Angle Power Sum via Binomial Expansion

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.ChebyshevOrthogonality

Statement

Theorem Chebyshev Angle Power Sum via Binomial Expansion
[blueprint]

For $0 < j < 2N$, $\sum_{k=0}^{N-1} \cos^j\!\left(\frac{(2k+1)\pi}{2N}\right) = 2^{-j} \sum_{r=0}^{j} \binom{j}{r} \sum_{k=0}^{N-1} \cos\!\left(\frac{(2r-j)(2k+1)\pi}{2N}\right)$. Each inner sum can then be evaluated using the Chebyshev angle sum vanishing lemmas.

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

Apply Euler's formula to convert $\cos^j$ into a power of exponential sums, expand binomially, interchange summation order, and extract the real part.


  -- Follows sum_cos_pow_eq_sum_binomial from PowerSums.lean
  simp only [cos_as_exp_chebyshev]

  -- Pull power inside re: (z.re)^j = (z^j).re when z is real
  have h_re_pow : ∀ k, ((Complex.exp (↑((2 * k + 1 : ℝ) * π / (2 * N)) * Complex.I) +
      Complex.exp (-(↑((2 * k + 1 : ℝ) * π / (2 * N)) * Complex.I))) / 2).re ^ j =
    (((Complex.exp (↑((2 * k + 1 : ℝ) * π / (2 * N)) * Complex.I) +
      Complex.exp (-(↑((2 * k + 1 : ℝ) * π / (2 * N)) * Complex.I))) / 2) ^ j).re := by
    intro k
    set z := (Complex.exp (↑((2 * k + 1 : ℝ) * π / (2 * N)) * Complex.I) +
        Complex.exp (-(↑((2 * k + 1 : ℝ) * π / (2 * N)) * Complex.I))) / 2 with z_def
    have h_real : z.im = 0 := by
      rw [z_def]
      have h1 : (Complex.exp (↑((2 * k + 1 : ℝ) * π / (2 * N)) * Complex.I) +
          Complex.exp (-(↑((2 * k + 1 : ℝ) * π / (2 * N)) * Complex.I))).im = 0 := by
        rw [Complex.add_im, Complex.exp_ofReal_mul_I_im]
        have : (Complex.exp (-(↑((2 * k + 1 : ℝ) * π / (2 * N)) * Complex.I))).im =
          Real.sin (-((2 * k + 1 : ℝ) * π / (2 * N))) := by
          rw [show -(↑((2 * k + 1 : ℝ) * π / (2 * N)) * Complex.I) =
            (↑(-((2 * k + 1 : ℝ) * π / (2 * 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
    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]

  simp only [div_pow]

  rw [show ∑ x ∈ range N, (Complex.exp (↑((2 * ↑x + 1) * π / (2 * ↑N)) * Complex.I) +
      Complex.exp (-(↑((2 * ↑x + 1) * π / (2 * ↑N)) * Complex.I))) ^ j / (2 : ℂ) ^ j =
    ∑ x ∈ range N, (∑ r ∈ range (j + 1), (j.choose r : ℂ) *
      Complex.exp ((2 * r - j : ℤ) * ↑((2 * ↑x + 1) * π / (2 * ↑N)) * Complex.I)) / (2 : ℂ) ^ j by
    apply Finset.sum_congr rfl
    intro i _
    rw [exp_add_exp_pow_chebyshev (↑((2 * ↑i + 1) * π / (2 * ↑N))) j]]

  rw [← Finset.sum_div, div_eq_mul_inv, mul_comm]

  rw [show ((2 : ℂ) ^ j)⁻¹ = (2 : ℂ) ^ (-(j : ℤ)) by
    rw [← zpow_natCast, ← zpow_neg_one, ← zpow_mul]
    norm_num]

  rw [Complex.mul_re]

  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

  rw [Finset.sum_comm]
  apply Finset.sum_congr rfl
  intro r hr
  rw [← Finset.mul_sum]
  congr 1

  rw [← Complex.re_sum, Complex.re_sum]
  apply Finset.sum_congr rfl
  intro k _

  -- Show exp(...).re = (exp(...).re + exp(-...).re) / 2
  -- First normalize the LHS to match RHS form
  have lhs_norm : (Complex.exp ((2 * ↑r - ↑j) * ((2 * ↑k + 1) * ↑π / (2 * ↑N)) * Complex.I)).re =
      (Complex.exp ((2 * ↑r - ↑j) * (2 * ↑k + 1) * ↑π / (2 * ↑N) * Complex.I)).re := by
    congr 1
    ring_nf

  rw [lhs_norm]

  -- Now show: exp(m*θ*I).re = (exp(m*θ*I).re + exp(-m*θ*I).re) / 2
  have h1 : (Complex.exp ((2 * ↑r - ↑j) * (2 * ↑k + 1) * ↑π / (2 * ↑N) * Complex.I)).re =
    Real.cos ((2 * ↑r - ↑j) * (2 * ↑k + 1) * π / (2 * ↑N)) := by
    have : (2 * ↑r - ↑j) * (2 * ↑k + 1) * ↑π / (2 * ↑N) * Complex.I =
      ↑((2 * ↑r - ↑j) * (2 * ↑k + 1) * π / (2 * ↑N)) * Complex.I := by
      push_cast
      ring
    rw [this, Complex.exp_ofReal_mul_I_re]
  have h2 : (Complex.exp (-((2 * ↑r - ↑j) * (2 * ↑k + 1) * ↑π / (2 * ↑N) * Complex.I))).re =
    Real.cos ((2 * ↑r - ↑j) * (2 * ↑k + 1) * π / (2 * ↑N)) := by
    have : -((2 * ↑r - ↑j) * (2 * ↑k + 1) * ↑π / (2 * ↑N) * Complex.I) =
      ↑(-((2 * ↑r - ↑j) * (2 * ↑k + 1) * π / (2 * ↑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