Integer Multiple Cosine Sum Vanishes

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PowerSums

Statement

Theorem Integer Multiple Cosine Sum Vanishes
[blueprint]

For $m \in \mathbb{Z}$ with $m \ne 0$ and $|m| < N$, $\sum_{k=0}^{N-1} \cos\bigl(m(\theta + 2\pi k/N)\bigr) = 0.$

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


  -- Case split on sign of m
  by_cases hm_pos : 0 < m
  · -- m > 0: use sum_cos_multiple_rotated_roots with m as ℕ
    have hm_nat_pos : 0 < m.toNat := by
      omega
    have hm_nat_lt : m.toNat < N := by
      have : (m.toNat : ℤ) = m := Int.toNat_of_nonneg (le_of_lt hm_pos)
      rw [← Nat.cast_lt (α := ℤ)]
      calc (m.toNat : ℤ)
        _ = m := this
        _ = |m| := (abs_of_pos hm_pos).symm
        _ < (N : ℤ) := hm'
    have h_cast : (m : ℝ) = (m.toNat : ℝ) := by
      have : (m.toNat : ℤ) = m := Int.toNat_of_nonneg (le_of_lt hm_pos)
      have : m = (m.toNat : ℤ) := this.symm
      exact_mod_cast this
    simp_rw [h_cast]
    exact sum_cos_multiple_rotated_roots N m.toNat θ hN hm_nat_pos hm_nat_lt
  · -- m < 0: use cos(-x) = cos(x) and the positive case
    push_neg at hm_pos
    have hm_neg : m < 0 := by omega
    have neg_m_pos : 0 < -m := neg_pos.mpr hm_neg
    have h_nat_pos : 0 < (-m).toNat := by
      omega
    have h_nat_lt : (-m).toNat < N := by
      have : ((-m).toNat : ℤ) = -m := Int.toNat_of_nonneg (le_of_lt neg_m_pos)
      rw [← Nat.cast_lt (α := ℤ)]
      calc ((-m).toNat : ℤ)
        _ = -m := this
        _ = |m| := (abs_of_neg hm_neg).symm
        _ < (N : ℤ) := hm'
    have h_cast : (m : ℝ) = -((-m).toNat : ℝ) := by
      have h1 : ((-m).toNat : ℤ) = -m := Int.toNat_of_nonneg (le_of_lt neg_m_pos)
      have h2 : (-m : ℝ) = ((-m).toNat : ℝ) := by exact_mod_cast h1.symm
      calc (m : ℝ)
        _ = -(-m : ℝ) := by ring
        _ = -((-m).toNat : ℝ) := by rw [h2]
    simp_rw [h_cast, neg_mul, Real.cos_neg]
    exact sum_cos_multiple_rotated_roots N (-m).toNat θ hN h_nat_pos h_nat_lt

Dependencies (uses)

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