Binomial Expansion of Exponential Sum

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.ChebyshevOrthogonality

Statement

Theorem Binomial Expansion of Exponential Sum
[blueprint]

For $x \in \mathbb{C}$ and $j \in \mathbb{N}$, $(e^{ix} + e^{-ix})^j = \sum_{r=0}^{j} \binom{j}{r}\, e^{i(2r-j)x}$. This identity converts the $j$-th power of a cosine-type expression into a sum of complex exponentials at integer frequencies, which is the key step in the binomial expansion technique for power sums.

theorem exp_add_exp_pow_chebyshev (x : ℂ) (j : ℕ) :
    (Complex.exp (x * Complex.I) + Complex.exp (-(x * Complex.I))) ^ j =
    ∑ r ∈ range (j + 1), (j.choose r : ℂ) * Complex.exp ((2 * r - j : ℤ) * x * Complex.I) := by
Proof ▼ 


  rw [Commute.add_pow (Commute.all _ _)]
  apply Finset.sum_congr rfl
  intro r hr
  have hr_le : r ≤ j := by simp only [mem_range] at hr; omega
  rw [← Complex.exp_nat_mul (n := r), ← Complex.exp_nat_mul (n := j - r)]
  rw [← Complex.exp_add, mul_comm]
  congr 1
  simp only [Nat.cast_sub hr_le]
  congr 1
  simp only [Int.cast_sub, Int.cast_mul, Int.cast_ofNat, Int.cast_natCast]
  ring

Dependencies (uses)

None

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