Theory Furstenberg_Topology
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..<b}. arith_prog_fb (a+i) b)"
proof (transfer fixing: b)
fix a :: int
have disjoint: "x ∉ arith_prog a b" if "x ∈ arith_prog (a + int i) b" "i ∈ {1..<b}" for x i
proof -
have "[a ≠ 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}. arith_prog (a + int i) b)" for x
proof -
define i where "i = nat ((x - a) mod (int b))"
have "[a + int i = a + (x - a) mod int b] (mod int b)"
unfolding i_def using ‹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}. arith_prog (a + int i) b)"
by blast
qed
also from ‹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 ∗‹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 ∗‹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
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 Furstenberg 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 ∗‹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)
qed (use q_gt_1 in auto)
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 _ 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 "⋀k. (if k = 0 ∨ int k dvd n then 0 else 1 / q ^ k)
≤ (if k ∈ {0, 1, p', n'} then 0 else (1 / q) ^ k)"
using q_gt_1 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 _ 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⇧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⇧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 Furstenberg 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