Kata

Chebyshev polynomials of the first kind are defined as follows:

For example, $T_3(x)=2x(2x-1)-x=4x^2-3xT\_3(x)\; =\; 2x(2x\; -\; 1)\; -\; x\; =\; 4x^2\; -\; 3x$.

If $xx$ is in the interval $[-1,1][-1,\; 1]$ then Chebyshev polynomials of the first kind satisfy the equation: $T_n(\cos x)=\cos (nx)T\_n(\backslash cos\; x)\; =\; \backslash cos(nx)$.

Your task is to prove this equation and derive from it the following bound of Chebyshev polynomials: $-1\le T_n(x)\le 1-1\; \backslash le\; T\_n(x)\; \backslash le\; 1$ if $-1\le x\le 1-1\; \backslash le\; x\; \backslash le\; 1$.

Preloaded code

Require Import Reals.

Local Open Scope R_scope.

Fixpoint cheb (n : nat) (x : R) : R :=
  match n with
  | 0 => 1
  | 1 => x
  | S (S n as n') => 2 * x * cheb n' x - cheb n x
  end.

Arguments cheb : simpl nomatch.

import data.polynomial data.complex.exponential

open polynomial

noncomputable def cheb : ℕ → polynomial ℝ
| 0 := 1
| 1 := X
| (n + 2) := 2 * X * cheb (n + 1) - cheb n

def SUBMISSION_COS := ∀ (n : ℕ) (x : ℝ), 
  eval (real.cos x) (cheb n) = real.cos (n * x)
notation `SUBMISSION_COS` := SUBMISSION_COS

def SUBMISSION_BOUNDED := ∀ (n : ℕ) (x : ℝ), 
  x ∈ set.Icc (-1 : ℝ) 1 →
  eval x (cheb n) ∈ set.Icc (-1 : ℝ) 1 
notation `SUBMISSION_BOUNDED` := SUBMISSION_BOUNDED