Example (24.4)

　前回の結果とDIFF_CONV，更に微積分の基本定理（その１）FTC1を用いて，定積分の値を具体化します．

let lemma01 = MESON[REAL_LE; REAL_ARITH `&1 <= &n ==> &0 < &n`; REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ; PI_POS; REAL_LE_LMUL_EQ; REAL_MUL_AC]
`1 <= n
==> (&(k - 1) / &n <= x /\ x <= &k / &n
<=> &(k - 1) * pi <= &n * pi * x /\ &n * pi * x <= &k * pi)`;;

g `!n. 1 <= n
 ==> !k. 1 <= k /\ k <= n
 ==> ((!x. &(k - 1) / &n <= x /\ x <= &k / &n ==> &0 <= sin (&n * pi * x)) \/
 (!x. &(k - 1) / &n <= x /\ x <= &k / &n ==> &0 <= --sin (&n * pi * x)))`;;
e(REPEAT STRIP_TAC THEN ASM_SIMP_TAC[UNDISCH lemma01; GSYM REAL_OF_NUM_SUB] THEN DISJ_CASES_TAC (SPEC `k:num` EVEN_OR_ODD));;
e(FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[EVEN_EXISTS] THEN STRIP_TAC THEN ASM_SIMP_TAC[GSYM REAL_MUL] THEN MESON_TAC[REAL_MUL_AC; SIN_NEG_PERIODIC]);;
e(FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[ODD_EXISTS] THEN STRIP_TAC THEN ASM_SIMP_TAC[ADD1; GSYM REAL_ADD; GSYM REAL_MUL; ] THEN ASM_MESON_TAC[REAL_ADD_AC; REAL_ADD_SUB; REAL_MUL_AC; SIN_POS_PERIODIC]);;
let thm16 = top_thm();;

g `!n. 1 <= n
 ==> !k. 1 <= k /\ k <= n
 ==> !x. &(k - 1) / &n <= x /\ x <= &k / &n
 ==> abs (sin (&n * pi * x))= (-- &1 pow (k + 1) ) * sin (&n * pi * x)`;;
e(STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[UNDISCH lemma01; GSYM REAL_OF_NUM_SUB;] THEN REPEAT STRIP_TAC THEN DISJ_CASES_TAC (SPEC `k:num` EVEN_OR_ODD));;

e(FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[EVEN_EXISTS] THEN STRIP_TAC);;
e(MP_TAC(SPECL[`m:num`;`&n * pi * x`]SIN_NEG_PERIODIC) THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN ASM_SIMP_TAC[REAL_MUL] THEN ONCE_ASM_SIMP_TAC[GSYM ABS_NEG] THEN STRIP_TAC);;
e(ASM_SIMP_TAC[real_abs; POW_ADD; POW_MINUS1; POW_1] THEN REAL_ARITH_TAC);;

e(FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[ODD_EXISTS; ADD1; GSYM REAL_ADD] THEN STRIP_TAC);;
e(MP_TAC(SPECL[`m:num`;`&n * pi * x`]SIN_POS_PERIODIC) THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN SIMP_TAC[REAL_ADD; REAL_MUL] THEN SUBGOAL_TAC""`&(2 * m + 1) - &1 = &(2 * m)`[ASM_MESON_TAC[REAL_OF_NUM_SUB; REAL_ADD_SUB; ADD_SUB;]]);;
e(FIRST_X_ASSUM SUBST_ALL_TAC THEN ASM_SIMP_TAC[] THEN STRIP_TAC);; 
e(ASM_SIMP_TAC[real_abs; ARITH_RULE`(2 * m + 1) + 1 = 2 * (m + 1)`; POW_MINUS1] THEN REAL_ARITH_TAC);;
let thm17 = top_thm();;
let thm17 = MESON[thm17]
`!n k x. 1 <= n /\ 1 <= k /\ k <= n /\ &(k - 1) / &n <= x /\ x <= &k / &n
 ==> abs (sin (&n * pi * x))= (-- &1 pow (k + 1) ) * sin (&n * pi * x)`;;


