Examples/polylog.ml

   1 (* ========================================================================= *)
   2 (* Pi series in Bailey/Borwein/Plouffe "polylogarithmic constants" paper.    *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/transc.ml";;
   6
   7 let FACTOR_1X4_LEMMA = prove
   8  (`!x. (x * x + x * sqrt (&2) + &1) * (x * x - x * sqrt (&2) + &1) =
   9        &1 + x pow 4`,
  10   REWRITE_TAC[REAL_ARITH
  11    `(a + b + c) * (a - b + c) = &2 * a * c + a * a - b * b + c * c`] THEN
  12   REWRITE_TAC[REAL_ARITH
  13    `&2 * (x * x) * &1 + a - (x * s) * x * s + &1 * &1 =
  14    (&2 - s * s) * x * x + (&1 + a)`] THEN
  15   SIMP_TAC[REWRITE_RULE[REAL_POW_2] SQRT_POW_2; REAL_POS] THEN
  16   REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_LZERO; REAL_ADD_LID] THEN
  17   SUBST1_TAC(SYM(NUM_REDUCE_CONV `SUC(SUC(SUC(SUC 0)))`)) THEN
  18   REWRITE_TAC[real_pow; REAL_MUL_ASSOC; REAL_MUL_RID]);;
  19
  20 let MAGIC_DERIVATIVE = prove
  21  (`!x. abs(x) < &1
  22        ==> ((\x. ln((x - &1) pow 2) +
  23                  ln((x + &1) pow 2) +
  24                  ln((x pow 2 + x * sqrt(&2) + &1) /
  25                     (x pow 2 - x * sqrt(&2) + &1)) +
  26                  &2 * atn(x * sqrt(&2) + &1) +
  27                  &2 * atn(x * sqrt(&2) - &1) +
  28                  &2 * atn(x pow 2) -
  29                  ln(x pow 4 + &1))
  30             diffl ((&4 * sqrt(&2) -
  31                     &8 * x pow 3 -
  32                     &4 * sqrt(&2) * x pow 4 -
  33                     &8 * x pow 5) / (&1 - x pow 8)))(x)`,
  34   REPEAT STRIP_TAC THEN
  35   W(MP_TAC o SPEC `x:real` o DIFF_CONV o lhand o rator o snd) THEN
  36   REWRITE_TAC[IMP_IMP] THEN
  37   MATCH_MP_TAC(TAUT
  38    `a /\ (a ==> (b <=> c)) ==> (a ==> b) ==> c`) THEN
  39   CONJ_TAC THENL
  40    [REWRITE_TAC[GSYM CONJ_ASSOC] THEN
  41     MATCH_MP_TAC(TAUT
  42      `a /\ (a ==> c) /\ (a /\ c ==> b) /\ d /\ e
  43       ==> e /\ d /\ b /\ a /\ c`) THEN
  44     REPEAT CONJ_TAC THENL
  45      [MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> &0 < x + &1`) THEN
  46       SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 + 2`)) THEN
  47       REWRITE_TAC[REAL_POW_ADD; REAL_LE_SQUARE];
  48       GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [REAL_ADD_SYM] THEN
  49       ONCE_REWRITE_TAC[GSYM FACTOR_1X4_LEMMA] THEN
  50       DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_IMP_NZ) THEN
  51       SIMP_TAC[REAL_POW_2; REAL_ENTIRE; DE_MORGAN_THM];
  52       STRIP_TAC THEN
  53       MATCH_MP_TAC REAL_LTE_TRANS THEN
  54       EXISTS_TAC `inv((x pow 2 - x * sqrt (&2) + &1) *
  55                       (x pow 2 - x * sqrt (&2) + &1)) *
  56                   ((x pow 2 - x * sqrt (&2) + &1) *
  57                    (x pow 2 - x * sqrt (&2) + &1)) *
  58                   (x pow 2 + x * sqrt (&2) + &1) /
  59                   (x pow 2 - x * sqrt (&2) + &1)` THEN
  60       CONJ_TAC THENL
  61        [MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC THENL
  62          [REWRITE_TAC[REAL_LT_INV_EQ; GSYM REAL_POW_2] THEN
  63           ASM_REWRITE_TAC[REAL_ARITH `&0 < x <=> &0 <= x /\ ~(x = &0)`;
  64                           REAL_POW_EQ_0] THEN
  65           REWRITE_TAC[REAL_LE_SQUARE; REAL_POW_2]; ALL_TAC] THEN
  66         ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_DIV_LMUL] THEN
  67         ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
  68         REWRITE_TAC[REAL_POW_2; FACTOR_1X4_LEMMA] THEN
  69         MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> &0 < &1 + x`) THEN
  70         SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 + 2`)) THEN
  71         REWRITE_TAC[REAL_POW_ADD; REAL_LE_SQUARE];
  72         ALL_TAC] THEN
  73       ONCE_REWRITE_TAC[REAL_MUL_ASSOC] THEN
  74       ASM_SIMP_TAC[REAL_MUL_LINV; REAL_ENTIRE; DE_MORGAN_THM] THEN
  75       REWRITE_TAC[REAL_LE_REFL; REAL_MUL_LID];
  76       REWRITE_TAC[REAL_ARITH `&0 < x <=> &0 <= x /\ ~(x = &0)`] THEN
  77       REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE; REAL_ENTIRE] THEN
  78       UNDISCH_TAC `abs(x) < &1` THEN REAL_ARITH_TAC;
  79       REWRITE_TAC[REAL_ARITH `&0 < x <=> &0 <= x /\ ~(x = &0)`] THEN
  80       REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE; REAL_ENTIRE] THEN
  81       UNDISCH_TAC `abs(x) < &1` THEN REAL_ARITH_TAC];
  82     ALL_TAC] THEN
  83   STRIP_TAC THEN
  84   CONV_TAC NUM_REDUCE_CONV THEN
  85   REWRITE_TAC[REAL_MUL_RZERO; REAL_MUL_LZERO; REAL_MUL_LID; REAL_MUL_RID;
  86               REAL_SUB_RZERO; REAL_SUB_LZERO; REAL_SUB_REFL;
  87               REAL_ADD_LID; REAL_ADD_RID] THEN
  88   AP_THM_TAC THEN AP_TERM_TAC THEN
  89   REWRITE_TAC[REAL_POW_1] THEN
  90   REWRITE_TAC[REAL_ARITH
  91    `(a + b) * (x - y + z) - (a - b) * (x + y + z) =
  92     &2 * (b * x + b * z - a * y)`] THEN
  93   REWRITE_TAC[REAL_POW_2; REAL_MUL_RID] THEN
  94   REWRITE_TAC[REAL_ARITH
  95    `s * x * x + s - (&2 * x) * x * s = s * (&1 - x * x)`] THEN
  96   REWRITE_TAC[real_div; REAL_INV_MUL; REAL_INV_INV; GSYM REAL_MUL_ASSOC] THEN
  97   REWRITE_TAC[AC REAL_MUL_AC
  98    `a * b * c * d * e * inv(a) * f =
  99     (a * inv a) * b * c * d * e * f`] THEN
 100   REWRITE_TAC[REAL_ARITH
 101    `&1 + (x * s + &1) * (x * s + &1) =
 102     &2 + &2 * x * s + (s * s) * x * x`] THEN
 103   REWRITE_TAC[REAL_ARITH
 104    `&1 + (x * s - &1) * (x * s - &1) =
 105     &2 + &2 * x * --s + (s * s) * x * x`] THEN
 106   SIMP_TAC[REWRITE_RULE[REAL_POW_2] SQRT_POW_2; REAL_POS] THEN
 107   REWRITE_TAC[GSYM REAL_ADD_LDISTRIB] THEN
 108   REWRITE_TAC[REAL_ARITH `&2 + &2 * x = &2 * (&1 + x)`] THEN
 109   REWRITE_TAC[REAL_MUL_LNEG] THEN
 110   REWRITE_TAC[REAL_ARITH
 111    `&1 + x * (a + b) = (&1 + x * a) + x * b`] THEN
 112   REWRITE_TAC[REAL_MUL_RNEG] THEN REWRITE_TAC[GSYM real_sub] THEN
 113   REWRITE_TAC[REAL_ARITH `(&1 + x * a) + x * x = x * x + x * a + &1`] THEN
 114   REWRITE_TAC[REAL_ARITH `(&1 - x * a) + x * x = x * x - x * a + &1`] THEN
 115   REWRITE_TAC[REAL_INV_MUL; GSYM REAL_MUL_ASSOC] THEN
 116   REWRITE_TAC[REAL_ARITH `inv(x) * y * z * x = (x * inv(x)) * y * z`] THEN
 117   SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH_EQ; REAL_MUL_LID] THEN
 118   REWRITE_TAC[REAL_ARITH
 119     `p' * n * &2 * s2 * aa * n' * n' =
 120      (n' * n) * (p' * n') * &2 * s2 * aa`] THEN
 121   MP_TAC(SPEC `x pow 2` REAL_LE_SQUARE) THEN
 122   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH `&0 <= x ==> ~(&1 + x = &0)`)) THEN
 123   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM REAL_POW_2] THEN
 124   REWRITE_TAC[REAL_POW_POW; ARITH] THEN
 125   REWRITE_TAC[GSYM FACTOR_1X4_LEMMA; REAL_ENTIRE; DE_MORGAN_THM] THEN
 126   STRIP_TAC THEN
 127   ASM_SIMP_TAC[REAL_MUL_LINV; REAL_MUL_LID] THEN
 128   SUBGOAL_THEN
 129    `!other. inv(x * x + x * sqrt (&2) + &1) * sqrt (&2) +
 130             inv(x * x - x * sqrt (&2) + &1) * sqrt (&2) + other =
 131             other + &2 * sqrt(&2) * (&1 + x * x) *
 132                     inv(x * x + x * sqrt (&2) + &1) *
 133                     inv(x * x - x * sqrt (&2) + &1)`
 134    (fun th -> ONCE_REWRITE_TAC[th])
 135   THENL
 136    [GEN_TAC THEN
 137     MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN
 138     EXISTS_TAC `(x * x + x * sqrt (&2) + &1) *
 139                 (x * x - x * sqrt (&2) + &1)` THEN
 140     MATCH_MP_TAC(TAUT `~a /\ (~a ==> b) ==> ~a /\ b`) THEN CONJ_TAC THENL
 141      [REWRITE_TAC[FACTOR_1X4_LEMMA] THEN
 142       MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> ~(&1 + x = &0)`) THEN
 143       SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 + 2`)) THEN
 144       REWRITE_TAC[REAL_POW_ADD; REAL_LE_SQUARE]; ALL_TAC] THEN
 145     REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM] THEN STRIP_TAC THEN
 146     GEN_REWRITE_TAC LAND_CONV [REAL_ARITH
 147      `(x * y) * (a + b + c) = (x * a) * y + (y * b) * x + x * y * c`] THEN
 148     ASM_SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_RINV] THEN
 149     REWRITE_TAC[REAL_ARITH
 150      `(a + b + x * other = x * (other + c)) <=> (a + b = x * c)`] THEN
 151     REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
 152     ONCE_REWRITE_TAC[AC REAL_MUL_AC
 153      `p * n * x * y * z * p' * n' =
 154       (p * p') * (n * n') * x * y * z`] THEN
 155     ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID; REAL_MUL_RID] THEN
 156     REWRITE_TAC[REAL_ARITH
 157      `a * (x - y + z) + a * (x + y + z) = &2 * a * (x + z)`] THEN
 158     REWRITE_TAC[REAL_ADD_AC]; ALL_TAC] THEN
 159   REWRITE_TAC[GSYM REAL_INV_MUL; FACTOR_1X4_LEMMA] THEN
 160   SUBGOAL_THEN `~(x + &1 = &0) /\ ~(x - &1 = &0)` STRIP_ASSUME_TAC THENL
 161    [CONJ_TAC THENL
 162      [UNDISCH_TAC `&0 < (x + &1) pow 2`;
 163       UNDISCH_TAC `&0 < (x - &1) pow 2`] THEN
 164     DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_IMP_NZ) THEN
 165     SIMP_TAC[REAL_POW_EQ_0; ARITH_EQ]; ALL_TAC] THEN
 166   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID] THEN
 167   REWRITE_TAC[REAL_ARITH
 168    `i4 * &2 * s * (&1 - x2) + other + &2 * s * (&1 + x2) * i4 =
 169     &4 * s * i4 + other`] THEN
 170   MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `&1 - x pow 8` THEN
 171   MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
 172    [MATCH_MP_TAC(REAL_ARITH `x < &1 ==> ~(&1 - x = &0)`) THEN
 173     SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 * 4`)) THEN
 174     SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `&1 pow 4`)) THEN
 175     REWRITE_TAC[GSYM REAL_POW_POW] THEN MATCH_MP_TAC REAL_POW_LT2 THEN
 176     REWRITE_TAC[ARITH_EQ; REAL_POW_2; REAL_LE_SQUARE] THEN
 177     REWRITE_TAC[GSYM REAL_POW_2] THEN
 178     ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
 179     SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `&1 pow 2`)) THEN
 180     MATCH_MP_TAC REAL_POW_LT2 THEN
 181     ASM_REWRITE_TAC[REAL_ABS_POS; ARITH_EQ]; ALL_TAC] THEN
 182   SIMP_TAC[GSYM real_div; REAL_DIV_LMUL] THEN
 183   SUBGOAL_THEN `!x. &1 - x pow 8 = (&1 + x pow 4) * (&1 - x pow 4)`
 184    (fun th -> REWRITE_TAC[th])
 185   THENL
 186    [SUBST1_TAC(SYM(NUM_REDUCE_CONV `4 * 2`)) THEN
 187     REWRITE_TAC[GSYM REAL_POW_POW] THEN
 188     REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 189   REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM] THEN STRIP_TAC THEN
 190   REWRITE_TAC[GSYM REAL_POW_2; GSYM(CONJUNCT2 real_pow)] THEN
 191   CONV_TAC NUM_REDUCE_CONV THEN
 192   SUBST1_TAC(SPECL [`x pow 4`; `&1`] REAL_ADD_SYM) THEN
 193   REWRITE_TAC[real_div; REAL_ARITH
 194    `a + b + c1 * c2 * x + x * d - x * e =
 195     (a + b) + x * (c1 * c2 + d - e)`] THEN
 196   ONCE_REWRITE_TAC[REAL_ARITH
 197    `(p * m) * (x + inv(p) * y) = m * x * p + (p * inv(p)) * m * y`] THEN
 198   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID] THEN
 199   UNDISCH_TAC `~(&1 - x pow 4 = &0)` THEN
 200   SUBGOAL_THEN `!x. &1 - x pow 4 = (&1 + x pow 2) * (&1 - x pow 2)`
 201    (fun th -> REWRITE_TAC[th])
 202   THENL
 203    [SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 * 2`)) THEN
 204     REWRITE_TAC[GSYM REAL_POW_POW] THEN
 205     REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 206   REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM] THEN STRIP_TAC THEN
 207   UNDISCH_TAC `~(&1 - x pow 2 = &0)` THEN
 208   SUBGOAL_THEN `!x. &1 - x pow 2 = (&1 + x) * (&1 - x)`
 209    (fun th -> REWRITE_TAC[th])
 210   THENL
 211    [REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 212   REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM] THEN STRIP_TAC THEN
 213   ONCE_REWRITE_TAC[REAL_ARITH
 214    `(x12 * (p1 + p2) * (m1 - m2)) * (m' * &2 + p' * &2) * other =
 215     --(&2) * x12 * other *
 216     ((p2 + p1) * (m2 - m1) * m' + (m2 - m1) * (p2 + p1) * p')`] THEN
 217   ASM_SIMP_TAC[REAL_MUL_RINV] THEN
 218   CONV_TAC(TOP_DEPTH_CONV num_CONV) THEN
 219   REWRITE_TAC[real_pow] THEN CONV_TAC NUM_REDUCE_CONV THEN
 220   REAL_ARITH_TAC);;
 221
 222 let POLYLOG_CONVERGES = prove
 223  (`!a b x. ~(a = 0) /\ ~(b = 0) /\ abs(x) < &1
 224            ==> summable (\n. x pow (a * n + b) / &(a * n + b))`,
 225   REPEAT STRIP_TAC THEN
 226   MATCH_MP_TAC SER_COMPAR THEN
 227   EXISTS_TAC `\n. abs(x) pow (a * n + b)` THEN CONJ_TAC THENL
 228    [EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 229     REWRITE_TAC[REAL_ABS_DIV; GSYM REAL_ABS_POW; REAL_ABS_NUM] THEN
 230     REWRITE_TAC[real_div] THEN
 231     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
 232     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 233     ASM_SIMP_TAC[REAL_INV_LE_1; REAL_OF_NUM_LE;
 234                  ARITH_RULE `~(b = 0) ==> 1 <= a + b`];
 235     ALL_TAC] THEN
 236   ONCE_REWRITE_TAC[ADD_SYM] THEN
 237   REWRITE_TAC[REAL_POW_ADD; GSYM REAL_POW_POW] THEN
 238   REWRITE_TAC[summable] THEN
 239   EXISTS_TAC `abs(x) pow b * inv(&1 - abs(x) pow a)` THEN
 240   MATCH_MP_TAC SER_CMUL THEN
 241   MATCH_MP_TAC GP THEN
 242   REWRITE_TAC[REAL_ABS_POW; REAL_ABS_ABS] THEN
 243   SUBST1_TAC(SYM(SPEC `a:num` REAL_POW_ONE)) THEN
 244   MATCH_MP_TAC REAL_POW_LT2 THEN
 245   ASM_REWRITE_TAC[REAL_ABS_POS]);;
 246
 247 let POLYLOG_DERIVATIVE = prove
 248  (`!a b x. ~(a = 0) /\ ~(b = 0) /\ abs(x) < &1
 249            ==> ((\x. suminf (\n. x pow (a * n + b) / &(a * n + b))) diffl
 250                (x pow (b - 1) / (&1 - x pow a)))(x)`,
 251   REPEAT STRIP_TAC THEN
 252   SUBGOAL_THEN `abs(x pow a) < &1` ASSUME_TAC THENL
 253    [REWRITE_TAC[REAL_ABS_POW] THEN
 254     SUBST1_TAC(SYM(SPEC `a:num` REAL_POW_ONE)) THEN
 255     MATCH_MP_TAC REAL_POW_LT2 THEN
 256     ASM_REWRITE_TAC[REAL_ABS_POS]; ALL_TAC] THEN
 257   MP_TAC(SPEC `x pow a` GP) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 258   SUBGOAL_THEN
 259    `((\x. suminf (\n. inv(&(a * n + b)) * x pow n)) diffl
 260      (suminf (\n. diffs (\n. inv(&(a * n + b))) n * (x pow a) pow n)))(x pow a)`
 261   MP_TAC THENL
 262    [MATCH_MP_TAC TERMDIFF_STRONG THEN
 263     EXISTS_TAC `(abs(x pow a) + &1) / &2` THEN
 264     ABBREV_TAC `k = (abs(x pow a) + &1) / &2` THEN
 265     SUBGOAL_THEN `abs(x pow a) < abs(k) /\ abs(k) < &1` STRIP_ASSUME_TAC THENL
 266      [EXPAND_TAC "k" THEN
 267       SIMP_TAC[REAL_ABS_DIV; REAL_ABS_NUM; REAL_LT_RDIV_EQ;
 268              REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
 269       UNDISCH_TAC `abs(x pow a) < &1` THEN REAL_ARITH_TAC; ALL_TAC] THEN
 270     ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SER_COMPAR THEN
 271     EXISTS_TAC `\n. abs(k) pow n` THEN CONJ_TAC THENL
 272      [EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 273       REWRITE_TAC[] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 274       REWRITE_TAC[GSYM real_div; REAL_ABS_DIV;
 275                   GSYM REAL_ABS_POW; REAL_ABS_NUM] THEN
 276       ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_OF_NUM_LT;
 277                    ARITH_RULE `~(b = 0) ==> 0 < a + b`] THEN
 278       GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
 279       MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 280       ASM_SIMP_TAC[REAL_OF_NUM_LE;
 281                    ARITH_RULE `~(b = 0) ==> 1 <= a + b`]; ALL_TAC] THEN
 282     REWRITE_TAC[summable] THEN EXISTS_TAC `inv(&1 - abs k)` THEN
 283     ASM_SIMP_TAC[GP; REAL_ABS_ABS]; ALL_TAC] THEN
 284   REWRITE_TAC[diffs] THEN
 285   MP_TAC(SPECL [`a:num`; `x:real`] DIFF_POW) THEN
 286   REWRITE_TAC[TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
 287   DISCH_THEN(MP_TAC o MATCH_MP DIFF_CHAIN) THEN
 288   REWRITE_TAC[] THEN
 289   MP_TAC(SPECL [`b:num`; `x:real`] DIFF_POW) THEN
 290   REWRITE_TAC[TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
 291   DISCH_THEN(MP_TAC o MATCH_MP DIFF_MUL) THEN
 292   REWRITE_TAC[] THEN
 293   SUBGOAL_THEN
 294    `summable (\n. &(SUC n) / &(a * SUC n + b) * (x pow a) pow (SUC n - 1))`
 295   ASSUME_TAC THENL
 296    [REWRITE_TAC[SUC_SUB1] THEN MATCH_MP_TAC SER_COMPAR THEN
 297     EXISTS_TAC `\n. abs(x pow a) pow n` THEN CONJ_TAC THENL
 298      [EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 299       REWRITE_TAC[] THEN ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN
 300       REWRITE_TAC[GSYM REAL_ABS_POW] THEN
 301       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
 302       MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 303       ASM_SIMP_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT; REAL_ABS_DIV; REAL_ABS_NUM;
 304                    ARITH_RULE `~(b = 0) ==> 0 < a + b /\ 1 <= a + b`;
 305                    REAL_MUL_LID; REAL_LE_LDIV_EQ] THEN
 306       MATCH_MP_TAC(ARITH_RULE `1 * n <= b ==> n <= b + c`) THEN
 307       ASM_SIMP_TAC[LE_MULT_RCANCEL; ARITH_RULE `1 <= n <=> ~(n = 0)`];
 308       ALL_TAC] THEN
 309     REWRITE_TAC[summable] THEN EXISTS_TAC `inv(&1 - abs(x pow a))` THEN
 310     ASM_SIMP_TAC[GP; REAL_ABS_ABS]; ALL_TAC] THEN
 311   FIRST_ASSUM(MP_TAC o
 312               MATCH_MP(SPECL [`f:num->real`; `1`] SER_OFFSET_REV) o
 313               REWRITE_RULE[ADD1]) THEN
 314   REWRITE_TAC[SUM_1] THEN
 315   REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_ADD_LID] THEN
 316   REWRITE_TAC[GSYM real_div] THEN
 317   CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV(ALPHA_CONV `n:num`))) THEN
 318   REWRITE_TAC[ADD_SUB] THEN REWRITE_TAC[ADD1] THEN
 319   DISCH_THEN(MP_TAC o MATCH_MP SER_CMUL) THEN
 320   DISCH_THEN(MP_TAC o SPEC `&a * x pow (a - 1) * x pow b`) THEN
 321   SUBGOAL_THEN
 322    `summable (\n. inv(&(a * n + b)) * x pow a pow n)`
 323   MP_TAC THENL
 324    [MATCH_MP_TAC SER_COMPAR THEN
 325     EXISTS_TAC `\n. abs(x pow a) pow n` THEN CONJ_TAC THENL
 326      [EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 327       REWRITE_TAC[REAL_ABS_MUL; GSYM REAL_ABS_POW; REAL_ABS_NUM] THEN
 328       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
 329       MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 330       REWRITE_TAC[REAL_ABS_INV; REAL_ABS_NUM] THEN
 331       ASM_SIMP_TAC[REAL_INV_LE_1; REAL_OF_NUM_LE;
 332                    ARITH_RULE `~(b = 0) ==> 1 <= a + b`];
 333       ALL_TAC] THEN
 334     REWRITE_TAC[summable] THEN
 335     EXISTS_TAC `inv(&1 - abs(x pow a))` THEN
 336     ASM_SIMP_TAC[GP; REAL_ABS_ABS]; ALL_TAC] THEN
 337   DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
 338   DISCH_THEN(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN
 339   DISCH_THEN(MP_TAC o MATCH_MP SER_CMUL) THEN
 340   DISCH_THEN(MP_TAC o SPEC `&b * x pow (b - 1)`) THEN
 341   ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
 342   DISCH_THEN(MP_TAC o MATCH_MP SER_ADD) THEN REWRITE_TAC[] THEN
 343   SUBGOAL_THEN
 344    `!n. (&a * x pow (a - 1) * x pow b) *
 345         &n / &(a * n + b) * x pow a pow (n - 1) +
 346         (&b * x pow (b - 1)) * inv(&(a * n + b)) * x pow a pow n =
 347         x pow (a * n + b - 1)`
 348    (fun th -> REWRITE_TAC[th])
 349   THENL
 350    [X_GEN_TAC `n:num` THEN ASM_CASES_TAC `n = 0` THENL
 351      [ASM_REWRITE_TAC[SUB_0; real_pow; MULT_CLAUSES; ADD_CLAUSES] THEN
 352       REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
 353       REWRITE_TAC[REAL_ADD_LID; GSYM REAL_MUL_ASSOC; REAL_MUL_RID] THEN
 354       ASM_SIMP_TAC[GSYM real_div; REAL_DIV_LMUL; REAL_OF_NUM_EQ]; ALL_TAC] THEN
 355     REWRITE_TAC[REAL_POW_ADD; GSYM REAL_POW_POW] THEN
 356     SUBGOAL_THEN `(x pow a) pow n = x pow a * (x pow a) pow (n - 1)`
 357     SUBST1_TAC THENL
 358      [REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
 359       AP_TERM_TAC THEN UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC; ALL_TAC] THEN
 360     REWRITE_TAC[REAL_POW_POW] THEN
 361     SUBGOAL_THEN `x pow a = x * x pow (a - 1)` SUBST1_TAC THENL
 362      [REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
 363       AP_TERM_TAC THEN UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
 364     SUBGOAL_THEN `x pow b = x * x pow (b - 1)` SUBST1_TAC THENL
 365      [REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
 366       AP_TERM_TAC THEN UNDISCH_TAC `~(b = 0)` THEN ARITH_TAC; ALL_TAC] THEN
 367     REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
 368     REWRITE_TAC[REAL_ARITH
 369      `a * xa1 * x * xb1 * n * i * xan1 + b * xb1 * i * x * xa1 * xan1 =
 370       x * xa1 * xan1 * xb1 * (a * n + b) * i`] THEN
 371     ASM_SIMP_TAC[GSYM real_div; REAL_OF_NUM_MUL; REAL_OF_NUM_ADD] THEN
 372     ASM_SIMP_TAC[REAL_DIV_REFL; REAL_MUL_RID; REAL_OF_NUM_EQ;
 373                  ARITH_RULE `~(b = 0) ==> ~(a + b = 0)`];
 374     ALL_TAC] THEN
 375   DISCH_THEN(MP_TAC o MATCH_MP SUM_UNIQ) THEN
 376   SUBGOAL_THEN
 377    `x pow (b - 1) / (&1 - x pow a) = suminf (\n. x pow (a * n + b - 1))`
 378   (SUBST1_TAC o SYM) THENL
 379    [MATCH_MP_TAC SUM_UNIQ THEN
 380     ONCE_REWRITE_TAC[ADD_SYM] THEN
 381     REWRITE_TAC[REAL_POW_ADD; real_div] THEN
 382     MATCH_MP_TAC SER_CMUL THEN
 383     ASM_SIMP_TAC[GSYM REAL_POW_POW; GP]; ALL_TAC] THEN
 384   SIMP_TAC[REAL_MUL_AC] THEN DISCH_THEN(K ALL_TAC) THEN
 385   REWRITE_TAC[diffl] THEN
 386   MATCH_MP_TAC(ONCE_REWRITE_RULE[IMP_CONJ]
 387                LIM_TRANSFORM) THEN
 388   REWRITE_TAC[LIM] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
 389   EXISTS_TAC `&1 - abs(x)` THEN
 390   ASM_REWRITE_TAC[REAL_SUB_LT; REAL_SUB_RZERO] THEN
 391   X_GEN_TAC `h:real` THEN STRIP_TAC THEN
 392   MATCH_MP_TAC(REAL_ARITH `(a = a') /\ &0 < b ==> abs(a - a') < b`) THEN
 393   ASM_REWRITE_TAC[] THEN
 394   AP_THM_TAC THEN AP_TERM_TAC THEN
 395   SUBGOAL_THEN `abs(x + h) < &1` ASSUME_TAC THENL
 396    [UNDISCH_TAC `abs(h) < &1 - abs(x)` THEN REAL_ARITH_TAC; ALL_TAC] THEN
 397   SUBGOAL_THEN
 398    `!z. abs(z) < &1
 399         ==> (suminf (\n. z pow (a * n + b) / &(a * n + b)) =
 400              z pow b * suminf (\n. inv (&(a * n + b)) * z pow a pow n))`
 401    (fun th -> ASM_SIMP_TAC[th]) THEN
 402   X_GEN_TAC `z:real` THEN DISCH_TAC THEN
 403   MATCH_MP_TAC(GSYM SUM_UNIQ) THEN
 404   ONCE_REWRITE_TAC[ADD_SYM] THEN
 405   REWRITE_TAC[REAL_POW_ADD; real_div; GSYM REAL_MUL_ASSOC] THEN
 406   MATCH_MP_TAC SER_CMUL THEN
 407   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
 408   REWRITE_TAC[GSYM REAL_POW_POW] THEN
 409   MATCH_MP_TAC SUMMABLE_SUM THEN
 410   ONCE_REWRITE_TAC[ADD_SYM] THEN
 411   MATCH_MP_TAC SER_COMPAR THEN
 412   EXISTS_TAC `\n. abs(z pow a) pow n` THEN CONJ_TAC THENL
 413    [EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 414     REWRITE_TAC[REAL_ABS_MUL; GSYM REAL_ABS_POW; REAL_ABS_NUM] THEN
 415     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
 416     MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 417     REWRITE_TAC[REAL_ABS_INV; REAL_ABS_NUM] THEN
 418     ASM_SIMP_TAC[REAL_INV_LE_1; REAL_OF_NUM_LE;
 419                  ARITH_RULE `~(b = 0) ==> 1 <= a + b`];
 420     ALL_TAC] THEN
 421   REWRITE_TAC[summable] THEN
 422   EXISTS_TAC `inv(&1 - abs(z pow a))` THEN
 423   MATCH_MP_TAC GP THEN REWRITE_TAC[REAL_ABS_ABS; REAL_ABS_POW] THEN
 424   SUBST1_TAC(SYM(SPEC `a:num` REAL_POW_ONE)) THEN
 425   MATCH_MP_TAC REAL_POW_LT2 THEN ASM_REWRITE_TAC[REAL_ABS_POS]);;
 426
 427 let POLYLOG_THM = prove
 428  (`(\n. inv(&16 pow n) * (&4 / &(8 * n + 1) -
 429                           &2 / &(8 * n + 4) -
 430                           &1 / &(8 * n + 5) -
 431                           &1 / &(8 * n + 6)))
 432    sums pi`,
 433   SUBGOAL_THEN
 434    `!x. abs(x) < &1
 435         ==> ((\x. suminf (\n. &4 * sqrt(&2) * x pow (8 * n + 1) / &(8 * n + 1) -
 436                               &8 * x pow (8 * n + 4) / &(8 * n + 4) -
 437                               &4 * sqrt(&2) * x pow (8 * n + 5) / &(8 * n + 5) -
 438                               &8 * x pow (8 * n + 6) / &(8 * n + 6)))
 439              diffl
 440               (&4 * sqrt(&2) -
 441                &8 * x pow 3 -
 442                &4 * sqrt(&2) * x pow 4 -
 443                &8 * x pow 5) / (&1 - x pow 8))(x)`
 444   ASSUME_TAC THENL
 445    [REPEAT STRIP_TAC THEN
 446     MP_TAC(SPECL [`8`; `1`; `x:real`] POLYLOG_DERIVATIVE) THEN
 447     CONV_TAC NUM_REDUCE_CONV THEN ASM_REWRITE_TAC[real_pow] THEN
 448     DISCH_THEN(MP_TAC o SPEC `&4 * sqrt(&2)` o MATCH_MP DIFF_CMUL) THEN
 449     MP_TAC(SPECL [`8`; `4`; `x:real`] POLYLOG_DERIVATIVE) THEN
 450     CONV_TAC NUM_REDUCE_CONV THEN ASM_REWRITE_TAC[] THEN
 451     DISCH_THEN(MP_TAC o SPEC `&8` o MATCH_MP DIFF_CMUL) THEN
 452     MP_TAC(SPECL [`8`; `5`; `x:real`] POLYLOG_DERIVATIVE) THEN
 453     CONV_TAC NUM_REDUCE_CONV THEN ASM_REWRITE_TAC[] THEN
 454     DISCH_THEN(MP_TAC o SPEC `&4 * sqrt(&2)` o MATCH_MP DIFF_CMUL) THEN
 455     MP_TAC(SPECL [`8`; `6`; `x:real`] POLYLOG_DERIVATIVE) THEN
 456     CONV_TAC NUM_REDUCE_CONV THEN ASM_REWRITE_TAC[] THEN
 457     DISCH_THEN(MP_TAC o SPEC `&8` o MATCH_MP DIFF_CMUL) THEN
 458     REWRITE_TAC[] THEN
 459     ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
 460     DISCH_THEN(MP_TAC o MATCH_MP DIFF_ADD) THEN
 461     ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
 462     DISCH_THEN(MP_TAC o MATCH_MP DIFF_ADD) THEN
 463     ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
 464     DISCH_THEN(MP_TAC o MATCH_MP DIFF_SUB) THEN
 465     REWRITE_TAC[real_div; REAL_MUL_ASSOC; GSYM REAL_ADD_RDISTRIB;
 466                 GSYM REAL_SUB_RDISTRIB] THEN
 467     REWRITE_TAC[REAL_ARITH `a - (b + c + d) = a - b - c - d`] THEN
 468     REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN
 469     REWRITE_TAC[REAL_MUL_ASSOC; REAL_MUL_RID] THEN
 470     REWRITE_TAC[diffl] THEN
 471     MATCH_MP_TAC(ONCE_REWRITE_RULE[IMP_CONJ]
 472                  LIM_TRANSFORM) THEN
 473     REWRITE_TAC[LIM] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
 474     EXISTS_TAC `&1 - abs(x)` THEN
 475     ASM_REWRITE_TAC[REAL_SUB_LT; REAL_SUB_RZERO] THEN
 476     X_GEN_TAC `h:real` THEN STRIP_TAC THEN
 477     MATCH_MP_TAC(REAL_ARITH `(a = a') /\ &0 < b ==> abs(a - a') < b`) THEN
 478     ASM_REWRITE_TAC[] THEN
 479     AP_THM_TAC THEN AP_TERM_TAC THEN
 480     SUBGOAL_THEN `abs(x + h) < &1` ASSUME_TAC THENL
 481      [UNDISCH_TAC `abs(h) < &1 - abs(x)` THEN REAL_ARITH_TAC; ALL_TAC] THEN
 482     SUBGOAL_THEN
 483      `!z. abs(z) < &1
 484           ==> (suminf
 485                   (\n. (&4 * sqrt (&2)) * z pow (8 * n + 1) / &(8 * n + 1) -
 486                        &8 * z pow (8 * n + 4) / &(8 * n + 4) -
 487                        (&4 * sqrt (&2)) * z pow (8 * n + 5) / &(8 * n + 5) -
 488                        &8 * z pow (8 * n + 6) / &(8 * n + 6)) =
 489             (&4 * sqrt (&2)) * suminf (\n. z pow (8 * n + 1) / &(8 * n + 1)) -
 490              &8 * suminf (\n. z pow (8 * n + 4) / &(8 * n + 4)) -
 491              (&4 * sqrt (&2)) * suminf (\n. z pow (8 * n + 5) / &(8 * n + 5)) -
 492              &8 * suminf (\n. z pow (8 * n + 6) / &(8 * n + 6)))`
 493      (fun th -> ASM_SIMP_TAC[th]) THEN
 494     X_GEN_TAC `z:real` THEN DISCH_TAC THEN
 495     MATCH_MP_TAC(GSYM SUM_UNIQ) THEN
 496     REPEAT(MATCH_MP_TAC SER_SUB THEN CONJ_TAC) THEN
 497     MATCH_MP_TAC SER_CMUL THEN
 498     MATCH_MP_TAC SUMMABLE_SUM THEN
 499     MATCH_MP_TAC POLYLOG_CONVERGES THEN
 500     ASM_REWRITE_TAC[] THEN CONV_TAC NUM_REDUCE_CONV; ALL_TAC] THEN
 501   MP_TAC(SPEC
 502    `\x. suminf (\n. &4 * sqrt (&2) * x pow (8 * n + 1) / &(8 * n + 1) -
 503                     &8 * x pow (8 * n + 4) / &(8 * n + 4) -
 504                     &4 * sqrt (&2) * x pow (8 * n + 5) / &(8 * n + 5) -
 505                     &8 * x pow (8 * n + 6) / &(8 * n + 6)) -
 506         (ln ((x - &1) pow 2) +
 507          ln((x + &1) pow 2) +
 508          ln((x pow 2 + x * sqrt (&2) + &1) /
 509             (x pow 2 - x * sqrt (&2) + &1)) +
 510          &2 * atn (x * sqrt (&2) + &1) +
 511          &2 * atn (x * sqrt (&2) - &1) +
 512          &2 * atn (x pow 2) - ln (x pow 4 + &1))` DIFF_ISCONST_END_SIMPLE) THEN
 513   DISCH_THEN(MP_TAC o SPECL [`&0`; `inv(sqrt(&2))`]) THEN
 514   W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
 515    [SIMP_TAC[SQRT_POS_LT; REAL_LT_INV_EQ; REAL_OF_NUM_LT; ARITH] THEN
 516     X_GEN_TAC `x:real` THEN STRIP_TAC THEN
 517     SUBGOAL_THEN `abs(x) < &1` MP_TAC THENL
 518      [MATCH_MP_TAC(REAL_ARITH
 519        `!a. &0 <= x /\ x <= a /\ a < &1 ==> abs(x) < &1`) THEN
 520       EXISTS_TAC `inv(sqrt(&2))` THEN ASM_REWRITE_TAC[] THEN
 521       SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `inv(&1)`)) THEN
 522       MATCH_MP_TAC REAL_LT_INV2 THEN REWRITE_TAC[REAL_LT_01] THEN
 523       MATCH_MP_TAC REAL_LTE_TRANS THEN
 524       EXISTS_TAC `sqrt((&5 / &4) pow 2)` THEN CONJ_TAC THENL
 525        [SIMP_TAC[POW_2_SQRT; REAL_LE_DIV; REAL_POS] THEN
 526         CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
 527       MATCH_MP_TAC SQRT_MONO_LE THEN CONV_TAC REAL_RAT_REDUCE_CONV;
 528       ALL_TAC] THEN
 529     DISCH_THEN(fun th -> MP_TAC(MATCH_MP MAGIC_DERIVATIVE th) THEN
 530                          ANTE_RES_THEN MP_TAC th) THEN
 531     ONCE_REWRITE_TAC[IMP_IMP] THEN
 532     DISCH_THEN(MP_TAC o MATCH_MP DIFF_SUB) THEN
 533     REWRITE_TAC[REAL_SUB_REFL]; ALL_TAC] THEN
 534   SIMP_TAC[snd(EQ_IMP_RULE(SPEC_ALL REAL_POW_EQ_0));
 535            ARITH_RULE `~(b = 0) ==> ~(a + b = 0)`;
 536            ARITH_EQ] THEN
 537   REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
 538   REWRITE_TAC[GSYM real_div; REAL_ADD_LID; REAL_ADD_RID] THEN
 539   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 540   REWRITE_TAC[REAL_DIV_1; LN_1; ATN_1; ATN_NEG; ATN_0] THEN
 541   REWRITE_TAC[REAL_ARITH `a * b + a * --b + c = c`] THEN
 542   SUBGOAL_THEN `suminf (\n. &0) = &0` SUBST1_TAC THENL
 543    [MATCH_MP_TAC(GSYM SUM_UNIQ) THEN
 544     MP_TAC(SPECL [`\n:num. &0`; `0`] SER_0) THEN REWRITE_TAC[sum];
 545     ALL_TAC] THEN
 546   REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID; REAL_SUB_REFL] THEN
 547   SIMP_TAC[REAL_MUL_LINV; REAL_LT_IMP_NZ; REAL_LT_INV_EQ;
 548            SQRT_POS_LT; REAL_OF_NUM_LT; ARITH_LE; ARITH_LT] THEN
 549   SUBGOAL_THEN `inv(sqrt(&2)) pow 4 = inv(sqrt(&2)) pow 2 pow 2`
 550   SUBST1_TAC THENL [REWRITE_TAC[REAL_POW_POW; ARITH]; ALL_TAC] THEN
 551   SUBGOAL_THEN `inv(sqrt(&2)) pow 2 = &1 / &2` SUBST1_TAC THENL
 552    [REWRITE_TAC[REAL_POW_INV; real_div; REAL_MUL_LID] THEN AP_TERM_TAC THEN
 553     SIMP_TAC[SQRT_POW_2; REAL_POS]; ALL_TAC] THEN
 554   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 555   SUBGOAL_THEN
 556    `!other. ln((inv (sqrt (&2)) - &1) pow 2) +
 557             ln((inv (sqrt (&2)) + &1) pow 2) + other =
 558             ln(&1 / &4) + other`
 559    (fun th -> ONCE_REWRITE_TAC[th])
 560   THENL
 561    [GEN_TAC THEN REWRITE_TAC[REAL_ADD_ASSOC] THEN
 562     AP_THM_TAC THEN AP_TERM_TAC THEN
 563     SUBGOAL_THEN `&0 < (inv(sqrt(&2)) - &1) pow 2 /\
 564                   &0 < (inv(sqrt (&2)) + &1) pow 2`
 565      (fun th -> SIMP_TAC[GSYM LN_MUL; th])
 566     THENL
 567      [REWRITE_TAC[REAL_ARITH `&0 < x <=> &0 <= x /\ ~(x = &0)`] THEN
 568       REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE; REAL_ENTIRE] THEN
 569       MATCH_MP_TAC(REAL_ARITH
 570        `&0 < x /\ x < &1 ==> ~(x - &1 = &0) /\ ~(x + &1 = &0)`) THEN
 571       SIMP_TAC[REAL_LT_INV_EQ; SQRT_POS_LT; REAL_OF_NUM_LT; ARITH] THEN
 572       MATCH_MP_TAC REAL_LET_TRANS THEN
 573       EXISTS_TAC `sqrt((&4 / &5) pow 2)` THEN CONJ_TAC THENL
 574        [ALL_TAC;
 575         SIMP_TAC[POW_2_SQRT; REAL_LE_DIV; REAL_POS] THEN
 576         CONV_TAC REAL_RAT_REDUCE_CONV] THEN
 577       SIMP_TAC[GSYM SQRT_INV; REAL_POS] THEN
 578       MATCH_MP_TAC SQRT_MONO_LE THEN CONV_TAC REAL_RAT_REDUCE_CONV;
 579       ALL_TAC] THEN
 580     REWRITE_TAC[GSYM REAL_POW_MUL] THEN
 581     REWRITE_TAC[REAL_ARITH `(x - &1) * (x + &1) = x * x - &1`] THEN
 582     REWRITE_TAC[GSYM REAL_POW_2] THEN
 583     SUBGOAL_THEN `inv(sqrt(&2)) pow 2 = &1 / &2` SUBST1_TAC THENL
 584      [REWRITE_TAC[REAL_POW_INV; real_div; REAL_MUL_LID] THEN AP_TERM_TAC THEN
 585       SIMP_TAC[SQRT_POW_2; REAL_POS]; ALL_TAC] THEN
 586     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
 587   REWRITE_TAC[ATN_0; REAL_MUL_RZERO; REAL_ADD_LID] THEN
 588   ONCE_REWRITE_TAC[REAL_ARITH
 589    `l1 + l2 + a + y - l3 = (l1 + l2 - l3) + a + y`] THEN
 590   SIMP_TAC[GSYM LN_DIV; GSYM LN_MUL; REAL_LT_DIV; REAL_LT_MUL; REAL_OF_NUM_LT;
 591            ARITH_LE; ARITH_LT] THEN
 592   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[LN_1; REAL_ADD_LID] THEN
 593   REWRITE_TAC[GSYM REAL_ADD_LDISTRIB] THEN
 594   ONCE_REWRITE_TAC[ADD_SYM] THEN
 595   REWRITE_TAC[REAL_POW_ADD; real_div; REAL_MUL_ASSOC] THEN
 596   SUBGOAL_THEN `!n. inv(sqrt (&2)) pow (8 * n) = inv(&16 pow n)`
 597    (fun th -> REWRITE_TAC[th])
 598   THENL
 599    [SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 * 4`)) THEN
 600     REWRITE_TAC[GSYM REAL_POW_POW] THEN
 601     SUBGOAL_THEN `inv(sqrt(&2)) pow 2 = &1 / &2` SUBST1_TAC THENL
 602      [REWRITE_TAC[REAL_POW_INV; real_div; REAL_MUL_LID] THEN AP_TERM_TAC THEN
 603       SIMP_TAC[SQRT_POW_2; REAL_POS]; ALL_TAC] THEN
 604     CONV_TAC REAL_RAT_REDUCE_CONV THEN
 605     REWRITE_TAC[GSYM REAL_POW_INV] THEN
 606     REWRITE_TAC[real_div; REAL_MUL_LID]; ALL_TAC] THEN
 607   REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_INV_MUL] THEN
 608   SUBGOAL_THEN `!x. x pow 5 = x * x pow 4` (fun th -> REWRITE_TAC[th]) THENL
 609    [REWRITE_TAC[GSYM(CONJUNCT2 real_pow); ARITH]; ALL_TAC] THEN
 610   REWRITE_TAC[REAL_POW_1] THEN
 611   ONCE_REWRITE_TAC[REAL_ARITH
 612    `a * s * i * b - c - d * s * (i * e) * f - g =
 613     (s * i) * a * b - c - (s * i) * d * e * f - g`] THEN
 614   SIMP_TAC[REAL_MUL_RINV; REAL_LT_IMP_NZ; SQRT_POS_LT; REAL_OF_NUM_LT;
 615            ARITH_LT; ARITH_LE] THEN
 616   SUBGOAL_THEN `!x. x pow 6 = (x pow 2) pow 3`
 617     (fun th -> REWRITE_TAC[th])
 618   THENL [REWRITE_TAC[REAL_POW_POW; ARITH]; ALL_TAC] THEN
 619   SUBGOAL_THEN `!x. x pow 4 = (x pow 2) pow 2`
 620     (fun th -> REWRITE_TAC[th])
 621   THENL [REWRITE_TAC[REAL_POW_POW; ARITH]; ALL_TAC] THEN
 622   SUBGOAL_THEN `inv(sqrt(&2)) pow 2 = &1 / &2` SUBST1_TAC THENL
 623    [REWRITE_TAC[REAL_POW_INV; real_div; REAL_MUL_LID] THEN AP_TERM_TAC THEN
 624     SIMP_TAC[SQRT_POW_2; REAL_POS]; ALL_TAC] THEN
 625   REWRITE_TAC[REAL_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 626   ONCE_REWRITE_TAC[ADD_SYM] THEN
 627   REWRITE_TAC[REAL_INV_MUL] THEN
 628   ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = b * a * c`] THEN
 629   REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN
 630   REWRITE_TAC[GSYM real_div] THEN
 631   REWRITE_TAC[REAL_SUB_0] THEN DISCH_TAC THEN
 632   SUBGOAL_THEN
 633    `summable
 634       (\n. inv (&16 pow n) *
 635            (&4 / &(8 * n + 1) -
 636             &2 / &(8 * n + 4) -
 637             &1 / &(8 * n + 5) -
 638             &1 / &(8 * n + 6)))`
 639   MP_TAC THENL
 640    [MATCH_MP_TAC SER_COMPAR THEN
 641     EXISTS_TAC `\n. &8 / &16 pow n` THEN CONJ_TAC THENL
 642      [EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 643       REWRITE_TAC[REAL_ABS_MUL; GSYM REAL_ABS_POW; REAL_ABS_NUM] THEN
 644       GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
 645       REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
 646       REWRITE_TAC[REAL_ABS_POS] THEN
 647       REWRITE_TAC[REAL_ABS_INV; REAL_ABS_POW; REAL_ABS_NUM; REAL_LE_REFL] THEN
 648       MATCH_MP_TAC(REAL_ARITH
 649        `abs(v) <= &1 /\ abs(w) <= &1 /\ abs(x) <= &1 /\ abs(y) <= &1
 650         ==> abs(&4 * v - &2 * w - &1 * x - &1 * y) <= &8`) THEN
 651       REWRITE_TAC[REAL_ABS_INV; REAL_ABS_NUM] THEN
 652       SUBST1_TAC(SYM REAL_INV_1) THEN
 653       REPEAT CONJ_TAC THEN MATCH_MP_TAC REAL_LE_INV2 THEN
 654       CONV_TAC REAL_RAT_REDUCE_CONV THEN
 655       REWRITE_TAC[REAL_OF_NUM_LE] THEN ARITH_TAC; ALL_TAC] THEN
 656     REWRITE_TAC[summable] THEN EXISTS_TAC `&8 / (&1 - inv(&16))` THEN
 657     REWRITE_TAC[real_div; GSYM REAL_POW_INV] THEN
 658     MATCH_MP_TAC SER_CMUL THEN
 659     MATCH_MP_TAC GP THEN CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
 660   DISCH_THEN(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN ASM_REWRITE_TAC[] THEN
 661   MATCH_MP_TAC EQ_IMP THEN
 662   REWRITE_TAC[real_div; REAL_MUL_LID] THEN AP_TERM_TAC THEN
 663   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 664   SIMP_TAC[GSYM REAL_EQ_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
 665   MP_TAC(SPEC `atn(&1 / &2)` TAN_COT) THEN
 666   REWRITE_TAC[ATN_TAN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 667   DISCH_THEN(MP_TAC o AP_TERM `atn`) THEN REWRITE_TAC[REAL_DIV_1] THEN
 668   MATCH_MP_TAC(REAL_ARITH
 669    `(a = d - c) ==> (a = b) ==> (b + c = d)`) THEN
 670   MATCH_MP_TAC TAN_ATN THEN REWRITE_TAC[PI2_PI4] THEN
 671   MATCH_MP_TAC(REAL_ARITH
 672    `&0 < x /\ x < p4
 673     ==> --(&2 * p4) < &2 * p4 - x /\ &2 * p4 - x < &2 * p4`) THEN
 674   CONJ_TAC THENL
 675    [SUBST1_TAC(SYM ATN_0) THEN MATCH_MP_TAC ATN_MONO_LT THEN
 676     CONV_TAC REAL_RAT_REDUCE_CONV;
 677     MATCH_MP_TAC ATN_LT_PI4_POS THEN CONV_TAC REAL_RAT_REDUCE_CONV]);;