(* ========================================================================= *)
(* Divergence of harmonic series.                                            *)
(* ========================================================================= *)

prioritize_real();;

let HARMONIC_DIVERGES = 
prove
 (`~(?s. !e. &0 < e
             ==> ?N. !n. N <= n ==> abs(sum(1..n) (\i. &1 / &i) - s) < e)`,

  STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `&1 / &4`) THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o SPEC `N + 1`) THEN REWRITE_TAC[LE_ADD] THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `(N + 1) + (N + 1)`) THEN
  ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
  SIMP_TAC[SUM_ADD_SPLIT; ARITH_RULE `1 <= (N + 1) + 1`] THEN
  MATCH_MP_TAC(REAL_ARITH
   `&1 / &2 <= y
    ==> abs((x + y) - s) < &1 / &4 ==> ~(abs(x - s) < &1 / &4)`) THEN
  REWRITE_TAC[GSYM MULT_2] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC `sum((N + 1) + 1 .. 2 * (N + 1)) (\i. &1 / &(2 * (N + 1)))` THEN
  CONJ_TAC THENL
   [SIMP_TAC[SUM_CONST_NUMSEG; ARITH_RULE `(2 * x + 1) - (x + 1) = x`] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD] THEN
    MP_TAC(SPEC `n:num` REAL_POS) THEN CONV_TAC REAL_FIELD;
    MATCH_MP_TAC SUM_LE_NUMSEG THEN REPEAT STRIP_TAC THEN
    REWRITE_TAC[real_div; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
    POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
    REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Formulation in terms of limits.                                           *)
(* ------------------------------------------------------------------------- *)

needs "Library/analysis.ml";;

let HARMONIC_DIVERGES' = 
prove
 (`~(convergent (\n. sum(1..n) (\i. &1 / &i)))`,

  REWRITE_TAC[convergent; SEQ; GE; HARMONIC_DIVERGES]);;
(* ------------------------------------------------------------------------- *)
(* Lower bound on the partial sums.                                          *)
(* ------------------------------------------------------------------------- *)

let HARMONIC_LEMMA = 
prove
 (`!m. sum(1..2 EXP m) (\n. &1 / &n) >= &m / &2`,

  REWRITE_TAC[real_ge] THEN INDUCT_TAC THEN
  REWRITE_TAC[EXP; MULT_2; SUM_SING_NUMSEG] THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN
  SIMP_TAC[SUM_ADD_SPLIT; ARITH_RULE `1 <= 2 EXP m + 1`] THEN
  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
   `a <= x ==> b - a <= y ==> b <= x + y`)) THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_SUC; GSYM (CONJUNCT2 EXP); GSYM MULT_2] THEN
  MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC `sum(2 EXP m + 1..2 EXP (SUC m))(\n. &1 / &(2 EXP (SUC m)))` THEN
  CONJ_TAC THENL
   [SIMP_TAC[SUM_CONST_NUMSEG; EXP; ARITH_RULE `(2 * x + 1) - (x + 1) = x`] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
    MP_TAC(SPECL [`2`; `m:num`] EXP_EQ_0) THEN
    REWRITE_TAC[ARITH] THEN REWRITE_TAC[GSYM REAL_OF_NUM_EQ] THEN
    CONV_TAC REAL_FIELD;
    MATCH_MP_TAC SUM_LE_NUMSEG THEN REPEAT STRIP_TAC THEN
    REWRITE_TAC[real_div; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
    POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
    REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Germ of an alternative proof.                                             *)
(* ------------------------------------------------------------------------- *)

needs "Library/transc.ml";;

let LOG_BOUND = 
prove
 (`&0 < x /\ x < &1 ==> ln(&1 + x) >= x / &2`,

  REWRITE_TAC[real_ge] THEN REPEAT STRIP_TAC THEN
  GEN_REWRITE_TAC LAND_CONV [GSYM LN_EXP] THEN
  ASM_SIMP_TAC[LN_MONO_LE; REAL_EXP_POS_LT; REAL_LT_ADD; REAL_LT_01] THEN
  MP_TAC(SPEC `x / &2` REAL_EXP_BOUND_LEMMA) THEN
  POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;