19 Real analysis (2)
では，証明です．
# 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) * x)))`
ここで定義と簡約の為の定理
# [cheb; REAL_MUL_LZERO; REAL_MUL_LID; COS_0];;
val it : thm list =
[|- (!x. cheb 0 x = &1) /\
(!x. cheb 1 x = x) /\
(!n x. cheb (n + 2) x = &2 * x * cheb (n + 1) x - cheb n x);
|- !x. &0 * x = &0; |- !x. &1 * x = x; |- cos (&0) = &1]
を参照します．
# e(REWRITE_TAC[cheb; REAL_MUL_LZERO; REAL_MUL_LID; COS_0]);;
val it : goalstack = 1 subgoal (1 total)`!n. (!x. cheb n (cos x) = cos (&n * x)) /\
(!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x))
==> (!x. &2 * cos x * cheb (n + 1) (cos x) - cheb n (cos x) =
cos (&(n + 2) * x))`# e(REPEAT STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)0 [`!x. cheb n (cos x) = cos (&n * x)`]
1 [`!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x)`]`&2 * cos x * cheb (n + 1) (cos x) - cheb n (cos x) = cos (&(n + 2) * x)`
仮定を用いて結論を余弦についての等式に書き換えましょう．
# e(ASM_REWRITE_TAC[]);;
val it : goalstack = 1 subgoal (1 total)0 [`!x. cheb n (cos x) = cos (&n * x)`]
1 [`!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x)`]`&2 * cos x * cos (&(n + 1) * x) - cos (&n * x) = cos (&(n + 2) * x)`
そしてカッコ内を:realの元の和に展開します．
# [GSYM REAL_OF_NUM_ADD; REAL_MUL_LID; REAL_ADD_RDISTRIB];;
val it : thm list =
[|- !m n. &(m + n) = &m + &n; |- !x. &1 * x = x;
|- !x y z. (x + y) * z = x * z + y * z]
# e(REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_MUL_LID; REAL_ADD_RDISTRIB]);;
val it : goalstack = 1 subgoal (1 total)0 [`!x. cheb n (cos x) = cos (&n * x)`]
1 [`!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x)`]`&2 * cos x * cos (&n * x + x) - cos (&n * x) = cos (&n * x + &2 * x)`
普通ならcos (&n * x)を右辺に移項して和積ですが，ここでは加法定理と2倍角
# [COS_ADD; COS_DOUBLE; SIN_DOUBLE];;
val it : thm list =
[|- !x y. cos (x + y) = cos x * cos y - sin x * sin y;
|- !x. cos (&2 * x) = cos x pow 2 - sin x pow 2;
|- !x. sin (&2 * x) = &2 * sin x * cos x]
を用いて素朴に辺々を展開比較します．
# e(REWRITE_TAC[COS_ADD; COS_DOUBLE; SIN_DOUBLE]);;
val it : goalstack = 1 subgoal (1 total)0 [`!x. cheb n (cos x) = cos (&n * x)`]
1 [`!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x)`]`&2 * cos x * (cos (&n * x) * cos x - sin (&n * x) * sin x) - cos (&n * x) =
cos (&n * x) * (cos x pow 2 - sin x pow 2) -
sin (&n * x) * &2 * sin x * cos x`
後は2乗の和=1
# SPECL [`x:real`] SIN_CIRCLE;;
val it : thm = |- sin x pow 2 + cos x pow 2 = &1
を前件に付して，REAL_RINGに処理させます．
# e(MP_TAC (SPECL [`x:real`] SIN_CIRCLE));;
val it : goalstack = 1 subgoal (1 total)0 [`!x. cheb n (cos x) = cos (&n * x)`]
1 [`!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x)`]`sin x pow 2 + cos x pow 2 = &1
==> &2 * cos x * (cos (&n * x) * cos x - sin (&n * x) * sin x) -
cos (&n * x) =
cos (&n * x) * (cos x pow 2 - sin x pow 2) -
sin (&n * x) * &2 * sin x * cos x`# e ( CONV_TAC REAL_RING );;
2 basis elements and 0 critical pairs
val it : goalstack = No subgoals
REAL_RING，REAL_FIELDは優秀なのでこれでOKですが，より明示的に
val it : goalstack = 1 subgoal (1 total)
0 [`!x. cheb n (cos x) = cos (&n * x)`]
1 [`!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x)`]`&2 * cos x * (cos (&n * x) * cos x - sin (&n * x) * sin x) - cos (&n * x) =
cos (&n * x) * (cos x pow 2 - sin x pow 2) -
sin (&n * x) * &2 * sin x * cos x`# let lemma = CONV_RULE (REWRITE_CONV[REAL_RING`a+b= &1<=>a= &1-b`]) SIN_CIRCLE;
;
1 basis elements and 0 critical pairs
2 basis elements and 0 critical pairs
val lemma : thm = |- !x. sin x pow 2 = &1 - cos x pow 2
# e (REWRITE_TAC[lemma]);;
val it : goalstack = 1 subgoal (1 total)0 [`!x. cheb n (cos x) = cos (&n * x)`]
1 [`!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x)`]`&2 * cos x * (cos (&n * x) * cos x - sin (&n * x) * sin x) - cos (&n * x) =
cos (&n * x) * (cos x pow 2 - (&1 - cos x pow 2)) -
sin (&n * x) * &2 * sin x * cos x`# e ( CONV_TAC REAL_RING );;
1 basis elements and 0 critical pairs
val it : goalstack = No subgoals
としても良いでしょう．
まとめると
# let CHEB_COS = prove
(`!n x. cheb n (cos x) = cos(&n * x)`,
MATCH_MP_TAC num2_INDUCTION THEN
REWRITE_TAC[cheb; REAL_MUL_LZERO; REAL_MUL_LID; COS_0] THEN
REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_MUL_LID; REAL_ADD_RDISTRIB] THEN
REWRITE_TAC[COS_ADD; COS_DOUBLE; SIN_DOUBLE] THEN
MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN CONV_TAC REAL_RING);;
2 basis elements and 0 critical pairs
val ( CHEB_COS ) : thm = |- !n x. cheb n (cos x) = cos (&n * x)
となります．
*1:&n)*x) ` ;; val it : goalstack = 1 subgoal (1 total) `!n x. cheb n (cos x) = cos (&n * x)` # e (MATCH_MP_TAC num2_INDUCTION) ;; val it : goalstack = 1 subgoal (1 total) `(!x. cheb 0 (cos x) = cos (&0 * x
