Cosine Sum at Integer Multiples Vanishes

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.TrigonometricIdentities

Statement

Theorem Cosine Sum at Integer Multiples Vanishes
[blueprint]

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

theorem sum_cos_multiple_rotated_roots (N : ℕ) (m : ℕ) (θ : ℝ)
    (hN : 0 < N) (hm : 0 < m) (hm' : m < N) :
    ∑ k ∈ Finset.range N, Real.cos (m * (θ + 2 * π * k / N)) = 0 := by
Proof ▼

Apply Euler's formula $\cos(m\theta) = \mathrm{Re}(e^{im\theta})$, factor out $e^{im\theta}$, and observe the inner geometric sum $\sum \omega^{mk}$ vanishes since $\omega^m \ne 1$ when $N \nmid m$.


  conv_lhs =>
    arg 2
    ext k
    rw [← Complex.exp_ofReal_mul_I_re (m * (θ + 2 * π * k / N))]
  rw [← Complex.re_sum]
  simp only [Complex.ofReal_mul, Complex.ofReal_add, Complex.ofReal_div, Complex.ofReal_natCast]
  have hN' : N ≠ 0 := Nat.pos_iff_ne_zero.mp hN
  let ζ := Complex.exp (2 * π * I / N)
  have hζ : IsPrimitiveRoot ζ N := Complex.isPrimitiveRoot_exp N hN'
  suffices h_sum_zero : ∑ k ∈ Finset.range N, cexp (↑m * (↑2 * ↑π * ↑k / ↑N) * I) = 0 by
    simp only [mul_add, add_mul]
    conv_lhs =>
      arg 1
      arg 2
      ext x
      rw [Complex.exp_add]
    rw [← Finset.mul_sum]
    have : ∑ i ∈ Finset.range N, cexp (↑m * (↑2 * ↑π * ↑i / ↑N) * I) = 0 := h_sum_zero
    simp [this]
  calc ∑ k ∈ Finset.range N, cexp (↑m * (↑2 * ↑π * ↑k / ↑N) * I)
      = ∑ k ∈ Finset.range N, ζ ^ (m * k) := by
        congr 1 with k
        simp only [ζ]
        rw [← Complex.exp_nat_mul]
        congr 1
        field_simp
        norm_cast
    _ = ∑ k ∈ Finset.range N, (ζ ^ m) ^ k := by
        congr 1 with k
        rw [← pow_mul]
    _ = 0 := by
        have h_ne_one : ζ ^ m ≠ 1 := by
          intro h_eq
          have h_div : N ∣ m := by
            have := hζ.pow_eq_one_iff_dvd m
            exact this.mp h_eq
          have : N ≤ m := Nat.le_of_dvd (by omega) h_div
          omega
        have h_pow_N : (ζ ^ m) ^ N = 1 := by
          rw [← pow_mul, mul_comm m N, pow_mul]
          simp [hζ.pow_eq_one]
        have h_geom : (ζ ^ m - 1) * ∑ k ∈ Finset.range N, (ζ ^ m) ^ k = (ζ ^ m) ^ N - 1 :=
          mul_geom_sum (ζ ^ m) N
        rw [h_pow_N] at h_geom
        have : (ζ ^ m - 1) * ∑ k ∈ Finset.range N, (ζ ^ m) ^ k = 0 := by
          rw [h_geom]; ring
        exact eq_zero_of_ne_zero_of_mul_left_eq_zero (sub_ne_zero_of_ne h_ne_one) this

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