Theory Padic_Int_Topology
theory Padic_Int_Topology
imports Padic_Integers Function_Ring
begin
type_synonym padic_int_seq = "nat ⇒ padic_int"
type_synonym padic_int_fun = "padic_int ⇒ padic_int"
sublocale padic_integers < FunZp?: U_function_ring "Zp"
unfolding U_function_ring_def
by (simp add: R.ring_axioms)
context padic_integers
begin
section‹Sequences over Zp›
text‹
The $p$-adic valuation can be thought of as equivalent to the $p$-adic absolute value, but with
the notion of size inverted so that small numbers have large valuation, and zero has maximally
large valuation. The $p$-adic distance between two points is just the valuation of the difference
of those points, and is thus equivalent to the metric induced by the $p$-adic absolute value.
For background on valuations and absolute values for $p$-adic rings see \<^cite>‹"engler2005valued"›.
In what follows, we develop the topology of the $p$-adic from a valuative perspective rather than
a metric perspective. Though equivalent to the metric approach in the $p$-adic case, this
approach is more general in that there exist valued rings whose valuations take values in
non-Archimedean ordered ablelian groups which do not embed into the real numbers.
›
subsection‹The Valuative Distance Function on $\mathbb{Z}_p$›
text‹
The following lemmas establish that the $p$-adic distance function satifies the standard
properties of an ultrametric. It is symmetric, obeys the ultrametric inequality, and only
identical elements are infinitely close.
›
definition val_Zp_dist :: "padic_int ⇒ padic_int ⇒ eint" where
"val_Zp_dist a b ≡ val_Zp (a ⊖ b)"
lemma val_Zp_dist_sym:
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
shows "val_Zp_dist a b = val_Zp_dist b a"
proof-
have 1: "a ⊖ b = ⊖ (b ⊖ a)" using assms(1) assms(2)
using minus_a_inv by blast
then show ?thesis
using R.minus_closed Zp_def assms(1) assms(2) padic_integers.val_Zp_of_minus
padic_integers_axioms val_Zp_dist_def by auto
qed
lemma val_Zp_dist_ultrametric:
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "c ∈ carrier Zp"
shows "val_Zp_dist b c ≥ min (val_Zp_dist a c) (val_Zp_dist a b)"
proof-
let ?X = "b ⊖ a"
let ?Y = "a ⊖ c"
let ?Z = "b ⊖ c"
have 0: "?Z = ?X ⊕ ?Y"
using R.add.m_comm assms(1) assms(2) assms(3) R.plus_diff_simp by auto
have 4: "val_Zp ?Z ≥ min (val_Zp ?X) (val_Zp ?Y)"
using "0" assms(1) assms(2) assms(3) val_Zp_ultrametric by auto
then show ?thesis
using assms val_Zp_dist_sym
unfolding val_Zp_dist_def
by (simp add: min.commute)
qed
lemma val_Zp_dist_infty:
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "val_Zp_dist a b = ∞"
shows "a = b"
using assms unfolding val_Zp_dist_def
by (metis R.r_right_minus_eq not_eint_eq val_ord_Zp)
lemma val_Zp_dist_infty':
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "a = b"
shows "val_Zp_dist a b = ∞"
using assms unfolding val_Zp_dist_def
by (simp add: val_Zp_def)
text‹
The following property will be useful in the proof of Hensel's Lemma: two $p$-adic integers are
close together if and only if their residues are equal at high orders.
›
lemma val_Zp_dist_res_eq:
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "val_Zp_dist a b > k"
shows "(a k) = (b k)"
using assms(1) assms(2) assms(3) val_Zp_dist_def
by (simp add: Zp_residue_eq)
lemma val_Zp_dist_res_eq2:
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "(a k) = (b k)"
shows "val_Zp_dist a b ≥ k"
using assms(1) assms(2) assms(3) Zp_residue_eq2
unfolding val_Zp_dist_def
by (simp add: val_Zp_def)
lemma val_Zp_dist_triangle_eqs:
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "c ∈ carrier Zp"
assumes "val_Zp_dist a b > n"
assumes "val_Zp_dist a c > n"
assumes "(k::nat) < n"
shows "a k = b k"
"a k = c k"
"b k = c k"
unfolding val_Zp_dist_def
proof-
show 0: "a k = b k"
using assms(1) assms(2) assms(4) assms(6) val_Zp_dist_res_eq
by (metis less_imp_le_nat p_residue_padic_int)
show 1: "a k = c k"
using assms(1) assms(3) assms(5) assms(6) val_Zp_dist_res_eq
by (meson eint_ord_simps(1) le_less_trans less_imp_triv not_less of_nat_le_iff)
show "b k = c k"
using 0 1 by auto
qed
subsection‹Cauchy Sequences›
text‹
The definition of Cauchy sequence here is equivalent to standard the metric notion, and is
identical to the one found on page 50 of \<^cite>‹"engler2005valued"›.
›
lemma closed_seqs_diff_closed:
assumes "s ∈ closed_seqs Zp"
assumes "a ∈ carrier Zp"
shows "s m ⊖ a ∈ carrier Zp"
using assms
by (simp add: closed_seqs_memE)
definition is_Zp_cauchy :: "padic_int_seq ⇒ bool" where
"is_Zp_cauchy s = ((s ∈ closed_seqs Zp) ∧ (∀ (n::int). ∃ (N::nat). ∀ m k::nat.
(m>N ∧ k>N ⟶ (val_Zp_dist (s m) (s k)) > eint n)))"
text‹Relation for a sequence which converges to a point:›
definition Zp_converges_to :: "padic_int_seq ⇒ padic_int ⇒ bool" where
"Zp_converges_to s a = ((a ∈ carrier Zp ∧ s ∈ closed_seqs Zp)
∧ (∀(n::int). (∃(k:: nat). (∀( m::nat).
(m > k ⟶ (val_Zp ((s m) ⊖ a)) > eint n) ))))"
lemma is_Zp_cauchy_imp_closed:
assumes "is_Zp_cauchy s"
shows "s ∈ closed_seqs Zp"
using assms unfolding is_Zp_cauchy_def by blast
text‹
Analogous to the lemmas about residues and $p$-adic distances, we can characterize Cauchy
sequences without reference to a distance function: a sequence is Cauchy if and only if for
every natural number $k$, the $k^{th}$ residues of the elements in the sequence are eventually
all equal.
›
lemma is_Zp_cauchy_imp_res_eventually_const_0:
assumes "is_Zp_cauchy s"
fixes n::nat
obtains N where "⋀ n0 n1. n0 > N ∧ n1 > N ⟹ (s n0) n = (s n1) n"
proof-
have "∃ (N::nat). ∀ m k::nat. (m>N ∧ k>N ⟶ (val_Zp_dist (s m) (s k)) > (int n))"
using assms is_Zp_cauchy_def by blast
then obtain N where P0: " ∀ m k::nat. (m>N ∧ k>N ⟶ (val_Zp_dist (s m) (s k)) > (int n))"
by blast
have P1: "⋀ n0 n1. n0 > N ∧ n1 > N ⟹ (s n0) n = (s n1) n"
proof-
fix n0 n1
assume A: "n0 > N ∧ n1 > N"
have "(n0>N ∧ n1>N ⟶ (val_Zp_dist (s n0) (s n1)) > (int n))"
using P0 by blast
then have C0: "(val_Zp_dist (s n0) (s n1)) > (int n)"
using A by blast
show "(s n0) n = (s n1) n"
proof-
have A0: "(val_Zp_dist (s n0) (s n1)) > (int n)"
using C0 by blast
have A1: "s n0 ∈ carrier Zp"
using is_Zp_cauchy_imp_closed[of s] assms
by (simp add: closed_seqs_memE)
have A2: "s n1 ∈ carrier Zp"
using is_Zp_cauchy_def assms closed_seqs_memE[of _ Zp]
by blast
show ?thesis
using A0 val_Zp_dist_res_eq A1 A2 by metis
qed
qed
then show ?thesis
using that by blast
qed
lemma is_Zp_cauchyI:
assumes "s ∈ closed_seqs Zp"
assumes "⋀ n. (∃N. (∀ n0 n1. n0 > N ∧ n1 > N ⟶ (s n0) n = (s n1) n))"
shows "is_Zp_cauchy s"
proof-
have "(∀ (n::int). ∃ (N::nat). ∀ m k::nat. (m>N ∧ k>N ⟶ (val_Zp_dist (s m) (s k)) > n))"
proof
fix n
show "∃ (N::nat). ∀ m k::nat. (m>N ∧ k>N ⟶ (val_Zp_dist (s m) (s k)) > eint n)"
proof-
have "(∃N. (∀ n0 n1. n0 > N ∧ n1 > N ⟶ (s n0) (Suc (nat n)) = (s n1) (Suc (nat n))))"
using assms(2) by blast
then obtain N where N_def: "(∀ n0 n1. n0 > N ∧ n1 > N ⟶ (s n0) (Suc (nat n)) = (s n1) (Suc (nat n)))"
by blast
have 0: "n ≤ eint (int (nat n))"
by simp
have "∀m k. N < m ∧ N < k ⟶ (nat n) < val_Zp_dist (s m) (s k)"
proof
fix m
show "∀k. N < m ∧ N < k ⟶ int (nat n) < val_Zp_dist (s m) (s k)"
proof
fix k
show "N < m ∧ N < k ⟶ int(nat n) < val_Zp_dist (s m) (s k)"
proof
assume A: "N < m ∧ N < k"
then have E: "(s m) (Suc(nat n)) = (s k) (Suc(nat n))"
using N_def by blast
then show " int (nat n) < val_Zp_dist (s m) (s k)"
proof-
have 0: "(s m) ∈ carrier Zp"
by (simp add: assms(1) closed_seqs_memE)
have 1: "(s k) ∈ carrier Zp"
using Zp_def assms(1) closed_seqs_memE[of _ Zp] padic_integers_axioms by blast
have "int (Suc (nat n)) ≤ val_Zp_dist (s m) (s k)"
using E 0 1 val_Zp_dist_res_eq[of "(s m)" "(s k)" "Suc (nat n)"] val_Zp_dist_res_eq2
by blast
then have "int (nat n) < val_Zp_dist (s m) (s k)"
by (metis Suc_ile_eq add.commute of_nat_Suc)
then show ?thesis
by blast
qed
qed
qed
qed
hence "∀m k. N < m ∧ N < k ⟶ n < val_Zp_dist (s m) (s k)"
using 0
by (simp add: order_le_less_subst2)
thus ?thesis by blast
qed
qed
then show ?thesis
using is_Zp_cauchy_def assms by blast
qed
lemma is_Zp_cauchy_imp_res_eventually_const:
assumes "is_Zp_cauchy s"
fixes n::nat
obtains N r where "r ∈ carrier (Zp_res_ring n)" and "⋀ m. m > N ⟹ (s m) n = r"
proof-
obtain N where A0: "⋀ n0 n1. n0 > N ∧ n1 > N ⟹ (s n0) n = (s n1) n"
using assms is_Zp_cauchy_imp_res_eventually_const_0 padic_integers_axioms by blast
obtain r where A1: "s (Suc N) n = r"
by simp
have 0: "r ∈ carrier (Zp_res_ring n)"
using Zp_def ‹s (Suc N) n = r› assms closed_seqs_memE[of _ Zp]
is_Zp_cauchy_def padic_integers_axioms residues_closed
by blast
have 1: "⋀ m. m > N ⟹ (s m) n = r"
proof-
fix m
assume " m > N"
then show "(s m) n = r"
using A0 A1 by blast
qed
then show ?thesis
using 0 1 that by blast
qed
text‹
This function identifies the eventual residues of the elements of a cauchy sequence.
Since a $p$-adic integer is defined to be the map which identifies its residues, this map
will turn out to be precisely the limit of a cauchy sequence.
›
definition res_lim :: "padic_int_seq ⇒ padic_int" where
"res_lim s = (λ k. (THE r. (∃N. (∀ m. m > N ⟶ (s m) k = r))))"
lemma res_lim_Zp_cauchy_0:
assumes "is_Zp_cauchy s"
assumes "f = (res_lim s) k"
shows "(∃N. (∀ m. (m > N ⟶ (s m) k = f)))"
"f ∈ carrier (Zp_res_ring k)"
proof-
obtain N r where P0: "r ∈ carrier (Zp_res_ring k)" and P1: "⋀ m. m > N ⟹ (s m) k = r"
by (meson assms(1) is_Zp_cauchy_imp_res_eventually_const)
obtain P where P_def: "P = (λ x. (∃N. (∀ m. m > N ⟶ (s m) k = x)))"
by simp
have 0: "P r"
using P1 P_def by auto
have 1: "(⋀x. P x ⟹ x = r)"
proof-
fix x
assume A_x: "P x"
obtain N0 where "(∀ m. m > N0 ⟶ (s m) k = x)"
using A_x P_def by blast
let ?M = "max N0 N"
have C0: "s (Suc ?M) k = x"
by (simp add: ‹∀m>N0. s m k = x›)
have C1: "s (Suc ?M) k = r"
by (simp add: P1)
show "x = r"
using C0 C1 by auto
qed
have R: "r = (THE x. P x)"
using the_equality 0 1 by metis
have "(res_lim s) k = (THE r. ∃N. ∀m>N. s m k = r)"
using res_lim_def by simp
then have "f = (THE r. ∃N. ∀m>N. s m k = r)"
using assms by auto
then have "f = (THE r. P r)"
using P_def by auto
then have "r = f"
using R by auto
then show "(∃N. (∀ m. (m > N ⟶ (s m) k = f)))" using 0 P_def
by blast
show "f ∈ carrier (Zp_res_ring k)"
using P0 ‹r = f› by auto
qed
lemma res_lim_Zp_cauchy:
assumes "is_Zp_cauchy s"
obtains N where "⋀ m. (m > N ⟶ (s m) k = (res_lim s) k)"
using res_lim_Zp_cauchy_0 assms by presburger
lemma res_lim_in_Zp:
assumes "is_Zp_cauchy s"
shows "res_lim s ∈ carrier Zp"
proof-
have "res_lim s ∈ padic_set p"
proof(rule padic_set_memI)
show "⋀m. res_lim s m ∈ carrier (residue_ring (p^ m))"
using res_lim_Zp_cauchy_0 by (simp add: assms)
show "⋀m n. m < n ⟹ residue (p^ m) (res_lim s n) = res_lim s m"
proof-
fix m n
obtain N where N0: "⋀ l. (l > N ⟶ (s l) m = (res_lim s) m)"
using assms res_lim_Zp_cauchy by blast
obtain M where M0: "⋀ l. (l > M ⟶ (s l) n = (res_lim s) n)"
using assms prod.simps(2) res_lim_Zp_cauchy by auto
obtain K where K_def: "K = max M N"
by simp
have Km: "⋀ l. (l > K ⟶ (s l) m = (res_lim s) m)"
using K_def N0 by simp
have Kn: "⋀ l. (l > K ⟶ (s l) n = (res_lim s) n)"
using K_def M0 by simp
assume "m < n"
show "residue (p^ m) (res_lim s n) = res_lim s m"
proof-
obtain l where l_def: "l = Suc K"
by simp
have ln: "(res_lim s n) = (s l) n"
by (simp add: Kn l_def)
have lm: "(res_lim s m) = (s l) m"
by (simp add: Km l_def)
have s_car: "s l ∈ carrier Zp"
using assms is_Zp_cauchy_def closed_seqs_memE[of _ Zp] by blast
then show ?thesis
using s_car lm ln ‹m < n› p_residue_def p_residue_padic_int by auto
qed
qed
qed
then show ?thesis
by (simp add: Zp_def padic_int_simps(5))
qed
subsection‹Completeness of $\mathbb{Z}_p$›
text‹
We can use the developments above to show that a sequence of $p$-adic integers is convergent
if and only if it is cauchy, and that limits of convergent sequences are always unique.
›
lemma is_Zp_cauchy_imp_has_limit:
assumes "is_Zp_cauchy s"
assumes "a = res_lim s"
shows "Zp_converges_to s a"
proof-
have 0: "(a ∈ carrier Zp ∧ s ∈ closed_seqs Zp)"
using assms(1) assms(2) is_Zp_cauchy_def res_lim_in_Zp by blast
have 1: "(∀(n::int). (∃(k:: nat). (∀( m::nat).
(m > k ⟶ (val_Zp ((s m) ⊖ a)) ≥ n))))"
proof
fix n
show "∃k. ∀m>k. eint n ≤ val_Zp (s m ⊖ a)"
proof-
obtain K where K_def: "⋀m. (m > K ⟶ (s m) (nat n) = (res_lim s) (nat n))"
using assms(1) res_lim_Zp_cauchy
by blast
have "∀m>K. n ≤ val_Zp_dist (s m) a"
proof
fix m
show "K < m ⟶ n ≤ val_Zp_dist (s m) a"
proof
assume A: "K < m"
show " n ≤ val_Zp_dist (s m) a"
proof-
have X: "(s m) ∈ carrier Zp"
using "0" closed_seqs_memE[of _ Zp]
by blast
have "(s m) (nat n) = (res_lim s) (nat n)"
using A K_def by blast
then have "(s m) (nat n) = a (nat n)"
using assms(2) by blast
then have "int (nat n) ≤ val_Zp_dist (s m) a"
using X val_Zp_dist_res_eq2 "0" by blast
then show ?thesis
by (metis eint_ord_simps(1) int_ops(1) less_not_sym nat_eq_iff2 not_le order_trans zero_eint_def)
qed
qed
qed
then show ?thesis
using val_Zp_dist_def by auto
qed
qed
then show ?thesis using
"0" Zp_converges_to_def
by (metis Suc_ile_eq val_Zp_dist_def)
qed
lemma convergent_imp_Zp_cauchy:
assumes "s ∈ closed_seqs Zp"
assumes "a ∈ carrier Zp"
assumes "Zp_converges_to s a"
shows "is_Zp_cauchy s"
apply(rule is_Zp_cauchyI)
using assms apply simp
proof-
fix n
show "∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ s n0 n = s n1 n "
proof-
obtain k where k_def:"∀m>k. n < val_Zp_dist (s m) a"
using assms val_Zp_dist_def
unfolding Zp_converges_to_def
by presburger
have A0: "∀n0 n1. k < n0 ∧ k < n1 ⟶ s n0 n = s n1 n "
proof- have "⋀n0 n1. k < n0 ∧ k < n1 ⟶ s n0 n = s n1 n"
proof
fix n0 n1
assume A: " k < n0 ∧ k < n1"
show " s n0 n = s n1 n "
proof-
have 0: "n < val_Zp_dist (s n0) a"
using k_def using A
by blast
have 1: "n < val_Zp_dist (s n1) a"
using k_def using A
by blast
hence 2: "(s n0) n = a n"
using 0 assms val_Zp_dist_res_eq[of "s n0" a n] closed_seqs_memE
by blast
hence 3: "(s n1) n = a n"
using 1 assms val_Zp_dist_res_eq[of "s n1" a n] closed_seqs_memE
by blast
show ?thesis
using 2 3
by auto
qed
qed
thus ?thesis by blast
qed
show ?thesis
using A0
by blast
qed
qed
lemma unique_limit:
assumes "s ∈ closed_seqs Zp"
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "Zp_converges_to s a"
assumes "Zp_converges_to s b"
shows "a = b"
proof-
have "⋀k. a k = b k"
proof-
fix k::nat
obtain k0 where k0_def:"∀m>k0. k < val_Zp_dist (s m) a"
using assms unfolding val_Zp_dist_def Zp_converges_to_def
by blast
obtain k1 where k1_def:"∀m>k1. k < val_Zp_dist (s m) b"
using assms unfolding val_Zp_dist_def Zp_converges_to_def
by blast
have k0_prop: "⋀m. m> k0 ⟹ (s m) k = a k" proof- fix m assume A: "m > k0"
then show "(s m) k = a k"
using k0_def assms closed_seqs_memE[of s Zp] val_Zp_dist_res_eq[of _ a k] of_nat_Suc
by blast
qed
have k1_prop: "⋀m. m> k1 ⟹ (s m) k = b k"
using k1_def assms closed_seqs_memE[of s Zp]
by (simp add: val_Zp_dist_res_eq)
have "⋀ m. m > (max k0 k1) ⟹ a k = b k"
using k0_prop k1_prop
by force
then show "a k = b k"
by blast
qed
then show ?thesis
by blast
qed
lemma unique_limit':
assumes "s ∈ closed_seqs Zp"
assumes "a ∈ carrier Zp"
assumes "Zp_converges_to s a"
shows "a = res_lim s"
using unique_limit[of s a "res_lim s"] assms
convergent_imp_Zp_cauchy is_Zp_cauchy_imp_has_limit res_lim_in_Zp
by blast
lemma Zp_converges_toE:
assumes "s ∈ closed_seqs Zp"
assumes "a ∈ carrier Zp"
assumes "Zp_converges_to s a"
shows "∃N. ∀k > N. s k n = a n"
by (metis assms(1) assms(2) assms(3)
convergent_imp_Zp_cauchy
res_lim_Zp_cauchy unique_limit')
lemma Zp_converges_toI:
assumes "s ∈ closed_seqs Zp"
assumes "a ∈ carrier Zp"
assumes "⋀n. ∃N. ∀k > N. s k n = a n"
shows "Zp_converges_to s a"
proof-
have 0: "(a ∈ carrier Zp ∧ s ∈ closed_seqs Zp)"
using assms
by auto
have 1: "(∀n::int. ∃k. ∀m>k. n < val_Zp_dist (s m) a) "
proof
fix n::int
show "∃k. ∀m>k. n < val_Zp_dist (s m) a "
proof(cases "n < 0")
case True
have "∀m>0. n < val_Zp_dist (s m) a "
proof
fix m ::nat
show "0 < m ⟶ n < val_Zp_dist (s m) a"
proof
have 0: "eint n < 0"
by (simp add: True zero_eint_def)
have 1: " s m ⊖ a ∈ carrier Zp"
using assms
by (simp add: closed_seqs_diff_closed)
thus " n < val_Zp_dist (s m) a"
using 0 True val_pos[of "s m ⊖ a"]
unfolding val_Zp_dist_def
by auto
qed
qed
then show ?thesis
by blast
next
case False
then have P0: "n ≥ 0"
by auto
obtain N where N_def: "∀k > N. s k (Suc (nat n)) = a (Suc (nat n))"
using assms by blast
have "∀m>N. n < val_Zp_dist (s m) a "
proof
fix m
show " N < m ⟶ n < val_Zp_dist (s m) a"
proof
assume A: "N < m"
then have A0: "s m (Suc (nat n)) = a (Suc (nat n))"
using N_def by blast
have "(Suc (nat n)) ≤ val_Zp_dist (s m) a"
using assms A0 val_Zp_dist_res_eq2[of "s m" a "Suc (nat n)"] closed_seqs_memE
by blast
thus "n < val_Zp_dist (s m) a"
using False
by (meson P0 eint_ord_simps(2) less_Suc_eq less_le_trans nat_less_iff)
qed
qed
then show ?thesis
by blast
qed
qed
show ?thesis
unfolding Zp_converges_to_def
using 0 1
by (simp add: val_Zp_dist_def)
qed
text‹Sums and products of cauchy sequences are cauchy:›
lemma sum_of_Zp_cauchy_is_Zp_cauchy:
assumes "is_Zp_cauchy s"
assumes "is_Zp_cauchy t"
shows "is_Zp_cauchy (s ⊕⇘Zp⇗ω⇖⇙ t)"
proof(rule is_Zp_cauchyI)
show "(s ⊕⇘Zp⇗ω⇖⇙ t) ∈ closed_seqs Zp"
using assms seq_plus_closed is_Zp_cauchy_def by blast
show "⋀n. ∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ (s ⊕⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊕⇘Zp⇗ω⇖⇙ t) n1 n"
proof-
fix n
show "∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ (s ⊕⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊕⇘Zp⇗ω⇖⇙ t) n1 n"
proof-
obtain N1 where N1_def: "∀n0 n1. N1 < n0 ∧ N1 < n1 ⟶ s n0 n = s n1 n"
using assms(1) is_Zp_cauchy_imp_res_eventually_const_0 padic_integers_axioms by blast
obtain N2 where N2_def: "∀n0 n1. N2 < n0 ∧ N2 < n1 ⟶ t n0 n = t n1 n"
using assms(2) is_Zp_cauchy_imp_res_eventually_const_0 padic_integers_axioms by blast
obtain M where M_def: "M = max N1 N2"
by simp
have "∀n0 n1. M < n0 ∧ M < n1 ⟶ (s ⊕⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊕⇘Zp⇗ω⇖⇙ t) n1 n"
proof
fix n0
show "∀n1. M < n0 ∧ M < n1 ⟶ (s ⊕⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊕⇘Zp⇗ω⇖⇙ t) n1 n"
proof
fix n1
show " M < n0 ∧ M < n1 ⟶ (s ⊕⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊕⇘Zp⇗ω⇖⇙ t) n1 n"
proof
assume A: "M < n0 ∧ M < n1 "
have Fs: " s n0 n = s n1 n" using A M_def N1_def by auto
have Ft: " t n0 n = t n1 n" using A M_def N2_def by auto
then show "(s ⊕⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊕⇘Zp⇗ω⇖⇙ t) n1 n"
using seq_plus_simp[of s t] assms
by (simp add: Fs is_Zp_cauchy_imp_closed residue_of_sum)
qed
qed
qed
then show ?thesis
by blast
qed
qed
qed
lemma prod_of_Zp_cauchy_is_Zp_cauchy:
assumes "is_Zp_cauchy s"
assumes "is_Zp_cauchy t"
shows "is_Zp_cauchy (s ⊗⇘Zp⇗ω⇖⇙ t)"
proof(rule is_Zp_cauchyI)
show "(s ⊗⇘Zp⇗ω⇖⇙ t) ∈ closed_seqs Zp"
using assms(1) assms(2) is_Zp_cauchy_def seq_mult_closed by auto
show "⋀n. ∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ (s ⊗⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊗⇘Zp⇗ω⇖⇙ t) n1 n"
proof-
fix n
show "∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ (s ⊗⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊗⇘Zp⇗ω⇖⇙ t) n1 n"
proof-
obtain N1 where N1_def: "∀n0 n1. N1 < n0 ∧ N1 < n1 ⟶ s n0 n = s n1 n"
using assms(1) is_Zp_cauchy_imp_res_eventually_const_0 padic_integers_axioms by blast
obtain N2 where N2_def: "∀n0 n1. N2 < n0 ∧ N2 < n1 ⟶ t n0 n = t n1 n"
using assms(2) is_Zp_cauchy_imp_res_eventually_const_0 padic_integers_axioms by blast
obtain M where M_def: "M = max N1 N2"
by simp
have "∀n0 n1. M < n0 ∧ M < n1 ⟶ (s ⊗⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊗⇘Zp⇗ω⇖⇙ t) n1 n"
proof
fix n0
show "∀n1. M < n0 ∧ M < n1 ⟶ (s ⊗⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊗⇘Zp⇗ω⇖⇙ t) n1 n"
proof
fix n1
show " M < n0 ∧ M < n1 ⟶ (s ⊗⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊗⇘Zp⇗ω⇖⇙ t) n1 n"
proof
assume A: "M < n0 ∧ M < n1 "
have Fs: " s n0 n = s n1 n" using A M_def N1_def by auto
have Ft: " t n0 n = t n1 n" using A M_def N2_def by auto
then show "(s ⊗⇘Zp⇗ω⇖⇙ t) n0 n = (s ⊗⇘Zp⇗ω⇖⇙ t) n1 n"
using seq_mult_simp[of s t] is_Zp_cauchy_imp_closed assms
by (simp add: Fs residue_of_prod)
qed
qed
qed
then show ?thesis
by blast
qed
qed
qed
text‹Constant sequences are cauchy:›
lemma constant_is_Zp_cauchy:
assumes "is_constant_seq Zp s"
shows "is_Zp_cauchy s"
proof(rule is_Zp_cauchyI)
show "s ∈ closed_seqs Zp"
proof(rule closed_seqs_memI)
fix k
show "s k ∈ carrier Zp"
using assms is_constant_seq_imp_closed
by (simp add: is_constant_seq_imp_closed closed_seqs_memE)
qed
obtain x where "⋀ k. s k = x"
using assms
by (meson is_constant_seqE)
then show "⋀n. ∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ s n0 n = s n1 n"
by simp
qed
text‹Scalar multiplies of cauchy sequences are cauchy:›
lemma smult_is_Zp_cauchy:
assumes "is_Zp_cauchy s"
assumes "a ∈ carrier Zp"
shows "is_Zp_cauchy (a ⊙⇘Zp⇗ω⇖⇙ s)"
apply(rule is_Zp_cauchyI)
apply (meson U_function_ring.ring_seq_smult_closed U_function_ring_axioms assms(1) assms(2) is_Zp_cauchy_def)
using assms ring_seq_smult_eval[of s a] is_Zp_cauchy_imp_closed[of s]
by (metis res_lim_Zp_cauchy residue_of_prod)
lemma Zp_cauchy_imp_approaches_res_lim:
assumes "is_Zp_cauchy s"
assumes "a = res_lim s"
obtains N where "⋀n. n> N ⟹ val_Zp (a ⊖ (s n)) > eint k"
proof-
have " (∀n::int. ∃k. ∀m>k. n < val_Zp_dist (s m) a)"
using Zp_converges_to_def[of s a] assms is_Zp_cauchy_imp_has_limit[of s a] val_Zp_dist_def
by simp
then have "∃N. ∀m>N. k < val_Zp_dist (s m) a"
by blast
then obtain N where N_def: "∀m>N. k < val_Zp_dist (s m) a"
by blast
have "⋀n. n> N ⟹ val_Zp (a ⊖ (s n)) > k"
proof-
fix m
assume "m > N"
then have 0: "k < val_Zp_dist (s m) a"
using N_def
by (simp add: val_Zp_def)
show "k < val_Zp (a ⊖ s m)"
using "0" assms(1) assms(2) is_Zp_cauchy_def closed_seqs_memE[of _ Zp] val_Zp_dist_def val_Zp_dist_sym res_lim_in_Zp by auto
qed
then show ?thesis
using that
by blast
qed
section‹Continuous Functions›
text‹
For convenience, we will use a slightly unorthodox definition of continuity here.
Since $\mathbb{Z}_p$ is complete, a function is continuous if and only if its compositions
with cauchy sequences are cauchy sequences. Thus we can define a continuous function on
$\mathbb{Z}_p$ as a function which carries cauchy sequences to cauchy sequences under
composition. Note that this does not generalize to a definition of continuity for functions
defined on incomplete subsets of $\mathbb{Z}_p$. For example, the function $1/x$ defined on
$\mathbb{Z}_p - \{0\}$ clearly does not have this property but is continuous. However, towards
a proof of Hensel's Lemma we will only need to consider polynomial functions and so this
definition suffices for our purposes.
›
subsection‹Defining Continuous Functions and Basic Examples›
abbreviation Zp_constant_function ("𝔠⇘Zp⇙") where
"𝔠⇘Zp⇙ a ≡ constant_function (carrier Zp) a"
definition is_Zp_continuous ::"padic_int_fun ⇒ bool" where
"is_Zp_continuous f = (f ∈ carrier (Fun Zp) ∧(∀ s. is_Zp_cauchy s ⟶ is_Zp_cauchy(f ∘ s)))"
lemma Zp_continuous_is_Zp_closed:
assumes "is_Zp_continuous f"
shows "f ∈ carrier (Fun Zp)"
using assms is_Zp_continuous_def by blast
lemma is_Zp_continuousI:
assumes "f ∈ carrier (Fun Zp)"
assumes "⋀s. is_Zp_cauchy s ⟹ is_Zp_cauchy (f ∘ s)"
shows "is_Zp_continuous f"
proof-
have "(∀ s. is_Zp_cauchy s ⟶ is_Zp_cauchy(f ∘ s))"
proof
fix s
show "is_Zp_cauchy s ⟶ is_Zp_cauchy (f ∘ s) "
by (simp add: assms(2))
qed
then show ?thesis
using assms(1) is_Zp_continuous_def by blast
qed
lemma Zp_continuous_is_closed:
assumes "is_Zp_continuous f"
shows "f ∈ carrier (Fun Zp)"
using assms unfolding is_Zp_continuous_def by blast
lemma constant_is_Zp_continuous:
assumes "a ∈ carrier Zp"
shows "is_Zp_continuous (const a)"
proof(rule is_Zp_continuousI)
show "𝔠⇘Zp⇙ a ∈ carrier (function_ring (carrier Zp) Zp)"
by (simp add: assms constant_function_closed)
show "⋀s. is_Zp_cauchy s ⟹ is_Zp_cauchy (𝔠⇘Zp⇙ a ∘ s) "
proof-
fix s
assume A: "is_Zp_cauchy s"
have "is_constant_seq Zp (𝔠⇘Zp⇙ a ∘ s)"
using constant_function_comp_is_constant_seq[of a s] A assms
is_Zp_cauchy_imp_closed by blast
then show "is_Zp_cauchy (𝔠⇘Zp⇙ a ∘ s)"
using A assms constant_is_Zp_cauchy
by blast
qed
qed
lemma sum_of_cont_is_cont:
assumes "is_Zp_continuous f"
assumes "is_Zp_continuous g"
shows "is_Zp_continuous (f ⊕⇘Fun Zp⇙ g)"
apply(rule is_Zp_continuousI)
using assms Zp_continuous_is_closed assms function_sum_comp_is_seq_sum[of _ f g]
apply (simp add: fun_add_closed)
using assms(1) assms(2) function_sum_comp_is_seq_sum is_Zp_cauchy_def is_Zp_continuous_def sum_of_Zp_cauchy_is_Zp_cauchy by auto
lemma prod_of_cont_is_cont:
assumes "is_Zp_continuous f"
assumes "is_Zp_continuous g"
shows "is_Zp_continuous (f ⊗⇘Fun Zp⇙ g)"
apply(rule is_Zp_continuousI)
using assms Zp_continuous_is_closed assms
apply (simp add: fun_mult_closed)
using function_mult_comp_is_seq_mult[of _ f g] assms(1) assms(2) is_Zp_cauchy_imp_closed
is_Zp_continuous_def prod_of_Zp_cauchy_is_Zp_cauchy by auto
lemma smult_is_continuous:
assumes "is_Zp_continuous f"
assumes "a ∈ carrier Zp"
shows "is_Zp_continuous (a ⊙⇘Fun Zp⇙ f)"
apply(rule is_Zp_continuousI)
using assms apply (simp add: assms function_smult_closed is_Zp_continuous_def)
using ring_seq_smult_comp_assoc assms
by (simp add: is_Zp_cauchy_imp_closed is_Zp_continuous_def smult_is_Zp_cauchy)
lemma id_Zp_is_Zp_continuous:
"is_Zp_continuous ring_id"
apply(rule is_Zp_continuousI)
by (auto simp add: is_Zp_cauchy_imp_closed ring_id_seq_comp)
lemma nat_pow_is_Zp_continuous:
assumes "is_Zp_continuous f"
shows "is_Zp_continuous (f[^]⇘Fun Zp⇙(n::nat))"
apply(induction n)
using constant_is_Zp_continuous function_one_is_constant apply force
by (simp add: assms prod_of_cont_is_cont)
lemma ring_id_pow_closed:
"(ring_id)[^]⇘Fun Zp⇙ (n::nat) ∈ carrier (Fun Zp)"
by (simp add: function_ring_is_monoid monoid.nat_pow_closed)
lemma monomial_equation:
assumes "c ∈ carrier Zp"
shows "monomial c n = c ⊙⇘Fun Zp⇙ (ring_id)[^]⇘Fun Zp⇙n"
apply(rule function_ring_car_eqI)
apply (simp add: assms monomial_functions)
using assms function_smult_closed[of c "ring_id [^]⇘Fun Zp⇙ n"] ring_id_pow_closed apply blast
unfolding monomial_function_def
using assms function_smult_eval[of c "(ring_id)[^]⇘Fun Zp⇙ (n::nat)"]
function_nat_pow_eval[of ring_id _ n]
by (simp add: ring_id_eval ring_id_pow_closed)
lemma monomial_is_Zp_continuous:
assumes "c ∈ carrier Zp"
shows "is_Zp_continuous (monomial c n)"
using monomial_equation[of c n] nat_pow_is_Zp_continuous
by (simp add: assms id_Zp_is_Zp_continuous smult_is_continuous)
subsection‹Composition by a Continuous Function Commutes with Taking Limits of Sequences›
text ‹
Due to our choice of definition for continuity, a little bit of care is required to show that
taking the limit of a cauchy sequence commutes with composition by a continuous function.
For a sequence $(s_n)_{n \in \mathbb{N}}$ converging to a point $t$, we can consider the
alternating sequence $(s_0, t, s_1, t, s_2, t, \dots)$ which is also cauchy. Clearly
composition with $f$ yields $(f(s_0), f(t), f(s_1), f(t), f(s_2), f(t), \dots)$ from which
we can see that the limit must be $f(t)$.
›
definition alt_seq where
"alt_seq s = (λk. (if (even k) then (s k) else (res_lim s)))"
lemma alt_seq_Zp_cauchy:
assumes "is_Zp_cauchy s"
shows "is_Zp_cauchy (alt_seq s)"
proof(rule is_Zp_cauchyI)
show "(alt_seq s) ∈ closed_seqs Zp"
unfolding alt_seq_def using assms is_Zp_cauchy_imp_closed
by (simp add: closed_seqs_memE closed_seqs_memI res_lim_in_Zp)
fix n
show "∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ alt_seq s n0 n = alt_seq s n1 n "
proof-
obtain N where N: " ∀n0 n1. N < n0 ∧ N < n1 ⟶ s n0 n = s n1 n "
using assms is_Zp_cauchy_imp_res_eventually_const_0 padic_integers_axioms
by blast
have "alt_seq s n0 n = alt_seq s n1 n"
if "N < n0" "N < n1" for n0 n1
using N apply (auto simp: alt_seq_def)
using that apply blast
apply (metis that(1) assms gt_ex linorder_not_less order_less_le_trans order_less_trans res_lim_Zp_cauchy)
apply (metis that(2) assms gt_ex linorder_neqE_nat order_less_trans res_lim_Zp_cauchy)
done
then show ?thesis
by blast
qed
qed
lemma alt_seq_limit:
assumes "is_Zp_cauchy s"
shows "res_lim(alt_seq s) = res_lim s"
proof-
have "⋀k. res_lim(alt_seq s) k = res_lim s k"
proof-
fix k
obtain N where N_def: "∀ m. m> N ⟶ s m k = res_lim s k"
using assms res_lim_Zp_cauchy
by blast
obtain N' where N'_def: "∀ m. m> N' ⟶ (alt_seq s) m k = res_lim (alt_seq s) k"
using assms res_lim_Zp_cauchy
alt_seq_Zp_cauchy
by blast
have "⋀m. m > (max N N') ⟹ s m k = res_lim (alt_seq s) k"
proof-
fix m
assume A0: "m > (max N N')"
have A1: "s m k = res_lim s k"
using A0 N_def
by simp
have A2: "(alt_seq s) m k = res_lim (alt_seq s) k"
using A0 N'_def
by simp
have A3: "(alt_seq s) m k = res_lim s k"
using alt_seq_def A1 A2
by presburger
show "s m k = res_lim (alt_seq s) k"
using A1 A2 A3
by auto
qed
then have P:"⋀m. m > (max N N') ⟹ (res_lim s k) = res_lim (alt_seq s) k"
using N_def
by auto
show "res_lim(alt_seq s) k = res_lim s k"
using P[of "Suc (max N N')"]
by auto
qed
then show ?thesis
by (simp add: ext)
qed
lemma res_lim_pushforward:
assumes "is_Zp_continuous f"
assumes "is_Zp_cauchy s"
assumes "t = alt_seq s"
shows "res_lim (f ∘ t) = f (res_lim t)"
proof-
have 0: "Zp_converges_to (f ∘ t) (res_lim (f ∘ t))"
using assms alt_seq_Zp_cauchy is_Zp_cauchy_imp_has_limit
is_Zp_continuous_def
by blast
have "⋀k. res_lim (f ∘ t) k = f (res_lim t) k"
proof-
fix k
show "res_lim (f ∘ t) k = f (res_lim t) k"
proof-
obtain N where N_def: "⋀m. m> N ⟹ (f ∘ t) m k = (res_lim (f ∘ t)) k"
using 0
by (meson convergent_imp_Zp_cauchy Zp_converges_to_def res_lim_Zp_cauchy)
obtain M where M_def: "M = 2*(Suc N) + 1"
by simp
have 0: "t M = res_lim s"
using assms
unfolding alt_seq_def
by (simp add: M_def)
have 1: "(f ∘ t) M k = (res_lim (f ∘ t)) k"
using N_def M_def
by auto
have 2: "(f ∘ t) M k = f (t M) k"
by simp
have 3: "(f ∘ t) M k = f (res_lim s) k"
using 0 2 by simp
have 4: "(f ∘ t) M k = f (res_lim t) k"
using 3 assms alt_seq_limit[of s]
by auto
show ?thesis
using 4 1 by auto
qed
qed
then show ?thesis by(simp add: ext)
qed
lemma res_lim_pushforward':
assumes "is_Zp_continuous f"
assumes "is_Zp_cauchy s"
assumes "t = alt_seq s"
shows "res_lim (f ∘ s) = res_lim (f ∘ t)"
proof-
obtain a where a_def: "a = res_lim (f ∘ s)"
by simp
obtain b where b_def: "b = res_lim (f ∘ t)"
by simp
have "⋀k. a k = b k"
proof-
fix k
obtain Na where Na_def: "⋀m. m > Na ⟹ (f ∘ s) m k = a k"
using a_def assms is_Zp_continuous_def
padic_integers_axioms res_lim_Zp_cauchy
by blast
obtain Nb where Nb_def: "⋀m. m > Nb ⟹ (f ∘ t) m k = b k"
using b_def assms is_Zp_continuous_def
padic_integers_axioms res_lim_Zp_cauchy
alt_seq_Zp_cauchy
by blast
obtain M where M_def: "M = 2*(max Na Nb) + 1"
by simp
have M0: "odd M"
by (simp add: M_def)
have M1: "M > Na"
using M_def
by auto
have M2: "M > Nb"
using M_def
by auto
have M3: "t M = res_lim s"
using assms alt_seq_def M0
by auto
have M4: "((f ∘ t) M) = f (res_lim s)"
using M3
by auto
have M5: "((f ∘ t) M) k = b k"
using M2 Nb_def by auto
have M6: "f (res_lim s) = f (res_lim t)"
using assms alt_seq_limit[of s]
by auto
have M7: "f (res_lim t) k = b k"
using M4 M5 M6 by auto
have M8: "(f ∘ s) M k = (f ∘ s) (Suc M) k"
using M1 Na_def by auto
have M9: "(f ∘ s) (Suc M) = (f ∘ t) (Suc M)"
using assms unfolding alt_seq_def
using M_def
by auto
have M10: "(f ∘ t) M k = (f ∘ t) (Suc M) k"
using M2 Nb_def by auto
have M11: "(f ∘ t) M k = (f ∘ s) M k"
using M10 M8 M9 by auto
show "a k = b k"
using M1 M11 M5 Na_def by auto
qed
then show ?thesis using a_def b_def ext[of a b] by auto
qed
lemma continuous_limit:
assumes "is_Zp_continuous f"
assumes "is_Zp_cauchy s"
shows "Zp_converges_to (f ∘ s) (f (res_lim s))"
proof-
obtain t where t_def: "t = alt_seq s"
by simp
have 0: "Zp_converges_to (f ∘ s) (res_lim (f ∘ s))"
using assms(1) assms(2) is_Zp_continuous_def
is_Zp_cauchy_imp_has_limit padic_integers_axioms by blast
have 1: "Zp_converges_to (f ∘ s) (res_lim (f ∘ t))"
using "0" assms(1) assms(2) res_lim_pushforward' t_def by auto
have 2: "Zp_converges_to (f ∘ s) (f (res_lim t))"
using "1" assms(1) assms(2) res_lim_pushforward padic_integers_axioms t_def by auto
then show "Zp_converges_to (f ∘ s) (f (res_lim s))"
by (simp add: alt_seq_limit assms(2) t_def)
qed
end
end