Distinctness of Chebyshev Roots

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.ChebyshevRoots

Statement

Theorem Distinctness of Chebyshev Roots
[blueprint]

For $N \geq 1$, if $0 \leq k_1, k_2 < N$ and $\xi_{k_1} = \xi_{k_2}$, then $k_1 = k_2$. The proof uses the injectivity of $\cos$ on $[0, \pi]$: since $(2k+1)\pi/(2N) \in (0, \pi)$ for all $0 \leq k < N$, equal cosines imply equal angles and hence equal indices.

theorem chebyshevRoots_distinct (N : ℕ) (hN : 0 < N) (k₁ k₂ : ℕ)
    (hk₁ : k₁ < N) (hk₂ : k₂ < N) (h_eq : chebyshevRoot N k₁ = chebyshevRoot N k₂) :
    k₁ = k₂ := by
Proof ▼

Show both angles lie in $[0,\pi]$, apply injectivity of cosine on this interval to conclude the angles are equal, then extract $k_1 = k_2$ by arithmetic.


  unfold chebyshevRoot at h_eq

  -- cos is injective on [0, π], and our angles are in this range
  let θ₁ := (2 * k₁ + 1 : ℝ) * π / (2 * N)
  let θ₂ := (2 * k₂ + 1 : ℝ) * π / (2 * N)

  -- Show both angles are in [0, π]
  have h₁_mem : θ₁ ∈ Set.Icc (0 : ℝ) π := by
    constructor
    · -- 0 ≤ θ₁
      simp only [θ₁]
      apply div_nonneg
      · apply mul_nonneg
        · norm_cast; omega
        · exact Real.pi_pos.le
      · norm_cast; omega
    · -- θ₁ ≤ π
      simp only [θ₁]
      have : (2 * k₁ + 1 : ℝ) < 2 * N := by norm_cast; omega
      have : (2 * k₁ + 1 : ℝ) * π < (2 * N) * π := by
        exact mul_lt_mul_of_pos_right this Real.pi_pos
      have lt_pi : (2 * k₁ + 1 : ℝ) * π / (2 * N) < π := by
        have hN' : (0 : ℝ) < 2 * N := by norm_cast; omega
        have : (2 * k₁ + 1 : ℝ) * π < π * (2 * N) := by linarith
        calc (2 * k₁ + 1 : ℝ) * π / (2 * N)
            < π * (2 * N) / (2 * N) := by
              exact div_lt_div_of_pos_right this hN'
          _ = π := by field_simp
      exact le_of_lt lt_pi

  have h₂_mem : θ₂ ∈ Set.Icc (0 : ℝ) π := by
    constructor
    · -- 0 ≤ θ₂
      simp only [θ₂]
      apply div_nonneg
      · apply mul_nonneg
        · norm_cast; omega
        · exact Real.pi_pos.le
      · norm_cast; omega
    · -- θ₂ ≤ π
      simp only [θ₂]
      have : (2 * k₂ + 1 : ℝ) < 2 * N := by norm_cast; omega
      have : (2 * k₂ + 1 : ℝ) * π < (2 * N) * π := by
        exact mul_lt_mul_of_pos_right this Real.pi_pos
      have lt_pi : (2 * k₂ + 1 : ℝ) * π / (2 * N) < π := by
        have hN' : (0 : ℝ) < 2 * N := by norm_cast; omega
        have : (2 * k₂ + 1 : ℝ) * π < π * (2 * N) := by linarith
        calc (2 * k₂ + 1 : ℝ) * π / (2 * N)
            < π * (2 * N) / (2 * N) := by
              exact div_lt_div_of_pos_right this hN'
          _ = π := by field_simp
      exact le_of_lt lt_pi

  -- Use injectivity of cos on [0, π]
  have cos_inj : θ₁ = θ₂ := by
    have inj := Real.injOn_cos
    unfold Set.InjOn at inj
    apply inj h₁_mem h₂_mem h_eq

  -- From θ₁ = θ₂, conclude k₁ = k₂
  simp only [θ₁, θ₂] at cos_inj
  have : (2 * k₁ + 1 : ℝ) * π / (2 * N) = (2 * k₂ + 1 : ℝ) * π / (2 * N) := cos_inj
  have : (2 * k₁ + 1 : ℝ) * π = (2 * k₂ + 1 : ℝ) * π := by
    have hN' : (0 : ℝ) < 2 * N := by norm_cast; omega
    have hN_ne : (2 * N : ℝ) ≠ 0 := ne_of_gt hN'
    calc (2 * k₁ + 1 : ℝ) * π
        = (2 * k₁ + 1 : ℝ) * π / (2 * N) * (2 * N) := by field_simp
      _ = (2 * k₂ + 1 : ℝ) * π / (2 * N) * (2 * N) := by rw [this]
      _ = (2 * k₂ + 1 : ℝ) * π := by field_simp
  have : (2 * k₁ + 1 : ℝ) = (2 * k₂ + 1 : ℝ) := by
    have hπ : π ≠ 0 := Real.pi_ne_zero
    calc (2 * k₁ + 1 : ℝ)
        = (2 * k₁ + 1 : ℝ) * π / π := by field_simp
      _ = (2 * k₂ + 1 : ℝ) * π / π := by rw [this]
      _ = (2 * k₂ + 1 : ℝ) := by field_simp
  have : 2 * k₁ + 1 = 2 * k₂ + 1 := by norm_cast at this
  omega

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