# HG changeset patch
# User huffman
# Date 1243963939 25200
# Node ID 3affcbc60c6d6caa3a44085a9d5adc1653e5bfb3
# Parent  e0c05b595d1f7863dba009ccfe98904b787faaf1
new lemmas

diff -r e0c05b595d1f -r 3affcbc60c6d src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Mon Jun 01 16:59:56 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 10:32:19 2009 -0700
@@ -522,6 +522,125 @@
 
 end
 
+lemma dist_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
+unfolding dist_vector_def
+by (rule member_le_setL2) simp_all
+
+lemma tendsto_Cart_nth:
+  fixes X :: "'a \<Rightarrow> 'b::metric_space ^ 'n::finite"
+  assumes "tendsto (\<lambda>n. X n) a net"
+  shows "tendsto (\<lambda>n. X n $ i) (a $ i) net"
+proof (rule tendstoI)
+  fix e :: real assume "0 < e"
+  with assms have "eventually (\<lambda>n. dist (X n) a < e) net"
+    by (rule tendstoD)
+  thus "eventually (\<lambda>n. dist (X n $ i) (a $ i) < e) net"
+  proof (rule eventually_elim1)
+    fix n :: 'a
+    have "dist (X n $ i) (a $ i) \<le> dist (X n) a"
+      by (rule dist_nth_le)
+    also assume "dist (X n) a < e"
+    finally show "dist (X n $ i) (a $ i) < e" .
+  qed
+qed
+
+lemma LIMSEQ_Cart_nth:
+  "(X ----> a) \<Longrightarrow> (\<lambda>n. X n $ i) ----> a $ i"
+unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth)
+
+lemma LIM_Cart_nth:
+  "(f -- x --> y) \<Longrightarrow> (\<lambda>x. f x $ i) -- x --> y $ i"
+unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth)
+
+lemma Cauchy_Cart_nth:
+  fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n::finite"
+  assumes "Cauchy (\<lambda>n. X n)"
+  shows "Cauchy (\<lambda>n. X n $ i)"
+proof (rule metric_CauchyI)
+  fix e :: real assume "0 < e"
+  obtain M where "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
+    using metric_CauchyD [OF `Cauchy X` `0 < e`] by fast
+  moreover
+  {
+    fix m n
+    assume "M \<le> m" "M \<le> n"
+    have "dist (X m $ i) (X n $ i) \<le> dist (X m) (X n)"
+      by (rule dist_nth_le)
+    also assume "dist (X m) (X n) < e"
+    finally have "dist (X m $ i) (X n $ i) < e" .
+  }
+  ultimately
+  have "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < e" by fast
+  thus "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < e" ..
+qed
+
+lemma LIMSEQ_vector:
+  fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n::finite"
+  assumes X: "\<And>i. (\<lambda>n. X n $ i) ----> (a $ i)"
+  shows "X ----> a"
+proof (rule metric_LIMSEQ_I)
+  fix r :: real assume "0 < r"
+  then have "0 < r / of_nat CARD('n)" (is "0 < ?s")
+    by (simp add: divide_pos_pos)
+  def N \<equiv> "\<lambda>i. LEAST N. \<forall>n\<ge>N. dist (X n $ i) (a $ i) < ?s"
+  def M \<equiv> "Max (range N)"
+  have "\<And>i. \<exists>N. \<forall>n\<ge>N. dist (X n $ i) (a $ i) < ?s"
+    using X `0 < ?s` by (rule metric_LIMSEQ_D)
+  hence "\<And>i. \<forall>n\<ge>N i. dist (X n $ i) (a $ i) < ?s"
+    unfolding N_def by (rule LeastI_ex)
+  hence M: "\<And>i. \<forall>n\<ge>M. dist (X n $ i) (a $ i) < ?s"
+    unfolding M_def by simp
+  {
+    fix n :: nat assume "M \<le> n"
+    have "dist (X n) a = setL2 (\<lambda>i. dist (X n $ i) (a $ i)) UNIV"
+      unfolding dist_vector_def ..
+    also have "\<dots> \<le> setsum (\<lambda>i. dist (X n $ i) (a $ i)) UNIV"
+      by (rule setL2_le_setsum [OF zero_le_dist])
+    also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV"
+      by (rule setsum_strict_mono, simp_all add: M `M \<le> n`)
+    also have "\<dots> = r"
+      by simp
+    finally have "dist (X n) a < r" .
+  }
+  hence "\<forall>n\<ge>M. dist (X n) a < r"
+    by simp
+  then show "\<exists>M. \<forall>n\<ge>M. dist (X n) a < r" ..
+qed
+
+lemma Cauchy_vector:
+  fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n::finite"
+  assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)"
+  shows "Cauchy (\<lambda>n. X n)"
+proof (rule metric_CauchyI)
+  fix r :: real assume "0 < r"
+  then have "0 < r / of_nat CARD('n)" (is "0 < ?s")
+    by (simp add: divide_pos_pos)
+  def N \<equiv> "\<lambda>i. LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"
+  def M \<equiv> "Max (range N)"
+  have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"
+    using X `0 < ?s` by (rule metric_CauchyD)
+  hence "\<And>i. \<forall>m\<ge>N i. \<forall>n\<ge>N i. dist (X m $ i) (X n $ i) < ?s"
+    unfolding N_def by (rule LeastI_ex)
+  hence M: "\<And>i. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < ?s"
+    unfolding M_def by simp
+  {
+    fix m n :: nat
+    assume "M \<le> m" "M \<le> n"
+    have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
+      unfolding dist_vector_def ..
+    also have "\<dots> \<le> setsum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
+      by (rule setL2_le_setsum [OF zero_le_dist])
+    also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV"
+      by (rule setsum_strict_mono, simp_all add: M `M \<le> m` `M \<le> n`)
+    also have "\<dots> = r"
+      by simp
+    finally have "dist (X m) (X n) < r" .
+  }
+  hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r"
+    by simp
+  then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" ..
+qed
+
 subsection {* Norms *}
 
 instantiation "^" :: (real_normed_vector, finite) real_normed_vector
@@ -558,6 +677,17 @@
 
 end
 
+lemma norm_nth_le: "norm (x $ i) \<le> norm x"
+unfolding vector_norm_def
+by (rule member_le_setL2) simp_all
+
+interpretation Cart_nth: bounded_linear "\<lambda>x. x $ i"
+apply default
+apply (rule vector_add_component)
+apply (rule vector_scaleR_component)
+apply (rule_tac x="1" in exI, simp add: norm_nth_le)
+done
+
 subsection {* Inner products *}
 
 instantiation "^" :: (real_inner, finite) real_inner