Problem on possibility of Chebyshev Polynomial

Stream: mathlib4

[Nick_adfor]

This should be easy for math, but I have trouble to formalize it in lean.

import Mathlib

open Polynomial Real
open Polynomial
open Chebyshev

/-- 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
  induction' n using Nat.strong_induction_on with n IH
  rcases n with (rfl | rfl | m)
  · -- Case n = 0
    simp
  · -- Case n = 1
    simp
    linarith [hy]
  · -- Case n = m + 2
    -- Get recursion relation for Chebyshev polynomials
    have rec := Chebyshev_U_recursion (m+2) (by omega)
    simp at rec
    -- Inductive hypotheses for m and m+1
    have IH_m   := IH m (by omega)
    -- Inductive hypotheses for m and m+1
    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
          -- Calculation
          have h2y : 2 * y ≥ 2 := by linarith
          simp
          -- Calculation
          have pos : 0 < eval y (U ℝ (↑m + 1)) := by
            exact IH_m1
          nlinarith [pos, h2y]
      _ > 0 := by
                -- Use the recurrence relation for U_{m+1}
                have recurrence_m1 : (U ℝ (m + 1)).eval y = 2 * y * (U ℝ m).eval y - (U ℝ (m - 1)).eval y := by
                  have h : U ℝ (m + 1) = 2 * X * U ℝ m - U ℝ (m - 1) := by exact U_add_one ℝ ↑m
                  rw [h]
                  simp [mul_add, add_mul]

                -- Rewrite the difference
                have diff_eq : (U ℝ (m + 1)).eval y - (U ℝ m).eval y =
                    (2 * y - 1) * (U ℝ m).eval y - (U ℝ (m - 1)).eval y := by
                  rw [recurrence_m1]
                  ring
                rw [diff_eq]

                -- Since y ≥ 1, we have 2y - 1 ≥ 1
                have two_y_minus_one_ge_one : 1 ≤ 2 * y - 1 := by nlinarith

                -- Prove U_m(y) > U_{m-1}(y) using a separate induction
                have strict_monotonic : (U ℝ (m - 1)).eval y < (U ℝ m).eval y := by
                  -- Base case: when m = 1, compare U₀(y) = 1 and U₁(y) = 2y
                  -- Since y ≥ 1, 2y ≥ 2 > 1
                  rcases m with _ | _ | k
                  · simp
                  · -- m = 1: U₀(y) = 1 < 2y = U₁(y) for y > 1
                    simp
                    nlinarith [hy]
                  · -- m = k + 2 (k ≥ 0)
                    -- We need to show: U_{k+1}(y) < U_{k+2}(y)
                    have recurrence_k2 : (U ℝ (k + 2)).eval y = 2 * y * (U ℝ (k + 1)).eval y - (U ℝ k).eval y := by
                      have h : U ℝ (k + 2) = 2 * X * U ℝ (k + 1) - U ℝ k := Chebyshev.U_add_two ℝ k
                      rw [h]
                      simp [mul_add, add_mul]

                    -- By induction hypothesis, we know U_{k+1}(y) > U_k(y)
                    have IH_strict : (U ℝ k).eval y < (U ℝ (k + 1)).eval y := by
                      sorry
                    have diff_k : (U ℝ (k + 2)).eval y - (U ℝ (k + 1)).eval y =
                        (2 * y - 1) * (U ℝ (k + 1)).eval y - (U ℝ k).eval y := by
                      rw [recurrence_k2]
                      ring
                    have goal_eq : (U ℝ (↑(k + 1 + 1) - 1)).eval y = (U ℝ (k + 1)).eval y := by
                      simp
                    rw [goal_eq]
                    have rec_eq_k2 : (U ℝ ↑(k + 1 + 1)).eval y = 2 * y * (U ℝ (k + 1)).eval y - (U ℝ k).eval y := by
                      rw [← recurrence_k2]
                      exact rfl
                    rw [rec_eq_k2]
                    have pos_k1 : 0 < (U ℝ (k + 1)).eval y := IH (k + 1) (by omega)
                    nlinarith
                nlinarith [two_y_minus_one_ge_one, IH_m, strict_monotonic]

[Yury G. Kudryashov]

You post some code without visible sorrys. What's your question?

[Weiyi Wang]

The code failed to compile very earily on at

have rec := Chebyshev_U_recursion (m+2) (by omega)

and as there isn't Chebyshev_U_recursion in the library, I don't know exact what you intend to do. Is this generated by AI without you reading through the code?

[Yury G. Kudryashov]

Who wrote this code?

[Yury G. Kudryashov]

Aristotle https://aristotle.harmonic.fun/ solves it in <3m:

import Mathlib

