Binomial Expansion of Exponential Sum

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PowerSums

Statement

Theorem Binomial Expansion of Exponential Sum
[blueprint]

$(e^{ix} + e^{-ix})^j = \sum_{r=0}^{j} \binom{j}{r}\, e^{i(2r - j)x}.$

theorem exp_add_exp_pow (x : ℂ) (j : ℕ) :
    (Complex.exp (x * Complex.I) + Complex.exp (-(x * Complex.I))) ^ j =
    ∑ r ∈ Finset.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 [Finset.mem_range] at hr
    omega
  -- LHS has: exp(xI)^r * exp(-xI)^(j-r) * choose(j,r)
  -- RHS has: choose(j,r) * exp((2r-j)*xI)
  rw [← Complex.exp_nat_mul (n := r), ← Complex.exp_nat_mul (n := j - r)]
  rw [← Complex.exp_add]
  rw [mul_comm]
  congr 1
  -- Show: r * (x * I) + (j - r) * (-(x * I)) = (2 * r - j) * x * I
  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