(* ========================================================================= *) (* Dirichlet's theorem. *) (* ========================================================================= *) needs "Library/products.ml";; needs "Library/agm.ml";; needs "Multivariate/transcendentals.ml";; needs "Library/pocklington.ml";; needs "Library/multiplicative.ml";; needs "Examples/mangoldt.ml";; prioritize_real();; prioritize_complex();; (* ------------------------------------------------------------------------- *) (* Rearranging a certain kind of double sum. *) (* ------------------------------------------------------------------------- *)(* ------------------------------------------------------------------------- *) (* Useful approximation lemmas. *) (* ------------------------------------------------------------------------- *)let VSUM_VSUM_DIVISORS =prove (`!f x. vsum (1..x) (\n. vsum {d | d divides n} (f n)) = vsum (1..x) (\n. vsum (1..(x DIV n)) (\k. f (k * n) n))`,let REAL_EXP_1_LE_4 =prove (`exp(&1) <= &4`,(* ------------------------------------------------------------------------- *) (* An ad-hoc fact about complex n'th roots. *) (* ------------------------------------------------------------------------- *)let DECREASING_LOG_OVER_N =prove (`!n. 4 <= n ==> log(&n + &1) / (&n + &1) <= log(&n) / &n`,(* ------------------------------------------------------------------------- *) (* Definition of a Dirichlet character mod d. *) (* ------------------------------------------------------------------------- *)let EXISTS_COMPLEX_ROOT_NONTRIVIAL =prove (`!a n. 2 <= n ==> ?z. z pow n = a /\ ~(z = Cx(&1))`,let dirichlet_character = new_definition `dirichlet_character d (c:num->complex) <=> (!n. c(n + d) = c(n)) /\ (!n. c(n) = Cx(&0) <=> ~coprime(n,d)) /\ (!m n. c(m * n) = c(m) * c(n))`;;let DIRICHLET_CHARACTER_PERIODIC =prove (`!d c n. dirichlet_character d c ==> c(n + d) = c(n)`,let DIRICHLET_CHARACTER_EQ_0 =prove (`!d c n. dirichlet_character d c ==> (c(n) = Cx(&0) <=> ~coprime(n,d))`,let DIRICHLET_CHARACTER_MUL =prove (`!d c m n. dirichlet_character d c ==> c(m * n) = c(m) * c(n)`,let DIRICHLET_CHARACTER_EQ_1 =prove (`!d c. dirichlet_character d c ==> c(1) = Cx(&1)`,let DIRICHLET_CHARACTER_PERIODIC_GEN =prove (`!d c m n. dirichlet_character d c ==> c(m * d + n) = c(n)`,let DIRICHLET_CHARACTER_CONG =prove (`!d c m n. dirichlet_character d c /\ (m == n) (mod d) ==> c(m) = c(n)`,let DIRICHLET_CHARACTER_ROOT =prove (`!d c n. dirichlet_character d c /\ coprime(d,n) ==> c(n) pow phi(d) = Cx(&1)`,(* ------------------------------------------------------------------------- *) (* The principal character mod d. *) (* ------------------------------------------------------------------------- *)let DIRICHLET_CHARACTER_NORM =prove (`!d c n. dirichlet_character d c ==> norm(c n) = if coprime(d,n) then &1 else &0`,let DIRICHLET_CHARACTER_NONPRINCIPAL =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) ==> ?n. coprime(n,d) /\ ~(c n = Cx(&0)) /\ ~(c n = Cx(&1))`,(* ------------------------------------------------------------------------- *) (* Finiteness of the set of characters (later we could get size = phi(d)). *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* Very basic group structure. *) (* ------------------------------------------------------------------------- *)let DIRICHLET_CHARACTER_1 =prove (`!c. dirichlet_character 1 c <=> !n. c n = Cx(&1)`,let DIRICHLET_CHARACTER_MUL_CNJ =prove (`!d c n. dirichlet_character d c /\ ~(c n = Cx(&0)) ==> cnj(c n) * c n = Cx(&1) /\ c n * cnj(c n) = Cx(&1)`,(* ------------------------------------------------------------------------- *) (* Orthogonality relations, a weak version of one first. *) (* ------------------------------------------------------------------------- *)let DIRICHLET_CHARACTER_GROUPMUL =prove (`!d c1 c2. dirichlet_character d c1 /\ dirichlet_character d c2 ==> dirichlet_character d (\n. c1(n) * c2(n))`,let DIRICHLET_CHARACTER_SUM_OVER_NUMBERS =prove (`!d c. dirichlet_character d c ==> vsum (1..d) c = if c = chi_0 d then Cx(&(phi d)) else Cx(&0)`,let DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_WEAK =prove (`!d n. vsum {c | dirichlet_character d c} (\x. x n) = Cx(&0) \/ coprime(n,d) /\ !c. dirichlet_character d c ==> c(n) = Cx(&1)`,(* ------------------------------------------------------------------------- *) (* A somewhat gruesome lemma about extending a character from a subgroup. *) (* ------------------------------------------------------------------------- *)let DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_POS =prove (`!d n. real(vsum {c | dirichlet_character d c} (\c. c n)) /\ &0 <= Re(vsum {c | dirichlet_character d c} (\c. c n))`,(* ------------------------------------------------------------------------- *) (* Hence the key result that we can find a distinguishing character. *) (* ------------------------------------------------------------------------- *)let CHARACTER_EXTEND_FROM_SUBGROUP =prove (`!f h a d. h SUBSET {x | x < d /\ coprime(x,d)} /\ (1 IN h) /\ (!x y. x IN h /\ y IN h ==> ((x * y) MOD d) IN h) /\ (!x. x IN h ==> ?y. y IN h /\ (x * y == 1) (mod d)) /\ (!x. x IN h ==> ~(f x = Cx(&0))) /\ (!x y. x IN h /\ y IN h ==> f((x * y) MOD d) = f(x) * f(y)) /\ a IN {x | x < d /\ coprime(x,d)} DIFF h ==> ?f' h'. (a INSERT h) SUBSET h' /\ h' SUBSET {x | x < d /\ coprime(x,d)} /\ (!x. x IN h ==> f'(x) = f(x)) /\ ~(f' a = Cx(&1)) /\ 1 IN h' /\ (!x y. x IN h' /\ y IN h' ==> ((x * y) MOD d) IN h') /\ (!x. x IN h' ==> ?y. y IN h' /\ (x * y == 1) (mod d)) /\ (!x. x IN h' ==> ~(f' x = Cx(&0))) /\ (!x y. x IN h' /\ y IN h' ==> f'((x * y) MOD d) = f'(x) * f'(y))`,(* ------------------------------------------------------------------------- *) (* Hence we get the full second orthogonality relation. *) (* ------------------------------------------------------------------------- *)let DIRICHLET_CHARACTER_DISCRIMINATOR =prove (`!d n. 1 < d /\ ~((n == 1) (mod d)) ==> ?c. dirichlet_character d c /\ ~(c n = Cx(&1))`,let DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_INEXPLICIT =prove (`!d n. vsum {c | dirichlet_character d c} (\c. c n) = if (n == 1) (mod d) then Cx(&(CARD {c | dirichlet_character d c})) else Cx(&0)`,(* ------------------------------------------------------------------------- *) (* L-series, just at the point s = 1. *) (* ------------------------------------------------------------------------- *)let DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS =prove (`!d n. 1 <= d ==> vsum {c | dirichlet_character d c} (\c. c(n)) = if (n == 1) (mod d) then Cx(&(phi d)) else Cx(&0)`,let Lfunction_DEF = new_definition `Lfunction c = infsum (from 1) (\n. c(n) / Cx(&n))`;;(* ------------------------------------------------------------------------- *) (* Other properties of conjugate characters. *) (* ------------------------------------------------------------------------- *)let LFUNCTION =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) ==> ((\n. c(n) / Cx(&n)) sums (Lfunction c)) (from 1)`,(* ------------------------------------------------------------------------- *) (* Explicit bound on truncating the Lseries. *) (* ------------------------------------------------------------------------- *)let LFUNCTION_CNJ =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) ==> Lfunction (\n. cnj(c n)) = cnj(Lfunction c)`,let LFUNCTION_PARTIAL_SUM =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) ==> ?B. &0 < B /\ !n. 1 <= n ==> norm(Lfunction c - vsum(1..n) (\n. c(n) / Cx(&n))) <= B / (&n + &1)`,(* ------------------------------------------------------------------------- *) (* First key bound, when the Lfunction is not zero (as indeed it isn't). *) (* ------------------------------------------------------------------------- *)let LFUNCTION_PARTIAL_SUM_STRONG =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) ==> ?B. &0 < B /\ !n. norm(Lfunction c - vsum(1..n) (\n. c(n) / Cx(&n))) <= B / (&n + &1)`,let BOUNDED_LFUNCTION_DIRICHLET_MANGOLDT_LEMMA =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) ==> bounded { Lfunction(c) * vsum(1..x) (\n. c(n) * Cx(mangoldt n / &n)) - vsum(1..x) (\n. c(n) * Cx(log(&n) / &n)) | x IN (:num)}`,let SUMMABLE_CHARACTER_LOG_OVER_N =prove (`!c d. dirichlet_character d c /\ ~(c = chi_0 d) ==> summable (from 1) (\n. c(n) * Cx(log(&n) / &n))`,let BOUNDED_LFUNCTION_DIRICHLET_MANGOLDT =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) ==> bounded { Lfunction(c) * vsum(1..x) (\n. c(n) * Cx(mangoldt n / &n)) | x IN (:num)}`,(* ------------------------------------------------------------------------- *) (* Now a bound when the Lfunction is zero (hypothetically). *) (* ------------------------------------------------------------------------- *)let BOUNDED_DIRICHLET_MANGOLDT_NONZERO =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) /\ ~(Lfunction c = Cx(&0)) ==> bounded { vsum(1..x) (\n. c n * Cx(mangoldt n / &n)) | x IN (:num)}`,let MANGOLDT_LOG_SUM =prove (`!n. 1 <= n ==> mangoldt(n) = --(sum {d | d divides n} (\d. mobius(d) * log(&d)))`,let BOUNDED_DIRICHLET_MANGOLDT_LEMMA =prove (`!d c x. dirichlet_character d c /\ ~(c = chi_0 d) /\ 1 <= x ==> Cx(log(&x)) + vsum (1..x) (\n. c(n) * Cx(mangoldt n / &n)) = vsum (1..x) (\n. c(n) / Cx(&n) * vsum {d | d divides n} (\d. Cx(mobius(d) * log(&x / &d))))`,let SUM_LOG_OVER_X_BOUND =prove (`!x. abs(sum(1..x) (\n. log(&x / &n) / &x)) <= &4`,(* ------------------------------------------------------------------------- *) (* Now the analogous result for the principal character. *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* The arithmetic-geometric mean that we want. *) (* ------------------------------------------------------------------------- *)let BOUNDED_DIRICHLET_MANGOLDT_ZERO =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) /\ Lfunction c = Cx(&0) ==> bounded { vsum(1..x) (\n. c n * Cx(mangoldt n / &n)) + Cx(log(&x)) | x IN (:num)}`,let SUM_OF_NUMBERS =prove (`!n. nsum(0..n) (\i. i) = (n * (n + 1)) DIV 2`,let PRODUCT_SPECIAL =prove (`!z i. product (0..n) (\i. z pow i) = z pow ((n * (n + 1)) DIV 2)`,(* ------------------------------------------------------------------------- *) (* The trickiest part: the nonvanishing of L-series for real character. *) (* Proof from Monsky's article (AMM 1993, pp. 861-2). *) (* ------------------------------------------------------------------------- *)let AGM_SPECIAL =prove (`!n t. &0 <= t ==> (&n + &1) pow 2 * t pow n <= (sum(0..n) (\k. t pow k)) pow 2`,let DIRICHLET_CHARACTER_DIVISORSUM_EQ_1 =prove (`!d c p k. dirichlet_character d c /\ prime p /\ p divides d ==> vsum {m | m divides (p EXP k)} c = Cx(&1)`,let DIRICHLET_CHARACTER_REAL_CASES =prove (`!d c. dirichlet_character d c /\ (!n. real(c n)) ==> !n. c n = --Cx(&1) \/ c n = Cx(&0) \/ c n = Cx(&1)`,let DIRICHLET_CHARACTER_DIVISORSUM_PRIMEPOW_POS =prove (`!d c p k. dirichlet_character d c /\ (!n. real(c n)) /\ prime p ==> &0 <= Re(vsum {m | m divides (p EXP k)} c)`,let DIRICHLET_CHARACTER_DIVISORSUM_POS =prove (`!d c n. dirichlet_character d c /\ (!n. real(c n)) /\ ~(n = 0) ==> &0 <= Re(vsum {m | m divides n} c)`,let lemma =prove (`!x n. &0 <= x /\ x <= &1 ==> &1 - &n * x <= (&1 - x) pow n`,(* ------------------------------------------------------------------------- *) (* Deduce nonvanishing of all the nonprincipal characters. *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* Hence derive our boundedness result for all nonprincipal characters. *) (* ------------------------------------------------------------------------- *)let LFUNCTION_NONZERO_REAL =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) /\ (!n. real(c n)) ==> ~(Lfunction c = Cx(&0))`,(* ------------------------------------------------------------------------- *) (* Hence the main sum result. *) (* ------------------------------------------------------------------------- *)let BOUNDED_DIRICHLET_MANGOLDT_NONPRINCIPAL =prove (`!d c. dirichlet_character d c /\ ~(c = chi_0 d) ==> bounded { vsum(1..x) (\n. c n * Cx(mangoldt n / &n)) | x IN (:num)}`,(* ------------------------------------------------------------------------- *) (* Ignore the density details and prove the main result. *) (* ------------------------------------------------------------------------- *)let BOUNDED_SUM_OVER_DIRICHLET_CHARACTERS =prove (`!d l. 1 <= d /\ coprime(l,d) ==> bounded { vsum {c | dirichlet_character d c} (\c. c(l) * vsum(1..x) (\n. c n * Cx (mangoldt n / &n))) - Cx(log(&x)) | x IN (:num)}`,