diff --git a/thys/Furstenberg_Topology/Furstenberg_Topology.thy b/thys/Furstenberg_Topology/Furstenberg_Topology.thy new file mode 100644 --- /dev/null +++ b/thys/Furstenberg_Topology/Furstenberg_Topology.thy @@ -0,0 +1,880 @@ +(* + File: Furstenberg_Topology.thy + Author: Manuel Eberl, TU München +*) +section \Furstenberg's topology and his proof of the infinitude of primes\ +theory Furstenberg_Topology + imports + "HOL-Real_Asymp.Real_Asymp" + "HOL-Analysis.Analysis" + "HOL-Number_Theory.Number_Theory" +begin + +text \ + This article gives a formal version of Furstenberg's topological proof of the infinitude of + primes~\cite{furstenberg}. He defines a topology on the integers based on arithmetic progressions + (or, equivalently, residue classes). + + Apart from yielding a short proof of the infinitude of primes, this topology is also fairly + `nice' in general: it is second countable, metrizable, and perfect. All of these (well-known) + facts will be formally proven below. +\ + +subsection \Arithmetic progressions of integers\ + +text \ + We first define `bidirectional infinite arithmetic progressions' on \\\ in the sense that + to an integer \a\ and a positive integer \b\, we associate all the integers \x\ such that + $x \equiv a\ (\text{mod}\ b)$, or, equivalently, $\{a + nb\mid n\in\mathbb{Z}\}$. +\ + +definition arith_prog :: "int \ nat \ int set" where + "arith_prog a b = {x. [x = a] (mod int b)}" + +lemma arith_prog_0_right [simp]: "arith_prog a 0 = {a}" + by (simp add: arith_prog_def) + +lemma arith_prog_Suc_0_right [simp]: "arith_prog a (Suc 0) = UNIV" + by (auto simp: arith_prog_def) + +lemma in_arith_progI [intro]: "[x = a] (mod b) \ x \ arith_prog a b" + by (auto simp: arith_prog_def) + +text \ + Two arithmetic progressions with the same period and noncongruent starting points are + disjoint. +\ +lemma arith_prog_disjoint: + assumes "[a \ a'] (mod int b)" and "b > 0" + shows "arith_prog a b \ arith_prog a' b = {}" + using assms by (auto simp: arith_prog_def cong_def) + +text \ + Multiplying the period gives us a subset of the original progression. +\ +lemma arith_prog_dvd_mono: "b dvd b' \ arith_prog a b' \ arith_prog a b" + by (auto simp: arith_prog_def cong_dvd_modulus) + +text \ + The following proves the alternative definition mentioned above. +\ +lemma bij_betw_arith_prog: + assumes "b > 0" + shows "bij_betw (\n. a + int b * n) UNIV (arith_prog a b)" +proof (rule bij_betwI[of _ _ _ "\x. (x - a) div int b"], goal_cases) + case 1 + thus ?case + by (auto simp: arith_prog_def cong_add_lcancel_0 cong_mult_self_right mult_of_nat_commute) +next + case 4 + thus ?case + by (auto simp: arith_prog_def cong_iff_lin) +qed (use \b > 0\ in \auto simp: arith_prog_def\) + +lemma arith_prog_altdef: "arith_prog a b = range (\n. a + int b * n)" +proof (cases "b = 0") + case False + thus ?thesis + using bij_betw_arith_prog[of b] by (auto simp: bij_betw_def) +qed auto + +text \ + A simple corollary from this is also that any such arithmetic progression is infinite. +\ +lemma infinite_arith_prog: "b > 0 \ infinite (arith_prog a b)" + using bij_betw_finite[OF bij_betw_arith_prog[of b]] by simp + + +subsection \The Furstenberg topology on \\\\ + +text \ + The typeclass-based topology is somewhat nicer to use in Isabelle/HOL, but the integers, + of course, already have a topology associated to them. We therefore need to introduce a type + copy of the integers and furnish them with the new topology. We can easily convert between + them and the `proper' integers using Lifting and Transfer. +\ +typedef fbint = "UNIV :: int set" + morphisms int_of_fbint fbint .. + +setup_lifting type_definition_fbint + +lift_definition arith_prog_fb :: "int \ nat \ fbint set" is "arith_prog" . + +instantiation fbint :: topological_space +begin + +text \ + Furstenberg defined the topology as the one generated by all arithmetic progressions. + We use a slightly more explicit equivalent formulation that exploits the fact that + the intersection of two arithmetic progressions is again an arithmetic progression (or empty). +\ +lift_definition open_fbint :: "fbint set \ bool" is + "\U. (\x\U. \b>0. arith_prog x b \ U)" . + +text \ + We now prove that this indeed forms a topology. +\ +instance proof + show "open (UNIV :: fbint set)" + by transfer auto +next + fix U V :: "fbint set" + assume "open U" and "open V" + show "open (U \ V)" + proof (use \open U\ \open V\ in transfer, safe) + fix U V :: "int set" and x :: int + assume U: "\x\U. \b>0. arith_prog x b \ U" and V: "\x\V. \b>0. arith_prog x b \ V" + assume x: "x \ U" "x \ V" + from U x obtain b1 where b1: "b1 > 0" "arith_prog x b1 \ U" by auto + from V x obtain b2 where b2: "b2 > 0" "arith_prog x b2 \ V" by auto + from b1 b2 have "lcm b1 b2 > 0" "arith_prog x (lcm b1 b2) \ U \ V" + using arith_prog_dvd_mono[of b1 "lcm b1 b2" x] arith_prog_dvd_mono[of b2 "lcm b1 b2" x] + by (auto simp: lcm_pos_nat) + thus "\b>0. arith_prog x b \ U \ V" by blast + qed +next + fix F :: "fbint set set" + assume *: "\U\F. open U" + show "open (\F)" + proof (use * in transfer, safe) + fix F :: "int set set" and U :: "int set" and x :: int + assume F: "\U\F. \x\U. \b>0. arith_prog x b \ U" + assume "x \ U" "U \ F" + with F obtain b where b: "b > 0" "arith_prog x b \ U" by blast + with \U \ F\ show "\b>0. arith_prog x b \ \F" + by blast + qed +qed + +end + +text \ + Since any non-empty open set contains an arithmetic progression and arithmetic progressions + are infinite, we obtain that all nonempty open sets are infinite. +\ +lemma open_fbint_imp_infinite: + fixes U :: "fbint set" + assumes "open U" and "U \ {}" + shows "infinite U" + using assms +proof transfer + fix U :: "int set" + assume *: "\x\U. \b>0. arith_prog x b \ U" and "U \ {}" + from \U \ {}\ obtain x where "x \ U" by auto + with * obtain b where b: "b > 0" "arith_prog x b \ U" by auto + from b have "infinite (arith_prog x b)" + using infinite_arith_prog by blast + with b show "infinite U" + using finite_subset by blast +qed + +lemma not_open_finite_fbint [simp]: + assumes "finite (U :: fbint set)" "U \ {}" + shows "\open U" + using open_fbint_imp_infinite assms by blast + +text \ + More or less by definition, any arithmetic progression is open. +\ +lemma open_arith_prog_fb [intro]: + assumes "b > 0" + shows "open (arith_prog_fb a b)" + using assms +proof transfer + fix a :: int and b :: nat + assume "b > 0" + show "\x\arith_prog a b. \b'>0. arith_prog x b' \ arith_prog a b" + proof (intro ballI exI[of _ b] conjI) + fix x assume "x \ arith_prog a b" + thus "arith_prog x b \ arith_prog a b" + using cong_trans by (auto simp: arith_prog_def ) + qed (use \b > 0\ in auto) +qed + +text \ + Slightly less obviously, any arithmetic progression is also closed. + This can be seen by realising that for a period \b\, we can partition the integers + into \b\ congruence classes and then the complement of each congruence class is the + union of the other \b - 1\ classes, and unions of open sets are open. +\ +lemma closed_arith_prog_fb [intro]: + assumes "b > 0" + shows "closed (arith_prog_fb a b)" +proof - + have "open (-arith_prog_fb a b)" + proof - + have "-arith_prog_fb a b = (\i\{1.. arith_prog a b" if "x \ arith_prog (a + int i) b" "i \ {1.. a + int i] (mod int b)" + proof + assume "[a = a + int i] (mod int b)" + hence "[a + 0 = a + int i] (mod int b)" by simp + hence "[0 = int i] (mod int b)" by (subst (asm) cong_add_lcancel) auto + with that show False by (auto simp: cong_def) + qed + thus ?thesis using arith_prog_disjoint[of a "a + int i" b] \b > 0\ that by auto + qed + + have covering: "x \ arith_prog a b \ x \ (\i\{1..b > 0\ by simp + also have "[a + (x - a) mod int b = a + (x - a)] (mod int b)" + by (intro cong_add) auto + finally have "[x = a + int i] (mod int b)" + by (simp add: cong_sym_eq) + hence "x \ arith_prog (a + int i) b" + using \b > 0\ by (auto simp: arith_prog_def) + moreover have "i < b" using \b > 0\ + by (auto simp: i_def nat_less_iff) + ultimately show ?thesis using \b > 0\ + by (cases "i = 0") auto + qed + + from disjoint and covering show "- arith_prog a b = (\i\{1..b > 0\ have "open \" + by auto + finally show ?thesis . + qed + thus ?thesis by (simp add: closed_def) +qed + +subsection \The infinitude of primes\ + +text \ + The infinite of the primes now follows quite obviously: The multiples of any prime form a + closed set, so if there were only finitely many primes, the union of all of these would also + be open. However, since any number other than \\1\ has a prime divisor, the union of all these + sets is simply \\\{\1}\, which is obviously \<^emph>\not\ closed since the finite set \{\1}\ is not + open. +\ +theorem "infinite {p::nat. prime p}" +proof + assume fin: "finite {p::nat. prime p}" + define A where "A = (\p\{p::nat. prime p}. arith_prog_fb 0 p)" + have "closed A" + unfolding A_def using fin by (intro closed_Union) (auto simp: prime_gt_0_nat) + hence "open (-A)" + by (simp add: closed_def) + also have "A = -{fbint 1, fbint (-1)}" + unfolding A_def + proof transfer + show "(\p\{p::nat. prime p}. arith_prog 0 p) = - {1, - 1}" + proof (intro equalityI subsetI) + fix x :: int assume x: "x \ -{1, -1}" + hence "\x\ \ 1" by auto + show "x \ (\p\{p::nat. prime p}. arith_prog 0 p)" + proof (cases "x = 0") + case True + thus ?thesis + by (auto simp: A_def intro!: exI[of _ 2]) + next + case [simp]: False + obtain p where p: "prime p" "p dvd x" + using prime_divisor_exists[of x] and \\x\ \ 1\ by auto + hence "x \ arith_prog 0 (nat p)" using prime_gt_0_int[of p] + by (auto simp: arith_prog_def cong_0_iff) + thus ?thesis using p + by (auto simp: A_def intro!: exI[of _ "nat p"]) + qed + qed (auto simp: A_def arith_prog_def cong_0_iff) + qed + also have "-(-{fbint 1, fbint (-1)}) = {fbint 1, fbint (-1)}" + by simp + finally have "open {fbint 1, fbint (-1)}" . + thus False by simp +qed + + + + +subsection \Additional topological properties\ + +text \ + Just for fun, let us also show a few more properties of Furstenberg's topology. + First, we show the equivalence to the above to Furstenberg's original definition + (the topology generated by all arithmetic progressions). +\ + +theorem topological_basis_fbint: "topological_basis {arith_prog_fb a b |a b. b > 0}" + unfolding topological_basis_def +proof safe + fix a :: int and b :: nat + assume "b > 0" + thus "open (arith_prog_fb a b)" + by auto +next + fix U :: "fbint set" assume "open U" + hence "\x\U. \b. b > 0 \ arith_prog_fb (int_of_fbint x) b \ U" + by transfer + hence "\f. \x\U. f x > 0 \ arith_prog_fb (int_of_fbint x) (f x) \ U" + by (subst (asm) bchoice_iff) + then obtain f where f: "\x\U. f x > 0 \ arith_prog_fb (int_of_fbint x) (f x) \ U" .. + define B where "B = (\x. arith_prog_fb (int_of_fbint x) (f x)) ` U" + have "B \ {arith_prog_fb a b |a b. b > 0}" + using f by (auto simp: B_def) + moreover have "\B = U" + proof safe + fix x assume "x \ U" + hence "x \ arith_prog_fb (int_of_fbint x) (f x)" + using f by transfer auto + with \x \ U\ show "x \ \B" by (auto simp: B_def) + qed (use f in \auto simp: B_def\) + ultimately show "\B'\{arith_prog_fb a b |a b. 0 < b}. \ B' = U" by auto +qed + +lemma open_fbint_altdef: "open = generate_topology {arith_prog_fb a b |a b. b > 0}" + using topological_basis_imp_subbasis[OF topological_basis_fbint] . + + +text \ + From this, we can immediately see that it is second countable: +\ +instance fbint :: second_countable_topology +proof + have "countable ((\(a,b). arith_prog_fb a b) ` (UNIV \ {b. b > 0}))" + by (intro countable_image) auto + also have "\ = {arith_prog_fb a b |a b. b > 0}" + by auto + ultimately show "\B::fbint set set. countable B \ open = generate_topology B" + unfolding open_fbint_altdef by auto +qed + +text \ + A trivial consequence of the fact that nonempty open sets in this topology are infinite + is that it is a perfect space: +\ +instance fbint :: perfect_space + by standard auto + + +text \ + It is also Hausdorff, since given any two distinct integers, we can easily + construct two non-overlapping arithmetic progressions that each contain one of them. + We do not \<^emph>\really\ have to prove this since we will get it for free later on when we + show that it is a metric space, but here is the proof anyway: +\ +instance fbint :: t2_space +proof + fix x y :: fbint + assume "x \ y" + define d where "d = nat \int_of_fbint x - int_of_fbint y\ + 1" + from \x \ y\ have "d > 0" + unfolding d_def by transfer auto + define U where "U = arith_prog_fb (int_of_fbint x) d" + define V where "V = arith_prog_fb (int_of_fbint y) d" + + have "U \ V = {}" unfolding U_def V_def d_def + proof (use \x \ y\ in transfer, rule arith_prog_disjoint) + fix x y :: int + assume "x \ y" + show "[x \ y] (mod int (nat \x - y\ + 1))" + proof + assume "[x = y] (mod int (nat \x - y\ + 1))" + hence "\x - y\ + 1 dvd \x - y\" + by (auto simp: cong_iff_dvd_diff algebra_simps) + hence "\x - y\ + 1 \ \x - y\" + by (rule zdvd_imp_le) (use \x \ y\ in auto) + thus False by simp + qed + qed auto + moreover have "x \ U" "y \ V" + unfolding U_def V_def by (use \d > 0\ in transfer, fastforce)+ + moreover have "open U" "open V" + using \d > 0\ by (auto simp: U_def V_def) + ultimately show "\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}" by blast +qed + +(* TODO Move? *) +text \ + Next, we need a small lemma: Given an additional assumption, a $T_2$ space is also $T_3$: +\ +lemma t2_space_t3_spaceI: + assumes "\(x :: 'a :: t2_space) U. x \ U \ open U \ + \V. x \ V \ open V \ closure V \ U" + shows "OFCLASS('a, t3_space_class)" +proof + fix X :: "'a set" and z :: 'a + assume X: "closed X" "z \ X" + with assms[of z "-X"] obtain V where V: "z \ V" "open V" "closure V \ -X" + by auto + show "\U V. open U \ open V \ z \ U \ X \ V \ U \ V = {}" + by (rule exI[of _ V], rule exI[of _ "-closure V"]) + (use X V closure_subset[of V] in auto) +qed + +text \ + Since the Fürstenberg topology is $T_2$ and every arithmetic progression is also closed, + we can now easily show that it is also $T_3$ (i.\,e.\ regular). + Again, we do not really need this proof, but here it is: +\ +instance fbint :: t3_space +proof (rule t2_space_t3_spaceI) + fix x :: fbint and U :: "fbint set" + assume "x \ U" and "open U" + then obtain b where b: "b > 0" "arith_prog_fb (int_of_fbint x) b \ U" + by transfer blast + define V where "V = arith_prog_fb (int_of_fbint x) b" + have "x \ V" + unfolding V_def by transfer auto + moreover have "open V" "closed V" + using \b > 0\ by (auto simp: V_def) + ultimately show "\V. x \ V \ open V \ closure V \ U" + using b by (intro exI[of _ V]) (auto simp: V_def) +qed + + +subsection \Metrizability\ + +text \ + The metrizability of Furstenberg's topology (i.\,e.\ that it is induced by some metric) can + be shown from the fact that it is second countable and $T_3$ using Urysohn's Metrization Theorem, + but this is not available in Isabelle yet. Let us therefore give an \<^emph>\explicit\ metric, + as described by Zulfeqarr~\cite{zulfeqarr}. We follow the exposition by Dirmeier~\cite{dirmeier}. + + First, we define a kind of norm on the integers. The norm depends on a real parameter \q > 1\. + The value of \q\ does not matter in the sense that all values induce the same topology + (which we will show). For the final definition, we then simply pick \q = 2\. +\ + +locale fbnorm = + fixes q :: "real" + assumes q_gt_1: "q > 1" +begin + +definition N :: "int \ real" where + "N n = (\k. if k = 0 \ int k dvd n then 0 else 1 / q ^ k)" + +lemma N_summable: "summable (\k. if k = 0 \ int k dvd n then 0 else 1 / q ^ k)" + by (rule summable_comparison_test[OF _ summable_geometric[of "1/q"]]) + (use q_gt_1 in \auto intro!: exI[of _ 0] simp: power_divide\) + +lemma N_sums: "(\k. if k = 0 \ int k dvd n then 0 else 1 / q ^ k) sums N n" + using N_summable unfolding N_def by (rule summable_sums) + +lemma N_nonneg: "N n \ 0" + by (rule sums_le[OF _ sums_zero N_sums]) (use q_gt_1 in auto) + +lemma N_uminus [simp]: "N (-n) = N n" + by (simp add: N_def) + +lemma N_minus_commute: "N (x - y) = N (y - x)" + using N_uminus[of "x - y"] by (simp del: N_uminus) + +lemma N_zero [simp]: "N 0 = 0" + by (simp add: N_def) + +lemma not_dvd_imp_N_ge: + assumes "\n dvd a" "n > 0" + shows "N a \ 1 / q ^ n" + by (rule sums_le[OF _ sums_single[of n] N_sums]) (use q_gt_1 assms in auto) + +lemma N_lt_imp_dvd: + assumes "N a < 1 / q ^ n" and "n > 0" + shows "n dvd a" + using not_dvd_imp_N_ge[of n a] assms by auto + +lemma N_pos: + assumes "n \ 0" + shows "N n > 0" +proof - + have "0 < 1 / q ^ (nat \n\+1)" + using q_gt_1 by simp + also have "\1 + \n\ dvd \n\" + using zdvd_imp_le[of "1 + \n\" "\n\"] assms by auto + hence "1 / q ^ (nat \n\+1) \ N n" + by (intro not_dvd_imp_N_ge) (use assms in auto) + finally show ?thesis . +qed + +lemma N_zero_iff [simp]: "N n = 0 \ n = 0" + using N_pos[of n] by (cases "n = 0") auto + +lemma N_triangle_ineq: "N (n + m) \ N n + N m" +proof (rule sums_le) + let ?I = "\n k. if k = 0 \ int k dvd n then 0 else 1 / q ^ k" + show "?I (n + m) sums N (n + m)" + by (rule N_sums) + show "(\k. ?I n k + ?I m k) sums (N n + N m)" + by (intro sums_add N_sums) + show "\k. ?I (n + m) k \ ?I n k + ?I m k" + using q_gt_1 by auto +qed + +lemma N_1: "N 1 = 1 / (q * (q - 1))" +proof (rule sums_unique2) + have "(\k. if k = 0 \ int k dvd 1 then 0 else 1 / q ^ k) sums N 1" + by (rule N_sums) + also have "(\k. if k = 0 \ int k dvd 1 then 0 else 1 / q ^ k) = + (\k. if k \ {0, 1} then 0 else (1 / q) ^ k)" + by (simp add: power_divide cong: if_cong) + finally show "(\k. if k \ {0, 1} then 0 else (1 / q) ^ k) sums N 1" . + + have "(\k. if k \ {0, 1} then 0 else (1 / q) ^ k) sums + (1 / (1 - 1 / q) + (- (1 / q) - 1))" + by (rule sums_If_finite_set'[OF geometric_sums]) (use q_gt_1 in auto) + also have "\ = 1 / (q * (q - 1))" + using q_gt_1 by (simp add: field_simps) + finally show "(\k. if k \ {0, 1} then 0 else (1 / q) ^ k) sums \" . +qed + +text \ + It follows directly from the definition that norms fulfil a kind of monotonicity property + with respect to divisibility: the norm of a number is at most as large as the norm of any of + its factors: +\ +lemma N_dvd_mono: + assumes "m dvd n" + shows "N n \ N m" +proof (rule sums_le[OF allI N_sums N_sums]) + fix k :: nat + show "(if k = 0 \ int k dvd n then 0 else 1 / q ^ k) \ + (if k = 0 \ int k dvd m then 0 else 1 / q ^ k)" + using q_gt_1 assms by auto +qed + +text \ + In particular, this means that 1 and -1 have the greatest norm. +\ +lemma N_le_N_1: "N n \ N 1" + by (rule N_dvd_mono) auto + +text \ + Primes have relatively large norms, almost reaching the norm of 1: +\ +lemma N_prime: + assumes "prime p" + shows "N p = N 1 - 1 / q ^ nat p" +proof (rule sums_unique2) + define p' where "p' = nat p" + have p: "p = int p'" + using assms by (auto simp: p'_def prime_ge_0_int) + have "prime p'" + using assms by (simp add: p) + + have "(\k. if k = 0 \ int k dvd p then 0 else 1 / q ^ k) sums N p" + by (rule N_sums) + also have "int k dvd p \ k \ {1, p'}" for k + using assms by (auto simp: p prime_nat_iff) + hence "(\k. if k = 0 \ int k dvd p then 0 else 1 / q ^ k) = + (\k. if k \ {0, 1, p'} then 0 else (1 / q) ^ k)" + using assms q_gt_1 by (simp add: power_divide cong: if_cong) + finally show "\ sums N p" . + + have "(\k. if k \ {0, 1, p'} then 0 else (1 / q) ^ k) sums + (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - 1))" + by (rule sums_If_finite_set'[OF geometric_sums]) + (use \prime p'\ q_gt_1 prime_gt_Suc_0_nat[of p'] in \auto simp: \) + also have "\ = N 1 - 1 / q ^ p'" + using q_gt_1 by (simp add: field_simps N_1) + finally show "(\k. if k \ {0, 1, p'} then 0 else (1 / q) ^ k) sums \" . +qed + +lemma N_2: "N 2 = 1 / (q ^ 2 * (q - 1))" + using q_gt_1 by (auto simp: N_prime N_1 field_simps power2_eq_square) + +lemma N_less_N_1: + assumes "n \ 1" "n \ -1" + shows "N n < N 1" +proof (cases "n = 0") + case False + then obtain p where p: "prime p" "p dvd n" + using prime_divisor_exists[of n] assms by force + hence "N n \ N p" by (intro N_dvd_mono) + also from p have "N p < N 1" + using q_gt_1 by (simp add: N_prime) + finally show ?thesis . +qed (use q_gt_1 in \auto simp: N_1\) + +text \ + Composites, on the other hand, do not achieve this: +\ +lemma nonprime_imp_N_lt: + assumes "\prime_elem n" "\n\ \ 1" "n \ 0" + shows "N n < N 1 - 1 / q ^ nat \n\" +proof - + obtain p where p: "prime p" "p dvd n" + using prime_divisor_exists[of n] assms by auto + define p' where "p' = nat p" + have p': "p = int p'" + using p by (auto simp: p'_def prime_ge_0_int) + have "prime p'" + using p by (simp add: p') + + define n' where "n' = nat \n\" + have "n' > 1" + using assms by (auto simp: n'_def) + + have "N n \ 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'" + proof (rule sums_le) + show "(\k. if k = 0 \ int k dvd n then 0 else 1 / q ^ k) sums N n" + by (rule N_sums) + next + from assms p have "n' \ p'" + by (auto simp: n'_def p'_def nat_eq_iff) + hence "(\k. if k \ {0, 1, p', n'} then 0 else (1 / q) ^ k) sums + (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - (1 / q) ^ n' - 1))" + by (intro sums_If_finite_set'[OF geometric_sums]) + (use \prime p'\ q_gt_1 prime_gt_Suc_0_nat[of p'] \n' > 1\ in \auto simp: \) + also have "\ = 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'" + using q_gt_1 by (simp add: field_simps) + finally show "(\k. if k \ {0, 1, p', n'} then 0 else (1 / q) ^ k) sums \" . + next + show " \na. (if na = 0 \ int na dvd n then 0 else 1 / q ^ na) + \ (if na \ {0, 1, p', n'} then 0 else (1 / q) ^ na)" + using q_gt_1 assms p by (auto simp: p'_def n'_def power_divide) + qed + also have "\ < 1 / (q * (q - 1)) - 1 / q ^ n'" + using q_gt_1 by simp + finally show ?thesis by (simp add: n'_def N_1) +qed + +text \ + This implies that one can use the norm as a primality test: +\ +lemma prime_iff_N_eq: + assumes "n \ 0" + shows "prime_elem n \ N n = N 1 - 1 / q ^ nat \n\" +proof - + have *: "prime_elem n \ N n = N 1 - 1 / q ^ nat \n\" if "n > 0" for n + proof - + consider "n = 1" | "prime n" | "\prime n" "n > 1" + using \n > 0\ by force + thus ?thesis + proof cases + assume "n = 1" + thus ?thesis using q_gt_1 + by (auto simp: N_1) + next + assume n: "\prime n" "n > 1" + with nonprime_imp_N_lt[of n] show ?thesis by simp + qed (auto simp: N_prime prime_ge_0_int) + qed + + show ?thesis + proof (cases "n > 0") + case True + with * show ?thesis by blast + next + case False + with *[of "-n"] assms show ?thesis by simp + qed +qed + +text \ + Factorials, on the other hand, have very small norms: +\ +lemma N_fact_le: "N (fact m) \ 1 / (q - 1) * 1 / q ^ m" +proof (rule sums_le[OF allI N_sums]) + have "(\k. 1 / q ^ k / q ^ Suc m) sums (q / (q - 1) / q ^ Suc m)" + using geometric_sums[of "1 / q"] q_gt_1 + by (intro sums_divide) (auto simp: field_simps) + also have "(q / (q - 1) / q ^ Suc m) = 1 / (q - 1) * 1 / q ^ m" + using q_gt_1 by (simp add: field_simps) + also have "(\k. 1 / q ^ k / q ^ Suc m) = (\k. 1 / q ^ (k + Suc m))" + using q_gt_1 by (simp add: field_simps power_add) + also have "\ = (\k. if k + Suc m \ m then 0 else 1 / q ^ (k + Suc m))" + by auto + finally have "\ sums (1 / (q - 1) * 1 / q ^ m)" . + also have "?this \ (\k. if k \ m then 0 else 1 / q ^ k) sums (1 / (q - 1) * 1 / q ^ m)" + by (rule sums_zero_iff_shift) auto + finally show \ . +next + fix k :: nat + have "int k dvd fact m" if "k > 0" "k \ m" + proof - + have "int k dvd int (fact m)" + unfolding int_dvd_int_iff using that by (simp add: dvd_fact) + thus "int k dvd fact m" + unfolding of_nat_fact by simp + qed + thus "(if k = 0 \ int k dvd fact m then 0 else 1 / q ^ k) \ + (if k \ m then 0 else 1 / q ^ k)" using q_gt_1 by auto +qed + +lemma N_prime_mono: + assumes "prime p" "prime p'" "p \ p'" + shows "N p \ N p'" + using assms q_gt_1 by (auto simp add: N_prime field_simps nat_le_iff prime_ge_0_int) + +lemma N_prime_ge: + assumes "prime p" + shows "N p \ 1 / (q\<^sup>2 * (q - 1))" +proof - + have "1 / (q ^ 2 * (q - 1)) = N 2" + using q_gt_1 by (auto simp: N_prime N_1 field_simps power2_eq_square) + also have "\ \ N p" + using assms by (intro N_prime_mono) (auto simp: prime_ge_2_int) + finally show ?thesis . +qed + +lemma N_prime_elem_ge: + assumes "prime_elem p" + shows "N p \ 1 / (q\<^sup>2 * (q - 1))" +proof (cases "p \ 0") + case True + with assms N_prime_ge show ?thesis by auto +next + case False + with assms N_prime_ge[of "-p"] show ?thesis by auto +qed + + +text \ + Next, we use this norm to derive a metric: +\ + +lift_definition dist :: "fbint \ fbint \ real" is + "\x y. N (x - y)" . + +lemma dist_self [simp]: "dist x x = 0" + by transfer simp + +lemma dist_sym [simp]: "dist x y = dist y x" + by transfer (simp add: N_minus_commute) + +lemma dist_pos: "x \ y \ dist x y > 0" + by transfer (use N_pos in simp) + +lemma dist_eq_0_iff [simp]: "dist x y = 0 \ x = y" + using dist_pos[of x y] by (cases "x = y") auto + +lemma dist_triangle_ineq: "dist x z \ dist x y + dist y z" +proof transfer + fix x y z :: int + show "N (x - z) \ N (x - y) + N (y - z)" + using N_triangle_ineq[of "x - y" "y - z"] by simp +qed + + +text \ + Lastly, we show that the metric we defined indeed induces the Furstenberg topology. +\ +theorem dist_induces_open: + "open U \ (\x\U. \e>0. \y. dist x y < e \ y \ U)" +proof (transfer, safe) + fix U :: "int set" and x :: int + assume *: "\x\U. \b>0. arith_prog x b \ U" + assume "x \ U" + with * obtain b where b: "b > 0" "arith_prog x b \ U" by blast + define e where "e = 1 / q ^ b" + + show "\e>0. \y. N (x - y) < e \ y \ U" + proof (rule exI; safe?) + show "e > 0" using q_gt_1 by (simp add: e_def) + next + fix y assume "N (x - y) < e" + also have "\ = 1 / q ^ b" by fact + finally have "b dvd (x - y)" + by (rule N_lt_imp_dvd) fact + hence "y \ arith_prog x b" + by (auto simp: arith_prog_def cong_iff_dvd_diff dvd_diff_commute) + with b show "y \ U" by blast + qed + +next + + fix U :: "int set" and x :: int + assume *: "\x\U. \e>0. \y. N (x - y) < e \ y \ U" + assume "x \ U" + with * obtain e where e: "e > 0" "\y. N (x - y) < e \ y \ U" by blast + have "eventually (\N. 1 / (q - 1) * 1 / q ^ N < e) at_top" + using q_gt_1 \e > 0\ by real_asymp + then obtain m where m: "1 / (q - 1) * 1 / q ^ m < e" + by (auto simp: eventually_at_top_linorder) + define b :: nat where "b = fact m" + + have "arith_prog x b \ U" + proof + fix y assume "y \ arith_prog x b" + show "y \ U" + proof (cases "y = x") + case False + from \y \ arith_prog x b\ obtain n where y: "y = x + int b * n" + by (auto simp: arith_prog_altdef) + from y and \y \ x\ have [simp]: "n \ 0" by auto + have "N (x - y) = N (int b * n)" by (simp add: y) + also have "\ \ N (int b)" + by (rule N_dvd_mono) auto + also have "\ \ 1 / (q - 1) * 1 / q ^ m" + using N_fact_le by (simp add: b_def) + also have "\ < e" by fact + finally show "y \ U" using e by auto + qed (use \x \ U\ in auto) + qed + moreover have "b > 0" by (auto simp: b_def) + ultimately show "\b>0. arith_prog x b \ U" + by blast +qed + +end + + +text \ + We now show that the Fürstenberg space is a metric space with this metric (with \q = 2\), + which essentially only amounts to plugging together all the results from above. +\ + +interpretation fb: fbnorm 2 + by standard auto + + +instantiation fbint :: dist +begin + +definition dist_fbint where "dist_fbint = fb.dist" + +instance .. + +end + + +instantiation fbint :: uniformity_dist +begin + +definition uniformity_fbint :: "(fbint \ fbint) filter" where + "uniformity_fbint = (INF e\{0 <..}. principal {(x, y). dist x y < e})" + +instance by standard (simp add: uniformity_fbint_def) + +end + + +instance fbint :: open_uniformity +proof + fix U :: "fbint set" + show "open U = (\x\U. eventually (\(x',y). x' = x \ y \ U) uniformity)" + unfolding eventually_uniformity_metric dist_fbint_def + using fb.dist_induces_open by simp +qed + + +instance fbint :: metric_space + by standard (use fb.dist_triangle_ineq in \auto simp: dist_fbint_def\) + +text \ + In particular, we can now show that the sequence \n!\ tends to 0 in the Furstenberg topology: +\ +lemma tendsto_fbint_fact: "(\n. fbint (fact n)) \ fbint 0" +proof - + have "(\n. dist (fbint (fact n)) (fbint 0)) \ 0" + proof (rule tendsto_sandwich[OF always_eventually always_eventually]; safe?) + fix n :: nat + show "dist (fbint (fact n)) (fbint 0) \ 1 / 2 ^ n" + unfolding dist_fbint_def by (transfer fixing: n) (use fb.N_fact_le[of n] in simp) + show "dist (fbint (fact n)) (fbint 0) \ 0" + by simp + show "(\n. 1 / 2 ^ n :: real) \ 0" + by real_asymp + qed simp_all + thus ?thesis + using tendsto_dist_iff by metis +qed + +end \ No newline at end of file diff --git a/thys/Furstenberg_Topology/ROOT b/thys/Furstenberg_Topology/ROOT new file mode 100644 --- /dev/null +++ b/thys/Furstenberg_Topology/ROOT @@ -0,0 +1,13 @@ +chapter AFP + +session Furstenberg_Topology (AFP) = "HOL-Analysis" + + options [timeout = 1200] + sessions + "HOL-Number_Theory" + "HOL-Real_Asymp" + theories + Furstenberg_Topology + document_files + "root.tex" + "root.bib" + diff --git a/thys/Furstenberg_Topology/document/root.bib b/thys/Furstenberg_Topology/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Furstenberg_Topology/document/root.bib @@ -0,0 +1,37 @@ +@article{zulfeqarr, + doi = {10.1007/s12045-019-0837-x}, + url = {https://doi.org/10.1007/s12045-019-0837-x}, + year = {2019}, + month = jul, + publisher = {Springer Science and Business Media {LLC}}, + volume = {24}, + number = {7}, + pages = {755--765}, + author = {Fahed Zulfeqarr}, + title = {Some Interesting Consequences of {F}urstenberg Topology}, + journal = {Resonance} +} + +@misc{dirmeier, + title={On Metrics Inducing the {F}ürstenberg Topology on the Integers}, + author={Alexander Dirmeier}, + year={2019}, + eprint={1912.11663}, + howpublished="\url{https://arxiv.org/abs/1912.11663}", + archivePrefix={arXiv}, + primaryClass={math.GN} +} + +@article{furstenberg, + doi = {10.2307/2307043}, + url = {https://doi.org/10.2307/2307043}, + year = {1955}, + month = may, + publisher = {Informa {UK} Limited}, + volume = {62}, + number = {5}, + pages = {353}, + author = {Harry Furstenberg}, + title = {On the Infinitude of Primes}, + journal = {The American Mathematical Monthly} +} diff --git a/thys/Furstenberg_Topology/document/root.tex b/thys/Furstenberg_Topology/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Furstenberg_Topology/document/root.tex @@ -0,0 +1,41 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} +\usepackage{amsfonts, amsmath, amssymb} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{Furstenberg's Topology And\\ His Proof of the Infinitude of Primes} +\author{Manuel Eberl} +\maketitle + +\begin{abstract} +This article gives a formal version of Furstenberg's topological proof of the infinitude of +primes. He defines a topology on the integers based on arithmetic progressions (or, equivalently, residue classes). +Using some fairly obvious properties of this topology, the infinitude of primes is then easily obtained. + +Apart from this, this topology is also fairly `nice' in general: it is second countable, metrizable, and perfect. All of these (well-known) +facts are formally proven, including an explicit metric for the topology given by Zulfeqarr. +\end{abstract} + +\tableofcontents +\newpage +\parindent 0pt\parskip 0.5ex + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,524 +1,525 @@ AODV Auto2_HOL Auto2_Imperative_HOL AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS AutoFocus-Stream Automatic_Refinement AxiomaticCategoryTheory BDD BNF_Operations Bell_Numbers_Spivey Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BNF_CC Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CYK CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CofGroups Coinductive Coinductive_Languages Collections Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Completeness Complete_Non_Orders Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructor_Funs Containers CoreC++ Core_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series Discrete_Summation DiscretePricing DiskPaxos DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Factored_Transition_System_Bounding Farkas FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Falling_Factorial_Sum FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover +Furstenberg_Topology GPU_Kernel_PL Gabow_SCC Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of Hello_World HereditarilyFinite Hermite Hidden_Markov_Models Higher_Order_Terms Hoare_Time HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interval_Arithmetic_Word32 Iptables_Semantics Irrationality_J_Hancl Isabelle_C Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knot_Theory Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_to_DRA LTL_to_GBA LTL_Master_Theorem Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_KBOs Lambda_Free_RPOs Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Lambda_Free_EPO Launchbury Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Lowe_Ontological_Argument Lower_Semicontinuous Lp MFMC_Countable MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mersenne_Primes MFOTL_Monitor MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multirelations Multi_Party_Computation Myhill-Nerode Name_Carrying_Type_Inference Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions Open_Induction OpSets Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinals_and_Cardinals Ordinary_Differential_Equations PCF PLM Pell POPLmark-deBruijn PSemigroupsConvolution Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Perfect-Number-Thm Perron_Frobenius Pi_Calculus Pi_Transcendental Planarity_Certificates Polynomial_Factorization Polynomial_Interpolation Polynomials Poincare_Bendixson Poincare_Disc Pop_Refinement Posix-Lexing Possibilistic_Noninterference Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Projective_Geometry Program-Conflict-Analysis Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Randomised_BSTs Random_Graph_Subgraph_Threshold Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regular-Sets Regular_Algebras Relation_Algebra Relational-Incorrectness-Logic Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Root_Balanced_Tree Routing Roy_Floyd_Warshall Safe_OCL SATSolverVerification SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Smooth_Manifolds Sort_Encodings Source_Coding_Theorem Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares SuperCalc Surprise_Paradox Symmetric_Polynomials Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Universal_Turing_Machine UPF UPF_Firewall UpDown_Scheme UTP Valuation VectorSpace VeriComp Verified-Prover VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval WOOT_Strong_Eventual_Consistency Word_Lib WorkerWrapper XML Zeta_Function Zeta_3_Irrational ZFC_in_HOL pGCL