Example (11)

　極限値が実数aの場合です．

let my_thm02 = prove
(`!x a. x tends_num_real a ==> (\n. sum(1..n)x / &n) tends_num_real a`,
let lemma01,lemma02,lemma03 =
CONV_RULE
(REWRITE_CONV[SEQ; REAL_SUB_RZERO; SUM_SUB_NUMSEG; SUM_CONST_NUMSEG; ARITH_RULE`(n+1)-1=n`; REAL_FIELD`(x-z*y)/z=x/z-z*y/z`; ])
(SPEC`(\k:num. x k - a:real)`my_thm01),
prove
(`(!e. &0 < e ==> (?N. !n. n >= N ==> abs (sum (1..n) x / &n - &n * a / &n) < e))==>(!e. &0 < e ==> (?N. !n. n >= N ==> &n> &0 /\ abs (sum (1..n) x / &n - &n * a / &n) < e))`,
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o (SPEC`e:real`)) THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN
EXISTS_TAC`N+1` THEN ASM_MESON_TAC[ARITH_RULE`n>=N+1==>n>=N:num /\ n>0`; REAL_OF_NUM_GT]),
MESON
[REAL_DIV_REFL; REAL_DIV_LMUL; REAL_ARITH`&n> &0==> ~(&n= &0)`]
`&n > &0 /\ abs (sum (1..n) x / &n - &n * a / &n) < e <=> &n > &0 /\ abs (sum (1..n) x / &n - a) < e` in
REWRITE_TAC[SEQ] THEN
MESON_TAC[IMP_TRANS lemma01 lemma02; lemma03]);;
0..0..solved at 2
0..0..1..4..11..25..87..229..721..3193..solved at 3216
0..0..solved at 2
0..0..1..4..11..25..87..229..721..3192..11545..46722..solved at 46769
0..0..1..3..solved at 7
0..0..1..3..solved at 7
1 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
0..0..1..2..4..6..8..10..12..14..17..20..23..32..41..50..71..92..113..144..175..
206..273..340..407..498..589..680..772..864..956..1061..1166..1271..1376..1481..
1586..1697..1808..1919..2184..2449..2714..2979..3244..3509..solved at 3964
val my_thm02 : thm =
|- !x a. x tends_num_real a ==> (\n. sum (1..n) x / &n) tends_num_real a