Example (10)

　今回は

# g`!x:num->real. x tends_num_real &0 ==> (\n. sum(1..n)x / &n) tends_num_real &0`;;
val it : goalstack = 1 subgoal (1 total)

`!x. x tends_num_real &0 ==> (\n. sum (1..n) x / &n) tends_num_real &0`

です．数学的には分割して評価する標準的なものですが，．．．．

prove(`!x. x tends_num_real &0 ==> (\n. sum(1..n)x / &n) tends_num_real &0`,
let lemma01,lemma02,lemma03=
MESON[REAL_LTE_TRANS;REAL_LE;REAL_LE_LMUL;REAL_MUL_AC;REAL_LT_IMP_LE;REAL_ARCH;REAL_POS;GE]`&0 ?N2. !n. n>=N2 ==> abs(sum(1..N1) x) < &n*e/ &2`,
MESON[ARITH_RULE`N1+1<=i /\ i<=n ==> i>=N1`;REAL_LT_IMP_LE]`(!n. n >= N1 ==> abs (x n) < e / &2)==>(!i. N1 + 1 <= i /\ i <= n ==> abs (x i) <= e / &2)`,
CONV_RULE ( (ONCE_DEPTH_CONV BETA_CONV) THENC REWRITE_CONV[SUM_CONST_NUMSEG;ARITH_RULE`(n+1)-(N1+1)=n-N1`;]) (SPECL[`(\k:num. abs ( (x:num->real) k))`;`(\k:num. e/ &2)`;`N1+1`;`n:num`]SUM_LE_NUMSEG) in
(REWRITE_TAC[SEQ;REAL_SUB_RZERO] THEN STRIP_TAC THEN STRIP_TAC) THEN
(ONCE_REWRITE_TAC[GSYM REAL_LT_HALF1] THEN REPEAT STRIP_TAC) THEN
(FIRST_X_ASSUM( fun t -> MP_TAC ( SPEC `e/ &2` t ) THEN ASM_SIMP_TAC THEN DISCH_THEN(X_CHOOSE_TAC `N1:num`) )) THEN
(MP_TAC(lemma01) THEN ASM_SIMP_TAC THEN STRIP_TAC) THEN
( (EXISTS_TAC`N1+N2+1`) THEN REPEAT STRIP_TAC ) THEN
(MP_TAC(ARITH_RULE`n>=N1+N2+1==>n>=N1 /\ N1<=n /\ n>=N2 /\ 1<=N1+1 /\ ~(n=0)`
) THEN ASM_SIMP_TAC THEN REPEAT STRIP_TAC THEN MP_TAC(SPEC`n:num`REAL_NZ_IMP_LT) THEN ASM_SIMP_TAC THEN STRIP_TAC) THEN
(ASM_SIMP_TAC[SPECL[`x:num->real`;`1`;`N1:num`;`n:num`](GSYM(SUM_COMBINE_R))]) THEN
(MATCH_MP_TAC(REAL_FIELD`abs(x/ &n)abs( (x+y)/ &n)( (abs(x/ &n)abs(x)< &n*p)/\(abs(x/ &n)<=p<=>abs(x)<= &n*p))`; ] ) THEN
(MATCH_MP_TAC (MESON[SUM_ABS_NUMSEG;REAL_LE_TRANS;]`sum(m..n)(\k. abs( x k ))<=p==>abs(sum(m..n) x)<=p`) ) THEN
(ASM_MESON_TAC[IMP_TRANS lemma02 lemma03;ARITH_RULE`n-m<=n:num`;REAL_LE;REAL_LE_RMUL_EQ;REAL_ARITH`x<=y==>(z<=x==>z<=y)`;]) );;
0..0..1..3..6..9..solved at 15
0..0..1..2..4..10..18..31..65..117..232..469..938..solved at 1048
0..0..1..2..solved at 6
0..0..1..2..4..10..18..28..46..66..89..156..226..317..507..701..solved at 749
0..0..1..2..3..7..12..17..26..35..44..82..120..168..268..368..513..746..988..132
5..solved at 1895
0..0..1..2..4..10..18..28..45..64..86..148..213..297..475..657..solved at 703
0..0..1..2..3..7..12..17..25..33..41..75..109..152..245..338..473..687..910..122
4..solved at 1771
3 basis elements and 0 critical pairs
3 basis elements and 0 critical pairs
2 basis elements and 0 critical pairs
2 basis elements and 0 critical pairs
0..0..2..4..12..24..47..79..138..210..348..539..849..solved at 1200
val it : thm =
|- !x. x tends_num_real &0 ==> (\n. sum (1..n) x / &n) tends_num_real &0