Factoring Chebyshev Angle Exponentials

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.ChebyshevOrthogonality

Statement

Theorem Factoring Chebyshev Angle Exponentials

$\sum_{k=0}^{N-1} e^{(2k+1)m\pi i/(2N)} = e^{m\pi i/(2N)} \cdot \sum_{k=0}^{N-1} e^{km\pi i/N}$. The identity $(2k+1) = 1 + 2k$ allows factoring out the common phase from each term.

theorem sum_exp_chebyshev_angles (N m : ℕ) :
    ∑ k ∈ range N, exp ((2 * k + 1 : ℂ) * m * π * I / (2 * N)) =
    exp (m * π * I / (2 * N)) * ∑ k ∈ range N, exp (k * m * π * I / N) := by

Proof ▼


  -- Factor out exp(mπi/(2N)) from each term
  -- (2k+1) * m * π/(2N) = m*π/(2N) + k * m * π/N
  conv_lhs => arg 2; ext k; rw [show (2 * k + 1 : ℂ) * m * π * I / (2 * N) =
      m * π * I / (2 * N) + k * m * π * I / N by
    field_simp
    ring]
  simp_rw [Complex.exp_add, Finset.mul_sum]

Dependencies (uses)

None

Dependents (used by)

None

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms