チェビシェフの多項式を書き下すことは難しくありません．まず，引数の処理に用いる，2以上の整数をn+2の形に書き換えるconvを作ります． let NUM_ADD2_CONV = let add_tm = `(+):num->num->num` and two_tm = `2` in fun tm -> let m = mk_numeral(dest_num…

先に定義したチェビシェフの多項式が定める関数による[-1,1]の像が[-1,1]に含まれることは，余弦の逆関数 # ACS;; val it : thm = |- !y. -- &1 ==> &0 acs y /\ acs y acs y) = y についての # ACS_COS;; val it : thm = |- !y. -- &1 cos (acs y) = y から…

では，証明です． # g `!n:num x:real. cheb n (cos(x)) = cos*1 /\ (!x. cheb 1 (cos x) = cos (&1 * x)) /\ (!n. (!x. cheb n (cos x) = cos (&n * x)) /\ (!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x)) ==> (!x. cheb (n + 2) (cos x) = cos (&(n + 2…