Sum of Cosines at Equally-Spaced Angles

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.TrigonometricIdentities

Statement

The discrete orthogonality of roots of unity manifests geometrically: the projections of equally-spaced points on the circle always balance around the origin.

Theorem Sum of Cosines at Equally-Spaced Angles

[blueprint]

For $N \ge 2$ and any $\theta \in \mathbb{R}$, $\sum_{k=0}^{N-1} \cos\bigl(\theta + \frac{2\pi k}{N}\bigr) = 0.$

theorem sum_cos_roots_of_unity (N : ℕ) (θ : ℝ) (hN : 2 ≤ N) :
    ∑ k ∈ Finset.range N, Real.cos (θ + 2 * π * k / N) = 0 := by

Proof ▼

Factor out $e^{i\theta}$ from the Euler-formula representation and apply the geometric sum for a primitive $N$-th root of unity.


  conv_lhs =>
    arg 2
    ext k
    rw [← Complex.exp_ofReal_mul_I_re (θ + 2 * π * k / N)]
  rw [← Complex.re_sum]
  simp only [Complex.ofReal_add, Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_natCast]
  conv_lhs =>
    arg 1
    arg 2
    ext k
    rw [add_mul, Complex.exp_add]
  rw [← Finset.mul_sum]
  have hN' : N ≠ 0 := by omega
  let ζ := Complex.exp (2 * π * I / N)
  have hζ : IsPrimitiveRoot ζ N := Complex.isPrimitiveRoot_exp N hN'
  have geom_sum : ∑ i ∈ Finset.range N, ζ ^ i = 0 := hζ.geom_sum_eq_zero (by omega : 1 < N)
  suffices ∑ i ∈ Finset.range N, Complex.exp (↑2 * ↑π * ↑i / ↑N * I) = 0 by
    simp [this]
  calc ∑ i ∈ Finset.range N, Complex.exp (↑2 * ↑π * ↑i / ↑N * I)
      = ∑ i ∈ Finset.range N, ζ ^ i := by
        congr 1 with i
        simp only [ζ]
        rw [← Complex.exp_nat_mul]
        congr 1
        field_simp
    _ = 0 := geom_sum

Dependencies (uses)

None

Dependents (used by)

Power Sum Invariance

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