Chebyshev polynomial

Stream: new members

[Nick_adfor]

I've trouble filling the following theorem, for the lemma I think useable cannot be fixed.

import Mathlib

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  intro n hn
  exact U_eq ℝ ↑n

/-with errors
failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    U_eval_one m-/
lemma Chebyshev.U_eval_one (n : ℕ) : (Chebyshev.U ℝ n).eval 1 = (n + 1 : ℝ) := by
  induction n with
  | zero => simp [Chebyshev.U]
  | succ n ih =>
    cases n with
    | zero => simp only [zero_add, Nat.cast_one, U_one, eval_mul, eval_ofNat, eval_X, mul_one]; ring_nf
    | succ m =>
      have : (Chebyshev.U ℝ (m + 2)).eval 1 = 2 * 1 * (Chebyshev.U ℝ (m + 1)).eval 1 - (Chebyshev.U ℝ m).eval 1 := by
        simp [U_add_two, Polynomial.eval_sub, Polynomial.eval_mul, Polynomial.eval_X, Polynomial.eval_C]
      have : (Chebyshev.U ℝ (m + 2)).eval 1 = 2 * (m + 2 : ℝ) - (m + 1 : ℝ) := by
        rw [this, Chebyshev.U_eval_one (m : ℕ)]
        ring_nf
        simp only [Polynomial.Chebyshev.U_eval_one, Int.cast_add, Int.cast_one, Int.cast_natCast]
        ring_nf
      ring_nf
      simp only [Nat.cast_add, Nat.cast_ofNat, Polynomial.Chebyshev.U_eval_one, Int.cast_add,
        Int.cast_ofNat, Int.cast_natCast]
      ring_nf

/-- lemma: U_n(-1) = (-1)^n (n+1).-/
lemma Chebyshev.U_eval_neg_one (n : ℕ) :
  (Chebyshev.U ℝ n).eval (-1) = (-1 : ℝ) ^ n * (n + 1 : ℝ) := by
  induction n with
  | zero => simp only [CharP.cast_eq_zero, U_zero, eval_one, pow_zero, zero_add, mul_one]
  | succ n ih =>
    cases n with
    | zero => simp only [zero_add, Nat.cast_one, U_one, eval_mul, eval_ofNat, eval_X, mul_neg,
      mul_one, pow_one, neg_mul, one_mul, neg_add_rev]; ring_nf

    | succ m =>
      have : (Chebyshev.U ℝ (m + 2)).eval (-1)
            = 2 * (-1) * (Chebyshev.U ℝ (m + 1)).eval (-1) - (Chebyshev.U ℝ m).eval (-1) := by
        simp [U_add_two, Polynomial.eval_sub, Polynomial.eval_mul, Polynomial.eval_X, Polynomial.eval_C]
      have h0 : (Chebyshev.U ℝ (m+2)).eval (-1) = Polynomial.eval (-1) (Chebyshev.U ℝ (m+2)) := rfl
      have h1 : (Chebyshev.U ℝ (m+1)).eval (-1) = Polynomial.eval (-1) (Chebyshev.U ℝ (m+1)) := rfl
      have h2 : (Chebyshev.U ℝ m).eval (-1) = Polynomial.eval (-1) (Chebyshev.U ℝ m) := rfl
      have recurrence_eq : Polynomial.eval (-1) (Chebyshev.U ℝ (m + 2)) =
                          2 * (-1) * Polynomial.eval (-1) (Chebyshev.U ℝ (m + 1)) -
                          Polynomial.eval (-1) (Chebyshev.U ℝ m) := by
        rw [← h0, ← h1, ← h2, this]
      have target_eq : (-1 : ℝ) ^ (m + 2) * ((m + 2 : ℕ) + 1 : ℝ) = 2 * (-1) * ((-1 : ℝ) ^ (m + 1) * (m + 2 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ)) := by
        calc
          (-1 : ℝ) ^ (m + 2) * ((m + 2 : ℕ) + 1 : ℝ) = (-1 : ℝ) ^ m * (-1) ^ 2 * (m + 3 : ℝ) := by
            ring_nf
            simp only [Nat.cast_add, Nat.cast_ofNat]
            ring_nf
          _ = (-1 : ℝ) ^ m * 1 * (m + 3 : ℝ) := by norm_num
          _ = 2 * (-1) * ((-1) * (-1 : ℝ) ^ m * (m + 2)) - ((-1 : ℝ) ^ m * (m + 1)) := by ring
          _ = 2 * (-1) * ((-1 : ℝ) ^ (m + 1) * (m + 2 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ)) := by
            rw [show (-1 : ℝ) * (-1 : ℝ) ^ m = (-1 : ℝ) ^ (m + 1) by ring]

      simp only [show (m + 1 + 1 : ℕ) = m + 2 by omega]
      sorry

theorem Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
  intro hx
  -- Use the fact that Chebyshev polynomials have simple roots in (-1,1)

  have : ∀ k : ℕ, k < n → ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval (Real.cos (Real.pi * (k + 1) / (n + 1))) ≠ 0 := by
    sorry  -- Would need to compute the derivative explicitly

  -- Show that x must be of the form cos(π*(k+1)/(n+1)) for some k
  have : ∃ k : ℕ, k < n ∧ x = Real.cos (Real.pi * (k + 1) / (n + 1)) := by
    set θ := Real.arccos (x/2) with hθ
    have hUθ := Chebyshev.U_real_cos θ n
    rw [Polynomial.eval_comp, Polynomial.eval_mul, Polynomial.eval_C,
        Polynomial.eval_X] at hx
    have hsinNθ : Real.sin ((n+1) * θ) = 0 := by
      sorry
    obtain ⟨k, hk⟩ := Real.sin_eq_zero_iff.1 hsinNθ
    sorry

  rcases this with ⟨k, _, hx⟩
  rw [hx]
  exact this k ‹k < n›

[Ilmārs Cīrulis]

The web editor tells me that "Unknown identifier Chebyshev.U".

[Ilmārs Cīrulis]

Adding open Polynomial solves this problem.

[Nick_adfor]

There's a terrible thing: I write the code in v4.16.0. Lean 4 web might be v4.22.0. Some of U should be Chebyshev.U.

[Nick_adfor]

Now I fixed the second lemma, leaving the third and the theorem.

lemma Chebyshev_U_eval_one (n : ℕ) : (Chebyshev.U ℝ n).eval (1 : ℝ) = (n + 1 : ℝ) := by
  induction' n with n IH
  · simp [Chebyshev.U_zero]
  · cases' n with n
    · simp only [zero_add, Nat.cast_one, U_one, eval_mul, eval_ofNat, eval_X, mul_one]
      ring_nf
    · have := Chebyshev_U_recursion (n + 2) (by omega)
      simp only [Nat.cast_add, Nat.cast_ofNat, U_add_two, add_sub_cancel_right, sub_left_inj,
        mul_eq_mul_left_iff, mul_eq_zero, OfNat.ofNat_ne_zero, X_ne_zero, or_self, or_false,
        Nat.cast_one, U_eval_one, Int.cast_add, Int.cast_natCast, Int.cast_one] at this ⊢

[Nick_adfor]

I'm wondering if there's some good way to finish realizing the theorem.

[Snir Broshi]

Can you please send a MWE that runs in Lean 4 Web correctly?
It's difficult to try to help without it

[Nick_adfor]

This part can work on lean 4 web (v4.24.0-rc1)

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  intro n hn
  exact Chebyshev.U_eq ℝ ↑n

lemma Chebyshev_U_eval_one (n : ℕ) : (Chebyshev.U ℝ n).eval (1 : ℝ) = (n + 1 : ℝ) := by
  induction' n with n IH
  · simp [Chebyshev.U_zero]
  · cases' n with n
    · simp
      ring_nf
    · have := Chebyshev_U_recursion (n + 2) (by omega)
      simp at this ⊢

