Example (12)

　今回は
\forall x:N\to R.\lim_{n\to\infty}x_n=+\infty\to \lim_{n\to\infty}\frac{1}{n}{\sum_{k=1}^{n}x_k}=+\infty
の証明です．

let limits_num_pinfinity = define `!x:num->real. limits_num_pinfinity x = !K:real. &0 (?N:num. !n. n>=N ==> K < x n)`;;

g`!x. limits_num_pinfinity x==>limits_num_pinfinity (\n. (sum(1..n)x)/ &n)`;;
e(REWRITE_TAC[limits_num_pinfinity] THEN REPEAT STRIP_TAC);;
e(FIRST_X_ASSUM( MP_TAC o SPEC`&4*K` ) THEN ASM_SIMP_TAC[REAL_ARITH`&0 &0< &4*K`] THEN DISCH_THEN(X_CHOOSE_THEN `N1:num` ASSUME_TAC ) );;
let lemma03 = REAL_SOSFIELD`&0= &N2 ==> x< &n*K`;;
let lemma04 = MESON[REAL_ARCH; lemma03; GE; real_ge; REAL_OF_NUM_LE; GSYM REAL_BOUNDS_LT; ]`&0 ?N2. !n. n>=N2 ==> -- (&n*K) < sum(1..N1)x`;;
e(MP_TAC lemma04 THEN ASM_SIMP_TAC THEN STRIP_TAC );;
e(EXISTS_TAC`2*N1+N2+1` THEN REPEAT STRIP_TAC);;

let lemma05 = ARITH_RULE `n>=2*N1+N2+1 ==> n>=N1 /\ n>=N2 /\ N1+1<=n /\ n>=2*N1 /\ ~(n=0) /\ 1 <= N1 + 1 /\ N1 <= n`;;
e(ASSUME_TAC( UNDISCH lemma05 ));;

let lemma01 = CONV_RULE((DEPTH_CONV BETA_CONV) THENC REWRITE_CONV[SUM_CONST_NUMSEG; ARITH_RULE`(n+1)-(N1+1)=n-N1`; ] )(SPECL[`(\i:num. &4*K)`;`x:num->real`;`N1+1`]SUM_LE_NUMSEG);;
let lemma02 = prove ( `&0=2*N1==> &2* &n*K<= &(n-N1)* &4*K`, REPEAT STRIP_TAC THEN ASM_SIMP_TAC[ARITH_RULE`n>=2*N1==>N1<=n`; GSYM REAL_OF_NUM_SUB; ] THEN MP_TAC(MESON[GE; GSYM REAL_OF_NUM_LE; GSYM REAL_MUL;]`n>=2*N1==> &2* &N1<= &n`) THEN ASM_SIMP_TAC THEN EVERY_ASSUM(MP_TAC) THEN CONV_TAC REAL_SOS );;

e( MP_TAC(lemma01) THEN MP_TAC(lemma02) THEN ASM_SIMP_TAC[ARITH_RULE`N1+1<=n ==> n>=N1`; REAL_LT_IMP_LE; ] THEN REPEAT STRIP_TAC);;
e ( ASM_MESON_TAC[ REAL_LT_RDIV_EQ; REAL_NZ_IMP_LT; SUM_COMBINE_R; REAL_LTE_ADD2; REAL_ARITH`--(a*b)+ &2*a*b=b*a`; REAL_LE_TRANS; ]);;

top_thm();;
val it : thm =
|- !x. limits_num_pinfinity x
==> limits_num_pinfinity (\n. sum (1..n) x / &n)