100/dirichlet.ml

   1 (* ========================================================================= *)
   2 (* Dirichlet's theorem.                                                      *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/products.ml";;
   6 needs "Library/agm.ml";;
   7 needs "Multivariate/transcendentals.ml";;
   8 needs "Library/pocklington.ml";;
   9 needs "Library/multiplicative.ml";;
  10 needs "Examples/mangoldt.ml";;
  11
  12 prioritize_real();;
  13 prioritize_complex();;
  14
  15 (* ------------------------------------------------------------------------- *)
  16 (* Rearranging a certain kind of double sum.                                 *)
  17 (* ------------------------------------------------------------------------- *)
  18
  19 let VSUM_VSUM_DIVISORS = prove
  20  (`!f x. vsum (1..x) (\n. vsum {d | d divides n} (f n)) =
  21          vsum (1..x) (\n. vsum (1..(x DIV n)) (\k. f (k * n) n))`,
  22   SIMP_TAC[VSUM; FINITE_DIVISORS; LE_1] THEN
  23   SIMP_TAC[VSUM; FINITE_NUMSEG; ITERATE_ITERATE_DIVISORS;
  24            MONOIDAL_VECTOR_ADD]);;
  25
  26 (* ------------------------------------------------------------------------- *)
  27 (* Useful approximation lemmas.                                              *)
  28 (* ------------------------------------------------------------------------- *)
  29
  30 let REAL_EXP_1_LE_4 = prove
  31  (`exp(&1) <= &4`,
  32   ONCE_REWRITE_TAC[ARITH_RULE `&1 = &1 / &2 + &1 / &2`; REAL_EXP_ADD] THEN
  33   REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`; REAL_EXP_ADD] THEN
  34   MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_EXP_POS_LE] THEN
  35   MP_TAC(SPEC `&1 / &2` REAL_EXP_BOUND_LEMMA) THEN REAL_ARITH_TAC);;
  36
  37 let DECREASING_LOG_OVER_N = prove
  38  (`!n. 4 <= n ==> log(&n + &1) / (&n + &1) <= log(&n) / &n`,
  39   REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN REPEAT STRIP_TAC THEN
  40   MP_TAC(ISPECL [`\z. clog z / z`; `\z. (Cx(&1) - clog(z)) / z pow 2`;
  41                  `Cx(&n)`; `Cx(&n + &1)`] COMPLEX_MVT_LINE) THEN
  42   REWRITE_TAC[IN_SEGMENT_CX_GEN] THEN
  43   REWRITE_TAC[REAL_ARITH `~(n + &1 <= x /\ x <= n)`] THEN ANTS_TAC THENL
  44    [X_GEN_TAC `w:complex` THEN STRIP_TAC THEN COMPLEX_DIFF_TAC THEN
  45     SUBGOAL_THEN `&0 < Re w` MP_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  46     ASM_CASES_TAC `w = Cx(&0)` THEN ASM_SIMP_TAC[RE_CX; REAL_LT_REFL] THEN
  47     DISCH_TAC THEN UNDISCH_TAC `~(w = Cx(&0))` THEN CONV_TAC COMPLEX_FIELD;
  48     DISCH_THEN(X_CHOOSE_THEN `z:complex`
  49      (CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
  50     SUBGOAL_THEN `&0 < &n /\ &0 < &n + &1` STRIP_ASSUME_TAC THENL
  51      [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  52     ASM_SIMP_TAC[GSYM CX_LOG; GSYM CX_DIV; RE_CX; GSYM CX_SUB] THEN
  53     MATCH_MP_TAC(REAL_ARITH `&0 <= --x ==> a - b = x ==> a <= b`) THEN
  54     REWRITE_TAC[RE_MUL_CX; GSYM REAL_MUL_LNEG] THEN
  55     MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
  56     SUBGOAL_THEN `?u. z = Cx(u)` (CHOOSE_THEN SUBST_ALL_TAC) THENL
  57      [ASM_MESON_TAC[REAL; real]; ALL_TAC] THEN
  58     RULE_ASSUM_TAC(REWRITE_RULE[IM_CX; RE_CX]) THEN
  59     UNDISCH_THEN `T` (K ALL_TAC) THEN
  60     SUBGOAL_THEN `&0 < u` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  61     ASM_SIMP_TAC[GSYM CX_LOG; GSYM CX_SUB; GSYM CX_POW; GSYM CX_DIV; RE_CX;
  62       real_div; GSYM REAL_MUL_LNEG; REAL_NEG_SUB; GSYM REAL_POW_INV] THEN
  63     MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE] THEN
  64     REWRITE_TAC[REAL_SUB_LE] THEN
  65     GEN_REWRITE_TAC LAND_CONV [GSYM LOG_EXP] THEN
  66     MATCH_MP_TAC LOG_MONO_LE_IMP THEN REWRITE_TAC[REAL_EXP_POS_LT] THEN
  67     MP_TAC REAL_EXP_1_LE_4 THEN ASM_REAL_ARITH_TAC]);;
  68
  69 (* ------------------------------------------------------------------------- *)
  70 (* An ad-hoc fact about complex n'th roots.                                  *)
  71 (* ------------------------------------------------------------------------- *)
  72
  73 let EXISTS_COMPLEX_ROOT_NONTRIVIAL = prove
  74  (`!a n. 2 <= n ==> ?z. z pow n = a /\ ~(z = Cx(&1))`,
  75   REPEAT STRIP_TAC THEN
  76   FIRST_ASSUM(ASSUME_TAC o MATCH_MP(ARITH_RULE `2 <= n ==> ~(n = 0)`)) THEN
  77   ASM_CASES_TAC  `a = Cx(&0)` THENL
  78    [EXISTS_TAC `Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_POW_ZERO] THEN
  79     CONV_TAC COMPLEX_RING;
  80     ALL_TAC] THEN
  81   ASM_CASES_TAC `a = Cx(&1)` THENL
  82    [EXISTS_TAC `cexp(Cx(&2) * Cx pi * ii * Cx(&1 / &n))` THEN
  83     ASM_SIMP_TAC[COMPLEX_ROOT_UNITY_EQ_1; DIVIDES_ONE;
  84                  ARITH_RULE `2 <= n ==> ~(n = 1)`; COMPLEX_ROOT_UNITY];
  85     MATCH_MP_TAC(MESON[]
  86      `(!x. ~Q x ==> ~P x) /\ (?x. P x) ==> (?x. P x /\ Q x)`) THEN
  87     ASM_SIMP_TAC[COMPLEX_POW_ONE] THEN EXISTS_TAC `cexp(clog a / Cx(&n))` THEN
  88     ASM_SIMP_TAC[GSYM CEXP_N; COMPLEX_DIV_LMUL; CX_INJ; REAL_OF_NUM_EQ] THEN
  89     ASM_SIMP_TAC[CEXP_CLOG]]);;
  90
  91 (* ------------------------------------------------------------------------- *)
  92 (* Definition of a Dirichlet character mod d.                                *)
  93 (* ------------------------------------------------------------------------- *)
  94
  95 let dirichlet_character = new_definition
  96  `dirichlet_character d (c:num->complex) <=>
  97         (!n. c(n + d) = c(n)) /\
  98         (!n. c(n) = Cx(&0) <=> ~coprime(n,d)) /\
  99         (!m n. c(m * n) = c(m) * c(n))`;;
 100
 101 let DIRICHLET_CHARACTER_PERIODIC = prove
 102  (`!d c n. dirichlet_character d c ==> c(n + d) = c(n)`,
 103   SIMP_TAC[dirichlet_character]);;
 104
 105 let DIRICHLET_CHARACTER_EQ_0 = prove
 106  (`!d c n. dirichlet_character d c ==> (c(n) = Cx(&0) <=> ~coprime(n,d))`,
 107   SIMP_TAC[dirichlet_character]);;
 108
 109 let DIRICHLET_CHARACTER_MUL = prove
 110  (`!d c m n. dirichlet_character d c ==> c(m * n) = c(m) * c(n)`,
 111   SIMP_TAC[dirichlet_character]);;
 112
 113 let DIRICHLET_CHARACTER_EQ_1 = prove
 114  (`!d c. dirichlet_character d c ==> c(1) = Cx(&1)`,
 115   REPEAT STRIP_TAC THEN
 116   FIRST_ASSUM(MP_TAC o MATCH_MP DIRICHLET_CHARACTER_MUL) THEN
 117   DISCH_THEN(MP_TAC o repeat (SPEC `1`)) THEN CONV_TAC NUM_REDUCE_CONV THEN
 118   REWRITE_TAC[COMPLEX_FIELD `a = a * a <=> a = Cx(&0) \/ a = Cx(&1)`] THEN
 119   ASM_SIMP_TAC[DIRICHLET_CHARACTER_EQ_0] THEN
 120   MESON_TAC[COPRIME_1; COPRIME_SYM]);;
 121
 122 let DIRICHLET_CHARACTER_POW = prove
 123  (`!d c m n. dirichlet_character d c ==> c(m EXP n) = c(m) pow n`,
 124   REPLICATE_TAC 3 GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
 125   DISCH_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[EXP; complex_pow] THENL
 126    [ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_1]; ALL_TAC] THEN
 127   FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP DIRICHLET_CHARACTER_MUL th]) THEN
 128   ASM_REWRITE_TAC[]);;
 129
 130 let DIRICHLET_CHARACTER_PERIODIC_GEN = prove
 131  (`!d c m n. dirichlet_character d c ==> c(m * d + n) = c(n)`,
 132   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
 133   REPEAT GEN_TAC THEN DISCH_TAC THEN
 134   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
 135   GEN_TAC THEN
 136   FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [GSYM th]) THEN
 137   ONCE_REWRITE_TAC[ARITH_RULE `(mk + d) + n:num = (mk + n) + d`] THEN
 138   ASM_SIMP_TAC[DIRICHLET_CHARACTER_PERIODIC]);;
 139
 140 let DIRICHLET_CHARACTER_CONG = prove
 141  (`!d c m n.
 142         dirichlet_character d c /\ (m == n) (mod d) ==> c(m) = c(n)`,
 143   REWRITE_TAC[CONG_CASES] THEN REPEAT STRIP_TAC THEN
 144   ASM_SIMP_TAC[DIRICHLET_CHARACTER_PERIODIC_GEN]);;
 145
 146 let DIRICHLET_CHARACTER_ROOT = prove
 147  (`!d c n. dirichlet_character d c /\ coprime(d,n)
 148            ==> c(n) pow phi(d) = Cx(&1)`,
 149   REPEAT STRIP_TAC THEN
 150   FIRST_ASSUM(SUBST1_TAC o GSYM o MATCH_MP DIRICHLET_CHARACTER_EQ_1) THEN
 151   FIRST_ASSUM(fun th ->
 152     REWRITE_TAC[GSYM(MATCH_MP DIRICHLET_CHARACTER_POW th)]) THEN
 153   MATCH_MP_TAC DIRICHLET_CHARACTER_CONG THEN
 154   EXISTS_TAC `d:num` THEN ASM_REWRITE_TAC[] THEN
 155   MATCH_MP_TAC FERMAT_LITTLE THEN ASM_MESON_TAC[COPRIME_SYM]);;
 156
 157 let DIRICHLET_CHARACTER_NORM = prove
 158  (`!d c n. dirichlet_character d c
 159            ==> norm(c n) = if coprime(d,n) then &1 else &0`,
 160   REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
 161    [ALL_TAC;
 162     REWRITE_TAC[COMPLEX_NORM_ZERO] THEN
 163     ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_0; COPRIME_SYM]] THEN
 164   ASM_CASES_TAC `d = 0` THENL
 165    [ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_1; COMPLEX_NORM_CX; REAL_ABS_NUM;
 166                   COPRIME_0; COPRIME_SYM];
 167     ALL_TAC] THEN
 168   MP_TAC(SPECL [`d:num`; `c:num->complex`; `n:num`]
 169     DIRICHLET_CHARACTER_ROOT) THEN ASM_REWRITE_TAC[] THEN
 170   DISCH_THEN(MP_TAC o AP_TERM `norm:complex->real`) THEN
 171   REWRITE_TAC[COMPLEX_NORM_POW; COMPLEX_NORM_CX; REAL_ABS_NUM] THEN
 172   DISCH_TAC THEN
 173   MP_TAC(SPECL [`norm((c:num->complex) n)`; `phi d`] REAL_POW_EQ_1_IMP) THEN
 174   ASM_REWRITE_TAC[REAL_ABS_NORM] THEN
 175   ASM_MESON_TAC[PHI_LOWERBOUND_1_STRONG; LE_1]);;
 176
 177 (* ------------------------------------------------------------------------- *)
 178 (* The principal character mod d.                                            *)
 179 (* ------------------------------------------------------------------------- *)
 180
 181 let chi_0 = new_definition
 182  `chi_0 d n = if coprime(n,d) then Cx(&1) else Cx(&0)`;;
 183
 184 let DIRICHLET_CHARACTER_CHI_0 = prove
 185  (`dirichlet_character d (chi_0 d)`,
 186   REWRITE_TAC[dirichlet_character; chi_0] THEN
 187   REWRITE_TAC[NUMBER_RULE `coprime(n + d,d) <=> coprime(n,d)`;
 188           NUMBER_RULE `coprime(m * n,d) <=> coprime(m,d) /\ coprime(n,d)`] THEN
 189   CONV_TAC COMPLEX_RING);;
 190
 191 let DIRICHLET_CHARACTER_EQ_PRINCIPAL = prove
 192  (`!d c. dirichlet_character d c
 193          ==> (c = chi_0 d <=> !n. coprime(n,d) ==> c(n) = Cx(&1))`,
 194   REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM; chi_0] THEN
 195   ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_0]);;
 196
 197 let DIRICHLET_CHARACTER_NONPRINCIPAL = prove
 198  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
 199          ==> ?n. coprime(n,d) /\ ~(c n = Cx(&0)) /\ ~(c n = Cx(&1))`,
 200   MESON_TAC[DIRICHLET_CHARACTER_EQ_PRINCIPAL; DIRICHLET_CHARACTER_EQ_0]);;
 201
 202 let DIRICHLET_CHARACTER_0 = prove
 203  (`!c. dirichlet_character 0 c <=> c = chi_0 0`,
 204   GEN_TAC THEN EQ_TAC THEN SIMP_TAC[DIRICHLET_CHARACTER_CHI_0] THEN
 205   DISCH_TAC THEN REWRITE_TAC[chi_0; FUN_EQ_THM; COPRIME_0] THEN
 206   X_GEN_TAC `n:num` THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 207   ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_1; DIRICHLET_CHARACTER_EQ_0;
 208                 COPRIME_0]);;
 209
 210 let DIRICHLET_CHARACTER_1 = prove
 211  (`!c. dirichlet_character 1 c <=> !n. c n = Cx(&1)`,
 212   GEN_TAC THEN REWRITE_TAC[dirichlet_character; COPRIME_1] THEN EQ_TAC THENL
 213    [STRIP_TAC THEN
 214     FIRST_X_ASSUM(MP_TAC o SPECL [`1`; `1`]) THEN
 215     ASM_REWRITE_TAC[ARITH; COMPLEX_RING
 216      `x = x * x <=> x = Cx(&0) \/ x = Cx(&1)`] THEN
 217     DISCH_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD1] THEN
 218     REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `0`)) THEN ASM_REWRITE_TAC[ARITH] THEN
 219     CONV_TAC COMPLEX_RING;
 220     DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC COMPLEX_RING]);;
 221
 222 let DIRICHLET_CHARACTER_NONPRINCIPAL_NONTRIVIAL = prove
 223  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
 224          ==> ~(d = 0) /\ ~(d = 1)`,
 225   REPEAT GEN_TAC THEN ASM_CASES_TAC `d = 0` THEN
 226   ASM_REWRITE_TAC[DIRICHLET_CHARACTER_0; TAUT `~(p /\ ~p)`] THEN
 227   ASM_CASES_TAC `d = 1` THEN
 228   ASM_REWRITE_TAC[DIRICHLET_CHARACTER_1; chi_0; FUN_EQ_THM; COPRIME_1] THEN
 229   CONV_TAC TAUT);;
 230
 231 let DIRICHLET_CHARACTER_ZEROSUM = prove
 232  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
 233          ==> vsum(1..d) c = Cx(&0)`,
 234   REPEAT GEN_TAC THEN DISCH_TAC THEN
 235   FIRST_ASSUM(STRIP_ASSUME_TAC o
 236     MATCH_MP DIRICHLET_CHARACTER_NONPRINCIPAL_NONTRIVIAL) THEN
 237   FIRST_ASSUM(MP_TAC o MATCH_MP DIRICHLET_CHARACTER_NONPRINCIPAL) THEN
 238   DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
 239   MATCH_MP_TAC(COMPLEX_RING
 240    `!x. x * c = c /\ ~(x = Cx(&1)) ==> c = Cx(&0)`) THEN
 241   EXISTS_TAC `(c:num->complex) m` THEN
 242   ASM_SIMP_TAC[GSYM VSUM_COMPLEX_LMUL; FINITE_NUMSEG] THEN
 243   MATCH_MP_TAC(MESON[]
 244    `!t. vsum t f = vsum s f /\ vsum t g = vsum s g /\ vsum t f = vsum t g
 245         ==> vsum s f = vsum s g`) THEN
 246   EXISTS_TAC `{n | coprime(n,d) /\ n < d}` THEN
 247   REPEAT(CONJ_TAC THENL
 248    [CONV_TAC SYM_CONV THEN MATCH_MP_TAC VSUM_SUPERSET THEN
 249     SIMP_TAC[SUBSET; IN_NUMSEG; LT_IMP_LE; IN_ELIM_THM] THEN CONJ_TAC THEN
 250     X_GEN_TAC `r:num` THENL
 251      [ASM_CASES_TAC `r = 0` THENL [ALL_TAC; ASM_ARITH_TAC] THEN
 252       ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[COPRIME_0];
 253       ASM_CASES_TAC `coprime(r,d)` THEN ASM_REWRITE_TAC[] THENL
 254        [ASM_CASES_TAC `r:num = d` THEN ASM_REWRITE_TAC[LT_REFL] THENL
 255          [ASM_MESON_TAC[COPRIME_REFL]; ASM_ARITH_TAC];
 256         REWRITE_TAC[COMPLEX_VEC_0] THEN
 257         ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_0; COMPLEX_MUL_RZERO]]];
 258     ALL_TAC]) THEN
 259   FIRST_ASSUM(fun th ->
 260     REWRITE_TAC[GSYM(MATCH_MP DIRICHLET_CHARACTER_MUL (CONJUNCT1 th))]) THEN
 261   SIMP_TAC[VSUM; PHI_FINITE_LEMMA] THEN
 262   MATCH_MP_TAC ITERATE_OVER_COPRIME THEN SIMP_TAC[MONOIDAL_VECTOR_ADD] THEN
 263   ASM_MESON_TAC[DIRICHLET_CHARACTER_CONG]);;
 264
 265 let DIRICHLET_CHARACTER_ZEROSUM_MUL = prove
 266  (`!d c n. dirichlet_character d c /\ ~(c = chi_0 d)
 267            ==> vsum(1..d*n) c = Cx(&0)`,
 268   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
 269   INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; VSUM_CLAUSES_NUMSEG] THEN
 270   REWRITE_TAC[ARITH; COMPLEX_VEC_0] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
 271   ASM_SIMP_TAC[VSUM_ADD_SPLIT; ARITH_RULE `1 <= n + 1`; COMPLEX_ADD_LID] THEN
 272   ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[VSUM_OFFSET] THEN
 273   FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP DIRICHLET_CHARACTER_ZEROSUM) THEN
 274   MATCH_MP_TAC VSUM_EQ THEN REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN
 275   MATCH_MP_TAC DIRICHLET_CHARACTER_CONG THEN EXISTS_TAC `d:num` THEN
 276   ASM_REWRITE_TAC[] THEN NUMBER_TAC);;
 277
 278 let DIRICHLET_CHARACTER_SUM_MOD = prove
 279  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
 280          ==> vsum(1..n) c = vsum(1..(n MOD d)) c`,
 281   REPEAT GEN_TAC THEN DISCH_TAC THEN
 282   FIRST_ASSUM(STRIP_ASSUME_TAC o MATCH_MP
 283     DIRICHLET_CHARACTER_NONPRINCIPAL_NONTRIVIAL) THEN
 284   FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP DIVISION) THEN
 285   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 286   DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
 287   SIMP_TAC[VSUM_ADD_SPLIT; ARITH_RULE `1 <= n + 1`] THEN
 288   ONCE_REWRITE_TAC[MULT_SYM] THEN
 289   ASM_SIMP_TAC[DIRICHLET_CHARACTER_ZEROSUM_MUL; COMPLEX_ADD_LID] THEN
 290   ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[VSUM_OFFSET] THEN
 291   FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP DIRICHLET_CHARACTER_ZEROSUM) THEN
 292   MATCH_MP_TAC VSUM_EQ THEN REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN
 293   MATCH_MP_TAC DIRICHLET_CHARACTER_CONG THEN EXISTS_TAC `d:num` THEN
 294   ASM_REWRITE_TAC[] THEN CONV_TAC NUMBER_RULE);;
 295
 296 (* ------------------------------------------------------------------------- *)
 297 (* Finiteness of the set of characters (later we could get size =  phi(d)).  *)
 298 (* ------------------------------------------------------------------------- *)
 299
 300 let FINITE_DIRICHLET_CHARACTERS = prove
 301  (`!d. FINITE {c | dirichlet_character d c}`,
 302   GEN_TAC THEN ASM_CASES_TAC `d = 0` THENL
 303    [ASM_SIMP_TAC[DIRICHLET_CHARACTER_0; SET_RULE `{x | x = a} = {a}`] THEN
 304     SIMP_TAC[FINITE_RULES];
 305     ALL_TAC] THEN
 306   MATCH_MP_TAC FINITE_SUBSET THEN
 307   EXISTS_TAC `IMAGE (\c n. c(n MOD d))
 308                     {c | (!m. m IN {m | m < d}
 309                              ==> c(m) IN (Cx(&0) INSERT
 310                                           {z | z pow (phi d) = Cx(&1)})) /\
 311                          (!m. ~(m IN {m | m < d})
 312                               ==> c(m) = Cx(&0))}` THEN
 313   CONJ_TAC THENL
 314    [MATCH_MP_TAC FINITE_IMAGE THEN MATCH_MP_TAC FINITE_FUNSPACE THEN
 315     ASM_SIMP_TAC[FINITE_NUMSEG_LT; FINITE_INSERT] THEN
 316     MATCH_MP_TAC FINITE_COMPLEX_ROOTS_UNITY THEN
 317     ASM_SIMP_TAC[PHI_LOWERBOUND_1_STRONG; LE_1];
 318     ALL_TAC] THEN
 319   REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN X_GEN_TAC `c:num->complex` THEN
 320   DISCH_TAC THEN REWRITE_TAC[IN_IMAGE; IN_ELIM_THM; IN_INSERT] THEN
 321   EXISTS_TAC `\n:num. if n < d then c(n) else Cx(&0)` THEN
 322   ASM_SIMP_TAC[DIVISION; FUN_EQ_THM] THEN CONJ_TAC THEN X_GEN_TAC `m:num` THENL
 323    [MATCH_MP_TAC DIRICHLET_CHARACTER_CONG THEN EXISTS_TAC `d:num` THEN
 324     ASM_MESON_TAC[CONG_MOD; CONG_SYM];
 325     ASM_MESON_TAC[DIRICHLET_CHARACTER_ROOT; COPRIME_SYM;
 326                   DIRICHLET_CHARACTER_EQ_0]]);;
 327
 328 (* ------------------------------------------------------------------------- *)
 329 (* Very basic group structure.                                               *)
 330 (* ------------------------------------------------------------------------- *)
 331
 332 let DIRICHLET_CHARACTER_MUL_CNJ = prove
 333  (`!d c n. dirichlet_character d c /\ ~(c n = Cx(&0))
 334            ==> cnj(c n) * c n = Cx(&1) /\ c n * cnj(c n) = Cx(&1)`,
 335   REPEAT GEN_TAC THEN STRIP_TAC THEN
 336   MATCH_MP_TAC(COMPLEX_FIELD
 337    `inv z = w /\ ~(z = Cx(&0)) ==> w * z = Cx(&1) /\ z * w = Cx(&1)`) THEN
 338   ASM_REWRITE_TAC[COMPLEX_INV_CNJ] THEN
 339   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM COMPLEX_NORM_NZ]) THEN
 340   FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP DIRICHLET_CHARACTER_NORM th]) THEN
 341   COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_LT_REFL; COMPLEX_POW_ONE] THEN
 342   REWRITE_TAC[COMPLEX_DIV_1]);;
 343
 344 let DIRICHLET_CHARACTER_CNJ = prove
 345  (`!d c. dirichlet_character d c ==> dirichlet_character d (\n. cnj(c n))`,
 346   SIMP_TAC[dirichlet_character; CNJ_MUL; CNJ_EQ_CX]);;
 347
 348 let DIRICHLET_CHARACTER_GROUPMUL = prove
 349  (`!d c1 c2. dirichlet_character d c1 /\ dirichlet_character d c2
 350              ==> dirichlet_character d (\n. c1(n) * c2(n))`,
 351   SIMP_TAC[dirichlet_character; COMPLEX_ENTIRE] THEN
 352   REWRITE_TAC[COMPLEX_MUL_AC]);;
 353
 354 let DIRICHLET_CHARACTER_GROUPINV = prove
 355  (`!d c. dirichlet_character d c ==> (\n. cnj(c n) * c n) = chi_0 d`,
 356   REPEAT STRIP_TAC THEN REWRITE_TAC[chi_0; FUN_EQ_THM] THEN
 357   REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
 358    [ASM_MESON_TAC[DIRICHLET_CHARACTER_MUL_CNJ; DIRICHLET_CHARACTER_EQ_0];
 359     ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_0; COMPLEX_MUL_RZERO]]);;
 360
 361 (* ------------------------------------------------------------------------- *)
 362 (* Orthogonality relations, a weak version of one first.                     *)
 363 (* ------------------------------------------------------------------------- *)
 364
 365 let DIRICHLET_CHARACTER_SUM_OVER_NUMBERS = prove
 366  (`!d c. dirichlet_character d c
 367          ==> vsum (1..d) c = if c = chi_0 d then Cx(&(phi d)) else Cx(&0)`,
 368   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
 369   ASM_SIMP_TAC[DIRICHLET_CHARACTER_ZEROSUM] THEN
 370   FIRST_X_ASSUM SUBST1_TAC THEN POP_ASSUM(K ALL_TAC) THEN
 371   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
 372   REWRITE_TAC[chi_0] THEN
 373   SIMP_TAC[GSYM VSUM_RESTRICT_SET; FINITE_NUMSEG; GSYM COMPLEX_VEC_0] THEN
 374   SIMP_TAC[phi; VSUM_CONST; FINITE_RESTRICT; FINITE_NUMSEG] THEN
 375   REWRITE_TAC[COMPLEX_CMUL; COMPLEX_MUL_RID] THEN
 376   AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
 377   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_NUMSEG] THEN
 378   X_GEN_TAC `x:num` THEN ASM_CASES_TAC `coprime(x,d)` THEN
 379   ASM_REWRITE_TAC[] THEN ARITH_TAC);;
 380
 381 let DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_WEAK = prove
 382  (`!d n. vsum {c | dirichlet_character d c} (\x. x n) = Cx(&0) \/
 383          coprime(n,d) /\ !c. dirichlet_character d c ==> c(n) = Cx(&1)`,
 384   REPEAT GEN_TAC THEN ASM_CASES_TAC `coprime(n,d)` THENL
 385    [ALL_TAC;
 386     DISJ1_TAC THEN REWRITE_TAC[GSYM COMPLEX_VEC_0] THEN
 387     MATCH_MP_TAC VSUM_EQ_0 THEN
 388     ASM_SIMP_TAC[IN_ELIM_THM; COMPLEX_VEC_0; DIRICHLET_CHARACTER_EQ_0]] THEN
 389   SUBGOAL_THEN
 390     `!c'. dirichlet_character d c'
 391           ==> vsum {c | dirichlet_character d c}
 392                    ((\c. c(n)) o (\c n. c'(n) * c(n))) =
 393               vsum {c | dirichlet_character d c} (\c. c(n))`
 394   MP_TAC THENL
 395    [ALL_TAC;
 396     SIMP_TAC[o_DEF; FINITE_DIRICHLET_CHARACTERS; VSUM_COMPLEX_LMUL] THEN
 397     REWRITE_TAC[COMPLEX_RING `a * x = x <=> a = Cx(&1) \/ x = Cx(&0)`] THEN
 398     ASM_MESON_TAC[]] THEN
 399   REPEAT STRIP_TAC THEN MATCH_MP_TAC VSUM_INJECTION THEN
 400   REWRITE_TAC[FINITE_DIRICHLET_CHARACTERS; IN_ELIM_THM] THEN
 401   ASM_SIMP_TAC[DIRICHLET_CHARACTER_GROUPMUL] THEN
 402   REPEAT STRIP_TAC THEN
 403   FIRST_X_ASSUM(MP_TAC o AP_TERM `(\c n. cnj(c'(n:num)) * c n)`) THEN
 404   REWRITE_TAC[FUN_EQ_THM] THEN DISCH_TAC THEN X_GEN_TAC `m:num` THEN
 405   ASM_CASES_TAC `coprime(m,d)` THENL
 406    [ALL_TAC; ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_0]] THEN
 407   FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
 408   MATCH_MP_TAC(COMPLEX_RING
 409     `a * b = Cx(&1) ==> a * b * x = a * b * y ==> x = y`) THEN
 410   ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_0; DIRICHLET_CHARACTER_MUL_CNJ]);;
 411
 412 let DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_POS = prove
 413  (`!d n. real(vsum {c | dirichlet_character d c} (\c. c n)) /\
 414          &0 <= Re(vsum {c | dirichlet_character d c} (\c. c n))`,
 415   MP_TAC DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_WEAK THEN
 416   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 417   STRIP_TAC THEN ASM_REWRITE_TAC[REAL_CX; RE_CX; REAL_LE_REFL] THEN
 418   CONJ_TAC THENL
 419    [MATCH_MP_TAC REAL_VSUM;
 420     SIMP_TAC[FINITE_DIRICHLET_CHARACTERS; RE_VSUM] THEN
 421     MATCH_MP_TAC SUM_POS_LE] THEN
 422   ASM_SIMP_TAC[FINITE_DIRICHLET_CHARACTERS; IN_ELIM_THM; REAL_CX; RE_CX] THEN
 423   REWRITE_TAC[REAL_POS]);;
 424
 425 (* ------------------------------------------------------------------------- *)
 426 (* A somewhat gruesome lemma about extending a character from a subgroup.    *)
 427 (* ------------------------------------------------------------------------- *)
 428
 429 let CHARACTER_EXTEND_FROM_SUBGROUP = prove
 430  (`!f h a d.
 431         h SUBSET {x | x < d /\ coprime(x,d)} /\
 432         (1 IN h) /\
 433         (!x y. x IN h /\ y IN h ==> ((x * y) MOD d) IN h) /\
 434         (!x. x IN h ==> ?y. y IN h /\ (x * y == 1) (mod d)) /\
 435         (!x. x IN h ==> ~(f x = Cx(&0))) /\
 436         (!x y. x IN h /\ y IN h
 437                  ==> f((x * y) MOD d) = f(x) * f(y)) /\
 438         a IN {x | x < d /\ coprime(x,d)} DIFF h
 439         ==> ?f' h'. (a INSERT h) SUBSET h' /\
 440                     h' SUBSET {x | x < d /\ coprime(x,d)} /\
 441                     (!x. x IN h ==> f'(x) = f(x)) /\
 442                     ~(f' a = Cx(&1)) /\
 443                     1 IN h' /\
 444                     (!x y. x IN h' /\ y IN h' ==> ((x * y) MOD d) IN h') /\
 445                     (!x. x IN h' ==> ?y. y IN h' /\ (x * y == 1) (mod d)) /\
 446                     (!x. x IN h' ==> ~(f' x = Cx(&0))) /\
 447                     (!x y. x IN h' /\ y IN h'
 448                            ==> f'((x * y) MOD d) = f'(x) * f'(y))`,
 449   REWRITE_TAC[IN_ELIM_THM; IN_DIFF; SUBSET] THEN REPEAT STRIP_TAC THEN
 450   SUBGOAL_THEN `1 < d` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 451   FIRST_ASSUM(ASSUME_TAC o MATCH_MP LT_IMP_LE) THEN
 452   SUBGOAL_THEN `?m x. 0 < m /\ x IN h /\ (a EXP m == x) (mod d)` MP_TAC THENL
 453    [MAP_EVERY EXISTS_TAC [`phi d`; `1`] THEN ASM_REWRITE_TAC[] THEN
 454     CONJ_TAC THENL [ASM_MESON_TAC[PHI_LOWERBOUND_1_STRONG; LE_1]; ALL_TAC] THEN
 455     MATCH_MP_TAC FERMAT_LITTLE THEN ASM SET_TAC[];
 456     ALL_TAC] THEN
 457   SUBGOAL_THEN `!x s. x IN h ==> ((x EXP s) MOD d) IN h` ASSUME_TAC THENL
 458    [REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
 459     INDUCT_TAC THEN ASM_SIMP_TAC[EXP; MOD_LT] THEN
 460     SUBGOAL_THEN `((x * (x EXP s) MOD d) MOD d) IN h` MP_TAC THEN
 461     ASM_MESON_TAC[MOD_MULT_RMOD; ASSUME `1 <= d`; LE_1];
 462     ALL_TAC] THEN
 463   GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
 464   DISCH_THEN(X_CHOOSE_THEN `m:num` MP_TAC) THEN
 465   DISCH_THEN(CONJUNCTS_THEN2
 466    (X_CHOOSE_THEN `am:num` STRIP_ASSUME_TAC) MP_TAC) THEN
 467   FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
 468    `0 < m ==> m = 1 \/ 2 <= m`))
 469   THENL
 470    [FIRST_X_ASSUM SUBST_ALL_TAC THEN UNDISCH_TAC `(a EXP 1 == am) (mod d)` THEN
 471     ASM_SIMP_TAC[EXP_1; GSYM CONG_MOD_LT; MOD_LT] THEN ASM_MESON_TAC[];
 472     ALL_TAC] THEN
 473   DISCH_THEN(MP_TAC o GEN `r:num` o SPEC `r MOD m`) THEN
 474   ASM_SIMP_TAC[DIVISION; LE_1; NOT_EXISTS_THM] THEN
 475   REWRITE_TAC[TAUT `~(a /\ b /\ c) <=> b /\ c ==> ~a`] THEN DISCH_TAC THEN
 476   SUBGOAL_THEN `!r x. x IN h /\ (a EXP r == x) (mod d) ==> m divides r`
 477   ASSUME_TAC THENL
 478    [REPEAT STRIP_TAC THEN ASM_SIMP_TAC[DIVIDES_MOD; LE_1] THEN
 479     REWRITE_TAC[ARITH_RULE `n = 0 <=> ~(0 < n)`] THEN
 480     FIRST_X_ASSUM MATCH_MP_TAC THEN
 481     EXISTS_TAC `(a EXP (r MOD m)) MOD d` THEN
 482     ASM_SIMP_TAC[CONG_RMOD; LE_1; CONG_REFL] THEN
 483     UNDISCH_TAC `!x. x IN h ==> (?y. y IN h /\ (x * y == 1) (mod d))` THEN
 484     DISCH_THEN(MP_TAC o SPEC `(a EXP (m * r DIV m)) MOD d`) THEN ANTS_TAC THENL
 485      [REWRITE_TAC[GSYM EXP_EXP] THEN
 486       SUBGOAL_THEN
 487        `(a EXP m) EXP (r DIV m) MOD d = (am EXP (r DIV m)) MOD d`
 488        (fun th -> ASM_SIMP_TAC[th]) THEN
 489       ASM_SIMP_TAC[GSYM CONG; LE_1] THEN
 490       ASM_SIMP_TAC[CONG_LMOD; CONG_EXP; LE_1];
 491       ALL_TAC] THEN
 492     DISCH_THEN(X_CHOOSE_THEN `y:num` STRIP_ASSUME_TAC) THEN
 493     UNDISCH_TAC `(a EXP r == x) (mod d)` THEN
 494     MP_TAC(SPECL [`r:num`; `m:num`] DIVISION) THEN ASM_SIMP_TAC[LE_1] THEN
 495     DISCH_THEN(fun th ->
 496       GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
 497     ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[EXP_ADD] THEN
 498     DISCH_THEN(MP_TAC o SPEC `y:num` o MATCH_MP
 499     (NUMBER_RULE `!a. (x:num == y) (mod n) ==> (a * x == a * y) (mod n)`)) THEN
 500     DISCH_THEN(MP_TAC o MATCH_MP (NUMBER_RULE
 501      `(y * e * a == z) (mod n)
 502       ==> (e * y == 1) (mod n) ==> (a == z) (mod n)`)) THEN
 503     ANTS_TAC THENL
 504      [MATCH_MP_TAC CONG_TRANS THEN
 505       EXISTS_TAC `a EXP (m * r DIV m) MOD d * y` THEN
 506       ASM_SIMP_TAC[CONG_MULT; CONG_REFL; CONG_RMOD; LE_1];
 507       ALL_TAC] THEN
 508     ASM_SIMP_TAC[CONG; LE_1];
 509     ALL_TAC] THEN
 510   MP_TAC(SPECL [`(f:num->complex) am`; `m:num`]
 511                EXISTS_COMPLEX_ROOT_NONTRIVIAL) THEN ASM_SIMP_TAC[] THEN
 512   DISCH_THEN(X_CHOOSE_THEN `z:complex` STRIP_ASSUME_TAC) THEN
 513   SUBGOAL_THEN
 514    `?g. !x k. x IN h ==> g((x * a EXP k) MOD d) = f(x) * z pow k`
 515   MP_TAC THENL
 516    [REWRITE_TAC[MESON[] `(?g. !x a. p x ==> g(f a x) = h a x) <=>
 517                          (?g. !y x a. p x /\ f a x = y ==> g y = h a x)`] THEN
 518     REWRITE_TAC[GSYM SKOLEM_THM] THEN
 519     REWRITE_TAC[MESON[]
 520      `(!y. ?z. !x k. p x /\ f x k = y ==> z = g x k) <=>
 521       (!x k x' k'. p x /\ p x' /\ f x k = f x' k' ==> g x k = g x' k')`] THEN
 522     ONCE_REWRITE_TAC[MESON[]
 523      `(!x k y j. P x k y j) <=> (!k j x y. P x k y j)`] THEN
 524     MATCH_MP_TAC WLOG_LE THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
 525     MAP_EVERY X_GEN_TAC [`k:num`; `j:num`] THEN DISCH_TAC THEN
 526     MAP_EVERY X_GEN_TAC [`x:num`; `y:num`] THEN
 527     ASM_SIMP_TAC[GSYM CONG; LE_1] THEN STRIP_TAC THEN
 528     UNDISCH_TAC `k:num <= j` THEN REWRITE_TAC[LE_EXISTS] THEN
 529     DISCH_THEN(X_CHOOSE_THEN `i:num` SUBST_ALL_TAC) THEN
 530     ONCE_REWRITE_TAC[ADD_SYM] THEN
 531     REWRITE_TAC[COMPLEX_POW_ADD; COMPLEX_MUL_ASSOC] THEN
 532     AP_THM_TAC THEN AP_TERM_TAC THEN
 533     SUBGOAL_THEN `m divides i` MP_TAC THENL
 534      [FIRST_X_ASSUM MATCH_MP_TAC THEN
 535       UNDISCH_TAC `!x. x IN h ==> (?y. y IN h /\ (x * y == 1) (mod d))` THEN
 536       DISCH_THEN(MP_TAC o SPEC `y:num`) THEN ASM_REWRITE_TAC[] THEN
 537       DISCH_THEN(X_CHOOSE_THEN `z:num` STRIP_ASSUME_TAC) THEN
 538       EXISTS_TAC `(z * x) MOD d` THEN ASM_SIMP_TAC[CONG_RMOD; LE_1] THEN
 539       MATCH_MP_TAC CONG_MULT_LCANCEL THEN EXISTS_TAC `y * a EXP k` THEN
 540       REWRITE_TAC[COPRIME_LMUL] THEN
 541       CONJ_TAC THENL [ASM_MESON_TAC[COPRIME_EXP; COPRIME_SYM]; ALL_TAC] THEN
 542       UNDISCH_TAC `(x * a EXP k == y * a EXP (k + i)) (mod d)` THEN
 543       REWRITE_TAC[EXP_ADD] THEN UNDISCH_TAC `(y * z == 1) (mod d)` THEN
 544       CONV_TAC NUMBER_RULE;
 545       ALL_TAC] THEN
 546     REWRITE_TAC[divides] THEN
 547     DISCH_THEN(X_CHOOSE_THEN `r:num` SUBST_ALL_TAC) THEN
 548     ASM_REWRITE_TAC[GSYM COMPLEX_POW_POW] THEN MATCH_MP_TAC EQ_TRANS THEN
 549     EXISTS_TAC `f((y * (am EXP r) MOD d) MOD d):complex` THEN CONJ_TAC THENL
 550      [AP_TERM_TAC THEN CONV_TAC SYM_CONV THEN ASM_SIMP_TAC[CONG_MOD_LT] THEN
 551       MATCH_MP_TAC CONG_TRANS THEN
 552       EXISTS_TAC `y * (a EXP m) EXP r` THEN CONJ_TAC THENL
 553        [MATCH_MP_TAC CONG_MULT THEN
 554         ASM_SIMP_TAC[CONG_MULT; CONG_LMOD; CONG_REFL; LE_1] THEN
 555         MATCH_MP_TAC CONG_EXP THEN ASM_MESON_TAC[CONG_SYM];
 556         ALL_TAC] THEN
 557       MATCH_MP_TAC CONG_MULT_LCANCEL THEN EXISTS_TAC `a EXP k` THEN
 558       CONJ_TAC THENL [ASM_MESON_TAC[COPRIME_EXP; COPRIME_SYM]; ALL_TAC] THEN
 559       UNDISCH_TAC `(x * a EXP k == y * a EXP (k + m * r)) (mod d)` THEN
 560       REWRITE_TAC[EXP_ADD; EXP_EXP] THEN CONV_TAC NUMBER_RULE;
 561       ALL_TAC] THEN
 562     ASM_SIMP_TAC[] THEN AP_TERM_TAC THEN
 563     SPEC_TAC(`r:num`,`s:num`) THEN INDUCT_TAC THEN
 564     ASM_SIMP_TAC[EXP; MOD_LT; complex_pow; COMPLEX_MUL_RID] THENL
 565      [UNDISCH_TAC
 566        `!x y. x IN h /\ y IN h ==> f ((x * y) MOD d):complex = f x * f y` THEN
 567       DISCH_THEN(MP_TAC o SPECL [`1`; `1`]) THEN
 568       ASM_SIMP_TAC[MULT_CLAUSES; MOD_LT] THEN
 569       UNDISCH_TAC `!x:num. x IN h ==> ~(f x = Cx (&0))` THEN
 570       DISCH_THEN(MP_TAC o SPEC `1`) THEN ASM_REWRITE_TAC[] THEN
 571       CONV_TAC COMPLEX_RING;
 572       ALL_TAC] THEN
 573     MATCH_MP_TAC EQ_TRANS THEN
 574     EXISTS_TAC `f((am * (am EXP s) MOD d) MOD d):complex` THEN CONJ_TAC THENL
 575      [ALL_TAC; ASM_SIMP_TAC[]] THEN
 576     AP_TERM_TAC THEN ASM_SIMP_TAC[MOD_MULT_RMOD; ASSUME `1 <= d`; LE_1];
 577     ALL_TAC] THEN
 578   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `g:num->complex` THEN
 579   DISCH_THEN (LABEL_TAC "*") THEN
 580   EXISTS_TAC `{(x * a EXP k) MOD d | x IN h /\ k IN (:num)}` THEN
 581   REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
 582    [REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INSERT; IN_UNIV] THEN
 583     X_GEN_TAC `x:num` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
 584      [MAP_EVERY EXISTS_TAC [`1`; `1`];
 585       MAP_EVERY EXISTS_TAC [`x:num`; `0`]] THEN
 586     ASM_SIMP_TAC[EXP_1; MULT_CLAUSES; EXP; MOD_LT];
 587     REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
 588     MAP_EVERY X_GEN_TAC [`y:num`; `x:num`; `k:num`] THEN
 589     STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
 590     ASM_SIMP_TAC[DIVISION; LE_1; COPRIME_MOD; COPRIME_LMUL] THEN
 591     ASM_MESON_TAC[COPRIME_EXP; COPRIME_SYM];
 592     X_GEN_TAC `x:num` THEN DISCH_TAC THEN
 593     REMOVE_THEN "*" (MP_TAC o SPECL [`x:num`; `0`]) THEN
 594     ASM_SIMP_TAC[MOD_LT; EXP; MULT_CLAUSES; complex_pow; COMPLEX_MUL_RID];
 595     REMOVE_THEN "*" (MP_TAC o SPECL [`1`; `1`]) THEN
 596     ASM_SIMP_TAC[EXP_1; MULT_CLAUSES; MOD_LT; COMPLEX_POW_1] THEN
 597     UNDISCH_TAC `!x y. x IN h /\ y IN h ==> f ((x * y) MOD d) = f x * f y` THEN
 598     DISCH_THEN(MP_TAC o SPECL [`1`; `1`]) THEN
 599     ASM_SIMP_TAC[MULT_CLAUSES; MOD_LT] THEN
 600     UNDISCH_TAC `~(z = Cx(&1))` THEN CONV_TAC COMPLEX_RING;
 601     REWRITE_TAC[IN_ELIM_THM; IN_UNIV] THEN
 602     MAP_EVERY EXISTS_TAC [`1`; `0`] THEN
 603     ASM_SIMP_TAC[EXP; MULT_CLAUSES; MOD_LT];
 604     REWRITE_TAC[IN_ELIM_THM; IN_UNIV; LEFT_AND_EXISTS_THM] THEN
 605     REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 606     MAP_EVERY X_GEN_TAC
 607      [`r:num`; `s:num`; `x:num`; `k:num`; `y:num`; `j:num`] THEN
 608     STRIP_TAC THEN REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN
 609     MAP_EVERY EXISTS_TAC [`(x * y) MOD d`; `j + k:num`] THEN
 610     ASM_SIMP_TAC[MOD_MULT_LMOD; MOD_MULT_RMOD; LE_1] THEN
 611     REWRITE_TAC[EXP_ADD; MULT_AC];
 612     REWRITE_TAC[IN_ELIM_THM; IN_UNIV; LEFT_IMP_EXISTS_THM] THEN
 613     MAP_EVERY X_GEN_TAC [`y:num`; `x:num`; `k:num`] THEN
 614     STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
 615     UNDISCH_TAC `!x. x IN h ==> (?y. y IN h /\ (x * y == 1) (mod d))` THEN
 616     DISCH_THEN(MP_TAC o SPEC `x:num`) THEN ASM_REWRITE_TAC[] THEN
 617     DISCH_THEN(X_CHOOSE_THEN `z:num` STRIP_ASSUME_TAC) THEN
 618     EXISTS_TAC `(z * a EXP ((phi d - 1) * k)) MOD d` THEN
 619     REWRITE_TAC[LEFT_EXISTS_AND_THM] THEN
 620     CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 621     MATCH_MP_TAC CONG_TRANS THEN
 622     EXISTS_TAC `(x * a EXP k) * (z * a EXP ((phi d - 1) * k))` THEN
 623     CONJ_TAC THENL
 624      [MATCH_MP_TAC CONG_MULT THEN ASM_SIMP_TAC[CONG_MOD; LE_1]; ALL_TAC] THEN
 625     ONCE_REWRITE_TAC[ARITH_RULE
 626      `(x * a) * (z * ak):num = (x * z) * (a * ak)`] THEN
 627     GEN_REWRITE_TAC (LAND_CONV) [ARITH_RULE `1 = 1 * 1`] THEN
 628     MATCH_MP_TAC CONG_MULT THEN ASM_REWRITE_TAC[] THEN
 629     REWRITE_TAC[GSYM EXP_ADD] THEN
 630     SUBGOAL_THEN `k + (phi d - 1) * k = phi(d) * k` SUBST1_TAC THENL
 631      [REWRITE_TAC[ARITH_RULE `k + a * k = (a + 1) * k`] THEN
 632       AP_THM_TAC THEN AP_TERM_TAC THEN
 633       ASM_SIMP_TAC[SUB_ADD; PHI_LOWERBOUND_1_STRONG];
 634       ALL_TAC] THEN
 635     REWRITE_TAC[GSYM EXP_EXP] THEN SUBST1_TAC(SYM(SPEC `k:num` EXP_ONE)) THEN
 636     MATCH_MP_TAC CONG_EXP THEN ASM_SIMP_TAC[FERMAT_LITTLE];
 637     REWRITE_TAC[IN_ELIM_THM; IN_UNIV] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 638     ASM_SIMP_TAC[COMPLEX_ENTIRE; COMPLEX_POW_EQ_0] THEN
 639     UNDISCH_TAC `!x:num. x IN h ==> ~(f x = Cx (&0))` THEN
 640     DISCH_THEN(MP_TAC o SPEC `am:num`) THEN ASM_REWRITE_TAC[] THEN
 641     SUBST1_TAC(SYM(ASSUME `z pow m = f(am:num)`)) THEN
 642     REWRITE_TAC[COMPLEX_POW_EQ_0] THEN ASM_SIMP_TAC[LE_1];
 643     REWRITE_TAC[IN_ELIM_THM; IN_UNIV; LEFT_AND_EXISTS_THM] THEN
 644     REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 645     MAP_EVERY X_GEN_TAC
 646      [`r:num`; `s:num`; `x:num`; `k:num`; `y:num`; `j:num`] THEN
 647     STRIP_TAC THEN REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN
 648     MATCH_MP_TAC EQ_TRANS THEN
 649     EXISTS_TAC `g(((x * y) MOD d * a EXP (k + j)) MOD d):complex` THEN
 650     CONJ_TAC THENL
 651      [AP_TERM_TAC THEN ASM_SIMP_TAC[MOD_MULT_LMOD; MOD_MULT_RMOD; LE_1] THEN
 652       REWRITE_TAC[EXP_ADD; MULT_AC];
 653       ALL_TAC] THEN
 654     ASM_SIMP_TAC[] THEN REWRITE_TAC[COMPLEX_POW_ADD; COMPLEX_MUL_AC]]);;
 655
 656 (* ------------------------------------------------------------------------- *)
 657 (* Hence the key result that we can find a distinguishing character.         *)
 658 (* ------------------------------------------------------------------------- *)
 659
 660 let DIRICHLET_CHARACTER_DISCRIMINATOR = prove
 661  (`!d n. 1 < d /\ ~((n == 1) (mod d))
 662           ==> ?c. dirichlet_character d c /\ ~(c n = Cx(&1))`,
 663   REPEAT STRIP_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP LT_IMP_LE) THEN
 664   ASM_CASES_TAC `coprime(n,d)` THENL
 665    [ALL_TAC;
 666     EXISTS_TAC `chi_0 d` THEN
 667     ASM_REWRITE_TAC[DIRICHLET_CHARACTER_CHI_0; chi_0] THEN
 668     CONV_TAC COMPLEX_RING] THEN
 669   MP_TAC(ISPECL [`\n:num. Cx(&1)`; `{1}`; `n MOD d`; `d:num`]
 670                 CHARACTER_EXTEND_FROM_SUBGROUP) THEN
 671   ASM_SIMP_TAC[IN_SING; IN_ELIM_THM; IN_DIFF] THEN ANTS_TAC THENL
 672    [ASM_SIMP_TAC[SUBSET; MULT_CLAUSES; MOD_LT; LE_1; IN_SING;
 673                  IN_ELIM_THM; DIVISION; COPRIME_MOD; CONG_MOD_LT;
 674                  COMPLEX_MUL_LID; CX_INJ; REAL_OF_NUM_EQ; ARITH] THEN
 675     ASM_MESON_TAC[COPRIME_1; COPRIME_SYM; CONG_REFL];
 676     ALL_TAC] THEN
 677   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 678   MAP_EVERY X_GEN_TAC [`f0:num->complex`; `h0:num->bool`] THEN
 679   STRIP_TAC THEN
 680   SUBGOAL_THEN
 681    `!m. m <= CARD {x | x < d /\ coprime(x,d)}
 682         ==> ?f h. h SUBSET {x | x < d /\ coprime(x,d)} /\
 683                  (1 IN h) /\ (n MOD d) IN h /\
 684                  (!x y. x IN h /\ y IN h ==> ((x * y) MOD d) IN h) /\
 685                  (!x. x IN h ==> ?y. y IN h /\ (x * y == 1) (mod d)) /\
 686                  ~(f(n MOD d) = Cx(&1)) /\
 687                  (!x. x IN h ==> ~(f x = Cx(&0))) /\
 688                  (!x y. x IN h /\ y IN h
 689                           ==> f((x * y) MOD d) = f(x) * f(y)) /\
 690                  m <= CARD h`
 691   MP_TAC THENL
 692    [MATCH_MP_TAC num_WF THEN X_GEN_TAC `m:num` THEN
 693     DISCH_THEN(LABEL_TAC "*") THEN DISCH_TAC THEN
 694     ASM_CASES_TAC `m = 0` THENL
 695      [MAP_EVERY EXISTS_TAC [`f0:num->complex`; `h0:num->bool`] THEN
 696       ASM_REWRITE_TAC[LE_0] THEN ASM SET_TAC[];
 697       ALL_TAC] THEN
 698     FIRST_ASSUM(MP_TAC o C MATCH_MP
 699      (MATCH_MP (ARITH_RULE `~(m = 0) ==> m - 1 < m`) (ASSUME `~(m = 0)`))) THEN
 700     ASM_SIMP_TAC[ARITH_RULE `x <= n ==> x - 1 <= n`; LEFT_IMP_EXISTS_THM] THEN
 701     MAP_EVERY X_GEN_TAC [`f:num->complex`; `h:num->bool`] THEN STRIP_TAC THEN
 702     ASM_CASES_TAC `m <= CARD(h:num->bool)` THENL
 703      [MAP_EVERY EXISTS_TAC [`f:num->complex`; `h:num->bool`] THEN
 704       ASM_REWRITE_TAC[];
 705       ALL_TAC] THEN
 706     MP_TAC(ASSUME `h SUBSET {x | x < d /\ coprime (x,d)}`) THEN
 707     DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE
 708      `s SUBSET t ==> ~(s = t) ==> ?a. a IN t /\ ~(a IN s)`)) THEN
 709     ANTS_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[IN_ELIM_THM]] THEN
 710     DISCH_THEN(X_CHOOSE_THEN `a:num` STRIP_ASSUME_TAC) THEN
 711     MP_TAC(ISPECL [`f:num->complex`; `h:num->bool`; `a:num`; `d:num`]
 712                 CHARACTER_EXTEND_FROM_SUBGROUP) THEN
 713     ASM_REWRITE_TAC[IN_DIFF; IN_ELIM_THM] THEN
 714     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `ff:num->complex` THEN
 715     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `hh:num->bool` THEN
 716     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 717     REPEAT(CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
 718     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `CARD((a:num) INSERT h)` THEN
 719     SUBGOAL_THEN `FINITE(h:num->bool)` ASSUME_TAC THENL
 720      [MATCH_MP_TAC FINITE_SUBSET THEN
 721       EXISTS_TAC `{x | x IN {x | x < d} /\ coprime(x,d)}` THEN
 722       SIMP_TAC[FINITE_RESTRICT; FINITE_NUMSEG_LT] THEN
 723       ASM_REWRITE_TAC[IN_ELIM_THM];
 724       ALL_TAC] THEN
 725     CONJ_TAC THENL
 726      [ASM_SIMP_TAC[CARD_CLAUSES] THEN
 727       UNDISCH_TAC `m - 1 <= CARD(h:num->bool)` THEN ARITH_TAC;
 728       MATCH_MP_TAC CARD_SUBSET THEN ASM_REWRITE_TAC[] THEN
 729       MATCH_MP_TAC FINITE_SUBSET THEN
 730       EXISTS_TAC `{x | x IN {x | x < d} /\ coprime(x,d)}` THEN
 731       SIMP_TAC[FINITE_RESTRICT; FINITE_NUMSEG_LT] THEN
 732       ASM_REWRITE_TAC[IN_ELIM_THM]];
 733     ALL_TAC] THEN
 734   DISCH_THEN(MP_TAC o SPEC `CARD {x | x < d /\ coprime(x,d)}`) THEN
 735   REWRITE_TAC[LE_REFL] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 736   MAP_EVERY X_GEN_TAC [`f:num->complex`; `h:num->bool`] THEN
 737   ASM_CASES_TAC `h = {x | x < d /\ coprime (x,d)}` THENL
 738    [ALL_TAC;
 739     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 740     REWRITE_TAC[CONJ_ASSOC] THEN MATCH_MP_TAC(TAUT `~b ==> a /\ b ==> c`) THEN
 741     REWRITE_TAC[NOT_LE] THEN MATCH_MP_TAC CARD_PSUBSET THEN
 742     ASM_REWRITE_TAC[PSUBSET] THEN
 743     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{x:num | x < d}` THEN
 744     SIMP_TAC[FINITE_RESTRICT; FINITE_NUMSEG_LT] THEN SET_TAC[]] THEN
 745   FIRST_X_ASSUM SUBST_ALL_TAC THEN
 746   REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN REWRITE_TAC[GSYM CONJ_ASSOC] THEN
 747   STRIP_TAC THEN
 748   EXISTS_TAC `\n. if coprime(n,d) then f(n MOD d) else Cx(&0)` THEN
 749   ASM_REWRITE_TAC[] THEN REWRITE_TAC[dirichlet_character] THEN
 750   REPEAT CONJ_TAC THEN X_GEN_TAC `x:num` THENL
 751    [REWRITE_TAC[NUMBER_RULE `coprime(x + d:num,d) <=> coprime(x,d)`] THEN
 752     COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
 753     ASM_SIMP_TAC[GSYM CONG; LE_1] THEN CONV_TAC NUMBER_RULE;
 754     COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 755     FIRST_X_ASSUM MATCH_MP_TAC THEN
 756     ASM_SIMP_TAC[COPRIME_MOD; DIVISION; LE_1];
 757     X_GEN_TAC `y:num` THEN REWRITE_TAC[COPRIME_LMUL] THEN
 758     MAP_EVERY ASM_CASES_TAC [`coprime(x,d)`; `coprime(y,d)`] THEN
 759     ASM_REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO] THEN
 760     MATCH_MP_TAC EQ_TRANS THEN
 761     EXISTS_TAC `f(((x MOD d) * (y MOD d)) MOD d):complex` THEN CONJ_TAC THENL
 762      [AP_TERM_TAC THEN ASM_SIMP_TAC[MOD_MULT_MOD2; LE_1];
 763       FIRST_X_ASSUM MATCH_MP_TAC THEN
 764       ASM_SIMP_TAC[DIVISION; COPRIME_MOD; LE_1]]]);;
 765
 766 (* ------------------------------------------------------------------------- *)
 767 (* Hence we get the full second orthogonality relation.                      *)
 768 (* ------------------------------------------------------------------------- *)
 769
 770 let DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_INEXPLICIT = prove
 771  (`!d n. vsum {c | dirichlet_character d c} (\c. c n) =
 772                 if (n == 1) (mod d)
 773                 then Cx(&(CARD {c | dirichlet_character d c}))
 774                 else Cx(&0)`,
 775   REPEAT GEN_TAC THEN
 776   ASM_CASES_TAC `d = 0` THENL
 777    [ASM_REWRITE_TAC[CONG_MOD_0; DIRICHLET_CHARACTER_0; SET_RULE
 778      `{x | x = a} = {a}`] THEN
 779     SIMP_TAC[VSUM_CLAUSES; CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY] THEN
 780     REWRITE_TAC[chi_0; COPRIME_0; VECTOR_ADD_RID] THEN REWRITE_TAC[ARITH];
 781     ALL_TAC] THEN
 782   ASM_CASES_TAC `d = 1` THENL
 783    [ASM_REWRITE_TAC[CONG_MOD_1; DIRICHLET_CHARACTER_1] THEN
 784     REWRITE_TAC[GSYM FUN_EQ_THM; ETA_AX] THEN
 785     ASM_REWRITE_TAC[SET_RULE `{x | x = a} = {a}`] THEN
 786     SIMP_TAC[VSUM_CLAUSES; CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY] THEN
 787     REWRITE_TAC[VECTOR_ADD_RID; ARITH];
 788     ALL_TAC] THEN
 789   COND_CASES_TAC THENL
 790    [MATCH_MP_TAC EQ_TRANS THEN
 791     EXISTS_TAC `vsum {c | dirichlet_character d c} (\c. Cx(&1))` THEN
 792     CONJ_TAC THENL
 793      [MATCH_MP_TAC VSUM_EQ THEN REWRITE_TAC[IN_ELIM_THM] THEN
 794       ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_1; DIRICHLET_CHARACTER_CONG];
 795       SIMP_TAC[FINITE_DIRICHLET_CHARACTERS; VSUM_CONST] THEN
 796       REWRITE_TAC[COMPLEX_CMUL; COMPLEX_MUL_RID]];
 797     MP_TAC(SPECL [`d:num`; `n:num`]
 798       DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_WEAK) THEN
 799     ASM_MESON_TAC[DIRICHLET_CHARACTER_DISCRIMINATOR;
 800                   ARITH_RULE `~(d = 0) /\ ~(d = 1) ==> 1 < d`]]);;
 801
 802 let DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS = prove
 803  (`!d n. 1 <= d
 804          ==> vsum {c | dirichlet_character d c} (\c. c(n)) =
 805                 if (n == 1) (mod d) then Cx(&(phi d)) else Cx(&0)`,
 806   REPEAT STRIP_TAC THEN
 807   REWRITE_TAC[DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_INEXPLICIT] THEN
 808   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 809   MP_TAC(ISPECL [`\c n. (c:num->complex) n`; `{c | dirichlet_character d c}`;
 810                  `1..d`;] VSUM_SWAP) THEN
 811   SIMP_TAC[DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_INEXPLICIT;
 812            DIRICHLET_CHARACTER_SUM_OVER_NUMBERS; FINITE_NUMSEG;
 813            FINITE_DIRICHLET_CHARACTERS; ETA_AX] THEN
 814   REWRITE_TAC[VSUM_DELTA; GSYM COMPLEX_VEC_0] THEN
 815   REWRITE_TAC[IN_ELIM_THM; DIRICHLET_CHARACTER_CHI_0] THEN
 816   DISCH_THEN SUBST1_TAC THEN
 817   SIMP_TAC[GSYM VSUM_RESTRICT_SET; FINITE_NUMSEG] THEN
 818   SUBGOAL_THEN `{j | j IN 1..d /\ (j == 1) (mod d)} = {1}`
 819    (fun th -> SIMP_TAC[th; VSUM_SING]) THEN
 820   REWRITE_TAC[EXTENSION; IN_SING; IN_ELIM_THM; IN_NUMSEG] THEN
 821   X_GEN_TAC `k:num` THEN EQ_TAC THEN ASM_SIMP_TAC[LE_REFL; CONG_REFL] THEN
 822   ASM_CASES_TAC `d = 1` THEN ASM_SIMP_TAC[CONG_MOD_1; LE_ANTISYM] THEN
 823   ASM_CASES_TAC `k:num = d` THENL
 824    [ASM_REWRITE_TAC[NUMBER_RULE `(d == 1) (mod d) <=> d divides 1`] THEN
 825     ASM_REWRITE_TAC[DIVIDES_ONE];
 826     STRIP_TAC THEN MATCH_MP_TAC CONG_IMP_EQ THEN EXISTS_TAC `d:num` THEN
 827     ASM_REWRITE_TAC[LT_LE]]);;
 828
 829 (* ------------------------------------------------------------------------- *)
 830 (* L-series, just at the point s = 1.                                        *)
 831 (* ------------------------------------------------------------------------- *)
 832
 833 let Lfunction_DEF = new_definition
 834  `Lfunction c = infsum (from 1) (\n. c(n) / Cx(&n))`;;
 835
 836 let BOUNDED_LFUNCTION_PARTIAL_SUMS = prove
 837  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
 838          ==> bounded {vsum (1..n) c | n IN (:num)}`,
 839   REPEAT GEN_TAC THEN DISCH_TAC THEN
 840   FIRST_ASSUM(fun th ->
 841     ONCE_REWRITE_TAC[MATCH_MP DIRICHLET_CHARACTER_SUM_MOD th]) THEN
 842   MATCH_MP_TAC BOUNDED_SUBSET THEN
 843   EXISTS_TAC `IMAGE (\n. vsum(1..n) c:complex) (0..d)` THEN
 844   SIMP_TAC[FINITE_IMP_BOUNDED; FINITE_IMAGE; FINITE_NUMSEG] THEN
 845   REWRITE_TAC[SIMPLE_IMAGE; SUBSET; FORALL_IN_IMAGE] THEN
 846   X_GEN_TAC `n:num` THEN REWRITE_TAC[IN_UNIV; IN_IMAGE] THEN
 847   EXISTS_TAC `n MOD d` THEN REWRITE_TAC[IN_NUMSEG; LE_0] THEN
 848   ASM_MESON_TAC[LT_IMP_LE; DIVISION;
 849                 DIRICHLET_CHARACTER_NONPRINCIPAL_NONTRIVIAL]);;
 850
 851 let LFUNCTION = prove
 852  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
 853          ==> ((\n. c(n) / Cx(&n)) sums (Lfunction c)) (from 1)`,
 854   REPEAT GEN_TAC THEN DISCH_TAC THEN SIMP_TAC[Lfunction_DEF; SUMS_INFSUM] THEN
 855   REWRITE_TAC[complex_div] THEN MATCH_MP_TAC SERIES_DIRICHLET_COMPLEX THEN
 856   REPEAT(EXISTS_TAC `1`) THEN FIRST_ASSUM(fun th ->
 857     REWRITE_TAC[MATCH_MP BOUNDED_LFUNCTION_PARTIAL_SUMS th]) THEN
 858   REWRITE_TAC[LIM_INV_N; GSYM CX_INV; REAL_CX; RE_CX] THEN
 859   SIMP_TAC[REAL_LE_INV2; REAL_OF_NUM_LE; REAL_OF_NUM_LT; LE_1; LE_ADD]);;
 860
 861 (* ------------------------------------------------------------------------- *)
 862 (* Other properties of conjugate characters.                                 *)
 863 (* ------------------------------------------------------------------------- *)
 864
 865 let CNJ_CHI_0 = prove
 866  (`!d n. cnj(chi_0 d n) = chi_0 d n`,
 867   REPEAT GEN_TAC THEN REWRITE_TAC[chi_0] THEN
 868   COND_CASES_TAC THEN ASM_REWRITE_TAC[CNJ_CX]);;
 869
 870 let LFUNCTION_CNJ = prove
 871  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
 872          ==> Lfunction (\n. cnj(c n)) = cnj(Lfunction c)`,
 873   REPEAT STRIP_TAC THEN REWRITE_TAC[Lfunction_DEF] THEN
 874   MATCH_MP_TAC INFSUM_UNIQUE THEN
 875   ONCE_REWRITE_TAC[GSYM CNJ_CX] THEN
 876   REWRITE_TAC[GSYM CNJ_DIV] THEN
 877   REWRITE_TAC[SUMS_CNJ; CNJ_CX; GSYM Lfunction_DEF] THEN
 878   ASM_MESON_TAC[LFUNCTION]);;
 879
 880 (* ------------------------------------------------------------------------- *)
 881 (* Explicit bound on truncating the Lseries.                                 *)
 882 (* ------------------------------------------------------------------------- *)
 883
 884 let LFUNCTION_PARTIAL_SUM = prove
 885  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
 886          ==> ?B. &0 < B /\
 887                  !n. 1 <= n
 888                      ==> norm(Lfunction c - vsum(1..n) (\n. c(n) / Cx(&n)))
 889                           <= B / (&n + &1)`,
 890   REPEAT GEN_TAC THEN DISCH_TAC THEN
 891   MP_TAC(ISPECL [`c:num->complex`; `\n. inv(Cx(&n))`; `1`; `1`]
 892                 SERIES_DIRICHLET_COMPLEX_EXPLICIT) THEN
 893   REWRITE_TAC[LE_REFL] THEN FIRST_ASSUM(fun th ->
 894     REWRITE_TAC[MATCH_MP BOUNDED_LFUNCTION_PARTIAL_SUMS th]) THEN
 895   REWRITE_TAC[LIM_INV_N; GSYM CX_INV; REAL_CX; RE_CX] THEN
 896   SIMP_TAC[REAL_LE_INV2; REAL_OF_NUM_LE; REAL_OF_NUM_LT; LE_1; LE_ADD] THEN
 897   REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS] THEN
 898   REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_INV; REAL_ABS_NUM] THEN
 899   REWRITE_TAC[CX_INV; GSYM complex_div; GSYM real_div] THEN
 900   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `B:real` THEN
 901   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `k:num` THEN DISCH_TAC THEN
 902   MATCH_MP_TAC(ISPEC `sequentially` LIM_NORM_UBOUND) THEN
 903   EXISTS_TAC `\n. vsum(k+1..n) (\n. c(n) / Cx(&n))` THEN
 904   REWRITE_TAC[TRIVIAL_LIMIT_SEQUENTIALLY] THEN CONJ_TAC THENL
 905    [FIRST_ASSUM(MP_TAC o MATCH_MP LFUNCTION) THEN
 906     MP_TAC(ISPECL [`sequentially`; `vsum (1..k) (\n. c n / Cx (&n))`]
 907                 LIM_CONST) THEN
 908     REWRITE_TAC[GSYM IMP_CONJ_ALT; sums; FROM_INTER_NUMSEG] THEN
 909     DISCH_THEN(MP_TAC o MATCH_MP LIM_SUB) THEN
 910     MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] LIM_TRANSFORM) THEN
 911     REWRITE_TAC[] THEN MATCH_MP_TAC LIM_EVENTUALLY THEN
 912     REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN EXISTS_TAC `k + 1` THEN
 913     X_GEN_TAC `m:num` THEN DISCH_TAC THEN
 914     FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `k + 1 <= m ==> k <= m`)) THEN
 915     SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM] THEN
 916     ASM_SIMP_TAC[VSUM_ADD_SPLIT; ARITH_RULE `1 <= k ==> 1 <= k + 1`] THEN
 917     REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC;
 918     MATCH_MP_TAC ALWAYS_EVENTUALLY THEN
 919     ASM_SIMP_TAC[ARITH_RULE `1 <= k + 1`; REAL_OF_NUM_ADD]]);;
 920
 921 let LFUNCTION_PARTIAL_SUM_STRONG = prove
 922  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
 923          ==> ?B. &0 < B /\
 924                  !n. norm(Lfunction c - vsum(1..n) (\n. c(n) / Cx(&n)))
 925                          <= B / (&n + &1)`,
 926   REPEAT GEN_TAC THEN DISCH_TAC THEN
 927   FIRST_ASSUM(MP_TAC o MATCH_MP LFUNCTION_PARTIAL_SUM) THEN
 928   DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
 929   EXISTS_TAC `max B (norm(Lfunction c))` THEN
 930   ASM_SIMP_TAC[REAL_LT_MAX] THEN X_GEN_TAC `n:num` THEN
 931   ASM_CASES_TAC `n = 0` THENL
 932    [ASM_REWRITE_TAC[VSUM_CLAUSES_NUMSEG; VECTOR_SUB_RZERO; ARITH] THEN
 933     REAL_ARITH_TAC;
 934     FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN ASM_SIMP_TAC[LE_1] THEN
 935     MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
 936     ASM_SIMP_TAC[REAL_LE_DIV2_EQ; REAL_ARITH `&0 < &n + &1`] THEN
 937     REAL_ARITH_TAC]);;
 938
 939 (* ------------------------------------------------------------------------- *)
 940 (* First key bound, when the Lfunction is not zero (as indeed it isn't).     *)
 941 (* ------------------------------------------------------------------------- *)
 942
 943 let BOUNDED_LFUNCTION_DIRICHLET_MANGOLDT_LEMMA = prove
 944  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
 945          ==> bounded
 946               { Lfunction(c) *
 947                 vsum(1..x) (\n. c(n) * Cx(mangoldt n / &n)) -
 948                 vsum(1..x) (\n. c(n) * Cx(log(&n) / &n)) | x IN (:num)}`,
 949   REWRITE_TAC[BOUNDED_POS; SIMPLE_IMAGE; FORALL_IN_IMAGE; IN_UNIV] THEN
 950   REPEAT STRIP_TAC THEN
 951   SIMP_TAC[LOG_MANGOLDT_SUM; real_div; CX_MUL;  GSYM VSUM_CX; FINITE_DIVISORS;
 952            LE_1; GSYM VSUM_COMPLEX_LMUL; GSYM VSUM_COMPLEX_RMUL] THEN
 953   REWRITE_TAC[VSUM_VSUM_DIVISORS] THEN
 954   FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP DIRICHLET_CHARACTER_MUL th]) THEN
 955   REWRITE_TAC[GSYM REAL_OF_NUM_MUL; COMPLEX_INV_MUL; CX_MUL; CX_INV] THEN
 956   ONCE_REWRITE_TAC[COMPLEX_RING
 957    `(ck * cn) * cm * k * n:complex = (ck * k) * (cn * cm * n)`] THEN
 958   SIMP_TAC[VSUM_COMPLEX_RMUL; FINITE_NUMSEG] THEN
 959   SIMP_TAC[GSYM VSUM_COMPLEX_LMUL; FINITE_NUMSEG] THEN
 960   SIMP_TAC[GSYM VSUM_SUB; FINITE_NUMSEG] THEN
 961   REWRITE_TAC[GSYM COMPLEX_SUB_RDISTRIB] THEN
 962   MP_TAC(SPECL [`d:num`; `c:num->complex`] LFUNCTION_PARTIAL_SUM_STRONG) THEN
 963   ASM_REWRITE_TAC[] THEN
 964   DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
 965   EXISTS_TAC `&18 * B` THEN
 966   ASM_SIMP_TAC[REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
 967   X_GEN_TAC `x:num` THEN MATCH_MP_TAC VSUM_NORM_TRIANGLE THEN
 968   REWRITE_TAC[FINITE_NUMSEG; COMPLEX_NORM_MUL] THEN
 969   REWRITE_TAC[COMPLEX_NORM_INV; COMPLEX_NORM_CX; REAL_ABS_NUM] THEN
 970   REWRITE_TAC[GSYM real_div] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN
 971   REWRITE_TAC[real_abs; MANGOLDT_POS_LE] THEN ASM_CASES_TAC `x = 0` THEN
 972   ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; ARITH; REAL_LE_MUL; REAL_LT_IMP_LE;
 973                REAL_OF_NUM_LT; ARITH] THEN
 974   MATCH_MP_TAC REAL_LE_TRANS THEN
 975   EXISTS_TAC `sum(1..x) (\n. B / &x * mangoldt n)` THEN CONJ_TAC THENL
 976    [ALL_TAC;
 977     REWRITE_TAC[SUM_LMUL] THEN
 978     MATCH_MP_TAC REAL_LE_TRANS THEN
 979     EXISTS_TAC `B / &x * &18 * &x` THEN CONJ_TAC THENL
 980      [MATCH_MP_TAC REAL_LE_LMUL THEN
 981       ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; REAL_LT_IMP_LE] THEN
 982       REWRITE_TAC[REWRITE_RULE[ETA_AX] PSI_BOUND];
 983       ASM_SIMP_TAC[REAL_FIELD `~(x = &0) ==> B / x * &18 * x = &18 * B`;
 984                    REAL_OF_NUM_EQ; REAL_LE_REFL]]] THEN
 985   MATCH_MP_TAC SUM_LE_NUMSEG THEN X_GEN_TAC `n:num` THEN
 986   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 987   FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP DIRICHLET_CHARACTER_NORM th]) THEN
 988   COND_CASES_TAC THEN
 989   ASM_SIMP_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_MUL_RID; REAL_LE_MUL;
 990                REAL_LE_DIV; REAL_POS; REAL_LT_IMP_LE; MANGOLDT_POS_LE] THEN
 991   REWRITE_TAC[real_div; REAL_ARITH `a * b * c <= d <=> (a * c) * b <= d`] THEN
 992   MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[MANGOLDT_POS_LE] THEN
 993   ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN
 994   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `B / (&(x DIV n) + &1)` THEN
 995   ASM_REWRITE_TAC[GSYM complex_div] THEN
 996   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
 997   ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN
 998   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_INV_INV] THEN
 999   ONCE_REWRITE_TAC[GSYM REAL_INV_MUL] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
1000   SUBGOAL_THEN `1 <= x` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
1001   ASM_SIMP_TAC[GSYM real_div; REAL_LT_DIV; REAL_OF_NUM_LT; LE_1] THEN
1002   ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN
1003   REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
1004   MP_TAC(SPECL [`x:num`; `n:num`] DIVISION) THEN ASM_ARITH_TAC);;
1005
1006 let SUMMABLE_CHARACTER_LOG_OVER_N = prove
1007  (`!c d. dirichlet_character d c /\ ~(c = chi_0 d)
1008          ==> summable (from 1) (\n. c(n) * Cx(log(&n) / &n))`,
1009   REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC SERIES_DIRICHLET_COMPLEX THEN
1010   MAP_EVERY EXISTS_TAC [`4`; `1`] THEN REWRITE_TAC[REAL_CX] THEN
1011   FIRST_ASSUM(fun th ->
1012     REWRITE_TAC[MATCH_MP BOUNDED_LFUNCTION_PARTIAL_SUMS th]) THEN
1013   CONJ_TAC THENL
1014    [SIMP_TAC[DECREASING_LOG_OVER_N; GSYM REAL_OF_NUM_ADD; RE_CX];
1015     MP_TAC LIM_LOG_OVER_N THEN
1016     MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] LIM_TRANSFORM_EVENTUALLY) THEN
1017     REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN EXISTS_TAC `1` THEN
1018     ASM_SIMP_TAC[CX_LOG; CX_DIV; LE_1; REAL_OF_NUM_LT]]);;
1019
1020 let BOUNDED_LFUNCTION_DIRICHLET_MANGOLDT = prove
1021  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
1022          ==> bounded
1023               { Lfunction(c) *
1024                 vsum(1..x) (\n. c(n) * Cx(mangoldt n / &n)) | x IN (:num)}`,
1025   REPEAT GEN_TAC THEN DISCH_TAC THEN
1026   FIRST_ASSUM(MP_TAC o
1027     MATCH_MP BOUNDED_LFUNCTION_DIRICHLET_MANGOLDT_LEMMA) THEN
1028   FIRST_ASSUM(MP_TAC o MATCH_MP SUMMABLE_CHARACTER_LOG_OVER_N) THEN
1029   DISCH_THEN(MP_TAC o MATCH_MP SUMMABLE_IMP_SUMS_BOUNDED) THEN
1030   REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP BOUNDED_SUMS) THEN
1031   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] BOUNDED_SUBSET) THEN
1032   REWRITE_TAC[SIMPLE_IMAGE; SUBSET; FORALL_IN_IMAGE] THEN
1033   REWRITE_TAC[IN_UNIV; IN_ELIM_THM; RIGHT_EXISTS_AND_THM; EXISTS_IN_IMAGE;
1034               GSYM CONJ_ASSOC] THEN
1035   X_GEN_TAC `n:num` THEN REPEAT(EXISTS_TAC `n:num`) THEN VECTOR_ARITH_TAC);;
1036
1037 let BOUNDED_DIRICHLET_MANGOLDT_NONZERO = prove
1038  (`!d c.
1039       dirichlet_character d c /\ ~(c = chi_0 d) /\ ~(Lfunction c = Cx(&0))
1040       ==> bounded { vsum(1..x) (\n. c n * Cx(mangoldt n / &n)) | x IN (:num)}`,
1041   REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
1042   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1043   DISCH_THEN(MP_TAC o MATCH_MP BOUNDED_LFUNCTION_DIRICHLET_MANGOLDT) THEN
1044   REWRITE_TAC[BOUNDED_POS; SIMPLE_IMAGE; FORALL_IN_IMAGE; IN_UNIV] THEN
1045   REWRITE_TAC[COMPLEX_NORM_MUL] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1046   ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; COMPLEX_NORM_NZ] THEN
1047   ASM_MESON_TAC[COMPLEX_NORM_NZ; REAL_LT_DIV]);;
1048
1049 (* ------------------------------------------------------------------------- *)
1050 (* Now a bound when the Lfunction is zero (hypothetically).                  *)
1051 (* ------------------------------------------------------------------------- *)
1052
1053 let MANGOLDT_LOG_SUM = prove
1054  (`!n. 1 <= n
1055        ==> mangoldt(n) = --(sum {d | d divides n} (\d. mobius(d) * log(&d)))`,
1056   REPEAT STRIP_TAC THEN
1057   MP_TAC(ISPECL [`\n. mangoldt n`; `\n. log(&n)`] MOBIUS_INVERSION) THEN
1058   ASM_SIMP_TAC[LOG_MANGOLDT_SUM; LE_1] THEN DISCH_THEN(K ALL_TAC) THEN
1059   MATCH_MP_TAC EQ_TRANS THEN
1060   EXISTS_TAC `sum {d | d divides n} (\x. mobius x * (log(&n) - log(&x)))` THEN
1061   CONJ_TAC THENL
1062    [MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `d:num` THEN
1063     REWRITE_TAC[IN_ELIM_THM; DIVIDES_DIV_MULT] THEN
1064     ABBREV_TAC `q = n DIV d` THEN
1065     MAP_EVERY ASM_CASES_TAC [`q = 0`; `d = 0`] THEN
1066     ASM_SIMP_TAC[MULT_CLAUSES; LE_1] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
1067     ASM_SIMP_TAC[GSYM REAL_OF_NUM_MUL; LOG_MUL; REAL_OF_NUM_LT; LE_1] THEN
1068     REAL_ARITH_TAC;
1069     ASM_SIMP_TAC[REAL_SUB_LDISTRIB; SUM_SUB; FINITE_DIVISORS; LE_1] THEN
1070     ASM_SIMP_TAC[SUM_RMUL; REWRITE_RULE[ETA_AX] DIVISORSUM_MOBIUS] THEN
1071     MATCH_MP_TAC(REAL_ARITH `a = &0 ==> a - b = --b`) THEN
1072     COND_CASES_TAC THEN ASM_REWRITE_TAC[LOG_1] THEN REAL_ARITH_TAC]);;
1073
1074 let BOUNDED_DIRICHLET_MANGOLDT_LEMMA = prove
1075  (`!d c x.
1076         dirichlet_character d c /\ ~(c = chi_0 d) /\ 1 <= x
1077         ==> Cx(log(&x)) + vsum (1..x) (\n. c(n) * Cx(mangoldt n / &n)) =
1078             vsum (1..x) (\n. c(n) / Cx(&n) *
1079                              vsum {d | d divides n}
1080                                   (\d. Cx(mobius(d) * log(&x / &d))))`,
1081   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[MANGOLDT_LOG_SUM] THEN
1082   MATCH_MP_TAC(COMPLEX_RING `c - b = a ==> (a:complex) + b = c`) THEN
1083   SIMP_TAC[GSYM VSUM_SUB; FINITE_NUMSEG] THEN
1084   SIMP_TAC[CX_NEG; CX_DIV; GSYM VSUM_CX; FINITE_NUMSEG; FINITE_DIVISORS;
1085            LE_1] THEN
1086   REWRITE_TAC[SIMPLE_COMPLEX_ARITH
1087    `c / d * x - c * --y / d:complex = c / d * (x + y)`] THEN
1088   SIMP_TAC[GSYM VSUM_ADD; FINITE_DIVISORS; LE_1] THEN
1089   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
1090    `vsum (1..x)
1091          (\n. c n / Cx(&n) * vsum {d | d divides n}
1092                (\d. Cx(mobius d * log(&x))))` THEN
1093   CONJ_TAC THENL
1094    [MATCH_MP_TAC VSUM_EQ_NUMSEG THEN X_GEN_TAC `n:num` THEN STRIP_TAC THEN
1095     REWRITE_TAC[] THEN AP_TERM_TAC THEN MATCH_MP_TAC VSUM_EQ THEN
1096     X_GEN_TAC `m:num` THEN REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
1097     REWRITE_TAC[CX_MUL; GSYM COMPLEX_ADD_LDISTRIB] THEN AP_TERM_TAC THEN
1098     REWRITE_TAC[GSYM CX_ADD; CX_INJ] THEN
1099     ASM_CASES_TAC `m = 0` THENL
1100      [ASM_MESON_TAC[DIVIDES_ZERO; LE_1]; ALL_TAC] THEN
1101     ASM_SIMP_TAC[LOG_DIV; REAL_OF_NUM_LT; LE_1] THEN REAL_ARITH_TAC;
1102     SIMP_TAC[FINITE_DIVISORS; CX_MUL; SUM_RMUL; LE_1; VSUM_CX] THEN
1103     SIMP_TAC[REWRITE_RULE[ETA_AX] DIVISORSUM_MOBIUS] THEN
1104     SIMP_TAC[COND_RAND; COND_RATOR; COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO] THEN
1105     ASM_SIMP_TAC[VSUM_DELTA; GSYM COMPLEX_VEC_0; IN_NUMSEG; LE_REFL] THEN
1106     MP_TAC(SPECL [`d:num`; `c:num->complex`] DIRICHLET_CHARACTER_EQ_1) THEN
1107     ASM_SIMP_TAC[COMPLEX_MUL_LID; COMPLEX_DIV_1]]);;
1108
1109 let SUM_LOG_OVER_X_BOUND = prove
1110  (`!x. abs(sum(1..x) (\n. log(&x / &n) / &x)) <= &4`,
1111   X_GEN_TAC `x:num` THEN ASM_CASES_TAC `x = 0` THENL
1112    [ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; REAL_ABS_NUM; REAL_POS];
1113     ALL_TAC] THEN
1114   SIMP_TAC[real_div; SUM_RMUL; REAL_ABS_MUL; REAL_ABS_INV; REAL_ABS_NUM] THEN
1115   ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN
1116   MATCH_MP_TAC REAL_LE_TRANS THEN
1117   EXISTS_TAC `sum (1..x) (\n. abs(log(&x / &n)))` THEN
1118   REWRITE_TAC[SUM_ABS_NUMSEG] THEN
1119   ASM_SIMP_TAC[real_abs; LOG_POS; REAL_LE_RDIV_EQ; REAL_OF_NUM_LT;
1120                LE_1; REAL_MUL_LID; REAL_OF_NUM_LE; LOG_DIV] THEN
1121   REWRITE_TAC[SUM_SUB_NUMSEG; GSYM LOG_FACT] THEN
1122   REWRITE_TAC[SUM_CONST_NUMSEG; ADD_SUB] THEN
1123   FIRST_ASSUM(MP_TAC o MATCH_MP LOG_FACT_BOUNDS) THEN
1124   MATCH_MP_TAC(REAL_ARITH
1125    `&2 * l + abs(x) + &1 <= b
1126     ==> abs(lf - (xl - x + &1)) <= &2 * l
1127         ==> xl - lf <= b`) THEN
1128  MATCH_MP_TAC(REAL_ARITH
1129    `&1 <= x /\ l <= x ==> &2 * l + abs(x) + &1 <= &4 * x`) THEN
1130   ASM_SIMP_TAC[REAL_OF_NUM_LE; LE_1; LOG_LE_REFL]);;
1131
1132 let BOUNDED_DIRICHLET_MANGOLDT_ZERO = prove
1133  (`!d c.
1134       dirichlet_character d c /\ ~(c = chi_0 d) /\ Lfunction c = Cx(&0)
1135       ==> bounded { vsum(1..x) (\n. c n * Cx(mangoldt n / &n)) +
1136                     Cx(log(&x)) | x IN (:num)}`,
1137   ONCE_REWRITE_TAC[COMPLEX_ADD_SYM] THEN REPEAT STRIP_TAC THEN
1138   MP_TAC(SPECL [`d:num`; `c:num->complex`] LFUNCTION_PARTIAL_SUM_STRONG) THEN
1139   ASM_REWRITE_TAC[COMPLEX_SUB_LZERO; NORM_NEG] THEN
1140   DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
1141   SIMP_TAC[SET_RULE `{f x | x IN (:num)} = f 0 INSERT {f x | ~(x = 0)}`] THEN
1142   REWRITE_TAC[BOUNDED_INSERT; ARITH_RULE `~(n = 0) <=> 1 <= n`] THEN
1143   ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
1144   REWRITE_TAC[BOUNDED_POS; FORALL_IN_IMAGE; IN_ELIM_THM] THEN
1145   MP_TAC(SPECL [`d:num`; `c:num->complex`]
1146     BOUNDED_DIRICHLET_MANGOLDT_LEMMA) THEN
1147   ASM_SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN
1148   SIMP_TAC[GSYM VSUM_COMPLEX_LMUL; FINITE_DIVISORS; LE_1] THEN
1149   REWRITE_TAC[VSUM_VSUM_DIVISORS] THEN
1150   FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP DIRICHLET_CHARACTER_MUL th]) THEN
1151   REWRITE_TAC[GSYM REAL_OF_NUM_MUL; CX_MUL; complex_div; COMPLEX_INV_MUL] THEN
1152   ONCE_REWRITE_TAC[COMPLEX_RING
1153    `((ck * cn) * k' * n') * m * l = (cn * m * n') * l * (ck * k')`] THEN
1154   REWRITE_TAC[GSYM complex_div] THEN
1155   SIMP_TAC[VSUM_COMPLEX_LMUL; FINITE_NUMSEG] THEN
1156   EXISTS_TAC `&4 * B` THEN
1157   ASM_SIMP_TAC[REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
1158   X_GEN_TAC `x:num` THEN DISCH_TAC THEN MATCH_MP_TAC VSUM_NORM_TRIANGLE THEN
1159   REWRITE_TAC[FINITE_NUMSEG] THEN
1160   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
1161    `sum(1..x) (\n. inv(&n) * log(&x / &n) * B / (&(x DIV n) + &1))` THEN
1162   CONJ_TAC THENL
1163    [MATCH_MP_TAC SUM_LE_NUMSEG THEN X_GEN_TAC `n:num` THEN
1164     STRIP_TAC THEN REWRITE_TAC[] THEN ONCE_REWRITE_TAC[COMPLEX_NORM_MUL] THEN
1165     MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[NORM_POS_LE] THEN CONJ_TAC THENL
1166      [REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_DIV; COMPLEX_NORM_CX] THEN
1167       FIRST_ASSUM(fun t -> SIMP_TAC[MATCH_MP DIRICHLET_CHARACTER_NORM t]) THEN
1168       COND_CASES_TAC THEN
1169       REWRITE_TAC[REAL_MUL_LZERO; REAL_LE_INV_EQ; REAL_POS] THEN
1170       REWRITE_TAC[REAL_MUL_LID; REAL_ABS_NUM] THEN
1171       ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN
1172       ASM_SIMP_TAC[REAL_FIELD `&1 <= n ==> inv(n) * n = &1`; REAL_OF_NUM_LE;
1173                    REAL_ABS_MOBIUS];
1174       SIMP_TAC[CX_LOG; REAL_LT_DIV; REAL_OF_NUM_LT; LE_1] THEN
1175       SIMP_TAC[COMPLEX_NORM_CX; COMPLEX_NORM_MUL] THEN
1176       MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS; NORM_POS_LE] THEN
1177       ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ARITH `abs x <= x <=> &0 <= x`] THEN
1178       ASM_SIMP_TAC[LOG_POS; REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; LE_1;
1179                    REAL_MUL_LID; REAL_OF_NUM_LE]];
1180     ALL_TAC] THEN
1181   SIMP_TAC[real_div; REAL_RING `a * l * B * i:real = ((l * i) * a) * B`] THEN
1182   REWRITE_TAC[SUM_RMUL] THEN ASM_SIMP_TAC[REAL_LE_RMUL_EQ] THEN
1183   MATCH_MP_TAC REAL_LE_TRANS THEN
1184   EXISTS_TAC `sum(1..x) (\n. log(&x / &n) / &x)` THEN
1185   ASM_SIMP_TAC[REAL_ARITH `abs x <= a ==> x <= a`; SUM_LOG_OVER_X_BOUND] THEN
1186   MATCH_MP_TAC SUM_LE_NUMSEG THEN X_GEN_TAC `n:num` THEN STRIP_TAC THEN
1187   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
1188   MATCH_MP_TAC REAL_LE_LMUL THEN
1189   ASM_SIMP_TAC[GSYM real_div; LOG_POS; REAL_LE_RDIV_EQ; REAL_OF_NUM_LT;
1190                LE_1; REAL_MUL_LID; REAL_OF_NUM_LE] THEN
1191   ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN
1192   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_INV_INV] THEN
1193   REWRITE_TAC[GSYM REAL_INV_MUL] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
1194   ASM_SIMP_TAC[GSYM real_div; REAL_LT_DIV; REAL_OF_NUM_LT; LE_1] THEN
1195   ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN
1196   REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
1197   MP_TAC(SPECL [`x:num`; `n:num`] DIVISION) THEN ASM_ARITH_TAC);;
1198
1199 (* ------------------------------------------------------------------------- *)
1200 (* Now the analogous result for the principal character.                     *)
1201 (* ------------------------------------------------------------------------- *)
1202
1203 let BOUNDED_DIRICHLET_MANGOLDT_PRINCIPAL_LEMMA = prove
1204  (`!d. 1 <= d
1205        ==> norm(vsum(1..x) (\n. (chi_0 d n - Cx(&1)) * Cx(mangoldt n / &n)))
1206             <= sum {p | prime p /\ p divides d} (\p. log(&p))`,
1207   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1208   EXISTS_TAC `sum {p | prime p /\ p divides d}
1209                   (\p. sum {k | 1 <= k /\ p EXP k <= x}
1210                            (\k. log(&p) / &p pow k))` THEN
1211   CONJ_TAC THENL
1212    [ALL_TAC;
1213     MATCH_MP_TAC SUM_LE THEN ASM_SIMP_TAC[FINITE_SPECIAL_DIVISORS; LE_1] THEN
1214     X_GEN_TAC `p:num` THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
1215     SUBGOAL_THEN `2 <= p /\ 1 <= p /\ 1 < p` ASSUME_TAC THENL
1216      [ASM_MESON_TAC[PRIME_GE_2; ARITH_RULE `2 <= p ==> 1 < p /\ 1 <= p`];
1217       ALL_TAC] THEN
1218     MATCH_MP_TAC REAL_LE_TRANS THEN
1219     EXISTS_TAC `sum(1..x) (\k. log(&p) / &p pow k)` THEN CONJ_TAC THENL
1220      [MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN REWRITE_TAC[FINITE_NUMSEG] THEN
1221       ASM_SIMP_TAC[IN_DIFF; IN_NUMSEG; IN_ELIM_THM; SUBSET; REAL_POW_LE;
1222                    REAL_POS; REAL_LE_DIV; LOG_POS; REAL_OF_NUM_LE;
1223                    PRIME_GE_2; ARITH_RULE `2 <= p ==> 1 <= p`] THEN
1224       X_GEN_TAC `k:num` THEN STRIP_TAC THEN
1225       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `p EXP k` THEN
1226       ASM_REWRITE_TAC[] THEN
1227       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 EXP k` THEN
1228       ASM_SIMP_TAC[LT_POW2_REFL; LT_IMP_LE; EXP_MONO_LE];
1229       REWRITE_TAC[real_div; SUM_LMUL] THEN
1230       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
1231       ASM_SIMP_TAC[REAL_LE_LMUL_EQ; LOG_POS_LT; REAL_OF_NUM_LT] THEN
1232       SIMP_TAC[GSYM REAL_POW_INV; SUM_GP; REAL_INV_EQ_1; REAL_OF_NUM_EQ] THEN
1233       COND_CASES_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1234       COND_CASES_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
1235       ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_SUB_LT; REAL_LT_LDIV_EQ;
1236                    REAL_MUL_LID; REAL_OF_NUM_LT; LE_1] THEN
1237       REWRITE_TAC[real_pow] THEN
1238       MATCH_MP_TAC(REAL_ARITH `&0 <= x * y /\ &2 * x <= &1
1239                                 ==> x pow 1 - x * y <= &1 - x`) THEN
1240       ASM_SIMP_TAC[REAL_LE_DIV; REAL_POW_LE; REAL_POS; REAL_LE_MUL] THEN
1241       REWRITE_TAC[real_div; REAL_MUL_LID] THEN REWRITE_TAC[GSYM real_div] THEN
1242       ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_MUL_LID; REAL_OF_NUM_LT;
1243                    REAL_OF_NUM_LE; LE_1]]] THEN
1244    W(MP_TAC o PART_MATCH (lhs o rand) SUM_SUM_PRODUCT o rand o snd) THEN
1245     ANTS_TAC THENL
1246      [ASM_SIMP_TAC[FINITE_SPECIAL_DIVISORS; LE_1] THEN
1247       X_GEN_TAC `p:num` THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
1248       MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `1..x` THEN
1249       SIMP_TAC[SUBSET; FINITE_NUMSEG; IN_NUMSEG; IN_ELIM_THM] THEN
1250       X_GEN_TAC `k:num` THEN STRIP_TAC THEN
1251       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `p EXP k` THEN
1252       ASM_REWRITE_TAC[] THEN
1253       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 EXP k` THEN
1254       ASM_SIMP_TAC[LT_POW2_REFL; LT_IMP_LE; EXP_MONO_LE; PRIME_GE_2];
1255       ALL_TAC] THEN
1256     DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC VSUM_NORM_TRIANGLE THEN
1257     REWRITE_TAC[FINITE_NUMSEG; COMPLEX_NORM_MUL; COMPLEX_NORM_CX] THEN
1258     REWRITE_TAC[chi_0; COND_RAND; COND_RATOR] THEN
1259     REWRITE_TAC[COMPLEX_SUB_REFL; COMPLEX_SUB_LZERO] THEN
1260     REWRITE_TAC[COMPLEX_NORM_CX; NORM_NEG; REAL_ABS_NUM] THEN
1261     REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_LID] THEN
1262     REWRITE_TAC[mangoldt; COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
1263     ONCE_REWRITE_TAC[COND_RAND] THEN
1264     REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_ABS_NUM] THEN
1265     REWRITE_TAC[TAUT `(if a then &0 else if b then x else &0) =
1266                       (if ~a /\ b then x else &0)`] THEN
1267     SIMP_TAC[GSYM real_div; GSYM SUM_RESTRICT_SET; FINITE_NUMSEG] THEN
1268     MATCH_MP_TAC REAL_EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN
1269     MATCH_MP_TAC SUM_EQ_GENERAL THEN EXISTS_TAC `\(p,k). p EXP k` THEN
1270     REWRITE_TAC[EXISTS_UNIQUE; EXISTS_PAIR_THM; FORALL_PAIR_THM] THEN
1271     REWRITE_TAC[IN_ELIM_PAIR_THM] THEN
1272     REWRITE_TAC[IN_ELIM_THM; IN_NUMSEG; PAIR_EQ] THEN CONJ_TAC THENL
1273      [X_GEN_TAC `y:num` THEN
1274       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
1275       MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `p:num` THEN
1276       MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:num` THEN
1277       STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
1278       UNDISCH_TAC `~(coprime(p EXP k,d))` THEN
1279       ASM_SIMP_TAC[ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_PRIMEPOW; LE_1] THEN
1280       DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`q:num`; `j:num`] THEN
1281       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
1282       ASM_SIMP_TAC[EQ_PRIME_EXP] THEN ASM_ARITH_TAC;
1283       ALL_TAC] THEN
1284     MAP_EVERY X_GEN_TAC [`p:num`; `k:num`]  THEN
1285     ASM_SIMP_TAC[ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_PRIMEPOW; LE_1] THEN
1286     REPEAT STRIP_TAC THENL
1287      [ASM_MESON_TAC[EXP_EQ_0; LE_1; PRIME_0]; ASM_MESON_TAC[]; ALL_TAC] THEN
1288     REWRITE_TAC[GSYM REAL_OF_NUM_POW; REAL_ABS_DIV; REAL_ABS_POW;
1289                 REAL_ABS_NUM] THEN
1290     AP_THM_TAC THEN AP_TERM_TAC THEN
1291     MATCH_MP_TAC(REAL_ARITH `&0 <= y /\ x = y ==> abs x = y`) THEN
1292     ASM_SIMP_TAC[LOG_POS; REAL_OF_NUM_LE; PRIME_IMP_NZ; LE_1] THEN
1293     AP_TERM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN
1294     X_GEN_TAC `q:num` THEN REWRITE_TAC[] THEN EQ_TAC THENL
1295      [ASM_MESON_TAC[PRIME_DIVEXP; DIVIDES_PRIME_PRIME];
1296       DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[] THEN
1297       SUBGOAL_THEN `k = SUC(k - 1)` SUBST1_TAC THENL
1298        [ASM_ARITH_TAC; SIMP_TAC[EXP; DIVIDES_RMUL; DIVIDES_REFL]]]);;
1299
1300 let BOUNDED_DIRICHLET_MANGOLDT_PRINCIPAL = prove
1301  (`!d. 1 <= d
1302        ==> bounded { vsum(1..x) (\n. chi_0 d n * Cx(mangoldt n / &n)) -
1303                      Cx(log(&x)) | x IN (:num)}`,
1304   REPEAT STRIP_TAC THEN
1305   REWRITE_TAC[bounded; SIMPLE_IMAGE; FORALL_IN_IMAGE; IN_UNIV] THEN
1306   EXISTS_TAC
1307    `abs(sum {p | prime p /\ p divides d} (\p. log(&p))) +
1308     abs(log(&0)) + &21` THEN
1309   X_GEN_TAC `x:num` THEN ASM_CASES_TAC `x = 0` THENL
1310    [ASM_SIMP_TAC[VSUM_CLAUSES_NUMSEG; ARITH; VECTOR_SUB_LZERO] THEN
1311     REWRITE_TAC[NORM_NEG; COMPLEX_NORM_CX] THEN REAL_ARITH_TAC;
1312     ALL_TAC] THEN
1313   MATCH_MP_TAC(REAL_ARITH `x <= a + b ==> x <= a + abs y + b`) THEN
1314   MATCH_MP_TAC(NORM_ARITH
1315    `!s'. norm(s') <= p /\ norm(s - s' - l) <= &21
1316         ==> norm(s - l) <= abs p + &21`) THEN
1317   EXISTS_TAC `vsum(1..x) (\n. (chi_0 d n - Cx(&1)) * Cx(mangoldt n / &n))` THEN
1318   ASM_SIMP_TAC[BOUNDED_DIRICHLET_MANGOLDT_PRINCIPAL_LEMMA] THEN
1319   SIMP_TAC[GSYM VSUM_SUB; FINITE_NUMSEG] THEN
1320   REWRITE_TAC[COMPLEX_RING `c * x - (c - Cx(&1)) * x = x`] THEN
1321   SIMP_TAC[GSYM CX_SUB; VSUM_CX; FINITE_NUMSEG; COMPLEX_NORM_CX] THEN
1322   MATCH_MP_TAC MERTENS_LEMMA THEN ASM_REWRITE_TAC[]);;
1323
1324 (* ------------------------------------------------------------------------- *)
1325 (* The arithmetic-geometric mean that we want.                               *)
1326 (* ------------------------------------------------------------------------- *)
1327
1328 let SUM_OF_NUMBERS = prove
1329  (`!n. nsum(0..n) (\i. i) = (n * (n + 1)) DIV 2`,
1330   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
1331
1332 let PRODUCT_POW_NSUM = prove
1333  (`!s. FINITE s ==> product s (\i. z pow (f i)) = z pow (nsum s f)`,
1334   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1335   SIMP_TAC[PRODUCT_CLAUSES; NSUM_CLAUSES; real_pow; REAL_POW_ADD]);;
1336
1337 let PRODUCT_SPECIAL = prove
1338  (`!z i. product (0..n) (\i. z pow i) = z pow ((n * (n + 1)) DIV 2)`,
1339   SIMP_TAC[PRODUCT_POW_NSUM; FINITE_NUMSEG; SUM_OF_NUMBERS]);;
1340
1341 let AGM_SPECIAL = prove
1342  (`!n t. &0 <= t
1343          ==> (&n + &1) pow 2 * t pow n <= (sum(0..n) (\k. t pow k)) pow 2`,
1344   REPEAT STRIP_TAC THEN
1345   MP_TAC(ISPECL [`n + 1`; `\k. (t:real) pow (k - 1)`] AGM) THEN
1346   ASM_SIMP_TAC[REAL_POW_LE; ARITH_RULE `1 <= n + 1`] THEN
1347   SUBGOAL_THEN `1..n+1 = 0+1..n+1` SUBST1_TAC THENL
1348    [REWRITE_TAC[ADD_CLAUSES]; ALL_TAC] THEN
1349   REWRITE_TAC[SUM_OFFSET; PRODUCT_OFFSET; ADD_SUB] THEN
1350   REWRITE_TAC[PRODUCT_SPECIAL] THEN
1351   DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT] REAL_POW_LE2)) THEN
1352   DISCH_THEN(MP_TAC o SPEC `2`) THEN
1353   ASM_SIMP_TAC[PRODUCT_POS_LE_NUMSEG; REAL_POW_LE] THEN
1354   REWRITE_TAC[REAL_POW_POW] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
1355   SUBGOAL_THEN `2 * (n * (n + 1)) DIV 2 = n * (n + 1)` SUBST1_TAC THENL
1356    [SUBGOAL_THEN `EVEN(n * (n + 1))` MP_TAC THENL
1357      [REWRITE_TAC[EVEN_ADD; EVEN_MULT; ARITH_EVEN] THEN CONV_TAC TAUT;
1358       SIMP_TAC[EVEN_EXISTS; LEFT_IMP_EXISTS_THM; DIV_MULT; ARITH]];
1359     REWRITE_TAC[GSYM REAL_POW_POW] THEN DISCH_THEN(MP_TAC o MATCH_MP
1360      (REWRITE_RULE[IMP_CONJ_ALT] REAL_POW_LE2_REV)) THEN
1361     REWRITE_TAC[ADD_EQ_0; ARITH_EQ; REAL_POW_2; REAL_LE_SQUARE] THEN
1362     REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_OF_NUM_ADD] THEN
1363     ASM_SIMP_TAC[REAL_POW_DIV; REAL_LE_RDIV_EQ; REAL_POW_LT;
1364                  REAL_ARITH `&0 < &n + &1`] THEN
1365     REWRITE_TAC[REAL_MUL_AC]]);;
1366
1367 (* ------------------------------------------------------------------------- *)
1368 (* The trickiest part: the nonvanishing of L-series for real character.      *)
1369 (* Proof from Monsky's article (AMM 1993, pp. 861-2).                        *)
1370 (* ------------------------------------------------------------------------- *)
1371
1372 let DIVISORSUM_PRIMEPOW = prove
1373  (`!f p k. prime p
1374            ==> sum {m | m divides (p EXP k)} c = sum(0..k) (\i. c(p EXP i))`,
1375   REPEAT STRIP_TAC THEN
1376   ASM_SIMP_TAC[DIVIDES_PRIMEPOW; SET_RULE
1377    `{m | ?i. P i /\ m = f i} = IMAGE f {i | P i}`] THEN
1378   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM o_DEF] THEN
1379   REWRITE_TAC[GSYM NUMSEG_LE] THEN MATCH_MP_TAC SUM_IMAGE THEN
1380   ASM_SIMP_TAC[IN_ELIM_THM; EQ_EXP; FINITE_NUMSEG_LE] THEN
1381   ASM_MESON_TAC[PRIME_0; PRIME_1]);;
1382
1383 let DIVISORVSUM_PRIMEPOW = prove
1384  (`!f p k. prime p
1385            ==> vsum {m | m divides (p EXP k)} c = vsum(0..k) (\i. c(p EXP i))`,
1386   REPEAT STRIP_TAC THEN
1387   ASM_SIMP_TAC[DIVIDES_PRIMEPOW; SET_RULE
1388    `{m | ?i. P i /\ m = f i} = IMAGE f {i | P i}`] THEN
1389   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM o_DEF] THEN
1390   REWRITE_TAC[GSYM NUMSEG_LE] THEN MATCH_MP_TAC VSUM_IMAGE THEN
1391   ASM_SIMP_TAC[IN_ELIM_THM; EQ_EXP; FINITE_NUMSEG_LE] THEN
1392   ASM_MESON_TAC[PRIME_0; PRIME_1]);;
1393
1394 let DIRICHLET_CHARACTER_DIVISORSUM_EQ_1 = prove
1395  (`!d c p k. dirichlet_character d c /\ prime p /\ p divides d
1396              ==> vsum {m | m divides (p EXP k)} c = Cx(&1)`,
1397   REPEAT STRIP_TAC THEN
1398   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `vsum {1} c : complex` THEN
1399   CONJ_TAC THENL
1400    [ALL_TAC;
1401     REWRITE_TAC[VSUM_SING] THEN ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_1]] THEN
1402   MATCH_MP_TAC VSUM_SUPERSET THEN
1403   SIMP_TAC[SUBSET; IN_SING; IN_ELIM_THM; DIVIDES_1] THEN
1404   ASM_SIMP_TAC[DIVIDES_PRIMEPOW; LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
1405   MAP_EVERY X_GEN_TAC [`y:num`; `i:num`] THEN
1406   DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
1407   FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[COMPLEX_VEC_0] THEN
1408   FIRST_ASSUM(fun th -> SIMP_TAC[MATCH_MP DIRICHLET_CHARACTER_EQ_0 th]) THEN
1409   ONCE_REWRITE_TAC[COPRIME_SYM] THEN REWRITE_TAC[COPRIME_REXP] THEN
1410   ASM_CASES_TAC `i = 0` THEN ASM_REWRITE_TAC[EXP] THEN
1411   ASM_MESON_TAC[COPRIME_SYM; PRIME_COPRIME_EQ]);;
1412
1413 let DIRICHLET_CHARACTER_REAL_CASES = prove
1414  (`!d c. dirichlet_character d c /\ (!n. real(c n))
1415          ==> !n. c n = --Cx(&1) \/ c n = Cx(&0) \/ c n = Cx(&1)`,
1416   REPEAT GEN_TAC THEN STRIP_TAC THEN X_GEN_TAC `n:num` THEN
1417   FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP DIRICHLET_CHARACTER_NORM) THEN
1418   FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN REWRITE_TAC[REAL_EXISTS] THEN
1419   DISCH_THEN(X_CHOOSE_THEN `t:real` SUBST1_TAC) THEN
1420   REWRITE_TAC[COMPLEX_NORM_CX; GSYM CX_NEG; CX_INJ] THEN REAL_ARITH_TAC);;
1421
1422 let DIRICHLET_CHARACTER_DIVISORSUM_PRIMEPOW_POS = prove
1423  (`!d c p k. dirichlet_character d c /\ (!n. real(c n)) /\ prime p
1424              ==> &0 <= Re(vsum {m | m divides (p EXP k)} c)`,
1425   REPEAT STRIP_TAC THEN
1426   ASM_SIMP_TAC[RE_VSUM; FINITE_DIVISORS; EXP_EQ_0; PRIME_IMP_NZ] THEN
1427   ASM_SIMP_TAC[DIVISORSUM_PRIMEPOW] THEN
1428   FIRST_ASSUM(fun th -> SIMP_TAC[MATCH_MP DIRICHLET_CHARACTER_POW th]) THEN
1429   MP_TAC(SPECL [`d:num`; `c:num->complex`] DIRICHLET_CHARACTER_REAL_CASES) THEN
1430   ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `p:num`) THEN STRIP_TAC THEN
1431   ASM_SIMP_TAC[GSYM CX_POW; RE_CX; SUM_POS_LE_NUMSEG;
1432                REAL_POW_LE; REAL_POS] THEN
1433   MATCH_MP_TAC(REAL_ARITH `(s = if EVEN k then &1 else &0) ==> &0 <= s`) THEN
1434   SPEC_TAC(`k:num`,`r:num`) THEN
1435   INDUCT_TAC THEN REWRITE_TAC[EVEN; SUM_CLAUSES_NUMSEG] THEN
1436   ASM_REWRITE_TAC[complex_pow; RE_CX; LE_0] THEN COND_CASES_TAC THEN
1437   ASM_REWRITE_TAC[COMPLEX_POW_NEG; COMPLEX_POW_ONE; COMPLEX_MUL_LNEG;
1438                   COMPLEX_MUL_RNEG; COMPLEX_NEG_NEG; COMPLEX_MUL_LID;
1439                   RE_NEG; RE_CX] THEN
1440   REAL_ARITH_TAC);;
1441
1442 let DIRICHLET_CHARACTER_DIVISORSUM_POS = prove
1443  (`!d c n. dirichlet_character d c /\ (!n. real(c n)) /\ ~(n = 0)
1444            ==> &0 <= Re(vsum {m | m divides n} c)`,
1445   REPEAT STRIP_TAC THEN FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
1446    `~(n = 0) ==> n = 1 \/ 1 < n`))
1447   THENL
1448    [ASM_SIMP_TAC[DIVIDES_ONE; SING_GSPEC; VSUM_SING] THEN
1449     ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_1; RE_CX; REAL_POS];
1450     ALL_TAC] THEN
1451   UNDISCH_TAC `1 < n` THEN SPEC_TAC(`n:num`,`n:num`) THEN
1452   MATCH_MP_TAC INDUCT_COPRIME_STRONG THEN CONJ_TAC THENL
1453    [ALL_TAC; ASM_MESON_TAC[DIRICHLET_CHARACTER_DIVISORSUM_PRIMEPOW_POS]] THEN
1454   MAP_EVERY X_GEN_TAC [`a:num`; `b:num`] THEN STRIP_TAC THEN
1455   MP_TAC(ISPEC `\m:num. Re(c m)` REAL_MULTIPLICATIVE_DIVISORSUM) THEN
1456   REWRITE_TAC[real_multiplicative] THEN ANTS_TAC THENL
1457    [FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP DIRICHLET_CHARACTER_MUL th]) THEN
1458     ASM_MESON_TAC[DIRICHLET_CHARACTER_EQ_1; RE_CX; REAL; CX_MUL];
1459   DISCH_THEN(MP_TAC o SPECL [`a:num`; `b:num`] o CONJUNCT2) THEN
1460   ASM_SIMP_TAC[GSYM RE_VSUM; FINITE_DIVISORS; MULT_EQ_0;
1461                ARITH_RULE `1 < n ==> ~(n = 0)`; REAL_LE_MUL]]);;
1462
1463 let lemma = prove
1464  (`!x n. &0 <= x /\ x <= &1 ==> &1 - &n * x <= (&1 - x) pow n`,
1465   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
1466   INDUCT_TAC THEN REWRITE_TAC[real_pow] THENL [REAL_ARITH_TAC; ALL_TAC] THEN
1467   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(&1 - x) * (&1 - &n * x)` THEN
1468   ASM_SIMP_TAC[REAL_LE_LMUL; REAL_SUB_LE; GSYM REAL_OF_NUM_SUC] THEN
1469   MATCH_MP_TAC(REAL_ARITH
1470    `&0 <= n * x * x ==> &1 - (n + &1) * x <= (&1 - x) * (&1 - n * x)`) THEN
1471   SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_LE_SQUARE]);;
1472
1473 let LFUNCTION_NONZERO_REAL = prove
1474  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) /\ (!n. real(c n))
1475          ==> ~(Lfunction c = Cx(&0))`,
1476   REPEAT STRIP_TAC THEN
1477   MP_TAC(SPECL [`d:num`; `c:num->complex`]
1478    DIRICHLET_CHARACTER_NONPRINCIPAL_NONTRIVIAL) THEN
1479   ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1480   SUBGOAL_THEN
1481    `!z. norm(z) < &1
1482         ==> summable (from 1) (\n. c(n) * z pow n / (Cx(&1) - z pow n))`
1483   MP_TAC THENL
1484    [GEN_TAC THEN DISCH_TAC THEN ASM_CASES_TAC `z = Cx(&0)` THENL
1485      [MATCH_MP_TAC SUMMABLE_FROM_ELSEWHERE THEN EXISTS_TAC `2` THEN
1486       MATCH_MP_TAC SUMMABLE_EQ THEN EXISTS_TAC `\n:num. Cx(&0)` THEN
1487       REWRITE_TAC[GSYM COMPLEX_VEC_0; SUMMABLE_0] THEN
1488       ASM_SIMP_TAC[COMPLEX_VEC_0; COMPLEX_POW_ZERO; IN_FROM;
1489                    ARITH_RULE `2 <= n ==> ~(n = 0)`] THEN
1490       CONV_TAC COMPLEX_RING;
1491       ALL_TAC] THEN
1492     MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
1493     EXISTS_TAC `\n. Cx(&2 * norm(z:complex) pow n)` THEN
1494     REWRITE_TAC[REAL_CX; RE_CX] THEN
1495     SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_POW_LE; NORM_POS_LE] THEN
1496     ASM_SIMP_TAC[CX_MUL; CX_POW; SUMMABLE_COMPLEX_LMUL; COMPLEX_NORM_CX;
1497                  REAL_ABS_NORM; SUMMABLE_GP] THEN
1498     REWRITE_TAC[COMPLEX_NORM_MUL] THEN
1499     FIRST_ASSUM(fun th -> SIMP_TAC[MATCH_MP DIRICHLET_CHARACTER_NORM th]) THEN
1500     ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
1501     ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
1502     SIMP_TAC[REAL_MUL_LZERO; REAL_MUL_LID; REAL_ABS_POS; REAL_LE_MUL] THEN
1503     REWRITE_TAC[TAUT `(p ==> (if q then x else T)) <=> p /\ q ==> x`] THEN
1504     MP_TAC(SPECL [`norm(z:complex)`; `&1 / &2`] REAL_ARCH_POW_INV) THEN
1505     CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_REWRITE_TAC[] THEN
1506     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN DISCH_TAC THEN
1507     X_GEN_TAC `n:num` THEN REWRITE_TAC[GE] THEN STRIP_TAC THEN
1508     REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NORM; REAL_ABS_NUM; REAL_ABS_POW] THEN
1509     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1510     REWRITE_TAC[complex_div; COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN
1511     MATCH_MP_TAC REAL_LE_LMUL THEN SIMP_TAC[REAL_POW_LE; NORM_POS_LE] THEN
1512     REWRITE_TAC[COMPLEX_NORM_INV] THEN
1513     SUBST1_TAC(REAL_ARITH `&2 = inv(&1 / &2)`) THEN
1514     MATCH_MP_TAC REAL_LE_INV2 THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1515     MATCH_MP_TAC(NORM_ARITH
1516      `norm(z) <= norm(w) - h ==> h <= norm(w - z)`) THEN
1517     REWRITE_TAC[COMPLEX_NORM_CX] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1518     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `norm(z:complex) pow N` THEN
1519     ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN REWRITE_TAC[COMPLEX_NORM_POW] THEN
1520     MATCH_MP_TAC REAL_POW_MONO_INV THEN
1521     ASM_SIMP_TAC[REAL_LT_IMP_LE; NORM_POS_LE];
1522     ALL_TAC] THEN
1523   REWRITE_TAC[summable; RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
1524   DISCH_THEN(X_CHOOSE_THEN `f:complex->complex` (LABEL_TAC "+")) THEN
1525   ABBREV_TAC `b = \z n. inv(Cx(&n) * (Cx(&1) - z)) -
1526                         z pow n / (Cx(&1) - z pow n)` THEN
1527   SUBGOAL_THEN
1528    `!z:complex. norm(z) < &1 ==> ((\n. c(n) * b z n) sums --(f z)) (from 1)`
1529    (LABEL_TAC "*")
1530   THENL
1531    [REPEAT STRIP_TAC THEN EXPAND_TAC "b" THEN
1532     REWRITE_TAC[COMPLEX_SUB_LDISTRIB; GSYM COMPLEX_SUB_LZERO] THEN
1533     MATCH_MP_TAC SERIES_SUB THEN ASM_SIMP_TAC[GSYM COMPLEX_SUB_LDISTRIB] THEN
1534     REWRITE_TAC[COMPLEX_INV_MUL; COMPLEX_MUL_ASSOC] THEN
1535     SUBST1_TAC(COMPLEX_RING `Cx(&0) = Cx(&0) * inv(Cx(&1) - z)`) THEN
1536     MATCH_MP_TAC SERIES_COMPLEX_RMUL THEN
1537     MP_TAC(SPECL [`d:num`; `c:num->complex`] LFUNCTION) THEN
1538     ASM_REWRITE_TAC[complex_div];
1539     ALL_TAC] THEN
1540   SUBGOAL_THEN `!z. norm(z) < &1
1541                     ==> ((\n. vsum {d | d divides n} (\d. c d) * z pow n) sums
1542                          f(z)) (from 1)`
1543   (LABEL_TAC "+") THENL
1544    [REPEAT STRIP_TAC THEN REWRITE_TAC[sums; FROM_INTER_NUMSEG] THEN
1545     SIMP_TAC[GSYM VSUM_COMPLEX_RMUL; FINITE_DIVISORS; LE_1] THEN
1546     REWRITE_TAC[VSUM_VSUM_DIVISORS] THEN
1547     REMOVE_THEN "+" (MP_TAC o SPEC `z:complex`) THEN
1548     ASM_REWRITE_TAC[] THEN
1549     SIMP_TAC[VSUM_COMPLEX_LMUL; FINITE_NUMSEG; sums; FROM_INTER_NUMSEG] THEN
1550     MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] LIM_TRANSFORM) THEN
1551     SIMP_TAC[GSYM VSUM_SUB; FINITE_NUMSEG] THEN
1552     REWRITE_TAC[GSYM COMPLEX_SUB_LDISTRIB] THEN
1553     ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[GSYM COMPLEX_POW_POW] THEN
1554     REWRITE_TAC[VSUM_GP; ARITH_RULE `n < 1 <=> n = 0`] THEN
1555     SIMP_TAC[DIV_EQ_0; LE_1] THEN SIMP_TAC[GSYM NOT_LE] THEN
1556     SUBGOAL_THEN `!k. 1 <= k ==> ~(z pow k = Cx(&1))` (fun th -> SIMP_TAC[th])
1557     THENL [ASM_MESON_TAC[COMPLEX_POW_EQ_1; LE_1; REAL_LT_REFL]; ALL_TAC] THEN
1558     REWRITE_TAC[COMPLEX_POW_1; complex_div] THEN
1559     REWRITE_TAC[COMPLEX_RING `(zx * i - (zx - w) * i) = w * i`] THEN
1560     SIMP_TAC[COMPLEX_POW_POW] THEN MATCH_MP_TAC LIM_TRANSFORM_EVENTUALLY THEN
1561     EXISTS_TAC `\x. vsum (1..x)
1562                        (\n. z pow x * c n *
1563                             z pow (n - x MOD n) / (Cx(&1) - z pow n))` THEN
1564     CONJ_TAC THENL
1565      [MATCH_MP_TAC ALWAYS_EVENTUALLY THEN X_GEN_TAC `x:num` THEN
1566       REWRITE_TAC[] THEN MATCH_MP_TAC VSUM_EQ_NUMSEG THEN
1567       X_GEN_TAC `n:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
1568       REWRITE_TAC[complex_div; COMPLEX_INV_MUL; COMPLEX_MUL_ASSOC] THEN
1569       AP_THM_TAC THEN AP_TERM_TAC THEN
1570       ONCE_REWRITE_TAC[COMPLEX_RING `(zx * cn) * zn = cn * zx * zn`] THEN
1571       AP_TERM_TAC THEN REWRITE_TAC[GSYM COMPLEX_POW_ADD] THEN
1572       AP_TERM_TAC THEN REWRITE_TAC[MULT_CLAUSES] THEN
1573       MP_TAC(SPECL [`x:num`; `n:num`] DIVISION) THEN ASM_SIMP_TAC[LE_1] THEN
1574       ARITH_TAC;
1575       ALL_TAC] THEN
1576     REWRITE_TAC[COMPLEX_VEC_0] THEN
1577     MATCH_MP_TAC LIM_NULL_COMPARISON_COMPLEX THEN
1578     EXISTS_TAC `\x. Cx(norm(z) / (&1 - norm z)) * Cx(&x) * z pow x` THEN
1579     CONJ_TAC THENL
1580      [MATCH_MP_TAC ALWAYS_EVENTUALLY THEN X_GEN_TAC `x:num` THEN
1581       REWRITE_TAC[] THEN MATCH_MP_TAC VSUM_NORM_TRIANGLE THEN
1582       REWRITE_TAC[FINITE_NUMSEG; COMPLEX_NORM_MUL; COMPLEX_NORM_CX;
1583                   REAL_ABS_DIV; REAL_ABS_NUM] THEN
1584       GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `a * &x * b = &x * a * b`] THEN
1585       GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV)
1586        [GSYM CARD_NUMSEG_1] THEN
1587       MATCH_MP_TAC SUM_BOUND THEN REWRITE_TAC[FINITE_NUMSEG] THEN
1588       X_GEN_TAC `n:num` THEN REWRITE_TAC[IN_NUMSEG] THEN STRIP_TAC THEN
1589       FIRST_ASSUM(fun t -> SIMP_TAC[MATCH_MP DIRICHLET_CHARACTER_NORM t]) THEN
1590       COND_CASES_TAC THEN
1591       ASM_SIMP_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_LE_DIV; REAL_ABS_POS;
1592                    NORM_POS_LE; REAL_LE_MUL; REAL_MUL_LID; REAL_ABS_NORM] THEN
1593       GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
1594       MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[NORM_POS_LE] THEN
1595       SIMP_TAC[complex_div; real_div; COMPLEX_NORM_MUL; COMPLEX_NORM_INV] THEN
1596       MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[NORM_POS_LE; REAL_LE_INV_EQ] THEN
1597       CONJ_TAC THENL
1598        [REWRITE_TAC[COMPLEX_NORM_POW] THEN
1599         GEN_REWRITE_TAC RAND_CONV [GSYM REAL_POW_1] THEN
1600         MATCH_MP_TAC REAL_POW_MONO_INV THEN
1601         ASM_SIMP_TAC[REAL_LT_IMP_LE; NORM_POS_LE] THEN
1602         MATCH_MP_TAC(ARITH_RULE `m < r ==> 1 <= r - m`) THEN
1603         ASM_SIMP_TAC[DIVISION; LE_1];
1604         ALL_TAC] THEN
1605       MATCH_MP_TAC REAL_LE_INV2 THEN
1606       REWRITE_TAC[REAL_ARITH `&0 < abs(x - a) <=> ~(a = x)`] THEN
1607       CONJ_TAC THENL [ASM_MESON_TAC[REAL_LT_REFL]; ALL_TAC] THEN
1608       MATCH_MP_TAC(NORM_ARITH
1609        `norm(w) = &1 /\ norm(z) < &1 /\ norm(zn) <= norm(z)
1610         ==> abs(&1 - norm(z)) <= norm(w - zn)`) THEN
1611       ASM_REWRITE_TAC[COMPLEX_NORM_NUM; COMPLEX_NORM_POW] THEN
1612       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_POW_1] THEN
1613       MATCH_MP_TAC REAL_POW_MONO_INV THEN
1614       ASM_SIMP_TAC[REAL_LT_IMP_LE; NORM_POS_LE];
1615       ALL_TAC] THEN
1616     MATCH_MP_TAC LIM_NULL_COMPLEX_LMUL THEN ASM_SIMP_TAC[LIM_N_TIMES_POWN];
1617     ALL_TAC] THEN
1618   SUBGOAL_THEN
1619    `~(bounded
1620        { (f:complex->complex)(t) | real t /\ &0 <= Re t /\ norm(t) < &1 })`
1621   MP_TAC THENL
1622    [REWRITE_TAC[BOUNDED_POS] THEN ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
1623     REWRITE_TAC[FORALL_IN_IMAGE; IN_ELIM_THM] THEN
1624     REWRITE_TAC[IMP_CONJ; FORALL_REAL] THEN
1625     REWRITE_TAC[COMPLEX_NORM_CX; RE_CX; IMP_IMP] THEN
1626     REWRITE_TAC[REAL_ARITH `&0 <= x /\ abs x < &1 <=> &0 <= x /\ x < &1`] THEN
1627     DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
1628     FIRST_ASSUM(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC o
1629       MATCH_MP PRIME_FACTOR) THEN
1630     X_CHOOSE_TAC `N:num` (SPEC `&2 * (B + &1)` REAL_ARCH_SIMPLE) THEN
1631     SUBGOAL_THEN `0 < N` ASSUME_TAC THENL
1632      [REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN
1633     ABBREV_TAC `t = &1 - inv(&(p EXP N)) / &2` THEN
1634     SUBGOAL_THEN `&0 <= t /\ t < &1` STRIP_ASSUME_TAC THENL
1635      [EXPAND_TAC "t" THEN
1636       MATCH_MP_TAC(REAL_ARITH
1637        `&0 < y /\ y <= &1 ==> &0 <= &1 - y / &2 /\ &1 - y / &2 < &1`) THEN
1638       ASM_SIMP_TAC[REAL_INV_LE_1; REAL_LT_INV_EQ; REAL_OF_NUM_LE;
1639                            REAL_OF_NUM_LT; LE_1; EXP_EQ_0; PRIME_IMP_NZ];
1640       ALL_TAC] THEN
1641     REMOVE_THEN "+" (MP_TAC o SPEC `Cx t`) THEN
1642     REWRITE_TAC[COMPLEX_NORM_CX; NOT_IMP] THEN
1643     CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
1644     FIRST_X_ASSUM(MP_TAC o SPEC `t:real`) THEN ASM_REWRITE_TAC[] THEN
1645     DISCH_TAC THEN REWRITE_TAC[SERIES_FROM; LIM_SEQUENTIALLY] THEN
1646     DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[REAL_LT_01] THEN
1647     DISCH_THEN(X_CHOOSE_THEN `M:num` MP_TAC) THEN
1648     SUBGOAL_THEN `?n. M <= n /\ 1 <= n /\ p EXP N <= n` STRIP_ASSUME_TAC THENL
1649      [EXISTS_TAC `p EXP N + M + 1` THEN ARITH_TAC; ALL_TAC] THEN
1650     DISCH_THEN(MP_TAC o SPEC `n:num`) THEN ASM_REWRITE_TAC[] THEN
1651     UNDISCH_TAC `norm (f (Cx t):complex) <= B` THEN
1652     MATCH_MP_TAC(NORM_ARITH
1653      `B + &1 <= norm(x) ==> norm(y) <= B ==> ~(dist(x,y) < &1)`) THEN
1654     MATCH_MP_TAC(REAL_ARITH
1655      `a <= Re z /\ abs(Re z) <= norm z ==> a <= norm z`) THEN
1656     REWRITE_TAC[COMPLEX_NORM_GE_RE_IM] THEN
1657     SIMP_TAC[RE_VSUM; FINITE_NUMSEG; RE_MUL_CX; GSYM CX_POW] THEN
1658     MATCH_MP_TAC REAL_LE_TRANS THEN
1659     EXISTS_TAC `sum (IMAGE (\k. p EXP k) (0..N))
1660                     (\x. Re (vsum {d | d divides x} (\d. c d)) * t pow x)` THEN
1661     CONJ_TAC THENL
1662      [ALL_TAC;
1663       MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN
1664       REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG; IN_DIFF; SUBSET; IN_ELIM_THM;
1665                   FORALL_IN_IMAGE] THEN
1666       MP_TAC(SPECL [`d:num`; `c:num->complex`]
1667         DIRICHLET_CHARACTER_DIVISORSUM_POS) THEN
1668       ASM_SIMP_TAC[REAL_POW_LE; REAL_LE_MUL; LE_1; ETA_AX] THEN
1669       DISCH_THEN(K ALL_TAC) THEN
1670       REWRITE_TAC[ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
1671       ASM_SIMP_TAC[EXP_EQ_0; PRIME_IMP_NZ] THEN
1672       X_GEN_TAC `k:num` THEN STRIP_TAC THEN
1673       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `p EXP N` THEN
1674       ASM_SIMP_TAC[LE_EXP; PRIME_IMP_NZ]] THEN
1675     W(MP_TAC o PART_MATCH (lhs o rand) SUM_IMAGE o rand o snd) THEN
1676     ANTS_TAC THENL
1677      [REWRITE_TAC[EQ_EXP] THEN ASM_MESON_TAC[PRIME_0; PRIME_1]; ALL_TAC] THEN
1678     DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[o_DEF] THEN
1679     MATCH_MP_TAC REAL_LE_TRANS THEN
1680     EXISTS_TAC `sum (0..N) (\k. &1 * &1 / &2)` THEN CONJ_TAC THENL
1681      [REWRITE_TAC[SUM_CONST_NUMSEG; SUB_0; GSYM REAL_OF_NUM_ADD] THEN
1682       ASM_REAL_ARITH_TAC;
1683       ALL_TAC] THEN
1684     MATCH_MP_TAC SUM_LE_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
1685     REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
1686     CONV_TAC REAL_RAT_REDUCE_CONV THEN CONJ_TAC THENL
1687      [MP_TAC(SPECL [`d:num`; `c:num->complex`; `p:num`; `k:num`]
1688                 DIRICHLET_CHARACTER_DIVISORSUM_EQ_1) THEN
1689       ASM_SIMP_TAC[ETA_AX; RE_CX; REAL_LE_REFL];
1690       ALL_TAC] THEN
1691     MP_TAC(ISPECL [`inv(&(p EXP N)) / &2`; `p EXP k`] lemma) THEN
1692     ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
1693      [REWRITE_TAC[real_div; GSYM REAL_INV_MUL; REAL_OF_NUM_MUL] THEN
1694       REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS] THEN
1695       MATCH_MP_TAC REAL_INV_LE_1 THEN
1696       REWRITE_TAC[REAL_OF_NUM_LE; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
1697       ASM_SIMP_TAC[EXP_EQ_0; MULT_EQ_0; ARITH; PRIME_IMP_NZ];
1698       ALL_TAC] THEN
1699     MATCH_MP_TAC(REAL_ARITH `b <= a ==> a <= x ==> b <= x`) THEN
1700     MATCH_MP_TAC(REAL_ARITH `x * y <= &1 ==> &1 / &2 <= &1 - x * y / &2`) THEN
1701     ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; LE_1;
1702                  EXP_EQ_0; PRIME_IMP_NZ] THEN
1703     ASM_REWRITE_TAC[REAL_MUL_LID; REAL_OF_NUM_LE; LE_EXP] THEN
1704     ASM_MESON_TAC[PRIME_0];
1705     ALL_TAC] THEN
1706   MP_TAC(SPECL [`d:num`; `c:num->complex`]
1707     BOUNDED_LFUNCTION_PARTIAL_SUMS) THEN
1708   ASM_REWRITE_TAC[] THEN
1709   DISCH_THEN(MP_TAC o MATCH_MP BOUNDED_PARTIAL_SUMS) THEN
1710   REWRITE_TAC[BOUNDED_POS] THEN ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
1711   REWRITE_TAC[FORALL_IN_IMAGE] THEN
1712   SIMP_TAC[IN_ELIM_THM; IN_UNIV; LEFT_IMP_EXISTS_THM] THEN
1713   REWRITE_TAC[MESON[] `(!x a b. x = f a b ==> p a b) <=> (!a b. p a b)`] THEN
1714   X_GEN_TAC `B:real` THEN STRIP_TAC THEN EXISTS_TAC `&2 * B` THEN
1715   ASM_SIMP_TAC[REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
1716   X_GEN_TAC `z:complex` THEN STRIP_TAC THEN
1717   ONCE_REWRITE_TAC[GSYM NORM_NEG] THEN
1718   MATCH_MP_TAC(ISPEC `sequentially` LIM_NORM_UBOUND) THEN
1719   EXISTS_TAC
1720    `\n. vsum(from 1 INTER (0..n)) (\k. c k * b (z:complex) k :complex)` THEN
1721   ASM_SIMP_TAC[TRIVIAL_LIMIT_SEQUENTIALLY; GSYM sums] THEN
1722   REWRITE_TAC[FROM_INTER_NUMSEG] THEN
1723   MATCH_MP_TAC ALWAYS_EVENTUALLY THEN X_GEN_TAC `n:num` THEN
1724   MP_TAC(ISPECL [`c:num->complex`; `(b:complex->num->complex) z`;
1725                  `B:real`; `1`] SERIES_DIRICHLET_COMPLEX_VERY_EXPLICIT) THEN
1726   ASM_REWRITE_TAC[LE_REFL] THEN ANTS_TAC THENL
1727    [ALL_TAC;
1728     DISCH_THEN(MP_TAC o SPEC `1`) THEN
1729     SUBGOAL_THEN `(b:complex->num->complex) z 1 = Cx(&1)` SUBST1_TAC THENL
1730      [EXPAND_TAC "b" THEN
1731       REWRITE_TAC[COMPLEX_POW_1; COMPLEX_INV_MUL; complex_div] THEN
1732       REWRITE_TAC[GSYM COMPLEX_SUB_RDISTRIB; COMPLEX_INV_1] THEN
1733       MATCH_MP_TAC COMPLEX_MUL_RINV THEN REWRITE_TAC[COMPLEX_SUB_0] THEN
1734       DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
1735       UNDISCH_TAC `norm(Cx(&1)) < &1` THEN
1736       REWRITE_TAC[COMPLEX_NORM_CX; REAL_LT_REFL; REAL_ABS_NUM];
1737       ALL_TAC] THEN
1738     REWRITE_TAC[COMPLEX_NORM_NUM; REAL_MUL_RID] THEN
1739     DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[LE_REFL]] THEN
1740   FIRST_X_ASSUM(X_CHOOSE_THEN `t:real` SUBST_ALL_TAC o
1741                 GEN_REWRITE_RULE I [REAL_EXISTS]) THEN
1742   RULE_ASSUM_TAC(REWRITE_RULE[RE_CX; COMPLEX_NORM_CX]) THEN
1743   SUBGOAL_THEN `!n. &0 < sum(0..n) (\m. t pow m)` ASSUME_TAC THENL
1744    [GEN_TAC THEN SIMP_TAC[LE_0; SUM_CLAUSES_LEFT; real_pow] THEN
1745     MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> &0 < &1 + x`) THEN
1746     ASM_SIMP_TAC[SUM_POS_LE_NUMSEG; REAL_POW_LE];
1747     ALL_TAC] THEN
1748   CONJ_TAC THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN EXPAND_TAC "b" THEN
1749   REWRITE_TAC[GSYM CX_SUB; GSYM CX_POW; GSYM CX_DIV; GSYM CX_MUL;
1750               GSYM CX_INV; REAL_CX; RE_CX]
1751   THENL
1752    [ASM_SIMP_TAC[REAL_SUB_POW_L1; REAL_SUB_LE] THEN
1753     ASM_REWRITE_TAC[real_div; REAL_INV_MUL] THEN
1754     ASM_SIMP_TAC[GSYM real_div; REAL_LE_RDIV_EQ; REAL_LT_MUL; REAL_OF_NUM_LT;
1755                  LE_1; REAL_ARITH `abs t < &1 ==> &0 < &1 - t`] THEN
1756     ASM_SIMP_TAC[real_div; REAL_FIELD
1757      `abs(t) < &1 ==> (x * inv(&1 - t) * y) * (&1 - t) = x * y`] THEN
1758     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
1759     ASM_SIMP_TAC[GSYM real_div; REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; LE_1] THEN
1760     ONCE_REWRITE_TAC[REAL_ARITH `x / y * &n = (&n * x) / y`] THEN
1761     ASM_SIMP_TAC[REAL_LE_LDIV_EQ] THEN
1762     MATCH_MP_TAC REAL_LE_TRANS THEN
1763     EXISTS_TAC `sum(0..n-1) (\m. t pow n)` THEN CONJ_TAC THENL
1764      [ASM_SIMP_TAC[SUM_CONST_NUMSEG; ARITH_RULE `1 <= n ==> n - 1 + 1 = n`;
1765                    SUB_0; REAL_LE_REFL];
1766       REWRITE_TAC[REAL_MUL_LID] THEN MATCH_MP_TAC SUM_LE_NUMSEG THEN
1767       GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[] THEN
1768       MATCH_MP_TAC REAL_POW_MONO_INV THEN REPEAT CONJ_TAC THEN
1769       TRY ASM_REAL_ARITH_TAC THEN ASM_ARITH_TAC];
1770     ALL_TAC] THEN
1771   ASM_SIMP_TAC[REAL_SUB_POW_L1; ARITH_RULE `1 <= n + 1`] THEN
1772   REWRITE_TAC[ADD_SUB; REAL_INV_MUL; real_div] THEN
1773   REWRITE_TAC[REAL_ARITH `x * t - y * t * z <= u * t - v * t * w <=>
1774                           t * (v * w - y * z) <= t * (u - x)`] THEN
1775   MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_LE_INV_EQ] THEN
1776   CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
1777   ASM_SIMP_TAC[GSYM real_div; REAL_FIELD
1778    `&0 < y /\ &0 < z ==> x / y - w / z = (x * z - w * y) / (y * z)`] THEN
1779   SUBGOAL_THEN `t pow n * sum (0..n) (\m. t pow m) -
1780                 t pow (n + 1) * sum (0..n - 1) (\m. t pow m) = t pow n`
1781   SUBST1_TAC THENL
1782    [REWRITE_TAC[GSYM SUM_LMUL; GSYM REAL_POW_ADD] THEN
1783     ONCE_REWRITE_TAC[ARITH_RULE `(n + 1) + x = n + x + 1`] THEN
1784     REWRITE_TAC[GSYM(SPEC `1` SUM_OFFSET); SUB_ADD; ADD_CLAUSES] THEN
1785     SIMP_TAC[SUM_CLAUSES_LEFT; LE_0; GSYM SUM_LMUL; ADD_CLAUSES] THEN
1786     ASM_SIMP_TAC[SUB_ADD; REAL_POW_ADD] THEN
1787     REWRITE_TAC[REAL_ARITH `(x + y) - y:real = x`];
1788     ALL_TAC] THEN
1789   ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LT_MUL; GSYM REAL_OF_NUM_ADD;
1790                REAL_OF_NUM_LE;
1791        REAL_FIELD `&1 <= n ==> inv(n) - inv(n + &1) = inv(n * (n + &1))`] THEN
1792   MATCH_MP_TAC REAL_POW_LE2_REV THEN EXISTS_TAC `2` THEN
1793   REWRITE_TAC[ARITH] THEN CONJ_TAC THENL
1794    [REPEAT(MATCH_MP_TAC REAL_LE_MUL THEN
1795            CONJ_TAC THEN REWRITE_TAC[REAL_LE_INV_EQ]) THEN
1796     ASM_SIMP_TAC[REAL_POW_LE; SUM_POS_LE_NUMSEG] THEN REAL_ARITH_TAC;
1797     ALL_TAC] THEN
1798   MP_TAC(SPECL [`n:num`; `t:real`] AGM_SPECIAL) THEN
1799   MP_TAC(SPECL [`n - 1`; `t:real`] AGM_SPECIAL) THEN
1800   ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB; REAL_SUB_ADD] THEN
1801   REWRITE_TAC[IMP_IMP] THEN
1802   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
1803   ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_POW_LT; REAL_OF_NUM_LT;
1804                LE_1; REAL_ARITH `&0 < &n + &1`] THEN
1805   DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE
1806    [TAUT `a /\ b /\ c /\ d ==> e <=> b /\ d ==> a /\ c ==> e`]
1807    REAL_LE_MUL2)) THEN
1808   ASM_SIMP_TAC[REAL_POW_LE; REAL_LE_MUL; REAL_ARITH `&0 <= &n + &1`] THEN
1809   MATCH_MP_TAC(REAL_ARITH `x = y /\ a <= b ==> b <= x ==> a <= y`) THEN
1810   CONJ_TAC THENL
1811    [REWRITE_TAC[REAL_POW_2; real_div; REAL_INV_MUL; REAL_POW_MUL] THEN
1812     REWRITE_TAC[REAL_MUL_AC];
1813     REWRITE_TAC[GSYM REAL_POW_ADD; REAL_POW_POW] THEN
1814     MATCH_MP_TAC REAL_POW_MONO_INV THEN ASM_REWRITE_TAC[] THEN
1815     CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ARITH_TAC]]);;
1816
1817 (* ------------------------------------------------------------------------- *)
1818 (* Deduce nonvanishing of all the nonprincipal characters.                   *)
1819 (* ------------------------------------------------------------------------- *)
1820
1821 let BOUNDED_DIFF_LOGMUL = prove
1822  (`!f a. bounded {f x - Cx(log(&x)) * a | x IN (:num)}
1823          ==> (!x. &0 <= Re(f x)) ==> &0 <= Re a`,
1824   REPEAT GEN_TAC THEN
1825   REWRITE_TAC[BOUNDED_POS; SIMPLE_IMAGE; FORALL_IN_IMAGE; IN_UNIV] THEN
1826   DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN DISCH_TAC THEN
1827   ONCE_REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN
1828   MP_TAC(ISPEC `exp((B + &1) / --(Re a))` REAL_ARCH_SIMPLE) THEN
1829   DISCH_THEN(X_CHOOSE_TAC `n:num`) THEN
1830   SUBGOAL_THEN `abs(Re(f n - Cx(log(&n)) * a)) <= B` MP_TAC THENL
1831    [ASM_MESON_TAC[COMPLEX_NORM_GE_RE_IM; REAL_LE_TRANS]; ALL_TAC] THEN
1832   REWRITE_TAC[RE_SUB; RE_MUL_CX; REAL_NOT_LE] THEN
1833   MATCH_MP_TAC(REAL_ARITH
1834    `B < l * --a /\ &0 <= f ==> B < abs(f - l * a)`) THEN
1835   ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ; REAL_NEG_GT0] THEN
1836   MATCH_MP_TAC REAL_LTE_TRANS THEN
1837   EXISTS_TAC `log(exp((B + &1) / --Re a))` THEN CONJ_TAC THENL
1838    [ASM_SIMP_TAC[LOG_EXP; REAL_NEG_GT0; REAL_LT_DIV2_EQ] THEN REAL_ARITH_TAC;
1839     MATCH_MP_TAC LOG_MONO_LE_IMP THEN ASM_REWRITE_TAC[REAL_EXP_POS_LT]]);;
1840
1841 let LFUNCTION_NONZERO_NONPRINCIPAL = prove
1842  (`!d c. dirichlet_character d c /\ ~(c = chi_0 d)
1843          ==> ~(Lfunction c = Cx(&0))`,
1844   let lemma = prove
1845    (`{a,b,c} SUBSET s
1846      ==> FINITE s
1847          ==> !f. sum s f = sum (s DIFF {a,b,c}) f + sum {a,b,c} f`,
1848     REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN
1849     MATCH_MP_TAC SUM_UNION_EQ THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[]) in
1850   GEN_TAC THEN ASM_CASES_TAC `d = 0` THENL
1851    [ASM_MESON_TAC[DIRICHLET_CHARACTER_0]; ALL_TAC] THEN
1852   MP_TAC(ISPECL
1853    [`\x c. vsum(1..x) (\n. c n * Cx(mangoldt n / &n)) -
1854            Cx(log(&x)) *
1855            (if c = chi_0 d then Cx(&1)
1856             else if Lfunction c = Cx(&0) then --Cx(&1)
1857             else Cx(&0))`;
1858     `(:num)`;
1859     `{c | dirichlet_character d c}`]
1860    BOUNDED_SUMS_IMAGES) THEN
1861   ANTS_TAC THENL
1862    [REWRITE_TAC[FINITE_DIRICHLET_CHARACTERS; IN_ELIM_THM] THEN
1863     X_GEN_TAC `c:num->complex` THEN
1864     ASM_CASES_TAC `c = chi_0 d` THEN
1865     ASM_SIMP_TAC[COMPLEX_MUL_RID; BOUNDED_DIRICHLET_MANGOLDT_PRINCIPAL;
1866                  LE_1] THEN
1867     ASM_CASES_TAC `Lfunction c = Cx(&0)` THEN
1868     ASM_REWRITE_TAC[COMPLEX_SUB_RZERO; COMPLEX_MUL_RNEG; COMPLEX_MUL_RZERO;
1869                     COMPLEX_MUL_RID; COMPLEX_SUB_RNEG] THEN
1870     ASM_MESON_TAC[BOUNDED_DIRICHLET_MANGOLDT_ZERO;
1871                   BOUNDED_DIRICHLET_MANGOLDT_NONZERO; LE_1];
1872     ALL_TAC] THEN
1873   SIMP_TAC[VSUM_SUB; FINITE_DIRICHLET_CHARACTERS; VSUM_COMPLEX_LMUL] THEN
1874   DISCH_THEN(MP_TAC o MATCH_MP BOUNDED_DIFF_LOGMUL) THEN
1875   REWRITE_TAC[IN_UNIV] THEN ANTS_TAC THENL
1876    [X_GEN_TAC `x:num` THEN
1877     W(MP_TAC o PART_MATCH (lhs o rand) VSUM_SWAP o funpow 2 rand o snd) THEN
1878     REWRITE_TAC[FINITE_DIRICHLET_CHARACTERS; FINITE_NUMSEG] THEN
1879     DISCH_THEN SUBST1_TAC THEN
1880     SIMP_TAC[VSUM_COMPLEX_RMUL; FINITE_DIRICHLET_CHARACTERS] THEN
1881     SIMP_TAC[RE_VSUM; FINITE_NUMSEG; RE_MUL_CX] THEN
1882     MATCH_MP_TAC SUM_POS_LE_NUMSEG THEN
1883     X_GEN_TAC `n:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
1884     MATCH_MP_TAC REAL_LE_MUL THEN
1885     SIMP_TAC[DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_POS;
1886              REAL_LE_DIV; REAL_POS; MANGOLDT_POS_LE];
1887     ALL_TAC] THEN
1888   SIMP_TAC[RE_VSUM; FINITE_DIRICHLET_CHARACTERS] THEN
1889   REPLICATE_TAC 2 (ONCE_REWRITE_TAC[COND_RAND]) THEN
1890   REWRITE_TAC[RE_NEG; RE_CX] THEN DISCH_TAC THEN
1891   X_GEN_TAC `c:num->complex` THEN STRIP_TAC THEN STRIP_TAC THEN
1892   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM REAL_NOT_LT]) THEN
1893   REWRITE_TAC[] THEN
1894   SUBGOAL_THEN
1895    `{chi_0 d,c,(\n. cnj(c n))} SUBSET {c | dirichlet_character d c}`
1896   MP_TAC THENL
1897    [REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
1898     REPEAT STRIP_TAC THEN
1899     ASM_SIMP_TAC[DIRICHLET_CHARACTER_CHI_0; DIRICHLET_CHARACTER_CNJ];
1900     ALL_TAC] THEN
1901   DISCH_THEN(MP_TAC o MATCH_MP lemma) THEN
1902   REWRITE_TAC[FINITE_DIRICHLET_CHARACTERS] THEN
1903   DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
1904   MATCH_MP_TAC(REAL_ARITH `s <= &0 /\ t < &0 ==> s + t < &0`) THEN
1905   CONJ_TAC THENL
1906    [MATCH_MP_TAC(REAL_ARITH `&0 <= --x ==> x <= &0`) THEN
1907     REWRITE_TAC[GSYM SUM_NEG] THEN MATCH_MP_TAC SUM_POS_LE THEN
1908     SIMP_TAC[FINITE_DIRICHLET_CHARACTERS; FINITE_DIFF] THEN
1909     SIMP_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
1910     REAL_ARITH_TAC;
1911     ALL_TAC] THEN
1912   ASM_SIMP_TAC[SUM_CLAUSES; FINITE_INSERT; IN_INSERT; NOT_IN_EMPTY;
1913                FINITE_RULES] THEN
1914   SUBGOAL_THEN `~(chi_0 d = (\n. cnj (c n)))` ASSUME_TAC THENL
1915    [DISCH_THEN(MP_TAC o AP_TERM `(\c n:num. cnj(c n))`) THEN
1916     REWRITE_TAC[CNJ_CNJ; FUN_EQ_THM; CNJ_CHI_0] THEN
1917     ASM_REWRITE_TAC[GSYM FUN_EQ_THM; ETA_AX];
1918     ALL_TAC] THEN
1919   SUBGOAL_THEN `~(c = \n:num. cnj(c n))` ASSUME_TAC THENL
1920    [ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1921     REWRITE_TAC[GSYM REAL_CNJ; FUN_EQ_THM] THEN
1922     ASM_MESON_TAC[LFUNCTION_NONZERO_REAL];
1923     ALL_TAC] THEN
1924   MP_TAC(SPECL [`d:num`; `c:num->complex`] LFUNCTION_CNJ) THEN
1925   ASM_SIMP_TAC[CNJ_EQ_CX] THEN REAL_ARITH_TAC);;
1926
1927 (* ------------------------------------------------------------------------- *)
1928 (* Hence derive our boundedness result for all nonprincipal characters.      *)
1929 (* ------------------------------------------------------------------------- *)
1930
1931 let BOUNDED_DIRICHLET_MANGOLDT_NONPRINCIPAL = prove
1932  (`!d c.
1933       dirichlet_character d c /\ ~(c = chi_0 d)
1934       ==> bounded { vsum(1..x) (\n. c n * Cx(mangoldt n / &n)) | x IN (:num)}`,
1935   REPEAT STRIP_TAC THEN MATCH_MP_TAC BOUNDED_DIRICHLET_MANGOLDT_NONZERO THEN
1936   EXISTS_TAC `d:num` THEN
1937   ASM_MESON_TAC[LFUNCTION_NONZERO_NONPRINCIPAL]);;
1938
1939 (* ------------------------------------------------------------------------- *)
1940 (* Hence the main sum result.                                                *)
1941 (* ------------------------------------------------------------------------- *)
1942
1943 let BOUNDED_SUM_OVER_DIRICHLET_CHARACTERS = prove
1944  (`!d l. 1 <= d /\ coprime(l,d)
1945          ==> bounded { vsum {c | dirichlet_character d c}
1946                             (\c. c(l) *
1947                                  vsum(1..x) (\n. c n * Cx (mangoldt n / &n))) -
1948                        Cx(log(&x)) | x IN (:num)}`,
1949   REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN
1950   SUBGOAL_THEN `!x. Cx(log(&x)) =
1951                         vsum {c | dirichlet_character d c}
1952                              (\c. if c = chi_0 d then Cx(log(&x)) else Cx(&0))`
1953    (fun th -> ONCE_REWRITE_TAC[th])
1954   THENL
1955    [SIMP_TAC[VSUM_DELTA; GSYM COMPLEX_VEC_0] THEN
1956     REWRITE_TAC[IN_ELIM_THM; DIRICHLET_CHARACTER_CHI_0];
1957     ALL_TAC] THEN
1958   SIMP_TAC[GSYM VSUM_SUB; FINITE_DIRICHLET_CHARACTERS] THEN
1959   MATCH_MP_TAC BOUNDED_SUMS_IMAGES THEN
1960   REWRITE_TAC[FINITE_DIRICHLET_CHARACTERS; IN_ELIM_THM] THEN
1961   X_GEN_TAC `c:num->complex` THEN DISCH_TAC THEN
1962   ASM_CASES_TAC `c = chi_0 d` THEN ASM_REWRITE_TAC[] THENL
1963    [FIRST_ASSUM(MP_TAC o MATCH_MP BOUNDED_DIRICHLET_MANGOLDT_PRINCIPAL) THEN
1964     ASM_REWRITE_TAC[chi_0; COMPLEX_MUL_LID];
1965     REWRITE_TAC[COMPLEX_SUB_RZERO] THEN
1966     MP_TAC(SPECL [`d:num`; `c:num->complex`]
1967       BOUNDED_DIRICHLET_MANGOLDT_NONPRINCIPAL) THEN
1968     ASM_REWRITE_TAC[] THEN
1969     REWRITE_TAC[BOUNDED_POS] THEN MATCH_MP_TAC MONO_EXISTS THEN
1970     ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
1971     REWRITE_TAC[FORALL_IN_IMAGE; IN_ELIM_THM; IN_UNIV] THEN
1972     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[COMPLEX_NORM_MUL] THEN
1973     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
1974     MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[NORM_POS_LE] THEN
1975     FIRST_ASSUM(fun th -> SIMP_TAC[MATCH_MP DIRICHLET_CHARACTER_NORM th]) THEN
1976     REAL_ARITH_TAC]);;
1977
1978 let DIRICHLET_MANGOLDT = prove
1979  (`!d k. 1 <= d /\ coprime(k,d)
1980          ==> bounded { Cx(&(phi d)) * vsum {n | n IN 1..x /\ (n == k) (mod d)}
1981                                            (\n. Cx(mangoldt n / &n)) -
1982                        Cx(log(&x)) | x IN (:num)}`,
1983   REPEAT STRIP_TAC THEN
1984   SUBGOAL_THEN `?l. (k * l == 1) (mod d)` CHOOSE_TAC THENL
1985    [ASM_MESON_TAC[CONG_SOLVE]; ALL_TAC] THEN
1986   MP_TAC(SPECL [`d:num`; `l:num`] BOUNDED_SUM_OVER_DIRICHLET_CHARACTERS) THEN
1987   ANTS_TAC THENL
1988    [ASM_REWRITE_TAC[] THEN UNDISCH_TAC `(k * l == 1) (mod d)` THEN
1989     CONV_TAC NUMBER_RULE;
1990     ALL_TAC] THEN
1991   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
1992   MATCH_MP_TAC(SET_RULE
1993    `(!x. x IN s ==> f x = g x) ==> {f x | x IN s} = {g x | x IN s}`) THEN
1994   X_GEN_TAC `x:num` THEN DISCH_THEN(K ALL_TAC) THEN
1995   AP_THM_TAC THEN AP_TERM_TAC THEN
1996   SIMP_TAC[GSYM VSUM_COMPLEX_LMUL; FINITE_NUMSEG; FINITE_RESTRICT] THEN
1997   SIMP_TAC[VSUM_RESTRICT_SET; FINITE_NUMSEG] THEN
1998   W(MP_TAC o PART_MATCH (lhs o rand) VSUM_SWAP o lhand o snd) THEN
1999   REWRITE_TAC[FINITE_DIRICHLET_CHARACTERS; FINITE_NUMSEG] THEN
2000   DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC VSUM_EQ_NUMSEG THEN
2001   X_GEN_TAC `n:num` THEN DISCH_TAC THEN REWRITE_TAC[COMPLEX_MUL_ASSOC] THEN
2002   MP_TAC(GSYM(SPEC `d:num` DIRICHLET_CHARACTER_MUL)) THEN
2003   SIMP_TAC[IN_ELIM_THM] THEN DISCH_THEN(K ALL_TAC) THEN
2004   SIMP_TAC[VSUM_COMPLEX_RMUL; FINITE_DIRICHLET_CHARACTERS] THEN
2005   ASM_SIMP_TAC[DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS] THEN
2006   SUBGOAL_THEN `(l * n == 1) (mod d) <=> (n == k) (mod d)` SUBST1_TAC THENL
2007    [UNDISCH_TAC `(k * l == 1) (mod d)` THEN CONV_TAC NUMBER_RULE;
2008     COND_CASES_TAC THEN ASM_REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_VEC_0]]);;
2009
2010 let DIRICHLET_MANGOLDT_EXPLICIT = prove
2011  (`!d k. 1 <= d /\ coprime (k,d)
2012          ==> ?B. &0 < B /\
2013                  !x. abs(sum {n | n IN 1..x /\ (n == k) (mod d)}
2014                              (\n. mangoldt n / &n) -
2015                          log(&x) / &(phi d)) <= B`,
2016   REPEAT GEN_TAC THEN DISCH_TAC THEN
2017   FIRST_ASSUM(MP_TAC o MATCH_MP DIRICHLET_MANGOLDT) THEN
2018   REWRITE_TAC[BOUNDED_POS] THEN
2019   SIMP_TAC[SIMPLE_IMAGE; FORALL_IN_IMAGE; IN_UNIV] THEN
2020   SIMP_TAC[VSUM_CX; FINITE_RESTRICT; FINITE_NUMSEG;
2021            GSYM CX_SUB; GSYM CX_MUL; COMPLEX_NORM_CX] THEN
2022   DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
2023   EXISTS_TAC `B / &(phi d)` THEN
2024   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; LE_1; PHI_LOWERBOUND_1_STRONG;
2025                REAL_LE_RDIV_EQ] THEN
2026   X_GEN_TAC `n:num` THEN
2027   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_ABS_NUM] THEN
2028   REWRITE_TAC[GSYM REAL_ABS_MUL] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
2029   ASM_SIMP_TAC[REAL_SUB_LDISTRIB; REAL_DIV_LMUL;
2030                LE_1; PHI_LOWERBOUND_1_STRONG; REAL_OF_NUM_EQ]);;
2031
2032 let DIRICHLET_STRONG = prove
2033  (`!d k. 1 <= d /\ coprime(k,d)
2034          ==> ?B. &0 < B /\
2035                  !x. abs(sum {p | p IN 1..x /\ prime p /\ (p == k) (mod d)}
2036                              (\p. log(&p) / &p) -
2037                          log(&x) / &(phi d)) <= B`,
2038   REPEAT GEN_TAC THEN DISCH_TAC THEN
2039   FIRST_ASSUM(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC o
2040     MATCH_MP DIRICHLET_MANGOLDT_EXPLICIT) THEN
2041   EXISTS_TAC `B + &3` THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
2042   X_GEN_TAC `x:num` THEN FIRST_X_ASSUM(MP_TAC o SPEC `x:num`) THEN
2043   MATCH_MP_TAC(REAL_ARITH
2044    `abs(x - y) <= a ==> abs(x - z) <= b ==> abs(y - z) <= b + a`) THEN
2045   MP_TAC(SPECL [`x:num`; `{n | n IN 1..x /\ (n == k) (mod d)}`]
2046                MERTENS_MANGOLDT_VERSUS_LOG) THEN
2047   SIMP_TAC[SUBSET; IN_ELIM_THM] THEN REWRITE_TAC[CONJ_ACI]);;
2048
2049 (* ------------------------------------------------------------------------- *)
2050 (* Ignore the density details and prove the main result.                     *)
2051 (* ------------------------------------------------------------------------- *)
2052
2053 let DIRICHLET = prove
2054  (`!d k. 1 <= d /\ coprime(k,d)
2055          ==> INFINITE {p | prime p /\ (p == k) (mod d)}`,
2056   REWRITE_TAC[INFINITE] THEN REPEAT STRIP_TAC THEN
2057   FIRST_ASSUM(MP_TAC o SPEC `\n:num. n` o MATCH_MP UPPER_BOUND_FINITE_SET) THEN
2058   REWRITE_TAC[IN_ELIM_THM; NOT_EXISTS_THM] THEN X_GEN_TAC `n:num` THEN
2059   DISCH_TAC THEN MP_TAC(SPECL [`d:num`; `k:num`] DIRICHLET_STRONG) THEN
2060   ASM_REWRITE_TAC[] THEN
2061   DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
2062   MP_TAC(SPEC
2063    `max (exp(&(phi d) *
2064             (&1 + B + sum {p | p IN 1..n /\ prime p /\ (p == k) (mod d)}
2065                           (\p. log(&p) / &p))))
2066         (max (&n) (&1))`
2067    REAL_ARCH_SIMPLE) THEN
2068   REWRITE_TAC[NOT_EXISTS_THM; REAL_MAX_LE; REAL_OF_NUM_LE] THEN
2069   X_GEN_TAC `m:num` THEN STRIP_TAC THEN
2070   FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
2071   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2072    `abs(x - y) <= b ==> y < &1 + b + x`)) THEN
2073   ASM_SIMP_TAC[REAL_NOT_LT; REAL_LE_RDIV_EQ; PHI_LOWERBOUND_1_STRONG;
2074                REAL_OF_NUM_LT; LE_1] THEN
2075   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
2076   ONCE_REWRITE_TAC[GSYM REAL_EXP_MONO_LE] THEN
2077   ASM_SIMP_TAC[EXP_LOG; REAL_OF_NUM_LT; LE_1] THEN
2078   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
2079    `x <= a ==> x = y ==> y <= a`)) THEN
2080   REPLICATE_TAC 4 AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2081   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_NUMSEG] THEN
2082   GEN_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[] THEN ASM_ARITH_TAC);;