new setL2 lemmas; instance ^ :: (topological_space, finite) topological_space
authorhuffman
Sun Jun 07 19:38:32 2009 -0700 (2009-06-07)
changeset 31493d92cfed6c6b2
parent 31492 5400beeddb55
child 31494 1ba61c7b129f
new setL2 lemmas; instance ^ :: (topological_space, finite) topological_space
src/HOL/Library/Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sun Jun 07 17:59:54 2009 -0700
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Sun Jun 07 19:38:32 2009 -0700
     1.3 @@ -331,6 +331,63 @@
     1.4  lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
     1.5    by (simp add: Cart_eq)
     1.6  
     1.7 +subsection {* Topological space *}
     1.8 +
     1.9 +instantiation "^" :: (topological_space, finite) topological_space
    1.10 +begin
    1.11 +
    1.12 +definition open_vector_def:
    1.13 +  "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
    1.14 +    (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
    1.15 +      (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"
    1.16 +
    1.17 +instance proof
    1.18 +  show "open (UNIV :: ('a ^ 'b) set)"
    1.19 +    unfolding open_vector_def by auto
    1.20 +next
    1.21 +  fix S T :: "('a ^ 'b) set"
    1.22 +  assume "open S" "open T" thus "open (S \<inter> T)"
    1.23 +    unfolding open_vector_def
    1.24 +    apply clarify
    1.25 +    apply (drule (1) bspec)+
    1.26 +    apply (clarify, rename_tac Sa Ta)
    1.27 +    apply (rule_tac x="\<lambda>i. Sa i \<inter> Ta i" in exI)
    1.28 +    apply (simp add: open_Int)
    1.29 +    done
    1.30 +next
    1.31 +  fix K :: "('a ^ 'b) set set"
    1.32 +  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
    1.33 +    unfolding open_vector_def
    1.34 +    apply clarify
    1.35 +    apply (drule (1) bspec)
    1.36 +    apply (drule (1) bspec)
    1.37 +    apply clarify
    1.38 +    apply (rule_tac x=A in exI)
    1.39 +    apply fast
    1.40 +    done
    1.41 +qed
    1.42 +
    1.43 +end
    1.44 +
    1.45 +lemma tendsto_Cart_nth:
    1.46 +  fixes f :: "'a \<Rightarrow> 'b::topological_space ^ 'n::finite"
    1.47 +  assumes "((\<lambda>x. f x) ---> a) net"
    1.48 +  shows "((\<lambda>x. f x $ i) ---> a $ i) net"
    1.49 +proof (rule topological_tendstoI)
    1.50 +  fix S :: "'b set" assume "open S" "a $ i \<in> S"
    1.51 +  then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"
    1.52 +    unfolding open_vector_def
    1.53 +    apply simp_all
    1.54 +    apply clarify
    1.55 +    apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI)
    1.56 +    apply simp
    1.57 +    done
    1.58 +  with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net"
    1.59 +    by (rule topological_tendstoD)
    1.60 +  then show "eventually (\<lambda>x. f x $ i \<in> S) net"
    1.61 +    by simp
    1.62 +qed
    1.63 +
    1.64  subsection {* Square root of sum of squares *}
    1.65  
    1.66  definition
    1.67 @@ -361,6 +418,9 @@
    1.68  lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
    1.69    unfolding setL2_def by simp
    1.70  
    1.71 +lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
    1.72 +  unfolding setL2_def by (simp add: real_sqrt_mult)
    1.73 +
    1.74  lemma setL2_mono:
    1.75    assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
    1.76    assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
    1.77 @@ -368,6 +428,14 @@
    1.78    unfolding setL2_def
    1.79    by (simp add: setsum_nonneg setsum_mono power_mono prems)
    1.80  
    1.81 +lemma setL2_strict_mono:
    1.82 +  assumes "finite K" and "K \<noteq> {}"
    1.83 +  assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
    1.84 +  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
    1.85 +  shows "setL2 f K < setL2 g K"
    1.86 +  unfolding setL2_def
    1.87 +  by (simp add: setsum_strict_mono power_strict_mono assms)
    1.88 +
    1.89  lemma setL2_right_distrib:
    1.90    "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
    1.91    unfolding setL2_def
    1.92 @@ -500,15 +568,22 @@
    1.93  
    1.94  subsection {* Metric *}
    1.95  
    1.96 +(* TODO: move somewhere else *)
    1.97 +lemma finite_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
    1.98 +apply (induct set: finite, simp_all)
    1.99 +apply (clarify, rename_tac y)
   1.100 +apply (rule_tac x="f(x:=y)" in exI, simp)
   1.101 +done
   1.102 +
   1.103  instantiation "^" :: (metric_space, finite) metric_space
   1.104  begin
   1.105  
   1.106  definition dist_vector_def:
   1.107    "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
   1.108  
   1.109 -definition open_vector_def:
   1.110 -  "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
   1.111 -    (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   1.112 +lemma dist_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
   1.113 +unfolding dist_vector_def
   1.114 +by (rule member_le_setL2) simp_all
   1.115  
   1.116  instance proof
   1.117    fix x y :: "'a ^ 'b"
   1.118 @@ -523,35 +598,48 @@
   1.119      apply (simp add: setL2_mono dist_triangle2)
   1.120      done
   1.121  next
   1.122 +  (* FIXME: long proof! *)
   1.123    fix S :: "('a ^ 'b) set"
   1.124    show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   1.125 -    by (rule open_vector_def)
   1.126 +    unfolding open_vector_def open_dist
   1.127 +    apply safe
   1.128 +     apply (drule (1) bspec)
   1.129 +     apply clarify
   1.130 +     apply (subgoal_tac "\<exists>e>0. \<forall>i y. dist y (x$i) < e \<longrightarrow> y \<in> A i")
   1.131 +      apply clarify
   1.132 +      apply (rule_tac x=e in exI, clarify)
   1.133 +      apply (drule spec, erule mp, clarify)
   1.134 +      apply (drule spec, drule spec, erule mp)
   1.135 +      apply (erule le_less_trans [OF dist_nth_le])
   1.136 +     apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>e>0. \<forall>y. dist y (x$i) < e \<longrightarrow> y \<in> A i")
   1.137 +      apply (drule finite_choice [OF finite], clarify)
   1.138 +      apply (rule_tac x="Min (range f)" in exI, simp)
   1.139 +     apply clarify
   1.140 +     apply (drule_tac x=i in spec, clarify)
   1.141 +     apply (erule (1) bspec)
   1.142 +    apply (drule (1) bspec, clarify)
   1.143 +    apply (subgoal_tac "\<exists>r. (\<forall>i::'b. 0 < r i) \<and> e = setL2 r UNIV")
   1.144 +     apply clarify
   1.145 +     apply (rule_tac x="\<lambda>i. {y. dist y (x$i) < r i}" in exI)
   1.146 +     apply (rule conjI)
   1.147 +      apply clarify
   1.148 +      apply (rule conjI)
   1.149 +       apply (clarify, rename_tac y)
   1.150 +       apply (rule_tac x="r i - dist y (x$i)" in exI, rule conjI, simp)
   1.151 +       apply clarify
   1.152 +       apply (simp only: less_diff_eq)
   1.153 +       apply (erule le_less_trans [OF dist_triangle])
   1.154 +      apply simp
   1.155 +     apply clarify
   1.156 +     apply (drule spec, erule mp)
   1.157 +     apply (simp add: dist_vector_def setL2_strict_mono)
   1.158 +    apply (rule_tac x="\<lambda>i. e / sqrt (of_nat CARD('b))" in exI)
   1.159 +    apply (simp add: divide_pos_pos setL2_constant)
   1.160 +    done
   1.161  qed
   1.162  
   1.163  end
   1.164  
   1.165 -lemma dist_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
   1.166 -unfolding dist_vector_def
   1.167 -by (rule member_le_setL2) simp_all
   1.168 -
   1.169 -lemma tendsto_Cart_nth:
   1.170 -  fixes X :: "'a \<Rightarrow> 'b::metric_space ^ 'n::finite"
   1.171 -  assumes "tendsto (\<lambda>n. X n) a net"
   1.172 -  shows "tendsto (\<lambda>n. X n $ i) (a $ i) net"
   1.173 -proof (rule tendstoI)
   1.174 -  fix e :: real assume "0 < e"
   1.175 -  with assms have "eventually (\<lambda>n. dist (X n) a < e) net"
   1.176 -    by (rule tendstoD)
   1.177 -  thus "eventually (\<lambda>n. dist (X n $ i) (a $ i) < e) net"
   1.178 -  proof (rule eventually_elim1)
   1.179 -    fix n :: 'a
   1.180 -    have "dist (X n $ i) (a $ i) \<le> dist (X n) a"
   1.181 -      by (rule dist_nth_le)
   1.182 -    also assume "dist (X n) a < e"
   1.183 -    finally show "dist (X n $ i) (a $ i) < e" .
   1.184 -  qed
   1.185 -qed
   1.186 -
   1.187  lemma LIMSEQ_Cart_nth:
   1.188    "(X ----> a) \<Longrightarrow> (\<lambda>n. X n $ i) ----> a $ i"
   1.189  unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth)