new lemmas
authorhuffman
Tue Jun 02 10:32:19 2009 -0700 (2009-06-02)
changeset 313893affcbc60c6d
parent 31388 e0c05b595d1f
child 31390 1d0478b16613
new lemmas
src/HOL/Library/Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon Jun 01 16:59:56 2009 -0700
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 10:32:19 2009 -0700
     1.3 @@ -522,6 +522,125 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma dist_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
     1.8 +unfolding dist_vector_def
     1.9 +by (rule member_le_setL2) simp_all
    1.10 +
    1.11 +lemma tendsto_Cart_nth:
    1.12 +  fixes X :: "'a \<Rightarrow> 'b::metric_space ^ 'n::finite"
    1.13 +  assumes "tendsto (\<lambda>n. X n) a net"
    1.14 +  shows "tendsto (\<lambda>n. X n $ i) (a $ i) net"
    1.15 +proof (rule tendstoI)
    1.16 +  fix e :: real assume "0 < e"
    1.17 +  with assms have "eventually (\<lambda>n. dist (X n) a < e) net"
    1.18 +    by (rule tendstoD)
    1.19 +  thus "eventually (\<lambda>n. dist (X n $ i) (a $ i) < e) net"
    1.20 +  proof (rule eventually_elim1)
    1.21 +    fix n :: 'a
    1.22 +    have "dist (X n $ i) (a $ i) \<le> dist (X n) a"
    1.23 +      by (rule dist_nth_le)
    1.24 +    also assume "dist (X n) a < e"
    1.25 +    finally show "dist (X n $ i) (a $ i) < e" .
    1.26 +  qed
    1.27 +qed
    1.28 +
    1.29 +lemma LIMSEQ_Cart_nth:
    1.30 +  "(X ----> a) \<Longrightarrow> (\<lambda>n. X n $ i) ----> a $ i"
    1.31 +unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth)
    1.32 +
    1.33 +lemma LIM_Cart_nth:
    1.34 +  "(f -- x --> y) \<Longrightarrow> (\<lambda>x. f x $ i) -- x --> y $ i"
    1.35 +unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth)
    1.36 +
    1.37 +lemma Cauchy_Cart_nth:
    1.38 +  fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n::finite"
    1.39 +  assumes "Cauchy (\<lambda>n. X n)"
    1.40 +  shows "Cauchy (\<lambda>n. X n $ i)"
    1.41 +proof (rule metric_CauchyI)
    1.42 +  fix e :: real assume "0 < e"
    1.43 +  obtain M where "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
    1.44 +    using metric_CauchyD [OF `Cauchy X` `0 < e`] by fast
    1.45 +  moreover
    1.46 +  {
    1.47 +    fix m n
    1.48 +    assume "M \<le> m" "M \<le> n"
    1.49 +    have "dist (X m $ i) (X n $ i) \<le> dist (X m) (X n)"
    1.50 +      by (rule dist_nth_le)
    1.51 +    also assume "dist (X m) (X n) < e"
    1.52 +    finally have "dist (X m $ i) (X n $ i) < e" .
    1.53 +  }
    1.54 +  ultimately
    1.55 +  have "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < e" by fast
    1.56 +  thus "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < e" ..
    1.57 +qed
    1.58 +
    1.59 +lemma LIMSEQ_vector:
    1.60 +  fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n::finite"
    1.61 +  assumes X: "\<And>i. (\<lambda>n. X n $ i) ----> (a $ i)"
    1.62 +  shows "X ----> a"
    1.63 +proof (rule metric_LIMSEQ_I)
    1.64 +  fix r :: real assume "0 < r"
    1.65 +  then have "0 < r / of_nat CARD('n)" (is "0 < ?s")
    1.66 +    by (simp add: divide_pos_pos)
    1.67 +  def N \<equiv> "\<lambda>i. LEAST N. \<forall>n\<ge>N. dist (X n $ i) (a $ i) < ?s"
    1.68 +  def M \<equiv> "Max (range N)"
    1.69 +  have "\<And>i. \<exists>N. \<forall>n\<ge>N. dist (X n $ i) (a $ i) < ?s"
    1.70 +    using X `0 < ?s` by (rule metric_LIMSEQ_D)
    1.71 +  hence "\<And>i. \<forall>n\<ge>N i. dist (X n $ i) (a $ i) < ?s"
    1.72 +    unfolding N_def by (rule LeastI_ex)
    1.73 +  hence M: "\<And>i. \<forall>n\<ge>M. dist (X n $ i) (a $ i) < ?s"
    1.74 +    unfolding M_def by simp
    1.75 +  {
    1.76 +    fix n :: nat assume "M \<le> n"
    1.77 +    have "dist (X n) a = setL2 (\<lambda>i. dist (X n $ i) (a $ i)) UNIV"
    1.78 +      unfolding dist_vector_def ..
    1.79 +    also have "\<dots> \<le> setsum (\<lambda>i. dist (X n $ i) (a $ i)) UNIV"
    1.80 +      by (rule setL2_le_setsum [OF zero_le_dist])
    1.81 +    also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV"
    1.82 +      by (rule setsum_strict_mono, simp_all add: M `M \<le> n`)
    1.83 +    also have "\<dots> = r"
    1.84 +      by simp
    1.85 +    finally have "dist (X n) a < r" .
    1.86 +  }
    1.87 +  hence "\<forall>n\<ge>M. dist (X n) a < r"
    1.88 +    by simp
    1.89 +  then show "\<exists>M. \<forall>n\<ge>M. dist (X n) a < r" ..
    1.90 +qed
    1.91 +
    1.92 +lemma Cauchy_vector:
    1.93 +  fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n::finite"
    1.94 +  assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)"
    1.95 +  shows "Cauchy (\<lambda>n. X n)"
    1.96 +proof (rule metric_CauchyI)
    1.97 +  fix r :: real assume "0 < r"
    1.98 +  then have "0 < r / of_nat CARD('n)" (is "0 < ?s")
    1.99 +    by (simp add: divide_pos_pos)
   1.100 +  def N \<equiv> "\<lambda>i. LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"
   1.101 +  def M \<equiv> "Max (range N)"
   1.102 +  have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"
   1.103 +    using X `0 < ?s` by (rule metric_CauchyD)
   1.104 +  hence "\<And>i. \<forall>m\<ge>N i. \<forall>n\<ge>N i. dist (X m $ i) (X n $ i) < ?s"
   1.105 +    unfolding N_def by (rule LeastI_ex)
   1.106 +  hence M: "\<And>i. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < ?s"
   1.107 +    unfolding M_def by simp
   1.108 +  {
   1.109 +    fix m n :: nat
   1.110 +    assume "M \<le> m" "M \<le> n"
   1.111 +    have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
   1.112 +      unfolding dist_vector_def ..
   1.113 +    also have "\<dots> \<le> setsum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
   1.114 +      by (rule setL2_le_setsum [OF zero_le_dist])
   1.115 +    also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV"
   1.116 +      by (rule setsum_strict_mono, simp_all add: M `M \<le> m` `M \<le> n`)
   1.117 +    also have "\<dots> = r"
   1.118 +      by simp
   1.119 +    finally have "dist (X m) (X n) < r" .
   1.120 +  }
   1.121 +  hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r"
   1.122 +    by simp
   1.123 +  then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" ..
   1.124 +qed
   1.125 +
   1.126  subsection {* Norms *}
   1.127  
   1.128  instantiation "^" :: (real_normed_vector, finite) real_normed_vector
   1.129 @@ -558,6 +677,17 @@
   1.130  
   1.131  end
   1.132  
   1.133 +lemma norm_nth_le: "norm (x $ i) \<le> norm x"
   1.134 +unfolding vector_norm_def
   1.135 +by (rule member_le_setL2) simp_all
   1.136 +
   1.137 +interpretation Cart_nth: bounded_linear "\<lambda>x. x $ i"
   1.138 +apply default
   1.139 +apply (rule vector_add_component)
   1.140 +apply (rule vector_scaleR_component)
   1.141 +apply (rule_tac x="1" in exI, simp add: norm_nth_le)
   1.142 +done
   1.143 +
   1.144  subsection {* Inner products *}
   1.145  
   1.146  instantiation "^" :: (real_inner, finite) real_inner