Convex hulls: theorems about interior, etc. And a few simple lemmas.
authorpaulson <lp15@cam.ac.uk>
Thu May 28 14:33:35 2015 +0100 (2015-05-28)
changeset 6030775e1aa7a450e
parent 60306 6b7c64ab8bd2
child 60308 f7e406aba90d
Convex hulls: theorems about interior, etc. And a few simple lemmas.
src/HOL/Complete_Lattices.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Thu May 28 10:18:46 2015 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Thu May 28 14:33:35 2015 +0100
     1.3 @@ -1204,6 +1204,9 @@
     1.4    "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
     1.5    by (fact Sup_image_eq)
     1.6  
     1.7 +lemma Union_SetCompr_eq: "\<Union> {f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
     1.8 +  by blast
     1.9 +
    1.10  lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
    1.11    using Union_iff [of _ "B ` A"] by simp
    1.12  
     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu May 28 10:18:46 2015 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu May 28 14:33:35 2015 +0100
     2.3 @@ -754,6 +754,10 @@
     2.4    using mem_affine_3[of S x y z 1 v "-v"] assms
     2.5    by (simp add: algebra_simps)
     2.6  
     2.7 +corollary mem_affine_3_minus2:
     2.8 +    "\<lbrakk>affine S; x \<in> S; y \<in> S; z \<in> S\<rbrakk> \<Longrightarrow> x - v *\<^sub>R (y-z) \<in> S"
     2.9 +  by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left)
    2.10 +
    2.11  
    2.12  subsubsection {* Some relations between affine hull and subspaces *}
    2.13  
    2.14 @@ -3129,6 +3133,11 @@
    2.15      using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto
    2.16  qed
    2.17  
    2.18 +corollary empty_interior_lowdim:
    2.19 +  fixes S :: "'n::euclidean_space set"
    2.20 +  shows "dim S < DIM ('n) \<Longrightarrow> interior S = {}"
    2.21 +by (metis low_dim_interior affine_hull_univ dim_affine_hull less_not_refl dim_UNIV)
    2.22 +
    2.23  subsection {* Relative interior of a set *}
    2.24  
    2.25  definition "rel_interior S =
    2.26 @@ -3336,7 +3345,7 @@
    2.27        using mem_interior_cball[of y "{a..}"] by auto
    2.28      moreover from e have "y - e \<in> cball y e"
    2.29        by (auto simp add: cball_def dist_norm)
    2.30 -    ultimately have "a \<le> y - e" by auto
    2.31 +    ultimately have "a \<le> y - e" by blast
    2.32      then have "a < y" using e by auto
    2.33    }
    2.34    ultimately show ?thesis by auto
    2.35 @@ -8897,5 +8906,392 @@
    2.36    then show ?thesis
    2.37      using `y < x` by (simp add: field_simps)
    2.38  qed simp
    2.39 +subsection{* Explicit formulas for interior and relative interior of convex hull*}
    2.40 + 
    2.41 +lemma affine_independent_convex_affine_hull:
    2.42 +  fixes s :: "'a::euclidean_space set"
    2.43 +  assumes "~affine_dependent s" "t \<subseteq> s"
    2.44 +    shows "convex hull t = affine hull t \<inter> convex hull s"
    2.45 +proof -
    2.46 +  have fin: "finite s" "finite t" using assms aff_independent_finite finite_subset by auto
    2.47 +    { fix u v x
    2.48 +      assume uv: "setsum u t = 1" "\<forall>x\<in>s. 0 \<le> v x" "setsum v s = 1" 
    2.49 +                 "(\<Sum>x\<in>s. v x *\<^sub>R x) = (\<Sum>v\<in>t. u v *\<^sub>R v)" "x \<in> t"
    2.50 +      then have s: "s = (s - t) \<union> t" --{*split into separate cases*}
    2.51 +        using assms by auto
    2.52 +      have [simp]: "(\<Sum>x\<in>t. v x *\<^sub>R x) + (\<Sum>x\<in>s - t. v x *\<^sub>R x) = (\<Sum>x\<in>t. u x *\<^sub>R x)"
    2.53 +                   "setsum v t + setsum v (s - t) = 1"
    2.54 +        using uv fin s
    2.55 +        by (auto simp: setsum.union_disjoint [symmetric] Un_commute)        
    2.56 +      have "(\<Sum>x\<in>s. if x \<in> t then v x - u x else v x) = 0" 
    2.57 +           "(\<Sum>x\<in>s. (if x \<in> t then v x - u x else v x) *\<^sub>R x) = 0"
    2.58 +        using uv fin
    2.59 +        by (subst s, subst setsum.union_disjoint, auto simp: algebra_simps setsum_subtractf)+
    2.60 +    } note [simp] = this
    2.61 +  have "convex hull t \<subseteq> affine hull t" 
    2.62 +    using convex_hull_subset_affine_hull by blast
    2.63 +  moreover have "convex hull t \<subseteq> convex hull s"
    2.64 +    using assms hull_mono by blast
    2.65 +  moreover have "affine hull t \<inter> convex hull s \<subseteq> convex hull t"
    2.66 +    using assms 
    2.67 +    apply (simp add: convex_hull_finite affine_hull_finite fin affine_dependent_explicit)
    2.68 +    apply (drule_tac x=s in spec)
    2.69 +    apply (auto simp: fin)
    2.70 +    apply (rule_tac x=u in exI)
    2.71 +    apply (rename_tac v)
    2.72 +    apply (drule_tac x="\<lambda>x. if x \<in> t then v x - u x else v x" in spec)
    2.73 +    apply (force)+
    2.74 +    done
    2.75 +  ultimately show ?thesis
    2.76 +    by blast
    2.77 +qed
    2.78 +
    2.79 +lemma affine_independent_span_eq: 
    2.80 +  fixes s :: "'a::euclidean_space set"
    2.81 +  assumes "~affine_dependent s" "card s = Suc (DIM ('a))"
    2.82 +    shows "affine hull s = UNIV"
    2.83 +proof (cases "s = {}")
    2.84 +  case True then show ?thesis
    2.85 +    using assms by simp
    2.86 +next
    2.87 +  case False
    2.88 +    then obtain a t where t: "a \<notin> t" "s = insert a t"
    2.89 +      by blast
    2.90 +    then have fin: "finite t" using assms 
    2.91 +      by (metis finite_insert aff_independent_finite)
    2.92 +    show ?thesis
    2.93 +    using assms t fin
    2.94 +      apply (simp add: affine_dependent_iff_dependent affine_hull_insert_span_gen)
    2.95 +      apply (rule subset_antisym)
    2.96 +      apply force
    2.97 +      apply (rule Fun.vimage_subsetD)
    2.98 +      apply (metis add.commute diff_add_cancel surj_def)
    2.99 +      apply (rule card_ge_dim_independent)
   2.100 +      apply (auto simp: card_image inj_on_def dim_subset_UNIV)
   2.101 +      done
   2.102 +qed
   2.103 +
   2.104 +lemma affine_independent_span_gt: 
   2.105 +  fixes s :: "'a::euclidean_space set"
   2.106 +  assumes ind: "~ affine_dependent s" and dim: "DIM ('a) < card s"
   2.107 +    shows "affine hull s = UNIV"
   2.108 +  apply (rule affine_independent_span_eq [OF ind])
   2.109 +  apply (rule antisym)
   2.110 +  using assms
   2.111 +  apply auto
   2.112 +  apply (metis add_2_eq_Suc' not_less_eq_eq affine_dependent_biggerset aff_independent_finite)
   2.113 +  done
   2.114 +
   2.115 +lemma empty_interior_affine_hull: 
   2.116 +  fixes s :: "'a::euclidean_space set"
   2.117 +  assumes "finite s" and dim: "card s \<le> DIM ('a)"
   2.118 +    shows "interior(affine hull s) = {}"
   2.119 +  using assms
   2.120 +  apply (induct s rule: finite_induct)
   2.121 +  apply (simp_all add:  affine_dependent_iff_dependent affine_hull_insert_span_gen interior_translation)
   2.122 +  apply (rule empty_interior_lowdim)
   2.123 +  apply (simp add: affine_dependent_iff_dependent affine_hull_insert_span_gen)
   2.124 +  apply (metis Suc_le_lessD not_less order_trans card_image_le finite_imageI dim_le_card)
   2.125 +  done
   2.126 +
   2.127 +lemma empty_interior_convex_hull: 
   2.128 +  fixes s :: "'a::euclidean_space set"
   2.129 +  assumes "finite s" and dim: "card s \<le> DIM ('a)"
   2.130 +    shows "interior(convex hull s) = {}"
   2.131 +  by (metis Diff_empty Diff_eq_empty_iff convex_hull_subset_affine_hull 
   2.132 +            interior_mono empty_interior_affine_hull [OF assms])
   2.133 +
   2.134 +lemma explicit_subset_rel_interior_convex_hull:
   2.135 +  fixes s :: "'a::euclidean_space set"
   2.136 +  shows "finite s 
   2.137 +         \<Longrightarrow> {y. \<exists>u. (\<forall>x \<in> s. 0 < u x \<and> u x < 1) \<and> setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}
   2.138 +             \<subseteq> rel_interior (convex hull s)"
   2.139 +  by (force simp add:  rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=s, simplified])
   2.140 +
   2.141 +lemma explicit_subset_rel_interior_convex_hull_minimal: 
   2.142 +  fixes s :: "'a::euclidean_space set"
   2.143 +  shows "finite s 
   2.144 +         \<Longrightarrow> {y. \<exists>u. (\<forall>x \<in> s. 0 < u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}
   2.145 +             \<subseteq> rel_interior (convex hull s)"
   2.146 +  by (force simp add:  rel_interior_convex_hull_union [where S="\<lambda>x. {x}" and I=s, simplified])
   2.147 +
   2.148 +lemma rel_interior_convex_hull_explicit: 
   2.149 +  fixes s :: "'a::euclidean_space set"
   2.150 +  assumes "~ affine_dependent s"
   2.151 +  shows "rel_interior(convex hull s) =
   2.152 +         {y. \<exists>u. (\<forall>x \<in> s. 0 < u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}"
   2.153 +         (is "?lhs = ?rhs")  
   2.154 +proof
   2.155 +  show "?rhs \<le> ?lhs"
   2.156 +    by (simp add: aff_independent_finite explicit_subset_rel_interior_convex_hull_minimal assms)
   2.157 +next
   2.158 +  show "?lhs \<le> ?rhs"
   2.159 +  proof (cases "\<exists>a. s = {a}")
   2.160 +    case True then show "?lhs \<le> ?rhs"
   2.161 +      by force
   2.162 +  next
   2.163 +    case False
   2.164 +    have fs: "finite s"
   2.165 +      using assms by (simp add: aff_independent_finite)
   2.166 +    { fix a b and d::real
   2.167 +      assume ab: "a \<in> s" "b \<in> s" "a \<noteq> b"
   2.168 +      then have s: "s = (s - {a,b}) \<union> {a,b}" --{*split into separate cases*}
   2.169 +        by auto
   2.170 +      have "(\<Sum>x\<in>s. if x = a then - d else if x = b then d else 0) = 0" 
   2.171 +           "(\<Sum>x\<in>s. (if x = a then - d else if x = b then d else 0) *\<^sub>R x) = d *\<^sub>R b - d *\<^sub>R a"
   2.172 +        using ab fs
   2.173 +        by (subst s, subst setsum.union_disjoint, auto)+
   2.174 +    } note [simp] = this
   2.175 +    { fix y
   2.176 +      assume y: "y \<in> convex hull s" "y \<notin> ?rhs"
   2.177 +      { fix u T a
   2.178 +        assume ua: "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "\<not> 0 < u a" "a \<in> s"
   2.179 +           and yT: "y = (\<Sum>x\<in>s. u x *\<^sub>R x)" "y \<in> T" "open T"
   2.180 +           and sb: "T \<inter> affine hull s \<subseteq> {w. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = w}" 
   2.181 +        have ua0: "u a = 0"
   2.182 +          using ua by auto
   2.183 +        obtain b where b: "b\<in>s" "a \<noteq> b"
   2.184 +          using ua False by auto
   2.185 +        obtain e where e: "0 < e" "ball (\<Sum>x\<in>s. u x *\<^sub>R x) e \<subseteq> T"
   2.186 +          using yT by (auto elim: openE)
   2.187 +        with b obtain d where d: "0 < d" "norm(d *\<^sub>R (a-b)) < e"
   2.188 +          by (auto intro: that [of "e / 2 / norm(a-b)"])
   2.189 +        have "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> affine hull s"
   2.190 +          using yT y by (metis affine_hull_convex_hull hull_redundant_eq)
   2.191 +        then have "(\<Sum>x\<in>s. u x *\<^sub>R x) - d *\<^sub>R (a - b) \<in> affine hull s"
   2.192 +          using ua b by (auto simp: hull_inc intro: mem_affine_3_minus2)
   2.193 +        then have "y - d *\<^sub>R (a - b) \<in> T \<inter> affine hull s"
   2.194 +          using d e yT by auto
   2.195 +        then obtain v where "\<forall>x\<in>s. 0 \<le> v x" 
   2.196 +                            "setsum v s = 1" 
   2.197 +                            "(\<Sum>x\<in>s. v x *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x) - d *\<^sub>R (a - b)"
   2.198 +          using subsetD [OF sb] yT
   2.199 +          by auto
   2.200 +        then have False
   2.201 +          using assms 
   2.202 +          apply (simp add: affine_dependent_explicit_finite fs)
   2.203 +          apply (drule_tac x="\<lambda>x. (v x - u x) - (if x = a then -d else if x = b then d else 0)" in spec)
   2.204 +          using ua b d
   2.205 +          apply (auto simp: algebra_simps setsum_subtractf setsum.distrib)
   2.206 +          done
   2.207 +      } note * = this
   2.208 +      have "y \<notin> rel_interior (convex hull s)"
   2.209 +        using y
   2.210 +        apply (simp add: mem_rel_interior affine_hull_convex_hull)
   2.211 +        apply (auto simp: convex_hull_finite [OF fs])
   2.212 +        apply (drule_tac x=u in spec)
   2.213 +        apply (auto intro: *)
   2.214 +        done
   2.215 +    } with rel_interior_subset show "?lhs \<le> ?rhs"
   2.216 +      by blast
   2.217 +  qed
   2.218 +qed
   2.219 +
   2.220 +lemma interior_convex_hull_explicit_minimal:
   2.221 +  fixes s :: "'a::euclidean_space set"
   2.222 +  shows
   2.223 +   "~ affine_dependent s
   2.224 +        ==> interior(convex hull s) =
   2.225 +             (if card(s) \<le> DIM('a) then {}
   2.226 +              else {y. \<exists>u. (\<forall>x \<in> s. 0 < u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = y})"
   2.227 +  apply (simp add: aff_independent_finite empty_interior_convex_hull, clarify)
   2.228 +  apply (rule trans [of _ "rel_interior(convex hull s)"])
   2.229 +  apply (simp add: affine_hull_convex_hull affine_independent_span_gt rel_interior_interior)
   2.230 +  by (simp add: rel_interior_convex_hull_explicit)
   2.231 +
   2.232 +lemma interior_convex_hull_explicit:
   2.233 +  fixes s :: "'a::euclidean_space set"
   2.234 +  assumes "~ affine_dependent s"
   2.235 +  shows
   2.236 +   "interior(convex hull s) =
   2.237 +             (if card(s) \<le> DIM('a) then {}
   2.238 +              else {y. \<exists>u. (\<forall>x \<in> s. 0 < u x \<and> u x < 1) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = y})"
   2.239 +proof -
   2.240 +  { fix u :: "'a \<Rightarrow> real" and a
   2.241 +    assume "card Basis < card s" and u: "\<And>x. x\<in>s \<Longrightarrow> 0 < u x" "setsum u s = 1" and a: "a \<in> s"
   2.242 +    then have cs: "Suc 0 < card s"
   2.243 +      by (metis DIM_positive less_trans_Suc)
   2.244 +    obtain b where b: "b \<in> s" "a \<noteq> b"
   2.245 +    proof (cases "s \<le> {a}")
   2.246 +      case True
   2.247 +      then show thesis
   2.248 +        using cs subset_singletonD by fastforce
   2.249 +    next
   2.250 +      case False
   2.251 +      then show thesis
   2.252 +      by (blast intro: that)
   2.253 +    qed        
   2.254 +    have "u a + u b \<le> setsum u {a,b}"
   2.255 +      using a b by simp
   2.256 +    also have "... \<le> setsum u s"
   2.257 +      apply (rule Groups_Big.setsum_mono2)
   2.258 +      using a b u
   2.259 +      apply (auto simp: less_imp_le aff_independent_finite assms)
   2.260 +      done      
   2.261 +    finally have "u a < 1"
   2.262 +      using `b \<in> s` u by fastforce
   2.263 +  } note [simp] = this
   2.264 +  show ?thesis
   2.265 +    using assms
   2.266 +    apply (auto simp: interior_convex_hull_explicit_minimal)
   2.267 +    apply (rule_tac x=u in exI)
   2.268 +    apply (auto simp: not_le)
   2.269 +    done
   2.270 +qed
   2.271 +
   2.272 +subsection{* Similar results for closure and (relative or absolute) frontier.*}
   2.273 +
   2.274 +lemma closure_convex_hull [simp]:
   2.275 +  fixes s :: "'a::euclidean_space set"
   2.276 +  shows "compact s ==> closure(convex hull s) = convex hull s"
   2.277 +  by (simp add: compact_imp_closed compact_convex_hull)
   2.278 +
   2.279 +lemma rel_frontier_convex_hull_explicit:
   2.280 +  fixes s :: "'a::euclidean_space set"
   2.281 +  assumes "~ affine_dependent s"
   2.282 +  shows "rel_frontier(convex hull s) =
   2.283 +         {y. \<exists>u. (\<forall>x \<in> s. 0 \<le> u x) \<and> (\<exists>x \<in> s. u x = 0) \<and> setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}"
   2.284 +proof -
   2.285 +  have fs: "finite s"
   2.286 +    using assms by (simp add: aff_independent_finite)
   2.287 +  show ?thesis
   2.288 +    apply (simp add: rel_frontier_def finite_imp_compact rel_interior_convex_hull_explicit assms fs)
   2.289 +    apply (auto simp: convex_hull_finite fs)
   2.290 +    apply (drule_tac x=u in spec)
   2.291 +    apply (rule_tac x=u in exI)
   2.292 +    apply force
   2.293 +    apply (rename_tac v)
   2.294 +    apply (rule notE [OF assms])
   2.295 +    apply (simp add: affine_dependent_explicit)
   2.296 +    apply (rule_tac x=s in exI)
   2.297 +    apply (auto simp: fs)
   2.298 +    apply (rule_tac x = "\<lambda>x. u x - v x" in exI)
   2.299 +    apply (force simp: setsum_subtractf scaleR_diff_left)
   2.300 +    done
   2.301 +qed
   2.302 +
   2.303 +lemma frontier_convex_hull_explicit:
   2.304 +  fixes s :: "'a::euclidean_space set"
   2.305 +  assumes "~ affine_dependent s"
   2.306 +  shows "frontier(convex hull s) =
   2.307 +         {y. \<exists>u. (\<forall>x \<in> s. 0 \<le> u x) \<and> (DIM ('a) < card s \<longrightarrow> (\<exists>x \<in> s. u x = 0)) \<and> 
   2.308 +             setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}"
   2.309 +proof -
   2.310 +  have fs: "finite s"
   2.311 +    using assms by (simp add: aff_independent_finite)
   2.312 +  show ?thesis
   2.313 +  proof (cases "DIM ('a) < card s")
   2.314 +    case True
   2.315 +    with assms fs show ?thesis
   2.316 +      by (simp add: rel_frontier_def frontier_def rel_frontier_convex_hull_explicit [symmetric] 
   2.317 +                    interior_convex_hull_explicit_minimal rel_interior_convex_hull_explicit)
   2.318 +  next
   2.319 +    case False
   2.320 +    then have "card s \<le> DIM ('a)"
   2.321 +      by linarith
   2.322 +    then show ?thesis
   2.323 +      using assms fs
   2.324 +      apply (simp add: frontier_def interior_convex_hull_explicit finite_imp_compact)
   2.325 +      apply (simp add: convex_hull_finite)
   2.326 +      done
   2.327 +  qed
   2.328 +qed
   2.329 +
   2.330 +lemma rel_frontier_convex_hull_cases:
   2.331 +  fixes s :: "'a::euclidean_space set"
   2.332 +  assumes "~ affine_dependent s"
   2.333 +  shows "rel_frontier(convex hull s) = \<Union>{convex hull (s - {x}) |x. x \<in> s}"
   2.334 +proof -
   2.335 +  have fs: "finite s"
   2.336 +    using assms by (simp add: aff_independent_finite)
   2.337 +  { fix u a
   2.338 +  have "\<forall>x\<in>s. 0 \<le> u x \<Longrightarrow> a \<in> s \<Longrightarrow> u a = 0 \<Longrightarrow> setsum u s = 1 \<Longrightarrow>
   2.339 +            \<exists>x v. x \<in> s \<and>
   2.340 +                  (\<forall>x\<in>s - {x}. 0 \<le> v x) \<and>
   2.341 +                      setsum v (s - {x}) = 1 \<and> (\<Sum>x\<in>s - {x}. v x *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)"
   2.342 +    apply (rule_tac x=a in exI)
   2.343 +    apply (rule_tac x=u in exI)
   2.344 +    apply (simp add: Groups_Big.setsum_diff1 fs)
   2.345 +    done }
   2.346 +  moreover 
   2.347 +  { fix a u
   2.348 +    have "a \<in> s \<Longrightarrow> \<forall>x\<in>s - {a}. 0 \<le> u x \<Longrightarrow> setsum u (s - {a}) = 1 \<Longrightarrow>
   2.349 +            \<exists>v. (\<forall>x\<in>s. 0 \<le> v x) \<and>
   2.350 +                 (\<exists>x\<in>s. v x = 0) \<and> setsum v s = 1 \<and> (\<Sum>x\<in>s. v x *\<^sub>R x) = (\<Sum>x\<in>s - {a}. u x *\<^sub>R x)"
   2.351 +    apply (rule_tac x="\<lambda>x. if x = a then 0 else u x" in exI)
   2.352 +    apply (auto simp: setsum.If_cases Diff_eq if_smult fs)
   2.353 +    done }
   2.354 +  ultimately show ?thesis
   2.355 +    using assms
   2.356 +    apply (simp add: rel_frontier_convex_hull_explicit)
   2.357 +    apply (simp add: convex_hull_finite fs Union_SetCompr_eq, auto)
   2.358 +    done
   2.359 +qed
   2.360 +
   2.361 +lemma frontier_convex_hull_eq_rel_frontier:
   2.362 +  fixes s :: "'a::euclidean_space set"
   2.363 +  assumes "~ affine_dependent s"
   2.364 +  shows "frontier(convex hull s) = 
   2.365 +           (if card s \<le> DIM ('a) then convex hull s else rel_frontier(convex hull s))"
   2.366 +  using assms 
   2.367 +  unfolding rel_frontier_def frontier_def 
   2.368 +  by (simp add: affine_independent_span_gt rel_interior_interior  
   2.369 +                finite_imp_compact empty_interior_convex_hull aff_independent_finite)
   2.370 +
   2.371 +lemma frontier_convex_hull_cases:
   2.372 +  fixes s :: "'a::euclidean_space set"
   2.373 +  assumes "~ affine_dependent s"
   2.374 +  shows "frontier(convex hull s) = 
   2.375 +           (if card s \<le> DIM ('a) then convex hull s else \<Union>{convex hull (s - {x}) |x. x \<in> s})"
   2.376 +by (simp add: assms frontier_convex_hull_eq_rel_frontier rel_frontier_convex_hull_cases)
   2.377 +
   2.378 +lemma in_frontier_convex_hull:
   2.379 +  fixes s :: "'a::euclidean_space set"
   2.380 +  assumes "finite s" "card s \<le> Suc (DIM ('a))" "x \<in> s"
   2.381 +  shows   "x \<in> frontier(convex hull s)"
   2.382 +proof (cases "affine_dependent s")
   2.383 +  case True 
   2.384 +  with assms show ?thesis
   2.385 +    apply (auto simp: affine_dependent_def frontier_def finite_imp_compact hull_inc)
   2.386 +    by (metis card.insert_remove convex_hull_subset_affine_hull empty_interior_affine_hull finite_Diff hull_redundant insert_Diff insert_Diff_single insert_not_empty interior_mono not_less_eq_eq subset_empty)
   2.387 +next
   2.388 +  case False 
   2.389 +  { assume "card s = Suc (card Basis)" 
   2.390 +    then have cs: "Suc 0 < card s"
   2.391 +      by (simp add: DIM_positive)
   2.392 +    with subset_singletonD have "\<exists>y \<in> s. y \<noteq> x"
   2.393 +      by (cases "s \<le> {x}") fastforce+
   2.394 +  } note [dest!] = this
   2.395 +  show ?thesis using assms
   2.396 +    unfolding frontier_convex_hull_cases [OF False] Union_SetCompr_eq
   2.397 +    by (auto simp: le_Suc_eq hull_inc)
   2.398 +qed
   2.399 +
   2.400 +lemma not_in_interior_convex_hull:
   2.401 +  fixes s :: "'a::euclidean_space set"
   2.402 +  assumes "finite s" "card s \<le> Suc (DIM ('a))" "x \<in> s"
   2.403 +  shows   "x \<notin> interior(convex hull s)"
   2.404 +using in_frontier_convex_hull [OF assms]
   2.405 +by (metis Diff_iff frontier_def)
   2.406 +
   2.407 +lemma interior_convex_hull_eq_empty:
   2.408 +  fixes s :: "'a::euclidean_space set"
   2.409 +  assumes "card s = Suc (DIM ('a))" "x \<in> s"
   2.410 +  shows   "interior(convex hull s) = {} \<longleftrightarrow> affine_dependent s"
   2.411 +proof -
   2.412 +  { fix a b
   2.413 +    assume ab: "a \<in> interior (convex hull s)" "b \<in> s" "b \<in> affine hull (s - {b})"
   2.414 +    then have "interior(affine hull s) = {}" using assms
   2.415 +      by (metis DIM_positive One_nat_def Suc_mono card.remove card_infinite empty_interior_affine_hull eq_iff hull_redundant insert_Diff not_less zero_le_one)
   2.416 +    then have False using ab
   2.417 +      by (metis convex_hull_subset_affine_hull equals0D interior_mono subset_eq)
   2.418 +  } then
   2.419 +  show ?thesis
   2.420 +    using assms
   2.421 +    apply auto
   2.422 +    apply (metis UNIV_I affine_hull_convex_hull affine_hull_empty affine_independent_span_eq convex_convex_hull empty_iff rel_interior_interior rel_interior_same_affine_hull)
   2.423 +    apply (auto simp: affine_dependent_def)
   2.424 +    done
   2.425 +qed
   2.426  
   2.427  end
     3.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu May 28 10:18:46 2015 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu May 28 14:33:35 2015 +0100
     3.3 @@ -1657,6 +1657,11 @@
     3.4    using maximal_independent_subset[of V] independent_bound
     3.5    by auto
     3.6  
     3.7 +corollary dim_le_card:
     3.8 +  fixes s :: "'a::euclidean_space set"
     3.9 +  shows "finite s \<Longrightarrow> dim s \<le> card s"
    3.10 +by (metis basis_exists card_mono)
    3.11 +
    3.12  text {* Consequences of independence or spanning for cardinality. *}
    3.13  
    3.14  lemma independent_card_le_dim:
     4.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu May 28 10:18:46 2015 +0200
     4.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu May 28 14:33:35 2015 +0100
     4.3 @@ -1222,6 +1222,9 @@
     4.4  lemma norm_conv_dist: "norm x = dist x 0"
     4.5    unfolding dist_norm by simp
     4.6  
     4.7 +lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
     4.8 +  by (simp_all add: dist_norm)
     4.9 +  
    4.10  subsection {* Bounded Linear and Bilinear Operators *}
    4.11  
    4.12  locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +