100/leibniz.ml

   1 (* ========================================================================= *)
   2 (* #26: Leibniz's series for pi                                              *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/transc.ml";;
   6
   7 prioritize_real();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Summability of alternating series.                                        *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let ALTERNATING_SUM_BOUNDS = prove
  14  (`!a. (!n. a(2 * n + 1) <= &0 /\ &0 <= a(2 * n)) /\
  15        (!n. abs(a(n + 1)) <= abs(a(n)))
  16        ==> !m n. (EVEN m ==> &0 <= sum(m,n) a /\ sum(m,n) a <= a(m)) /\
  17                  (ODD m ==> a(m) <= sum(m,n) a /\ sum(m,n) a <= &0)`,
  18   GEN_TAC THEN STRIP_TAC THEN
  19   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
  20   INDUCT_TAC THEN REWRITE_TAC[ODD; EVEN] THENL
  21    [SIMP_TAC[sum; ODD_EXISTS; EVEN_EXISTS; LEFT_IMP_EXISTS_THM; ADD1] THEN
  22     ASM_SIMP_TAC[REAL_LE_REFL];
  23     ALL_TAC] THEN
  24   X_GEN_TAC `m:num` THEN
  25   REWRITE_TAC[ARITH_RULE `SUC n = 1 + n`; GSYM SUM_SPLIT] THEN
  26   FIRST_X_ASSUM(MP_TAC o check (is_conj o concl) o SPEC `SUC m`) THEN
  27   REWRITE_TAC[ODD; EVEN; SUM_1] THEN REWRITE_TAC[ADD1; GSYM NOT_EVEN] THEN
  28   UNDISCH_THEN `!n. abs(a(n + 1)) <= abs(a n)` (MP_TAC o SPEC `m:num`) THEN
  29   ASM_CASES_TAC `EVEN m` THEN ASM_REWRITE_TAC[] THENL
  30    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN
  31     DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST_ALL_TAC) THEN
  32     FIRST_X_ASSUM(MP_TAC o SPEC `p:num`) THEN REAL_ARITH_TAC;
  33     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EVEN]) THEN
  34     REWRITE_TAC[ODD_EXISTS] THEN
  35     DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST_ALL_TAC) THEN
  36     REWRITE_TAC[ADD1] THEN
  37     FIRST_X_ASSUM(MP_TAC o SPEC `p:num`) THEN REAL_ARITH_TAC]);;
  38
  39 let ALTERNATING_SUM_BOUND = prove
  40  (`!a. (!n. a(2 * n + 1) <= &0 /\ &0 <= a(2 * n)) /\
  41        (!n. abs(a(n + 1)) <= abs(a(n)))
  42        ==> !m n. abs(sum(m,n) a) <= abs(a m)`,
  43   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP ALTERNATING_SUM_BOUNDS) THEN
  44   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
  45   REWRITE_TAC[GSYM NOT_EVEN] THEN ASM_CASES_TAC `EVEN m` THEN
  46   ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
  47
  48 let SUMMABLE_ALTERNATING = prove
  49  (`!v. (!n. a(2 * n + 1) <= &0 /\ &0 <= a(2 * n)) /\
  50        (!n. abs(a(n + 1)) <= abs(a(n))) /\ a tends_num_real &0
  51        ==> summable a`,
  52   REPEAT STRIP_TAC THEN REWRITE_TAC[SER_CAUCHY] THEN
  53   X_GEN_TAC `e:real` THEN STRIP_TAC THEN
  54   FIRST_X_ASSUM(MP_TAC o SPEC `e:real` o GEN_REWRITE_RULE I [SEQ]) THEN
  55   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
  56   REWRITE_TAC[REAL_SUB_RZERO] THEN
  57   ASM_MESON_TAC[ALTERNATING_SUM_BOUND; REAL_LET_TRANS]);;
  58
  59 (* ------------------------------------------------------------------------- *)
  60 (* Another version of the atan series.                                       *)
  61 (* ------------------------------------------------------------------------- *)
  62
  63 let REAL_ATN_POWSER_ALT = prove
  64  (`!x. abs(x) < &1
  65        ==> (\n. (-- &1) pow n / &(2 * n + 1) * x pow (2 * n + 1))
  66            sums (atn x)`,
  67   REPEAT STRIP_TAC THEN
  68   FIRST_ASSUM(ASSUME_TAC o MATCH_MP REAL_ATN_POWSER) THEN
  69   FIRST_ASSUM(MP_TAC o C CONJ (ARITH_RULE `0 < 2`) o
  70               MATCH_MP SUM_SUMMABLE) THEN
  71   DISCH_THEN(MP_TAC o MATCH_MP SER_GROUP) THEN
  72   FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP SUM_UNIQ) THEN
  73   REWRITE_TAC[SUM_2; EVEN_MULT; EVEN_ADD; ARITH_EVEN; ADD_SUB] THEN
  74   ONCE_REWRITE_TAC[ARITH_RULE `n * 2 = 2 * n`] THEN
  75   SIMP_TAC[DIV_MULT; ARITH_EQ; REAL_MUL_LZERO; REAL_ADD_LID]);;
  76
  77 (* ------------------------------------------------------------------------- *)
  78 (* Summability of the same series for x = 1.                                 *)
  79 (* ------------------------------------------------------------------------- *)
  80
  81 let SUMMABLE_LEIBNIZ = prove
  82  (`summable (\n. (-- &1) pow n / &(2 * n + 1))`,
  83   MATCH_MP_TAC SUMMABLE_ALTERNATING THEN
  84   REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
  85    [REWRITE_TAC[REAL_POW_ADD; REAL_POW_MUL; GSYM REAL_POW_POW] THEN
  86     CONV_TAC REAL_RAT_REDUCE_CONV THEN
  87     REWRITE_TAC[REAL_POW_ONE; real_div; REAL_MUL_LID; REAL_MUL_LNEG] THEN
  88     REWRITE_TAC[REAL_LE_LNEG; REAL_ADD_RID; REAL_LE_INV_EQ; REAL_POS];
  89     GEN_TAC THEN REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NEG] THEN
  90     REWRITE_TAC[REAL_ABS_NUM; REAL_POW_ONE; real_div; REAL_MUL_LID] THEN
  91     MATCH_MP_TAC REAL_LE_INV2 THEN
  92     REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN ARITH_TAC;
  93     REWRITE_TAC[SEQ; REAL_SUB_RZERO; REAL_ABS_DIV; REAL_ABS_POW] THEN
  94     REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM; REAL_POW_ONE] THEN
  95     SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH_RULE `0 < n + 1`] THEN
  96     GEN_TAC THEN DISCH_TAC THEN
  97     FIRST_ASSUM(MP_TAC o SPEC `&1` o MATCH_MP REAL_ARCH) THEN
  98     MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[GE] THEN REPEAT STRIP_TAC THEN
  99     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 100      `&1 < x * e ==> e * x <= y ==> &1 < y`)) THEN
 101     ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_OF_NUM_LE] THEN
 102     ASM_ARITH_TAC]);;
 103
 104 (* ------------------------------------------------------------------------- *)
 105 (* The tricky sum-bounding lemma.                                            *)
 106 (* ------------------------------------------------------------------------- *)
 107
 108 let SUM_DIFFERENCES = prove
 109  (`!a m n. m <= n + 1 ==> sum(m..n) (\i. a(i) - a(i+1)) = a(m) - a(n + 1)`,
 110   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THENL
 111    [REWRITE_TAC[ARITH_RULE `m <= 0 + 1 <=> m = 0 \/ m = 1`] THEN
 112     STRIP_TAC THEN ASM_REWRITE_TAC[SUM_SING_NUMSEG] THEN
 113     ASM_SIMP_TAC[SUM_TRIV_NUMSEG; ARITH; REAL_SUB_REFL];
 114     ALL_TAC] THEN
 115   REWRITE_TAC[ARITH_RULE `m <= SUC n + 1 <=> m <= n + 1 \/ m = SUC n + 1`] THEN
 116   STRIP_TAC THEN
 117   ASM_SIMP_TAC[SUM_TRIV_NUMSEG; ARITH_RULE `n < n + 1`; REAL_SUB_REFL] THEN
 118   ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG;
 119     ARITH_RULE `m <= n + 1 ==> m <= SUC n /\ m <= SUC n + 1`] THEN
 120   REWRITE_TAC[ADD1] THEN REAL_ARITH_TAC);;
 121
 122 let SUM_REARRANGE_LEMMA = prove
 123  (`!a v m n.
 124         m <= n + 1
 125         ==> sum(m..n+1) (\i. a i * v i) =
 126             sum(m..n) (\k. sum(m..k) a * (v(k) - v(k+1))) +
 127             sum(m..n+1) a * v(n+1)`,
 128   REPLICATE_TAC 3 GEN_TAC THEN INDUCT_TAC THENL
 129    [REWRITE_TAC[SUM_CLAUSES_NUMSEG; num_CONV `1`; ADD_CLAUSES] THEN
 130     ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[ARITH] THEN REAL_ARITH_TAC;
 131     ALL_TAC] THEN
 132   REWRITE_TAC[ADD_CLAUSES; SUM_CLAUSES_NUMSEG] THEN
 133   DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN
 134   ASM_CASES_TAC `m = SUC(n + 1)` THENL
 135    [ASM_REWRITE_TAC[LE_SUC; ARITH_RULE `~(n + 1 <= n)`] THEN
 136     ASM_SIMP_TAC[SUM_TRIV_NUMSEG; ARITH_RULE
 137      `n < SUC n /\ n < SUC(n + 1)`] THEN
 138     REAL_ARITH_TAC;
 139     ALL_TAC] THEN
 140   ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 141   DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[] THEN
 142   ONCE_REWRITE_TAC[ARITH_RULE
 143    `m <= SUC n <=> m <= SUC(n + 1) /\ ~(m = SUC(n + 1))`] THEN
 144   ASM_REWRITE_TAC[] THEN
 145   REWRITE_TAC[GSYM REAL_ADD_ASSOC; REAL_EQ_ADD_LCANCEL] THEN
 146   REWRITE_TAC[REAL_ADD_ASSOC; REAL_ADD_RDISTRIB; REAL_EQ_ADD_RCANCEL] THEN
 147   REWRITE_TAC[GSYM ADD1; SUM_CLAUSES_NUMSEG] THEN
 148   ASM_SIMP_TAC[ARITH_RULE
 149    `m <= SUC(n + 1) /\ ~(m = SUC(n + 1)) ==> m <= SUC n`] THEN
 150   REWRITE_TAC[REAL_ARITH
 151    `(s1 * (v - w) + x) + (s2 + y) * w =
 152     (x + y * w) + (v - w) * s1 + w * s2`] THEN
 153   GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
 154   SIMP_TAC[REAL_ADD_LDISTRIB; GSYM SUM_CMUL; GSYM SUM_ADD_NUMSEG] THEN
 155   REWRITE_TAC[REAL_SUB_ADD; REAL_SUB_RDISTRIB] THEN REAL_ARITH_TAC);;
 156
 157 let SUM_BOUNDS_LEMMA = prove
 158  (`!a v l u m n.
 159         m <= n /\
 160         (!i. m <= i /\ i <= n ==> &0 <= v(i) /\ v(i+1) <= v(i)) /\
 161         (!k. m <= k /\ k <= n ==> l <= sum(m..k) a /\ sum(m..k) a <= u)
 162         ==> l * v(m) <= sum(m..n) (\i. a(i) * v(i)) /\
 163             sum(m..n) (\i. a(i) * v(i)) <= u * v(m)`,
 164   REPLICATE_TAC 5 GEN_TAC THEN INDUCT_TAC THENL
 165    [REWRITE_TAC[LE; SUM_CLAUSES_NUMSEG] THEN
 166     SIMP_TAC[ARITH_RULE `m <= i /\ i = 0 <=> m = 0 /\ i = 0`] THEN
 167     REWRITE_TAC[LEFT_FORALL_IMP_THM; RIGHT_EXISTS_AND_THM; EXISTS_REFL] THEN
 168     ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[SUM_SING_NUMSEG] THEN
 169     SIMP_TAC[REAL_LE_RMUL];
 170     POP_ASSUM(K ALL_TAC) THEN REWRITE_TAC[ADD1]] THEN
 171   SIMP_TAC[SUM_REARRANGE_LEMMA] THEN STRIP_TAC THEN CONJ_TAC THENL
 172    [MATCH_MP_TAC REAL_LE_TRANS THEN
 173     EXISTS_TAC `sum(m..n) (\k. l * (v(k) - v(k + 1))) + l * v(n+1)` THEN
 174     CONJ_TAC THENL
 175      [ASM_SIMP_TAC[SUM_LMUL; SUM_DIFFERENCES] THEN REAL_ARITH_TAC;
 176       ALL_TAC];
 177     MATCH_MP_TAC REAL_LE_TRANS THEN
 178     EXISTS_TAC `sum(m..n) (\k. u * (v(k) - v(k + 1))) + u * v(n+1)` THEN
 179     CONJ_TAC THENL
 180      [ALL_TAC;
 181       ASM_SIMP_TAC[SUM_LMUL; SUM_DIFFERENCES] THEN REAL_ARITH_TAC]] THEN
 182   MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_SIMP_TAC[REAL_LE_RMUL; LE_REFL] THEN
 183   MATCH_MP_TAC SUM_LE_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
 184   REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
 185   ASM_SIMP_TAC[REAL_SUB_LE; ARITH_RULE `k <= n ==> k <= n + 1`]);;
 186
 187 let SUM_BOUND_LEMMA = prove
 188  (`!a v b m n.
 189         m <= n /\
 190         (!i. m <= i /\ i <= n ==> &0 <= v(i) /\ v(i+1) <= v(i)) /\
 191         (!k. m <= k /\ k <= n ==> abs(sum(m..k) a) <= b)
 192         ==> abs(sum(m..n) (\i. a(i) * v(i))) <= b * abs(v m)`,
 193   REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
 194    `--b * k <= a /\ a <= b * k ==> abs(a) <= b * k`) THEN
 195   ASM_SIMP_TAC[LE_REFL; real_abs] THEN
 196   MATCH_MP_TAC SUM_BOUNDS_LEMMA THEN
 197   ASM_REWRITE_TAC[REAL_BOUNDS_LE]);;
 198
 199 (* ------------------------------------------------------------------------- *)
 200 (* Hence the final theorem.                                                  *)
 201 (* ------------------------------------------------------------------------- *)
 202
 203 let LEIBNIZ_PI = prove
 204  (`(\n. (-- &1) pow n / &(2 * n + 1)) sums (pi / &4)`,
 205   REWRITE_TAC[GSYM ATN_1] THEN
 206   ASSUME_TAC(MATCH_MP SUMMABLE_SUM SUMMABLE_LEIBNIZ) THEN
 207   ABBREV_TAC `s = suminf(\n. (-- &1) pow n / &(2 * n + 1))` THEN
 208   SUBGOAL_THEN `s = atn(&1)` (fun th -> ASM_MESON_TAC[th]) THEN
 209   MATCH_MP_TAC(REAL_ARITH `~(&0 < abs(x - y)) ==> x = y`) THEN
 210   ABBREV_TAC `e = abs(s - atn(&1))` THEN DISCH_TAC THEN
 211   FIRST_ASSUM(MP_TAC o MATCH_MP SUM_SUMMABLE) THEN
 212   REWRITE_TAC[SER_CAUCHY] THEN DISCH_THEN(MP_TAC o SPEC `e / &7`) THEN
 213   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
 214   DISCH_THEN(X_CHOOSE_THEN `N:num` STRIP_ASSUME_TAC) THEN
 215   SUBGOAL_THEN
 216    `(\x. sum(0,N) (\n. (-- &1) pow n / &(2 * n + 1) * x pow (2 * n + 1)))
 217     contl (&1)`
 218   MP_TAC THENL
 219    [MATCH_MP_TAC DIFF_CONT THEN EXISTS_TAC
 220      `sum(0,N) (\n. (-- &1) pow n * &1 pow (2 * n))` THEN
 221     MATCH_MP_TAC DIFF_SUM THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
 222     REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
 223     MATCH_MP_TAC DIFF_CMUL THEN
 224     MP_TAC(SPECL [`2 * k + 1`; `&1`] DIFF_POW) THEN
 225     DISCH_THEN(MP_TAC o SPEC `inv(&(2 * k + 1))` o MATCH_MP DIFF_CMUL) THEN
 226     MATCH_MP_TAC(TAUT `a = b ==> a ==> b`) THEN
 227     REWRITE_TAC[ADD_SUB] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
 228     REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
 229     REWRITE_TAC[REAL_POW_ONE] THEN CONV_TAC REAL_FIELD;
 230     ALL_TAC] THEN
 231   SUBGOAL_THEN `atn contl (&1)` MP_TAC THENL
 232    [MESON_TAC[DIFF_CONT; DIFF_ATN]; ALL_TAC] THEN
 233   REWRITE_TAC[CONTL_LIM; LIM] THEN
 234   REWRITE_TAC[TAUT `a ==> ~b <=> ~(a /\ b)`; AND_FORALL_THM] THEN
 235   DISCH_THEN(MP_TAC o SPEC `e / &6`) THEN
 236   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH; GSYM SUM_SUB] THEN
 237   ONCE_REWRITE_TAC[GSYM REAL_ABS_NEG] THEN
 238   REWRITE_TAC[GSYM SUM_NEG; REAL_NEG_SUB; GSYM REAL_MUL_RNEG] THEN
 239   REWRITE_TAC[REAL_POW_ONE; GSYM REAL_SUB_LDISTRIB] THEN DISCH_THEN
 240    (CONJUNCTS_THEN2 (X_CHOOSE_THEN `d1:real` STRIP_ASSUME_TAC)
 241                     (X_CHOOSE_THEN `d2:real` STRIP_ASSUME_TAC)) THEN
 242   ABBREV_TAC `x = &1 - min (min (d1 / &2) (d2 / &2)) (&1 / &2)` THEN
 243   REPEAT(FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN ANTS_TAC THENL
 244           [ASM_REAL_ARITH_TAC; DISCH_TAC]) THEN
 245   SUBGOAL_THEN `&0 < x /\ x < &1 /\ abs x < &1` STRIP_ASSUME_TAC THENL
 246    [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 247   FIRST_X_ASSUM(MP_TAC o MATCH_MP REAL_ATN_POWSER_ALT) THEN
 248   REWRITE_TAC[sums; SEQ] THEN DISCH_THEN(MP_TAC o SPEC `e / &6`) THEN
 249   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
 250   DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN
 251   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [sums]) THEN
 252   REWRITE_TAC[SEQ] THEN DISCH_THEN(MP_TAC o SPEC `e / &6`) THEN
 253   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
 254   DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN
 255   REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `N + N1 + N2:num`) THEN
 256          ANTS_TAC THENL [ARITH_TAC; ALL_TAC]) THEN
 257   REWRITE_TAC[] THEN ONCE_REWRITE_TAC[GSYM SUM_SPLIT] THEN
 258   REWRITE_TAC[ADD_CLAUSES] THEN REPEAT STRIP_TAC THEN
 259   SUBGOAL_THEN
 260    `abs(sum(N,N1+N2) (\n. -- &1 pow n / &(2 * n + 1) * x pow (2 * n + 1)))
 261      < e / &6`
 262   ASSUME_TAC THENL
 263    [ASM_CASES_TAC `N1 + N2 = 0` THENL
 264      [ASM_SIMP_TAC[sum; REAL_LT_DIV; REAL_OF_NUM_LT; REAL_ABS_NUM; ARITH];
 265       ALL_TAC] THEN
 266     MATCH_MP_TAC(REAL_ARITH `x <= e / &7 /\ &0 < e ==> x < e / &6`) THEN
 267     ASM_REWRITE_TAC[] THEN
 268     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
 269      `e / &7 * abs(x pow (2 * N + 1))` THEN
 270     CONJ_TAC THENL
 271      [ALL_TAC;
 272       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
 273       MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 274       ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
 275       REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NUM] THEN
 276       MATCH_MP_TAC REAL_POW_1_LE THEN
 277       MAP_EVERY UNDISCH_TAC [`&0 < x`; `x < &1`] THEN REAL_ARITH_TAC] THEN
 278     ASM_SIMP_TAC[PSUM_SUM_NUMSEG] THEN MATCH_MP_TAC SUM_BOUND_LEMMA THEN
 279     CONJ_TAC THENL [UNDISCH_TAC `~(N1 + N2 = 0)` THEN ARITH_TAC; ALL_TAC] THEN
 280     REPEAT STRIP_TAC THENL
 281      [ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_POW_LT];
 282       REWRITE_TAC[ARITH_RULE `2 * (m + 1) + 1 = (2 * m + 1) + 2`] THEN
 283       GEN_REWRITE_TAC LAND_CONV [REAL_POW_ADD] THEN
 284       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
 285       MATCH_MP_TAC REAL_LE_LMUL THEN
 286       ASM_SIMP_TAC[REAL_POW_LE; REAL_POW_1_LE; REAL_LT_IMP_LE];
 287       MATCH_MP_TAC REAL_LT_IMP_LE THEN
 288       FIRST_X_ASSUM(MP_TAC o SPECL [`N:num`; `(k - N:num) + 1`]) THEN
 289       SIMP_TAC[PSUM_SUM_NUMSEG; ADD_EQ_0; ARITH_EQ] THEN
 290       ASM_SIMP_TAC[ARITH_RULE `N <= k ==> (N + (k - N) + 1) - 1 = k`] THEN
 291       REWRITE_TAC[GE; LE_REFL; REAL_LT_IMP_LE]];
 292     ALL_TAC] THEN
 293   FIRST_X_ASSUM(MP_TAC o SPECL [`N:num`; `N1 + N2:num`]) THEN
 294   REWRITE_TAC[GE; LE_REFL] THEN
 295   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 296    `abs((slo + shi) - s) < e / &6
 297     ==> ~(abs(slo - s) < e / &3) ==> ~(abs(shi) < e / &7)`)) THEN
 298   RULE_ASSUM_TAC(REWRITE_RULE[REAL_SUB_LDISTRIB; SUM_SUB; REAL_MUL_RID]) THEN
 299   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 300    `abs(s1 - sx) < e / &6
 301     ==> ~(abs(sx - s) < e / &2) ==> ~(abs(s1 - s) < e / &3)`)) THEN
 302   ASM_REAL_ARITH_TAC);;