100/triangular.ml

   1 (* ========================================================================= *)
   2 (* Sum of reciprocals of triangular numbers.                                 *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/misc.ml";;  (*** Just for REAL_ARCH_INV! ***)
   6
   7 prioritize_real();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Definition of triangular numbers.                                         *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let triangle = new_definition
  14  `triangle n = (n * (n + 1)) DIV 2`;;
  15
  16 (* ------------------------------------------------------------------------- *)
  17 (* Mapping them into the reals: division is exact.                           *)
  18 (* ------------------------------------------------------------------------- *)
  19
  20 let REAL_TRIANGLE = prove
  21  (`&(triangle n) = (&n * (&n + &1)) / &2`,
  22   MATCH_MP_TAC(REAL_ARITH `&2 * x = y ==> x = y / &2`) THEN
  23   REWRITE_TAC[triangle; REAL_OF_NUM_MUL; REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
  24   SUBGOAL_THEN `EVEN(n * (n + 1))` MP_TAC THENL
  25    [REWRITE_TAC[EVEN_MULT; EVEN_ADD; ARITH] THEN CONV_TAC TAUT;
  26     REWRITE_TAC[EVEN_EXISTS] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  27     AP_TERM_TAC THEN MATCH_MP_TAC DIV_MULT THEN REWRITE_TAC[ARITH]]);;
  28
  29 (* ------------------------------------------------------------------------- *)
  30 (* Sum of a finite number of terms.                                          *)
  31 (* ------------------------------------------------------------------------- *)
  32
  33 let TRIANGLE_FINITE_SUM = prove
  34  (`!n. sum(1..n) (\k. &1 / &(triangle k)) = &2 - &2 / (&n + &1)`,
  35   INDUCT_TAC THEN
  36   ASM_REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ARITH_RULE `1 <= SUC n`] THEN
  37   CONV_TAC REAL_RAT_REDUCE_CONV THEN
  38   REWRITE_TAC[REAL_TRIANGLE; GSYM REAL_OF_NUM_SUC] THEN CONV_TAC REAL_FIELD);;
  39
  40 (* ------------------------------------------------------------------------- *)
  41 (* Hence limit.                                                              *)
  42 (* ------------------------------------------------------------------------- *)
  43
  44 let TRIANGLE_CONVERGES = prove
  45  (`!e. &0 < e
  46        ==> ?N. !n. n >= N
  47                    ==> abs(sum(1..n) (\k. &1 / &(triangle k)) - &2) < e`,
  48   GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [REAL_ARCH_INV] THEN
  49   DISCH_THEN(X_CHOOSE_THEN `N:num` STRIP_ASSUME_TAC) THEN
  50   EXISTS_TAC `2 * N + 1` THEN REWRITE_TAC[GE] THEN REPEAT STRIP_TAC THEN
  51   REWRITE_TAC[TRIANGLE_FINITE_SUM; REAL_ARITH `abs(x - y - x) = abs y`] THEN
  52   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `inv(&N)` THEN
  53   ASM_SIMP_TAC[REAL_ABS_DIV; REAL_ABS_NUM] THEN
  54   ONCE_REWRITE_TAC[GSYM REAL_INV_DIV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
  55   SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
  56   REWRITE_TAC[REAL_ARITH `abs(&n + &1) = &n + &1`] THEN
  57   REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
  58   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;
  59
  60 (* ------------------------------------------------------------------------- *)
  61 (* In terms of limits.                                                       *)
  62 (* ------------------------------------------------------------------------- *)
  63
  64 needs "Library/analysis.ml";;
  65
  66 override_interface ("-->",`(tends_num_real)`);;
  67
  68 let TRIANGLE_CONVERGES' = prove
  69  (`(\n. sum(1..n) (\k. &1 / &(triangle k))) --> &2`,
  70   REWRITE_TAC[SEQ; TRIANGLE_CONVERGES]);;