Chebyshev Polynomial Degree

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.PolynomialProperties

Statement

Theorem Chebyshev Polynomial Degree

For $N \geq 1$, $\deg(T_N) = N$. The proof uses strong induction: the base case $T_1 = X$ has degree $1$, and the recurrence step shows $\deg(2X \cdot T_{n+1} - T_n) = n + 2$ because the leading term dominates.

theorem chebyshev_T_degree (N : ℕ) (hN : 0 < N) :
    (Polynomial.Chebyshev.T ℝ N).degree = N := by

Proof ▼


  induction N using Nat.strong_induction_on with
  | h n IH =>
    cases n with
    | zero => omega
    | succ n' =>
      cases n' with
      | zero => norm_num
      | succ m =>
        have h_rec : Chebyshev.T ℝ (↑(m + 2) : ℤ) =
            2 * X * Chebyshev.T ℝ (↑(m + 1) : ℤ) - Chebyshev.T ℝ (↑m : ℤ) := by
          have := Polynomial.Chebyshev.T_add_two ℝ (↑m : ℤ)
          convert this using 2
        simp only [] at *
        rw [h_rec]
        have IH_m1 : (Chebyshev.T ℝ ↑(m + 1)).degree = ↑(m + 1) := by
          apply IH (m + 1) <;> omega
        have h_deg_prod : (2 * X * Chebyshev.T ℝ ↑(m + 1)).degree = ↑(m + 2) := by
          have h_rearrange : (2 : ℝ[X]) * X * Chebyshev.T ℝ ↑(m + 1) =
              2 * (X * Chebyshev.T ℝ ↑(m + 1)) := by ring
          rw [h_rearrange]
          simp only [Polynomial.degree_mul, IH_m1, Polynomial.degree_X]
          have : (2 : ℝ[X]).degree = 0 := Polynomial.degree_C (show (2 : ℝ) ≠ 0 by norm_num)
          simp [this]; ring
        have h_deg_smaller : (Chebyshev.T ℝ ↑m).degree <
            (2 * X * Chebyshev.T ℝ ↑(m + 1)).degree := by
          rw [h_deg_prod]
          by_cases hm : m = 0
          · simp [hm]
          · have IH_m : (Chebyshev.T ℝ ↑m).degree = ↑m := by apply IH m <;> omega
            rw [IH_m]; norm_cast; omega
        rw [Polynomial.degree_sub_eq_left_of_degree_lt h_deg_smaller, h_deg_prod]

Dependencies (uses)

None

Dependents (used by)

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