/-- lemma: U_n(-1) = (-1)^n (n+1).-/
lemma Chebyshev.U_eval_neg_one (n : ℕ) :
    (Chebyshev.U ℝ n).eval (-1) = (-1 : ℝ) ^ n * (n + 1 : ℝ) := by
  induction' n using Nat.strong_induction_on with n IH
  rcases n with (rfl|rfl|m)
  · simp  -- n = 0
  · simp   -- n = 1
    ring_nf
  · -- n = m + 2, where m : ℕ
    have : m + 2 = (m + 1) + 1 := by omega
    rw [<-this]
    have hm1 : m < m + 2 := by omega
    have hm2 : m + 1 < m + 2 := by omega
    have rec_eq := Chebyshev.U_add_two ℝ (m)
    simp only at rec_eq ⊢
    have IH_m1 := IH (m + 1) hm2
    have eval_rec_eq : (Chebyshev.U ℝ (m + 2)).eval (-1) =
                      (2 * X * Chebyshev.U ℝ (m + 1) - Chebyshev.U ℝ m).eval (-1) := by
      rw [rec_eq]
    have cast_eq1 : (U ℝ (m + 2) : Polynomial ℝ) = U ℝ (↑(m + 2) : ℕ) := by simp
    have cast_eq2 : (U ℝ (m + 1) : Polynomial ℝ) = U ℝ (↑(m + 1) : ℕ) := by simp
    have cast_eq3 : (U ℝ m : Polynomial ℝ) = U ℝ (↑m : ℕ) := by simp
    rw [← cast_eq1]
    rw [rec_eq]
    simp only [eval_sub, eval_mul, eval_ofNat, eval_X]
    rw [IH m hm1]
    rw [cast_eq2]
    rw [IH (m + 1) hm2]
    calc
      2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * ((m + 1 : ℕ) + 1 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ))
        = 2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * (m + 2 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ)) := by
        simp
        ring_nf
      _ = 2 * (-1) * ((-1) * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * (1 * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * ((-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = (-1) ^ m * (2*(m + 2) - (m + 1)) := by ring
      _ = (-1) ^ m * (m + 3) := by ring
      _ = (-1) ^ m * (-1)^2 * (m + 3) := by norm_num
      _ = (-1) ^ (m + 2) * (m + 3) := by ring
      _ = (-1 : ℝ) ^ (m + 2) * (((m + 2 : ℕ) : ℝ) + 1) := by simp; ring_nf

theorem Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
  intro hx
  -- Use the fact that Chebyshev polynomials have simple roots in (-1,1)

  have : ∀ k : ℕ, k < n → ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval (Real.cos (Real.pi * (k + 1) / (n + 1))) ≠ 0 := by
    sorry  -- Would need to compute the derivative explicitly

  -- Show that x must be of the form cos(π*(k+1)/(n+1)) for some k
  have : ∃ k : ℕ, k < n ∧ x = Real.cos (Real.pi * (k + 1) / (n + 1)) := by
    set θ := Real.arccos (x/2) with hθ
    have hUθ := Chebyshev.U_real_cos θ n
    rw [Polynomial.eval_comp, Polynomial.eval_mul, Polynomial.eval_C,
        Polynomial.eval_X] at hx
    have hsinNθ : Real.sin ((n+1) * θ) = 0 := by
      sorry
    obtain ⟨k, hk⟩ := Real.sin_eq_zero_iff.1 hsinNθ
    sorry

  rcases this with ⟨k, _, hx⟩
  rw [hx]
  exact this k ‹k < n›

[Nick_adfor]

Snir said:

Can you please send a MWE that runs in Lean 4 Web correctly?
It's difficult to try to help without it

Thank you for your attention. But now the main theorem haven't finished.

[Nick_adfor]

Ilmārs Cīrulis said:

Adding open Polynomial solves this problem.

More namespace is added in my new code to make it compatible for both v4.16.0 and v4.24.0-rc1(Lean 4 Web). But now the main theorem haven't finished.

[Ilmārs Cīrulis]

Thank you, will take a look today.

[Ilmārs Cīrulis]

Looks nontrivial to me, won't promise anything though.

[Nick_adfor]

Ilmārs Cīrulis said:

Looks nontrivial to me, won't promise anything though.

Terrible : (

[Ilmārs Cīrulis]

Did you manage to finish your proof?

[Nick_adfor]

Till today I just have a draft. I even do not find a good way to have all the lemma used in the proof of theorem.

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

macro "by_eval" : tactic => `(tactic| (
  apply Polynomial.funext
  intro x
  simp only [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast, eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
  ring
))

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  intro n hn
  exact Chebyshev.U_eq ℝ ↑n

lemma Chebyshev_U_eval_one (n : ℕ) : (Chebyshev.U ℝ n).eval (1 : ℝ) = (n + 1 : ℝ) := by
  induction' n with n IH
  · simp [Chebyshev.U_zero]
  · cases' n with n
    · simp
      ring_nf
    · have := Chebyshev_U_recursion (n + 2) (by omega)
      simp at this ⊢

/-- lemma: U_n(-1) = (-1)^n (n+1).-/
lemma Chebyshev.U_eval_neg_one (n : ℕ) :
    (Chebyshev.U ℝ n).eval (-1) = (-1 : ℝ) ^ n * (n + 1 : ℝ) := by
  induction' n using Nat.strong_induction_on with n IH
  rcases n with (rfl|rfl|m)
  · simp  -- n = 0
  · simp   -- n = 1
    ring_nf
  · -- n = m + 2, where m : ℕ
    have : m + 2 = (m + 1) + 1 := by omega
    rw [<-this]
    have hm1 : m < m + 2 := by omega
    have hm2 : m + 1 < m + 2 := by omega
    have rec_eq := Chebyshev.U_add_two ℝ (m)
    simp only at rec_eq ⊢
    have IH_m1 := IH (m + 1) hm2
    have eval_rec_eq : (Chebyshev.U ℝ (m + 2)).eval (-1) =
                      (2 * X * Chebyshev.U ℝ (m + 1) - Chebyshev.U ℝ m).eval (-1) := by
      rw [rec_eq]
    have cast_eq1 : (U ℝ (m + 2) : Polynomial ℝ) = U ℝ (↑(m + 2) : ℕ) := by simp
    have cast_eq2 : (U ℝ (m + 1) : Polynomial ℝ) = U ℝ (↑(m + 1) : ℕ) := by simp
    have cast_eq3 : (U ℝ m : Polynomial ℝ) = U ℝ (↑m : ℕ) := by simp
    rw [← cast_eq1]
    rw [rec_eq]
    simp only [eval_sub, eval_mul, eval_ofNat, eval_X]
    rw [IH m hm1]
    rw [cast_eq2]
    rw [IH (m + 1) hm2]
    calc
      2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * ((m + 1 : ℕ) + 1 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ))
        = 2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * (m + 2 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ)) := by
        simp
        ring_nf
      _ = 2 * (-1) * ((-1) * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * (1 * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * ((-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = (-1) ^ m * (2*(m + 2) - (m + 1)) := by ring
      _ = (-1) ^ m * (m + 3) := by ring
      _ = (-1) ^ m * (-1)^2 * (m + 3) := by norm_num
      _ = (-1) ^ (m + 2) * (m + 3) := by ring
      _ = (-1 : ℝ) ^ (m + 2) * (((m + 2 : ℕ) : ℝ) + 1) := by simp; ring_nf

theorem Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
  intro hx
  -- Use the fact that Chebyshev polynomials have simple roots in (-1,1)
  have comp_eval : ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = (Chebyshev.U ℝ n).eval ((1/2 : ℝ) * x) := by
    simp [Polynomial.eval_comp, Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_X]

  rw [comp_eval] at hx

  have : ∃ (θ : ℝ), x = 2 * Real.cos θ ∧ Real.sin ((n + 1 : ℝ) * θ) = 0 := by
    by_cases h : x^2 ≤ 4
    · let θ := Real.arccos (x/2)
      have hθ1 : -1 ≤ x/2 ∧ x/2 ≤ 1 := by
        constructor <;> sorry
      have hθ2 : Real.cos θ = x/2 := Real.cos_arccos hθ1.1 hθ1.2
      refine ⟨θ, by field_simp [hθ2], ?_⟩
      have := Chebyshev.U_real_cos θ n

      have : Real.sin θ ≠ 0 := by
        intro hsin
        have : x^2 = 4 := by
          have := Real.sin_sq_add_cos_sq θ
          rw [hsin, hθ2] at this
          nlinarith
        sorry
      field_simp [this] at hx
      sorry
    · exfalso
      have bound : ∀ (n : ℕ) (x : ℝ), |x| > 1 → (Chebyshev.U ℝ n).eval x ≠ 0 := by
        intro k y hy
        induction' k using Nat.strong_induction_on with k IH
        rcases k with (rfl|rfl|m)
        · simp [Chebyshev.U_zero]
        · simp
          sorry
        · have rec_eq := Chebyshev.U_add_two ℝ m
          simp [rec_eq, Polynomial.eval_sub, Polynomial.eval_mul, Polynomial.eval_X, Polynomial.eval_C] at *
          intro h
          have : 2 * y * (Chebyshev.U ℝ (m + 1)).eval y = (Chebyshev.U ℝ m).eval y := by sorry --seems wrong???
          have h1 : |2 * y * (Chebyshev.U ℝ (m + 1)).eval y| > |(Chebyshev.U ℝ m).eval y| := by
            have hy_pos : |y| > 0 := by
              have : y ≠ 0 := by
                intro hy0
                have : |y| = 0 := by rw [hy0]; norm_num
                linarith [hy]
              exact abs_pos.mpr this
            sorry
          sorry
      have : |x/2| > 1 := by
        rw [abs_div, abs_two]
        sorry
      sorry

  rcases this with ⟨θ, hx_eq, hsin⟩
  rw [hx_eq]

  have deriv_comp : ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative =
                   Polynomial.C ((n + 1 : ℝ) / 2) * (Chebyshev.U ℝ (n - 1)).comp (Polynomial.C (1/2) * X) := by
    induction' n using Nat.strong_induction_on with k IH
    rcases k with (rfl|rfl|m)
    · simp
    · simp
      by_eval
    · simp only [Nat.cast_add, Nat.cast_one, one_div, add_sub_cancel_right]
      sorry

  rw [deriv_comp, Polynomial.eval_mul, Polynomial.eval_C]

  have hn_pos : (n + 1 : ℝ) / 2 ≠ 0 := by
    intro h
    have : n + 1 = 0 := by sorry
    omega

  refine mul_ne_zero (by exact hn_pos) ?_

  simp [Polynomial.eval_comp, Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_X]

  have : Real.sin ((n + 1 : ℝ) * θ) = 0 := hsin
  have : ∃ (k : ℤ), (n + 1 : ℝ) * θ = π * k := by
    sorry

  rcases this with ⟨k, hk⟩
  have : θ = (π * k) / (n + 1) := by
    field_simp
    linarith [hk]

  have U_eval : (Chebyshev.U ℝ (n - 1)).eval (Real.cos (π * k / (n + 1))) =
               Real.sin (n * (π * k / (n + 1))) / Real.sin (π * k / (n + 1)) := by
    sorry

  sorry
  /-have : ∀ k : ℕ, k < n → ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval (Real.cos (Real.pi * (k + 1) / (n + 1))) ≠ 0 := by
    sorry  -- Would need to compute the derivative explicitly

  -- Show that x must be of the form cos(π*(k+1)/(n+1)) for some k
  have : ∃ k : ℕ, k < n ∧ x = Real.cos (Real.pi * (k + 1) / (n + 1)) := by
    set θ := Real.arccos (x/2) with hθ
    have hUθ := Chebyshev.U_real_cos θ n
    rw [Polynomial.eval_comp, Polynomial.eval_mul, Polynomial.eval_C,
        Polynomial.eval_X] at hx
    have hsinNθ : Real.sin ((n+1) * θ) = 0 := by
      sorry
    obtain ⟨k, hk⟩ := Real.sin_eq_zero_iff.1 hsinNθ
    sorry

  rcases this with ⟨k, _, hx⟩
  rw [hx]
  exact this k ‹k < n›-/

[Nick_adfor]

Ilmārs Cīrulis said:

Did you manage to finish your proof?

lemma Chebyshev.U_eval_neg_one and lemma Chebyshev.U_eval_one is not used. Maybe I do not remember the reason why I write these two lemma : (

[Nick_adfor]

Now I try to have one way (with sorry, containing two lemmas)

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

macro "by_eval" : tactic => `(tactic| (
  apply Polynomial.funext
  intro x
  simp only [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast, eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
  ring
))

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  intro n hn
  exact Chebyshev.U_eq ℝ ↑n

lemma Chebyshev_U_eval_one (n : ℕ) : (Chebyshev.U ℝ n).eval (1 : ℝ) = (n + 1 : ℝ) := by
  induction' n with n IH
  · simp [Chebyshev.U_zero]
  · cases' n with n
    · simp
      ring_nf
    · have := Chebyshev_U_recursion (n + 2) (by omega)
      simp at this ⊢

/-- lemma: U_n(-1) = (-1)^n (n+1).-/
lemma Chebyshev.U_eval_neg_one (n : ℕ) :
    (Chebyshev.U ℝ n).eval (-1) = (-1 : ℝ) ^ n * (n + 1 : ℝ) := by
  induction' n using Nat.strong_induction_on with n IH
  rcases n with (rfl|rfl|m)
  · simp  -- n = 0
  · simp   -- n = 1
    ring_nf
  · -- n = m + 2, where m : ℕ
    have : m + 2 = (m + 1) + 1 := by omega
    rw [<-this]
    have hm1 : m < m + 2 := by omega
    have hm2 : m + 1 < m + 2 := by omega
    have rec_eq := Chebyshev.U_add_two ℝ (m)
    simp only at rec_eq ⊢
    have IH_m1 := IH (m + 1) hm2
    have eval_rec_eq : (Chebyshev.U ℝ (m + 2)).eval (-1) =
                      (2 * X * Chebyshev.U ℝ (m + 1) - Chebyshev.U ℝ m).eval (-1) := by
      rw [rec_eq]
    have cast_eq1 : (U ℝ (m + 2) : Polynomial ℝ) = U ℝ (↑(m + 2) : ℕ) := by simp
    have cast_eq2 : (U ℝ (m + 1) : Polynomial ℝ) = U ℝ (↑(m + 1) : ℕ) := by simp
    have cast_eq3 : (U ℝ m : Polynomial ℝ) = U ℝ (↑m : ℕ) := by simp
    rw [← cast_eq1]
    rw [rec_eq]
    simp only [eval_sub, eval_mul, eval_ofNat, eval_X]
    rw [IH m hm1]
    rw [cast_eq2]
    rw [IH (m + 1) hm2]
    calc
      2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * ((m + 1 : ℕ) + 1 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ))
        = 2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * (m + 2 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ)) := by
        simp
        ring_nf
      _ = 2 * (-1) * ((-1) * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * (1 * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * ((-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = (-1) ^ m * (2*(m + 2) - (m + 1)) := by ring
      _ = (-1) ^ m * (m + 3) := by ring
      _ = (-1) ^ m * (-1)^2 * (m + 3) := by norm_num
      _ = (-1) ^ (m + 2) * (m + 3) := by ring
      _ = (-1 : ℝ) ^ (m + 2) * (((m + 2 : ℕ) : ℝ) + 1) := by simp; ring_nf

theorem Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
  intro hx
  have U_at_1 := Chebyshev_U_eval_one n
  have U_at_neg1 := Chebyshev.U_eval_neg_one n
  have endpoints_nonzero : n > 0 →
      ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval 2 ≠ 0 ∧
      ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval (-2) ≠ 0 := by
    intro hn
    constructor
    · simp
      linarith [show (0 : ℝ) < n + 1 from by exact_mod_cast Nat.succ_pos n]
    · simp
      exact Nat.cast_add_one_ne_zero n
  have root_in_open_interval : x^2 < 4 := by
    by_cases h : n = 0
    · subst h
      simp at hx ⊢
    · have hn : n > 0 := Nat.pos_of_ne_zero h
      have ⟨h1, h2⟩ := endpoints_nonzero hn
      by_contra! H
      have : x ≤ -2 ∨ x ≥ 2 := by
        by_cases h : x ≥ 0
        · right
          nlinarith [H]
        · left
          have : x ≤ 0 := by linarith
          nlinarith [H]
      rcases this with (hx' | hx')
      · have : (1/2 : ℝ) * x ≤ -1 := by linarith
        have mono : ∀ (y : ℝ), y ≤ -1 → (Chebyshev.U ℝ n).eval y ≠ 0 := by
          intro y hy
          rw [show y = -(-y) by ring] at hy ⊢
          have : -y ≥ 1 := by linarith
          have U_neg : (Chebyshev.U ℝ n).eval (-y) = (-1)^n * (Chebyshev.U ℝ n).eval y := by
            induction' n with k IH
            · simp
            · rcases k with (rfl|k)
              · simp
              · have rec_eq := Chebyshev_U_recursion (k + 2) (by omega)
                rw [rec_eq]
                simp
                rw [show (-1 : ℝ) ^ (k + 2) = (-1)^2 * (-1)^k by ring, show (-1 : ℝ)^2 = 1 by norm_num]
                ring_nf
                sorry
          have : (Chebyshev.U ℝ n).eval 1 = n + 1 := U_at_1
          have pos : 0 < (Chebyshev.U ℝ n).eval 1 := by sorry
          intro H
          sorry
        simp [Polynomial.eval_comp, eval_mul, eval_C, eval_X] at hx
        sorry
      · have : (1/2 : ℝ) * x ≥ 1 := by linarith
        have : ∀ (y : ℝ), y ≥ 1 → (Chebyshev.U ℝ n).eval y ≠ 0 := by
          intro y hy
          have pos : 0 < (Chebyshev.U ℝ n).eval y := by
            induction' n with k IH
            · simp [Chebyshev.U_zero]
            · rcases k with (rfl|k)
              · simp [Chebyshev.U_one, hy]
                sorry
              · have rec_eq := Chebyshev_U_recursion (k + 2) (by omega)
                rw [rec_eq]
                simp [eval_sub, eval_mul, eval_X, eval_C, eval_ofNat]
                sorry
          exact ne_of_gt pos
        simp at hx
        exact this ((2⁻¹ : ℝ) * x) (by linarith) hx
  have : ∃ (θ : ℝ), x = 2 * Real.cos θ := by
    have : -1 ≤ x/2 ∧ x/2 ≤ 1 := by
      constructor <;> sorry
    exact ⟨Real.arccos (x/2), by rw [Real.cos_arccos this.1 this.2]; ring⟩

  rcases this with ⟨θ, hx_eq⟩
  rw [hx_eq]

  have deriv_formula : ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative =
                     Polynomial.C ((n + 1 : ℝ) / 2) * (Chebyshev.U ℝ (n - 1)).comp (Polynomial.C (1/2) * X) := by
    sorry

  rw [deriv_formula, Polynomial.eval_mul, Polynomial.eval_C]

  refine mul_ne_zero (by norm_num; exact Nat.cast_add_one_ne_zero n) ?_
  simp [Polynomial.eval_comp, eval_mul, eval_C, eval_X]

  have : (Chebyshev.U ℝ (n - 1)).eval (cos θ) ≠ 0 := by
    intro H
    have U_prev_at_1 : (Chebyshev.U ℝ (n - 1)).eval (1 : ℝ) = n := by
      by_cases h : n = 0
      · subst h; simp [Chebyshev.U_zero]
      · have := Chebyshev_U_eval_one (n - 1)
        simp at this ⊢
    have U_prev_at_neg1 : (Chebyshev.U ℝ (n - 1)).eval (-1 : ℝ) = (-1)^(n - 1) * n := by
      by_cases h : n = 0
      · subst h; simp [Chebyshev.U_zero]
      · have := Chebyshev.U_eval_neg_one (n - 1)
        simp at this ⊢
        sorry
    sorry
  exact this

  /-have : ∀ k : ℕ, k < n → ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval (Real.cos (Real.pi * (k + 1) / (n + 1))) ≠ 0 := by
    sorry  -- Would need to compute the derivative explicitly

  -- Show that x must be of the form cos(π*(k+1)/(n+1)) for some k
  have : ∃ k : ℕ, k < n ∧ x = Real.cos (Real.pi * (k + 1) / (n + 1)) := by
    set θ := Real.arccos (x/2) with hθ
    have hUθ := Chebyshev.U_real_cos θ n
    rw [Polynomial.eval_comp, Polynomial.eval_mul, Polynomial.eval_C,
        Polynomial.eval_X] at hx
    have hsinNθ : Real.sin ((n+1) * θ) = 0 := by
      sorry
    obtain ⟨k, hk⟩ := Real.sin_eq_zero_iff.1 hsinNθ
    sorry

  rcases this with ⟨k, _, hx⟩
  rw [hx]
  exact this k ‹k < n›-/

[Nick_adfor]

Ilmārs Cīrulis said:

Did you manage to finish your proof?

You seem full of passion and able to offer some help, thank you so much!

[Ilmārs Cīrulis]

Are you talking about me? :sweat_smile: I'm no help currently because of lack of motivation.

[Nick_adfor]

Ilmārs Cīrulis said:

Are you talking about me? :sweat_smile: I'm no help currently because of lack of motivation.

Your reply seems to be pushing me to finish the proof. Doesn't that mean you already have a good way to complete it?

[Ilmārs Cīrulis]

Not exactly. But I'm glad you are progressing (it seems to me).

[Hagb (Junyu Guo)]

got a few sorries fixed, based on the last version posted

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

macro "by_eval" : tactic => `(tactic| (
  apply Polynomial.funext
  intro x
  simp only [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast, eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
  ring
))

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  intro n hn
  exact Chebyshev.U_eq ℝ ↑n

lemma Chebyshev_U_eval_one (n : ℕ) : (Chebyshev.U ℝ n).eval (1 : ℝ) = (n + 1 : ℝ) := by
  induction' n with n IH
  · simp [Chebyshev.U_zero]
  · cases' n with n
    · simp
      ring_nf
    · have := Chebyshev_U_recursion (n + 2) (by omega)
      simp at this ⊢

/-- lemma: U_n(-1) = (-1)^n (n+1).-/
lemma Chebyshev.U_eval_neg_one (n : ℕ) :
    (Chebyshev.U ℝ n).eval (-1) = (-1 : ℝ) ^ n * (n + 1 : ℝ) := by
  induction' n using Nat.strong_induction_on with n IH
  rcases n with (rfl|rfl|m)
  · simp  -- n = 0
  · simp   -- n = 1
    ring_nf
  · -- n = m + 2, where m : ℕ
    have : m + 2 = (m + 1) + 1 := by omega
    rw [<-this]
    have hm1 : m < m + 2 := by omega
    have hm2 : m + 1 < m + 2 := by omega
    have rec_eq := Chebyshev.U_add_two ℝ (m)
    simp only at rec_eq ⊢
    have IH_m1 := IH (m + 1) hm2
    have eval_rec_eq : (Chebyshev.U ℝ (m + 2)).eval (-1) =
                      (2 * X * Chebyshev.U ℝ (m + 1) - Chebyshev.U ℝ m).eval (-1) := by
      rw [rec_eq]
    have cast_eq1 : (U ℝ (m + 2) : Polynomial ℝ) = U ℝ (↑(m + 2) : ℕ) := by simp
    have cast_eq2 : (U ℝ (m + 1) : Polynomial ℝ) = U ℝ (↑(m + 1) : ℕ) := by simp
    have cast_eq3 : (U ℝ m : Polynomial ℝ) = U ℝ (↑m : ℕ) := by simp
    rw [← cast_eq1]
    rw [rec_eq]
    simp only [eval_sub, eval_mul, eval_ofNat, eval_X]
    rw [IH m hm1]
    rw [cast_eq2]
    rw [IH (m + 1) hm2]
    calc
      2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * ((m + 1 : ℕ) + 1 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ))
        = 2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * (m + 2 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ)) := by
        simp
        ring_nf
      _ = 2 * (-1) * ((-1) * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * (1 * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * ((-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = (-1) ^ m * (2*(m + 2) - (m + 1)) := by ring
      _ = (-1) ^ m * (m + 3) := by ring
      _ = (-1) ^ m * (-1)^2 * (m + 3) := by norm_num
      _ = (-1) ^ (m + 2) * (m + 3) := by ring
      _ = (-1 : ℝ) ^ (m + 2) * (((m + 2 : ℕ) : ℝ) + 1) := by simp; ring_nf

theorem Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
  intro hx
  have U_at_1 := Chebyshev_U_eval_one n
  have U_at_neg1 := Chebyshev.U_eval_neg_one n
  have endpoints_nonzero : n > 0 →
      ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval 2 ≠ 0 ∧
      ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval (-2) ≠ 0 := by
    intro hn
    constructor
    · simp
      linarith [show (0 : ℝ) < n + 1 from by exact_mod_cast Nat.succ_pos n]
    · simp
      exact Nat.cast_add_one_ne_zero n
  have root_in_open_interval : x^2 < 4 := by
    by_cases h : n = 0
    · subst h
      simp at hx ⊢
    · have hn : n > 0 := Nat.pos_of_ne_zero h
      have ⟨h1, h2⟩ := endpoints_nonzero hn
      by_contra! H
      have : x ≤ -2 ∨ x ≥ 2 := by
        by_cases h : x ≥ 0
        · right
          nlinarith [H]
        · left
          have : x ≤ 0 := by linarith
          nlinarith [H]
      rcases this with (hx' | hx')
      · have : (1/2 : ℝ) * x ≤ -1 := by linarith
        have mono : ∀ (y : ℝ), y ≤ -1 → (Chebyshev.U ℝ n).eval y ≠ 0 := by
          intro y hy
          rw [show y = -(-y) by ring] at hy ⊢
          have : -y ≥ 1 := by linarith
          have U_neg : (Chebyshev.U ℝ n).eval (-y) = (-1)^n * (Chebyshev.U ℝ n).eval y := by
            induction' n with k IH
            · simp
            · rcases k with (rfl|k)
              · simp
              · have rec_eq := Chebyshev_U_recursion (k + 2) (by omega)
                rw [rec_eq]
                simp
                rw [show (-1 : ℝ) ^ (k + 2) = (-1)^2 * (-1)^k by ring, show (-1 : ℝ)^2 = 1 by norm_num]
                ring_nf
                sorry
          have : (Chebyshev.U ℝ n).eval 1 = n + 1 := U_at_1
          have pos : 0 < (Chebyshev.U ℝ n).eval 1 := by linarith
          intro H
          simp at H
          simp [H] at U_neg
        simp [Polynomial.eval_comp, eval_mul, eval_C, eval_X] at hx
        sorry
      · have : (1/2 : ℝ) * x ≥ 1 := by linarith
        have : ∀ (y : ℝ), y ≥ 1 → (Chebyshev.U ℝ n).eval y ≠ 0 := by
          intro y hy
          have pos : 0 < (Chebyshev.U ℝ n).eval y := by
            induction' n with k IH
            · simp [Chebyshev.U_zero]
            · rcases k with (rfl|k)
              · simp [Chebyshev.U_one, hy]
                linarith
              · have rec_eq := Chebyshev_U_recursion (k + 2) (by omega)
                rw [rec_eq]
                simp [eval_sub, eval_mul, eval_X, eval_C, eval_ofNat]
                sorry
          exact ne_of_gt pos
        simp at hx
        exact this ((2⁻¹ : ℝ) * x) (by linarith) hx
  have : ∃ (θ : ℝ), x = 2 * Real.cos θ := by
    have : -1 ≤ x/2 ∧ x/2 ≤ 1 := by
      convert_to x * x < 2 * 2 at root_in_open_interval
      · ring
      · ring
      rw [← abs_lt_iff_mul_self_lt, abs_lt, abs_two] at root_in_open_interval
      split_ands <;> linarith
    exact ⟨Real.arccos (x/2), by rw [Real.cos_arccos this.1 this.2]; ring⟩

  rcases this with ⟨θ, hx_eq⟩
  rw [hx_eq]

  have deriv_formula : ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative =
                     Polynomial.C ((n + 1 : ℝ) / 2) * (Chebyshev.U ℝ (n - 1)).comp (Polynomial.C (1/2) * X) := by
    sorry

  rw [deriv_formula, Polynomial.eval_mul, Polynomial.eval_C]

  refine mul_ne_zero (by norm_num; exact Nat.cast_add_one_ne_zero n) ?_
  simp [Polynomial.eval_comp, eval_mul, eval_C, eval_X]

  have : (Chebyshev.U ℝ (n - 1)).eval (cos θ) ≠ 0 := by
    intro H
    have U_prev_at_1 : (Chebyshev.U ℝ (n - 1)).eval (1 : ℝ) = n := by
      by_cases h : n = 0
      · subst h; simp [Chebyshev.U_zero]
      · have := Chebyshev_U_eval_one (n - 1)
        simp at this ⊢
    have U_prev_at_neg1 : (Chebyshev.U ℝ (n - 1)).eval (-1 : ℝ) = (-1)^(n - 1) * n := by
      by_cases h : n = 0
      · subst h; simp [Chebyshev.U_zero]
      · have := Chebyshev.U_eval_neg_one (n - 1)
        simp at this ⊢
        have n_ge_one : n ≥ 1 := Nat.one_le_iff_ne_zero.mpr h
        simpa [n_ge_one]
    sorry
  exact this

  /-have : ∀ k : ℕ, k < n → ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval (Real.cos (Real.pi * (k + 1) / (n + 1))) ≠ 0 := by
    sorry  -- Would need to compute the derivative explicitly

  -- Show that x must be of the form cos(π*(k+1)/(n+1)) for some k
  have : ∃ k : ℕ, k < n ∧ x = Real.cos (Real.pi * (k + 1) / (n + 1)) := by
    set θ := Real.arccos (x/2) with hθ
    have hUθ := Chebyshev.U_real_cos θ n
    rw [Polynomial.eval_comp, Polynomial.eval_mul, Polynomial.eval_C,
        Polynomial.eval_X] at hx
    have hsinNθ : Real.sin ((n+1) * θ) = 0 := by
      sorry
    obtain ⟨k, hk⟩ := Real.sin_eq_zero_iff.1 hsinNθ
    sorry

  rcases this with ⟨k, _, hx⟩
  rw [hx]
  exact this k ‹k < n›-/

[Nick_adfor]

Line 121 lacks a sorry

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

macro "by_eval" : tactic => `(tactic| (
  apply Polynomial.funext
  intro x
  simp only [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast, eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
  ring
))

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  intro n hn
  exact Chebyshev.U_eq ℝ ↑n

lemma Chebyshev_U_eval_one (n : ℕ) : (Chebyshev.U ℝ n).eval (1 : ℝ) = (n + 1 : ℝ) := by
  induction' n with n IH
  · simp [Chebyshev.U_zero]
  · cases' n with n
    · simp
      ring_nf
    · have := Chebyshev_U_recursion (n + 2) (by omega)
      simp at this ⊢

/-- lemma: U_n(-1) = (-1)^n (n+1).-/
lemma Chebyshev.U_eval_neg_one (n : ℕ) :
    (Chebyshev.U ℝ n).eval (-1) = (-1 : ℝ) ^ n * (n + 1 : ℝ) := by
  induction' n using Nat.strong_induction_on with n IH
  rcases n with (rfl|rfl|m)
  · simp  -- n = 0
  · simp   -- n = 1
    ring_nf
  · -- n = m + 2, where m : ℕ
    have : m + 2 = (m + 1) + 1 := by omega
    rw [<-this]
    have hm1 : m < m + 2 := by omega
    have hm2 : m + 1 < m + 2 := by omega
    have rec_eq := Chebyshev.U_add_two ℝ (m)
    simp only at rec_eq ⊢
    have IH_m1 := IH (m + 1) hm2
    have eval_rec_eq : (Chebyshev.U ℝ (m + 2)).eval (-1) =
                      (2 * X * Chebyshev.U ℝ (m + 1) - Chebyshev.U ℝ m).eval (-1) := by
      rw [rec_eq]
    have cast_eq1 : (U ℝ (m + 2) : Polynomial ℝ) = U ℝ (↑(m + 2) : ℕ) := by simp
    have cast_eq2 : (U ℝ (m + 1) : Polynomial ℝ) = U ℝ (↑(m + 1) : ℕ) := by simp
    have cast_eq3 : (U ℝ m : Polynomial ℝ) = U ℝ (↑m : ℕ) := by simp
    rw [← cast_eq1]
    rw [rec_eq]
    simp only [eval_sub, eval_mul, eval_ofNat, eval_X]
    rw [IH m hm1]
    rw [cast_eq2]
    rw [IH (m + 1) hm2]
    calc
      2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * ((m + 1 : ℕ) + 1 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ))
        = 2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * (m + 2 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ)) := by
        simp
        ring_nf
      _ = 2 * (-1) * ((-1) * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * (1 * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * ((-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = (-1) ^ m * (2*(m + 2) - (m + 1)) := by ring
      _ = (-1) ^ m * (m + 3) := by ring
      _ = (-1) ^ m * (-1)^2 * (m + 3) := by norm_num
      _ = (-1) ^ (m + 2) * (m + 3) := by ring
      _ = (-1 : ℝ) ^ (m + 2) * (((m + 2 : ℕ) : ℝ) + 1) := by simp; ring_nf

theorem Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
  intro hx
  have U_at_1 := Chebyshev_U_eval_one n
  have U_at_neg1 := Chebyshev.U_eval_neg_one n
  have endpoints_nonzero : n > 0 →
      ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval 2 ≠ 0 ∧
      ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval (-2) ≠ 0 := by
    intro hn
    constructor
    · simp
      linarith [show (0 : ℝ) < n + 1 from by exact_mod_cast Nat.succ_pos n]
    · simp
      exact Nat.cast_add_one_ne_zero n
  have root_in_open_interval : x^2 < 4 := by
    by_cases h : n = 0
    · subst h
      simp at hx ⊢
    · have hn : n > 0 := Nat.pos_of_ne_zero h
      have ⟨h1, h2⟩ := endpoints_nonzero hn
      by_contra! H
      have : x ≤ -2 ∨ x ≥ 2 := by
        by_cases h : x ≥ 0
        · right
          nlinarith [H]
        · left
          have : x ≤ 0 := by linarith
          nlinarith [H]
      rcases this with (hx' | hx')
      · have : (1/2 : ℝ) * x ≤ -1 := by linarith
        have mono : ∀ (y : ℝ), y ≤ -1 → (Chebyshev.U ℝ n).eval y ≠ 0 := by
          intro y hy
          rw [show y = -(-y) by ring] at hy ⊢
          have : -y ≥ 1 := by linarith
          have U_neg : (Chebyshev.U ℝ n).eval (-y) = (-1)^n * (Chebyshev.U ℝ n).eval y := by
            induction' n with k IH
            · simp
            · rcases k with (rfl|k)
              · simp
              · have rec_eq := Chebyshev_U_recursion (k + 2) (by omega)
                rw [rec_eq]
                simp
                rw [show (-1 : ℝ) ^ (k + 2) = (-1)^2 * (-1)^k by ring, show (-1 : ℝ)^2 = 1 by norm_num]
                ring_nf
                sorry
          have : (Chebyshev.U ℝ n).eval 1 = n + 1 := U_at_1
          have pos : 0 < (Chebyshev.U ℝ n).eval 1 := by linarith
          intro H
          simp at H
          simp [H] at U_neg
          sorry
        simp [Polynomial.eval_comp, eval_mul, eval_C, eval_X] at hx
        sorry
      · have : (1/2 : ℝ) * x ≥ 1 := by linarith
        have : ∀ (y : ℝ), y ≥ 1 → (Chebyshev.U ℝ n).eval y ≠ 0 := by
          intro y hy
          have pos : 0 < (Chebyshev.U ℝ n).eval y := by
            induction' n with k IH
            · simp [Chebyshev.U_zero]
            · rcases k with (rfl|k)
              · simp [Chebyshev.U_one, hy]
                linarith
              · have rec_eq := Chebyshev_U_recursion (k + 2) (by omega)
                rw [rec_eq]
                simp [eval_sub, eval_mul, eval_X, eval_C, eval_ofNat]
                sorry
          exact ne_of_gt pos
        simp at hx
        exact this ((2⁻¹ : ℝ) * x) (by linarith) hx
  have : ∃ (θ : ℝ), x = 2 * Real.cos θ := by
    have : -1 ≤ x/2 ∧ x/2 ≤ 1 := by
      convert_to x * x < 2 * 2 at root_in_open_interval
      · ring
      · ring
      rw [← abs_lt_iff_mul_self_lt, abs_lt, abs_two] at root_in_open_interval
      split_ands <;> linarith
    exact ⟨Real.arccos (x/2), by rw [Real.cos_arccos this.1 this.2]; ring⟩

  rcases this with ⟨θ, hx_eq⟩
  rw [hx_eq]

  have deriv_formula : ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative =
                     Polynomial.C ((n + 1 : ℝ) / 2) * (Chebyshev.U ℝ (n - 1)).comp (Polynomial.C (1/2) * X) := by
    sorry

  rw [deriv_formula, Polynomial.eval_mul, Polynomial.eval_C]

  refine mul_ne_zero (by norm_num; exact Nat.cast_add_one_ne_zero n) ?_
  simp [Polynomial.eval_comp, eval_mul, eval_C, eval_X]

  have : (Chebyshev.U ℝ (n - 1)).eval (cos θ) ≠ 0 := by
    intro H
    have U_prev_at_1 : (Chebyshev.U ℝ (n - 1)).eval (1 : ℝ) = n := by
      by_cases h : n = 0
      · subst h; simp [Chebyshev.U_zero]
      · have := Chebyshev_U_eval_one (n - 1)
        simp at this ⊢
    have U_prev_at_neg1 : (Chebyshev.U ℝ (n - 1)).eval (-1 : ℝ) = (-1)^(n - 1) * n := by
      by_cases h : n = 0
      · subst h; simp [Chebyshev.U_zero]
      · have := Chebyshev.U_eval_neg_one (n - 1)
        simp at this ⊢
        have n_ge_one : n ≥ 1 := Nat.one_le_iff_ne_zero.mpr h
        simpa [n_ge_one]
    sorry
  exact this

  /-have : ∀ k : ℕ, k < n → ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval (Real.cos (Real.pi * (k + 1) / (n + 1))) ≠ 0 := by
    sorry  -- Would need to compute the derivative explicitly

  -- Show that x must be of the form cos(π*(k+1)/(n+1)) for some k
  have : ∃ k : ℕ, k < n ∧ x = Real.cos (Real.pi * (k + 1) / (n + 1)) := by
    set θ := Real.arccos (x/2) with hθ
    have hUθ := Chebyshev.U_real_cos θ n
    rw [Polynomial.eval_comp, Polynomial.eval_mul, Polynomial.eval_C,
        Polynomial.eval_X] at hx
    have hsinNθ : Real.sin ((n+1) * θ) = 0 := by
      sorry
    obtain ⟨k, hk⟩ := Real.sin_eq_zero_iff.1 hsinNθ
    sorry

  rcases this with ⟨k, _, hx⟩
  rw [hx]
  exact this k ‹k < n›-/

[Nick_adfor]

This part seems to need a tactic like by_eval?... But I'm not so familiar with the library about .comp.

  have deriv_formula : ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative =
                     Polynomial.C ((n + 1 : ℝ) / 2) * (Chebyshev.U ℝ (n - 1)).comp (Polynomial.C (1/2) * X) := by
    sorry

[Jireh Loreaux]

Here's a computation of the roots of the Chebyshev polynomials of the second kind and that they all have multiplicity one.

import Mathlib.Algebra.Polynomial.Roots
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev
import Mathlib.Tactic.ComputeDegree

namespace Polynomial
namespace Chebyshev

variable (R : Type*) [CommRing R]

lemma degree_U_neg_one : (U R (-1)).degree = ⊥ := by
  simp [U_neg_one]

lemma degree_U_zero [Nontrivial R] : (U R 0).degree = 0 := by
  simp [U_zero]

lemma degree_U_ofNat [IsDomain R] (h : ringChar R ≠ 2) : (n : ℕ) → (U R n).degree = n
  | 0 => degree_U_zero R
  | 1 => by
    simp [U_one]
    have : degree (2 : R[X]) = 0 := by
      compute_degree
      exact Ring.two_ne_zero h
    simp [this]
  | n + 2 => by
    simp only [Nat.cast_add, Nat.cast_ofNat, U_add_two]
    have : degree (2 * X * U R (n + 1)) = n + 2 := by
      have h₂ : degree (2 * X : R[X]) = 1 := by
        compute_degree
        · exact Ring.two_ne_zero h
        · simp
      have this : (U R (n + 1)).degree = n + 1 := degree_U_ofNat h (n + 1)
      rw [degree_mul, this, add_comm, h₂]
      rfl
    rwa [degree_sub_eq_left_of_degree_lt]
    rw [this]
    rw [degree_U_ofNat h n]
    exact Order.lt_succ _ |>.trans <| Order.lt_succ _

open Real

lemma nodups (n : ℕ) :
    (Multiset.map (fun k : ℕ ↦ cos ((k + 1) * π / (n + 1))) (.range n)).Nodup := by
  refine (Finset.range n).nodup_map_iff_injOn.mpr ?_
  cases n with
  | zero => simp
  | succ n =>
    intro x hx y hy h
    simp at hx hy h
    replace h := injOn_cos ⟨?h₁, ?h₂⟩ ⟨?h₃, ?h₄⟩ h
    field_simp at h
    simpa using h
    case h₁ => positivity
    case h₃ => positivity
    all_goals
      rw [mul_div_right_comm]
      apply le_of_lt
      calc
        _ / (n + 1 + 1) * π < (n + 1 + 1) / (n + 1 + 1) * π := by gcongr; norm_cast
        _ = π := by field_simp

lemma roots_U_real (n : ℕ) :
    (U ℝ n).roots = Multiset.map (fun k : ℕ ↦ cos ((k + 1) * π / (n + 1))) (.range n):= by
  cases n with
  | zero => simp
  | succ n =>
    have : (U ℝ (n + 1)).roots.card ≤ n + 1 := by
      convert card_roots' _
      exact Eq.symm <| natDegree_eq_of_degree_eq_some <| degree_U_ofNat ℝ (by simp) (n + 1)
    apply Eq.symm <| Multiset.eq_of_le_of_card_le ?_ (by simpa)
    rw [Multiset.le_iff_count]
    intro x
    simp only [count_roots]
    rw [Multiset.count_eq_of_nodup (nodups (n + 1))]
    split_ifs with h
    · change 0 < _
      simp
      refine ⟨ne_zero_of_degree_gt (n := 0) ?_, ?_⟩
      · calc
          (0 : WithBot ℕ) < n + 1 := by positivity
          _ = (U ℝ (n + 1)).degree := degree_U_ofNat ℝ (by simp) (n + 1) |>.symm
      · simp only [Nat.cast_add, Nat.cast_one, Multiset.mem_map, Multiset.mem_range] at h
        obtain ⟨k, hk, rfl⟩ := h
        have : 0 < sin ((k + 1) * π / (n + 1 + 1)) := by
          apply sin_pos_of_mem_Ioo ⟨by positivity, ?_⟩
          calc
            _ < (n + 1 + 1 : ℝ) * π / (n + 1 + 1) := by gcongr; norm_cast
            _ = π := by field_simp
        rw [← mul_right_cancel_iff_of_pos this, zero_mul, U_real_cos]
        norm_cast
        field_simp
        exact sin_nat_mul_pi (k + 1)
    · simp

lemma rootMultiplicity_U_real {n : ℕ} {k : ℕ} (hk : k < n) :
    (U ℝ n).rootMultiplicity (cos ((k + 1) * π / (n + 1))) = 1 := by
  rw [← count_roots, roots_U_real]
  refine Multiset.count_eq_one_of_mem (nodups n) ?_
  simpa using ⟨k, hk, rfl⟩

end Chebyshev
end Polynomial

[Jireh Loreaux]

It's likely possible to simplify the above code a bit, but I think this is the natural argument. That is, "here are n distinct roots of this polynomial of degree n, so they all have multiplicity 1."

[Nick_adfor]

It seems that I should not choose derivative to finish the proof. (But later in Oct. 15th I find this part gives me more thoughts about developing API for scaleRoots.

[Nick_adfor]

Now this.

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

macro "by_eval" : tactic => `(tactic| (
  apply Polynomial.funext
  intro x
  simp only [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast, eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
  ring
))

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  intro n hn
  exact Chebyshev.U_eq ℝ ↑n

lemma Chebyshev_U_eval_one (n : ℕ) : (Chebyshev.U ℝ n).eval (1 : ℝ) = (n + 1 : ℝ) := by
  induction' n with n IH
  · simp [Chebyshev.U_zero]
  · cases' n with n
    · simp
      ring_nf
    · have := Chebyshev_U_recursion (n + 2) (by omega)
      simp at this ⊢

/-- lemma: U_n(-1) = (-1)^n (n+1).-/
lemma Chebyshev.U_eval_neg_one (n : ℕ) :
    (Chebyshev.U ℝ n).eval (-1) = (-1 : ℝ) ^ n * (n + 1 : ℝ) := by
  induction' n using Nat.strong_induction_on with n IH
  rcases n with (rfl|rfl|m)
  · simp  -- n = 0
  · simp   -- n = 1
    ring_nf
  · -- n = m + 2, where m : ℕ
    have : m + 2 = (m + 1) + 1 := by omega
    rw [<-this]
    have hm1 : m < m + 2 := by omega
    have hm2 : m + 1 < m + 2 := by omega
    have rec_eq := Chebyshev.U_add_two ℝ (m)
    simp only at rec_eq ⊢
    have IH_m1 := IH (m + 1) hm2
    have eval_rec_eq : (Chebyshev.U ℝ (m + 2)).eval (-1) =
                      (2 * X * Chebyshev.U ℝ (m + 1) - Chebyshev.U ℝ m).eval (-1) := by
      rw [rec_eq]
    have cast_eq1 : (U ℝ (m + 2) : Polynomial ℝ) = U ℝ (↑(m + 2) : ℕ) := by simp
    have cast_eq2 : (U ℝ (m + 1) : Polynomial ℝ) = U ℝ (↑(m + 1) : ℕ) := by simp
    have cast_eq3 : (U ℝ m : Polynomial ℝ) = U ℝ (↑m : ℕ) := by simp
    rw [← cast_eq1]
    rw [rec_eq]
    simp only [eval_sub, eval_mul, eval_ofNat, eval_X]
    rw [IH m hm1]
    rw [cast_eq2]
    rw [IH (m + 1) hm2]
    calc
      2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * ((m + 1 : ℕ) + 1 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ))
        = 2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * (m + 2 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ)) := by
        simp
        ring_nf
      _ = 2 * (-1) * ((-1) * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * (1 * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * ((-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = (-1) ^ m * (2*(m + 2) - (m + 1)) := by ring
      _ = (-1) ^ m * (m + 3) := by ring
      _ = (-1) ^ m * (-1)^2 * (m + 3) := by norm_num
      _ = (-1) ^ (m + 2) * (m + 3) := by ring
      _ = (-1 : ℝ) ^ (m + 2) * (((m + 2 : ℕ) : ℝ) + 1) := by simp; ring_nf

lemma Chebyshev.U_neg (n : ℕ) (x : ℝ) :
    (U ℝ n).eval (-x) = (-1 : ℝ)^n * (U ℝ n).eval x := by
  induction' n using Nat.strong_induction_on with n ih
  rcases n with (rfl|rfl|m)
  · -- n = 0
    simp
  · -- n = 1
    simp
  · -- n = m + 2
    have eval_rec : (U ℝ (m + 2)).eval (-x) =
                    2 * (-x) * (U ℝ (m + 1)).eval (-x) - (U ℝ m).eval (-x) := by
                      rw [ih m (Nat.le.step Nat.le.refl)]
                      simp
                      have h2 := ih m (by omega)
                      rw [h2]
    calc
      (U ℝ (m + 2)).eval (-x)
          = 2 * (-x) * (U ℝ (m + 1)).eval (-x) - (U ℝ m).eval (-x) := by rw [eval_rec]
      _ = 2 * (-x) * ((-1 : ℝ)^(m + 1) * (U ℝ (m + 1)).eval x)
            - ((-1 : ℝ)^m * (U ℝ m).eval x) := by
            norm_num
            ring_nf
            rw [ih m (Nat.le.step Nat.le.refl)]
            ring_nf
            simp
            calc
              -(x * eval (-x) (U ℝ (1 + m)) * 2)
                  = -(x * ((-1)^(m+1) * eval x (U ℝ (m+1))) * 2) := by
                    congr 1
                    congr 1
                    congr 1
                    ring_nf
                    have h_eq : eval (-x) (U ℝ (1 + ↑m)) = -(eval x (U ℝ (1 + ↑m)) * (-1)^m) := by
                      calc
                        eval (-x) (U ℝ (1 + ↑m))
                            = eval (-x) (U ℝ ↑(m+1)) := by simp; ring_nf
                        _   = (-1)^(m+1) * eval x (U ℝ ↑(m+1)) := by rw [ih (m + 1) Nat.le.refl]
                        _   = (-1)^m * (-1) * eval x (U ℝ (1+↑m)) := by ring_nf; simp
                        _   = -(eval x (U ℝ (1+↑m)) * (-1)^m) := by ring
                    exact h_eq
              _ = x * eval x (U ℝ (m+1)) * (-1)^m * 2 := by
                    rw [pow_succ]
                    ring
            rw [Int.add_comm]
      _ = (-1 : ℝ)^m * (2 * x * (U ℝ (m + 1)).eval x - (U ℝ m).eval x) := by ring
      _ = (-1 : ℝ)^m * (U ℝ (m + 2)).eval x := by simp
      _ = (-1 : ℝ)^(m + 2) * (U ℝ (m + 2)).eval x := by
        norm_num
        ring_nf
        exact (true_or (x * eval x (U ℝ (1 + ↑m)) * 2 - eval x (U ℝ ↑m) = 0)).mpr trivial


theorem Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
  intro hx
  have U_at_1 := Chebyshev_U_eval_one n
  have U_at_neg1 := Chebyshev.U_eval_neg_one n
  have endpoints_nonzero : n > 0 →
      ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval 2 ≠ 0 ∧
      ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval (-2) ≠ 0 := by
    intro hn
    constructor
    · simp
      linarith [show (0 : ℝ) < n + 1 from by exact_mod_cast Nat.succ_pos n]
    · simp
      exact Nat.cast_add_one_ne_zero n
  have root_in_open_interval : x^2 < 4 := by
    by_cases h : n = 0
    · subst h
      simp at hx ⊢
    · have hn : n > 0 := Nat.pos_of_ne_zero h
      have ⟨h1, h2⟩ := endpoints_nonzero hn
      by_contra! H
      have : x ≤ -2 ∨ x ≥ 2 := by
        by_cases h : x ≥ 0
        · right
          nlinarith [H]
        · left
          have : x ≤ 0 := by linarith
          nlinarith [H]
      rcases this with (hx' | hx')
      · have : (1/2 : ℝ) * x ≤ -1 := by linarith
        have mono : ∀ (y : ℝ), y ≤ -1 → (Chebyshev.U ℝ n).eval y ≠ 0 := by
          intro y hy
          rw [show y = -(-y) by ring] at hy ⊢
          have : -y ≥ 1 := by linarith
          have U_neg : (Chebyshev.U ℝ n).eval (-y) = (-1)^n * (Chebyshev.U ℝ n).eval y := by exact Chebyshev.U_neg n y
          have : (Chebyshev.U ℝ n).eval 1 = n + 1 := U_at_1
          have pos : 0 < (Chebyshev.U ℝ n).eval 1 := by linarith
          intro H
          simp at H
          simp [H] at U_neg
          sorry
        simp [Polynomial.eval_comp, eval_mul, eval_C, eval_X] at hx
        sorry
      · have : (1/2 : ℝ) * x ≥ 1 := by linarith
        have : ∀ (y : ℝ), y ≥ 1 → (Chebyshev.U ℝ n).eval y ≠ 0 := by
          intro y hy
          have pos : 0 < (Chebyshev.U ℝ n).eval y := by
            induction' n with k IH
            · simp [Chebyshev.U_zero]
            · rcases k with (rfl|k)
              · simp [Chebyshev.U_one, hy]
                linarith
              · have rec_eq := Chebyshev_U_recursion (k + 2) (by omega)
                rw [rec_eq]
                simp [eval_sub, eval_mul, eval_X, eval_C, eval_ofNat]
                sorry
          exact ne_of_gt pos
        simp at hx
        exact this ((2⁻¹ : ℝ) * x) (by linarith) hx
  have : ∃ (θ : ℝ), x = 2 * Real.cos θ := by
    have : -1 ≤ x/2 ∧ x/2 ≤ 1 := by
      convert_to x * x < 2 * 2 at root_in_open_interval
      · ring
      · ring
      rw [← abs_lt_iff_mul_self_lt, abs_lt, abs_two] at root_in_open_interval
      split_ands <;> linarith
    exact ⟨Real.arccos (x/2), by rw [Real.cos_arccos this.1 this.2]; ring⟩

  rcases this with ⟨θ, hx_eq⟩
  rw [hx_eq]

  have deriv_formula : ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative =
                     Polynomial.C ((n + 1 : ℝ) / 2) * (Chebyshev.U ℝ (n - 1)).comp (Polynomial.C (1/2) * X) := by
    sorry

  rw [deriv_formula, Polynomial.eval_mul, Polynomial.eval_C]

  refine mul_ne_zero (by norm_num; exact Nat.cast_add_one_ne_zero n) ?_
  simp [Polynomial.eval_comp, eval_mul, eval_C, eval_X]

  have : (Chebyshev.U ℝ (n - 1)).eval (cos θ) ≠ 0 := by
    intro H
    have U_prev_at_1 : (Chebyshev.U ℝ (n - 1)).eval (1 : ℝ) = n := by
      by_cases h : n = 0
      · subst h; simp [Chebyshev.U_zero]
      · have := Chebyshev_U_eval_one (n - 1)
        simp at this ⊢
    have U_prev_at_neg1 : (Chebyshev.U ℝ (n - 1)).eval (-1 : ℝ) = (-1)^(n - 1) * n := by
      by_cases h : n = 0
      · subst h; simp [Chebyshev.U_zero]
      · have := Chebyshev.U_eval_neg_one (n - 1)
        simp at this ⊢
        have n_ge_one : n ≥ 1 := Nat.one_le_iff_ne_zero.mpr h
        simpa [n_ge_one]
    sorry
  exact this

[Nick_adfor]

(deleted)

[Nick_adfor]

I extract some of the code as Chebyshev.U_pos_of_ge_one, leaving a lot of sorry.

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  intro n hn
  exact Chebyshev.U_eq ℝ ↑n


lemma Chebyshev.U_pos_of_ge_one {n : ℕ} {y : ℝ} (hy : 1 ≤ y) :
    0 < (U ℝ n).eval y := by
  induction' n using Nat.strong_induction_on with n IH
  rcases n with (rfl | rfl | m)
  · simp
  · simp [U_one]
    linarith [hy]
  · have rec := Chebyshev_U_recursion (m+2) (by omega)
    simp [eval_sub, eval_mul, eval_X, eval_C, eval_ofNat] at rec
    have IH_m   := IH m (by omega)
    have IH_m1  := IH (m + 1) (by omega)
    calc
      (U ℝ (m+2)).eval y
          = (2 * y) * (U ℝ (m+1)).eval y - (U ℝ m).eval y := by
          rw [rec]
          simp
          ring_nf
          exact (true_or (y = 0)).mpr trivial
      _ > (U ℝ (m+1)).eval y - (U ℝ m).eval y := by
          have h2y : 2 * y ≥ 2 := by linarith
          simp
          ring_nf
          sorry
      _ > 0 := by
          have : (U ℝ (m+1)).eval y > (U ℝ m).eval y := by
            rcases m with _ | m
            · simp [U_zero, U_one, eval_X]
              linarith [hy]
            · have rec' := Chebyshev_U_recursion (m+1) (by simp; sorry)
              simp [eval_sub, eval_mul, eval_X, eval_C, eval_ofNat] at rec'
              have IH_m := IH m (by omega)
              have IH_m_sub1 := IH (m-1) (by omega)
              have : (U ℝ (m+1)).eval y = 2 * y * (U ℝ m).eval y - (U ℝ (m-1)).eval y := by
                rw [rec']
                simp [eval_sub, eval_mul, eval_X, eval_C]
                ring_nf
              have h2y : 2 * y ≥ 2 := by linarith
              have : (U ℝ m).eval y > (U ℝ (m-1)).eval y := by
                rcases m with _ | m
                · simp
                · have : (U ℝ (m+1)).eval y > (U ℝ m).eval y := by
                    have rec'' := Chebyshev_U_recursion (m+1) (by sorry)
                    simp [eval_sub, eval_mul, eval_X, eval_C, eval_ofNat] at rec''
                    have IH_m := IH m (by omega)
                    have IH_m_sub1 := IH (m-1) (by omega)
                    have h2y : 2 * y > 1 := by linarith [hy]
                    sorry
                  simp
                  exact this
              sorry
          nlinarith

[Nick_adfor]

I cannot understand the topic : (

[Nick_adfor]

Now I extract some of the code as Chebyshev.U_pos_of_ge_one, leaving a lot of sorry (in my origin post)

[Nick_adfor]

Now the code writes like this:

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

set_option maxHeartbeats 1000000

lemma Chebyshev_U_recursion :
  ∀ n : ℕ, n ≥ 2 → Chebyshev.U ℝ n = 2 * X * Chebyshev.U ℝ (n-1) - Chebyshev.U ℝ (n-2) := by
  intro n hn
  exact Chebyshev.U_eq ℝ ↑n


lemma Chebyshev.U_pos_of_ge_one {n : ℕ} {y : ℝ} (hy : 1 ≤ y) :
    0 < (U ℝ n).eval y := by
  induction' n using Nat.strong_induction_on with n IH
  rcases n with (rfl | rfl | m)
  · simp
  · simp [U_one]
    linarith [hy]
  · have rec := Chebyshev_U_recursion (m+2) (by omega)
    simp [eval_sub, eval_mul, eval_X, eval_C, eval_ofNat] at rec
    have IH_m   := IH m (by omega)
    have IH_m1  := IH (m + 1) (by omega)
    calc
      (U ℝ (m+2)).eval y
          = (2 * y) * (U ℝ (m+1)).eval y - (U ℝ m).eval y := by
          rw [rec]
          simp
          ring_nf
          exact (true_or (y = 0)).mpr trivial
      _ > (U ℝ (m+1)).eval y - (U ℝ m).eval y := by
          have h2y : 2 * y ≥ 2 := by linarith
          simp
          ring_nf
          sorry
      _ > 0 := by
          have : (U ℝ (m+1)).eval y > (U ℝ m).eval y := by
            rcases m with _ | m
            · simp [U_zero, U_one, eval_X]
              linarith [hy]
            · have rec' := Chebyshev_U_recursion (m+1) (by simp; sorry)
              simp [eval_sub, eval_mul, eval_X, eval_C, eval_ofNat] at rec'
              have IH_m := IH m (by omega)
              have IH_m_sub1 := IH (m-1) (by omega)
              have : (U ℝ (m+1)).eval y = 2 * y * (U ℝ m).eval y - (U ℝ (m-1)).eval y := by
                rw [rec']
                simp [eval_sub, eval_mul, eval_X, eval_C]
                ring_nf
              have h2y : 2 * y ≥ 2 := by linarith
              have : (U ℝ m).eval y > (U ℝ (m-1)).eval y := by
                rcases m with _ | m
                · simp
                · have : (U ℝ (m+1)).eval y > (U ℝ m).eval y := by
                    have rec'' := Chebyshev_U_recursion (m+1) (by sorry)
                    simp [eval_sub, eval_mul, eval_X, eval_C, eval_ofNat] at rec''
                    have IH_m := IH m (by omega)
                    have IH_m_sub1 := IH (m-1) (by omega)
                    have h2y : 2 * y > 1 := by linarith [hy]
                    sorry
                  simp
                  exact this
              sorry
          nlinarith


lemma Chebyshev_U_eval_one (n : ℕ) : (Chebyshev.U ℝ n).eval (1 : ℝ) = (n + 1 : ℝ) := by
  induction' n with n IH
  · simp
  · cases' n with n
    · simp
      ring_nf
    · simp

/-- lemma: U_n(-1) = (-1)^n (n+1).-/
lemma Chebyshev.U_eval_neg_one (n : ℕ) :
    (Chebyshev.U ℝ n).eval (-1) = (-1 : ℝ) ^ n * (n + 1 : ℝ) := by
  induction' n using Nat.strong_induction_on with n IH
  rcases n with (rfl|rfl|m)
  · simp  -- n = 0
  · simp   -- n = 1
    ring_nf
  · -- n = m + 2, where m : ℕ
    have : m + 2 = (m + 1) + 1 := by omega
    rw [<-this]
    have hm1 : m < m + 2 := by omega
    have hm2 : m + 1 < m + 2 := by omega
    have rec_eq := Chebyshev.U_add_two ℝ (m)
    simp only at rec_eq ⊢
    have eval_rec_eq : (Chebyshev.U ℝ (m + 2)).eval (-1) =
                      (2 * X * Chebyshev.U ℝ (m + 1) - Chebyshev.U ℝ m).eval (-1) := by
      rw [rec_eq]
    have cast_eq1 : (U ℝ (m + 2) : Polynomial ℝ) = U ℝ (↑(m + 2) : ℕ) := by simp
    have cast_eq2 : (U ℝ (m + 1) : Polynomial ℝ) = U ℝ (↑(m + 1) : ℕ) := by simp
    have cast_eq3 : (U ℝ m : Polynomial ℝ) = U ℝ (↑m : ℕ) := by simp
    rw [← cast_eq1]
    rw [rec_eq]
    simp only [eval_sub, eval_mul, eval_ofNat, eval_X]
    rw [IH m hm1]
    rw [cast_eq2]
    rw [IH (m + 1) hm2]
    calc
      2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * ((m + 1 : ℕ) + 1 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ))
        = 2 * (-1 : ℝ) * ((-1 : ℝ) ^ (m + 1) * (m + 2 : ℝ)) - ((-1 : ℝ) ^ m * (m + 1 : ℝ)) := by
        simp
        ring_nf
      _ = 2 * (-1) * ((-1) * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * (1 * (-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = 2 * ((-1) ^ m * (m + 2)) - ((-1) ^ m * (m + 1)) := by ring
      _ = (-1) ^ m * (2*(m + 2) - (m + 1)) := by ring
      _ = (-1) ^ m * (m + 3) := by ring
      _ = (-1) ^ m * (-1)^2 * (m + 3) := by norm_num
      _ = (-1) ^ (m + 2) * (m + 3) := by ring
      _ = (-1 : ℝ) ^ (m + 2) * (((m + 2 : ℕ) : ℝ) + 1) := by simp; ring_nf

lemma Chebyshev.U_neg (n : ℕ) (x : ℝ) :
    (U ℝ n).eval (-x) = (-1 : ℝ)^n * (U ℝ n).eval x := by
  induction' n using Nat.strong_induction_on with n ih
  rcases n with (rfl|rfl|m)
  · -- n = 0
    simp
  · -- n = 1
    simp
  · -- n = m + 2
    have eval_rec : (U ℝ (m + 2)).eval (-x) =
                    2 * (-x) * (U ℝ (m + 1)).eval (-x) - (U ℝ m).eval (-x) := by
                      rw [ih m (Nat.le.step Nat.le.refl)]
                      simp
                      have h2 := ih m (by omega)
                      rw [h2]
    calc
      (U ℝ (m + 2)).eval (-x)
          = 2 * (-x) * (U ℝ (m + 1)).eval (-x) - (U ℝ m).eval (-x) := by rw [eval_rec]
      _ = 2 * (-x) * ((-1 : ℝ)^(m + 1) * (U ℝ (m + 1)).eval x)
            - ((-1 : ℝ)^m * (U ℝ m).eval x) := by
            norm_num
            ring_nf
            rw [ih m (Nat.le.step Nat.le.refl)]
            ring_nf
            simp
            calc
              -(x * eval (-x) (U ℝ (1 + m)) * 2)
                  = -(x * ((-1)^(m+1) * eval x (U ℝ (m+1))) * 2) := by
                    congr 1
                    congr 1
                    congr 1
                    ring_nf
                    have h_eq : eval (-x) (U ℝ (1 + ↑m)) = -(eval x (U ℝ (1 + ↑m)) * (-1)^m) := by
                      calc
                        eval (-x) (U ℝ (1 + ↑m))
                            = eval (-x) (U ℝ ↑(m+1)) := by simp; ring_nf
                        _   = (-1)^(m+1) * eval x (U ℝ ↑(m+1)) := by rw [ih (m + 1) Nat.le.refl]
                        _   = (-1)^m * (-1) * eval x (U ℝ (1+↑m)) := by ring_nf; simp
                        _   = -(eval x (U ℝ (1+↑m)) * (-1)^m) := by ring
                    exact h_eq
              _ = x * eval x (U ℝ (m+1)) * (-1)^m * 2 := by
                    rw [pow_succ]
                    ring
            rw [Int.add_comm]
      _ = (-1 : ℝ)^m * (2 * x * (U ℝ (m + 1)).eval x - (U ℝ m).eval x) := by ring
      _ = (-1 : ℝ)^m * (U ℝ (m + 2)).eval x := by simp
      _ = (-1 : ℝ)^(m + 2) * (U ℝ (m + 2)).eval x := by
        norm_num
        ring_nf
        exact (true_or (x * eval x (U ℝ (1 + ↑m)) * 2 - eval x (U ℝ ↑m) = 0)).mpr trivial




theorem Chebyshev_U_simple_roots (n : ℕ) (x : ℝ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by
  intro hx
  have U_at_1 := Chebyshev_U_eval_one n
  have U_at_neg1 := Chebyshev.U_eval_neg_one n
  have endpoints_nonzero : n > 0 →
      ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval 2 ≠ 0 ∧
      ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval (-2) ≠ 0 := by
    intro hn
    constructor
    · simp
      linarith [show (0 : ℝ) < n + 1 from by exact_mod_cast Nat.succ_pos n]
    · simp
      exact Nat.cast_add_one_ne_zero n
  have root_in_open_interval : x^2 < 4 := by
    by_cases h : n = 0
    · subst h
      simp at hx ⊢
    · have hn : n > 0 := Nat.pos_of_ne_zero h
      have ⟨h1, h2⟩ := endpoints_nonzero hn
      by_contra! H
      have : x ≤ -2 ∨ x ≥ 2 := by
        by_cases h : x ≥ 0
        · right
          nlinarith [H]
        · left
          have : x ≤ 0 := by linarith
          nlinarith [H]
      rcases this with (hx' | hx')
      · sorry

      · have : ∀ (y : ℝ), y ≥ 1 → (Chebyshev.U ℝ n).eval y ≠ 0 := by
          intro y hy
          have pos : 0 < (Chebyshev.U ℝ n).eval y := by exact Chebyshev.U_pos_of_ge_one hy
          exact ne_of_gt pos
        simp at hx
        exact this ((2⁻¹ : ℝ) * x) (by linarith) hx
  have : ∃ (θ : ℝ), x = 2 * Real.cos θ := by
    have : -1 ≤ x/2 ∧ x/2 ≤ 1 := by
      convert_to x * x < 2 * 2 at root_in_open_interval
      · ring
      · ring
      rw [← abs_lt_iff_mul_self_lt, abs_lt, abs_two] at root_in_open_interval
      split_ands <;> linarith
    exact ⟨Real.arccos (x/2), by rw [Real.cos_arccos this.1 this.2]; ring⟩

  rcases this with ⟨θ, hx_eq⟩
  rw [hx_eq]

  have deriv_formula : ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative =
                     Polynomial.C ((n + 1 : ℝ) / 2) * (Chebyshev.U ℝ (n - 1)).comp (Polynomial.C (1/2) * X) := by
    sorry

  rw [deriv_formula, Polynomial.eval_mul, Polynomial.eval_C]

  refine mul_ne_zero (by norm_num; exact Nat.cast_add_one_ne_zero n) ?_
  simp [Polynomial.eval_comp, eval_mul, eval_C, eval_X]

  have : (Chebyshev.U ℝ (n - 1)).eval (cos θ) ≠ 0 := by
    intro H
    have U_prev_at_1 : (Chebyshev.U ℝ (n - 1)).eval (1 : ℝ) = n := by
      by_cases h : n = 0
      · subst h; simp
      · have := Chebyshev_U_eval_one (n - 1)
        simp at this ⊢
    have U_prev_at_neg1 : (Chebyshev.U ℝ (n - 1)).eval (-1 : ℝ) = (-1)^(n - 1) * n := by
      by_cases h : n = 0
      · subst h; simp
      · have := Chebyshev.U_eval_neg_one (n - 1)
        simp at this ⊢
        have n_ge_one : n ≥ 1 := Nat.one_le_iff_ne_zero.mpr h
        simpa [n_ge_one]
    have h₀ : (Chebyshev.U ℝ n).eval (cos θ) = 0 := by
      simp [hx_eq] at hx
      exact hx
    have h₁ : (Chebyshev.U ℝ (n - 1)).eval (cos θ) = 0 := H
    have : ∀ m, m ≤ n → (Chebyshev.U ℝ (n - m)).eval (cos θ) = 0 := by sorry
  exact this

--#lint docBlameThm

[Notification Bot]

3 messages were moved here from #general > Computable polynomial representation based on sorted list by Eric Wieser.

[Eric Wieser]

@Nick_adfor , please don't double post. If you want to draw attention in one thread to a problem you have in another, I recommend linking between the threads instead

[Nick_adfor]

Eric Wieser said:

Nick_adfor , please don't double post. If you want to draw attention in one thread to a problem you have in another, I recommend linking between the threads instead

@Eric Wieser , please do not remove code from the post. Some of them are from my historical versions. How do I version back if you remove them?

[Eric Wieser]

I did not remove anything, I just moved your messages between the threads:

Notification Bot said:

3 messages were moved here from #general > Computable polynomial representation based on sorted list by Eric Wieser.

[Nick_adfor]

I've finished the part Chebyshev_U_scaled_deriv_ne_zero(417 lines) so I just admit here. For the main theorem, I want to use Chebyshev_U_scaled_deriv_ne_zero to prove the scaled polynomial is separable, then transfer this property to the original Chebyshev polynomial via root scaling relationship.

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

/-- Derivative at roots of scaled Chebyshev polynomials is nonzero.-/
lemma Chebyshev_U_scaled_deriv_ne_zero (n : ℕ) (x : ℝ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by admit
-- I've finished the `admit` part, but it's very long （417 lines）. So I just `admit` here.

/-- All roots of Chebyshev polynomials of the second kind are simple. -/
theorem Chebyshev_U_roots_simple (n : ℕ) :
    (Polynomial.roots (Chebyshev.U ℝ n)).Nodup := by
  have root_scaling : Polynomial.roots (Chebyshev.U ℝ n) =
         (Polynomial.roots ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X))).map (· * 2) := by
    sorry
  rw [root_scaling]
  apply Multiset.Nodup.map
  · -- Multiplication by 2 is injective
    intro a b h
    sorry
  · -- Scaled polynomial has simple roots
    have h_separable : Polynomial.Separable ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)) := by
      rw [Polynomial.separable_iff_derivative_ne_zero]
      intro h
      -- If derivative is zero polynomial, find contradiction
      by_cases hn : n = 0
      · subst hn; sorry
      · -- Chebyshev polynomials have roots (e.g., use intermediate value theorem)
        have : ∃ x : ℝ, ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 := by
          sorry
        rcases this with ⟨x, hx⟩
        have := Chebyshev_U_scaled_deriv_ne_zero n x hx
        rw [h] at this
        simp at this
      have irreducible : Irreducible ((U ℝ ↑n).comp (Polynomial.C (1 / 2) * X)) := by sorry
      exact irreducible
    exact nodup_roots h_separable

[Jireh Loreaux]

Nick, I already proved this for you in another thread? See #new members > Chebyshev polynomial @ 💬 . Why are you continuing with this exactly?

[Nick_adfor]

This is classic programmer humor :-) I'm basically reinventing the wheel, but all in the name of creating more APIs.

[Notification Bot]

3 messages were moved here from #mathlib4 > Prove that Chebyshev_U_roots_simple by Kevin Buzzard.

[Jireh Loreaux]

Nick, I don't really consider it humorous that you're asking people to duplicate work that's already been done, especially without reference to the prior work, as this can influence whether someone wants to put forth the effort to help you or not. Notice that Kevin merged the threads. I've noticed you have several threads about Chebyshev polynomials floating around, and some of those were merged as well. It's generally in bad taste on Zulip to ask virtually the same question multiple times in different places.

If you want to create more API, go for it, but that doesn't really seem to be what you're doing here. From what I can tell, you're proving very specific facts about Chebyshev polynomials, and you're not choosing to use the API that does already exist.

[Nick_adfor]

Okay Jireh, your instant help is appreciated. But I have to say that my whole work is to solve a whole problem (long lemmas and theorems), so check all API is really needed. The problem is as follows:

Problem 1: Prove the recurrence relation for the characteristic polynomial
Let the matrix A(n) be an n × n real matrix with elements defined as:
A(n)ij =
0, if | i - j | > 1
1, if | i - j | = 1
0, otherwise
This means A(n) is a tridiagonal matrix with 0 on the main diagonal and 1 on the sub- and super-diagonals.
Let pₙ(X) = charpoly(A(n)) = det(XIₙ - A(n)). We need to prove:
pₙ(X) = X ⋅ pₙ₋₁(X) - pₙ₋₂(X), for n ≥ 2

Problem 2: Prove that all roots of the second kind Chebyshev polynomial Uₙ(x) are real and simple

Problem 3: Prove that all eigenvalues of matrix A(n) are real and distinct

[Nick_adfor]

As you can see here, now we are working on problem 2 and you give a splendid proof. But I should have good way to use problem 2 to finish proving problem 3. So I do need some work on scaled Chebyshev polynomial. In the process of Chebyshev_U_scaled_deriv_ne_zero, I leave some lemma (I may call them API) suitable for scaled ones.

[Jireh Loreaux]

So for this, you shouldn't be asking about Chebyshev polynomials. You should ask the more general question: if p : R[X] is a polynomial, how are its roots related to those of p.comp (C a * X) for a : R? And in your case R := ℝ and a := 1 / 2.

The approach I think you should likely take here is to develop API for docs#Polynomial.scaleRoots. It is not quite the case that the characteristic polynomial of your matrix is a scaleRoots version of the Chebyshev polynomial, but it should be after multiplying by a suitable constant (in particular, I think the characteristic polynomial of your matrix is C (2 ^ (-n : ℤ)) * ((U ℝ n).scaleRoots 2)). So you should prove a fact relating the docs#Polynomial.rootMultiplicity of the scaled root of docs#Polynomial.scaleRoots to the root multiplicity of the original root of the polynomial. This should be possible using docs#IsUnit.scaleRoots_dvd_iff and docs#Polynomial.le_rootMultiplicity_iff and docs#Polynomial.rootMultiplicity_le_iff. From there you can get the appropriate statement relating the roots of the two polynomials.

[Jireh Loreaux]

Basically, if p is a polynomial of degree n in R[X] and a : Rˣ, then p.comp (C (a⁻¹) * X) = C (a ^ (-n : ℤ)) * p.scaleRoots a.

[Nick_adfor]

This would be a great extension, translating my specific situations into abstract ones.

[Jireh Loreaux]

Glad you agree. I suggest you write it.

[Nick_adfor]

These are the finished part. admit means that I have finished them. Now I try to get some of them expanded, also develop API for scaleRoots.

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

/-- Non-vanishing at endpoints for scaled Chebyshev polynomials.
For any natural number n, Uₙ(1) ≠ 0 and Uₙ(-1) ≠ 0. -/
lemma endpoints_nonzero (n : ℕ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval 2 ≠ 0 ∧
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval (-2) ≠ 0 := by admit

/-- Parity property of Chebyshev polynomials.
For any natural number n and real number x, Uₙ(-x) = (-1)ⁿUₙ(x). -/
lemma Chebyshev.U_neg (n : ℕ) (x : ℝ) :
    (U ℝ n).eval (-x) = (-1 : ℝ) ^ n * (U ℝ n).eval x := by admit

/-- Cosine representation theorem for real numbers in a symmetric interval.
For any a > 0 and real number x with |x| ≤ a, there exists θ such that x = a cos θ. -/
lemma exists_cos_representation_general (x a : ℝ) (ha : a > 0) (h : |x| ≤ a) :
    ∃ (θ : ℝ), x = a * Real.cos θ := by
  -- Show that x / a is in the domain of arccos [-1, 1]
  have bound : -1 ≤ x / a ∧ x / a ≤ 1 := by admit

/-- Cosine representation theorem for real numbers in the interval (-2, 2).-/
lemma exists_cos_representation (x : ℝ) (h : x ^ 2 < 4) : ∃ (θ : ℝ), x = 2 * Real.cos θ := by admit

/-- Positivity of Chebyshev polynomials of the second kind on [1, ∞).-/
lemma Chebyshev.U_pos_of_ge_one {n : ℕ} {y : ℝ} (hy : 1 ≤ y) :
    0 < (U ℝ n).eval y := by admit

/-- Derivative of the composition U_n(cos θ) using the chain rule.-/
lemma deriv_chebyshev_U_compose_cos (n : ℕ) (θ : ℝ) :
    deriv (fun t => (Chebyshev.U ℝ n).eval (Real.cos t)) θ =
    (Polynomial.derivative (Chebyshev.U ℝ n)).eval (Real.cos θ) * (-Real.sin θ) := by admit

/-- Roots of scaled Chebyshev polynomials lie in the open interval (-2, 2). -/
lemma root_in_open_interval (n : ℕ) (x : ℝ)
    (hx : ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0) :
    x ^ 2 < 4 := by admit

/-- Evaluation of Chebyshev polynomials at x = 1.
For any natural number n, Uₙ(1) = n + 1. -/
lemma Chebyshev_U_eval_one (n : ℕ) : (Chebyshev.U ℝ n).eval (1 : ℝ) = (n + 1 : ℝ) := by admit

/-- Evaluation of Chebyshev polynomials at x = -1.
For any natural number n, Uₙ(-1) = (-1)ⁿ(n + 1). -/
lemma Chebyshev.U_eval_neg_one (n : ℕ) :
    (Chebyshev.U ℝ n).eval (-1) = (-1 : ℝ) ^ n * (n + 1 : ℝ) := by admit

/-- Analysis of roots of scaled Chebyshev polynomials of the second kind.

If `((U ℝ n).comp (C (1/2) * X)).eval x = 0`, then there exists an angle `θ` such that:
- `x = 2 * cos θ` (cosine representation)
- `Uₙ(cos θ) = 0` (Chebyshev polynomial vanishes at cos θ)
- `sin((n+1)θ) = 0` (trigonometric identity consequence)
- `sin θ ≠ 0` (non-degeneracy condition)
- The derivative satisfies a specific formula:
  `Uₙ'(cos θ) = -(n+1)cos((n+1)θ)/sin²θ`

This provides a complete characterization of roots in terms of trigonometric functions. -/
lemma chebyshev_root_analysis (n : ℕ) (x : ℝ)
    (hx : ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0) :
    ∃ (θ : ℝ),
      x = 2 * Real.cos θ ∧
      (Chebyshev.U ℝ n).eval (Real.cos θ) = 0 ∧
      Real.sin ((n + 1 : ℝ) * θ) = 0 ∧
      Real.sin θ ≠ 0 ∧
      (Polynomial.derivative (Chebyshev.U ℝ n)).eval (Real.cos θ) =
      - (n + 1 : ℝ) * Real.cos ((n + 1) * θ) / (Real.sin θ) ^ 2 := by admit

/-- Derivative at roots of scaled Chebyshev polynomials is nonzero.-/
theorem Chebyshev_U_scaled_deriv_ne_zero (n : ℕ) (x : ℝ) :
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).eval x = 0 →
    ((Chebyshev.U ℝ n).comp (Polynomial.C (1/2) * X)).derivative.eval x ≠ 0 := by admit

[Nick_adfor]

Jireh Loreaux said:

It's likely possible to simplify the above code a bit, but I think this is the natural argument. That is, "here are n distinct roots of this polynomial of degree n, so they all have multiplicity 1."

I’m going to simplify this later.

[Nick_adfor]

Jireh Loreaux said:

Nick, I already proved this for you in another thread? See #new members > Chebyshev polynomial @ 💬 . Why are you continuing with this exactly?

Sir, I spent some time searching for my memory of the reason why I do not use your method. It is that in your code

lemma nodups (n : ℕ) :
    (Multiset.map (fun k : ℕ ↦ cos ((k + 1) * π / (n + 1))) (.range n)).Nodup := by
  refine (Finset.range n).nodup_map_iff_injOn.mpr ?_

This part cannot work on v4.16.0. It gives an error

function expected at
  Finset.nodup_map_iff_injOn
term has type
  (Multiset.map ?m.32354 (Finset.val ?m.32355)).Nodup ↔ Set.InjOn ?m.32354 ↑?m.32355Lean 4
Finset.nodup_map_iff_injOn.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α → β} {s : Finset α} :
  (Multiset.map f s.val).Nodup ↔ Set.InjOn f ↑s

which I cannot find how to fix. It seems that the error is not about lacking a theorem in the latest version, but about some auto proof.

[Ruben Van de Velde]

Why are you using 4.16?

[Nick_adfor]

4.16 is the version of leansearch.net so to build this search engine every code must be able to run in 4.16 (rather than the latest version)

[Kenny Lau]

why do you have to use leansearch

[Nick_adfor]

I am in the team of leansearch.net

[Nick_adfor]

As this is a year-long (and potentially longer) team project, we need to standardize on a version for training the search engine to ensure the entire team is aligned.

[Nick_adfor]

This means that as more contributors build upon Mathlib beyond v4.16.0, the wider the compatibility gap with our search engine grows. This, in turn, reduces the engine's ability to make newer code discoverable. Striking a balance is challenging, which is why assistance from communities like Zulip becomes vital. However, a key problem remains: porting code from the latest version back to our old engine base often requires significant additional work.

[Nick_adfor]

Like now I really have problem with Jireh Loreaux's nodup

[Kevin Buzzard]

Thanks a lot for explaining the background, it makes things a lot clearer! I am still a bit confused about the relationship between LeanSearch (a natural language search engine) and your goal to prove new theorems about Chebyshev polynomials (which seems to have nothing to do with search engines per se).

I think that in practice you are going to find it quite difficult to find people in this community who are going to answer questions of the form "how do I get this working in v4.16".

[Nick_adfor]

It is a great honor, Professor. This problem on Chebyshev polynomials is being used as a dataset to enhance the LeanSearch engine's understanding of version v4.16.0.

I have sought help from the Zulip community regarding these problems, while being fully aware that the solutions provided there are likely based on much newer versions rather than v4.16.0. Whether the code runs successfully is somewhat a matter of luck, and subsequent adjustments are often necessary. That said, I do need to address the question raised here: "If the proof of this theorem is already complete, why write another version?" In reality, the final refinements will still be carried out by me independently — yet every bit of assistance is warmly welcomed and deeply appreciated.

[Jireh Loreaux]

Tip: don't backport code to train on 4.16. Retrain the existing model on the current version. If you don't, your results will be lost to oblivion and won't be interesting anyway as they will already be nine months (or much more!) out of date. If you can't update the model every few months quickly and efficiently, then that's the first problem to solve.

[Jireh Loreaux]

Kevin Buzzard said:

I think that in practice you are going to find it quite difficult to find people in this community who are going to answer questions of the form "how do I get this working in v4.16".

Indeed, I don't have time to waste backporting code to train AI, so I'll be disengaging now.

[Nick_adfor]

Jireh Loreaux said:

Tip: don't backport code to train on 4.16. Retrain the existing model on the current version.

We are facing a time constraint. The fact that a perfect search engine remains elusive nine months after the release of v4.16.0 suggests that we may have to treat the development of Mathlib and the search engine as mutually exclusive priorities.

[Nick_adfor]

But in fact if familiar with both the latest and the old version, we can write code suitable for both the versions. Its just different technique team doing different things and there's nothing terrible.

[Kim Morrison]

I think the lesson from this is that you need a fundamental rethink of your search engine design --- i.e. the lesson is that that current design is a failure, not that you should be spending effort backporting material.

[Kim Morrison]

And I'd request please not dragging others into the time-wasting activity of backporting to ancient versions. (i.e. by asking for assistance for such...)

[Nick_adfor]

Kim Morrison said:

And I'd request please not dragging others into the time-wasting activity of backporting to ancient versions. (i.e. by asking for assistance for such...)

I'll incorporate further updates based on the suggestions here. Yet I must emphasize that all the questions and answers are built on the latest version. If anything isn't compatible with an earlier one, I'll handle the extra work myself. Honestly, these are just some leftover tasks from earlier. Going forward, these theorem about Chebyshev Polynomials will be updated with more integrated tactics by myself into Mathlib, using a much more effective approach.