100/stirling.ml

   1 (* ========================================================================= *)
   2 (* Stirling's approximation.                                                 *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/analysis.ml";;
   6 needs "Library/transc.ml";;
   7
   8 override_interface("-->",`(tends_num_real)`);;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* This is a handy induction for Wallis's product below.                     *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let ODDEVEN_INDUCT = prove
  15  (`!P. P 0 /\ P 1 /\ (!n. P n ==> P(n + 2)) ==> !n. P n`,
  16   GEN_TAC THEN STRIP_TAC THEN
  17   SUBGOAL_THEN `!n. P n /\ P(n + 1)` (fun th -> MESON_TAC[th]) THEN
  18   INDUCT_TAC THEN ASM_SIMP_TAC[ADD1; GSYM ADD_ASSOC] THEN
  19   ASM_SIMP_TAC[ARITH]);;
  20
  21 (* ------------------------------------------------------------------------- *)
  22 (* A particular limit we need below.                                         *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 let LN_LIM_BOUND = prove
  26  (`!n. ~(n = 0) ==> abs(&n * ln(&1 + &1 / &n) - &1) <= &1 / (&2 * &n)`,
  27   REPEAT STRIP_TAC THEN MP_TAC(SPECL [`&1 / &n`; `2`] MCLAURIN_LN_POS) THEN
  28   ASM_SIMP_TAC[SUM_2; REAL_LT_DIV; REAL_OF_NUM_LT; LT_NZ; ARITH] THEN
  29   DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
  30   ASM_REWRITE_TAC[] THEN
  31   REWRITE_TAC[real_div; REAL_INV_0; REAL_MUL_RZERO; REAL_ADD_LID] THEN
  32   REWRITE_TAC[REAL_POW_1; REAL_POW_2; REAL_MUL_LNEG; REAL_MUL_RNEG;
  33               REAL_NEG_NEG; REAL_MUL_LID; REAL_INV_1; REAL_POW_NEG;
  34               REAL_POW_ONE; ARITH; REAL_MUL_RID] THEN
  35   ASM_SIMP_TAC[REAL_OF_NUM_EQ; REAL_FIELD
  36    `~(x = &0) ==> x * (inv(x) + a) - &1 = x * a`] THEN
  37   REWRITE_TAC[REAL_ARITH `n * --((i * i) * a) = --((n * i) * a * i)`] THEN
  38   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH; REAL_MUL_LID] THEN
  39   REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_MUL] THEN
  40   ONCE_REWRITE_TAC[REAL_INV_MUL] THEN REWRITE_TAC[REAL_ABS_MUL] THEN
  41   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
  42   MATCH_MP_TAC REAL_LE_LMUL THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
  43   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
  44   MATCH_MP_TAC REAL_LE_RMUL THEN
  45   ASM_SIMP_TAC[real_div; REAL_MUL_LID; REAL_LE_INV_EQ; REAL_POS] THEN
  46   REWRITE_TAC[REAL_ABS_INV] THEN MATCH_MP_TAC REAL_INV_LE_1 THEN
  47   REWRITE_TAC[REAL_ABS_MUL] THEN
  48   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN
  49   MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_POS] THEN
  50   UNDISCH_TAC `&0 < t` THEN REAL_ARITH_TAC);;
  51
  52 let LN_LIM_LEMMA = prove
  53  (`(\n. &n * ln(&1 + &1 / &n)) --> &1`,
  54   GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV)
  55    [REAL_ARITH `a = (a - &1) + &1`] THEN
  56   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_ADD_LID] THEN
  57   MATCH_MP_TAC SEQ_ADD THEN REWRITE_TAC[SEQ_CONST] THEN
  58   MATCH_MP_TAC SEQ_LE_0 THEN EXISTS_TAC `\n. &1 / &n` THEN
  59   REWRITE_TAC[SEQ_HARMONIC] THEN
  60   EXISTS_TAC `1` THEN REWRITE_TAC[ARITH_RULE `n >= 1 <=> ~(n = 0)`] THEN
  61   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
  62   EXISTS_TAC `&1 / (&2 * &n)` THEN ASM_SIMP_TAC[LN_LIM_BOUND] THEN
  63   REWRITE_TAC[real_div; REAL_MUL_LID; REAL_ABS_INV] THEN
  64   MATCH_MP_TAC REAL_LE_INV2 THEN UNDISCH_TAC `~(n = 0)` THEN
  65   REWRITE_TAC[GSYM REAL_OF_NUM_EQ] THEN REAL_ARITH_TAC);;
  66
  67 (* ------------------------------------------------------------------------- *)
  68 (* Lemma for proving inequality via derivative and limit at infinity.        *)
  69 (* ------------------------------------------------------------------------- *)
  70
  71 let POSITIVE_DIFF_LEMMA = prove
  72  (`!f f'. (!x. &0 < x ==> (f diffl f'(x)) x /\ f'(x) < &0) /\
  73           (\n. f(&n)) --> &0
  74           ==> !n. ~(n = 0) ==> &0 < f(&n)`,
  75   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LE] THEN DISCH_TAC THEN
  76   SUBGOAL_THEN `!m p. n <= m /\ m < p ==> (f:real->real)(&p) < f(&m)`
  77   ASSUME_TAC THENL
  78    [REPEAT STRIP_TAC THEN
  79     MP_TAC(SPECL [`f:real->real`; `f':real->real`; `&m`; `&p`] MVT_ALT) THEN
  80     ANTS_TAC THENL
  81      [ASM_MESON_TAC[LT_NZ; LTE_TRANS; REAL_OF_NUM_LT; REAL_LTE_TRANS];
  82       ALL_TAC] THEN
  83     REWRITE_TAC[REAL_EQ_SUB_RADD] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  84     MATCH_MP_TAC(REAL_ARITH `&0 < z * --y ==> z * y + a < a`) THEN
  85     MATCH_MP_TAC REAL_LT_MUL THEN
  86     ASM_REWRITE_TAC[REAL_SUB_LT; REAL_OF_NUM_LT] THEN
  87     REWRITE_TAC[REAL_ARITH `&0 < --x <=> x < &0`] THEN
  88     ASM_MESON_TAC[LT_NZ; LTE_TRANS; REAL_OF_NUM_LT; REAL_LT_TRANS];
  89     ALL_TAC] THEN
  90   SUBGOAL_THEN `f(&(n + 1)) < &0` ASSUME_TAC THENL
  91    [FIRST_ASSUM(MP_TAC o SPECL [`n:num`; `n + 1`]) THEN ANTS_TAC THENL
  92      [ARITH_TAC; UNDISCH_TAC `f(&n) <= &0` THEN REAL_ARITH_TAC];
  93     ALL_TAC] THEN
  94   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [SEQ]) THEN
  95   DISCH_THEN(MP_TAC o SPEC `--f(&(n + 1))`) THEN
  96   ASM_REWRITE_TAC[REAL_SUB_RZERO; REAL_ARITH `&0 < --x <=> x < &0`] THEN
  97   DISCH_THEN(X_CHOOSE_THEN `p:num` (MP_TAC o SPEC `n + p + 2`)) THEN
  98   ANTS_TAC THENL [ARITH_TAC; ALL_TAC] THEN
  99   MATCH_MP_TAC(REAL_ARITH `y < &0 /\ z < y ==> abs(z) < --y ==> F`) THEN
 100   ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ARITH_TAC);;
 101
 102 (* ------------------------------------------------------------------------- *)
 103 (* Auxiliary definition.                                                     *)
 104 (* ------------------------------------------------------------------------- *)
 105
 106 let stirling = new_definition
 107  `stirling n = ln(&(FACT n)) - ((&n + &1 / &2) * ln(&n) - &n)`;;
 108
 109 (* ------------------------------------------------------------------------- *)
 110 (* This difference is a decreasing sequence.                                 *)
 111 (* ------------------------------------------------------------------------- *)
 112
 113 let STIRLING_DIFF = prove
 114  (`!n. ~(n = 0)
 115        ==> stirling(n) - stirling(n + 1) =
 116            (&n + &1 / &2) * ln((&n + &1) / &n) - &1`,
 117   REPEAT STRIP_TAC THEN REWRITE_TAC[stirling] THEN
 118   MATCH_MP_TAC(REAL_ARITH
 119    `(f' - f) + x = (nl' - nl) /\ n' = n + &1
 120     ==> (f - (nl - n)) - (f' - (nl' - n')) = x - &1`) THEN
 121   REWRITE_TAC[REAL_OF_NUM_ADD] THEN
 122   REWRITE_TAC[REWRITE_RULE[ADD1] FACT; GSYM REAL_OF_NUM_MUL] THEN
 123   SIMP_TAC[LN_MUL; FACT_LT; ADD_EQ_0; ARITH; LT_NZ; REAL_OF_NUM_LT] THEN
 124   ASM_SIMP_TAC[LN_DIV; REAL_OF_NUM_LT; ADD_EQ_0; ARITH; LT_NZ] THEN
 125   REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC);;
 126
 127 let STIRLING_DELTA_DERIV = prove
 128  (`!x. &0 < x
 129        ==> ((\x. ln ((x + &1) / x) - &1 / (x + &1 / &2)) diffl
 130             (-- &1 / (x * (x + &1) * (&2 * x + &1) pow 2))) x`,
 131   GEN_TAC THEN DISCH_TAC THEN
 132   W(fun (asl,w) -> MP_TAC(SPEC(rand w) (DIFF_CONV(lhand(rator w))))) THEN
 133   REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
 134    [REPEAT CONJ_TAC THEN TRY(MATCH_MP_TAC REAL_LT_DIV) THEN
 135     POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD;
 136     ALL_TAC] THEN
 137   MATCH_MP_TAC EQ_IMP THEN
 138   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[REAL_POW_2] THEN
 139   POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD);;
 140
 141 let STIRLING_DELTA_LIMIT = prove
 142  (`(\n. ln ((&n + &1) / &n) - &1 / (&n + &1 / &2)) --> &0`,
 143   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_SUB_RZERO] THEN
 144   MATCH_MP_TAC SEQ_SUB THEN CONJ_TAC THEN MATCH_MP_TAC SEQ_LE_0 THEN
 145   EXISTS_TAC `\n. &1 / &n` THEN REWRITE_TAC[SEQ_HARMONIC] THEN
 146   EXISTS_TAC `1` THEN X_GEN_TAC `n:num` THEN
 147   REWRITE_TAC[GE; GSYM REAL_OF_NUM_LE] THEN
 148   DISCH_TAC THEN MATCH_MP_TAC
 149    (REAL_ARITH `&0 <= x /\ x <= y ==> abs x <= abs y`)
 150   THEN CONJ_TAC THENL
 151    [MATCH_MP_TAC LN_POS THEN
 152     ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_ARITH `&1 <= x ==> &0 < x`] THEN
 153     REAL_ARITH_TAC;
 154     ASM_SIMP_TAC[REAL_FIELD `&1 <= x ==> (x + &1) / x = &1 + &1 / x`] THEN
 155     MATCH_MP_TAC LN_LE THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS];
 156     MATCH_MP_TAC REAL_LE_DIV THEN REAL_ARITH_TAC;
 157     REWRITE_TAC[real_div; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
 158     POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]);;
 159
 160 let STIRLING_DECREASES = prove
 161  (`!n. ~(n = 0) ==> stirling(n + 1) < stirling(n)`,
 162   ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN SIMP_TAC[STIRLING_DIFF] THEN
 163   REWRITE_TAC[REAL_SUB_LT] THEN
 164   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 165   SIMP_TAC[GSYM REAL_LT_LDIV_EQ; REAL_ARITH `&0 < &n + &1 / &2`] THEN
 166   ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN
 167   MATCH_MP_TAC POSITIVE_DIFF_LEMMA THEN
 168   EXISTS_TAC `\x. -- &1 / (x * (x + &1) * (&2 * x + &1) pow 2)` THEN
 169   SIMP_TAC[STIRLING_DELTA_DERIV; STIRLING_DELTA_LIMIT] THEN
 170   X_GEN_TAC `x:real` THEN DISCH_TAC THEN
 171   REWRITE_TAC[real_div; REAL_MUL_LNEG; REAL_MUL_LID] THEN
 172   REWRITE_TAC[REAL_ARITH `--x < &0 <=> &0 < x`; REAL_LT_INV_EQ] THEN
 173   REWRITE_TAC[REAL_POW_2] THEN
 174   REPEAT(MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC) THEN
 175   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 176
 177 (* ------------------------------------------------------------------------- *)
 178 (* However a slight tweak gives an *increasing* sequence.                    *)
 179 (* ------------------------------------------------------------------------- *)
 180
 181 let OTHER_DERIV_LEMMA = prove
 182  (`!x. &0 < x
 183        ==> ((\x. &1 / (&12 * x * (x + &1) * (x + &1 / &2))) diffl
 184             --(&3 * x pow 2 + &3 * x + &1 / &2) /
 185               (&12 * (x * (x + &1) * (x + &1 / &2)) pow 2)) x`,
 186   REPEAT STRIP_TAC THEN
 187   W(fun (asl,w) -> MP_TAC(SPEC(rand w) (DIFF_CONV(lhand(rator w))))) THEN
 188   REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
 189    [REWRITE_TAC[REAL_ENTIRE] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
 190     ALL_TAC] THEN
 191   MATCH_MP_TAC EQ_IMP THEN
 192   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[REAL_POW_2] THEN
 193   POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD);;
 194
 195 let STIRLING_INCREASES = prove
 196  (`!n. ~(n = 0)
 197        ==> stirling(n + 1) - &1 / (&12 * (&(n + 1)))
 198            > stirling(n) - &1 / (&12 * &n)`,
 199   REWRITE_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_ADD] THEN
 200   REWRITE_TAC[REAL_ARITH `a - b > c - d <=> c - a < d - b`] THEN
 201   SIMP_TAC[REAL_FIELD
 202     `~(&n = &0) ==> &1 / (&12 * &n) - &1 / (&12 * (&n + &1)) =
 203                     &1 / (&12 * &n * (&n + &1))`] THEN
 204   SIMP_TAC[REAL_OF_NUM_EQ; STIRLING_DIFF] THEN
 205   REWRITE_TAC[REAL_ARITH `a * b - &1 < c <=> b * a < c + &1`] THEN
 206   SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_ARITH `&0 < &n + &1 / &2`] THEN
 207   REWRITE_TAC[REAL_ARITH `(&1 / x + &1) / y = &1 / x / y + &1 / y`] THEN
 208   REWRITE_TAC[REAL_ARITH `a < b + c <=> &0 < b - (a - c)`] THEN
 209   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; GSYM REAL_INV_MUL] THEN
 210   REWRITE_TAC[GSYM real_div] THEN MATCH_MP_TAC POSITIVE_DIFF_LEMMA THEN
 211   EXISTS_TAC `\x. &1 / (x * (x + &1) * (&2 * x + &1) pow 2) -
 212                   (&3 * x pow 2 + &3 * x + &1 / &2) /
 213                   (&12 * (x * (x + &1) * (x + &1 / &2)) pow 2)` THEN
 214   REWRITE_TAC[] THEN CONJ_TAC THENL
 215    [ALL_TAC;
 216     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_SUB_RZERO] THEN
 217     MATCH_MP_TAC SEQ_SUB THEN REWRITE_TAC[STIRLING_DELTA_LIMIT] THEN
 218     REWRITE_TAC[real_div; REAL_INV_MUL; REAL_MUL_LID] THEN
 219     REWRITE_TAC[REAL_FIELD
 220      `inv(&12) * x * y * inv(&n + inv(&2)) = x * y * inv(&12 * &n + &6)`] THEN
 221     GEN_REWRITE_TAC RAND_CONV [SYM(REAL_RAT_REDUCE_CONV `&0 * &0 * &0`)] THEN
 222     REPEAT(MATCH_MP_TAC SEQ_MUL THEN CONJ_TAC) THEN
 223     MP_TAC(SPEC `&1` SEQ_HARMONIC) THEN
 224     REWRITE_TAC[real_div; REAL_MUL_LID] THEN
 225     DISCH_THEN(MP_TAC o MATCH_MP SEQ_SUBSEQ) THENL
 226      [DISCH_THEN(MP_TAC o SPECL [`1`; `1`]);
 227       DISCH_THEN(MP_TAC o SPECL [`12`; `6`])] THEN
 228     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL; ARITH; MULT_CLAUSES]] THEN
 229   X_GEN_TAC `x:real` THEN DISCH_TAC THEN CONJ_TAC THENL
 230    [GEN_REWRITE_TAC LAND_CONV
 231      [REAL_ARITH `&1 / x - y / z = --y / z - -- &1 / x`] THEN
 232     MATCH_MP_TAC DIFF_SUB THEN
 233     ASM_SIMP_TAC[STIRLING_DELTA_DERIV; OTHER_DERIV_LEMMA];
 234     ALL_TAC] THEN
 235   REWRITE_TAC[REAL_ARITH `a - b < &0 <=> a < b`] THEN
 236   ASM_SIMP_TAC[GSYM REAL_POW_2; REAL_FIELD
 237    `&0 < x
 238     ==> &1 / (x * (x + &1) * (&2 * x + &1) pow 2) =
 239         (&3 * x * (x + &1)) /
 240         (&12 * (x * (x + &1) * (x + &1 / &2)) *
 241                (x * (x + &1) * (x + &1 / &2)))`] THEN
 242   ONCE_REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LT_RMUL THEN
 243   CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
 244   REWRITE_TAC[REAL_LT_INV_EQ; REAL_POW_2] THEN
 245   REPEAT(MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC) THEN
 246   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 247
 248 (* ------------------------------------------------------------------------- *)
 249 (* Hence it converges to *something*.                                        *)
 250 (* ------------------------------------------------------------------------- *)
 251
 252 let STIRLING_UPPERBOUND = prove
 253  (`!n. stirling(SUC n) <= &1`,
 254   INDUCT_TAC THENL
 255    [REWRITE_TAC[stirling] THEN CONV_TAC NUM_REDUCE_CONV THEN
 256     REWRITE_TAC[LN_1] THEN CONV_TAC REAL_RAT_REDUCE_CONV;
 257     ALL_TAC] THEN
 258   MATCH_MP_TAC REAL_LE_TRANS THEN
 259   EXISTS_TAC `stirling(SUC n)` THEN ASM_REWRITE_TAC[] THEN
 260   REWRITE_TAC[ARITH_RULE `SUC(SUC n) = SUC n + 1`] THEN
 261   MATCH_MP_TAC REAL_LT_IMP_LE THEN MATCH_MP_TAC STIRLING_DECREASES THEN
 262   ARITH_TAC);;
 263
 264 let STIRLING_LOWERBOUND = prove
 265  (`!n. -- &1 <= stirling(SUC n)`,
 266   GEN_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 267   EXISTS_TAC `stirling(SUC n) - &1 / (&12 * &(SUC n))` THEN CONJ_TAC THENL
 268    [ALL_TAC;
 269     SIMP_TAC[REAL_ARITH `a - b <= a <=> &0 <= b`] THEN
 270     REWRITE_TAC[real_div; REAL_MUL_LID; REAL_LE_INV_EQ] THEN
 271     REWRITE_TAC[REAL_OF_NUM_MUL; REAL_POS]] THEN
 272   SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THENL
 273    [REWRITE_TAC[stirling] THEN CONV_TAC NUM_REDUCE_CONV THEN
 274     REWRITE_TAC[LN_1] THEN CONV_TAC REAL_RAT_REDUCE_CONV;
 275     ALL_TAC] THEN
 276   MATCH_MP_TAC REAL_LE_TRANS THEN
 277   EXISTS_TAC `stirling(SUC n) - &1 / (&12 * &(SUC n))` THEN
 278   ASM_REWRITE_TAC[] THEN
 279   REWRITE_TAC[ARITH_RULE `SUC(SUC n) = SUC n + 1`] THEN
 280   MATCH_MP_TAC(REAL_ARITH `b > a ==> a <= b`) THEN
 281   MATCH_MP_TAC STIRLING_INCREASES THEN ARITH_TAC);;
 282
 283 let STIRLING_MONO = prove
 284  (`!m n. ~(m = 0) /\ m <= n ==> stirling n <= stirling m`,
 285   REPEAT STRIP_TAC THEN
 286   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
 287   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
 288   SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THEN
 289   REWRITE_TAC[ADD_CLAUSES; REAL_LE_REFL] THEN
 290   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `stirling(m + d)` THEN
 291   ASM_SIMP_TAC[ADD1; REAL_LT_IMP_LE; STIRLING_DECREASES; ADD_EQ_0]);;
 292
 293 let STIRLING_CONVERGES = prove
 294  (`?c. stirling --> c`,
 295   ONCE_REWRITE_TAC[SEQ_SUC] THEN
 296   REWRITE_TAC[GSYM convergent] THEN MATCH_MP_TAC SEQ_BCONV THEN CONJ_TAC THENL
 297    [ALL_TAC;
 298     REWRITE_TAC[mono; real_ge] THEN DISJ2_TAC THEN REPEAT GEN_TAC THEN
 299     DISCH_TAC THEN MATCH_MP_TAC STIRLING_MONO THEN
 300     POP_ASSUM MP_TAC THEN ARITH_TAC] THEN
 301   REWRITE_TAC[MR1_BOUNDED; GE; LE_REFL] THEN
 302   MAP_EVERY EXISTS_TAC [`&2`; `0`] THEN REWRITE_TAC[LE_0] THEN
 303   SIMP_TAC[REAL_ARITH `-- &1 <= x /\ x <= &1 ==> abs(x) < &2`;
 304            STIRLING_UPPERBOUND; STIRLING_LOWERBOUND]);;
 305
 306 (* ------------------------------------------------------------------------- *)
 307 (* Now derive Wallis's infinite product.                                     *)
 308 (* ------------------------------------------------------------------------- *)
 309
 310 let [PI2_LT; PI2_LE; PI2_NZ] = (CONJUNCTS o prove)
 311  (`&0 < pi / &2 /\ &0 <= pi / &2 /\ ~(pi / &2 = &0)`,
 312   MP_TAC PI_POS THEN REAL_ARITH_TAC);;
 313
 314 let WALLIS_PARTS = prove
 315  (`!n. (&n + &2) * integral(&0,pi / &2) (\x. sin(x) pow (n + 2)) =
 316        (&n + &1) * integral(&0,pi / &2) (\x. sin(x) pow n)`,
 317   GEN_TAC THEN
 318   MP_TAC(SPECL [`\x. sin(x) pow (n + 1)`; `\x. --cos(x)`;
 319                 `\x. (&n + &1) * sin(x) pow n * cos(x)`;
 320                 `\x. sin(x)`; `&0`; `pi / &2`] INTEGRAL_BY_PARTS) THEN
 321   REWRITE_TAC[] THEN ANTS_TAC THENL
 322    [SIMP_TAC[REAL_LT_IMP_LE; PI_POS; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
 323     CONV_TAC(ONCE_DEPTH_CONV INTEGRABLE_CONV) THEN REWRITE_TAC[] THEN
 324     CONJ_TAC THEN GEN_TAC THEN STRIP_TAC THEN DIFF_TAC THEN
 325     REWRITE_TAC[REAL_OF_NUM_ADD; ADD_SUB] THEN REAL_ARITH_TAC;
 326     ALL_TAC] THEN
 327   REWRITE_TAC[SIN_PI2; COS_PI2; SIN_0; COS_0] THEN
 328   REWRITE_TAC[REAL_ARITH `s pow k * s = s * s pow k`] THEN
 329   REWRITE_TAC[GSYM(CONJUNCT2 real_pow); ARITH_RULE `SUC(n + 1) = n + 2`] THEN
 330   REWRITE_TAC[GSYM ADD1; real_pow; REAL_MUL_LZERO; REAL_MUL_RZERO;
 331               REAL_NEG_0; REAL_SUB_LZERO] THEN
 332   REWRITE_TAC[C MATCH_MP (SPEC_ALL SIN_CIRCLE) (REAL_RING
 333     `sin(x) pow 2 + cos(x) pow 2 = &1
 334      ==> (n * sn * cos(x)) * --cos(x) = (n * sn) * (sin(x) pow 2 - &1)`)] THEN
 335   REWRITE_TAC[REAL_SUB_LDISTRIB; GSYM REAL_MUL_ASSOC; GSYM REAL_POW_ADD] THEN
 336   REWRITE_TAC[REAL_MUL_RID] THEN
 337   SUBGOAL_THEN
 338    `integral(&0,pi / &2)
 339         (\x. (&n + &1) * sin x pow (n + 2) - (&n + &1) * sin x pow n) =
 340     (&n + &1) * (integral(&0,pi / &2) (\x. sin(x) pow (n + 2)) -
 341                  integral(&0,pi / &2) (\x. sin(x) pow n))`
 342    (fun th -> SUBST1_TAC th THEN REAL_ARITH_TAC) THEN
 343   REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN MATCH_MP_TAC EQ_TRANS THEN
 344   EXISTS_TAC
 345    `(&n + &1) *
 346     integral(&0,pi / &2) (\x. sin x pow (n + 2) - sin x pow n)` THEN
 347   CONJ_TAC THENL
 348    [MATCH_MP_TAC INTEGRAL_CMUL;
 349     AP_TERM_TAC THEN MATCH_MP_TAC INTEGRAL_SUB] THEN
 350   CONV_TAC(ONCE_DEPTH_CONV INTEGRABLE_CONV) THEN SIMP_TAC[PI2_LE]);;
 351
 352 let WALLIS_PARTS' = prove
 353  (`!n. integral(&0,pi / &2) (\x. sin(x) pow (n + 2)) =
 354        (&n + &1) / (&n + &2) * integral(&0,pi / &2) (\x. sin(x) pow n)`,
 355   MP_TAC WALLIS_PARTS THEN MATCH_MP_TAC MONO_FORALL THEN
 356   CONV_TAC REAL_FIELD);;
 357
 358 let WALLIS_0 = prove
 359  (`integral(&0,pi / &2) (\x. sin(x) pow 0) = pi / &2`,
 360   REWRITE_TAC[real_pow; REAL_DIV_1; REAL_MUL_LID] THEN
 361   SIMP_TAC[INTEGRAL_CONST; REAL_LT_IMP_LE; PI_POS; REAL_LT_DIV;
 362            REAL_OF_NUM_LT; ARITH; REAL_MUL_LID; REAL_SUB_RZERO]);;
 363
 364 let WALLIS_1 = prove
 365  (`integral(&0,pi / &2) (\x. sin(x) pow 1) = &1`,
 366   MATCH_MP_TAC DEFINT_INTEGRAL THEN REWRITE_TAC[PI2_LE; REAL_POW_1] THEN
 367   MP_TAC(SPECL [`\x. --cos(x)`; `\x. sin x`; `&0`; `pi / &2`] FTC1) THEN
 368   REWRITE_TAC[COS_0; COS_PI2] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 369   DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[PI2_LE] THEN
 370   REPEAT STRIP_TAC THEN DIFF_TAC THEN REAL_ARITH_TAC);;
 371
 372 let WALLIS_EVEN = prove
 373  (`!n. integral(&0,pi / &2) (\x. sin(x) pow (2 * n)) =
 374          (&(FACT(2 * n)) / (&2 pow n * &(FACT n)) pow 2) * pi / &2`,
 375   INDUCT_TAC THENL
 376    [CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 377     REWRITE_TAC[WALLIS_0] THEN REAL_ARITH_TAC;
 378     ALL_TAC] THEN
 379   ASM_REWRITE_TAC[ARITH_RULE `2 * SUC n = 2 * n + 2`; WALLIS_PARTS'] THEN
 380   REWRITE_TAC[REAL_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
 381   REWRITE_TAC[FACT; real_pow; GSYM REAL_OF_NUM_MUL] THEN
 382   ONCE_REWRITE_TAC[REAL_ARITH `(&2 * x) * y * z = (&2 * y) * (x * z)`] THEN
 383   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [REAL_POW_MUL] THEN
 384   REWRITE_TAC[real_div; REAL_INV_MUL; REAL_MUL_ASSOC] THEN
 385   AP_THM_TAC THEN AP_TERM_TAC THEN
 386   REWRITE_TAC[ARITH_RULE `2 * n + 2 = SUC(SUC(2 * n))`] THEN
 387   REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_2; FACT;
 388               GSYM REAL_OF_NUM_MUL] THEN
 389   CONV_TAC REAL_FIELD);;
 390
 391 let WALLIS_ODD = prove
 392  (`!n. integral(&0,pi / &2) (\x. sin(x) pow (2 * n + 1)) =
 393          (&2 pow n * &(FACT n)) pow 2 / &(FACT(2 * n + 1))`,
 394   INDUCT_TAC THENL
 395    [CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 396     REWRITE_TAC[WALLIS_1] THEN CONV_TAC REAL_RAT_REDUCE_CONV;
 397     ALL_TAC] THEN
 398   ASM_REWRITE_TAC[ARITH_RULE `2 * SUC n + 1 = (2 * n + 1) + 2`;
 399                   WALLIS_PARTS'] THEN
 400   GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
 401   REWRITE_TAC[FACT; real_pow; GSYM REAL_OF_NUM_MUL] THEN
 402   ONCE_REWRITE_TAC[REAL_ARITH `(&2 * x) * y * z = (x * z) * (&2 * y)`] THEN
 403   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [REAL_POW_MUL] THEN
 404   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
 405   GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
 406   REWRITE_TAC[ARITH_RULE `n + 2 = SUC(SUC n)`] THEN
 407   REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_2; FACT;
 408               GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
 409   MP_TAC(SPEC `2 * n + 1` FACT_LT) THEN REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
 410   CONV_TAC REAL_FIELD);;
 411
 412 let WALLIS_QUOTIENT = prove
 413  (`!n. integral(&0,pi / &2) (\x. sin(x) pow (2 * n)) /
 414        integral(&0,pi / &2) (\x. sin(x) pow (2 * n + 1)) =
 415         (&(FACT(2 * n)) * &(FACT(2 * n + 1))) / (&2 pow n * &(FACT n)) pow 4 *
 416         pi / &2`,
 417   GEN_TAC THEN REWRITE_TAC[WALLIS_EVEN; WALLIS_ODD] THEN
 418   REWRITE_TAC[real_div; REAL_INV_MUL; GSYM REAL_POW_INV; REAL_INV_INV] THEN
 419   REAL_ARITH_TAC);;
 420
 421 let WALLIS_QUOTIENT' = prove
 422  (`!n. integral(&0,pi / &2) (\x. sin(x) pow (2 * n)) /
 423        integral(&0,pi / &2) (\x. sin(x) pow (2 * n + 1)) * &2 / pi =
 424          (&(FACT(2 * n)) * &(FACT(2 * n + 1))) / (&2 pow n * &(FACT n)) pow 4`,
 425   GEN_TAC THEN REWRITE_TAC[WALLIS_QUOTIENT] THEN
 426   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV) [GSYM REAL_INV_DIV] THEN
 427   REWRITE_TAC[GSYM real_div] THEN MATCH_MP_TAC REAL_DIV_RMUL THEN
 428   MP_TAC PI2_NZ THEN CONV_TAC REAL_FIELD);;
 429
 430 let WALLIS_MONO = prove
 431  (`!m n. m <= n
 432          ==> integral(&0,pi / &2) (\x. sin(x) pow n)
 433                 <= integral(&0,pi / &2) (\x. sin(x) pow m)`,
 434   REWRITE_TAC[LE_EXISTS] THEN REPEAT STRIP_TAC THEN
 435   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INTEGRAL_LE THEN
 436   CONV_TAC(ONCE_DEPTH_CONV INTEGRABLE_CONV) THEN REWRITE_TAC[PI2_LE] THEN
 437   REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_POW_ADD] THEN
 438   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
 439   MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL
 440    [MATCH_MP_TAC REAL_POW_LE; MATCH_MP_TAC REAL_POW_1_LE] THEN
 441   REWRITE_TAC[SIN_BOUNDS] THEN
 442   (MP_TAC(SPEC `x:real` SIN_POS_PI_LE) THEN
 443    ANTS_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
 444    REPEAT(POP_ASSUM MP_TAC) THEN MP_TAC PI2_LT THEN REAL_ARITH_TAC));;
 445
 446 let WALLIS_LT = prove
 447  (`!n. &0 < integral(&0,pi / &2) (\x. sin(x) pow n)`,
 448   MATCH_MP_TAC ODDEVEN_INDUCT THEN
 449   REWRITE_TAC[WALLIS_0; WALLIS_1; PI2_LT; REAL_OF_NUM_LT; ARITH] THEN
 450   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[WALLIS_PARTS'] THEN
 451   MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[] THEN
 452   MATCH_MP_TAC REAL_LT_DIV THEN REAL_ARITH_TAC);;
 453
 454 let WALLIS_NZ = prove
 455  (`!n. ~(integral(&0,pi / &2) (\x. sin(x) pow n) = &0)`,
 456   MP_TAC WALLIS_LT THEN MATCH_MP_TAC MONO_FORALL THEN REAL_ARITH_TAC);;
 457
 458 let WALLIS_BOUNDS = prove
 459  (`!n. integral(&0,pi / &2) (\x. sin(x) pow (n + 1))
 460         <= integral(&0,pi / &2) (\x. sin(x) pow n) /\
 461        integral(&0,pi / &2) (\x. sin(x) pow n) <=
 462         (&n + &2) / (&n + &1) * integral(&0,pi / &2) (\x. sin(x) pow (n + 1))`,
 463   GEN_TAC THEN SIMP_TAC[WALLIS_MONO; LE_ADD] THEN
 464   MATCH_MP_TAC REAL_LE_TRANS THEN
 465   EXISTS_TAC `(&n + &2) / (&n + &1) *
 466               integral (&0,pi / &2) (\x. sin x pow (n + 2))` THEN
 467   CONJ_TAC THENL
 468    [REWRITE_TAC[WALLIS_PARTS'] THEN
 469     MATCH_MP_TAC REAL_EQ_IMP_LE THEN CONV_TAC REAL_FIELD;
 470     ALL_TAC] THEN
 471   MATCH_MP_TAC REAL_LE_LMUL THEN
 472   SIMP_TAC[WALLIS_MONO; ARITH_RULE `n + 1 <= n + 2`] THEN
 473   MATCH_MP_TAC REAL_LE_DIV THEN REAL_ARITH_TAC);;
 474
 475 let WALLIS_RATIO_BOUNDS = prove
 476  (`!n. &1 <= integral(&0,pi / &2) (\x. sin(x) pow n) /
 477             integral(&0,pi / &2) (\x. sin(x) pow (n + 1)) /\
 478       integral(&0,pi / &2) (\x. sin(x) pow n) /
 479       integral(&0,pi / &2) (\x. sin(x) pow (n + 1)) <= (&n + &2) / (&n + &1)`,
 480   GEN_TAC THEN CONJ_TAC THENL
 481    [SIMP_TAC[REAL_LE_RDIV_EQ; WALLIS_LT; REAL_MUL_LID; WALLIS_BOUNDS];
 482     SIMP_TAC[REAL_LE_LDIV_EQ; WALLIS_LT; WALLIS_BOUNDS]]);;
 483
 484 let WALLIS = prove
 485  (`(\n. (&2 pow n * &(FACT n)) pow 4 / (&(FACT(2 * n)) * &(FACT(2 * n + 1))))
 486    --> pi / &2`,
 487   ONCE_REWRITE_TAC[GSYM REAL_INV_DIV] THEN MATCH_MP_TAC SEQ_INV THEN
 488   CONJ_TAC THENL [ALL_TAC; MP_TAC PI2_NZ THEN CONV_TAC REAL_FIELD] THEN
 489   REWRITE_TAC[GSYM WALLIS_QUOTIENT'] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 490   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
 491   MATCH_MP_TAC SEQ_MUL THEN REWRITE_TAC[SEQ_CONST] THEN
 492   GEN_REWRITE_TAC (LAND_CONV o ABS_CONV) [REAL_ARITH `x = (x - &1) + &1`] THEN
 493   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_ADD_LID] THEN
 494   MATCH_MP_TAC SEQ_ADD THEN REWRITE_TAC[SEQ_CONST] THEN
 495   MATCH_MP_TAC SEQ_LE_0 THEN EXISTS_TAC `\n. &1 / &n` THEN
 496   REWRITE_TAC[SEQ_HARMONIC] THEN EXISTS_TAC `1` THEN
 497   REWRITE_TAC[GE] THEN REPEAT STRIP_TAC THEN
 498   MATCH_MP_TAC(REAL_ARITH
 499    `!d. &1 <= x /\ x <= d /\ d - &1 <= e ==> abs(x - &1) <= e`) THEN
 500   EXISTS_TAC `(&(2 * n) + &2) / (&(2 * n) + &1)` THEN
 501   REWRITE_TAC[WALLIS_RATIO_BOUNDS] THEN
 502   REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
 503   REWRITE_TAC[REAL_FIELD
 504    `(&2 * &n + &2) / (&2 * &n + &1) - &1 = &1 / (&2 * &n + &1)`] THEN
 505   REWRITE_TAC[real_div; REAL_MUL_LID; REAL_ABS_INV; REAL_ABS_NUM] THEN
 506   MATCH_MP_TAC REAL_LE_INV2 THEN POP_ASSUM MP_TAC THEN
 507   REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN REAL_ARITH_TAC);;
 508
 509 (* ------------------------------------------------------------------------- *)
 510 (* Hence determine the actual value of the limit.                            *)
 511 (* ------------------------------------------------------------------------- *)
 512
 513 let LN_WALLIS = prove
 514  (`(\n. &4 * &n * ln(&2) + &4 * ln(&(FACT n)) -
 515         (ln(&(FACT(2 * n))) + ln(&(FACT(2 * n + 1))))) --> ln(pi / &2)`,
 516   REWRITE_TAC[REAL_ARITH `&4 * x + &4 * y - z = &4 * (x + y) - z`] THEN
 517   SUBGOAL_THEN `!n. &0 < &2 pow n`
 518    (fun th -> SIMP_TAC[th; GSYM LN_POW; REAL_OF_NUM_LT; ARITH; GSYM LN_MUL;
 519                        FACT_LT; REAL_POW_LT; REAL_LT_MUL; GSYM LN_DIV]) THEN
 520   SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
 521   MATCH_MP_TAC CONTL_SEQ THEN REWRITE_TAC[WALLIS] THEN
 522   MATCH_MP_TAC DIFF_CONT THEN EXISTS_TAC `inv(pi / &2)` THEN
 523   MP_TAC(SPEC `pi / &2` (DIFF_CONV `\x. ln(x)`)) THEN
 524   SIMP_TAC[ETA_AX; PI2_LT; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
 525   REWRITE_TAC[REAL_MUL_RID]);;
 526
 527 let STIRLING = prove
 528  (`(\n. ln(&(FACT n)) - ((&n + &1 / &2) * ln(&n) - &n + ln(&2 * pi) / &2))
 529    --> &0`,
 530   REWRITE_TAC[REAL_ARITH `a - (b - c + d) = (a - (b - c)) - d`] THEN
 531   SUBST1_TAC(SYM(SPEC `ln(&2 * pi) / &2` REAL_SUB_REFL)) THEN
 532   MATCH_MP_TAC SEQ_SUB THEN REWRITE_TAC[SEQ_CONST] THEN
 533   X_CHOOSE_THEN `C:real` MP_TAC STIRLING_CONVERGES THEN
 534   GEN_REWRITE_TAC (funpow 2 LAND_CONV) [GSYM ETA_AX] THEN
 535   REWRITE_TAC[stirling] THEN DISCH_TAC THEN
 536   FIRST_ASSUM(MP_TAC o SPECL [`2`; `1`] o MATCH_MP SEQ_SUBSEQ) THEN
 537   FIRST_ASSUM(MP_TAC o SPECL [`2`; `0`] o MATCH_MP SEQ_SUBSEQ) THEN
 538   REWRITE_TAC[ARITH; ADD_CLAUSES; IMP_IMP] THEN
 539   DISCH_THEN(MP_TAC o MATCH_MP SEQ_ADD) THEN
 540   FIRST_ASSUM(MP_TAC o MATCH_MP SEQ_MUL o CONJ (SPEC `&4` SEQ_CONST)) THEN
 541   REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP SEQ_SUB) THEN
 542   MP_TAC LN_WALLIS THEN REWRITE_TAC[IMP_IMP] THEN
 543   DISCH_THEN(MP_TAC o MATCH_MP SEQ_SUB) THEN
 544   REWRITE_TAC[ARITH_RULE
 545    `(a + &4 * x - (y + z)) - (&4 * (x - b) - ((y - c) + (z - d))) =
 546     (a + &4 * b) - (c + d)`] THEN
 547   DISCH_THEN(fun th -> POP_ASSUM MP_TAC THEN ASSUME_TAC th) THEN
 548   SUBGOAL_THEN `C = ln(&2 * pi) / &2` (fun th -> REWRITE_TAC[th]) THEN
 549   POP_ASSUM(MP_TAC o CONJ (SPEC `&2 * ln(&2)` SEQ_CONST)) THEN
 550   DISCH_THEN(MP_TAC o MATCH_MP SEQ_ADD) THEN
 551   SIMP_TAC[LN_DIV; PI_POS; REAL_OF_NUM_LT; ARITH; LN_MUL] THEN
 552   REWRITE_TAC[REAL_ARITH `&2 * l + p - l - (&4 * C - (C + C)) =
 553                           (l + p) - &2 * C`] THEN
 554   SIMP_TAC[REAL_ARITH `C = (l + p) / &2 <=> (l + p) - &2 * C = &0`] THEN
 555   MATCH_MP_TAC(REWRITE_RULE[TAUT `a /\ b ==> c <=> b ==> a ==> c`]
 556     SEQ_UNIQ) THEN
 557   REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
 558   REWRITE_TAC[REAL_ARITH
 559    `a + (b + &4 * (c - x)) - ((d - &2 * x) + (e - (&2 * x + &1))) =
 560     (a + b + &4 * c + &1) - (d + e)`] THEN
 561   REWRITE_TAC[REAL_ARITH `&2 * l + &4 * n * l + &4 * (n + &1 / &2) * x + &1 =
 562                           (&4 * n + &2) * (l + x) + &1`] THEN
 563   ONCE_REWRITE_TAC[SEQ_SUC] THEN
 564   SIMP_TAC[GSYM LN_MUL; REAL_OF_NUM_LT; ARITH; LT_0] THEN
 565   REWRITE_TAC[GSYM SEQ_SUC] THEN
 566   CONV_TAC(LAND_CONV(GEN_ALPHA_CONV `n:num`)) THEN
 567   REWRITE_TAC[REAL_ARITH
 568    `((&4 * n + &2) * l + &1) - ((&2 * n + &1 / &2) * l + z) =
 569     (&2 * n + &3 / &2) * l + &1 - z`] THEN
 570   REWRITE_TAC[REAL_ARITH
 571    `(&2 * n + &3 / &2) * l + &1 - ((&2 * n + &1) + &1 / &2) * l' =
 572     (&2 * n + &3 / &2) * (l - l') + &1`] THEN
 573   GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `&0 = -- &1 + &1`] THEN
 574   MATCH_MP_TAC SEQ_ADD THEN REWRITE_TAC[SEQ_CONST] THEN
 575   ONCE_REWRITE_TAC[REAL_ARITH `a * (b - c) = --(a * (c - b))`] THEN
 576   REWRITE_TAC[GSYM SEQ_NEG] THEN
 577   ONCE_REWRITE_TAC[SEQ_SUC] THEN
 578   SIMP_TAC[GSYM LN_DIV; REAL_LT_MUL; REAL_OF_NUM_LT; LT_0; ARITH;
 579            REAL_ARITH `&0 < &2 * &n + &1`] THEN
 580   SIMP_TAC[REAL_OF_NUM_LT; LT_0; REAL_FIELD
 581    `&0 < x ==> (&2 * x + &1) / (&2 * x) = &1 + &1 / (&2 * x)`] THEN
 582   REWRITE_TAC[GSYM SEQ_SUC] THEN
 583   CONV_TAC(LAND_CONV(GEN_ALPHA_CONV `n:num`)) THEN
 584   MP_TAC SEQ_SUBSEQ THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
 585   DISCH_THEN(MP_TAC o GENL [`f:num->real`; `l:real`] o
 586    SPECL [`f:num->real`; `l:real`; `2`; `0`]) THEN
 587   REWRITE_TAC[ADD_CLAUSES; ARITH; REAL_OF_NUM_MUL] THEN
 588   DISCH_THEN MATCH_MP_TAC THEN CONV_TAC(LAND_CONV(GEN_ALPHA_CONV `n:num`)) THEN
 589   REWRITE_TAC[REAL_ADD_RDISTRIB] THEN
 590   GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `&1 = &1 + &3 / &2 * &0`] THEN
 591   MATCH_MP_TAC SEQ_ADD THEN REWRITE_TAC[LN_LIM_LEMMA] THEN
 592   MATCH_MP_TAC SEQ_MUL THEN REWRITE_TAC[SEQ_CONST] THEN
 593   MP_TAC LN_LIM_LEMMA THEN MP_TAC(SPEC `&1` SEQ_HARMONIC) THEN
 594   REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP SEQ_MUL) THEN
 595   REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SEQ_SUC] THEN
 596   SIMP_TAC[real_div; REAL_MUL_LID; REAL_MUL_ASSOC; REAL_MUL_LINV;
 597            REAL_MUL_RID; REAL_OF_NUM_EQ; NOT_SUC]);;