Examples/mangoldt.ml

   1 (* ========================================================================= *)
   2 (* Mangoldt function and elementary Chebyshev/Mertens results.               *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/pocklington.ml";;
   6 needs "Multivariate/transcendentals.ml";;
   7
   8 prioritize_real();;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* Useful approximation/bound lemmas, simple rather than sharp.              *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let LOG_FACT = prove
  15  (`!n. log(&(FACT n)) = sum(1..n) (\d. log(&d))`,
  16   INDUCT_TAC THEN
  17   SIMP_TAC[FACT; SUM_CLAUSES_NUMSEG; LOG_1; ARITH; ARITH_RULE `1 <= SUC n`] THEN
  18   SIMP_TAC[GSYM REAL_OF_NUM_MUL; LOG_MUL; REAL_OF_NUM_LT; FACT_LT; LT_0] THEN
  19   ASM_REWRITE_TAC[ADD1] THEN REWRITE_TAC[ADD_AC; REAL_ADD_AC]);;
  20
  21 let SUM_DIVISORS_FLOOR_LEMMA = prove
  22  (`!n d. ~(d = 0)
  23          ==> sum(1..n) (\m. if d divides m then &1 else &0) = floor(&n / &d)`,
  24   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[FLOOR_DIV_DIV] THEN
  25   SIMP_TAC[GSYM SUM_RESTRICT_SET; FINITE_NUMSEG; SUM_CONST; FINITE_RESTRICT;
  26            REAL_MUL_RID; REAL_OF_NUM_EQ] THEN
  27   GEN_REWRITE_TAC RAND_CONV [GSYM CARD_NUMSEG_1] THEN
  28   MATCH_MP_TAC BIJECTIONS_CARD_EQ THEN
  29   MAP_EVERY EXISTS_TAC [`\m:num. m DIV d`; `\m:num. m * d`] THEN
  30   ASM_SIMP_TAC[IN_ELIM_THM; IN_NUMSEG; LE_1; DIV_MULT; DIVIDES_DIV_MULT;
  31                FINITE_NUMSEG; ONCE_REWRITE_RULE[MULT_SYM] DIV_MULT;
  32                DIV_MONO; LE_1] THEN
  33   ASM_SIMP_TAC[LE_RDIV_EQ; MULT_EQ_0; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
  34   CONJ_TAC THENL [GEN_TAC THEN STRIP_TAC; ARITH_TAC] THEN
  35   FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN ASM_SIMP_TAC[DIV_EQ_0] THEN
  36   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [ARITH_RULE `d = 1 * d`] THEN
  37   ASM_SIMP_TAC[LT_MULT_RCANCEL; ARITH_RULE `n < 1 <=> n = 0`] THEN
  38   ASM_MESON_TAC[MULT_CLAUSES]);;
  39
  40 let LOG_2_BOUNDS = prove
  41  (`&1 / &2 <= log(&2) /\ log(&2) <= &1`,
  42   CONJ_TAC THENL
  43    [GEN_REWRITE_TAC LAND_CONV [GSYM LOG_EXP] THEN
  44     MP_TAC(SPEC `inv(&2)` REAL_EXP_BOUND_LEMMA);
  45     GEN_REWRITE_TAC RAND_CONV [GSYM LOG_EXP] THEN
  46     MP_TAC(SPEC `&1` REAL_EXP_LE_X)] THEN
  47   CONV_TAC REAL_RAT_REDUCE_CONV THEN MATCH_MP_TAC EQ_IMP THEN
  48   CONV_TAC SYM_CONV THEN MATCH_MP_TAC LOG_MONO_LE THEN
  49   REWRITE_TAC[REAL_EXP_POS_LT; REAL_OF_NUM_LT; ARITH]);;
  50
  51 let LOG_LE_REFL = prove
  52  (`!n. ~(n = 0) ==> log(&n) <= &n`,
  53   REPEAT STRIP_TAC THEN
  54   MATCH_MP_TAC(REAL_ARITH `x <= y - &1 ==> x <= y`) THEN
  55   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV)
  56    [REAL_ARITH `n = &1 + (n  - &1)`] THEN
  57   MATCH_MP_TAC LOG_LE THEN
  58   REWRITE_TAC[REAL_LE_SUB_LADD; REAL_OF_NUM_ADD; REAL_OF_NUM_LE] THEN
  59   UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC);;
  60
  61 let LOG_FACT_BOUNDS = prove
  62  (`!n. ~(n = 0)
  63        ==> abs(log(&(FACT n)) - (&n * log(&n) - &n + &1)) <= &2 * log(&n)`,
  64   REPEAT STRIP_TAC THEN ASM_CASES_TAC `n = 1` THENL
  65    [ASM_REWRITE_TAC[num_CONV `1`; FACT] THEN
  66     REWRITE_TAC[ARITH; LOG_1] THEN REAL_ARITH_TAC;
  67     ALL_TAC] THEN
  68   ASM_SIMP_TAC[LOG_FACT] THEN
  69   REWRITE_TAC[REAL_ARITH `abs(x - y) <= e <=> x <= y + e /\ y - e <= x`] THEN
  70   CONJ_TAC THENL
  71    [MP_TAC(ISPECL[`\z. clog(z)`; `\z. z * clog z - z`; `1`; `n:num`]
  72                  SUM_INTEGRAL_UBOUND_INCREASING) THEN
  73     REWRITE_TAC[] THEN ANTS_TAC THENL
  74      [CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
  75       CONJ_TAC THENL
  76        [REWRITE_TAC[IN_SEGMENT_CX_GEN] THEN REPEAT STRIP_TAC THENL
  77          [COMPLEX_DIFF_TAC THEN CONJ_TAC THEN UNDISCH_TAC `&1 <= Re x` THENL
  78            [REAL_ARITH_TAC; ALL_TAC] THEN
  79           ASM_CASES_TAC `x = Cx(&0)` THEN ASM_REWRITE_TAC[RE_CX] THENL
  80            [REAL_ARITH_TAC;
  81             UNDISCH_TAC `~(x = Cx(&0))` THEN CONV_TAC COMPLEX_FIELD];
  82           FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM LT_NZ]) THEN
  83           REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
  84           ASM_REAL_ARITH_TAC];
  85         MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN STRIP_TAC THEN
  86         SUBGOAL_THEN `&0 < a /\ &0 < b` ASSUME_TAC THENL
  87          [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  88         ASM_SIMP_TAC[GSYM CX_LOG; RE_CX; LOG_MONO_LE_IMP]];
  89         ALL_TAC];
  90      ASM_SIMP_TAC[SUM_CLAUSES_LEFT; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
  91      REWRITE_TAC[LOG_1; REAL_ADD_LID; ARITH] THEN
  92      FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
  93       `~(n = 0) ==> n = 1 \/ 2 <= n`))
  94      THENL
  95       [ASM_REWRITE_TAC[] THEN CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
  96        REWRITE_TAC[LOG_1; SUM_CLAUSES] THEN REAL_ARITH_TAC;
  97        ALL_TAC] THEN
  98      MP_TAC(ISPECL[`\z. clog(z)`; `\z. z * clog z - z`; `2`; `n:num`]
  99                   SUM_INTEGRAL_LBOUND_INCREASING) THEN
 100      REWRITE_TAC[] THEN ANTS_TAC THENL
 101       [CONJ_TAC THENL [POP_ASSUM MP_TAC THEN ARITH_TAC; ALL_TAC] THEN
 102        CONV_TAC REAL_RAT_REDUCE_CONV THEN CONJ_TAC THENL
 103         [REWRITE_TAC[IN_SEGMENT_CX_GEN] THEN REPEAT STRIP_TAC THENL
 104           [COMPLEX_DIFF_TAC THEN CONJ_TAC THEN UNDISCH_TAC `&1 <= Re x` THENL
 105             [REAL_ARITH_TAC; ALL_TAC] THEN
 106            ASM_CASES_TAC `x = Cx(&0)` THEN ASM_REWRITE_TAC[RE_CX] THENL
 107             [REAL_ARITH_TAC;
 108              UNDISCH_TAC `~(x = Cx(&0))` THEN CONV_TAC COMPLEX_FIELD];
 109            FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM REAL_OF_NUM_LE]) THEN
 110            ASM_REAL_ARITH_TAC];
 111         MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN STRIP_TAC THEN
 112         SUBGOAL_THEN `&0 < a /\ &0 < b` ASSUME_TAC THENL
 113          [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 114         ASM_SIMP_TAC[GSYM CX_LOG; RE_CX; LOG_MONO_LE_IMP]];
 115        ALL_TAC]] THEN
 116   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 117   MATCH_MP_TAC(REAL_ARITH `y <= x /\ a <= b ==> x <= a ==> y <= b`) THEN
 118   ASM_SIMP_TAC[GSYM CX_LOG; SUM_EQ_NUMSEG; REAL_OF_NUM_LT; LE_1; CLOG_1;
 119                ARITH_RULE `2 <= n ==> 0 < n`; RE_CX;
 120                REAL_ARITH `&0 < &n + &1`; REAL_EQ_IMP_LE] THEN
 121   REWRITE_TAC[GSYM CX_MUL; GSYM CX_SUB; GSYM CX_ADD; RE_CX] THEN
 122   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_SUB_RNEG] THENL
 123    [REWRITE_TAC[REAL_ARITH
 124      `(n + &1) * l' - (n + &1) + &1 <= (n * l - n + &1) + k * l <=>
 125       (n + &1) * l' <= (n + k) * l + &1`] THEN
 126     MATCH_MP_TAC REAL_LE_TRANS THEN
 127     EXISTS_TAC `(&n + &1) * (log(&n) + &1 / &n)` THEN CONJ_TAC THENL
 128      [MATCH_MP_TAC REAL_LE_LMUL THEN
 129       CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
 130       REWRITE_TAC[REAL_ARITH `x <= y + z <=> x - y <= z`] THEN
 131       ASM_SIMP_TAC[GSYM LOG_DIV; REAL_OF_NUM_LT; LT_NZ;
 132                    REAL_ARITH `&0 < &n + &1`;
 133                    REAL_FIELD `&0 < x ==> (x + &1) / x = &1 + &1 / x`] THEN
 134       MATCH_MP_TAC LOG_LE THEN SIMP_TAC[REAL_LE_DIV; REAL_POS];
 135       ALL_TAC] THEN
 136     REWRITE_TAC[REAL_ARITH
 137     `(n + &1) * (l + n') <= (n + k) * l + &1 <=>
 138       n' * (n + &1) <= (k - &1) * l + &1`] THEN
 139     ASM_SIMP_TAC[REAL_OF_NUM_EQ; REAL_LE_RADD; REAL_FIELD
 140      `~(n = &0) ==> &1 / n * (n + &1) = inv(n) + &1`] THEN
 141     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2)` THEN CONJ_TAC THENL
 142      [MATCH_MP_TAC REAL_LE_INV2 THEN
 143       REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
 144       ASM_ARITH_TAC;
 145       ALL_TAC] THEN
 146     CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_MUL_LID] THEN
 147     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `log(&2)` THEN
 148     REWRITE_TAC[LOG_2_BOUNDS] THEN MATCH_MP_TAC LOG_MONO_LE_IMP THEN
 149     REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LE] THEN ASM_ARITH_TAC;
 150     SUBGOAL_THEN `&0 <= log(&n)` MP_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
 151     MATCH_MP_TAC LOG_POS THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN
 152     ASM_ARITH_TAC]);;
 153
 154 (* ------------------------------------------------------------------------- *)
 155 (* The Mangoldt function and its key expansion.                              *)
 156 (* ------------------------------------------------------------------------- *)
 157
 158 let mangoldt = new_definition
 159  `mangoldt n = if ?p k. 1 <= k /\ prime p /\ n = p EXP k
 160                then log(&(@p. prime p /\ p divides n))
 161                else &0`;;
 162
 163 let MANGOLDT_1 = prove
 164  (`mangoldt 1 = &0`,
 165   REWRITE_TAC[mangoldt] THEN
 166   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN
 167   REWRITE_TAC[EXP_EQ_1] THEN MESON_TAC[PRIME_1; ARITH_RULE `~(1 <= 0)`]);;
 168
 169 let MANGOLDT_PRIMEPOW = prove
 170  (`!p k. prime p ==> mangoldt(p EXP k) = if 1 <= k then log(&p) else &0`,
 171   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[mangoldt] THEN
 172   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> ~(a /\ b ==> ~c)`] THEN
 173   ASM_SIMP_TAC[EQ_PRIME_EXP; LE_1] THEN
 174   REWRITE_TAC[TAUT `~(a /\ b ==> ~(c /\ d)) <=> d /\ c /\ a /\ b`] THEN
 175   ASM_REWRITE_TAC[UNWIND_THM1] THEN
 176   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT AP_TERM_TAC THEN
 177   ASM_SIMP_TAC[DIVIDES_PRIMEPOW] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
 178   ASM_MESON_TAC[PRIME_DIVEXP; prime; PRIME_1; DIVIDES_REFL; EXP_1]);;
 179
 180 let MANGOLDT_POS_LE = prove
 181  (`!n. &0 <= mangoldt n`,
 182   GEN_TAC THEN ASM_CASES_TAC `?p k. 1 <= k /\ prime p /\ n = p EXP k` THENL
 183    [FIRST_X_ASSUM(REPEAT_TCL CHOOSE_THEN STRIP_ASSUME_TAC) THEN
 184     ASM_SIMP_TAC[MANGOLDT_PRIMEPOW] THEN MATCH_MP_TAC LOG_POS THEN
 185     REWRITE_TAC[REAL_OF_NUM_LE] THEN
 186     FIRST_X_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN ARITH_TAC;
 187     ASM_REWRITE_TAC[mangoldt; REAL_LE_REFL]]);;
 188
 189 let LOG_MANGOLDT_SUM = prove
 190  (`!n. ~(n = 0) ==> log(&n) = sum {d | d divides n} (\d. mangoldt(d))`,
 191   REPEAT STRIP_TAC THEN ASM_CASES_TAC `n = 1` THENL
 192    [ASM_REWRITE_TAC[LOG_1; DIVIDES_ONE; SET_RULE `{x | x = a} = {a}`] THEN
 193     REWRITE_TAC[SUM_SING; mangoldt] THEN
 194     GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN
 195     REWRITE_TAC[EXP_EQ_1] THEN MESON_TAC[PRIME_1; ARITH_RULE `~(1 <= 0)`];
 196     ALL_TAC] THEN
 197   SUBGOAL_THEN `1 < n` MP_TAC THENL
 198    [ASM_ARITH_TAC; ALL_TAC] THEN
 199   SPEC_TAC(`n:num`,`n:num`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
 200   MATCH_MP_TAC INDUCT_COPRIME THEN REPEAT STRIP_TAC THENL
 201    [ASM_SIMP_TAC[LOG_MUL; GSYM REAL_OF_NUM_MUL; REAL_OF_NUM_LT;
 202                  ARITH_RULE `1 < a ==> 0 < a`] THEN
 203     MATCH_MP_TAC EQ_TRANS THEN
 204     EXISTS_TAC
 205      `sum ({d | d divides a} UNION {d | d divides b}) (\d. mangoldt d)` THEN
 206     CONJ_TAC THEN CONV_TAC SYM_CONV THENL
 207      [MATCH_MP_TAC SUM_UNION_NONZERO THEN REWRITE_TAC[IN_INTER] THEN
 208       ASM_SIMP_TAC[FINITE_DIVISORS; ARITH_RULE `1 < n ==> ~(n = 0)`] THEN
 209       REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[coprime; MANGOLDT_1];
 210       MATCH_MP_TAC SUM_SUPERSET THEN REWRITE_TAC[UNION_SUBSET; IN_UNION] THEN
 211       SIMP_TAC[SUBSET; IN_ELIM_THM; DIVIDES_LMUL; DIVIDES_RMUL] THEN
 212       X_GEN_TAC `d:num` THEN STRIP_TAC THEN REWRITE_TAC[mangoldt] THEN
 213       COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 214       ASM_MESON_TAC[PRIME_DIVPROD_POW]];
 215     ALL_TAC] THEN
 216   ASM_SIMP_TAC[DIVIDES_PRIMEPOW; GSYM REAL_OF_NUM_POW] THEN
 217   REWRITE_TAC[SET_RULE `{d | ?i. i <= k /\ d = p EXP i} =
 218                         IMAGE (\i. p EXP i) {i | i <= k}`] THEN
 219   ASM_SIMP_TAC[EQ_EXP; SUM_IMAGE; PRIME_GE_2;
 220                ARITH_RULE `2 <= p ==> ~(p = 0) /\ ~(p = 1)`] THEN
 221   ASM_SIMP_TAC[MANGOLDT_PRIMEPOW; o_DEF] THEN
 222   ASM_SIMP_TAC[GSYM SUM_RESTRICT_SET; IN_ELIM_THM; FINITE_NUMSEG_LE] THEN
 223   ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[GSYM numseg] THEN
 224   ASM_SIMP_TAC[LOG_POW; PRIME_IMP_NZ; REAL_OF_NUM_LT; LT_NZ] THEN
 225   SIMP_TAC[SUM_CONST; CARD_NUMSEG_1; FINITE_NUMSEG]);;
 226
 227 let MANGOLDT = prove
 228  (`!n. log(&(FACT n)) = sum(1..n) (\d. mangoldt(d) * floor(&n / &d))`,
 229   GEN_TAC THEN REWRITE_TAC[LOG_FACT] THEN MATCH_MP_TAC EQ_TRANS THEN
 230   EXISTS_TAC `sum(1..n) (\m. sum {d | d divides m} (\d. mangoldt d))` THEN
 231   SIMP_TAC[LOG_MANGOLDT_SUM; SUM_EQ_NUMSEG; LE_1] THEN
 232   MATCH_MP_TAC EQ_TRANS THEN
 233   EXISTS_TAC
 234    `sum (1..n) (\m. sum (1..n)
 235      (\d. mangoldt d * (if d divides m then &1 else &0)))` THEN
 236   CONJ_TAC THENL
 237    [MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `m:num` THEN
 238     STRIP_TAC THEN REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN
 239     MATCH_MP_TAC SUM_EQ_SUPERSET THEN
 240     ASM_SIMP_TAC[LE_1; FINITE_DIVISORS; IN_ELIM_THM; REAL_MUL_RZERO;
 241                  REAL_MUL_RID; SUBSET; IN_NUMSEG] THEN
 242     GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE_STRONG) THEN
 243     ASM_ARITH_TAC;
 244     GEN_REWRITE_TAC LAND_CONV [SUM_SWAP_NUMSEG] THEN
 245     MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `d:num` THEN
 246     ASM_SIMP_TAC[SUM_DIVISORS_FLOOR_LEMMA; LE_1; SUM_LMUL]]);;
 247
 248 (* ------------------------------------------------------------------------- *)
 249 (* The Chebyshev psi function and the key bounds on it.                      *)
 250 (* ------------------------------------------------------------------------- *)
 251
 252 let PSI_BOUND_INDUCT = prove
 253  (`!n. ~(n = 0)
 254        ==> sum(1..2*n) (\d. mangoldt(d)) -
 255            sum(1..n) (\d. mangoldt(d)) <= &9 * &n`,
 256   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 257   EXISTS_TAC `sum (n+1..2 * n) (\d. mangoldt d)` THEN CONJ_TAC THENL
 258    [MATCH_MP_TAC REAL_EQ_IMP_LE THEN REWRITE_TAC[REAL_EQ_SUB_RADD] THEN
 259     CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_UNION_EQ THEN
 260     ONCE_REWRITE_TAC[UNION_COMM] THEN REWRITE_TAC[FINITE_NUMSEG] THEN
 261     ASM_SIMP_TAC[NUMSEG_COMBINE_R; ARITH_RULE
 262      `~(n = 0) ==> 1 <= n + 1 /\ n <= 2 * n`] THEN
 263     REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY; IN_NUMSEG] THEN ARITH_TAC;
 264     ALL_TAC] THEN
 265   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
 266    `sum (n+1..2*n)
 267         (\d. mangoldt(d) * (floor(&(2 * n) / &d) - &2 * floor(&n / &d)))` THEN
 268   CONJ_TAC THENL
 269    [MATCH_MP_TAC SUM_LE_NUMSEG THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
 270     REWRITE_TAC[] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
 271     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[MANGOLDT_POS_LE] THEN
 272     MATCH_MP_TAC(REAL_ARITH `&1 <= a /\ b = &0 ==> &1 <= a - &2 * b`) THEN
 273     SUBGOAL_THEN `~(r = 0)` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 274     ASM_SIMP_TAC[FLOOR_DIV_DIV; FLOOR_NUM; REAL_OF_NUM_LE; REAL_OF_NUM_EQ] THEN
 275     ASM_SIMP_TAC[DIV_EQ_0; LE_RDIV_EQ] THEN ASM_ARITH_TAC;
 276     ALL_TAC] THEN
 277   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
 278    `sum (1..2*n)
 279         (\d. mangoldt(d) * (floor(&(2 * n) / &d) - &2 * floor(&n / &d)))` THEN
 280   CONJ_TAC THENL
 281    [MATCH_MP_TAC SUM_SUBSET THEN
 282     REWRITE_TAC[FINITE_NUMSEG; IN_DIFF; IN_NUMSEG] THEN
 283     CONJ_TAC THENL [ARITH_TAC; ALL_TAC] THEN
 284     X_GEN_TAC `r:num` THEN STRIP_TAC THEN
 285     SUBGOAL_THEN `~(r = 0)` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 286     MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[MANGOLDT_POS_LE] THEN
 287     ASM_SIMP_TAC[FLOOR_DIV_DIV; REAL_NEG_SUB; REAL_SUB_LE] THEN
 288     ASM_SIMP_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LE; MULT_DIV_LE];
 289     ALL_TAC] THEN
 290   REWRITE_TAC[REAL_ARITH `m * (f1 - &2 * f2) = m * f1 - &2 * m * f2`] THEN
 291   REWRITE_TAC[SUM_SUB_NUMSEG; SUM_LMUL] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 292   EXISTS_TAC `sum(1..2*n) (\d. mangoldt(d) * floor(&(2 * n) / &d)) -
 293               &2 * sum(1..n) (\d. mangoldt(d) * floor(&n / &d))` THEN
 294   CONJ_TAC THENL
 295    [MATCH_MP_TAC(REAL_ARITH `y' <= y ==> x - y <= x - y'`) THEN
 296     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
 297     MATCH_MP_TAC SUM_SUBSET THEN
 298     REWRITE_TAC[FINITE_NUMSEG; IN_DIFF; IN_NUMSEG] THEN
 299     SIMP_TAC[FLOOR_DIV_DIV; LE_1; FLOOR_NUM; REAL_LE_MUL; REAL_POS;
 300              MANGOLDT_POS_LE] THEN
 301     ARITH_TAC;
 302     ALL_TAC] THEN
 303   REWRITE_TAC[GSYM MANGOLDT] THEN
 304   MAP_EVERY (MP_TAC o C SPEC LOG_FACT_BOUNDS) [`n:num`; `2 * n`] THEN
 305   ASM_REWRITE_TAC[MULT_EQ_0; ARITH_EQ] THEN
 306   MATCH_MP_TAC(REAL_ARITH
 307     `a2 + e2 + &2 * (e1 - a1) <= m
 308      ==> abs(f2 - a2) <= e2 ==> abs(f1 - a1) <= e1 ==> f2 - &2 * f1 <= m`) THEN
 309   ASM_SIMP_TAC[GSYM REAL_OF_NUM_MUL; LOG_MUL; REAL_OF_NUM_LT; LT_NZ; ARITH] THEN
 310   MATCH_MP_TAC REAL_LE_TRANS THEN
 311   EXISTS_TAC
 312    `&6 * log(&n) + (&2 * log(&2) - &1) * &1 + (&2 * log(&2)) * &n` THEN
 313   CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
 314   MATCH_MP_TAC REAL_LE_TRANS THEN
 315   EXISTS_TAC `&6 * &n + (&2 * log(&2) - &1) * &n + (&2 * log(&2)) * &n` THEN
 316   CONJ_TAC THENL
 317    [MATCH_MP_TAC REAL_LE_ADD2 THEN
 318     ASM_SIMP_TAC[LOG_LE_REFL; REAL_LE_LMUL; REAL_POS; REAL_LE_RADD] THEN
 319     MATCH_MP_TAC REAL_LE_LMUL THEN
 320     ASM_REWRITE_TAC[REAL_OF_NUM_LE; ARITH_RULE `1 <= n <=> ~(n = 0)`];
 321     REWRITE_TAC[GSYM REAL_ADD_RDISTRIB] THEN
 322     MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_POS]] THEN
 323   MP_TAC LOG_2_BOUNDS THEN REAL_ARITH_TAC);;
 324
 325 let PSI_BOUND_EXP = prove
 326  (`!n. sum(1..2 EXP n) (\d. mangoldt(d)) <= &9 * &(2 EXP n)`,
 327   INDUCT_TAC THEN
 328   SIMP_TAC[EXP; SUM_SING_NUMSEG; MANGOLDT_1; REAL_LE_MUL; REAL_POS] THEN
 329   REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
 330   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 331    `s1 <= &9 * e ==> s2 - s1 <= &9 * e ==> s2 <= &9 * &2 * e`)) THEN
 332   MATCH_MP_TAC PSI_BOUND_INDUCT THEN
 333   REWRITE_TAC[EXP_EQ_0; ARITH]);;
 334
 335 let PSI_BOUND = prove
 336  (`!n. sum(1..n) (\d. mangoldt(d)) <= &18 * &n`,
 337   GEN_TAC THEN ASM_CASES_TAC `n <= 1` THENL
 338    [MATCH_MP_TAC REAL_LE_TRANS THEN
 339     EXISTS_TAC `sum(1..1) (\d. mangoldt d)` THEN CONJ_TAC THENL
 340      [MATCH_MP_TAC SUM_SUBSET; ALL_TAC] THEN
 341     REWRITE_TAC[SUM_SING_NUMSEG; FINITE_NUMSEG; IN_DIFF; IN_NUMSEG] THEN
 342     SIMP_TAC[MANGOLDT_POS_LE; MANGOLDT_1; REAL_LE_MUL; REAL_POS] THEN
 343     ASM_ARITH_TAC;
 344     ALL_TAC] THEN
 345   SUBGOAL_THEN `?k. n <= 2 EXP k /\ !l. l < k ==> ~(n <= 2 EXP l)`
 346   STRIP_ASSUME_TAC THENL
 347    [REWRITE_TAC[GSYM num_WOP] THEN EXISTS_TAC `n:num` THEN
 348     MP_TAC(SPEC `n:num` LT_POW2_REFL) THEN REWRITE_TAC[EXP] THEN ARITH_TAC;
 349     ALL_TAC] THEN
 350   MATCH_MP_TAC REAL_LE_TRANS THEN
 351   EXISTS_TAC `sum(1..2 EXP k) (\d. mangoldt d)` THEN CONJ_TAC THENL
 352    [MATCH_MP_TAC SUM_SUBSET THEN
 353     REWRITE_TAC[FINITE_NUMSEG; IN_DIFF; IN_NUMSEG; MANGOLDT_POS_LE] THEN
 354     ASM_ARITH_TAC;
 355     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&9 * &(2 EXP k)` THEN
 356     REWRITE_TAC[PSI_BOUND_EXP] THEN
 357     ASM_CASES_TAC `k = 0` THENL
 358      [FIRST_X_ASSUM SUBST_ALL_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN
 359     FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
 360      `~(k = 0) ==> k = SUC(k - 1)`)) THEN
 361     FIRST_X_ASSUM(MP_TAC o SPEC `k - 1`) THEN
 362     ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 363     REWRITE_TAC[REAL_OF_NUM_MUL; EXP; REAL_OF_NUM_LE] THEN ARITH_TAC]);;
 364
 365 (* ------------------------------------------------------------------------- *)
 366 (* Now Mertens's first theorem.                                              *)
 367 (* ------------------------------------------------------------------------- *)
 368
 369 let MERTENS_LEMMA = prove
 370  (`!n. ~(n = 0) ==> abs(sum(1..n) (\d. mangoldt(d) / &d) - log(&n)) <= &21`,
 371   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN
 372   EXISTS_TAC `&n` THEN ASM_SIMP_TAC[REAL_OF_NUM_LT; LT_NZ] THEN
 373   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM REAL_ABS_NUM] THEN
 374   REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_SUB_LDISTRIB; GSYM SUM_LMUL] THEN
 375   FIRST_ASSUM(MP_TAC o MATCH_MP LOG_FACT_BOUNDS) THEN REWRITE_TAC[MANGOLDT] THEN
 376   MATCH_MP_TAC(REAL_ARITH
 377    `abs(n - &1) <= n /\ abs(s' - s) <= (k - &1) * n - a
 378     ==> abs(s' - (nl - n + &1)) <= a
 379         ==> abs(s - nl) <= n * k`) THEN
 380   CONJ_TAC THENL
 381    [MATCH_MP_TAC(REAL_ARITH `&1 <= x ==> abs(x - &1) <= x`) THEN
 382     REWRITE_TAC[REAL_OF_NUM_LE] THEN ASM_ARITH_TAC;
 383     ALL_TAC] THEN
 384   REWRITE_TAC[GSYM SUM_SUB_NUMSEG] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 385   ONCE_REWRITE_TAC[REAL_ARITH `n * i / x:real = i * n / x`] THEN
 386   REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 387   EXISTS_TAC `sum(1..n) (\i. mangoldt i)` THEN CONJ_TAC THENL
 388    [MATCH_MP_TAC(REAL_ARITH `&0 <= --x /\ --x <= y ==> abs(x) <= y`) THEN
 389     REWRITE_TAC[GSYM SUM_NEG; REAL_ARITH
 390      `--(a * (x - y)):real = a * (y - x)`] THEN
 391     CONJ_TAC THENL
 392      [MATCH_MP_TAC SUM_POS_LE_NUMSEG THEN SIMP_TAC[] THEN
 393       X_GEN_TAC `i:num` THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LE_MUL;
 394       MATCH_MP_TAC SUM_LE_NUMSEG THEN SIMP_TAC[] THEN
 395        X_GEN_TAC `i:num` THEN STRIP_TAC THEN
 396       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
 397       MATCH_MP_TAC REAL_LE_LMUL] THEN
 398     ASM_REWRITE_TAC[MANGOLDT_POS_LE; REAL_SUB_LE; REAL_LE_SUB_RADD] THEN
 399     MP_TAC(SPEC `&n / &i` FLOOR) THEN REAL_ARITH_TAC;
 400     ALL_TAC] THEN
 401   MATCH_MP_TAC(REAL_ARITH
 402    `x <= (k - &2) * n /\ l <= n ==> x <= k * n - &2 * l`) THEN
 403   ASM_SIMP_TAC[LOG_LE_REFL] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 404   ASM_REWRITE_TAC[PSI_BOUND]);;
 405
 406 let MERTENS_MANGOLDT_VERSUS_LOG = prove
 407  (`!n s. s SUBSET (1..n)
 408          ==> abs (sum s (\d. mangoldt d / &d) -
 409                   sum {p | prime p /\ p IN s} (\p. log (&p) / &p)) <= &3`,
 410   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
 411    [ASM_REWRITE_TAC[NUMSEG_CLAUSES; ARITH; SUBSET_EMPTY] THEN
 412     DISCH_THEN SUBST_ALL_TAC THEN
 413     REWRITE_TAC[NOT_IN_EMPTY; EMPTY_GSPEC; SUM_CLAUSES] THEN REAL_ARITH_TAC;
 414     DISCH_TAC] THEN
 415   MATCH_MP_TAC REAL_LE_TRANS THEN
 416   EXISTS_TAC `abs(sum (1..n) (\d. mangoldt d / &d) -
 417                   sum {p | prime p /\ p IN 1..n} (\p. log (&p) / &p))` THEN
 418   CONJ_TAC THENL
 419    [SUBGOAL_THEN `FINITE(s:num->bool)` ASSUME_TAC THENL
 420      [ASM_MESON_TAC[FINITE_SUBSET; FINITE_NUMSEG]; ALL_TAC] THEN
 421     ONCE_REWRITE_TAC[CONJ_SYM] THEN
 422     ASM_SIMP_TAC[SUM_RESTRICT_SET; FINITE_NUMSEG] THEN
 423     ASM_SIMP_TAC[GSYM SUM_SUB; FINITE_NUMSEG] THEN
 424     MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x <= y ==> abs x <= abs y`) THEN
 425     CONJ_TAC THENL
 426      [MATCH_MP_TAC SUM_POS_LE; MATCH_MP_TAC SUM_SUBSET_SIMPLE] THEN
 427     ASM_SIMP_TAC[IN_DIFF; FINITE_NUMSEG; REAL_SUB_LE] THEN
 428     X_GEN_TAC `x:num` THEN STRIP_TAC THEN COND_CASES_TAC THEN
 429     ASM_SIMP_TAC[REAL_LE_DIV; MANGOLDT_POS_LE; REAL_POS] THEN
 430     GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV) [GSYM EXP_1] THEN
 431     ASM_SIMP_TAC[MANGOLDT_PRIMEPOW; LE_REFL; REAL_LE_REFL];
 432     ALL_TAC] THEN
 433   SUBGOAL_THEN `{p | prime p /\ p IN 1..n} = {p | prime p /\ p <= n}`
 434   SUBST1_TAC THENL
 435    [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_NUMSEG] THEN
 436     MESON_TAC[ARITH_RULE `2 <= p ==> 1 <= p`; PRIME_GE_2];
 437     ALL_TAC] THEN
 438   SUBGOAL_THEN
 439    `sum(1..n) (\d. mangoldt d / &d) -
 440     sum {p | prime p /\ p <= n} (\p. log (&p) / &p) =
 441     sum {p EXP k | prime p /\ p EXP k <= n /\ k >= 2} (\d. mangoldt d / &d)`
 442   SUBST1_TAC THENL
 443    [SUBGOAL_THEN
 444      `sum {p | prime p /\ p <= n} (\p. log (&p) / &p) =
 445       sum {p | prime p /\ p <= n} (\d. mangoldt d / &d)`
 446     SUBST1_TAC THENL
 447      [MATCH_MP_TAC SUM_EQ THEN REWRITE_TAC[IN_ELIM_THM] THEN
 448       REPEAT STRIP_TAC THEN
 449       GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV) [GSYM EXP_1] THEN
 450       ASM_SIMP_TAC[MANGOLDT_PRIMEPOW; ARITH];
 451       ALL_TAC] THEN
 452     REWRITE_TAC[REAL_EQ_SUB_RADD] THEN MATCH_MP_TAC EQ_TRANS THEN
 453     EXISTS_TAC
 454      `sum {p EXP k | prime p /\ p EXP k <= n /\ k >= 1}
 455           (\d. mangoldt d / &d)` THEN
 456     CONJ_TAC THENL
 457      [MATCH_MP_TAC SUM_SUPERSET THEN
 458       SIMP_TAC[IN_ELIM_THM; SUBSET; IN_NUMSEG] THEN
 459       CONJ_TAC THEN GEN_TAC THEN STRIP_TAC THEN
 460       ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; EXP_EQ_0] THENL
 461        [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
 462       REWRITE_TAC[real_div; REAL_ENTIRE] THEN DISJ1_TAC THEN
 463       REWRITE_TAC[mangoldt] THEN ASM_MESON_TAC[GE];
 464       ALL_TAC] THEN
 465     CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_UNION_EQ THEN CONJ_TAC THENL
 466      [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
 467       REWRITE_TAC[SUBSET; IN_ELIM_THM; FINITE_NUMSEG; IN_NUMSEG; LE_0] THEN
 468       MESON_TAC[];
 469       ALL_TAC] THEN
 470     CONJ_TAC THENL
 471      [REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM; NOT_IN_EMPTY] THEN
 472       MESON_TAC[PRIME_EXP; ARITH_RULE `~(1 >= 2)`];
 473       REWRITE_TAC[ARITH_RULE `k >= 1 <=> k >= 2 \/ k = 1`] THEN
 474       REWRITE_TAC[EXTENSION; IN_UNION; IN_ELIM_THM] THEN MESON_TAC[EXP_1]];
 475     ALL_TAC] THEN
 476   MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x <= y ==> abs(x) <= y`) THEN
 477   CONJ_TAC THENL
 478    [MATCH_MP_TAC SUM_POS_LE THEN
 479     SIMP_TAC[REAL_LE_DIV; REAL_POS; MANGOLDT_POS_LE]THEN
 480     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
 481     REWRITE_TAC[SUBSET; IN_ELIM_THM; FINITE_NUMSEG; IN_NUMSEG; LE_0] THEN
 482     MESON_TAC[];
 483     ALL_TAC] THEN
 484   MATCH_MP_TAC REAL_LE_TRANS THEN
 485   EXISTS_TAC
 486    `sum {p | p IN 1..n /\ prime p}
 487         (\p. sum (2..n) (\k. log(&p) / &p pow k))` THEN
 488   CONJ_TAC THENL
 489    [SIMP_TAC[SUM_SUM_PRODUCT; FINITE_NUMSEG; FINITE_RESTRICT] THEN
 490     MATCH_MP_TAC SUM_LE_INCLUDED THEN EXISTS_TAC `\(p,k). p EXP k` THEN
 491     SIMP_TAC[FINITE_PRODUCT; FINITE_NUMSEG; FINITE_RESTRICT] THEN
 492     CONJ_TAC THENL
 493      [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
 494       REWRITE_TAC[SUBSET; IN_ELIM_THM; FINITE_NUMSEG; IN_NUMSEG; LE_0] THEN
 495       MESON_TAC[];
 496       ALL_TAC] THEN
 497     REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM; EXISTS_PAIR_THM] THEN
 498     SIMP_TAC[IN_ELIM_THM; IN_NUMSEG; REAL_LE_DIV; REAL_POW_LE; REAL_POS;
 499              LOG_POS; REAL_OF_NUM_LE] THEN
 500     X_GEN_TAC `x:num` THEN
 501     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `p:num` THEN
 502     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:num` THEN
 503     STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
 504     ASM_SIMP_TAC[MANGOLDT_PRIMEPOW; GSYM REAL_OF_NUM_POW; REAL_LE_REFL;
 505                  ARITH_RULE `k >= 2 ==> 1 <= k /\ 2 <= k`] THEN
 506     ASM_SIMP_TAC[PRIME_IMP_NZ; ARITH_RULE `1 <= k <=> ~(k = 0)`] THEN
 507     CONJ_TAC THENL
 508      [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `p EXP k` THEN ASM_SIMP_TAC[] THEN
 509       GEN_REWRITE_TAC LAND_CONV [GSYM EXP_1] THEN
 510       ASM_SIMP_TAC[PRIME_IMP_NZ; LE_EXP] THEN ASM_ARITH_TAC;
 511       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `p EXP k` THEN ASM_SIMP_TAC[] THEN
 512       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 EXP k` THEN
 513       ASM_SIMP_TAC[LT_POW2_REFL; LT_IMP_LE; EXP_MONO_LE; PRIME_GE_2]];
 514     ALL_TAC] THEN
 515   REWRITE_TAC[real_div; SUM_LMUL; GSYM REAL_POW_INV; SUM_GP] THEN
 516   MATCH_MP_TAC REAL_LE_TRANS THEN
 517   EXISTS_TAC `sum {p | p IN 1..n /\ prime p}
 518                   (\p. log(&p) / (&p * (&p - &1)))` THEN
 519   CONJ_TAC THENL
 520    [MATCH_MP_TAC SUM_LE THEN SIMP_TAC[FINITE_NUMSEG; FINITE_RESTRICT] THEN
 521     X_GEN_TAC `p:num` THEN REWRITE_TAC[IN_ELIM_THM; IN_NUMSEG] THEN
 522     ASM_SIMP_TAC[REAL_INV_EQ_1; REAL_OF_NUM_EQ; PRIME_GE_2;
 523                  ARITH_RULE `2 <= p ==> ~(p = 1)`] THEN
 524     STRIP_TAC THEN COND_CASES_TAC THEN
 525     ASM_SIMP_TAC[REAL_MUL_RZERO; REAL_LE_DIV; REAL_LE_MUL; REAL_SUB_LE;
 526                  REAL_OF_NUM_LE; LOG_POS; LE_0] THEN
 527     REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LE_LMUL THEN
 528     ASM_SIMP_TAC[LOG_POS; REAL_OF_NUM_LE] THEN
 529     MATCH_MP_TAC(REAL_ARITH
 530      `&0 <= y * z /\ x * z <= a ==> (x - y) * z <= a`) THEN
 531     CONJ_TAC THENL
 532      [MATCH_MP_TAC REAL_LE_MUL THEN
 533       ASM_SIMP_TAC[REAL_POW_LE; REAL_LE_INV_EQ; REAL_POS; REAL_SUB_LE] THEN
 534       MATCH_MP_TAC REAL_INV_LE_1 THEN ASM_REWRITE_TAC[REAL_OF_NUM_LE];
 535       ALL_TAC] THEN
 536     MATCH_MP_TAC REAL_EQ_IMP_LE THEN
 537     FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN
 538     REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN CONV_TAC REAL_FIELD;
 539     ALL_TAC] THEN
 540   MATCH_MP_TAC REAL_LE_TRANS THEN
 541   EXISTS_TAC `sum (2..n)  (\p. log(&p) / (&p * (&p - &1)))` THEN
 542   CONJ_TAC THENL
 543    [MATCH_MP_TAC SUM_SUBSET THEN SIMP_TAC[FINITE_NUMSEG; FINITE_RESTRICT] THEN
 544     REWRITE_TAC[IN_DIFF; IN_NUMSEG; IN_ELIM_THM] THEN
 545     CONJ_TAC THENL [MESON_TAC[PRIME_GE_2]; ALL_TAC] THEN
 546     ASM_SIMP_TAC[LOG_POS; REAL_OF_NUM_LE; ARITH_RULE `2 <= p ==> 1 <= p`;
 547                  REAL_LE_MUL; REAL_POS; REAL_SUB_LE; REAL_LE_DIV];
 548     ALL_TAC] THEN
 549   MATCH_MP_TAC REAL_LE_TRANS THEN
 550   EXISTS_TAC `sum (2..n) (\m. log(&m) / (&m - &1) pow 2)` THEN CONJ_TAC THENL
 551    [MATCH_MP_TAC SUM_LE_NUMSEG THEN REPEAT STRIP_TAC THEN
 552     REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LE_LMUL THEN
 553     ASM_SIMP_TAC[LOG_POS; REAL_OF_NUM_LE; ARITH_RULE `2 <= p ==> 1 <= p`] THEN
 554     MATCH_MP_TAC REAL_LE_INV2 THEN
 555     ASM_SIMP_TAC[REAL_POW_2; REAL_LE_RMUL_EQ; REAL_LT_MUL; REAL_LT_IMP_LE;
 556                  REAL_SUB_LT; REAL_OF_NUM_LT; ARITH_RULE `1 < p <=> 2 <= p`;
 557                  REAL_ARITH `x - &1 <= x`];
 558     ALL_TAC] THEN
 559   ASM_CASES_TAC `n < 2` THENL
 560    [RULE_ASSUM_TAC(REWRITE_RULE[GSYM NUMSEG_EMPTY]);
 561     RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT])] THEN
 562   ASM_SIMP_TAC[SUM_CLAUSES] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 563   ASM_SIMP_TAC[SUM_CLAUSES_LEFT; ARITH] THEN
 564   MATCH_MP_TAC(REAL_ARITH
 565     `x <= &1 /\ y <= e - &1 ==> x + y <= e`) THEN
 566   CONJ_TAC THENL [MP_TAC LOG_2_BOUNDS THEN REAL_ARITH_TAC; ALL_TAC] THEN
 567   ASM_CASES_TAC `n < 3` THENL
 568    [RULE_ASSUM_TAC(REWRITE_RULE[GSYM NUMSEG_EMPTY]);
 569     RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT])] THEN
 570   ASM_SIMP_TAC[SUM_CLAUSES] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 571   MP_TAC(ISPECL
 572    [`\z. clog(z) / (z - Cx(&1)) pow 2`;
 573     `\z. clog(z - Cx(&1)) - clog(z) - clog(z) / (z - Cx(&1))`;
 574     `3`; `n:num`] SUM_INTEGRAL_UBOUND_DECREASING) THEN
 575   ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN ANTS_TAC THENL
 576    [CONJ_TAC THENL
 577      [REWRITE_TAC[IN_SEGMENT_CX_GEN] THEN X_GEN_TAC `z:complex` THEN
 578       STRIP_TAC THENL
 579        [COMPLEX_DIFF_TAC THEN SIMP_TAC[COMPLEX_SUB_RZERO; COMPLEX_MUL_LID] THEN
 580         ASM_SIMP_TAC[RE_SUB; RE_CX; REAL_SUB_LT] THEN
 581         ASM_SIMP_TAC[REAL_ARITH `&2 <= x ==> &1 < x /\ &0 < x`] THEN
 582         SUBGOAL_THEN `~(z = Cx(&0)) /\ ~(z = Cx(&1))` MP_TAC THENL
 583          [ALL_TAC; CONV_TAC COMPLEX_FIELD] THEN
 584         REPEAT STRIP_TAC THEN UNDISCH_TAC `&2 <= Re z` THEN
 585         ASM_REWRITE_TAC[RE_CX] THEN REAL_ARITH_TAC;
 586         RULE_ASSUM_TAC(REWRITE_RULE[GSYM REAL_OF_NUM_LE]) THEN
 587         ASM_ARITH_TAC];
 588       ALL_TAC] THEN
 589     MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN STRIP_TAC THEN
 590     MP_TAC(SPECL [`\z. clog(z) / (z - Cx(&1)) pow 2`;
 591                   `\z. inv(z * (z - Cx(&1)) pow 2) -
 592                        Cx(&2) * clog(z) / (z - Cx(&1)) pow 3`;
 593                   `Cx(x)`; `Cx(y)`] COMPLEX_MVT_LINE) THEN
 594     REWRITE_TAC[] THEN ANTS_TAC THENL
 595      [REWRITE_TAC[IN_SEGMENT_CX_GEN] THEN X_GEN_TAC `z:complex` THEN
 596       REWRITE_TAC[REAL_ARITH `a <= x /\ x <= b \/ b <= x /\ x <= a <=>
 597                          a <= x /\ x <= b \/ b < a /\ b <= x /\ x <= a`] THEN
 598       STRIP_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
 599       COMPLEX_DIFF_TAC THEN REWRITE_TAC[GSYM CONJ_ASSOC] THEN
 600       CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 601       CONV_TAC NUM_REDUCE_CONV THEN
 602       SUBGOAL_THEN `~(z = Cx(&0)) /\ ~(z = Cx(&1))` MP_TAC THENL
 603        [ALL_TAC; CONV_TAC COMPLEX_FIELD] THEN
 604       CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
 605       REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[RE_CX; IM_CX] THEN
 606       REAL_ARITH_TAC;
 607       ALL_TAC] THEN
 608     GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `x <= y <=> x - y <= &0`] THEN
 609     DISCH_THEN(X_CHOOSE_THEN `w:complex`
 610      (CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC)) THEN
 611     REWRITE_TAC[GSYM CX_SUB; RE_MUL_CX] THEN
 612     REWRITE_TAC[REAL_ARITH `a * (y - x) <= &0 <=> &0 <= --a * (y - x)`] THEN
 613     MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[REAL_SUB_LE] THEN
 614     REWRITE_TAC[RE_SUB; REAL_NEG_SUB; REAL_SUB_LE] THEN
 615     SUBGOAL_THEN `real w` ASSUME_TAC THENL
 616      [ASM_MESON_TAC[REAL_SEGMENT; REAL_CX]; ALL_TAC] THEN
 617     FIRST_X_ASSUM(SUBST_ALL_TAC o SYM o GEN_REWRITE_RULE I [REAL]) THEN
 618     ABBREV_TAC `u = Re w` THEN
 619     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_SEGMENT_CX]) THEN
 620     ASM_SIMP_TAC[REAL_ARITH
 621      `x <= y
 622       ==> (x <= u /\ u <= y \/ y <= u /\ u <= x <=> x <= u /\ u <= y)`] THEN
 623     STRIP_TAC THEN
 624     SUBGOAL_THEN `&0 < u /\ &1 < u /\ &2 <= u` STRIP_ASSUME_TAC THENL
 625      [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 626     ASM_SIMP_TAC[GSYM CX_LOG; GSYM CX_SUB; GSYM CX_POW; GSYM CX_DIV;
 627                  GSYM CX_MUL; GSYM CX_INV; RE_CX] THEN
 628     REWRITE_TAC[REAL_POW_2; real_div; REAL_INV_MUL; REAL_MUL_ASSOC;
 629                 REAL_RING `(x:real) pow 3 = x * x pow 2`] THEN
 630     ASM_SIMP_TAC[REAL_LE_RMUL_EQ; REAL_LT_INV_EQ; REAL_SUB_LT] THEN
 631     ASM_SIMP_TAC[GSYM real_div; REAL_LE_RDIV_EQ; REAL_SUB_LT] THEN
 632     MATCH_MP_TAC(REAL_ARITH
 633      `a * b <= &1 /\ &1 / &2 <= c ==> b * a <= &2 * c`) THEN
 634     ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ] THEN
 635     CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 636     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `log(&2)` THEN
 637     REWRITE_TAC[LOG_2_BOUNDS] THEN MATCH_MP_TAC LOG_MONO_LE_IMP THEN
 638     ASM_REAL_ARITH_TAC;
 639     ALL_TAC] THEN
 640   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 641   MATCH_MP_TAC(REAL_ARITH `x = y /\ a <= b ==> x <= a ==> y <= b`) THEN
 642   CONJ_TAC THENL [MATCH_MP_TAC SUM_EQ_NUMSEG; ALL_TAC] THEN
 643   ASM_SIMP_TAC[GSYM CX_SUB; GSYM CX_LOG; GSYM CX_DIV; REAL_SUB_LT; ARITH;
 644       RE_CX; REAL_OF_NUM_LT; ARITH_RULE `3 <= n ==> 0 < n /\ 1 < n`;
 645       GSYM CX_POW] THEN
 646   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 647   REWRITE_TAC[LOG_1; REAL_ARITH `a - (&0 - x - x / &1) = a + &2 * x`] THEN
 648   MATCH_MP_TAC(REAL_ARITH
 649    `a <= e - &2 /\ x <= &1 ==> a + &2 * x <= e`) THEN
 650   REWRITE_TAC[LOG_2_BOUNDS] THEN
 651   MATCH_MP_TAC(REAL_ARITH `a <= b /\ --c <= e ==> a - b - c <= e`) THEN
 652   REWRITE_TAC[REAL_SUB_REFL; REAL_ARITH `--x <= &0 <=> &0 <= x`] THEN
 653   ASM_SIMP_TAC[REAL_LE_DIV; REAL_SUB_LE; LOG_POS; REAL_OF_NUM_LE;
 654     REAL_OF_NUM_LT; LOG_MONO_LE_IMP; REAL_ARITH `x - &1 <= x`; REAL_SUB_LT;
 655     LE_0; ARITH_RULE `3 <= n ==> 1 <= n /\ 1 < n`]);;
 656
 657 let MERTENS = prove
 658  (`!n. ~(n = 0)
 659        ==> abs(sum {p | prime p /\ p <= n}
 660                    (\p. log(&p) / &p) - log(&n)) <= &24`,
 661   REPEAT STRIP_TAC THEN
 662   FIRST_ASSUM(MP_TAC o MATCH_MP MERTENS_LEMMA) THEN
 663   MATCH_MP_TAC(REAL_ARITH
 664    `abs(s1 - s2) <= k - e ==> abs(s1 - l) <= e ==> abs(s2 - l) <= k`) THEN
 665   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 666   SUBGOAL_THEN `{p | prime p /\ p <= n} = {p | prime p /\ p IN 1..n}`
 667   SUBST1_TAC THENL
 668    [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_NUMSEG] THEN
 669     MESON_TAC[ARITH_RULE `2 <= p ==> 1 <= p`; PRIME_GE_2];
 670     MATCH_MP_TAC MERTENS_MANGOLDT_VERSUS_LOG THEN
 671     EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[SUBSET_REFL]]);;