author huffman Tue, 29 May 2007 20:31:53 +0200 changeset 23123 e2e370bccde1 parent 23122 3d853d6f2f7d child 23124 892e0a4551da
instance complex :: banach
```--- a/src/HOL/Complex/Complex.thy	Tue May 29 20:31:42 2007 +0200
+++ b/src/HOL/Complex/Complex.thy	Tue May 29 20:31:53 2007 +0200
@@ -457,6 +457,47 @@
lemmas real_sum_squared_expand = power2_sum [where 'a=real]

+subsection {* Completeness of the Complexes *}
+
+interpretation Re: bounded_linear ["Re"]
+apply (unfold_locales, simp, simp)
+apply (rule_tac x=1 in exI)
+done
+
+interpretation Im: bounded_linear ["Im"]
+apply (unfold_locales, simp, simp)
+apply (rule_tac x=1 in exI)
+done
+
+lemma LIMSEQ_Complex:
+  "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
+apply (rule LIMSEQ_I)
+apply (subgoal_tac "0 < r / sqrt 2")
+apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
+apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
+apply (rename_tac M N, rule_tac x="max M N" in exI, safe)
+done
+
+instance complex :: banach
+proof
+  fix X :: "nat \<Rightarrow> complex"
+  assume X: "Cauchy X"
+  from Re.Cauchy [OF X] have 1: "(\<lambda>n. Re (X n)) ----> lim (\<lambda>n. Re (X n))"
+    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
+  from Im.Cauchy [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
+    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
+  have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
+    using LIMSEQ_Complex [OF 1 2] by simp
+  thus "convergent X"
+    by (rule convergentI)
+qed
+
+
subsection{*Exponentiation*}

primrec```