1 (* ========================================================================= *)
2 (* Divergence of harmonic series. *)
3 (* ========================================================================= *)
7 let HARMONIC_DIVERGES = prove
9 ==> ?N. !n. N <= n ==> abs(sum(1..n) (\i. &1 / &i) - s) < e)`,
10 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `&1 / &4`) THEN
11 CONV_TAC REAL_RAT_REDUCE_CONV THEN STRIP_TAC THEN
12 FIRST_ASSUM(MP_TAC o SPEC `N + 1`) THEN REWRITE_TAC[LE_ADD] THEN
13 FIRST_X_ASSUM(MP_TAC o SPEC `(N + 1) + (N + 1)`) THEN
14 ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
15 SIMP_TAC[SUM_ADD_SPLIT; ARITH_RULE `1 <= (N + 1) + 1`] THEN
16 MATCH_MP_TAC(REAL_ARITH
18 ==> abs((x + y) - s) < &1 / &4 ==> ~(abs(x - s) < &1 / &4)`) THEN
19 REWRITE_TAC[GSYM MULT_2] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
20 EXISTS_TAC `sum((N + 1) + 1 .. 2 * (N + 1)) (\i. &1 / &(2 * (N + 1)))` THEN
22 [SIMP_TAC[SUM_CONST_NUMSEG; ARITH_RULE `(2 * x + 1) - (x + 1) = x`] THEN
23 REWRITE_TAC[GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD] THEN
24 MP_TAC(SPEC `n:num` REAL_POS) THEN CONV_TAC REAL_FIELD;
25 MATCH_MP_TAC SUM_LE_NUMSEG THEN REPEAT STRIP_TAC THEN
26 REWRITE_TAC[real_div; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
27 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
28 REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN ARITH_TAC]);;
30 (* ------------------------------------------------------------------------- *)
31 (* Formulation in terms of limits. *)
32 (* ------------------------------------------------------------------------- *)
34 needs "Library/analysis.ml";;
36 let HARMONIC_DIVERGES' = prove
37 (`~(convergent (\n. sum(1..n) (\i. &1 / &i)))`,
38 REWRITE_TAC[convergent; SEQ; GE; HARMONIC_DIVERGES]);;
40 (* ------------------------------------------------------------------------- *)
41 (* Lower bound on the partial sums. *)
42 (* ------------------------------------------------------------------------- *)
44 let HARMONIC_LEMMA = prove
45 (`!m. sum(1..2 EXP m) (\n. &1 / &n) >= &m / &2`,
46 REWRITE_TAC[real_ge] THEN INDUCT_TAC THEN
47 REWRITE_TAC[EXP; MULT_2; SUM_SING_NUMSEG] THEN
48 CONV_TAC REAL_RAT_REDUCE_CONV THEN
49 SIMP_TAC[SUM_ADD_SPLIT; ARITH_RULE `1 <= 2 EXP m + 1`] THEN
50 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
51 `a <= x ==> b - a <= y ==> b <= x + y`)) THEN
52 REWRITE_TAC[GSYM REAL_OF_NUM_SUC; GSYM (CONJUNCT2 EXP); GSYM MULT_2] THEN
53 MATCH_MP_TAC REAL_LE_TRANS THEN
54 EXISTS_TAC `sum(2 EXP m + 1..2 EXP (SUC m))(\n. &1 / &(2 EXP (SUC m)))` THEN
56 [SIMP_TAC[SUM_CONST_NUMSEG; EXP; ARITH_RULE `(2 * x + 1) - (x + 1) = x`] THEN
57 REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
58 MP_TAC(SPECL [`2`; `m:num`] EXP_EQ_0) THEN
59 REWRITE_TAC[ARITH] THEN REWRITE_TAC[GSYM REAL_OF_NUM_EQ] THEN
61 MATCH_MP_TAC SUM_LE_NUMSEG THEN REPEAT STRIP_TAC THEN
62 REWRITE_TAC[real_div; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
63 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
64 REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN ARITH_TAC]);;
66 (* ------------------------------------------------------------------------- *)
67 (* Germ of an alternative proof. *)
68 (* ------------------------------------------------------------------------- *)
70 needs "Library/transc.ml";;
73 (`&0 < x /\ x < &1 ==> ln(&1 + x) >= x / &2`,
74 REWRITE_TAC[real_ge] THEN REPEAT STRIP_TAC THEN
75 GEN_REWRITE_TAC LAND_CONV [GSYM LN_EXP] THEN
76 ASM_SIMP_TAC[LN_MONO_LE; REAL_EXP_POS_LT; REAL_LT_ADD; REAL_LT_01] THEN
77 MP_TAC(SPEC `x / &2` REAL_EXP_BOUND_LEMMA) THEN
78 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;