let lemma03 = MESON[FTC1; DEFINT_INTEGRAL]
`!f f' a b.
    a <= b /\ (!x. a <= x /\ x <= b ==> (f diffl f' x) x)
    ==> integral (a,b) f' = f b - f a`;;
let lemma04 = MESON
[DIFF_CONV`(\x. &1 / pi * &1 / &n * (--cos (&n * pi * x)))`;
REAL_SOSFIELD`&0 < pi /\ &1 <= &n ==> &0 * &1 / &n * --cos (&n * pi * x) +
(&0 * --cos (&n * pi * x) +
 --(--sin (&n * pi * x) * (&0 * pi * x + (&0 * x + &1 * pi) * &n)) *
 &1 / &n) *
&1 / pi = sin (&n * pi * x)`;
REAL_LE]
`&0 < pi /\ 1 <= n ==> !x. ((\x. &1 / pi * &1 / &n * (--cos (&n * pi * x))) diffl sin (&n * pi * x) ) x`;;

let lemma05 = prove(
`!x. (\x:real. f x) contl x <=> f contl x`,
SIMP_TAC[contl] THEN BETA_TAC THEN MESON_TAC[]);;

let lemma06 = prove(
`!a b f g. a <= b /\
            (!x. a <= x /\ x <= b ==> f x = g x) /\
            (!x. a <= x /\ x <= b ==> (\x:real. f x) contl x)
 ==> integral (a,b) f = integral (a,b) g`,
SIMP_TAC[lemma05] THEN MESON_TAC[INTEGRABLE_CONTINUOUS; INTEGRABLE_DEFINT; INTEGRAL_EQ; DEFINT_INTEGRAL]);;

let lemma07 = prove(
`!n a b x. a <= x /\ x <= b ==> (\x. abs( sin (&n * pi * x))) contl x`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC CONT_ABS THEN SIMP_TAC[thm09]);;

g `!n k. 1 <= n /\ 1 <= k /\ k <= n
==> integral (&(k - 1) / &n,&k / &n) (\x. abs (sin (&n * pi * x))) = &2 / pi * &1 / &n`;;
e(ASSUME_TAC PI_POS THEN REPEAT STRIP_TAC THEN MP_TAC thm05 THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN MP_TAC lemma04 THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(MP_TAC(SPECL[`(\x. &1 / pi * &1 / &n * --cos (&n * pi * x))`;`(\x. sin (&n * pi * x))`;`&(k - 1) / &n`;`&k / &n`]lemma03) THEN BETA_TAC THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(MAP_EVERY MP_TAC[SPECL[`n:num`;`k:num`]thm17; SPECL[`n:num`;`&(k - 1) / &n`;`&k / &n`]lemma07] THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;

e(MP_TAC(SPECL[`&(k - 1) / &n`;`&k / &n`;`\x.  abs (sin (&n * pi * x))`;`\x. -- &1 pow (k + 1) * sin (&n * pi * x)`]lemma06) THEN BETA_TAC THEN ASM_SIMP_TAC[INTEGRABLE_CONTINUOUS; INTEGRAL_CMUL; thm09] THEN REPEAT STRIP_TAC);;

e(SUBGOAL_TAC""`&1 <= &n`[ASM_SIMP_TAC[REAL_LE]] THEN ASM_SIMP_TAC[UNDISCH(REAL_FIELD`&1 <= &n ==> &n * pi * &k / &n = &k * pi`); COS_NPI; REAL_SUB_LDISTRIB; ]);;

e(SIMP_TAC[SPEC`(-- &1 pow k)`REAL_NEG_MINUS1; REAL_MUL_AC; GSYM POW_ADD; UNDISCH(ARITH_RULE`1 <= k ==> k + k + 1 = 2 * k + 1 /\ k - 1 + k + 1 = 2 * k`);]);;

e(SIMP_TAC[ POW_ADD; POW_MINUS1; POW_1] THEN ASM_REAL_ARITH_TAC);;
let thm18 = top_thm();;