19 Real analysis (3)

　先に定義したチェビシェフの多項式が定める関数による[-1,1]の像が[-1,1]に含まれることは，余弦の逆関数

# ACS;;
val it : thm =
|- !y. -- &1 <= y /\ y <= &1
==> &0 <= acs y /\ acs y <= pi /\ cos (acs y) = y

についての

# ACS_COS;;
val it : thm = |- !y. -- &1 <= y /\ y <= &1 ==> cos (acs y) = y

から直ちに判ります．実際

# g `!n x. abs(x)<= &1 ==> abs(cheb n x)<= &1` ;;
val it : goalstack = 1 subgoal (1 total)

`!n x. abs x <= &1 ==> abs (cheb n x) <= &1`

に対して，まず絶対値記号を

# GSYM REAL_BOUNDS_LE;;
val it : thm = |- !x k. abs x <= k <=> --k <= x /\ x <= k

により

# e(REWRITE_TAC[GSYM REAL_BOUNDS_LE]);;
val it : goalstack = 1 subgoal (1 total)

`!n x. -- &1 <= x /\ x <= &1 ==> -- &1 <= cheb n x /\ cheb n x <= &1`|- `!n x. abs(x)<= &1 ==> abs(cheb n x)<= &1`

と外せば，x = cos t として，先の

# CHEB_COS;;
val it : thm = |- !n x. cheb n (cos x) = cos (&n * x)

および

# COS_BOUNDS;;
val it : thm = |- !x. -- &1 <= cos x /\ cos x <= &1

から

# e (MESON_TAC[CHEB_COS; ACS_COS; COS_BOUNDS]);;
0..0..1..2..3..7..14..26..46..74..111..solved at 136
0..0..1..2..3..7..14..26..48..78..117..solved at 151
val it : goalstack = No subgoals

# top_thm();;
val it : thm = |- !n x. abs x <= &1 ==> abs (cheb n x) <= &1

となります．