/-- Positivity of Chebyshev polynomials of the second kind on [1, ∞).-/
lemma Chebyshev.U_pos_of_ge_one {n : ℕ} {y : ℝ} (hy : 1 ≤ y) :
    0 < (Polynomial.Chebyshev.U ℝ n).eval y := by
  have h_poly_pos_step : ∀ n : ℕ, ∀ y : ℝ, 1 ≤ y → 0 < Polynomial.eval y (Polynomial.Chebyshev.U ℝ n) ∧ Polynomial.eval y (Polynomial.Chebyshev.U ℝ (n + 1)) > Polynomial.eval y (Polynomial.Chebyshev.U ℝ n) := by
    intros n y hy; induction n <;> aesop;
    · linarith;
    · linarith;
    · norm_num [ add_assoc ] at * ; nlinarith;
  exact h_poly_pos_step n y hy |>.1

[Nick_adfor]

Yury G. Kudryashov said:

You post some code without visible sorrys. What's your question?

The question is to solve the sorry.

[Nick_adfor]

Weiyi Wang said:

The code failed to compile very earily on at

have rec := Chebyshev_U_recursion (m+2) (by omega)

and as there isn't Chebyshev_U_recursion in the library, I don't know exact what you intend to do. Is this generated by AI without you reading through the code?

No. As I'm writing code on v4.16.0, some change of name in mathlib will result in error just like you have mentioned here if you use latest version. By the way, AI like ChatGPT uses earlier version or even lean 3 so its error will be more complicated. But name change is truly one reason.

[Kevin Buzzard]

Nick_adfor said:

Yury G. Kudryashov said:

You post some code without visible sorrys. What's your question?

The question is to solve the sorry.

My question is: what sorry are you talking about in that sentence?

[Nick_adfor]

Kevin Buzzard said:

Nick_adfor said:

Yury G. Kudryashov said:

You post some code without visible sorrys. What's your question?

The question is to solve the sorry.

My question is: what sorry are you talking about in that sentence?

The sorry is

have IH_strict : (U ℝ k).eval y < (U ℝ (k + 1)).eval y := by
                      sorry

[Nick_adfor]

Yury G. Kudryashov said:

Aristotle https://aristotle.harmonic.fun/ solves it in <3m:

import Mathlib

/-- Positivity of Chebyshev polynomials of the second kind on [1, ∞).-/
lemma Chebyshev.U_pos_of_ge_one {n : ℕ} {y : ℝ} (hy : 1 ≤ y) :
    0 < (Polynomial.Chebyshev.U ℝ n).eval y := by
  have h_poly_pos_step : ∀ n : ℕ, ∀ y : ℝ, 1 ≤ y → 0 < Polynomial.eval y (Polynomial.Chebyshev.U ℝ n) ∧ Polynomial.eval y (Polynomial.Chebyshev.U ℝ (n + 1)) > Polynomial.eval y (Polynomial.Chebyshev.U ℝ n) := by
    intros n y hy; induction n <;> aesop;
    · linarith;
    · linarith;
    · norm_num [ add_assoc ] at * ; nlinarith;
  exact h_poly_pos_step n y hy |>.1

Well, aesop: failed to prove the goal after exhaustive search. Seems that Aristotle does not pass down the wisdom of the Philosopher.

[Lawrence Wu (llllvvuu)]

that’s just a warning, it doesn’t stop the proof from going through

[Lawrence Wu (llllvvuu)]

if you don’t want to see the warning you can change aesop to aesop (config := { warnOnNonterminal := false })

[Nick_adfor]

Thanks! I must be misunderstanding Aristotle.

[Nick_adfor]

How does aesop solve this and why does the warning appear?

[Jakob von Raumer]

The warning apperas because the developers of aesop meant for aesop to be used as a terminal tactic only, so it gives a warning if there's any goals left to prove after its application.

[Nick_adfor]

So in this code generated by Aristotle, how does aesop following three cases work? My understanding is that aesop first resolves some portion of the goal, and then the remaining work is split into these three cases.

[Jakob von Raumer]

Without looking at the output, I'd assume that induction n splits it in two goals and then aesop splits the conjunction in one of the goals. The aesop repository has a pretty good documentation of what aesop does.

[Nick_adfor]

Using this lemma, I've proved

/-- 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.

The final goal is to prove that all roots of Chebyshev polynomials of the second kind are simple.

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

[Nick_adfor]

(deleted)

[Nick_adfor]

Yury G. Kudryashov said:

Aristotle https://aristotle.harmonic.fun/ solves it in <3m:

import Mathlib

/-- Positivity of Chebyshev polynomials of the second kind on [1, ∞).-/
lemma Chebyshev.U_pos_of_ge_one {n : ℕ} {y : ℝ} (hy : 1 ≤ y) :
    0 < (Polynomial.Chebyshev.U ℝ n).eval y := by
  have h_poly_pos_step : ∀ n : ℕ, ∀ y : ℝ, 1 ≤ y → 0 < Polynomial.eval y (Polynomial.Chebyshev.U ℝ n) ∧ Polynomial.eval y (Polynomial.Chebyshev.U ℝ (n + 1)) > Polynomial.eval y (Polynomial.Chebyshev.U ℝ n) := by
    intros n y hy; induction n <;> aesop;
    · linarith;
    · linarith;
    · norm_num [ add_assoc ] at * ; nlinarith;
  exact h_poly_pos_step n y hy |>.1

Aristotle seems to be hard to get access! In this case, your access to Aristotle is highly appreciated.