100/primerecip.ml

   1 (* ========================================================================= *)
   2 (* Divergence of prime reciprocal series.                                    *)
   3 (* ========================================================================= *)
   4
   5 (* ------------------------------------------------------------------------- *)
   6 (* Now load other stuff needed.                                              *)
   7 (* ------------------------------------------------------------------------- *)
   8
   9 needs "100/bertrand.ml";;
  10 needs "100/divharmonic.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Variant of induction.                                                     *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let INDUCTION_FROM_1 = prove
  17  (`!P. P 0 /\ P 1 /\ (!n. 1 <= n /\ P n ==> P(SUC n)) ==> !n. P n`,
  18   GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN
  19   ASM_MESON_TAC[num_CONV `1`; ARITH_RULE `n = 0 \/ 1 <= n`]);;
  20
  21 (* ------------------------------------------------------------------------- *)
  22 (* Evaluate sums over explicit intervals.                                    *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 let SUM_CONV =
  26   let pth = prove
  27    (`sum(1..1) f = f 1 /\ sum(1..SUC n) f = sum(1..n) f + f(SUC n)`,
  28     SIMP_TAC[SUM_CLAUSES_NUMSEG; LE_0;
  29              ARITH_RULE `1 <= SUC n`; SUM_SING_NUMSEG]) in
  30   let econv_0 = GEN_REWRITE_CONV I [CONJUNCT1 pth]
  31   and econv_1 = GEN_REWRITE_CONV I [CONJUNCT2 pth] in
  32   let rec sconv tm =
  33     (econv_0 ORELSEC
  34      (LAND_CONV(RAND_CONV num_CONV) THENC econv_1 THENC
  35       COMB2_CONV (RAND_CONV sconv) (RAND_CONV NUM_SUC_CONV))) tm in
  36   sconv;;
  37
  38 (* ------------------------------------------------------------------------- *)
  39 (* Lower bound relative to harmonic series.                                  *)
  40 (* ------------------------------------------------------------------------- *)
  41
  42 let PRIMERECIP_HARMONIC_LBOUND = prove
  43  (`!n. (&3 / (&16 * ln(&32))) * sum(1..n) (\i. &1 / &i) <=
  44        sum(1..32 EXP n) (\i. if prime(i) then &1 / &i else &0)`,
  45   MATCH_MP_TAC INDUCTION_FROM_1 THEN CONJ_TAC THENL
  46    [SIMP_TAC[SUM_TRIV_NUMSEG; ARITH; SUM_SING_NUMSEG; REAL_MUL_RZERO] THEN
  47     REWRITE_TAC[PRIME_1; REAL_LE_REFL];
  48     ALL_TAC] THEN
  49   CONJ_TAC THENL
  50    [REWRITE_TAC[ARITH; SUM_SING_NUMSEG] THEN
  51     CONV_TAC(RAND_CONV SUM_CONV) THEN REWRITE_TAC[] THEN
  52     CONV_TAC(ONCE_DEPTH_CONV PRIME_CONV) THEN
  53     CONV_TAC REAL_RAT_REDUCE_CONV THEN
  54     REWRITE_TAC[SYM(REAL_RAT_REDUCE_CONV `&2 pow 5`)] THEN
  55     SIMP_TAC[LN_POW; REAL_OF_NUM_LT; ARITH; real_div; REAL_INV_MUL] THEN
  56     REWRITE_TAC[REAL_MUL_ASSOC; REAL_MUL_RID] THEN
  57     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
  58     SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
  59     CONV_TAC REAL_RAT_REDUCE_CONV THEN
  60     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_DIV] THEN
  61     MATCH_MP_TAC REAL_LE_INV2 THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
  62     REWRITE_TAC[LN_2_COMPOSITION; real_div; real_sub] THEN
  63     CONV_TAC REALCALC_REL_CONV;
  64     ALL_TAC] THEN
  65   X_GEN_TAC `n:num` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  66   MATCH_MP_TAC(REAL_ARITH
  67    `b - a <= s2 - s1 ==> a <= s1 ==> b <= s2`) THEN
  68   REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN
  69   REWRITE_TAC[SUM_CLAUSES_NUMSEG; REAL_ADD_SUB; ARITH_RULE `1 <= SUC n`] THEN
  70   MP_TAC(SPEC `32 EXP n` PII_UBOUND_5) THEN ANTS_TAC THENL
  71    [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `32 EXP 1` THEN
  72     ASM_REWRITE_TAC[LE_EXP] THEN REWRITE_TAC[ARITH];
  73     ALL_TAC] THEN
  74   MP_TAC(SPEC `32 EXP (SUC n)` PII_LBOUND) THEN ANTS_TAC THENL
  75    [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `32 EXP 1` THEN
  76     ASM_REWRITE_TAC[LE_EXP] THEN REWRITE_TAC[ARITH] THEN ARITH_TAC;
  77     ALL_TAC] THEN
  78   REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP(REAL_ARITH
  79    `a <= s1 /\ s2 <= b ==> a - b <= s1 - s2`)) THEN
  80   SIMP_TAC[pii; PSUM_SUM_NUMSEG; EXP_EQ_0; ARITH; ADD_SUB2] THEN
  81   REWRITE_TAC[GSYM REAL_OF_NUM_POW] THEN
  82   REWRITE_TAC[EXP; ARITH_RULE `32 * n = n + 31 * n`] THEN
  83   SIMP_TAC[SUM_ADD_SPLIT; ARITH_RULE `1 <= n + 1`; REAL_ADD_SUB] THEN
  84   REWRITE_TAC[ARITH_RULE `n + 31 * n = 32 * n`] THEN
  85   REWRITE_TAC[GSYM(CONJUNCT2 EXP)] THEN STRIP_TAC THEN
  86   MATCH_MP_TAC REAL_LE_TRANS THEN
  87   EXISTS_TAC
  88    `inv(&32 pow (SUC n)) *
  89     sum(32 EXP n + 1 .. 32 EXP SUC n) (\i. if prime i then &1 else &0)` THEN
  90   CONJ_TAC THENL
  91    [ALL_TAC;
  92     REWRITE_TAC[GSYM SUM_LMUL] THEN MATCH_MP_TAC SUM_LE_NUMSEG THEN
  93     X_GEN_TAC `i:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
  94     COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL; REAL_MUL_RZERO] THEN
  95     REWRITE_TAC[real_div; REAL_MUL_LID; REAL_MUL_RID] THEN
  96     MATCH_MP_TAC REAL_LE_INV2 THEN
  97     ASM_REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
  98     UNDISCH_TAC `32 EXP n + 1 <= i` THEN
  99     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 100     SIMP_TAC[ARITH_RULE `~(0 < i) <=> i = 0`] THEN
 101     REWRITE_TAC[LE; ARITH; ADD_EQ_0]] THEN
 102   GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
 103   SIMP_TAC[GSYM real_div; REAL_POW_LT; REAL_LE_RDIV_EQ;
 104            REAL_OF_NUM_LT; ARITH] THEN
 105   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 106     `a <= x ==> b <= a ==> b <= x`)) THEN
 107   SIMP_TAC[LN_POW; REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
 108   REWRITE_TAC[real_pow; GSYM REAL_OF_NUM_SUC] THEN
 109   REWRITE_TAC[REAL_FIELD
 110    `&1 / &2 * (&32 * n32) / (n1 * l) - &5 * n32 / (n * l) =
 111     (n32 / l) * (&16 / n1 - &5 / n)`] THEN
 112   REWRITE_TAC[REAL_FIELD
 113    `(&3 / (&16 * l) * i) * &32 * n32 = (n32 / l) * (&6 * i)`] THEN
 114   MATCH_MP_TAC REAL_LE_LMUL THEN
 115   SIMP_TAC[REAL_LE_DIV; REAL_POW_LE; LN_POS; REAL_OF_NUM_LE; ARITH] THEN
 116   REWRITE_TAC[real_div; REAL_ARITH
 117    `&6 * &1 * n1 <= &16 * n1 - &5 * n <=> n <= inv(inv(&2)) * n1`] THEN
 118   REWRITE_TAC[GSYM REAL_INV_MUL] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
 119   POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN REAL_ARITH_TAC);;
 120
 121 (* ------------------------------------------------------------------------- *)
 122 (* Hence an overall lower bound.                                             *)
 123 (* ------------------------------------------------------------------------- *)
 124
 125 let PRIMERECIP_LBOUND = prove
 126  (`!n. &3 / (&32 * ln(&32)) * &n
 127        <= sum (1 .. 32 EXP (2 EXP n)) (\i. if prime i then &1 / &i else &0)`,
 128   GEN_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 129   EXISTS_TAC `&3 / (&16 * ln(&32)) * sum (1 .. 2 EXP n) (\i. &1 / &i)` THEN
 130   REWRITE_TAC[PRIMERECIP_HARMONIC_LBOUND] THEN
 131   REWRITE_TAC[REAL_FIELD
 132    `&3 / (&32 * ln(&32)) * &n = &3 / (&16 * ln(&32)) * (&n / &2)`] THEN
 133   MATCH_MP_TAC REAL_LE_LMUL THEN
 134   REWRITE_TAC[REWRITE_RULE[real_ge] HARMONIC_LEMMA] THEN
 135   SIMP_TAC[REAL_LE_DIV; REAL_LE_MUL; LN_POS; REAL_OF_NUM_LE; ARITH]);;
 136
 137 (* ------------------------------------------------------------------------- *)
 138 (* General lemma.                                                            *)
 139 (* ------------------------------------------------------------------------- *)
 140
 141 let UNBOUNDED_DIVERGENT = prove
 142  (`!s. (!k. ?N. !n. n >= N ==> sum(1..n) s >= k)
 143        ==> ~(convergent(\n. sum(1..n) s))`,
 144   REWRITE_TAC[convergent; SEQ] THEN
 145   REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `&1`) THEN
 146   REWRITE_TAC[REAL_LT_01] THEN STRIP_TAC THEN
 147   FIRST_X_ASSUM(MP_TAC o SPEC `l + &1`) THEN
 148   REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `M:num` THEN
 149   DISCH_THEN(MP_TAC o SPEC `M + N:num`) THEN
 150   FIRST_X_ASSUM(MP_TAC o SPEC `M + N:num`) THEN
 151   REWRITE_TAC[LE_ADD; ONCE_REWRITE_RULE[ADD_SYM] LE_ADD; GE] THEN
 152   REAL_ARITH_TAC);;
 153
 154 (* ------------------------------------------------------------------------- *)
 155 (* Hence divergence.                                                         *)
 156 (* ------------------------------------------------------------------------- *)
 157
 158 let PRIMERECIP_DIVERGES_NUMSEG = prove
 159  (`~(convergent (\n. sum (1..n) (\i. if prime i then &1 / &i else &0)))`,
 160   MATCH_MP_TAC UNBOUNDED_DIVERGENT THEN X_GEN_TAC `k:real` THEN
 161   MP_TAC(SPEC `&3 / (&32 * ln(&32))` REAL_ARCH) THEN
 162   SIMP_TAC[REAL_LT_DIV; LN_POS_LT; REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
 163   DISCH_THEN(MP_TAC o SPEC `k:real`) THEN DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN
 164   EXISTS_TAC `32 EXP (2 EXP N)` THEN
 165   X_GEN_TAC `n:num` THEN REWRITE_TAC[GE; real_ge] THEN STRIP_TAC THEN
 166   MATCH_MP_TAC REAL_LE_TRANS THEN
 167   EXISTS_TAC `&N * &3 / (&32 * ln (&32))` THEN
 168   ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 169   GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
 170   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
 171    `sum(1 .. 32 EXP (2 EXP N)) (\i. if prime i then &1 / &i else &0)` THEN
 172   REWRITE_TAC[PRIMERECIP_LBOUND] THEN
 173   FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
 174   SIMP_TAC[SUM_ADD_SPLIT; ARITH_RULE `1 <= n + 1`; REAL_LE_ADDR] THEN
 175   MATCH_MP_TAC SUM_POS_LE_NUMSEG THEN REPEAT STRIP_TAC THEN
 176   REWRITE_TAC[] THEN COND_CASES_TAC THEN SIMP_TAC[REAL_LE_DIV; REAL_POS]);;
 177
 178 (* ------------------------------------------------------------------------- *)
 179 (* A perhaps more intuitive formulation.                                     *)
 180 (* ------------------------------------------------------------------------- *)
 181
 182 let PRIMERECIP_DIVERGES = prove
 183  (`~(convergent (\n. sum {p | prime p /\ p <= n} (\p. &1 / &p)))`,
 184   MP_TAC PRIMERECIP_DIVERGES_NUMSEG THEN
 185   MATCH_MP_TAC(TAUT `(a <=> b) ==> ~a ==> ~b`) THEN
 186   AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `n:num` THEN
 187   SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THENL
 188    [SUBGOAL_THEN `{p | prime p /\ p <= 0} = {}`
 189      (fun th -> SIMP_TAC[SUM_CLAUSES; SUM_TRIV_NUMSEG; th; ARITH]) THEN
 190     REWRITE_TAC[EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY; LE] THEN
 191     MESON_TAC[PRIME_0];
 192     ALL_TAC] THEN
 193   ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; ARITH_RULE `1 <= SUC n`] THEN
 194   SUBGOAL_THEN
 195    `{p | prime p /\ p <= SUC n} =
 196         if prime(SUC n) then (SUC n) INSERT {p | prime p /\ p <= n}
 197         else {p | prime p /\ p <= n}`
 198   SUBST1_TAC THENL
 199    [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT] THEN
 200     GEN_TAC THEN COND_CASES_TAC THEN
 201     REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; LE] THEN
 202     ASM_MESON_TAC[];
 203     ALL_TAC] THEN
 204   COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_ADD_RID] THEN
 205   SUBGOAL_THEN `FINITE {p | prime p /\ p <= n}`
 206    (fun th -> SIMP_TAC[SUM_CLAUSES; th])
 207   THENL
 208    [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `1..n` THEN
 209     SIMP_TAC[FINITE_NUMSEG; IN_NUMSEG; IN_ELIM_THM; SUBSET] THEN
 210     MESON_TAC[PRIME_0; ARITH_RULE `1 <= i <=> ~(i = 0)`];
 211     REWRITE_TAC[IN_ELIM_THM; ARITH_RULE `~(SUC n <= n)`; REAL_ADD_AC]]);;