100/divharmonic.ml

   1 (* ========================================================================= *)
   2 (* Divergence of harmonic series.                                            *)
   3 (* ========================================================================= *)
   4
   5 prioritize_real();;
   6
   7 let HARMONIC_DIVERGES = prove
   8  (`~(?s. !e. &0 < e
   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
  17    `&1 / &2 <= y
  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
  21   CONJ_TAC THENL
  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]);;
  29
  30 (* ------------------------------------------------------------------------- *)
  31 (* Formulation in terms of limits.                                           *)
  32 (* ------------------------------------------------------------------------- *)
  33
  34 needs "Library/analysis.ml";;
  35
  36 let HARMONIC_DIVERGES' = prove
  37  (`~(convergent (\n. sum(1..n) (\i. &1 / &i)))`,
  38   REWRITE_TAC[convergent; SEQ; GE; HARMONIC_DIVERGES]);;
  39
  40 (* ------------------------------------------------------------------------- *)
  41 (* Lower bound on the partial sums.                                          *)
  42 (* ------------------------------------------------------------------------- *)
  43
  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
  55   CONJ_TAC THENL
  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
  60     CONV_TAC REAL_FIELD;
  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]);;
  65
  66 (* ------------------------------------------------------------------------- *)
  67 (* Germ of an alternative proof.                                             *)
  68 (* ------------------------------------------------------------------------- *)
  69
  70 needs "Library/transc.ml";;
  71
  72 let LOG_BOUND = prove
  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);;