Extend convex analysis by Bogdan Grechuk
authorhoelzl
Fri Nov 05 14:17:18 2010 +0100 (2010-11-05)
changeset 403770e5d48096f58
parent 40367 6fb991dc074b
child 40378 8809b6489667
Extend convex analysis by Bogdan Grechuk
CONTRIBUTORS
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
     1.1 --- a/CONTRIBUTORS	Fri Nov 05 09:07:14 2010 +0100
     1.2 +++ b/CONTRIBUTORS	Fri Nov 05 14:17:18 2010 +0100
     1.3 @@ -21,6 +21,9 @@
     1.4  * July 2010: Florian Haftmann, TUM
     1.5    Reworking and extension of the Imperative HOL framework.
     1.6  
     1.7 +* October 2010: Bogdan Grechuck, University of Edinburgh
     1.8 +  Extended convex analysis in Multivariate Analysis
     1.9 +
    1.10  
    1.11  Contributions to Isabelle2009-2
    1.12  --------------------------------------
     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 05 09:07:14 2010 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 05 14:17:18 2010 +0100
     2.3 @@ -13,9 +13,307 @@
     2.4  (* To be moved elsewhere                                                     *)
     2.5  (* ------------------------------------------------------------------------- *)
     2.6  
     2.7 +lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)"
     2.8 +  by (metis linear_conv_bounded_linear scaleR.bounded_linear_right)
     2.9 +
    2.10 +lemma injective_scaleR: 
    2.11 +assumes "(c :: real) ~= 0"
    2.12 +shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
    2.13 +by (metis assms datatype_injI injI real_vector.scale_cancel_left)
    2.14 +
    2.15 +lemma linear_add_cmul:
    2.16 +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" 
    2.17 +assumes "linear f"
    2.18 +shows "f(a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x +  b *\<^sub>R f y"
    2.19 +using linear_add[of f] linear_cmul[of f] assms by (simp) 
    2.20 +
    2.21 +lemma mem_convex_2:
    2.22 +  assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v=1"
    2.23 +  shows "(u *\<^sub>R x + v *\<^sub>R y) : S"
    2.24 +  using assms convex_def[of S] by auto
    2.25 +
    2.26 +lemma mem_convex_alt:
    2.27 +  assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v>0"
    2.28 +  shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) : S"
    2.29 +apply (subst mem_convex_2) 
    2.30 +using assms apply (auto simp add: algebra_simps zero_le_divide_iff)
    2.31 +using add_divide_distrib[of u v "u+v"] by auto
    2.32 +
    2.33 +lemma card_ge1: assumes "d ~= {}" "finite d" shows "card d >= 1"
    2.34 +by (metis Suc_eq_plus1 assms(1) assms(2) card_eq_0_iff fact_ge_one_nat fact_num_eq_if_nat one_le_mult_iff plus_nat.add_0)
    2.35 +
    2.36 +lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)" 
    2.37 +by (blast dest: inj_onD)
    2.38 +
    2.39 +lemma independent_injective_on_span_image:
    2.40 +  assumes iS: "independent (S::(_::euclidean_space) set)" 
    2.41 +     and lf: "linear f" and fi: "inj_on f (span S)"
    2.42 +  shows "independent (f ` S)"
    2.43 +proof-
    2.44 +  {fix a assume a: "a : S" "f a : span (f ` S - {f a})"
    2.45 +    have eq: "f ` S - {f a} = f ` (S - {a})" using fi a span_inc
    2.46 +      by (auto simp add: inj_on_def)
    2.47 +    from a have "f a : f ` span (S -{a})"
    2.48 +      unfolding eq span_linear_image[OF lf, of "S - {a}"]  by blast
    2.49 +    moreover have "span (S -{a}) <= span S" using span_mono[of "S-{a}" S] by auto
    2.50 +    ultimately have "a : span (S -{a})" using fi a span_inc by (auto simp add: inj_on_def)
    2.51 +    with a(1) iS  have False by (simp add: dependent_def) }
    2.52 +  then show ?thesis unfolding dependent_def by blast
    2.53 +qed
    2.54 +
    2.55 +lemma dim_image_eq:
    2.56 +fixes f :: "'n::euclidean_space => 'm::euclidean_space"
    2.57 +assumes lf: "linear f" and fi: "inj_on f (span S)" 
    2.58 +shows "dim (f ` S) = dim (S:: ('n::euclidean_space) set)"
    2.59 +proof-
    2.60 +obtain B where B_def: "B<=S & independent B & S <= span B & card B = dim S" 
    2.61 +  using basis_exists[of S] by auto
    2.62 +hence "span S = span B" using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
    2.63 +hence "independent (f ` B)" using independent_injective_on_span_image[of B f] B_def assms by auto
    2.64 +moreover have "card (f ` B) = card B" using assms card_image[of f B] subset_inj_on[of f "span S" B] 
    2.65 +   B_def span_inc by auto
    2.66 +moreover have "(f ` B) <= (f ` S)" using B_def by auto
    2.67 +ultimately have "dim (f ` S) >= dim S" 
    2.68 +  using independent_card_le_dim[of "f ` B" "f ` S"] B_def by auto
    2.69 +from this show ?thesis using dim_image_le[of f S] assms by auto
    2.70 +qed
    2.71 +
    2.72 +lemma linear_injective_on_subspace_0:
    2.73 +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
    2.74 +assumes lf: "linear f" and "subspace S"
    2.75 +  shows "inj_on f S <-> (!x : S. f x = 0 --> x = 0)"
    2.76 +proof-
    2.77 +  have "inj_on f S <-> (!x : S. !y : S. f x = f y --> x = y)" by (simp add: inj_on_def)
    2.78 +  also have "... <-> (!x : S. !y : S. f x - f y = 0 --> x - y = 0)" by simp
    2.79 +  also have "... <-> (!x : S. !y : S. f (x - y) = 0 --> x - y = 0)"
    2.80 +    by (simp add: linear_sub[OF lf])
    2.81 +  also have "... <-> (! x : S. f x = 0 --> x = 0)" 
    2.82 +    using `subspace S` subspace_def[of S] subspace_sub[of S] by auto
    2.83 +  finally show ?thesis .
    2.84 +qed
    2.85 +
    2.86 +lemma subspace_Inter: "(!s : f. subspace s) ==> subspace (Inter f)"
    2.87 +  unfolding subspace_def by auto 
    2.88 +
    2.89 +lemma span_eq[simp]: "(span s = s) <-> subspace s"
    2.90 +proof-
    2.91 +  { fix f assume "f <= subspace"
    2.92 +    hence "subspace (Inter f)" using subspace_Inter[of f] unfolding subset_eq mem_def by auto  }
    2.93 +  thus ?thesis using hull_eq[unfolded mem_def, of subspace s] span_def by auto
    2.94 +qed
    2.95 +
    2.96 +lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d"
    2.97 +  by(auto simp add: inj_on_def euclidean_eq[where 'a='n])
    2.98 +  
    2.99 +lemma finite_substdbasis: "finite {basis i ::'n::euclidean_space |i. i : (d:: nat set)}" (is "finite ?S")
   2.100 +proof-
   2.101 +  have eq: "?S = basis ` d" by blast
   2.102 +  show ?thesis unfolding eq apply(rule finite_subset[OF _ range_basis_finite]) by auto
   2.103 +qed
   2.104 +
   2.105 +lemma card_substdbasis: assumes "d \<subseteq> {..<DIM('n::euclidean_space)}"
   2.106 +  shows "card {basis i ::'n::euclidean_space | i. i : d} = card d" (is "card ?S = _")
   2.107 +proof-
   2.108 +  have eq: "?S = basis ` d" by blast
   2.109 +  show ?thesis unfolding eq using card_image[OF basis_inj_on[of d]] assms by auto
   2.110 +qed
   2.111 +
   2.112 +lemma substdbasis_expansion_unique: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
   2.113 +  shows "setsum (%i. f i *\<^sub>R basis i) d = (x::'a::euclidean_space)
   2.114 +      <-> (!i<DIM('a). (i:d --> f i = x$$i) & (i ~: d --> x $$ i = 0))"
   2.115 +proof- have *:"\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto
   2.116 +  have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp
   2.117 +  have ***:"\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)"
   2.118 +    unfolding euclidean_component.setsum euclidean_scaleR basis_component *
   2.119 +    apply(rule setsum_cong2) using assms by auto
   2.120 +  show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
   2.121 +qed
   2.122 +
   2.123 +lemma independent_substdbasis: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
   2.124 +  shows "independent {basis i ::'a::euclidean_space |i. i : (d :: nat set)}" (is "independent ?A")
   2.125 +proof -
   2.126 +  have *: "{basis i |i. i < DIM('a)} = basis ` {..<DIM('a)}" by auto
   2.127 +  show ?thesis
   2.128 +    apply(intro independent_mono[of "{basis i ::'a |i. i : {..<DIM('a::euclidean_space)}}" "?A"] )
   2.129 +    using independent_basis[where 'a='a] assms by (auto simp: *)
   2.130 +qed
   2.131 +
   2.132 +lemma dim_cball: 
   2.133 +assumes "0<e"
   2.134 +shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)"
   2.135 +proof-
   2.136 +{ fix x :: "'n::euclidean_space" def y == "(e/norm x) *\<^sub>R x"
   2.137 +  hence "y : cball 0 e" using cball_def dist_norm[of 0 y] assms by auto
   2.138 +  moreover have "x = (norm x/e) *\<^sub>R y" using y_def assms by simp
   2.139 +  moreover hence "x = (norm x/e) *\<^sub>R y"  by auto
   2.140 +  ultimately have "x : span (cball 0 e)"
   2.141 +     using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto
   2.142 +} hence "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto 
   2.143 +from this show ?thesis using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp add: dim_UNIV)
   2.144 +qed
   2.145 +
   2.146 +lemma indep_card_eq_dim_span:
   2.147 +fixes B :: "('n::euclidean_space) set"
   2.148 +assumes "independent B"
   2.149 +shows "finite B & card B = dim (span B)" 
   2.150 +  using assms basis_card_eq_dim[of B "span B"] span_inc by auto
   2.151 +
   2.152 +lemma setsum_not_0: "setsum f A ~= 0 ==> EX a:A. f a ~= 0"
   2.153 +  apply(rule ccontr) by auto
   2.154 +
   2.155 +lemma translate_inj_on: 
   2.156 +fixes A :: "('n::euclidean_space) set"
   2.157 +shows "inj_on (%x. a+x) A" unfolding inj_on_def by auto
   2.158 +
   2.159 +lemma translation_assoc:
   2.160 +  fixes a b :: "'a::ab_group_add"
   2.161 +  shows "(\<lambda>x. b+x) ` ((\<lambda>x. a+x) ` S) = (\<lambda>x. (a+b)+x) ` S" by auto
   2.162 +
   2.163 +lemma translation_invert:
   2.164 +  fixes a :: "'a::ab_group_add"
   2.165 +  assumes "(\<lambda>x. a+x) ` A = (\<lambda>x. a+x) ` B"
   2.166 +  shows "A=B"
   2.167 +proof-
   2.168 +  have "(%x. -a+x) ` ((%x. a+x) ` A) = (%x. -a+x) ` ((%x. a+x) ` B)" using assms by auto
   2.169 +  from this show ?thesis using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto 
   2.170 +qed
   2.171 +
   2.172 +lemma translation_galois:
   2.173 +  fixes a :: "'a::ab_group_add"
   2.174 +  shows "T=((\<lambda>x. a+x) ` S) <-> S=((\<lambda>x. (-a)+x) ` T)"
   2.175 +  using translation_assoc[of "-a" a S] apply auto
   2.176 +  using translation_assoc[of a "-a" T] by auto
   2.177 +
   2.178 +lemma translation_inverse_subset:
   2.179 +  assumes "((%x. -a+x) ` V) <= (S :: 'n::ab_group_add set)" 
   2.180 +  shows "V <= ((%x. a+x) ` S)"
   2.181 +proof-
   2.182 +{ fix x assume "x:V" hence "x-a : S" using assms by auto 
   2.183 +  hence "x : {a + v |v. v : S}" apply auto apply (rule exI[of _ "x-a"]) apply simp done 
   2.184 +  hence "x : ((%x. a+x) ` S)" by auto }
   2.185 +  from this show ?thesis by auto
   2.186 +qed
   2.187 +
   2.188  lemma basis_0[simp]:"(basis i::'a::euclidean_space) = 0 \<longleftrightarrow> i\<ge>DIM('a)"
   2.189    using norm_basis[of i, where 'a='a] unfolding norm_eq_zero[where 'a='a,THEN sym] by auto
   2.190  
   2.191 +lemma basis_to_basis_subspace_isomorphism:
   2.192 +  assumes s: "subspace (S:: ('n::euclidean_space) set)"
   2.193 +  and t: "subspace (T :: ('m::euclidean_space) set)"
   2.194 +  and d: "dim S = dim T"
   2.195 +  and B: "B <= S" "independent B" "S <= span B" "card B = dim S"
   2.196 +  and C: "C <= T" "independent C" "T <= span C" "card C = dim T"
   2.197 +  shows "EX f. linear f & f ` B = C & f ` S = T & inj_on f S"
   2.198 +proof-
   2.199 +(* Proof is a modified copy of the proof of similar lemma subspace_isomorphism
   2.200 +*)
   2.201 +  from B independent_bound have fB: "finite B" by blast
   2.202 +  from C independent_bound have fC: "finite C" by blast
   2.203 +  from B(4) C(4) card_le_inj[of B C] d obtain f where
   2.204 +    f: "f ` B \<subseteq> C" "inj_on f B" using `finite B` `finite C` by auto
   2.205 +  from linear_independent_extend[OF B(2)] obtain g where
   2.206 +    g: "linear g" "\<forall>x\<in> B. g x = f x" by blast
   2.207 +  from inj_on_iff_eq_card[OF fB, of f] f(2)
   2.208 +  have "card (f ` B) = card B" by simp
   2.209 +  with B(4) C(4) have ceq: "card (f ` B) = card C" using d
   2.210 +    by simp
   2.211 +  have "g ` B = f ` B" using g(2)
   2.212 +    by (auto simp add: image_iff)
   2.213 +  also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] .
   2.214 +  finally have gBC: "g ` B = C" .
   2.215 +  have gi: "inj_on g B" using f(2) g(2)
   2.216 +    by (auto simp add: inj_on_def)
   2.217 +  note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
   2.218 +  {fix x y assume x: "x \<in> S" and y: "y \<in> S" and gxy:"g x = g y"
   2.219 +    from B(3) x y have x': "x \<in> span B" and y': "y \<in> span B" by blast+
   2.220 +    from gxy have th0: "g (x - y) = 0" by (simp add: linear_sub[OF g(1)])
   2.221 +    have th1: "x - y \<in> span B" using x' y' by (metis span_sub)
   2.222 +    have "x=y" using g0[OF th1 th0] by simp }
   2.223 +  then have giS: "inj_on g S"
   2.224 +    unfolding inj_on_def by blast
   2.225 +  from span_subspace[OF B(1,3) s]
   2.226 +  have "g ` S = span (g ` B)" by (simp add: span_linear_image[OF g(1)])
   2.227 +  also have "\<dots> = span C" unfolding gBC ..
   2.228 +  also have "\<dots> = T" using span_subspace[OF C(1,3) t] .
   2.229 +  finally have gS: "g ` S = T" .
   2.230 +  from g(1) gS giS gBC show ?thesis by blast
   2.231 +qed
   2.232 +
   2.233 +lemma closure_linear_image:
   2.234 +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
   2.235 +assumes "linear f"
   2.236 +shows "f ` (closure S) <= closure (f ` S)"
   2.237 +using image_closure_subset[of S f "closure (f ` S)"] assms linear_conv_bounded_linear[of f] 
   2.238 +linear_continuous_on[of f "closure S"] closed_closure[of "f ` S"] closure_subset[of "f ` S"] by auto
   2.239 +
   2.240 +lemma closure_injective_linear_image:
   2.241 +fixes f :: "('n::euclidean_space) => ('n::euclidean_space)"
   2.242 +assumes "linear f" "inj f"
   2.243 +shows "f ` (closure S) = closure (f ` S)"
   2.244 +proof-
   2.245 +obtain f' where f'_def: "linear f' & f o f' = id & f' o f = id" 
   2.246 +   using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
   2.247 +hence "f' ` closure (f ` S) <= closure (S)"
   2.248 +   using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto
   2.249 +hence "f ` f' ` closure (f ` S) <= f ` closure (S)" by auto
   2.250 +hence "closure (f ` S) <= f ` closure (S)" using image_compose[of f f' "closure (f ` S)"] f'_def by auto
   2.251 +from this show ?thesis using closure_linear_image[of f S] assms by auto 
   2.252 +qed
   2.253 +
   2.254 +lemma closure_direct_sum:
   2.255 +fixes S :: "('n::euclidean_space) set"
   2.256 +fixes T :: "('m::euclidean_space) set"
   2.257 +shows "closure (S <*> T) = closure S <*> closure T"
   2.258 +proof-
   2.259 +{ fix x assume "x : closure S <*> closure T"
   2.260 +  from this obtain xs xt where xst_def: "xs : closure S & xt : closure T & (xs,xt) = x" by auto
   2.261 +  { fix ee assume ee_def: "(ee :: real) > 0"
   2.262 +    def e == "ee/2" hence e_def: "(e :: real)>0 & 2*e=ee" using ee_def by auto
   2.263 +    from this obtain e where e_def: "(e :: real)>0 & 2*e=ee" by auto
   2.264 +    obtain ys where ys_def: "ys : S & (dist ys xs < e)"
   2.265 +      using e_def xst_def closure_approachable[of xs S] by auto
   2.266 +    obtain yt where yt_def: "yt : T & (dist yt xt < e)"
   2.267 +      using e_def xst_def closure_approachable[of xt T] by auto
   2.268 +    from ys_def yt_def have "dist (ys,yt) (xs,xt) < sqrt (2*e^2)" 
   2.269 +      unfolding dist_norm apply (auto simp add: norm_Pair) 
   2.270 +      using mult_strict_mono'[of "norm (ys - xs)" e "norm (ys - xs)" e] e_def
   2.271 +      mult_strict_mono'[of "norm (yt - xt)" e "norm (yt - xt)" e] by (simp add: power2_eq_square)
   2.272 +    hence "((ys,yt) : S <*> T) & (dist (ys,yt) x < 2*e)"
   2.273 +      using e_def sqrt_add_le_add_sqrt[of "e^2" "e^2"] xst_def ys_def yt_def by auto
   2.274 +    hence "EX y: S <*> T. dist y x < ee" using e_def by auto
   2.275 +  } hence "x : closure (S <*> T)" using closure_approachable[of x "S <*> T"] by auto
   2.276 +}
   2.277 +hence "closure (S <*> T) >= closure S <*> closure T" by auto
   2.278 +moreover have "closed (closure S <*> closure T)" using closed_Times by auto
   2.279 +ultimately show ?thesis using closure_minimal[of "S <*> T" "closure S <*> closure T"]
   2.280 +  closure_subset[of S] closure_subset[of T] by auto
   2.281 +qed
   2.282 +
   2.283 +lemma closure_scaleR: 
   2.284 +fixes S :: "('n::euclidean_space) set"
   2.285 +shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
   2.286 +proof-
   2.287 +{ assume "c ~= 0" hence ?thesis using closure_injective_linear_image[of "(op *\<^sub>R c)" S]
   2.288 +      linear_scaleR injective_scaleR by auto 
   2.289 +}
   2.290 +moreover
   2.291 +{ assume zero: "c=0 & S ~= {}"
   2.292 +  hence "closure S ~= {}" using closure_subset by auto
   2.293 +  hence "op *\<^sub>R c ` (closure S) = {0}" using zero by auto
   2.294 +  moreover have "op *\<^sub>R 0 ` S = {0}" using zero by auto
   2.295 +  ultimately have ?thesis using zero by auto
   2.296 +}
   2.297 +moreover
   2.298 +{ assume "S={}" hence ?thesis by auto }
   2.299 +ultimately show ?thesis by blast
   2.300 +qed
   2.301 +
   2.302 +lemma fst_linear: "linear fst" unfolding linear_def by (simp add: algebra_simps)
   2.303 +
   2.304 +lemma snd_linear: "linear snd" unfolding linear_def by (simp add: algebra_simps)
   2.305 +
   2.306 +lemma fst_snd_linear: "linear (%z. fst z + snd z)" unfolding linear_def by (simp add: algebra_simps)
   2.307 +
   2.308  lemma scaleR_2:
   2.309    fixes x :: "'a::real_vector"
   2.310    shows "scaleR 2 x = x + x"
   2.311 @@ -272,6 +570,30 @@
   2.312      apply(rule_tac x=u in exI) by(auto intro!: exI)
   2.313  qed
   2.314  
   2.315 +lemma mem_affine:
   2.316 +  assumes "affine S" "x : S" "y : S" "u+v=1"
   2.317 +  shows "(u *\<^sub>R x + v *\<^sub>R y) : S"
   2.318 +  using assms affine_def[of S] by auto
   2.319 +
   2.320 +lemma mem_affine_3:
   2.321 +  assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1"
   2.322 +  shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S"
   2.323 +proof-
   2.324 +have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}"
   2.325 +  using affine_hull_3[of x y z] assms by auto
   2.326 +moreover have " affine hull {x, y, z} <= affine hull S" 
   2.327 +  using hull_mono[of "{x, y, z}" "S"] assms by auto
   2.328 +moreover have "affine hull S = S" 
   2.329 +  using assms affine_hull_eq[of S] by auto
   2.330 +ultimately show ?thesis by auto 
   2.331 +qed
   2.332 +
   2.333 +lemma mem_affine_3_minus:
   2.334 +  assumes "affine S" "x : S" "y : S" "z : S"
   2.335 +  shows "x + v *\<^sub>R (y-z) : S"
   2.336 +using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps)
   2.337 +
   2.338 +
   2.339  subsection {* Some relations between affine hull and subspaces. *}
   2.340  
   2.341  lemma affine_hull_insert_subset_span:
   2.342 @@ -318,6 +640,163 @@
   2.343    shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
   2.344    using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
   2.345  
   2.346 +subsection{* Parallel Affine Sets *}
   2.347 +
   2.348 +definition affine_parallel :: "'a::real_vector set => 'a::real_vector set => bool"
   2.349 +where "affine_parallel S T = (? a. T = ((%x. a + x) ` S))"
   2.350 +
   2.351 +lemma affine_parallel_expl_aux:
   2.352 +   fixes S T :: "'a::real_vector set"
   2.353 +   assumes "!x. (x : S <-> (a+x) : T)" 
   2.354 +   shows "T = ((%x. a + x) ` S)"
   2.355 +proof-
   2.356 +{ fix x assume "x : T" hence "(-a)+x : S" using assms by auto
   2.357 +  hence " x : ((%x. a + x) ` S)" using imageI[of "-a+x" S "(%x. a+x)"] by auto}
   2.358 +moreover have "T >= ((%x. a + x) ` S)" using assms by auto 
   2.359 +ultimately show ?thesis by auto
   2.360 +qed
   2.361 +
   2.362 +lemma affine_parallel_expl: 
   2.363 +   "affine_parallel S T = (? a. !x. (x : S <-> (a+x) : T))" 
   2.364 +   unfolding affine_parallel_def using affine_parallel_expl_aux[of S _ T] by auto
   2.365 +
   2.366 +lemma affine_parallel_reflex: "affine_parallel S S" unfolding affine_parallel_def apply (rule exI[of _ "0"]) by auto
   2.367 +
   2.368 +lemma affine_parallel_commut:
   2.369 +assumes "affine_parallel A B" shows "affine_parallel B A" 
   2.370 +proof-
   2.371 +from assms obtain a where "B=((%x. a + x) ` A)" unfolding affine_parallel_def by auto 
   2.372 +from this show ?thesis using translation_galois[of B a A] unfolding affine_parallel_def by auto
   2.373 +qed
   2.374 +
   2.375 +lemma affine_parallel_assoc:
   2.376 +assumes "affine_parallel A B" "affine_parallel B C"
   2.377 +shows "affine_parallel A C" 
   2.378 +proof-
   2.379 +from assms obtain ab where "B=((%x. ab + x) ` A)" unfolding affine_parallel_def by auto 
   2.380 +moreover 
   2.381 +from assms obtain bc where "C=((%x. bc + x) ` B)" unfolding affine_parallel_def by auto
   2.382 +ultimately show ?thesis using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto 
   2.383 +qed
   2.384 +
   2.385 +lemma affine_translation_aux:
   2.386 +  fixes a :: "'a::real_vector"
   2.387 +  assumes "affine ((%x. a + x) ` S)" shows "affine S"
   2.388 +proof-
   2.389 +{ fix x y u v
   2.390 +  assume xy: "x : S" "y : S" "(u :: real)+v=1"
   2.391 +  hence "(a+x):((%x. a + x) ` S)" "(a+y):((%x. a + x) ` S)" by auto
   2.392 +  hence h1: "u *\<^sub>R  (a+x) + v *\<^sub>R (a+y) : ((%x. a + x) ` S)" using xy assms unfolding affine_def by auto
   2.393 +  have "u *\<^sub>R (a+x) + v *\<^sub>R (a+y) = (u+v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)" by (simp add:algebra_simps)
   2.394 +  also have "...= a + (u *\<^sub>R x + v *\<^sub>R y)" using `u+v=1` by auto
   2.395 +  ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) : ((%x. a + x) ` S)" using h1 by auto
   2.396 +  hence "u *\<^sub>R x + v *\<^sub>R y : S" by auto
   2.397 +} from this show ?thesis unfolding affine_def by auto
   2.398 +qed
   2.399 +
   2.400 +lemma affine_translation:
   2.401 +  fixes a :: "'a::real_vector"
   2.402 +  shows "affine S <-> affine ((%x. a + x) ` S)"
   2.403 +proof-
   2.404 +have "affine S ==> affine ((%x. a + x) ` S)" using affine_translation_aux[of "-a" "((%x. a + x) ` S)"]  using translation_assoc[of "-a" a S] by auto
   2.405 +from this show ?thesis using affine_translation_aux by auto
   2.406 +qed
   2.407 +
   2.408 +lemma parallel_is_affine:
   2.409 +fixes S T :: "'a::real_vector set"
   2.410 +assumes "affine S" "affine_parallel S T"
   2.411 +shows "affine T"
   2.412 +proof-
   2.413 +  from assms obtain a where "T=((%x. a + x) ` S)" unfolding affine_parallel_def by auto 
   2.414 +  from this show ?thesis using affine_translation assms by auto
   2.415 +qed
   2.416 +
   2.417 +lemma subspace_imp_affine:
   2.418 +  fixes s :: "(_::euclidean_space) set" shows "subspace s \<Longrightarrow> affine s"
   2.419 +  unfolding subspace_def affine_def by auto
   2.420 +
   2.421 +subsection{* Subspace Parallel to an Affine Set *}
   2.422 +
   2.423 +lemma subspace_affine:
   2.424 +  fixes S :: "('n::euclidean_space) set"
   2.425 +  shows "subspace S <-> (affine S & 0 : S)"
   2.426 +proof-
   2.427 +have h0: "subspace S ==> (affine S & 0 : S)" using subspace_imp_affine[of S] subspace_0 by auto
   2.428 +{ assume assm: "affine S & 0 : S"
   2.429 +  { fix c :: real 
   2.430 +    fix x assume x_def: "x : S"
   2.431 +    have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto
   2.432 +    moreover have "(1-c) *\<^sub>R 0 + c *\<^sub>R x : S" using affine_alt[of S] assm x_def by auto
   2.433 +    ultimately have "c *\<^sub>R x : S" by auto
   2.434 +  } hence h1: "!c. !x : S. c *\<^sub>R x : S" by auto
   2.435 +  { fix x y assume xy_def: "x : S" "y : S"
   2.436 +    def u == "(1 :: real)/2"
   2.437 +    have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" by auto
   2.438 +    moreover have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" by (simp add: algebra_simps)
   2.439 +    moreover have "(1-u) *\<^sub>R x + u *\<^sub>R y : S" using affine_alt[of S] assm xy_def by auto
   2.440 +    ultimately have "(1/2) *\<^sub>R (x+y) : S" using u_def by auto
   2.441 +    moreover have "(x+y) = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" by auto
   2.442 +    ultimately have "(x+y) : S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
   2.443 +  } hence "!x : S. !y : S. (x+y) : S" by auto 
   2.444 +  hence "subspace S" using h1 assm unfolding subspace_def by auto
   2.445 +} from this show ?thesis using h0 by metis
   2.446 +qed
   2.447 +
   2.448 +lemma affine_diffs_subspace:
   2.449 +  fixes S :: "('n::euclidean_space) set"
   2.450 +  assumes "affine S" "a : S"
   2.451 +  shows "subspace ((%x. (-a)+x) ` S)"
   2.452 +proof-
   2.453 +have "affine ((%x. (-a)+x) ` S)" using  affine_translation assms by auto  
   2.454 +moreover have "0 : ((%x. (-a)+x) ` S)" using assms exI[of "(%x. x:S & -a+x=0)" a] by auto
   2.455 +ultimately show ?thesis using subspace_affine by auto 
   2.456 +qed
   2.457 +
   2.458 +lemma parallel_subspace_explicit:
   2.459 +fixes a :: "'n::euclidean_space"
   2.460 +assumes "affine S" "a : S"
   2.461 +assumes "L == {y. ? x : S. (-a)+x=y}" 
   2.462 +shows "subspace L & affine_parallel S L" 
   2.463 +proof-
   2.464 +have par: "affine_parallel S L" unfolding affine_parallel_def using assms by auto
   2.465 +hence "affine L" using assms parallel_is_affine by auto  
   2.466 +moreover have "0 : L" using assms apply auto using exI[of "(%x. x:S & -a+x=0)" a] by auto
   2.467 +ultimately show ?thesis using subspace_affine par by auto 
   2.468 +qed
   2.469 +
   2.470 +lemma parallel_subspace_aux:
   2.471 +fixes A B :: "('n::euclidean_space) set"
   2.472 +assumes "subspace A" "subspace B" "affine_parallel A B"
   2.473 +shows "A>=B"
   2.474 +proof-
   2.475 +from assms obtain a where a_def: "!x. (x : A <-> (a+x) : B)" using affine_parallel_expl[of A B] by auto
   2.476 +hence "-a : A" using assms subspace_0[of B] by auto
   2.477 +hence "a : A" using assms subspace_neg[of A "-a"] by auto
   2.478 +from this show ?thesis using assms a_def unfolding subspace_def by auto
   2.479 +qed
   2.480 +
   2.481 +lemma parallel_subspace:
   2.482 +fixes A B :: "('n::euclidean_space) set"
   2.483 +assumes "subspace A" "subspace B" "affine_parallel A B"
   2.484 +shows "A=B"
   2.485 +proof-
   2.486 +have "A>=B" using assms parallel_subspace_aux by auto
   2.487 +moreover have "A<=B" using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto
   2.488 +ultimately show ?thesis by auto  
   2.489 +qed
   2.490 +
   2.491 +lemma affine_parallel_subspace:
   2.492 +fixes S :: "('n::euclidean_space) set"
   2.493 +assumes "affine S" "S ~= {}"
   2.494 +shows "?!L. subspace L & affine_parallel S L" 
   2.495 +proof-
   2.496 +have ex: "? L. subspace L & affine_parallel S L" using assms  parallel_subspace_explicit by auto 
   2.497 +{ fix L1 L2 assume ass: "subspace L1 & affine_parallel S L1" "subspace L2 & affine_parallel S L2"
   2.498 +  hence "affine_parallel L1 L2" using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto
   2.499 +  hence "L1=L2" using ass parallel_subspace by auto
   2.500 +} from this show ?thesis using ex by auto
   2.501 +qed
   2.502 +
   2.503  subsection {* Cones. *}
   2.504  
   2.505  definition
   2.506 @@ -343,6 +822,116 @@
   2.507    apply(rule hull_eq[unfolded mem_def])
   2.508    using cone_Inter unfolding subset_eq by (auto simp add: mem_def)
   2.509  
   2.510 +lemma mem_cone:
   2.511 +  assumes "cone S" "x : S" "c>=0"
   2.512 +  shows "c *\<^sub>R x : S"
   2.513 +  using assms cone_def[of S] by auto
   2.514 +
   2.515 +lemma cone_contains_0:
   2.516 +fixes S :: "('m::euclidean_space) set"
   2.517 +assumes "cone S"
   2.518 +shows "(S ~= {}) <-> (0 : S)"
   2.519 +proof-
   2.520 +{ assume "S ~= {}" from this obtain a where "a:S" by auto
   2.521 +  hence "0 : S" using assms mem_cone[of S a 0] by auto
   2.522 +} from this show ?thesis by auto
   2.523 +qed
   2.524 +
   2.525 +lemma cone_0:
   2.526 +shows "cone {(0 :: 'm::euclidean_space)}"
   2.527 +unfolding cone_def by auto
   2.528 +
   2.529 +lemma cone_Union[intro]: "(!s:f. cone s) --> (cone (Union f))"
   2.530 +  unfolding cone_def by blast
   2.531 +
   2.532 +lemma cone_iff:
   2.533 +fixes S :: "('m::euclidean_space) set"
   2.534 +assumes "S ~= {}"
   2.535 +shows "cone S <-> 0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)"
   2.536 +proof-
   2.537 +{ assume "cone S"
   2.538 +  { fix c assume "(c :: real)>0"
   2.539 +    { fix x assume "x : S" hence "x : (op *\<^sub>R c) ` S" unfolding image_def
   2.540 +        using `cone S` `c>0` mem_cone[of S x "1/c"]
   2.541 +        exI[of "(%t. t:S & x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] by auto
   2.542 +    }
   2.543 +    moreover
   2.544 +    { fix x assume "x : (op *\<^sub>R c) ` S"
   2.545 +      (*from this obtain t where "t:S & x = c *\<^sub>R t" by auto*)
   2.546 +      hence "x:S" using `cone S` `c>0` unfolding cone_def image_def `c>0` by auto
   2.547 +    }
   2.548 +    ultimately have "((op *\<^sub>R c) ` S) = S" by auto
   2.549 +  } hence "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" using `cone S` cone_contains_0[of S] assms by auto
   2.550 +}
   2.551 +moreover
   2.552 +{ assume a: "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)"
   2.553 +  { fix x assume "x:S"
   2.554 +    fix c1 assume "(c1 :: real)>=0"
   2.555 +    hence "(c1=0) | (c1>0)" by auto
   2.556 +    hence "c1 *\<^sub>R x : S" using a `x:S` by auto
   2.557 +  }
   2.558 + hence "cone S" unfolding cone_def by auto
   2.559 +} ultimately show ?thesis by blast
   2.560 +qed
   2.561 +
   2.562 +lemma cone_hull_empty:
   2.563 +"cone hull {} = {}"
   2.564 +by (metis cone_empty cone_hull_eq)
   2.565 +
   2.566 +lemma cone_hull_empty_iff:
   2.567 +fixes S :: "('m::euclidean_space) set"
   2.568 +shows "(S = {}) <-> (cone hull S = {})"
   2.569 +by (metis bot_least cone_hull_empty hull_subset xtrans(5))
   2.570 +
   2.571 +lemma cone_hull_contains_0: 
   2.572 +fixes S :: "('m::euclidean_space) set"
   2.573 +shows "(S ~= {}) <-> (0 : cone hull S)"
   2.574 +using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S] by auto
   2.575 +
   2.576 +lemma mem_cone_hull:
   2.577 +  assumes "x : S" "c>=0"
   2.578 +  shows "c *\<^sub>R x : cone hull S"
   2.579 +by (metis assms cone_cone_hull hull_inc mem_cone mem_def)
   2.580 +
   2.581 +lemma cone_hull_expl:
   2.582 +fixes S :: "('m::euclidean_space) set"
   2.583 +shows "cone hull S = {c *\<^sub>R x | c x. c>=0 & x : S}" (is "?lhs = ?rhs")
   2.584 +proof-
   2.585 +{ fix x assume "x : ?rhs"
   2.586 +  from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
   2.587 +  fix c assume c_def: "(c :: real)>=0"
   2.588 +  hence "c *\<^sub>R x = (c*cx) *\<^sub>R xx" using x_def by (simp add: algebra_simps)
   2.589 +  moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto
   2.590 +  ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto
   2.591 +} hence "cone ?rhs" unfolding cone_def by auto
   2.592 +  hence "?rhs : cone" unfolding mem_def by auto
   2.593 +{ fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto
   2.594 +  hence "x : ?rhs" by auto
   2.595 +} hence "S <= ?rhs" by auto
   2.596 +hence "?lhs <= ?rhs" using `?rhs : cone` hull_minimal[of S "?rhs" "cone"] by auto
   2.597 +moreover
   2.598 +{ fix x assume "x : ?rhs"
   2.599 +  from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
   2.600 +  hence "xx : cone hull S" using hull_subset[of S] by auto
   2.601 +  hence "x : ?lhs" using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto
   2.602 +} ultimately show ?thesis by auto
   2.603 +qed
   2.604 +
   2.605 +lemma cone_closure:
   2.606 +fixes S :: "('m::euclidean_space) set"
   2.607 +assumes "cone S"
   2.608 +shows "cone (closure S)"
   2.609 +proof-
   2.610 +{ assume "S = {}" hence ?thesis by auto }
   2.611 +moreover
   2.612 +{ assume "S ~= {}" hence "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto
   2.613 +  hence "0:(closure S) & (!c. c>0 --> op *\<^sub>R c ` (closure S) = (closure S))"
   2.614 +     using closure_subset by (auto simp add: closure_scaleR)
   2.615 +  hence ?thesis using cone_iff[of "closure S"] by auto
   2.616 +}
   2.617 +ultimately show ?thesis by blast
   2.618 +qed
   2.619 +
   2.620  subsection {* Affine dependence and consequential theorems (from Lars Schewe). *}
   2.621  
   2.622  definition
   2.623 @@ -514,6 +1103,28 @@
   2.624    shows "finite s \<Longrightarrow> bounded(convex hull s)"
   2.625    using bounded_convex_hull finite_imp_bounded by auto
   2.626  
   2.627 +subsection {* Convex hull is "preserved" by a linear function. *}
   2.628 +
   2.629 +lemma convex_hull_linear_image:
   2.630 +  assumes "bounded_linear f"
   2.631 +  shows "f ` (convex hull s) = convex hull (f ` s)"
   2.632 +  apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3  
   2.633 +  apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
   2.634 +  apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
   2.635 +proof-
   2.636 +  interpret f: bounded_linear f by fact
   2.637 +  show "convex {x. f x \<in> convex hull f ` s}" 
   2.638 +  unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next
   2.639 +  interpret f: bounded_linear f by fact
   2.640 +  show "convex {x. x \<in> f ` (convex hull s)}" using  convex_convex_hull[unfolded convex_def, of s] 
   2.641 +    unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
   2.642 +qed auto
   2.643 +
   2.644 +lemma in_convex_hull_linear_image:
   2.645 +  assumes "bounded_linear f" "x \<in> convex hull s"
   2.646 +  shows "(f x) \<in> convex hull (f ` s)"
   2.647 +using convex_hull_linear_image[OF assms(1)] assms(2) by auto
   2.648 +
   2.649  subsection {* Stepping theorems for convex hulls of finite sets. *}
   2.650  
   2.651  lemma convex_hull_empty[simp]: "convex hull {} = {}"
   2.652 @@ -775,10 +1386,6 @@
   2.653  text {* TODO: Generalize linear algebra concepts defined in @{text
   2.654  Euclidean_Space.thy} so that we can generalize these lemmas. *}
   2.655  
   2.656 -lemma subspace_imp_affine:
   2.657 -  fixes s :: "(_::euclidean_space) set" shows "subspace s \<Longrightarrow> affine s"
   2.658 -  unfolding subspace_def affine_def by auto
   2.659 -
   2.660  lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
   2.661    unfolding affine_def convex_def by auto
   2.662  
   2.663 @@ -952,6 +1559,979 @@
   2.664    thus "x \<in> convex hull p" using hull_mono[OF `s\<subseteq>p`] by auto
   2.665  qed
   2.666  
   2.667 +
   2.668 +subsection {* Some Properties of Affine Dependent Sets *}
   2.669 +
   2.670 +lemma affine_independent_empty: "~(affine_dependent {})"
   2.671 +  by (simp add: affine_dependent_def)
   2.672 +
   2.673 +lemma affine_independent_sing:
   2.674 +fixes a :: "'n::euclidean_space" 
   2.675 +shows "~(affine_dependent {a})"
   2.676 + by (simp add: affine_dependent_def)
   2.677 +
   2.678 +lemma affine_hull_translation:
   2.679 +"affine hull ((%x. a + x) `  S) = (%x. a + x) ` (affine hull S)"
   2.680 +proof-
   2.681 +have "affine ((%x. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by auto
   2.682 +moreover have "(%x. a + x) `  S <= (%x. a + x) ` (affine hull S)" using hull_subset[of S] by auto
   2.683 +ultimately have h1: "affine hull ((%x. a + x) `  S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal mem_def)
   2.684 +have "affine((%x. -a + x) ` (affine hull ((%x. a + x) `  S)))"  using affine_translation affine_affine_hull by auto
   2.685 +moreover have "(%x. -a + x) ` (%x. a + x) `  S <= (%x. -a + x) ` (affine hull ((%x. a + x) `  S))" using hull_subset[of "(%x. a + x) `  S"] by auto 
   2.686 +moreover have "S=(%x. -a + x) ` (%x. a + x) `  S" using  translation_assoc[of "-a" a] by auto
   2.687 +ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) `  S)) >= (affine hull S)" by (metis hull_minimal mem_def)
   2.688 +hence "affine hull ((%x. a + x) `  S) >= (%x. a + x) ` (affine hull S)" by auto
   2.689 +from this show ?thesis using h1 by auto
   2.690 +qed
   2.691 +
   2.692 +lemma affine_dependent_translation:
   2.693 +  assumes "affine_dependent S"
   2.694 +  shows "affine_dependent ((%x. a + x) ` S)"
   2.695 +proof-
   2.696 +obtain x where x_def: "x : S & x : affine hull (S - {x})" using assms affine_dependent_def by auto
   2.697 +have "op + a ` (S - {x}) = op + a ` S - {a + x}" by auto
   2.698 +hence "a+x : affine hull ((%x. a + x) ` S - {a+x})" using  affine_hull_translation[of a "S-{x}"] x_def by auto
   2.699 +moreover have "a+x : (%x. a + x) ` S" using x_def by auto  
   2.700 +ultimately show ?thesis unfolding affine_dependent_def by auto 
   2.701 +qed
   2.702 +
   2.703 +lemma affine_dependent_translation_eq:
   2.704 +  "affine_dependent S <-> affine_dependent ((%x. a + x) ` S)"
   2.705 +proof-
   2.706 +{ assume "affine_dependent ((%x. a + x) ` S)" 
   2.707 +  hence "affine_dependent S" using affine_dependent_translation[of "((%x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] by auto  
   2.708 +} from this show ?thesis using affine_dependent_translation by auto
   2.709 +qed
   2.710 +
   2.711 +lemma affine_hull_0_dependent:
   2.712 +  fixes S ::  "('n::euclidean_space) set"
   2.713 +  assumes "0 : affine hull S"
   2.714 +  shows "dependent S"
   2.715 +proof-
   2.716 +obtain s u where s_u_def: "finite s & s ~= {} & s <= S & setsum u s = 1 & (SUM v:s. u v *\<^sub>R v) = 0" using assms affine_hull_explicit[of S] by auto
   2.717 +hence "EX v:s. u v ~= 0" using setsum_not_0[of "u" "s"] by auto 
   2.718 +hence "finite s & s <= S & (EX v:s. u v ~= 0 & (SUM v:s. u v *\<^sub>R v) = 0)" using s_u_def by auto
   2.719 +from this show ?thesis unfolding dependent_explicit[of S] by auto
   2.720 +qed
   2.721 +
   2.722 +lemma affine_dependent_imp_dependent2:
   2.723 +  fixes S :: "('n::euclidean_space) set" 
   2.724 +  assumes "affine_dependent (insert 0 S)"
   2.725 +  shows "dependent S"
   2.726 +proof-
   2.727 +obtain x where x_def: "x:insert 0 S & x : affine hull (insert 0 S - {x})" using affine_dependent_def[of "(insert 0 S)"] assms by blast
   2.728 +hence "x : span (insert 0 S - {x})" using affine_hull_subset_span by auto
   2.729 +moreover have "span (insert 0 S - {x}) = span (S - {x})" using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto
   2.730 +ultimately have "x : span (S - {x})" by auto
   2.731 +hence "(x~=0) ==> dependent S" using x_def dependent_def by auto
   2.732 +moreover
   2.733 +{ assume "x=0" hence "0 : affine hull S" using x_def hull_mono[of "S - {0}" S] by auto
   2.734 +               hence "dependent S" using affine_hull_0_dependent by auto  
   2.735 +} ultimately show ?thesis by auto
   2.736 +qed
   2.737 +
   2.738 +lemma affine_dependent_iff_dependent:
   2.739 +  fixes S :: "('n::euclidean_space) set" 
   2.740 +  assumes "a ~: S"
   2.741 +  shows "affine_dependent (insert a S) <-> dependent ((%x. -a + x) ` S)" 
   2.742 +proof-
   2.743 +have "(op + (- a) ` S)={x - a| x . x : S}" by auto
   2.744 +from this show ?thesis using affine_dependent_translation_eq[of "(insert a S)" "-a"] 
   2.745 +      affine_dependent_imp_dependent2 assms 
   2.746 +      dependent_imp_affine_dependent[of a S] by auto
   2.747 +qed
   2.748 +
   2.749 +lemma affine_dependent_iff_dependent2:
   2.750 +  fixes S :: "('n::euclidean_space) set" 
   2.751 +  assumes "a : S"
   2.752 +  shows "affine_dependent S <-> dependent ((%x. -a + x) ` (S-{a}))"
   2.753 +proof-
   2.754 +have "insert a (S - {a})=S" using assms by auto
   2.755 +from this show ?thesis using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto 
   2.756 +qed
   2.757 +
   2.758 +lemma affine_hull_insert_span_gen:
   2.759 +  fixes a :: "_::euclidean_space"
   2.760 +  shows "affine hull (insert a s) = (%x. a+x) ` span ((%x. -a+x) ` s)" 
   2.761 +proof-
   2.762 +have h1: "{x - a |x. x : s}=((%x. -a+x) ` s)" by auto
   2.763 +{ assume "a ~: s" hence ?thesis using affine_hull_insert_span[of a s] h1 by auto}  
   2.764 +moreover
   2.765 +{ assume a1: "a : s"
   2.766 +  have "EX x. x:s & -a+x=0" apply (rule exI[of _ a]) using a1 by auto
   2.767 +  hence "insert 0 ((%x. -a+x) ` (s - {a}))=(%x. -a+x) ` s" by auto
   2.768 +  hence "span ((%x. -a+x) ` (s - {a}))=span ((%x. -a+x) ` s)" 
   2.769 +    using span_insert_0[of "op + (- a) ` (s - {a})"] by auto
   2.770 +  moreover have "{x - a |x. x : (s - {a})}=((%x. -a+x) ` (s - {a}))" by auto 
   2.771 +  moreover have "insert a (s - {a})=(insert a s)" using assms by auto
   2.772 +  ultimately have ?thesis using assms affine_hull_insert_span[of "a" "s-{a}"] by auto
   2.773 +} 
   2.774 +ultimately show ?thesis by auto  
   2.775 +qed
   2.776 +
   2.777 +lemma affine_hull_span2:
   2.778 +  fixes a :: "_::euclidean_space"
   2.779 +  assumes "a : s"
   2.780 +  shows "affine hull s = (%x. a+x) ` span ((%x. -a+x) ` (s-{a}))"
   2.781 +  using affine_hull_insert_span_gen[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
   2.782 +
   2.783 +lemma affine_hull_span_gen:
   2.784 +  fixes a :: "_::euclidean_space"
   2.785 +  assumes "a : affine hull s"
   2.786 +  shows "affine hull s = (%x. a+x) ` span ((%x. -a+x) ` s)"
   2.787 +proof-
   2.788 +have "affine hull (insert a s) = affine hull s" using hull_redundant[of a affine s] assms by auto
   2.789 +from this show ?thesis using affine_hull_insert_span_gen[of a "s"] by auto
   2.790 +qed
   2.791 +
   2.792 +lemma affine_hull_span_0:
   2.793 +  assumes "(0 :: _::euclidean_space) : affine hull S"
   2.794 +  shows "affine hull S = span S"
   2.795 +using affine_hull_span_gen[of "0" S] assms by auto
   2.796 +
   2.797 +
   2.798 +lemma extend_to_affine_basis:
   2.799 +fixes S V :: "('n::euclidean_space) set"
   2.800 +assumes "~(affine_dependent S)" "S <= V" "S~={}"
   2.801 +shows "? T. ~(affine_dependent T) & S<=T & T<=V & affine hull T = affine hull V"
   2.802 +proof-
   2.803 +obtain a where a_def: "a : S" using assms by auto
   2.804 +hence h0: "independent  ((%x. -a + x) ` (S-{a}))" using affine_dependent_iff_dependent2 assms by auto
   2.805 +from this obtain B 
   2.806 +   where B_def: "(%x. -a+x) ` (S - {a}) <= B & B <= (%x. -a+x) ` V & independent B & (%x. -a+x) ` V <= span B" 
   2.807 +   using maximal_independent_subset_extend[of "(%x. -a+x) ` (S-{a})" "(%x. -a + x) ` V"] assms by blast
   2.808 +def T == "(%x. a+x) ` (insert 0 B)" hence "T=insert a ((%x. a+x) ` B)" by auto
   2.809 +hence "affine hull T = (%x. a+x) ` span B" using affine_hull_insert_span_gen[of a "((%x. a+x) ` B)"] translation_assoc[of "-a" a B] by auto
   2.810 +hence "V <= affine hull T" using B_def assms translation_inverse_subset[of a V "span B"] by auto
   2.811 +moreover have "T<=V" using T_def B_def a_def assms by auto
   2.812 +ultimately have "affine hull T = affine hull V" 
   2.813 +    by (metis Int_absorb1 Int_absorb2 Int_commute Int_lower2 assms hull_hull hull_mono) 
   2.814 +moreover have "S<=T" using T_def B_def translation_inverse_subset[of a "S-{a}" B] by auto
   2.815 +moreover have "~(affine_dependent T)" using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B_def by auto
   2.816 +ultimately show ?thesis using `T<=V` by auto
   2.817 +qed
   2.818 +
   2.819 +lemma affine_basis_exists: 
   2.820 +fixes V :: "('n::euclidean_space) set"
   2.821 +shows "? B. B <= V & ~(affine_dependent B) & affine hull V = affine hull B"
   2.822 +proof-
   2.823 +{ assume empt: "V={}" have "? B. B <= V & ~(affine_dependent B) & (affine hull V=affine hull B)" using empt affine_independent_empty by auto
   2.824 +}
   2.825 +moreover
   2.826 +{ assume nonempt: "V~={}" obtain x where "x:V" using nonempt by auto
   2.827 +  hence "? B. B <= V & ~(affine_dependent B) & (affine hull V=affine hull B)"
   2.828 +  using affine_dependent_def[of "{x}"] extend_to_affine_basis[of "{x}:: ('n::euclidean_space) set" V] by auto
   2.829 +}
   2.830 +ultimately show ?thesis by auto
   2.831 +qed
   2.832 +
   2.833 +subsection {* Affine Dimension of a Set *}
   2.834 +
   2.835 +definition "aff_dim V = (SOME d :: int. ? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = d+1))"
   2.836 +
   2.837 +lemma aff_dim_basis_exists:
   2.838 +  fixes V :: "('n::euclidean_space) set" 
   2.839 +  shows "? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)"
   2.840 +proof-
   2.841 +obtain B where B_def: "~(affine_dependent B) & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto
   2.842 +from this show ?thesis unfolding aff_dim_def some_eq_ex[of "%d. ? (B :: ('n::euclidean_space) set). (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = d+1)"] apply auto apply (rule exI[of _ "int (card B)-(1 :: int)"]) apply (rule exI[of _ "B"]) by auto
   2.843 +qed
   2.844 +
   2.845 +lemma affine_hull_nonempty: "(S ~= {}) <-> affine hull S ~= {}"
   2.846 +proof-
   2.847 +fix S have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto 
   2.848 +moreover have "affine hull S = {} ==> S = {}" unfolding hull_def by auto
   2.849 +ultimately show "(S ~= {}) <-> affine hull S ~= {}" by blast
   2.850 +qed
   2.851 +
   2.852 +lemma aff_dim_parallel_subspace_aux:
   2.853 +fixes B :: "('n::euclidean_space) set"
   2.854 +assumes "~(affine_dependent B)" "a:B"
   2.855 +shows "finite B & ((card B) - 1 = dim (span ((%x. -a+x) ` (B-{a}))))" 
   2.856 +proof-
   2.857 +have "independent ((%x. -a + x) ` (B-{a}))" using affine_dependent_iff_dependent2 assms by auto
   2.858 +hence fin: "dim (span ((%x. -a+x) ` (B-{a}))) = card ((%x. -a + x) ` (B-{a}))" "finite ((%x. -a + x) ` (B - {a}))"  using indep_card_eq_dim_span[of "(%x. -a+x) ` (B-{a})"] by auto
   2.859 +{ assume emp: "(%x. -a + x) ` (B - {a}) = {}" 
   2.860 +  have "B=insert a ((%x. a + x) ` (%x. -a + x) ` (B - {a}))" using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto
   2.861 +  hence "B={a}" using emp by auto
   2.862 +  hence ?thesis using assms fin by auto  
   2.863 +}
   2.864 +moreover
   2.865 +{ assume "(%x. -a + x) ` (B - {a}) ~= {}"
   2.866 +  hence "card ((%x. -a + x) ` (B - {a}))>0" using fin by auto
   2.867 +  moreover have h1: "card ((%x. -a + x) ` (B-{a})) = card (B-{a})"  
   2.868 +     apply (rule card_image) using translate_inj_on by auto
   2.869 +  ultimately have "card (B-{a})>0" by auto
   2.870 +  hence "finite(B-{a})" using card_gt_0_iff[of "(B - {a})"] by auto
   2.871 +  moreover hence "(card (B-{a})= (card B) - 1)" using card_Diff_singleton assms by auto
   2.872 +  ultimately have ?thesis using fin h1 by auto
   2.873 +} ultimately show ?thesis by auto
   2.874 +qed
   2.875 +
   2.876 +lemma aff_dim_parallel_subspace:
   2.877 +fixes V L :: "('n::euclidean_space) set"
   2.878 +assumes "V ~= {}"
   2.879 +assumes "subspace L" "affine_parallel (affine hull V) L"
   2.880 +shows "aff_dim V=int(dim L)"
   2.881 +proof-
   2.882 +obtain B where B_def: "affine hull B = affine hull V & ~ affine_dependent B & int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto
   2.883 +hence "B~={}" using assms B_def  affine_hull_nonempty[of V] affine_hull_nonempty[of B] by auto 
   2.884 +from this obtain a where a_def: "a : B" by auto
   2.885 +def Lb == "span ((%x. -a+x) ` (B-{a}))"
   2.886 +  moreover have "affine_parallel (affine hull B) Lb"
   2.887 +     using Lb_def B_def assms affine_hull_span2[of a B] a_def  affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto
   2.888 +  moreover have "subspace Lb" using Lb_def subspace_span by auto
   2.889 +  moreover have "affine hull B ~= {}" using assms B_def affine_hull_nonempty[of V] by auto
   2.890 +  ultimately have "L=Lb" using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B_def by auto 
   2.891 +  hence "dim L=dim Lb" by auto 
   2.892 +  moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def B_def by auto
   2.893 +(*  hence "card B=dim Lb+1" using `B~={}` card_gt_0_iff[of B] by auto *)
   2.894 +  ultimately show ?thesis using B_def `B~={}` card_gt_0_iff[of B] by auto
   2.895 +qed
   2.896 +
   2.897 +lemma aff_independent_finite:
   2.898 +fixes B :: "('n::euclidean_space) set"
   2.899 +assumes "~(affine_dependent B)"
   2.900 +shows "finite B"
   2.901 +proof-
   2.902 +{ assume "B~={}" from this obtain a where "a:B" by auto 
   2.903 +  hence ?thesis using aff_dim_parallel_subspace_aux assms by auto 
   2.904 +} from this show ?thesis by auto
   2.905 +qed
   2.906 +
   2.907 +lemma independent_finite:
   2.908 +fixes B :: "('n::euclidean_space) set"
   2.909 +assumes "independent B" 
   2.910 +shows "finite B"
   2.911 +using affine_dependent_imp_dependent[of B] aff_independent_finite[of B] assms by auto
   2.912 +
   2.913 +lemma subspace_dim_equal:
   2.914 +assumes "subspace (S :: ('n::euclidean_space) set)" "subspace T" "S <= T" "dim S >= dim T"
   2.915 +shows "S=T"
   2.916 +proof- 
   2.917 +obtain B where B_def: "B <= S & independent B & S <= span B & (card B = dim S)" using basis_exists[of S] by auto
   2.918 +hence "span B <= S" using span_mono[of B S] span_eq[of S] assms by metis 
   2.919 +hence "span B = S" using B_def by auto
   2.920 +have "dim S = dim T" using assms dim_subset[of S T] by auto
   2.921 +hence "T <= span B" using card_eq_dim[of B T] B_def independent_finite assms by auto
   2.922 +from this show ?thesis using assms `span B=S` by auto
   2.923 +qed
   2.924 +
   2.925 +lemma span_substd_basis:  assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
   2.926 +  shows "(span {basis i | i. i : d}) = {x::'a::euclidean_space. (!i<DIM('a). i ~: d --> x$$i = 0)}"
   2.927 +  (is "span ?A = ?B")
   2.928 +proof-
   2.929 +have "?A <= ?B" by auto
   2.930 +moreover have s: "subspace ?B" using subspace_substandard[of "%i. i ~: d"] .
   2.931 +ultimately have "span ?A <= ?B" using span_mono[of "?A" "?B"] span_eq[of "?B"] by blast
   2.932 +moreover have "card d <= dim (span ?A)" using independent_card_le_dim[of "?A" "span ?A"] 
   2.933 +   independent_substdbasis[OF assms] card_substdbasis[OF assms] span_inc[of "?A"] by auto
   2.934 +moreover hence "dim ?B <= dim (span ?A)" using dim_substandard[OF assms] by auto
   2.935 +ultimately show ?thesis using s subspace_dim_equal[of "span ?A" "?B"] 
   2.936 +  subspace_span[of "?A"] by auto
   2.937 +qed
   2.938 +
   2.939 +lemma basis_to_substdbasis_subspace_isomorphism:
   2.940 +fixes B :: "('a::euclidean_space) set" 
   2.941 +assumes "independent B"
   2.942 +shows "EX f d. card d = card B & linear f & f ` B = {basis i::'a |i. i : (d :: nat set)} & 
   2.943 +       f ` span B = {x. ALL i<DIM('a). i ~: d --> x $$ i = (0::real)} &  inj_on f (span B) \<and> d\<subseteq>{..<DIM('a)}" 
   2.944 +proof-
   2.945 +  have B:"card B=dim B" using dim_unique[of B B "card B"] assms span_inc[of B] by auto
   2.946 +  def d \<equiv> "{..<dim B}" have t:"card d = dim B" unfolding d_def by auto
   2.947 +  have "dim B <= DIM('a)" using dim_subset_UNIV[of B] by auto
   2.948 +  hence d:"d\<subseteq>{..<DIM('a)}" unfolding d_def by auto
   2.949 +  let ?t = "{x::'a::euclidean_space. !i<DIM('a). i ~: d --> x$$i = 0}"
   2.950 +  have "EX f. linear f & f ` B = {basis i |i. i : d} &
   2.951 +    f ` span B = ?t & inj_on f (span B)"
   2.952 +    apply (rule basis_to_basis_subspace_isomorphism[of "span B" ?t B "{basis i |i. i : d}"])
   2.953 +    apply(rule subspace_span) apply(rule subspace_substandard) defer
   2.954 +    apply(rule span_inc) apply(rule assms) defer unfolding dim_span[of B] apply(rule B)
   2.955 +    unfolding span_substd_basis[OF d,THEN sym] card_substdbasis[OF d] apply(rule span_inc)
   2.956 +    apply(rule independent_substdbasis[OF d]) apply(rule,assumption)
   2.957 +    unfolding t[THEN sym] span_substd_basis[OF d] dim_substandard[OF d] by auto
   2.958 +  from this t `card B=dim B` show ?thesis using d by auto 
   2.959 +qed
   2.960 +
   2.961 +lemma aff_dim_empty:
   2.962 +fixes S :: "('n::euclidean_space) set" 
   2.963 +shows "S = {} <-> aff_dim S = -1"
   2.964 +proof-
   2.965 +obtain B where "affine hull B = affine hull S & ~ affine_dependent B & int (card B) = aff_dim S + 1" using aff_dim_basis_exists by auto
   2.966 +moreover hence "S={} <-> B={}" using affine_hull_nonempty[of B] affine_hull_nonempty[of S] by auto
   2.967 +ultimately show ?thesis using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
   2.968 +qed
   2.969 +
   2.970 +lemma aff_dim_affine_hull:
   2.971 +fixes S :: "('n::euclidean_space) set"
   2.972 +shows "aff_dim (affine hull S)=aff_dim S" 
   2.973 +unfolding aff_dim_def using hull_hull[of _ S] by auto 
   2.974 +
   2.975 +lemma aff_dim_affine_hull2:
   2.976 +fixes S T :: "('n::euclidean_space) set"
   2.977 +assumes "affine hull S=affine hull T"
   2.978 +shows "aff_dim S=aff_dim T" unfolding aff_dim_def using assms by auto
   2.979 +
   2.980 +lemma aff_dim_unique: 
   2.981 +fixes B V :: "('n::euclidean_space) set" 
   2.982 +assumes "(affine hull B=affine hull V) & ~(affine_dependent B)"
   2.983 +shows "of_nat(card B) = aff_dim V+1"
   2.984 +proof-
   2.985 +{ assume "B={}" hence "V={}" using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms by auto
   2.986 +  hence "aff_dim V = (-1::int)"  using aff_dim_empty by auto  
   2.987 +  hence ?thesis using `B={}` by auto
   2.988 +}
   2.989 +moreover
   2.990 +{ assume "B~={}" from this obtain a where a_def: "a:B" by auto 
   2.991 +  def Lb == "span ((%x. -a+x) ` (B-{a}))"
   2.992 +  have "affine_parallel (affine hull B) Lb"
   2.993 +     using Lb_def affine_hull_span2[of a B] a_def  affine_parallel_commut[of "Lb" "(affine hull B)"] 
   2.994 +     unfolding affine_parallel_def by auto
   2.995 +  moreover have "subspace Lb" using Lb_def subspace_span by auto
   2.996 +  ultimately have "aff_dim B=int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] `B~={}` by auto 
   2.997 +  moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def assms by auto
   2.998 +  ultimately have "(of_nat(card B) = aff_dim B+1)" using  `B~={}` card_gt_0_iff[of B] by auto
   2.999 +  hence ?thesis using aff_dim_affine_hull2 assms by auto
  2.1000 +} ultimately show ?thesis by blast
  2.1001 +qed
  2.1002 +
  2.1003 +lemma aff_dim_affine_independent: 
  2.1004 +fixes B :: "('n::euclidean_space) set" 
  2.1005 +assumes "~(affine_dependent B)"
  2.1006 +shows "of_nat(card B) = aff_dim B+1"
  2.1007 +  using aff_dim_unique[of B B] assms by auto
  2.1008 +
  2.1009 +lemma aff_dim_sing: 
  2.1010 +fixes a :: "'n::euclidean_space" 
  2.1011 +shows "aff_dim {a}=0"
  2.1012 +  using aff_dim_affine_independent[of "{a}"] affine_independent_sing by auto
  2.1013 +
  2.1014 +lemma aff_dim_inner_basis_exists:
  2.1015 +  fixes V :: "('n::euclidean_space) set" 
  2.1016 +  shows "? B. B<=V & (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)"
  2.1017 +proof-
  2.1018 +obtain B where B_def: "~(affine_dependent B) & B<=V & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto
  2.1019 +moreover hence "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto
  2.1020 +ultimately show ?thesis by auto
  2.1021 +qed
  2.1022 +
  2.1023 +lemma aff_dim_le_card:
  2.1024 +fixes V :: "('n::euclidean_space) set" 
  2.1025 +assumes "finite V"
  2.1026 +shows "aff_dim V <= of_nat(card V) - 1"
  2.1027 + proof-
  2.1028 + obtain B where B_def: "B<=V & (of_nat(card B) = aff_dim V+1)" using aff_dim_inner_basis_exists[of V] by auto 
  2.1029 + moreover hence "card B <= card V" using assms card_mono by auto
  2.1030 + ultimately show ?thesis by auto
  2.1031 +qed
  2.1032 +
  2.1033 +lemma aff_dim_parallel_eq:
  2.1034 +fixes S T :: "('n::euclidean_space) set"
  2.1035 +assumes "affine_parallel (affine hull S) (affine hull T)"
  2.1036 +shows "aff_dim S=aff_dim T"
  2.1037 +proof-
  2.1038 +{ assume "T~={}" "S~={}" 
  2.1039 +  from this obtain L where L_def: "subspace L & affine_parallel (affine hull T) L" 
  2.1040 +       using affine_parallel_subspace[of "affine hull T"] affine_affine_hull[of T] affine_hull_nonempty by auto
  2.1041 +  hence "aff_dim T = int(dim L)" using aff_dim_parallel_subspace `T~={}` by auto
  2.1042 +  moreover have "subspace L & affine_parallel (affine hull S) L" 
  2.1043 +     using L_def affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto
  2.1044 +  moreover hence "aff_dim S = int(dim L)" using aff_dim_parallel_subspace `S~={}` by auto 
  2.1045 +  ultimately have ?thesis by auto
  2.1046 +}
  2.1047 +moreover
  2.1048 +{ assume "S={}" hence "S={} & T={}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto
  2.1049 +  hence ?thesis using aff_dim_empty by auto
  2.1050 +}
  2.1051 +moreover
  2.1052 +{ assume "T={}" hence "S={} & T={}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto
  2.1053 +  hence ?thesis using aff_dim_empty by auto
  2.1054 +}
  2.1055 +ultimately show ?thesis by blast
  2.1056 +qed
  2.1057 +
  2.1058 +lemma aff_dim_translation_eq:
  2.1059 +fixes a :: "'n::euclidean_space"
  2.1060 +shows "aff_dim ((%x. a + x) ` S)=aff_dim S" 
  2.1061 +proof-
  2.1062 +have "affine_parallel (affine hull S) (affine hull ((%x. a + x) ` S))" unfolding affine_parallel_def apply (rule exI[of _ "a"]) using affine_hull_translation[of a S] by auto
  2.1063 +from this show ?thesis using  aff_dim_parallel_eq[of S "(%x. a + x) ` S"] by auto 
  2.1064 +qed
  2.1065 +
  2.1066 +lemma aff_dim_affine:
  2.1067 +fixes S L :: "('n::euclidean_space) set"
  2.1068 +assumes "S ~= {}" "affine S"
  2.1069 +assumes "subspace L" "affine_parallel S L"
  2.1070 +shows "aff_dim S=int(dim L)" 
  2.1071 +proof-
  2.1072 +have 1: "(affine hull S) = S" using assms affine_hull_eq[of S] by auto 
  2.1073 +hence "affine_parallel (affine hull S) L" using assms by (simp add:1)
  2.1074 +from this show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast 
  2.1075 +qed
  2.1076 +
  2.1077 +lemma dim_affine_hull:
  2.1078 +fixes S :: "('n::euclidean_space) set"
  2.1079 +shows "dim (affine hull S)=dim S"
  2.1080 +proof-
  2.1081 +have "dim (affine hull S)>=dim S" using dim_subset by auto
  2.1082 +moreover have "dim(span S) >= dim (affine hull S)" using dim_subset affine_hull_subset_span by auto
  2.1083 +moreover have "dim(span S)=dim S" using dim_span by auto
  2.1084 +ultimately show ?thesis by auto
  2.1085 +qed
  2.1086 +
  2.1087 +lemma aff_dim_subspace:
  2.1088 +fixes S :: "('n::euclidean_space) set"
  2.1089 +assumes "S ~= {}" "subspace S"
  2.1090 +shows "aff_dim S=int(dim S)" using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] by auto 
  2.1091 +
  2.1092 +lemma aff_dim_zero:
  2.1093 +fixes S :: "('n::euclidean_space) set"
  2.1094 +assumes "0 : affine hull S"
  2.1095 +shows "aff_dim S=int(dim S)"
  2.1096 +proof-
  2.1097 +have "subspace(affine hull S)" using subspace_affine[of "affine hull S"] affine_affine_hull assms by auto
  2.1098 +hence "aff_dim (affine hull S) =int(dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto  
  2.1099 +from this show ?thesis using aff_dim_affine_hull[of S] dim_affine_hull[of S] by auto
  2.1100 +qed
  2.1101 +
  2.1102 +lemma aff_dim_univ: "aff_dim (UNIV :: ('n::euclidean_space) set) = int(DIM('n))"
  2.1103 +  using aff_dim_subspace[of "(UNIV :: ('n::euclidean_space) set)"]
  2.1104 +    dim_UNIV[where 'a="'n::euclidean_space"] by auto
  2.1105 +
  2.1106 +lemma aff_dim_geq:
  2.1107 +  fixes V :: "('n::euclidean_space) set"
  2.1108 +  shows "aff_dim V >= -1"
  2.1109 +proof-
  2.1110 +obtain B where B_def: "affine hull B = affine hull V & ~ affine_dependent B & int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto
  2.1111 +from this show ?thesis by auto
  2.1112 +qed
  2.1113 +
  2.1114 +lemma independent_card_le_aff_dim: 
  2.1115 +  assumes "(B::('n::euclidean_space) set) <= V"
  2.1116 +  assumes "~(affine_dependent B)" 
  2.1117 +  shows "int(card B) <= aff_dim V+1"
  2.1118 +proof-
  2.1119 +{ assume "B~={}" 
  2.1120 +  from this obtain T where T_def: "~(affine_dependent T) & B<=T & T<=V & affine hull T = affine hull V" 
  2.1121 +  using assms extend_to_affine_basis[of B V] by auto
  2.1122 +  hence "of_nat(card T) = aff_dim V+1" using aff_dim_unique by auto
  2.1123 +  hence ?thesis using T_def card_mono[of T B] aff_independent_finite[of T] by auto
  2.1124 +}
  2.1125 +moreover
  2.1126 +{ assume "B={}"
  2.1127 +  moreover have "-1<= aff_dim V" using aff_dim_geq by auto
  2.1128 +  ultimately have ?thesis by auto
  2.1129 +}  ultimately show ?thesis by blast
  2.1130 +qed
  2.1131 +
  2.1132 +lemma aff_dim_subset:
  2.1133 +  fixes S T :: "('n::euclidean_space) set"
  2.1134 +  assumes "S <= T"
  2.1135 +  shows "aff_dim S <= aff_dim T"
  2.1136 +proof-
  2.1137 +obtain B where B_def: "~(affine_dependent B) & B<=S & (affine hull B=affine hull S) & of_nat(card B) = aff_dim S+1" using aff_dim_inner_basis_exists[of S] by auto
  2.1138 +moreover hence "int (card B) <= aff_dim T + 1" using assms independent_card_le_aff_dim[of B T] by auto
  2.1139 +ultimately show ?thesis by auto
  2.1140 +qed
  2.1141 +
  2.1142 +lemma aff_dim_subset_univ:
  2.1143 +fixes S :: "('n::euclidean_space) set"
  2.1144 +shows "aff_dim S <= int(DIM('n))"
  2.1145 +proof - 
  2.1146 +  have "aff_dim (UNIV :: ('n::euclidean_space) set) = int(DIM('n))" using aff_dim_univ by auto
  2.1147 +  from this show "aff_dim (S:: ('n::euclidean_space) set) <= int(DIM('n))" using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
  2.1148 +qed
  2.1149 +
  2.1150 +lemma affine_dim_equal:
  2.1151 +assumes "affine (S :: ('n::euclidean_space) set)" "affine T" "S ~= {}" "S <= T" "aff_dim S = aff_dim T"
  2.1152 +shows "S=T"
  2.1153 +proof-
  2.1154 +obtain a where "a : S" using assms by auto 
  2.1155 +hence "a : T" using assms by auto
  2.1156 +def LS == "{y. ? x : S. (-a)+x=y}"
  2.1157 +hence ls: "subspace LS & affine_parallel S LS" using assms parallel_subspace_explicit[of S a LS] `a : S` by auto 
  2.1158 +hence h1: "int(dim LS) = aff_dim S" using assms aff_dim_affine[of S LS] by auto
  2.1159 +have "T ~= {}" using assms by auto
  2.1160 +def LT == "{y. ? x : T. (-a)+x=y}" 
  2.1161 +hence lt: "subspace LT & affine_parallel T LT" using assms parallel_subspace_explicit[of T a LT] `a : T` by auto
  2.1162 +hence "int(dim LT) = aff_dim T" using assms aff_dim_affine[of T LT] `T ~= {}` by auto 
  2.1163 +hence "dim LS = dim LT" using h1 assms by auto
  2.1164 +moreover have "LS <= LT" using LS_def LT_def assms by auto
  2.1165 +ultimately have "LS=LT" using subspace_dim_equal[of LS LT] ls lt by auto
  2.1166 +moreover have "S = {x. ? y : LS. a+y=x}" using LS_def by auto 
  2.1167 +moreover have "T = {x. ? y : LT. a+y=x}" using LT_def by auto
  2.1168 +ultimately show ?thesis by auto 
  2.1169 +qed
  2.1170 +
  2.1171 +lemma affine_hull_univ:
  2.1172 +fixes S :: "('n::euclidean_space) set"
  2.1173 +assumes "aff_dim S = int(DIM('n))"
  2.1174 +shows "affine hull S = (UNIV :: ('n::euclidean_space) set)"
  2.1175 +proof-
  2.1176 +have "S ~= {}" using assms aff_dim_empty[of S] by auto
  2.1177 +have h0: "S <= affine hull S" using hull_subset[of S _] by auto
  2.1178 +have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S" using aff_dim_univ assms by auto
  2.1179 +hence h2: "aff_dim (affine hull S) <= aff_dim (UNIV :: ('n::euclidean_space) set)" using aff_dim_subset_univ[of "affine hull S"] assms h0 by auto  
  2.1180 +have h3: "aff_dim S <= aff_dim (affine hull S)" using h0 aff_dim_subset[of S "affine hull S"] assms by auto
  2.1181 +hence h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)" using h0 h1 h2 by auto
  2.1182 +from this show ?thesis using affine_dim_equal[of "affine hull S" "(UNIV :: ('n::euclidean_space) set)"] affine_affine_hull[of S] affine_UNIV assms h4 h0 `S ~= {}` by auto
  2.1183 +qed
  2.1184 +
  2.1185 +lemma aff_dim_convex_hull:
  2.1186 +fixes S :: "('n::euclidean_space) set"
  2.1187 +shows "aff_dim (convex hull S)=aff_dim S"
  2.1188 +  using aff_dim_affine_hull[of S] convex_hull_subset_affine_hull[of S] 
  2.1189 +  hull_subset[of S "convex"] aff_dim_subset[of S "convex hull S"] 
  2.1190 +  aff_dim_subset[of "convex hull S" "affine hull S"] by auto
  2.1191 +
  2.1192 +lemma aff_dim_cball:
  2.1193 +fixes a :: "'n::euclidean_space" 
  2.1194 +assumes "0<e"
  2.1195 +shows "aff_dim (cball a e) = int (DIM('n))"
  2.1196 +proof-
  2.1197 +have "(%x. a + x) ` (cball 0 e)<=cball a e" unfolding cball_def dist_norm by auto
  2.1198 +hence "aff_dim (cball (0 :: 'n::euclidean_space) e) <= aff_dim (cball a e)"
  2.1199 +  using aff_dim_translation_eq[of a "cball 0 e"] 
  2.1200 +        aff_dim_subset[of "op + a ` cball 0 e" "cball a e"] by auto
  2.1201 +moreover have "aff_dim (cball (0 :: 'n::euclidean_space) e) = int (DIM('n))" 
  2.1202 +   using hull_inc[of "(0 :: 'n::euclidean_space)" "cball 0 e"] centre_in_cball[of "(0 :: 'n::euclidean_space)"] assms 
  2.1203 +   by (simp add: dim_cball[of e] aff_dim_zero[of "cball 0 e"])
  2.1204 +ultimately show ?thesis using aff_dim_subset_univ[of "cball a e"] by auto 
  2.1205 +qed
  2.1206 +
  2.1207 +lemma aff_dim_open:
  2.1208 +fixes S :: "('n::euclidean_space) set"
  2.1209 +assumes "open S" "S ~= {}"
  2.1210 +shows "aff_dim S = int (DIM('n))"
  2.1211 +proof-
  2.1212 +obtain x where "x:S" using assms by auto
  2.1213 +from this obtain e where e_def: "e>0 & cball x e <= S" using open_contains_cball[of S] assms by auto
  2.1214 +from this have "aff_dim (cball x e) <= aff_dim S" using aff_dim_subset by auto
  2.1215 +from this show ?thesis using aff_dim_cball[of e x] aff_dim_subset_univ[of S] e_def by auto     
  2.1216 +qed
  2.1217 +
  2.1218 +lemma low_dim_interior:
  2.1219 +fixes S :: "('n::euclidean_space) set"
  2.1220 +assumes "~(aff_dim S = int (DIM('n)))"
  2.1221 +shows "interior S = {}"
  2.1222 +proof-
  2.1223 +have "aff_dim(interior S) <= aff_dim S" 
  2.1224 +   using interior_subset aff_dim_subset[of "interior S" S] by auto 
  2.1225 +from this show ?thesis using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto   
  2.1226 +qed
  2.1227 +
  2.1228 +subsection{* Relative Interior of a Set *}
  2.1229 +
  2.1230 +definition "rel_interior S = {x. ? T. openin (subtopology euclidean (affine hull S)) T & x : T & T <= S}"
  2.1231 +
  2.1232 +lemma rel_interior: "rel_interior S = {x : S. ? T. open T & x : T & (T Int (affine hull S)) <= S}"
  2.1233 +  unfolding rel_interior_def[of S] openin_open[of "affine hull S"] apply auto
  2.1234 +proof-
  2.1235 +fix x T assume a: "x:S" "open T" "x : T" "(T Int (affine hull S)) <= S"
  2.1236 +hence h1: "x : T Int affine hull S" using hull_inc by auto
  2.1237 +show "EX Tb. (EX Ta. open Ta & Tb = affine hull S Int Ta) & x : Tb & Tb <= S"
  2.1238 +apply (rule_tac x="T Int (affine hull S)" in exI)
  2.1239 +using a h1 by auto
  2.1240 +qed
  2.1241 +
  2.1242 +lemma mem_rel_interior: 
  2.1243 +     "x : rel_interior S <-> (? T. open T & x : (T Int S) & (T Int (affine hull S)) <= S)" 
  2.1244 +     by (auto simp add: rel_interior)
  2.1245 +
  2.1246 +lemma mem_rel_interior_ball: "x : rel_interior S <-> x : S & (? e. 0 < e & ((ball x e) Int (affine hull S)) <= S)"
  2.1247 +  apply (simp add: rel_interior, safe)
  2.1248 +  apply (force simp add: open_contains_ball)
  2.1249 +  apply (rule_tac x="ball x e" in exI)
  2.1250 +  apply (simp add: open_ball centre_in_ball)
  2.1251 +  done
  2.1252 +
  2.1253 +lemma rel_interior_ball: 
  2.1254 +      "rel_interior S = {x : S. ? e. e>0 & ((ball x e) Int (affine hull S)) <= S}" 
  2.1255 +      using mem_rel_interior_ball [of _ S] by auto 
  2.1256 +
  2.1257 +lemma mem_rel_interior_cball: "x : rel_interior S <-> x : S & (? e. 0 < e & ((cball x e) Int (affine hull S)) <= S)"
  2.1258 +  apply (simp add: rel_interior, safe) 
  2.1259 +  apply (force simp add: open_contains_cball)
  2.1260 +  apply (rule_tac x="ball x e" in exI)
  2.1261 +  apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball])
  2.1262 +  apply auto
  2.1263 +  done
  2.1264 +
  2.1265 +lemma rel_interior_cball: "rel_interior S = {x : S. ? e. e>0 & ((cball x e) Int (affine hull S)) <= S}"       using mem_rel_interior_cball [of _ S] by auto
  2.1266 +
  2.1267 +lemma rel_interior_empty: "rel_interior {} = {}" 
  2.1268 +   by (auto simp add: rel_interior_def) 
  2.1269 +
  2.1270 +lemma affine_hull_sing: "affine hull {a :: 'n::euclidean_space} = {a}"
  2.1271 +by (metis affine_hull_eq affine_sing)
  2.1272 +
  2.1273 +lemma rel_interior_sing: "rel_interior {a :: 'n::euclidean_space} = {a}"
  2.1274 +   unfolding rel_interior_ball affine_hull_sing apply auto
  2.1275 +   apply(rule_tac x="1 :: real" in exI) apply simp
  2.1276 +   done
  2.1277 +
  2.1278 +lemma subset_rel_interior:
  2.1279 +fixes S T :: "('n::euclidean_space) set"
  2.1280 +assumes "S<=T" "affine hull S=affine hull T"
  2.1281 +shows "rel_interior S <= rel_interior T"
  2.1282 +  using assms by (auto simp add: rel_interior_def)  
  2.1283 +
  2.1284 +lemma rel_interior_subset: "rel_interior S <= S" 
  2.1285 +   by (auto simp add: rel_interior_def)
  2.1286 +
  2.1287 +lemma rel_interior_subset_closure: "rel_interior S <= closure S" 
  2.1288 +   using rel_interior_subset by (auto simp add: closure_def) 
  2.1289 +
  2.1290 +lemma interior_subset_rel_interior: "interior S <= rel_interior S" 
  2.1291 +   by (auto simp add: rel_interior interior_def)
  2.1292 +
  2.1293 +lemma interior_rel_interior:
  2.1294 +fixes S :: "('n::euclidean_space) set"
  2.1295 +assumes "aff_dim S = int(DIM('n))"
  2.1296 +shows "rel_interior S = interior S"
  2.1297 +proof -
  2.1298 +have "affine hull S = UNIV" using assms affine_hull_univ[of S] by auto 
  2.1299 +from this show ?thesis unfolding rel_interior interior_def by auto
  2.1300 +qed
  2.1301 +
  2.1302 +lemma rel_interior_open:
  2.1303 +fixes S :: "('n::euclidean_space) set"
  2.1304 +assumes "open S"
  2.1305 +shows "rel_interior S = S"
  2.1306 +by (metis assms interior_eq interior_subset_rel_interior rel_interior_subset set_eq_subset)
  2.1307 +
  2.1308 +lemma interior_rel_interior_gen:
  2.1309 +fixes S :: "('n::euclidean_space) set"
  2.1310 +shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})"
  2.1311 +by (metis interior_rel_interior low_dim_interior)
  2.1312 +
  2.1313 +lemma rel_interior_univ: 
  2.1314 +fixes S :: "('n::euclidean_space) set"
  2.1315 +shows "rel_interior (affine hull S) = affine hull S"
  2.1316 +proof-
  2.1317 +have h1: "rel_interior (affine hull S) <= affine hull S" using rel_interior_subset by auto 
  2.1318 +{ fix x assume x_def: "x : affine hull S"
  2.1319 +  obtain e :: real where "e=1" by auto
  2.1320 +  hence "e>0 & ball x e Int affine hull (affine hull S) <= affine hull S" using hull_hull[of _ S] by auto
  2.1321 +  hence "x : rel_interior (affine hull S)" using x_def rel_interior_ball[of "affine hull S"] by auto
  2.1322 +} from this show ?thesis using h1 by auto 
  2.1323 +qed
  2.1324 +
  2.1325 +lemma rel_interior_univ2: "rel_interior (UNIV :: ('n::euclidean_space) set) = UNIV"
  2.1326 +by (metis open_UNIV rel_interior_open)
  2.1327 +
  2.1328 +lemma rel_interior_convex_shrink:
  2.1329 +  fixes S :: "('a::euclidean_space) set"
  2.1330 +  assumes "convex S" "c : rel_interior S" "x : S" "0 < e" "e <= 1"
  2.1331 +  shows "x - e *\<^sub>R (x - c) : rel_interior S"
  2.1332 +proof- 
  2.1333 +(* Proof is a modified copy of the proof of similar lemma mem_interior_convex_shrink 
  2.1334 +*)
  2.1335 +obtain d where "d>0" and d:"ball c d Int affine hull S <= S" 
  2.1336 +  using assms(2) unfolding  mem_rel_interior_ball by auto
  2.1337 +{   fix y assume as:"dist (x - e *\<^sub>R (x - c)) y < e * d & y : affine hull S"
  2.1338 +    have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
  2.1339 +    have "x : affine hull S" using assms hull_subset[of S] by auto
  2.1340 +    moreover have "1 / e + - ((1 - e) / e) = 1" 
  2.1341 +       using `e>0` mult_left.diff[of "1" "(1-e)" "1/e"] by auto
  2.1342 +    ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S"
  2.1343 +        using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"] by (simp add: algebra_simps)     
  2.1344 +    have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
  2.1345 +      unfolding dist_norm unfolding norm_scaleR[THEN sym] apply(rule arg_cong[where f=norm]) using `e>0`
  2.1346 +      by(auto simp add:euclidean_eq[where 'a='a] field_simps) 
  2.1347 +    also have "... = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
  2.1348 +    also have "... < d" using as[unfolded dist_norm] and `e>0`
  2.1349 +      by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
  2.1350 +    finally have "y : S" apply(subst *) 
  2.1351 +apply(rule assms(1)[unfolded convex_alt,rule_format])
  2.1352 +      apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) ** by auto
  2.1353 +} hence "ball (x - e *\<^sub>R (x - c)) (e*d) Int affine hull S <= S" by auto
  2.1354 +moreover have "0 < e*d" using `0<e` `0<d` using real_mult_order by auto
  2.1355 +moreover have "c : S" using assms rel_interior_subset by auto
  2.1356 +moreover hence "x - e *\<^sub>R (x - c) : S"
  2.1357 +   using mem_convex[of S x c e] apply (simp add: algebra_simps) using assms by auto
  2.1358 +ultimately show ?thesis 
  2.1359 +  using mem_rel_interior_ball[of "x - e *\<^sub>R (x - c)" S] `e>0` by auto
  2.1360 +qed
  2.1361 +
  2.1362 +lemma interior_real_semiline:
  2.1363 +fixes a :: real
  2.1364 +shows "interior {a..} = {a<..}"
  2.1365 +proof-
  2.1366 +{ fix y assume "a<y" hence "y : interior {a..}"
  2.1367 +  apply (simp add: mem_interior) apply (rule_tac x="(y-a)" in exI) apply (auto simp add: dist_norm) 
  2.1368 +  done }
  2.1369 +moreover
  2.1370 +{ fix y assume "y : interior {a..}" (*hence "a<=y" using interior_subset by auto*)
  2.1371 +  from this obtain e where e_def: "e>0 & cball y e \<subseteq> {a..}" 
  2.1372 +     using mem_interior_cball[of y "{a..}"] by auto
  2.1373 +  moreover hence "y-e : cball y e" by (auto simp add: cball_def dist_norm) 
  2.1374 +  ultimately have "a<=y-e" by auto
  2.1375 +  hence "a<y" using e_def by auto
  2.1376 +} ultimately show ?thesis by auto
  2.1377 +qed
  2.1378 +
  2.1379 +lemma rel_interior_real_interval:
  2.1380 +  fixes a b :: real assumes "a < b" shows "rel_interior {a..b} = {a<..<b}"
  2.1381 +proof-
  2.1382 +  have "{a<..<b} \<noteq> {}" using assms unfolding set_eq_iff by (auto intro!: exI[of _ "(a + b) / 2"])
  2.1383 +  then show ?thesis
  2.1384 +    using interior_rel_interior_gen[of "{a..b}", symmetric]
  2.1385 +    by (simp split: split_if_asm add: interior_closed_interval)
  2.1386 +qed
  2.1387 +
  2.1388 +lemma rel_interior_real_semiline:
  2.1389 +  fixes a :: real shows "rel_interior {a..} = {a<..}"
  2.1390 +proof-
  2.1391 +  have *: "{a<..} \<noteq> {}" unfolding set_eq_iff by (auto intro!: exI[of _ "a + 1"])
  2.1392 +  then show ?thesis using interior_real_semiline
  2.1393 +     interior_rel_interior_gen[of "{a..}"]
  2.1394 +     by (auto split: split_if_asm)
  2.1395 +qed
  2.1396 +
  2.1397 +subsection "Relative open"
  2.1398 +
  2.1399 +definition "rel_open S <-> (rel_interior S) = S"
  2.1400 +
  2.1401 +lemma rel_open: "rel_open S <-> openin (subtopology euclidean (affine hull S)) S"
  2.1402 + unfolding rel_open_def rel_interior_def apply auto
  2.1403 + using openin_subopen[of "subtopology euclidean (affine hull S)" S] by auto
  2.1404 +
  2.1405 +lemma opein_rel_interior: 
  2.1406 +  "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
  2.1407 +  apply (simp add: rel_interior_def)
  2.1408 +  apply (subst openin_subopen) by blast
  2.1409 +
  2.1410 +lemma affine_rel_open: 
  2.1411 +  fixes S :: "('n::euclidean_space) set"
  2.1412 +  assumes "affine S" shows "rel_open S" 
  2.1413 +  unfolding rel_open_def using assms rel_interior_univ[of S] affine_hull_eq[of S] by metis
  2.1414 +
  2.1415 +lemma affine_closed: 
  2.1416 +  fixes S :: "('n::euclidean_space) set"
  2.1417 +  assumes "affine S" shows "closed S"
  2.1418 +proof-
  2.1419 +{ assume "S ~= {}"
  2.1420 +  from this obtain L where L_def: "subspace L & affine_parallel S L"
  2.1421 +     using assms affine_parallel_subspace[of S] by auto
  2.1422 +  from this obtain "a" where a_def: "S=(op + a ` L)" 
  2.1423 +     using affine_parallel_def[of L S] affine_parallel_commut by auto 
  2.1424 +  have "closed L" using L_def closed_subspace by auto
  2.1425 +  hence "closed S" using closed_translation a_def by auto
  2.1426 +} from this show ?thesis by auto
  2.1427 +qed
  2.1428 +
  2.1429 +lemma closure_affine_hull:
  2.1430 +  fixes S :: "('n::euclidean_space) set"
  2.1431 +  shows "closure S <= affine hull S"
  2.1432 +proof-
  2.1433 +have "closure S <= closure (affine hull S)" using subset_closure by auto
  2.1434 +moreover have "closure (affine hull S) = affine hull S" 
  2.1435 +   using affine_affine_hull affine_closed[of "affine hull S"] closure_eq by auto
  2.1436 +ultimately show ?thesis by auto  
  2.1437 +qed
  2.1438 +
  2.1439 +lemma closure_same_affine_hull:
  2.1440 +  fixes S :: "('n::euclidean_space) set"
  2.1441 +  shows "affine hull (closure S) = affine hull S"
  2.1442 +proof-
  2.1443 +have "affine hull (closure S) <= affine hull S"
  2.1444 +   using hull_mono[of "closure S" "affine hull S" "affine"] closure_affine_hull[of S] hull_hull[of "affine" S] by auto
  2.1445 +moreover have "affine hull (closure S) >= affine hull S"  
  2.1446 +   using hull_mono[of "S" "closure S" "affine"] closure_subset by auto
  2.1447 +ultimately show ?thesis by auto  
  2.1448 +qed
  2.1449 +
  2.1450 +lemma closure_aff_dim: 
  2.1451 +  fixes S :: "('n::euclidean_space) set"
  2.1452 +  shows "aff_dim (closure S) = aff_dim S"
  2.1453 +proof-
  2.1454 +have "aff_dim S <= aff_dim (closure S)" using aff_dim_subset closure_subset by auto
  2.1455 +moreover have "aff_dim (closure S) <= aff_dim (affine hull S)" 
  2.1456 +  using aff_dim_subset closure_affine_hull by auto
  2.1457 +moreover have "aff_dim (affine hull S) = aff_dim S" using aff_dim_affine_hull by auto
  2.1458 +ultimately show ?thesis by auto
  2.1459 +qed
  2.1460 +
  2.1461 +lemma rel_interior_closure_convex_shrink:
  2.1462 +  fixes S :: "(_::euclidean_space) set"
  2.1463 +  assumes "convex S" "c : rel_interior S" "x : closure S" "0 < e" "e <= 1"
  2.1464 +  shows "x - e *\<^sub>R (x - c) : rel_interior S"
  2.1465 +proof- 
  2.1466 +(* Proof is a modified copy of the proof of similar lemma mem_interior_closure_convex_shrink
  2.1467 +*)
  2.1468 +obtain d where "d>0" and d:"ball c d Int affine hull S <= S" 
  2.1469 +  using assms(2) unfolding mem_rel_interior_ball by auto
  2.1470 +have "EX y : S. norm (y - x) * (1 - e) < e * d" proof(cases "x : S")
  2.1471 +    case True thus ?thesis using `e>0` `d>0` by(rule_tac bexI[where x=x], auto intro!: mult_pos_pos) next
  2.1472 +    case False hence x:"x islimpt S" using assms(3)[unfolded closure_def] by auto
  2.1473 +    show ?thesis proof(cases "e=1")
  2.1474 +      case True obtain y where "y : S" "y ~= x" "dist y x < 1"
  2.1475 +        using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto
  2.1476 +      thus ?thesis apply(rule_tac x=y in bexI) unfolding True using `d>0` by auto next
  2.1477 +      case False hence "0 < e * d / (1 - e)" and *:"1 - e > 0"
  2.1478 +        using `e<=1` `e>0` `d>0` by(auto intro!:mult_pos_pos divide_pos_pos)
  2.1479 +      then obtain y where "y : S" "y ~= x" "dist y x < e * d / (1 - e)"
  2.1480 +        using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
  2.1481 +      thus ?thesis apply(rule_tac x=y in bexI) unfolding dist_norm using pos_less_divide_eq[OF *] by auto qed qed
  2.1482 +  then obtain y where "y : S" and y:"norm (y - x) * (1 - e) < e * d" by auto
  2.1483 +  def z == "c + ((1 - e) / e) *\<^sub>R (x - y)"
  2.1484 +  have *:"x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using `e>0` by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
  2.1485 +  have zball: "z\<in>ball c d"
  2.1486 +    using mem_ball z_def dist_norm[of c] using y and assms(4,5) by (auto simp add:field_simps norm_minus_commute)
  2.1487 +  have "x : affine hull S" using closure_affine_hull assms by auto
  2.1488 +  moreover have "y : affine hull S" using `y : S` hull_subset[of S] by auto
  2.1489 +  moreover have "c : affine hull S" using assms rel_interior_subset hull_subset[of S] by auto
  2.1490 +  ultimately have "z : affine hull S" 
  2.1491 +    using z_def affine_affine_hull[of S] 
  2.1492 +          mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"] 
  2.1493 +          assms by (auto simp add: field_simps)
  2.1494 +  hence "z : S" using d zball by auto
  2.1495 +  obtain d1 where "d1>0" and d1:"ball z d1 <= ball c d"
  2.1496 +    using zball open_ball[of c d] openE[of "ball c d" z] by auto
  2.1497 +  hence "(ball z d1) Int (affine hull S) <= (ball c d) Int (affine hull S)" by auto
  2.1498 +  hence "(ball z d1) Int (affine hull S) <= S" using d by auto 
  2.1499 +  hence "z : rel_interior S" using mem_rel_interior_ball using `d1>0` `z : S` by auto
  2.1500 +  hence "y - e *\<^sub>R (y - z) : rel_interior S" using rel_interior_convex_shrink[of S z y e] assms`y : S` by auto
  2.1501 +  thus ?thesis using * by auto 
  2.1502 +qed
  2.1503 +
  2.1504 +subsection{* Relative interior preserves under linear transformations *}
  2.1505 +
  2.1506 +lemma rel_interior_translation_aux:
  2.1507 +fixes a :: "'n::euclidean_space"
  2.1508 +shows "((%x. a + x) ` rel_interior S) <= rel_interior ((%x. a + x) ` S)"
  2.1509 +proof-
  2.1510 +{ fix x assume x_def: "x : rel_interior S"
  2.1511 +  from this obtain T where T_def: "open T & x : (T Int S) & (T Int (affine hull S)) <= S" using mem_rel_interior[of x S] by auto 
  2.1512 +  from this have "open ((%x. a + x) ` T)" and 
  2.1513 +    "(a + x) : (((%x. a + x) ` T) Int ((%x. a + x) ` S))" and 
  2.1514 +    "(((%x. a + x) ` T) Int (affine hull ((%x. a + x) ` S))) <= ((%x. a + x) ` S)" 
  2.1515 +    using affine_hull_translation[of a S] open_translation[of T a] x_def by auto 
  2.1516 +  from this have "(a+x) : rel_interior ((%x. a + x) ` S)" 
  2.1517 +    using mem_rel_interior[of "a+x" "((%x. a + x) ` S)"] by auto 
  2.1518 +} from this show ?thesis by auto 
  2.1519 +qed
  2.1520 +
  2.1521 +lemma rel_interior_translation:
  2.1522 +fixes a :: "'n::euclidean_space"
  2.1523 +shows "rel_interior ((%x. a + x) ` S) = ((%x. a + x) ` rel_interior S)"
  2.1524 +proof-
  2.1525 +have "(%x. (-a) + x) ` rel_interior ((%x. a + x) ` S) <= rel_interior S" 
  2.1526 +   using rel_interior_translation_aux[of "-a" "(%x. a + x) ` S"] 
  2.1527 +         translation_assoc[of "-a" "a"] by auto
  2.1528 +hence "((%x. a + x) ` rel_interior S) >= rel_interior ((%x. a + x) ` S)" 
  2.1529 +   using translation_inverse_subset[of a "rel_interior (op + a ` S)" "rel_interior S"] 
  2.1530 +   by auto
  2.1531 +from this show ?thesis using  rel_interior_translation_aux[of a S] by auto 
  2.1532 +qed
  2.1533 +
  2.1534 +
  2.1535 +lemma affine_hull_linear_image:
  2.1536 +assumes "bounded_linear f"
  2.1537 +shows "f ` (affine hull s) = affine hull f ` s"
  2.1538 +(* Proof is a modified copy of the proof of similar lemma convex_hull_linear_image
  2.1539 +*)
  2.1540 +  apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3  
  2.1541 +  apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
  2.1542 +  apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
  2.1543 +proof-
  2.1544 +  interpret f: bounded_linear f by fact
  2.1545 +  show "affine {x. f x : affine hull f ` s}" 
  2.1546 +  unfolding affine_def by(auto simp add: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format]) next
  2.1547 +  interpret f: bounded_linear f by fact
  2.1548 +  show "affine {x. x : f ` (affine hull s)}" using affine_affine_hull[unfolded affine_def, of s] 
  2.1549 +    unfolding affine_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
  2.1550 +qed auto
  2.1551 +
  2.1552 +
  2.1553 +lemma rel_interior_injective_on_span_linear_image:
  2.1554 +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
  2.1555 +fixes S :: "('m::euclidean_space) set"
  2.1556 +assumes "bounded_linear f" and "inj_on f (span S)"
  2.1557 +shows "rel_interior (f ` S) = f ` (rel_interior S)"
  2.1558 +proof-
  2.1559 +{ fix z assume z_def: "z : rel_interior (f ` S)"
  2.1560 +  have "z : f ` S" using z_def rel_interior_subset[of "f ` S"] by auto
  2.1561 +  from this obtain x where x_def: "x : S & (f x = z)" by auto
  2.1562 +  obtain e2 where e2_def: "e2>0 & cball z e2 Int affine hull (f ` S) <= (f ` S)" 
  2.1563 +    using z_def rel_interior_cball[of "f ` S"] by auto
  2.1564 +  obtain K where K_def: "K>0 & (! x. norm (f x) <= norm x * K)" 
  2.1565 +   using assms RealVector.bounded_linear.pos_bounded[of f] by auto
  2.1566 +  def e1 == "1/K" hence e1_def: "e1>0 & (! x. e1 * norm (f x) <= norm x)" 
  2.1567 +   using K_def pos_le_divide_eq[of e1] by auto
  2.1568 +  def e == "e1 * e2" hence "e>0" using e1_def e2_def real_mult_order by auto 
  2.1569 +  { fix y assume y_def: "y : cball x e Int affine hull S"
  2.1570 +    from this have h1: "f y : affine hull (f ` S)" 
  2.1571 +      using affine_hull_linear_image[of f S] assms by auto 
  2.1572 +    from y_def have "norm (x-y)<=e1 * e2" 
  2.1573 +      using cball_def[of x e] dist_norm[of x y] e_def by auto
  2.1574 +    moreover have "(f x)-(f y)=f (x-y)"
  2.1575 +       using assms linear_sub[of f x y] linear_conv_bounded_linear[of f] by auto
  2.1576 +    moreover have "e1 * norm (f (x-y)) <= norm (x-y)" using e1_def by auto
  2.1577 +    ultimately have "e1 * norm ((f x)-(f y)) <= e1 * e2" by auto
  2.1578 +    hence "(f y) : (cball z e2)" 
  2.1579 +      using cball_def[of "f x" e2] dist_norm[of "f x" "f y"] e1_def x_def by auto
  2.1580 +    hence "f y : (f ` S)" using y_def e2_def h1 by auto
  2.1581 +    hence "y : S" using assms y_def hull_subset[of S] affine_hull_subset_span 
  2.1582 +         inj_on_image_mem_iff[of f "span S" S y] by auto
  2.1583 +  } 
  2.1584 +  hence "z : f ` (rel_interior S)" using mem_rel_interior_cball[of x S] `e>0` x_def by auto
  2.1585 +} 
  2.1586 +moreover
  2.1587 +{ fix x assume x_def: "x : rel_interior S"
  2.1588 +  from this obtain e2 where e2_def: "e2>0 & cball x e2 Int affine hull S <= S" 
  2.1589 +    using rel_interior_cball[of S] by auto
  2.1590 +  have "x : S" using x_def rel_interior_subset by auto
  2.1591 +  hence *: "f x : f ` S" by auto
  2.1592 +  have "! x:span S. f x = 0 --> x = 0" 
  2.1593 +    using assms subspace_span linear_conv_bounded_linear[of f] 
  2.1594 +          linear_injective_on_subspace_0[of f "span S"] by auto
  2.1595 +  from this obtain e1 where e1_def: "e1>0 & (! x : span S. e1 * norm x <= norm (f x))" 
  2.1596 +   using assms injective_imp_isometric[of "span S" f] 
  2.1597 +         subspace_span[of S] closed_subspace[of "span S"] by auto
  2.1598 +  def e == "e1 * e2" hence "e>0" using e1_def e2_def real_mult_order by auto 
  2.1599 +  { fix y assume y_def: "y : cball (f x) e Int affine hull (f ` S)"
  2.1600 +    from this have "y : f ` (affine hull S)" using affine_hull_linear_image[of f S] assms by auto 
  2.1601 +    from this obtain xy where xy_def: "xy : affine hull S & (f xy = y)" by auto
  2.1602 +    from this y_def have "norm ((f x)-(f xy))<=e1 * e2" 
  2.1603 +      using cball_def[of "f x" e] dist_norm[of "f x" y] e_def by auto
  2.1604 +    moreover have "(f x)-(f xy)=f (x-xy)"
  2.1605 +       using assms linear_sub[of f x xy] linear_conv_bounded_linear[of f] by auto
  2.1606 +    moreover have "x-xy : span S" 
  2.1607 +       using subspace_sub[of "span S" x xy] subspace_span `x : S` xy_def 
  2.1608 +             affine_hull_subset_span[of S] span_inc by auto
  2.1609 +    moreover hence "e1 * norm (x-xy) <= norm (f (x-xy))" using e1_def by auto
  2.1610 +    ultimately have "e1 * norm (x-xy) <= e1 * e2" by auto
  2.1611 +    hence "xy : (cball x e2)"  using cball_def[of x e2] dist_norm[of x xy] e1_def by auto
  2.1612 +    hence "y : (f ` S)" using xy_def e2_def by auto
  2.1613 +  } 
  2.1614 +  hence "(f x) : rel_interior (f ` S)" 
  2.1615 +     using mem_rel_interior_cball[of "(f x)" "(f ` S)"] * `e>0` by auto
  2.1616 +} 
  2.1617 +ultimately show ?thesis by auto
  2.1618 +qed
  2.1619 +
  2.1620 +lemma rel_interior_injective_linear_image:
  2.1621 +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
  2.1622 +assumes "bounded_linear f" and "inj f"
  2.1623 +shows "rel_interior (f ` S) = f ` (rel_interior S)"
  2.1624 +using assms rel_interior_injective_on_span_linear_image[of f S] 
  2.1625 +      subset_inj_on[of f "UNIV" "span S"] by auto
  2.1626 +
  2.1627 +subsection{* Some Properties of subset of standard basis *}
  2.1628 +
  2.1629 +lemma affine_hull_substd_basis: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
  2.1630 +  shows "affine hull (insert 0 {basis i | i. i : d}) =
  2.1631 +  {x::'a::euclidean_space. (!i<DIM('a). i ~: d --> x$$i = 0)}"
  2.1632 + (is "affine hull (insert 0 ?A) = ?B")
  2.1633 +proof- have *:"\<And>A. op + (0\<Colon>'a) ` A = A" "\<And>A. op + (- (0\<Colon>'a)) ` A = A" by auto
  2.1634 +  show ?thesis unfolding affine_hull_insert_span_gen span_substd_basis[OF assms,THEN sym] * ..
  2.1635 +qed
  2.1636 +
  2.1637 +lemma affine_hull_convex_hull: "affine hull (convex hull S) = affine hull S"
  2.1638 +by (metis Int_absorb1 Int_absorb2 convex_hull_subset_affine_hull hull_hull hull_mono hull_subset)
  2.1639 +
  2.1640  subsection {* Openness and compactness are preserved by convex hull operation. *}
  2.1641  
  2.1642  lemma open_convex_hull[intro]:
  2.1643 @@ -1525,6 +3105,61 @@
  2.1644    "convex hull ((\<lambda>x. a + c *\<^sub>R x) ` s) = (\<lambda>x. a + c *\<^sub>R x) ` (convex hull s)"
  2.1645  by(simp only: image_image[THEN sym] convex_hull_scaling convex_hull_translation)
  2.1646  
  2.1647 +subsection {* Convexity of cone hulls *}
  2.1648 +
  2.1649 +lemma convex_cone_hull:
  2.1650 +fixes S :: "('m::euclidean_space) set"
  2.1651 +assumes "convex S"
  2.1652 +shows "convex (cone hull S)"
  2.1653 +proof-
  2.1654 +{ fix x y assume xy_def: "x : cone hull S & y : cone hull S"
  2.1655 +  hence "S ~= {}" using cone_hull_empty_iff[of S] by auto
  2.1656 +  fix u v assume uv_def: "u>=0 & v>=0 & (u :: real)+v=1"
  2.1657 +  hence *: "u *\<^sub>R x : cone hull S & v *\<^sub>R y : cone hull S"
  2.1658 +     using cone_cone_hull[of S] xy_def cone_def[of "cone hull S"] by auto
  2.1659 +  from * obtain cx xx where x_def: "u *\<^sub>R x = cx *\<^sub>R xx & (cx :: real)>=0 & xx : S"
  2.1660 +     using cone_hull_expl[of S] by auto
  2.1661 +  from * obtain cy yy where y_def: "v *\<^sub>R y = cy *\<^sub>R yy & (cy :: real)>=0 & yy : S"
  2.1662 +     using cone_hull_expl[of S] by auto
  2.1663 +  { assume "cx+cy<=0" hence "u *\<^sub>R x=0 & v *\<^sub>R y=0" using x_def y_def by auto
  2.1664 +    hence "u *\<^sub>R x+ v *\<^sub>R y = 0" by auto
  2.1665 +    hence "u *\<^sub>R x+ v *\<^sub>R y : cone hull S" using cone_hull_contains_0[of S] `S ~= {}` by auto
  2.1666 +  }
  2.1667 +  moreover
  2.1668 +  { assume "cx+cy>0"
  2.1669 +    hence "(cx/(cx+cy)) *\<^sub>R xx + (cy/(cx+cy)) *\<^sub>R yy : S"
  2.1670 +      using assms mem_convex_alt[of S xx yy cx cy] x_def y_def by auto
  2.1671 +    hence "cx *\<^sub>R xx + cy *\<^sub>R yy : cone hull S"
  2.1672 +      using mem_cone_hull[of "(cx/(cx+cy)) *\<^sub>R xx + (cy/(cx+cy)) *\<^sub>R yy" S "cx+cy"]
  2.1673 +      `cx+cy>0` by (auto simp add: scaleR_right_distrib)
  2.1674 +    hence "u *\<^sub>R x+ v *\<^sub>R y : cone hull S" using x_def y_def by auto
  2.1675 +  }
  2.1676 +  moreover have "(cx+cy<=0) | (cx+cy>0)" by auto
  2.1677 +  ultimately have "u *\<^sub>R x+ v *\<^sub>R y : cone hull S" by blast
  2.1678 +} from this show ?thesis unfolding convex_def by auto
  2.1679 +qed
  2.1680 +
  2.1681 +lemma cone_convex_hull:
  2.1682 +fixes S :: "('m::euclidean_space) set"
  2.1683 +assumes "cone S"
  2.1684 +shows "cone (convex hull S)"
  2.1685 +proof-
  2.1686 +{ assume "S = {}" hence ?thesis by auto }
  2.1687 +moreover
  2.1688 +{ assume "S ~= {}" hence *: "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto
  2.1689 +  { fix c assume "(c :: real)>0"
  2.1690 +    hence "op *\<^sub>R c ` (convex hull S) = convex hull (op *\<^sub>R c ` S)"
  2.1691 +       using convex_hull_scaling[of _ S] by auto
  2.1692 +    also have "...=convex hull S" using * `c>0` by auto
  2.1693 +    finally have "op *\<^sub>R c ` (convex hull S) = convex hull S" by auto
  2.1694 +  }
  2.1695 +  hence "0 : convex hull S & (!c. c>0 --> (op *\<^sub>R c ` (convex hull S)) = (convex hull S))"
  2.1696 +     using * hull_subset[of S convex] by auto
  2.1697 +  hence ?thesis using `S ~= {}` cone_iff[of "convex hull S"] by auto
  2.1698 +}
  2.1699 +ultimately show ?thesis by blast
  2.1700 +qed
  2.1701 +
  2.1702  subsection {* Convex set as intersection of halfspaces. *}
  2.1703  
  2.1704  lemma convex_halfspace_intersection:
  2.1705 @@ -1653,28 +3288,6 @@
  2.1706    shows "\<Inter> f \<noteq>{}"
  2.1707    apply(rule helly_induct) using assms by auto
  2.1708  
  2.1709 -subsection {* Convex hull is "preserved" by a linear function. *}
  2.1710 -
  2.1711 -lemma convex_hull_linear_image:
  2.1712 -  assumes "bounded_linear f"
  2.1713 -  shows "f ` (convex hull s) = convex hull (f ` s)"
  2.1714 -  apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3  
  2.1715 -  apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
  2.1716 -  apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
  2.1717 -proof-
  2.1718 -  interpret f: bounded_linear f by fact
  2.1719 -  show "convex {x. f x \<in> convex hull f ` s}" 
  2.1720 -  unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next
  2.1721 -  interpret f: bounded_linear f by fact
  2.1722 -  show "convex {x. x \<in> f ` (convex hull s)}" using  convex_convex_hull[unfolded convex_def, of s] 
  2.1723 -    unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
  2.1724 -qed auto
  2.1725 -
  2.1726 -lemma in_convex_hull_linear_image:
  2.1727 -  assumes "bounded_linear f" "x \<in> convex hull s"
  2.1728 -  shows "(f x) \<in> convex hull (f ` s)"
  2.1729 -using convex_hull_linear_image[OF assms(1)] assms(2) by auto
  2.1730 -
  2.1731  subsection {* Homeomorphism of all convex compact sets with nonempty interior. *}
  2.1732  
  2.1733  lemma compact_frontier_line_lemma:
  2.1734 @@ -2459,43 +4072,49 @@
  2.1735    apply(rule_tac x=u in exI) defer apply(rule_tac x="\<lambda>x. if x = 0 then 1 - setsum u s else u x" in exI) using assms(2)
  2.1736    unfolding if_smult and setsum_delta_notmem[OF assms(2)] by auto
  2.1737  
  2.1738 +lemma substd_simplex: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
  2.1739 +  shows "convex hull (insert 0 { basis i | i. i : d}) =
  2.1740 +        {x::'a::euclidean_space . (!i<DIM('a). 0 <= x$$i) & setsum (%i. x$$i) d <= 1 &
  2.1741 +  (!i<DIM('a). i ~: d --> x$$i = 0)}" 
  2.1742 +  (is "convex hull (insert 0 ?p) = ?s")
  2.1743 +(* Proof is a modified copy of the proof of similar lemma std_simplex in Convex_Euclidean_Space.thy *)
  2.1744 +proof- let ?D = d (*"{..<DIM('a::euclidean_space)}"*)
  2.1745 +  have "0 ~: ?p" using assms by (auto simp: image_def)
  2.1746 +  have "{(basis i)::'n::euclidean_space |i. i \<in> ?D} = basis ` ?D" by auto
  2.1747 +  note sumbas = this setsum_reindex[OF basis_inj_on[of d], unfolded o_def, OF assms]
  2.1748 +  show ?thesis unfolding simplex[OF finite_substdbasis `0 ~: ?p`] 
  2.1749 +    apply(rule set_eqI) unfolding mem_Collect_eq apply rule
  2.1750 +    apply(erule exE, (erule conjE)+) apply(erule_tac[2] conjE)+ proof-
  2.1751 +    fix x::"'a::euclidean_space" and u assume as: "\<forall>x\<in>{basis i |i. i \<in>?D}. 0 \<le> u x"
  2.1752 +      "setsum u {basis i |i. i \<in> ?D} \<le> 1" "(\<Sum>x\<in>{basis i |i. i \<in>?D}. u x *\<^sub>R x) = x"
  2.1753 +    have *:"\<forall>i<DIM('a). i:d --> u (basis i) = x$$i" and "(!i<DIM('a). i ~: d --> x $$ i = 0)" using as(3) 
  2.1754 +      unfolding sumbas unfolding substdbasis_expansion_unique[OF assms] by auto
  2.1755 +    hence **:"setsum u {basis i |i. i \<in> ?D} = setsum (op $$ x) ?D" unfolding sumbas 
  2.1756 +      apply-apply(rule setsum_cong2) using assms by auto
  2.1757 +    have " (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (op $$ x) ?D \<le> 1" 
  2.1758 +      apply - proof(rule,rule,rule)
  2.1759 +      fix i assume i:"i<DIM('a)" have "i : d ==> 0 \<le> x$$i" unfolding *[rule_format,OF i,THEN sym] 
  2.1760 +         apply(rule_tac as(1)[rule_format]) by auto
  2.1761 +      moreover have "i ~: d ==> 0 \<le> x$$i" 
  2.1762 +        using `(!i<DIM('a). i ~: d --> x $$ i = 0)`[rule_format, OF i] by auto
  2.1763 +      ultimately show "0 \<le> x$$i" by auto
  2.1764 +    qed(insert as(2)[unfolded **], auto)
  2.1765 +    from this show " (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (op $$ x) ?D \<le> 1 & (!i<DIM('a). i ~: d --> x $$ i = 0)" 
  2.1766 +      using `(!i<DIM('a). i ~: d --> x $$ i = 0)` by auto
  2.1767 +  next fix x::"'a::euclidean_space" assume as:"\<forall>i<DIM('a). 0 \<le> x $$ i" "setsum (op $$ x) ?D \<le> 1"
  2.1768 +      "(!i<DIM('a). i ~: d --> x $$ i = 0)"
  2.1769 +    show "\<exists>u. (\<forall>x\<in>{basis i |i. i \<in> ?D}. 0 \<le> u x) \<and>
  2.1770 +      setsum u {basis i |i. i \<in> ?D} \<le> 1 \<and> (\<Sum>x\<in>{basis i |i. i \<in> ?D}. u x *\<^sub>R x) = x"
  2.1771 +      apply(rule_tac x="\<lambda>y. inner y x" in exI) apply(rule,rule) unfolding mem_Collect_eq apply(erule exE)
  2.1772 +      using as(1) apply(erule_tac x=i in allE) unfolding sumbas apply safe unfolding not_less basis_zero
  2.1773 +      unfolding substdbasis_expansion_unique[OF assms] euclidean_component_def[THEN sym]
  2.1774 +      using as(2,3) by(auto simp add:dot_basis not_less  basis_zero) 
  2.1775 +  qed qed
  2.1776 +
  2.1777  lemma std_simplex:
  2.1778    "convex hull (insert 0 { basis i | i. i<DIM('a)}) =
  2.1779          {x::'a::euclidean_space . (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (\<lambda>i. x$$i) {..<DIM('a)} \<le> 1 }"
  2.1780 -  (is "convex hull (insert 0 ?p) = ?s")
  2.1781 -proof- let ?D = "{..<DIM('a)}"
  2.1782 -  have *:"finite ?p" "0\<notin>?p" by auto
  2.1783 -  have "{(basis i)::'a |i. i<DIM('a)} = basis ` ?D" by auto
  2.1784 -  note sumbas = this  setsum_reindex[OF basis_inj, unfolded o_def]
  2.1785 -  show ?thesis unfolding simplex[OF *] apply(rule set_eqI) unfolding mem_Collect_eq apply rule
  2.1786 -    apply(erule exE, (erule conjE)+) apply(erule_tac[2] conjE)+ proof-
  2.1787 -    fix x::"'a" and u assume as: "\<forall>x\<in>{basis i |i. i<DIM('a)}. 0 \<le> u x"
  2.1788 -      "setsum u {basis i |i. i<DIM('a)} \<le> 1" "(\<Sum>x\<in>{basis i |i. i<DIM('a)}. u x *\<^sub>R x) = x"
  2.1789 -    have *:"\<forall>i<DIM('a). u (basis i) = x$$i" 
  2.1790 -    proof safe case goal1
  2.1791 -      have "x$$i = (\<Sum>j<DIM('a). (if j = i then u (basis j) else 0))"
  2.1792 -        unfolding as(3)[THEN sym] euclidean_component.setsum unfolding  sumbas
  2.1793 -        apply(rule setsum_cong2) by(auto simp add: basis_component)
  2.1794 -      also have "... = u (basis i)" apply(subst setsum_delta) using goal1 by auto
  2.1795 -      finally show ?case by auto
  2.1796 -    qed
  2.1797 -    hence **:"setsum u {basis i |i. i<DIM('a)} = setsum (op $$ x) ?D" unfolding sumbas 
  2.1798 -      apply-apply(rule setsum_cong2) by auto
  2.1799 -    show "(\<forall>i<DIM('a). 0 \<le> x $$ i) \<and> setsum (op $$ x) ?D \<le> 1" apply - proof(rule,rule,rule)
  2.1800 -      fix i assume i:"i<DIM('a)" show "0 \<le> x$$i"  unfolding *[rule_format,OF i,THEN sym]
  2.1801 -        apply(rule_tac as(1)[rule_format]) using i by auto
  2.1802 -    qed(insert as(2)[unfolded **], auto)
  2.1803 -  next fix x::"'a" assume as:"\<forall>i<DIM('a). 0 \<le> x $$ i" "setsum (op $$ x) ?D \<le> 1"
  2.1804 -    show "\<exists>u. (\<forall>x\<in>{basis i |i. i<DIM('a)}. 0 \<le> u x) \<and>
  2.1805 -      setsum u {basis i |i. i<DIM('a)} \<le> 1 \<and> (\<Sum>x\<in>{basis i |i. i<DIM('a)}. u x *\<^sub>R x) = x"
  2.1806 -      apply(rule_tac x="\<lambda>y. inner y x" in exI) apply safe using as(1)
  2.1807 -      proof- show "(\<Sum>y\<in>{basis i |i. i < DIM('a)}. y \<bullet> x) \<le> 1" unfolding sumbas
  2.1808 -          using as(2) unfolding euclidean_component_def[THEN sym] .
  2.1809 -        show "(\<Sum>xa\<in>{basis i |i. i < DIM('a)}. (xa \<bullet> x) *\<^sub>R xa) = x" unfolding sumbas
  2.1810 -          apply(subst (7) euclidean_representation) apply(rule setsum_cong2)
  2.1811 -          unfolding euclidean_component_def by auto
  2.1812 -      qed (auto simp add:euclidean_component_def)
  2.1813 -    qed qed
  2.1814 +  using substd_simplex[of "{..<DIM('a)}"] by auto
  2.1815  
  2.1816  lemma interior_std_simplex:
  2.1817    "interior (convex hull (insert 0 { basis i| i. i<DIM('a)})) =
  2.1818 @@ -2552,4 +4171,1252 @@
  2.1819      also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps)
  2.1820      finally show "setsum (op $$ ?a) ?D < 1" by auto qed qed
  2.1821  
  2.1822 +lemma rel_interior_substd_simplex: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
  2.1823 +  shows "rel_interior (convex hull (insert 0 { basis i| i. i : d})) =
  2.1824 +  {x::'a::euclidean_space. (\<forall>i\<in>d. 0 < x$$i) & setsum (%i. x$$i) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)}"
  2.1825 +  (is "rel_interior (convex hull (insert 0 ?p)) = ?s")
  2.1826 +(* Proof is a modified copy of the proof of similar lemma interior_std_simplex in Convex_Euclidean_Space.thy *)
  2.1827 +proof-
  2.1828 +have "finite d" apply(rule finite_subset) using assms by auto
  2.1829 +{ assume "d={}" hence ?thesis using rel_interior_sing using euclidean_eq[of _ 0] by auto }
  2.1830 +moreover
  2.1831 +{ assume "d~={}"
  2.1832 +have h0: "affine hull (convex hull (insert 0 ?p))={x::'a::euclidean_space. (!i<DIM('a). i ~: d --> x$$i = 0)}" 
  2.1833 +   using affine_hull_convex_hull affine_hull_substd_basis assms by auto 
  2.1834 +have aux: "!x::'n::euclidean_space. !i. ((! i:d. 0 <= x$$i) & (!i. i ~: d --> x$$i = 0))--> 0 <= x$$i" by auto
  2.1835 +{ fix x::"'a::euclidean_space" assume x_def: "x : rel_interior (convex hull (insert 0 ?p))"
  2.1836 +  from this obtain e where e0: "e>0" and 
  2.1837 +       "ball x e Int {xa. (!i<DIM('a). i ~: d --> xa$$i = 0)} <= convex hull (insert 0 ?p)" 
  2.1838 +       using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto   
  2.1839 +  hence as: "ALL xa. (dist x xa < e & (!i<DIM('a). i ~: d --> xa$$i = 0)) -->
  2.1840 +    (!i : d. 0 <= xa $$ i) & setsum (op $$ xa) d <= 1"
  2.1841 +    unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto
  2.1842 +  have x0: "(!i<DIM('a). i ~: d --> x$$i = 0)" 
  2.1843 +    using x_def rel_interior_subset  substd_simplex[OF assms] by auto
  2.1844 +  have "(!i : d. 0 < x $$ i) & setsum (op $$ x) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)" apply(rule,rule) 
  2.1845 +  proof-
  2.1846 +    fix i::nat assume "i:d" 
  2.1847 +    hence "\<forall>ia\<in>d. 0 \<le> (x - (e / 2) *\<^sub>R basis i) $$ ia" apply-apply(rule as[rule_format,THEN conjunct1])
  2.1848 +      unfolding dist_norm using assms `e>0` x0 by auto
  2.1849 +    thus "0 < x $$ i" apply(erule_tac x=i in ballE) using `e>0` `i\<in>d` assms by auto
  2.1850 +  next obtain a where a:"a:d" using `d ~= {}` by auto
  2.1851 +    have **:"dist x (x + (e / 2) *\<^sub>R basis a) < e"
  2.1852 +      using  `e>0` and Euclidean_Space.norm_basis[of a]
  2.1853 +      unfolding dist_norm by auto
  2.1854 +    have "\<And>i. (x + (e / 2) *\<^sub>R basis a) $$ i = x$$i + (if i = a then e/2 else 0)"
  2.1855 +      unfolding euclidean_simps using a assms by auto
  2.1856 +    hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis a)) d =
  2.1857 +      setsum (\<lambda>i. x$$i + (if a = i then e/2 else 0)) d" by(rule_tac setsum_cong, auto)
  2.1858 +    have h1: "(ALL i<DIM('a). i ~: d --> (x + (e / 2) *\<^sub>R basis a) $$ i = 0)"
  2.1859 +      using as[THEN spec[where x="x + (e / 2) *\<^sub>R basis a"]] `a:d` using x0
  2.1860 +      by(auto simp add: norm_basis elim:allE[where x=a]) 
  2.1861 +    have "setsum (op $$ x) d < setsum (op $$ (x + (e / 2) *\<^sub>R basis a)) d" unfolding * setsum_addf
  2.1862 +      using `0<e` `a:d` using `finite d` by(auto simp add: setsum_delta')
  2.1863 +    also have "\<dots> \<le> 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R basis a"] by auto
  2.1864 +    finally show "setsum (op $$ x) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)" using x0 by auto 
  2.1865 +  qed
  2.1866 +}
  2.1867 +moreover
  2.1868 +{
  2.1869 +  fix x::"'a::euclidean_space" assume as: "x : ?s"
  2.1870 +  have "!i. ((0<x$$i) | (0=x$$i) --> 0<=x$$i)" by auto
  2.1871 +  moreover have "!i. (i:d) | (i ~: d)" by auto
  2.1872 +  ultimately 
  2.1873 +  have "!i. ( (ALL i:d. 0 < x$$i) & (ALL i. i ~: d --> x$$i = 0) ) --> 0 <= x$$i" by metis
  2.1874 +  hence h2: "x : convex hull (insert 0 ?p)" using as assms 
  2.1875 +    unfolding substd_simplex[OF assms] by fastsimp 
  2.1876 +  obtain a where a:"a:d" using `d ~= {}` by auto
  2.1877 +  let ?d = "(1 - setsum (op $$ x) d) / real (card d)"
  2.1878 +  have "card d >= 1" using `d ~={}` card_ge1[of d] using `finite d` by auto
  2.1879 +  have "Min ((op $$ x) ` d) > 0" apply(rule Min_grI) using as `card d >= 1` `finite d` by auto
  2.1880 +  moreover have "?d > 0" apply(rule divide_pos_pos) using as using `card d >= 1` by(auto simp add: Suc_le_eq)
  2.1881 +  ultimately have h3: "min (Min ((op $$ x) ` d)) ?d > 0" by auto
  2.1882 +
  2.1883 +  have "x : rel_interior (convex hull (insert 0 ?p))"
  2.1884 +    unfolding rel_interior_ball mem_Collect_eq h0 apply(rule,rule h2)
  2.1885 +    unfolding substd_simplex[OF assms]
  2.1886 +    apply(rule_tac x="min (Min ((op $$ x) ` d)) ?d" in exI) apply(rule,rule h3) apply safe unfolding mem_ball
  2.1887 +  proof- fix y::'a assume y:"dist x y < min (Min (op $$ x ` d)) ?d" and y2:"(!i<DIM('a). i ~: d --> y$$i = 0)"
  2.1888 +    have "setsum (op $$ y) d \<le> setsum (\<lambda>i. x$$i + ?d) d" proof(rule setsum_mono)
  2.1889 +      fix i assume i:"i\<in>d"
  2.1890 +      have "abs (y$$i - x$$i) < ?d" apply(rule le_less_trans) using component_le_norm[of "y - x" i]
  2.1891 +        using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2]
  2.1892 +        by(auto simp add: norm_minus_commute)
  2.1893 +      thus "y $$ i \<le> x $$ i + ?d" by auto qed
  2.1894 +    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat
  2.1895 +      using `card d >= 1` by(auto simp add: Suc_le_eq)
  2.1896 +    finally show "setsum (op $$ y) d \<le> 1" .
  2.1897 +     
  2.1898 +    fix i assume "i<DIM('a)" thus "0 \<le> y$$i" 
  2.1899 +    proof(cases "i\<in>d") case True
  2.1900 +      have "norm (x - y) < x$$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
  2.1901 +        using Min_gr_iff[of "op $$ x ` d" "norm (x - y)"] `card d >= 1` `i:d`
  2.1902 +        apply auto by (metis Suc_n_not_le_n True card_eq_0_iff finite_imageI)
  2.1903 +      thus "0 \<le> y$$i" using component_le_norm[of "x - y" i] and as(1)[rule_format] by auto
  2.1904 +    qed(insert y2, auto)
  2.1905 +  qed
  2.1906 +} ultimately have
  2.1907 +    "!!x :: 'a::euclidean_space. (x : rel_interior (convex hull insert 0 {basis i |i. i : d})) =
  2.1908 +    (x : {x. (ALL i:d. 0 < x $$ i) &
  2.1909 +    setsum (op $$ x) d < 1 & (ALL i<DIM('a). i ~: d --> x $$ i = 0)})" by blast
  2.1910 +from this have ?thesis by (rule set_eqI)
  2.1911 +} ultimately show ?thesis by blast
  2.1912 +qed
  2.1913 +
  2.1914 +lemma rel_interior_substd_simplex_nonempty: assumes "d ~={}" "d\<subseteq>{..<DIM('a::euclidean_space)}"
  2.1915 +  obtains a::"'a::euclidean_space" where
  2.1916 +  "a : rel_interior(convex hull (insert 0 {basis i | i . i : d}))" proof-
  2.1917 +(* Proof is a modified copy of the proof of similar lemma interior_std_simplex_nonempty in Convex_Euclidean_Space.thy *)
  2.1918 +  let ?D = d let ?a = "setsum (\<lambda>b::'a::euclidean_space. inverse (2 * real (card d)) *\<^sub>R b) {(basis i) | i. i \<in> ?D}"
  2.1919 +  have *:"{basis i :: 'a | i. i \<in> ?D} = basis ` ?D" by auto
  2.1920 +  have "finite d" apply(rule finite_subset) using assms(2) by auto
  2.1921 +  hence d1: "real(card d) >= 1" using `d ~={}` card_ge1[of d] by auto
  2.1922 +  { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))"
  2.1923 +      unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def
  2.1924 +      apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"]) 
  2.1925 +      unfolding euclidean_component.setsum
  2.1926 +      apply(rule setsum_cong2)
  2.1927 +      using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2)
  2.1928 +      by (auto simp add: Euclidean_Space.basis_component[of i])}
  2.1929 +  note ** = this
  2.1930 +  show ?thesis apply(rule that[of ?a]) unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq
  2.1931 +  proof safe fix i assume "i:d" 
  2.1932 +    have "0 < inverse (2 * real (card d))" using d1 by(auto simp add: Suc_le_eq)
  2.1933 +    also have "...=?a $$ i" using **[of i] `i:d` by auto
  2.1934 +    finally show "0 < ?a $$ i" by auto
  2.1935 +  next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real (card d))) ?D" 
  2.1936 +      by(rule setsum_cong2, rule **) 
  2.1937 +    also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat real_divide_def[THEN sym]
  2.1938 +      by (auto simp add:field_simps)
  2.1939 +    finally show "setsum (op $$ ?a) ?D < 1" by auto
  2.1940 +  next fix i assume "i<DIM('a)" and "i~:d"
  2.1941 +    have "?a : (span {basis i | i. i : d})" 
  2.1942 +      apply (rule span_setsum[of "{basis i |i. i : d}" "(%b. b /\<^sub>R (2 * real (card d)))" "{basis i |i. i : d}"]) 
  2.1943 +      using finite_substdbasis[of d] apply blast 
  2.1944 +    proof-
  2.1945 +      { fix x assume "(x :: 'a::euclidean_space): {basis i |i. i : d}"
  2.1946 +        hence "x : span {basis i |i. i : d}" 
  2.1947 +          using span_superset[of _ "{basis i |i. i : d}"] by auto
  2.1948 +        hence "(x /\<^sub>R (2 * real (card d))) : (span {basis i |i. i : d})"
  2.1949 +          using span_mul[of x "{basis i |i. i : d}" "(inverse (real (card d)) / 2)"] by auto
  2.1950 +      } thus "\<forall>x\<in>{basis i |i. i \<in> d}. x /\<^sub>R (2 * real (card d)) \<in> span {basis i ::'a |i. i \<in> d}" by auto
  2.1951 +    qed
  2.1952 +    thus "?a $$ i = 0 " using `i~:d` unfolding span_substd_basis[OF assms(2)] using `i<DIM('a)` by auto
  2.1953 +  qed
  2.1954 +qed
  2.1955 +
  2.1956 +subsection{* Relative Interior of Convex Set *}
  2.1957 +
  2.1958 +lemma rel_interior_convex_nonempty_aux: 
  2.1959 +fixes S :: "('n::euclidean_space) set" 
  2.1960 +assumes "convex S" and "0 : S"
  2.1961 +shows "rel_interior S ~= {}"
  2.1962 +proof-
  2.1963 +{ assume "S = {0}" hence ?thesis using rel_interior_sing by auto }
  2.1964 +moreover { 
  2.1965 +assume "S ~= {0}"
  2.1966 +obtain B where B_def: "independent B & B<=S & (S <= span B) & card B = dim S" using basis_exists[of S] by auto
  2.1967 +hence "B~={}" using B_def assms `S ~= {0}` span_empty by auto
  2.1968 +have "insert 0 B <= span B" using subspace_span[of B] subspace_0[of "span B"] span_inc by auto
  2.1969 +hence "span (insert 0 B) <= span B" 
  2.1970 +    using span_span[of B] span_mono[of "insert 0 B" "span B"] by blast
  2.1971 +hence "convex hull insert 0 B <= span B" 
  2.1972 +    using convex_hull_subset_span[of "insert 0 B"] by auto
  2.1973 +hence "span (convex hull insert 0 B) <= span B"
  2.1974 +    using span_span[of B] span_mono[of "convex hull insert 0 B" "span B"] by blast
  2.1975 +hence *: "span (convex hull insert 0 B) = span B" 
  2.1976 +    using span_mono[of B "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
  2.1977 +hence "span (convex hull insert 0 B) = span S"
  2.1978 +    using B_def span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
  2.1979 +moreover have "0 : affine hull (convex hull insert 0 B)"
  2.1980 +    using hull_subset[of "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
  2.1981 +ultimately have **: "affine hull (convex hull insert 0 B) = affine hull S"
  2.1982 +    using affine_hull_span_0[of "convex hull insert 0 B"] affine_hull_span_0[of "S"] 
  2.1983 +    assms  hull_subset[of S] by auto
  2.1984 +obtain d and f::"'n=>'n" where fd: "card d = card B & linear f & f ` B = {basis i |i. i : (d :: nat set)} & 
  2.1985 +       f ` span B = {x. ALL i<DIM('n). i ~: d --> x $$ i = (0::real)} &  inj_on f (span B)" and d:"d\<subseteq>{..<DIM('n)}"
  2.1986 +    using basis_to_substdbasis_subspace_isomorphism[of B,OF _ ] B_def by auto
  2.1987 +hence "bounded_linear f" using linear_conv_bounded_linear by auto
  2.1988 +have "d ~={}" using fd B_def `B ~={}` by auto
  2.1989 +have "(insert 0 {basis i |i. i : d}) = f ` (insert 0 B)" using fd linear_0 by auto
  2.1990 +hence "(convex hull (insert 0 {basis i |i. i : d})) = f ` (convex hull (insert 0 B))"
  2.1991 +   using convex_hull_linear_image[of f "(insert 0 {basis i |i. i : d})"] 
  2.1992 +   convex_hull_linear_image[of f "(insert 0 B)"] `bounded_linear f` by auto
  2.1993 +moreover have "rel_interior (f ` (convex hull insert 0 B)) = 
  2.1994 +   f ` rel_interior (convex hull insert 0 B)"
  2.1995 +   apply (rule  rel_interior_injective_on_span_linear_image[of f "(convex hull insert 0 B)"])
  2.1996 +   using `bounded_linear f` fd * by auto
  2.1997 +ultimately have "rel_interior (convex hull insert 0 B) ~= {}"
  2.1998 +   using rel_interior_substd_simplex_nonempty[OF `d~={}` d] apply auto by blast 
  2.1999 +moreover have "convex hull (insert 0 B) <= S"
  2.2000 +   using B_def assms hull_mono[of "insert 0 B" "S" "convex"] convex_hull_eq by auto
  2.2001 +ultimately have ?thesis using subset_rel_interior[of "convex hull insert 0 B" S] ** by auto
  2.2002 +} ultimately show ?thesis by auto
  2.2003 +qed
  2.2004 +
  2.2005 +lemma rel_interior_convex_nonempty:
  2.2006 +fixes S :: "('n::euclidean_space) set"
  2.2007 +assumes "convex S"
  2.2008 +shows "rel_interior S = {} <-> S = {}"
  2.2009 +proof-
  2.2010 +{ assume "S ~= {}" from this obtain a where "a : S" by auto
  2.2011 +  hence "0 : op + (-a) ` S" using assms exI[of "(%x. x:S & -a+x=0)" a] by auto
  2.2012 +  hence "rel_interior (op + (-a) ` S) ~= {}"  
  2.2013 +    using rel_interior_convex_nonempty_aux[of "op + (-a) ` S"] 
  2.2014 +          convex_translation[of S "-a"] assms by auto 
  2.2015 +  hence "rel_interior S ~= {}" using rel_interior_translation by auto
  2.2016 +} from this show ?thesis using rel_interior_empty by auto
  2.2017 +qed
  2.2018 +
  2.2019 +lemma convex_rel_interior:
  2.2020 +fixes S :: "(_::euclidean_space) set"
  2.2021 +assumes "convex S"
  2.2022 +shows "convex (rel_interior S)"
  2.2023 +proof-
  2.2024 +{ fix "x" "y" "u"
  2.2025 +  assume assm: "x:rel_interior S" "y:rel_interior S" "0<=u" "(u :: real) <= 1"
  2.2026 +  hence "x:S" using rel_interior_subset by auto
  2.2027 +  have "x - u *\<^sub>R (x-y) : rel_interior S"
  2.2028 +  proof(cases "0=u")
  2.2029 +     case False hence "0<u" using assm by auto 
  2.2030 +        thus ?thesis
  2.2031 +        using assm rel_interior_convex_shrink[of S y x u] assms `x:S` by auto
  2.2032 +     next
  2.2033 +     case True thus ?thesis using assm by auto
  2.2034 +  qed
  2.2035 +  hence "(1-u) *\<^sub>R x + u *\<^sub>R y : rel_interior S" by (simp add: algebra_simps)
  2.2036 +} from this show ?thesis unfolding convex_alt by auto
  2.2037 +qed
  2.2038 +
  2.2039 +lemma convex_closure_rel_interior: 
  2.2040 +fixes S :: "('n::euclidean_space) set" 
  2.2041 +assumes "convex S"
  2.2042 +shows "closure(rel_interior S) = closure S"
  2.2043 +proof-
  2.2044 +have h1: "closure(rel_interior S) <= closure S" 
  2.2045 +   using subset_closure[of "rel_interior S" S] rel_interior_subset[of S] by auto
  2.2046 +{ assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S" 
  2.2047 +    using rel_interior_convex_nonempty assms by auto
  2.2048 +  { fix x assume x_def: "x : closure S"
  2.2049 +    { assume "x=a" hence "x : closure(rel_interior S)" using a_def unfolding closure_def by auto }
  2.2050 +    moreover
  2.2051 +    { assume "x ~= a"
  2.2052 +       { fix e :: real assume e_def: "e>0" 
  2.2053 +         def e1 == "min 1 (e/norm (x - a))" hence e1_def: "e1>0 & e1<=1 & e1*norm(x-a)<=e"
  2.2054 +            using `x ~= a` `e>0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm(x-a)"] by simp 
  2.2055 +         hence *: "x - e1 *\<^sub>R (x - a) : rel_interior S"
  2.2056 +            using rel_interior_closure_convex_shrink[of S a x e1] assms x_def a_def e1_def by auto
  2.2057 +         have "EX y. y:rel_interior S & y ~= x & (dist y x) <= e"
  2.2058 +            apply (rule_tac x="x - e1 *\<^sub>R (x - a)" in exI)
  2.2059 +            using * e1_def dist_norm[of "x - e1 *\<^sub>R (x - a)" x] `x ~= a` by simp
  2.2060 +      } hence "x islimpt rel_interior S" unfolding islimpt_approachable_le by auto 
  2.2061 +      hence "x : closure(rel_interior S)" unfolding closure_def by auto 
  2.2062 +    } ultimately have "x : closure(rel_interior S)" by auto
  2.2063 +  } hence ?thesis using h1 by auto
  2.2064 +}
  2.2065 +moreover
  2.2066 +{ assume "S = {}" hence "rel_interior S = {}" using rel_interior_empty by auto
  2.2067 +  hence "closure(rel_interior S) = {}" using closure_empty by auto 
  2.2068 +  hence ?thesis using `S={}` by auto 
  2.2069 +} ultimately show ?thesis by blast
  2.2070 +qed
  2.2071 +
  2.2072 +lemma rel_interior_same_affine_hull:
  2.2073 +  fixes S :: "('n::euclidean_space) set"
  2.2074 +  assumes "convex S"
  2.2075 +  shows "affine hull (rel_interior S) = affine hull S"
  2.2076 +by (metis assms closure_same_affine_hull convex_closure_rel_interior)
  2.2077 +
  2.2078 +lemma rel_interior_aff_dim: 
  2.2079 +  fixes S :: "('n::euclidean_space) set"
  2.2080 +  assumes "convex S"
  2.2081 +  shows "aff_dim (rel_interior S) = aff_dim S"
  2.2082 +by (metis aff_dim_affine_hull2 assms rel_interior_same_affine_hull)
  2.2083 +
  2.2084 +lemma rel_interior_rel_interior:
  2.2085 +  fixes S :: "('n::euclidean_space) set"
  2.2086 +  assumes "convex S"
  2.2087 +  shows "rel_interior (rel_interior S) = rel_interior S"
  2.2088 +proof-
  2.2089 +have "openin (subtopology euclidean (affine hull (rel_interior S))) (rel_interior S)"
  2.2090 +  using opein_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
  2.2091 +from this show ?thesis using rel_interior_def by auto
  2.2092 +qed
  2.2093 +
  2.2094 +lemma rel_interior_rel_open:
  2.2095 +  fixes S :: "('n::euclidean_space) set"
  2.2096 +  assumes "convex S"
  2.2097 +  shows "rel_open (rel_interior S)"
  2.2098 +unfolding rel_open_def using rel_interior_rel_interior assms by auto
  2.2099 +
  2.2100 +lemma convex_rel_interior_closure_aux:
  2.2101 +  fixes x y z :: "_::euclidean_space"
  2.2102 +  assumes "0 < a" "0 < b" "(a+b) *\<^sub>R z = a *\<^sub>R x + b *\<^sub>R y"
  2.2103 +  obtains e where "0 < e" "e <= 1" "z = y - e *\<^sub>R (y-x)"
  2.2104 +proof-
  2.2105 +def e == "a/(a+b)"
  2.2106 +have "z = (1 / (a + b)) *\<^sub>R ((a + b) *\<^sub>R z)" apply auto using assms by simp
  2.2107 +also have "... = (1 / (a + b)) *\<^sub>R (a *\<^sub>R x + b *\<^sub>R y)" using assms
  2.2108 +   scaleR_cancel_left[of "1/(a+b)" "(a + b) *\<^sub>R z" "a *\<^sub>R x + b *\<^sub>R y"] by auto
  2.2109 +also have "... = y - e *\<^sub>R (y-x)" using e_def apply (simp add: algebra_simps)
  2.2110 +   using scaleR_left_distrib[of "a/(a+b)" "b/(a+b)" y] assms add_divide_distrib[of a b "a+b"] by auto
  2.2111 +finally have "z = y - e *\<^sub>R (y-x)" by auto
  2.2112 +moreover have "0<e" using e_def assms divide_pos_pos[of a "a+b"] by auto
  2.2113 +moreover have "e<=1" using e_def assms by auto
  2.2114 +ultimately show ?thesis using that[of e] by auto
  2.2115 +qed
  2.2116 +
  2.2117 +lemma convex_rel_interior_closure: 
  2.2118 +  fixes S :: "('n::euclidean_space) set" 
  2.2119 +  assumes "convex S"
  2.2120 +  shows "rel_interior (closure S) = rel_interior S"
  2.2121 +proof-
  2.2122 +{ assume "S={}" hence ?thesis using assms rel_interior_convex_nonempty by auto }
  2.2123 +moreover
  2.2124 +{ assume "S ~= {}"
  2.2125 +  have "rel_interior (closure S) >= rel_interior S" 
  2.2126 +    using subset_rel_interior[of S "closure S"] closure_same_affine_hull closure_subset by auto
  2.2127 +  moreover
  2.2128 +  { fix z assume z_def: "z : rel_interior (closure S)"
  2.2129 +    obtain x where x_def: "x : rel_interior S" 
  2.2130 +      using `S ~= {}` assms rel_interior_convex_nonempty by auto  
  2.2131 +    { assume "x=z" hence "z : rel_interior S" using x_def by auto }
  2.2132 +    moreover
  2.2133 +    { assume "x ~= z"
  2.2134 +      obtain e where e_def: "e > 0 & cball z e Int affine hull closure S <= closure S" 
  2.2135 +        using z_def rel_interior_cball[of "closure S"] by auto
  2.2136 +      hence *: "0 < e/norm(z-x)" using e_def `x ~= z` divide_pos_pos[of e "norm(z-x)"] by auto 
  2.2137 +      def y == "z + (e/norm(z-x)) *\<^sub>R (z-x)"
  2.2138 +      have yball: "y : cball z e"
  2.2139 +        using mem_cball y_def dist_norm[of z y] e_def by auto 
  2.2140 +      have "x : affine hull closure S" 
  2.2141 +        using x_def rel_interior_subset_closure hull_inc[of x "closure S"] by auto
  2.2142 +      moreover have "z : affine hull closure S" 
  2.2143 +        using z_def rel_interior_subset hull_subset[of "closure S"] by auto
  2.2144 +      ultimately have "y : affine hull closure S" 
  2.2145 +        using y_def affine_affine_hull[of "closure S"] 
  2.2146 +          mem_affine_3_minus [of "affine hull closure S" z z x "e/norm(z-x)"] by auto
  2.2147 +      hence "y : closure S" using e_def yball by auto
  2.2148 +      have "(1+(e/norm(z-x))) *\<^sub>R z = (e/norm(z-x)) *\<^sub>R x + y"
  2.2149 +        using y_def by (simp add: algebra_simps) 
  2.2150 +      from this obtain e1 where "0 < e1 & e1 <= 1 & z = y - e1 *\<^sub>R (y - x)"
  2.2151 +        using * convex_rel_interior_closure_aux[of "e / norm (z - x)" 1 z x y] 
  2.2152 +          by (auto simp add: algebra_simps)
  2.2153 +      hence "z : rel_interior S" 
  2.2154 +        using rel_interior_closure_convex_shrink assms x_def `y : closure S` by auto
  2.2155 +    } ultimately have "z : rel_interior S" by auto
  2.2156 +  } ultimately have ?thesis by auto
  2.2157 +} ultimately show ?thesis by blast
  2.2158 +qed
  2.2159 +
  2.2160 +lemma convex_interior_closure: 
  2.2161 +fixes S :: "('n::euclidean_space) set" 
  2.2162 +assumes "convex S"
  2.2163 +shows "interior (closure S) = interior S"
  2.2164 +using closure_aff_dim[of S] interior_rel_interior_gen[of S] interior_rel_interior_gen[of "closure S"] 
  2.2165 +      convex_rel_interior_closure[of S] assms by auto
  2.2166 +
  2.2167 +lemma closure_eq_rel_interior_eq:
  2.2168 +fixes S1 S2 ::  "('n::euclidean_space) set" 
  2.2169 +assumes "convex S1" "convex S2"
  2.2170 +shows "(closure S1 = closure S2) <-> (rel_interior S1 = rel_interior S2)"
  2.2171 + by (metis convex_rel_interior_closure convex_closure_rel_interior assms)
  2.2172 +
  2.2173 +
  2.2174 +lemma closure_eq_between:
  2.2175 +fixes S1 S2 ::  "('n::euclidean_space) set" 
  2.2176 +assumes "convex S1" "convex S2"
  2.2177 +shows "(closure S1 = closure S2) <-> 
  2.2178 +      ((rel_interior S1 <= S2) & (S2 <= closure S1))" (is "?A <-> ?B")
  2.2179 +proof-
  2.2180 +have "?A --> ?B" by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
  2.2181 +moreover have "?B --> (closure S1 <= closure S2)" 
  2.2182 +     by (metis assms(1) convex_closure_rel_interior subset_closure)
  2.2183 +moreover have "?B --> (closure S1 >= closure S2)" by (metis closed_closure closure_minimal)
  2.2184 +ultimately show ?thesis by blast
  2.2185 +qed
  2.2186 +
  2.2187 +lemma open_inter_closure_rel_interior:
  2.2188 +fixes S A ::  "('n::euclidean_space) set" 
  2.2189 +assumes "convex S" "open A"
  2.2190 +shows "((A Int closure S) = {}) <-> ((A Int rel_interior S) = {})"
  2.2191 +by (metis assms convex_closure_rel_interior open_inter_closure_eq_empty) 
  2.2192 +
  2.2193 +definition "rel_frontier S = closure S - rel_interior S"
  2.2194 +
  2.2195 +lemma closed_affine_hull: "closed (affine hull ((S :: ('n::euclidean_space) set)))"
  2.2196 +by (metis affine_affine_hull affine_closed)
  2.2197 +
  2.2198 +lemma closed_rel_frontier: "closed(rel_frontier (S :: ('n::euclidean_space) set))"
  2.2199 +proof-
  2.2200 +have *: "closedin (subtopology euclidean (affine hull S)) (closure S - rel_interior S)" 
  2.2201 +apply (rule closedin_diff[of "subtopology euclidean (affine hull S)""closure S" "rel_interior S"])  using closed_closedin_trans[of "affine hull S" "closure S"] closed_affine_hull[of S] 
  2.2202 +  closure_affine_hull[of S] opein_rel_interior[of S] by auto 
  2.2203 +show ?thesis apply (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"]) 
  2.2204 +  unfolding rel_frontier_def using * closed_affine_hull by auto 
  2.2205 +qed
  2.2206 + 
  2.2207 +
  2.2208 +lemma convex_rel_frontier_aff_dim:
  2.2209 +fixes S1 S2 ::  "('n::euclidean_space) set" 
  2.2210 +assumes "convex S1" "convex S2" "S2 ~= {}"
  2.2211 +assumes "S1 <= rel_frontier S2"
  2.2212 +shows "aff_dim S1 < aff_dim S2" 
  2.2213 +proof-
  2.2214 +have "S1 <= closure S2" using assms unfolding rel_frontier_def by auto
  2.2215 +hence *: "affine hull S1 <= affine hull S2" 
  2.2216 +   using hull_mono[of "S1" "closure S2"] closure_same_affine_hull[of S2] by auto
  2.2217 +hence "aff_dim S1 <= aff_dim S2" using * aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2] 
  2.2218 +    aff_dim_subset[of "affine hull S1" "affine hull S2"] by auto
  2.2219 +moreover
  2.2220 +{ assume eq: "aff_dim S1 = aff_dim S2"
  2.2221 +  hence "S1 ~= {}" using aff_dim_empty[of S1] aff_dim_empty[of S2] `S2 ~= {}` by auto
  2.2222 +  have **: "affine hull S1 = affine hull S2" 
  2.2223 +     apply (rule affine_dim_equal) using * affine_affine_hull apply auto
  2.2224 +     using `S1 ~= {}` hull_subset[of S1] apply auto
  2.2225 +     using eq aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2] by auto
  2.2226 +  obtain a where a_def: "a : rel_interior S1"
  2.2227 +     using  `S1 ~= {}` rel_interior_convex_nonempty assms by auto
  2.2228 +  obtain T where T_def: "open T & a : T Int S1 & T Int affine hull S1 <= S1"
  2.2229 +     using mem_rel_interior[of a S1] a_def by auto
  2.2230 +  hence "a : T Int closure S2" using a_def assms unfolding rel_frontier_def by auto
  2.2231 +  from this obtain b where b_def: "b : T Int rel_interior S2" 
  2.2232 +     using open_inter_closure_rel_interior[of S2 T] assms T_def by auto
  2.2233 +  hence "b : affine hull S1" using rel_interior_subset hull_subset[of S2] ** by auto
  2.2234 +  hence "b : S1" using T_def b_def by auto
  2.2235 +  hence False using b_def assms unfolding rel_frontier_def by auto
  2.2236 +} ultimately show ?thesis using zless_le by auto
  2.2237 +qed
  2.2238 +
  2.2239 +
  2.2240 +lemma convex_rel_interior_if:
  2.2241 +fixes S ::  "('n::euclidean_space) set" 
  2.2242 +assumes "convex S"
  2.2243 +assumes "z : rel_interior S"
  2.2244 +shows "(!x:affine hull S. EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S ))"
  2.2245 +proof-
  2.2246 +obtain e1 where e1_def: "e1>0 & cball z e1 Int affine hull S <= S" 
  2.2247 +    using mem_rel_interior_cball[of z S] assms by auto
  2.2248 +{ fix x assume x_def: "x:affine hull S"
  2.2249 +  { assume "x ~= z"
  2.2250 +    def m == "1+e1/norm(x-z)" 
  2.2251 +    hence "m>1" using e1_def `x ~= z` divide_pos_pos[of e1 "norm (x - z)"] by auto 
  2.2252 +    { fix e assume e_def: "e>1 & e<=m"
  2.2253 +      have "z : affine hull S" using assms rel_interior_subset hull_subset[of S] by auto
  2.2254 +      hence *: "(1-e)*\<^sub>R x+ e *\<^sub>R z : affine hull S"
  2.2255 +         using mem_affine[of "affine hull S" x z "(1-e)" e] affine_affine_hull[of S] x_def by auto
  2.2256 +      have "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) = norm ((e - 1) *\<^sub>R (x-z))" by (simp add: algebra_simps)
  2.2257 +      also have "...= (e - 1) * norm(x-z)" using norm_scaleR e_def by auto  
  2.2258 +      also have "...<=(m - 1) * norm(x-z)" using e_def mult_right_mono[of _ _ "norm(x-z)"] by auto
  2.2259 +      also have "...= (e1 / norm (x - z)) * norm (x - z)" using m_def by auto
  2.2260 +      also have "...=e1" using `x ~= z` e1_def by simp
  2.2261 +      finally have **: "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) <= e1" by auto
  2.2262 +      have "(1-e)*\<^sub>R x+ e *\<^sub>R z : cball z e1"
  2.2263 +         using m_def ** unfolding cball_def dist_norm by (auto simp add: algebra_simps)
  2.2264 +      hence "(1-e)*\<^sub>R x+ e *\<^sub>R z : S" using e_def * e1_def by auto
  2.2265 +    } hence "EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S )" using `m>1` by auto
  2.2266 +  }
  2.2267 +  moreover
  2.2268 +  { assume "x=z" def m == "1+e1" hence "m>1" using e1_def by auto
  2.2269 +    { fix e assume e_def: "e>1 & e<=m"
  2.2270 +      hence "(1-e)*\<^sub>R x+ e *\<^sub>R z : S"
  2.2271 +        using e1_def x_def `x=z` by (auto simp add: algebra_simps)
  2.2272 +      hence "(1-e)*\<^sub>R x+ e *\<^sub>R z : S" using e_def by auto
  2.2273 +    } hence "EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S )" using `m>1` by auto
  2.2274 +  } ultimately have "EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S )" by auto
  2.2275 +} from this show ?thesis by auto 
  2.2276 +qed
  2.2277 +
  2.2278 +lemma convex_rel_interior_if2:
  2.2279 +fixes S ::  "('n::euclidean_space) set" 
  2.2280 +assumes "convex S"
  2.2281 +assumes "z : rel_interior S"
  2.2282 +shows "(!x:affine hull S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)"
  2.2283 +using convex_rel_interior_if[of S z] assms by auto
  2.2284 +
  2.2285 +lemma convex_rel_interior_only_if:
  2.2286 +fixes S ::  "('n::euclidean_space) set" 
  2.2287 +assumes "convex S" "S ~= {}"
  2.2288 +assumes "(!x:S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)"
  2.2289 +shows "z : rel_interior S" 
  2.2290 +proof-
  2.2291 +obtain x where x_def: "x : rel_interior S" using rel_interior_convex_nonempty assms by auto
  2.2292 +hence "x:S" using rel_interior_subset by auto
  2.2293 +from this obtain e where e_def: "e>1 & (1 - e) *\<^sub>R x + e *\<^sub>R z : S" using assms by auto
  2.2294 +def y == "(1 - e) *\<^sub>R x + e *\<^sub>R z" hence "y:S" using e_def by auto
  2.2295 +def e1 == "1/e" hence "0<e1 & e1<1" using e_def by auto
  2.2296 +hence "z=y-(1-e1)*\<^sub>R (y-x)" using e1_def y_def by (auto simp add: algebra_simps)
  2.2297 +from this show ?thesis 
  2.2298 +    using rel_interior_convex_shrink[of S x y "1-e1"] `0<e1 & e1<1` `y:S` x_def assms by auto
  2.2299 +qed
  2.2300 +
  2.2301 +lemma convex_rel_interior_iff:
  2.2302 +fixes S ::  "('n::euclidean_space) set" 
  2.2303 +assumes "convex S" "S ~= {}"
  2.2304 +shows "z : rel_interior S <-> (!x:S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)"
  2.2305 +using assms hull_subset[of S "affine"] 
  2.2306 +      convex_rel_interior_if[of S z] convex_rel_interior_only_if[of S z] by auto
  2.2307 +
  2.2308 +lemma convex_rel_interior_iff2:
  2.2309 +fixes S ::  "('n::euclidean_space) set" 
  2.2310 +assumes "convex S" "S ~= {}"
  2.2311 +shows "z : rel_interior S <-> (!x:affine hull S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)"
  2.2312 +using assms hull_subset[of S] 
  2.2313 +      convex_rel_interior_if2[of S z] convex_rel_interior_only_if[of S z] by auto
  2.2314 +
  2.2315 +
  2.2316 +lemma convex_interior_iff:
  2.2317 +fixes S ::  "('n::euclidean_space) set" 
  2.2318 +assumes "convex S"
  2.2319 +shows "z : interior S <-> (!x. EX e. e>0 & z+ e *\<^sub>R x : S)"
  2.2320 +proof-
  2.2321 +{ assume a: "~(aff_dim S = int DIM('n))"
  2.2322 +  { assume "z : interior S"
  2.2323 +    hence False using a interior_rel_interior_gen[of S] by auto
  2.2324 +  }
  2.2325 +  moreover
  2.2326 +  { assume r: "!x. EX e. e>0 & z+ e *\<^sub>R x : S"
  2.2327 +    { fix x obtain e1 where e1_def: "e1>0 & z+ e1 *\<^sub>R (x-z) : S" using r by auto
  2.2328 +      obtain e2 where e2_def: "e2>0 & z+ e2 *\<^sub>R (z-x) : S" using r by auto
  2.2329 +      def x1 == "z+ e1 *\<^sub>R (x-z)"
  2.2330 +         hence x1: "x1 : affine hull S" using e1_def hull_subset[of S] by auto
  2.2331 +      def x2 == "z+ e2 *\<^sub>R (z-x)"
  2.2332 +         hence x2: "x2 : affine hull S" using e2_def hull_subset[of S] by auto
  2.2333 +      have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using divide.add[of e1 e2 "e1+e2"] e1_def e2_def by simp
  2.2334 +      hence "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
  2.2335 +         using x1_def x2_def apply (auto simp add: algebra_simps)
  2.2336 +         using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] by auto
  2.2337 +      hence z: "z : affine hull S" 
  2.2338 +         using mem_affine[of "affine hull S" x1 x2 "e2/(e1+e2)" "e1/(e1+e2)"]  
  2.2339 +         x1 x2 affine_affine_hull[of S] * by auto
  2.2340 +      have "x1-x2 = (e1+e2) *\<^sub>R (x-z)"
  2.2341 +         using x1_def x2_def by (auto simp add: algebra_simps)
  2.2342 +      hence "x=z+(1/(e1+e2)) *\<^sub>R (x1-x2)" using e1_def e2_def by simp
  2.2343 +      hence "x : affine hull S" using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"] 
  2.2344 +          x1 x2 z affine_affine_hull[of S] by auto
  2.2345 +    } hence "affine hull S = UNIV" by auto
  2.2346 +    hence "aff_dim S = int DIM('n)" using aff_dim_affine_hull[of S] by (simp add: aff_dim_univ)
  2.2347 +    hence False using a by auto
  2.2348 +  } ultimately have ?thesis by auto
  2.2349 +}
  2.2350 +moreover
  2.2351 +{ assume a: "aff_dim S = int DIM('n)"
  2.2352 +  hence "S ~= {}" using aff_dim_empty[of S] by auto
  2.2353 +  have *: "affine hull S=UNIV" using a affine_hull_univ by auto
  2.2354 +  { assume "z : interior S"
  2.2355 +    hence "z : rel_interior S" using a interior_rel_interior_gen[of S] by auto
  2.2356 +    hence **: "(!x. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)"
  2.2357 +      using convex_rel_interior_iff2[of S z] assms `S~={}` * by auto
  2.2358 +    fix x obtain e1 where e1_def: "e1>1 & (1-e1)*\<^sub>R (z-x)+ e1 *\<^sub>R z : S"
  2.2359 +      using **[rule_format, of "z-x"] by auto
  2.2360 +    def e == "e1 - 1"
  2.2361 +    hence "(1-e1)*\<^sub>R (z-x)+ e1 *\<^sub>R z = z+ e *\<^sub>R x" by (simp add: algebra_simps)
  2.2362 +    hence "e>0 & z+ e *\<^sub>R x : S" using e1_def e_def by auto
  2.2363 +    hence "EX e. e>0 & z+ e *\<^sub>R x : S" by auto
  2.2364 +  }
  2.2365 +  moreover
  2.2366 +  { assume r: "(!x. EX e. e>0 & z+ e *\<^sub>R x : S)"
  2.2367 +    { fix x obtain e1 where e1_def: "e1>0 & z + e1*\<^sub>R (z-x) : S"
  2.2368 +         using r[rule_format, of "z-x"] by auto
  2.2369 +      def e == "e1 + 1"
  2.2370 +      hence "z + e1*\<^sub>R (z-x) = (1-e)*\<^sub>R x+ e *\<^sub>R z" by (simp add: algebra_simps)
  2.2371 +      hence "e > 1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S" using e1_def e_def by auto
  2.2372 +      hence "EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S" by auto
  2.2373 +    }
  2.2374 +    hence "z : rel_interior S" using convex_rel_interior_iff2[of S z] assms `S~={}` by auto
  2.2375 +    hence "z : interior S" using a interior_rel_interior_gen[of S] by auto
  2.2376 +  } ultimately have ?thesis by auto
  2.2377 +} ultimately show ?thesis by auto
  2.2378 +qed
  2.2379 +
  2.2380 +subsection{* Relative interior and closure under commom operations *}
  2.2381 +
  2.2382 +lemma rel_interior_inter_aux: "Inter {rel_interior S |S. S : I} <= Inter I"
  2.2383 +proof- 
  2.2384 +{ fix y assume "y : Inter {rel_interior S |S. S : I}"
  2.2385 +  hence y_def: "!S : I. y : rel_interior S" by auto
  2.2386 +  { fix S assume "S : I" hence "y : S" using rel_interior_subset y_def by auto }
  2.2387 +  hence "y : Inter I" by auto
  2.2388 +} thus ?thesis by auto
  2.2389 +qed
  2.2390 +
  2.2391 +lemma closure_inter: "closure (Inter I) <= Inter {closure S |S. S : I}"
  2.2392 +proof- 
  2.2393 +{ fix y assume "y : Inter I" hence y_def: "!S : I. y : S" by auto
  2.2394 +  { fix S assume "S : I" hence "y : closure S" using closure_subset y_def by auto }
  2.2395 +  hence "y : Inter {closure S |S. S : I}" by auto
  2.2396 +} hence "Inter I <= Inter {closure S |S. S : I}" by auto
  2.2397 +moreover have "Inter {closure S |S. S : I} : closed" 
  2.2398 +  unfolding mem_def closed_Inter closed_closure by auto
  2.2399 +ultimately show ?thesis using closure_hull[of "Inter I"]
  2.2400 +  hull_minimal[of "Inter I" "Inter {closure S |S. S : I}" "closed"] by auto
  2.2401 +qed
  2.2402 +
  2.2403 +lemma convex_closure_rel_interior_inter: 
  2.2404 +assumes "!S : I. convex (S :: ('n::euclidean_space) set)"
  2.2405 +assumes "Inter {rel_interior S |S. S : I} ~= {}"
  2.2406 +shows "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})"
  2.2407 +proof-
  2.2408 +obtain x where x_def: "!S : I. x : rel_interior S" using assms by auto
  2.2409 +{ fix y assume "y : Inter {closure S |S. S : I}" hence y_def: "!S : I. y : closure S" by auto
  2.2410 +  { assume "y = x" 
  2.2411 +    hence "y : closure (Inter {rel_interior S |S. S : I})"
  2.2412 +       using x_def closure_subset[of "Inter {rel_interior S |S. S : I}"] by auto
  2.2413 +  }
  2.2414 +  moreover
  2.2415 +  { assume "y ~= x"
  2.2416 +    { fix e :: real assume e_def: "0 < e"
  2.2417 +      def e1 == "min 1 (e/norm (y - x))" hence e1_def: "e1>0 & e1<=1 & e1*norm(y-x)<=e"
  2.2418 +        using `y ~= x` `e>0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm(y-x)"] by simp 
  2.2419 +      def z == "y - e1 *\<^sub>R (y - x)"
  2.2420 +      { fix S assume "S : I" 
  2.2421 +        hence "z : rel_interior S" using rel_interior_closure_convex_shrink[of S x y e1] 
  2.2422 +           assms x_def y_def e1_def z_def by auto
  2.2423 +      } hence *: "z : Inter {rel_interior S |S. S : I}" by auto
  2.2424 +      have "EX z. z:Inter {rel_interior S |S. S : I} & z ~= y & (dist z y) <= e"
  2.2425 +           apply (rule_tac x="z" in exI) using `y ~= x` z_def * e1_def e_def dist_norm[of z y] by simp
  2.2426 +    } hence "y islimpt Inter {rel_interior S |S. S : I}" unfolding islimpt_approachable_le by blast 
  2.2427 +    hence "y : closure (Inter {rel_interior S |S. S : I})" unfolding closure_def by auto
  2.2428 +  } ultimately have "y : closure (Inter {rel_interior S |S. S : I})" by auto
  2.2429 +} from this show ?thesis by auto
  2.2430 +qed
  2.2431 +
  2.2432 +
  2.2433 +lemma convex_closure_inter: 
  2.2434 +assumes "!S : I. convex (S :: ('n::euclidean_space) set)"
  2.2435 +assumes "Inter {rel_interior S |S. S : I} ~= {}"
  2.2436 +shows "closure (Inter I) = Inter {closure S |S. S : I}"
  2.2437 +proof-
  2.2438 +have "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})" 
  2.2439 +  using convex_closure_rel_interior_inter assms by auto
  2.2440 +moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" 
  2.2441 +    using rel_interior_inter_aux 
  2.2442 +          subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
  2.2443 +ultimately show ?thesis using closure_inter[of I] by auto
  2.2444 +qed
  2.2445 +
  2.2446 +lemma convex_inter_rel_interior_same_closure: 
  2.2447 +assumes "!S : I. convex (S :: ('n::euclidean_space) set)"
  2.2448 +assumes "Inter {rel_interior S |S. S : I} ~= {}"
  2.2449 +shows "closure (Inter {rel_interior S |S. S : I}) = closure (Inter I)"
  2.2450 +proof-
  2.2451 +have "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})" 
  2.2452 +  using convex_closure_rel_interior_inter assms by auto
  2.2453 +moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" 
  2.2454 +    using rel_interior_inter_aux 
  2.2455 +          subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
  2.2456 +ultimately show ?thesis using closure_inter[of I] by auto
  2.2457 +qed
  2.2458 +
  2.2459 +lemma convex_rel_interior_inter: 
  2.2460 +assumes "!S : I. convex (S :: ('n::euclidean_space) set)"
  2.2461 +assumes "Inter {rel_interior S |S. S : I} ~= {}"
  2.2462 +shows "rel_interior (Inter I) <= Inter {rel_interior S |S. S : I}"
  2.2463 +proof-
  2.2464 +have "convex(Inter I)" using assms convex_Inter by auto
  2.2465 +moreover have "convex(Inter {rel_interior S |S. S : I})" apply (rule convex_Inter)
  2.2466 +   using assms convex_rel_interior by auto 
  2.2467 +ultimately have "rel_interior (Inter {rel_interior S |S. S : I}) = rel_interior (Inter I)"
  2.2468 +   using convex_inter_rel_interior_same_closure assms 
  2.2469 +   closure_eq_rel_interior_eq[of "Inter {rel_interior S |S. S : I}" "Inter I"] by blast
  2.2470 +from this show ?thesis using rel_interior_subset[of "Inter {rel_interior S |S. S : I}"] by auto
  2.2471 +qed
  2.2472 +
  2.2473 +lemma convex_rel_interior_finite_inter: 
  2.2474 +assumes "!S : I. convex (S :: ('n::euclidean_space) set)"
  2.2475 +assumes "Inter {rel_interior S |S. S : I} ~= {}"
  2.2476 +assumes "finite I"
  2.2477 +shows "rel_interior (Inter I) = Inter {rel_interior S |S. S : I}"
  2.2478 +proof-
  2.2479 +have "Inter I ~= {}" using assms rel_interior_inter_aux[of I] by auto
  2.2480 +have "convex (Inter I)" using convex_Inter assms by auto
  2.2481 +{ assume "I={}" hence ?thesis using Inter_empty rel_interior_univ2 by auto }
  2.2482 +moreover
  2.2483 +{ assume "I ~= {}"
  2.2484 +{ fix z assume z_def: "z : Inter {rel_interior S |S. S : I}"
  2.2485 +  { fix x assume x_def: "x : Inter I"
  2.2486 +    { fix S assume S_def: "S : I" hence "z : rel_interior S" "x : S" using z_def x_def by auto 
  2.2487 +      (*from this obtain e where e_def: "e>1 & (1 - e) *\<^sub>R x + e *\<^sub>R z : S"*)
  2.2488 +      hence "EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S )"
  2.2489 +         using convex_rel_interior_if[of S z] S_def assms hull_subset[of S] by auto
  2.2490 +    } from this obtain mS where mS_def: "!S : I. (mS(S) > (1 :: real) & 
  2.2491 +         (!e. (e>1 & e<=mS(S)) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S))" by metis
  2.2492 +    obtain e where e_def: "e=Min (mS ` I)" by auto 
  2.2493 +    have "e : (mS ` I)" using e_def assms `I ~= {}` by (simp add: Min_in) 
  2.2494 +    hence "e>(1 :: real)" using mS_def by auto
  2.2495 +    moreover have "!S : I. e<=mS(S)" using e_def assms by auto
  2.2496 +    ultimately have "EX e>1. (1 - e) *\<^sub>R x + e *\<^sub>R z : Inter I" using mS_def by auto
  2.2497 +  } hence "z : rel_interior (Inter I)" using convex_rel_interior_iff[of "Inter I" z]
  2.2498 +       `Inter I ~= {}` `convex (Inter I)` by auto
  2.2499 +} from this have ?thesis using convex_rel_interior_inter[of I] assms by auto
  2.2500 +} ultimately show ?thesis by blast
  2.2501 +qed
  2.2502 +
  2.2503 +lemma convex_closure_inter_two: 
  2.2504 +fixes S T :: "('n::euclidean_space) set"
  2.2505 +assumes "convex S" "convex T"
  2.2506 +assumes "(rel_interior S) Int (rel_interior T) ~= {}"
  2.2507 +shows "closure (S Int T) = (closure S) Int (closure T)" 
  2.2508 +using convex_closure_inter[of "{S,T}"] assms by auto
  2.2509 +
  2.2510 +lemma convex_rel_interior_inter_two: 
  2.2511 +fixes S T :: "('n::euclidean_space) set"
  2.2512 +assumes "convex S" "convex T"
  2.2513 +assumes "(rel_interior S) Int (rel_interior T) ~= {}"
  2.2514 +shows "rel_interior (S Int T) = (rel_interior S) Int (rel_interior T)" 
  2.2515 +using convex_rel_interior_finite_inter[of "{S,T}"] assms by auto
  2.2516 +
  2.2517 +
  2.2518 +lemma convex_affine_closure_inter: 
  2.2519 +fixes S T :: "('n::euclidean_space) set"
  2.2520 +assumes "convex S" "affine T"
  2.2521 +assumes "(rel_interior S) Int T ~= {}"
  2.2522 +shows "closure (S Int T) = (closure S) Int T"
  2.2523 +proof- 
  2.2524 +have "affine hull T = T" using assms by auto
  2.2525 +hence "rel_interior T = T" using rel_interior_univ[of T] by metis
  2.2526 +moreover have "closure T = T" using assms affine_closed[of T] by auto
  2.2527 +ultimately show ?thesis using convex_closure_inter_two[of S T] assms affine_imp_convex by auto 
  2.2528 +qed
  2.2529 +
  2.2530 +lemma convex_affine_rel_interior_inter: 
  2.2531 +fixes S T :: "('n::euclidean_space) set"
  2.2532 +assumes "convex S" "affine T"
  2.2533 +assumes "(rel_interior S) Int T ~= {}"
  2.2534 +shows "rel_interior (S Int T) = (rel_interior S) Int T"
  2.2535 +proof- 
  2.2536 +have "affine hull T = T" using assms by auto
  2.2537 +hence "rel_interior T = T" using rel_interior_univ[of T] by metis
  2.2538 +moreover have "closure T = T" using assms affine_closed[of T] by auto
  2.2539 +ultimately show ?thesis using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto 
  2.2540 +qed
  2.2541 +
  2.2542 +lemma subset_rel_interior_convex:
  2.2543 +fixes S T :: "('n::euclidean_space) set"
  2.2544 +assumes "convex S" "convex T"
  2.2545 +assumes "S <= closure T"
  2.2546 +assumes "~(S <= rel_frontier T)"
  2.2547 +shows "rel_interior S <= rel_interior T"
  2.2548 +proof-
  2.2549 +have *: "S Int closure T = S" using assms by auto
  2.2550 +have "~(rel_interior S <= rel_frontier T)"
  2.2551 +     using subset_closure[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] 
  2.2552 +     closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
  2.2553 +hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}" 
  2.2554 +     using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
  2.2555 +hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure  
  2.2556 +     convex_rel_interior_inter_two[of S "closure T"] convex_rel_interior_closure[of T] by auto
  2.2557 +also have "...=rel_interior (S)" using * by auto
  2.2558 +finally show ?thesis by auto
  2.2559 +qed
  2.2560 +
  2.2561 +
  2.2562 +lemma rel_interior_convex_linear_image:
  2.2563 +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
  2.2564 +assumes "linear f"
  2.2565 +assumes "convex S"
  2.2566 +shows "f ` (rel_interior S) = rel_interior (f ` S)"
  2.2567 +proof-
  2.2568 +{ assume "S = {}" hence ?thesis using assms rel_interior_empty rel_interior_convex_nonempty by auto }
  2.2569 +moreover
  2.2570 +{ assume "S ~= {}"
  2.2571 +have *: "f ` (rel_interior S) <= f ` S" unfolding image_mono using rel_interior_subset by auto
  2.2572 +have "f ` S <= f ` (closure S)" unfolding image_mono using closure_subset by auto
  2.2573 +also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto  
  2.2574 +also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto 
  2.2575 +finally have "closure (f ` S) = closure (f ` rel_interior S)"
  2.2576 +   using subset_closure[of "f ` S" "closure (f ` rel_interior S)"] closure_closure 
  2.2577 +         subset_closure[of "f ` rel_interior S" "f ` S"] * by auto
  2.2578 +hence "rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior
  2.2579 +   linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"] 
  2.2580 +   closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"] by auto
  2.2581 +hence "rel_interior (f ` S) <= f ` rel_interior S" using rel_interior_subset by auto
  2.2582 +moreover
  2.2583 +{ fix z assume z_def: "z : f ` rel_interior S"
  2.2584 +  from this obtain z1 where z1_def: "z1 : rel_interior S & (f z1 = z)" by auto
  2.2585 +  { fix x assume "x : f ` S"
  2.2586 +    from this obtain x1 where x1_def: "x1 : S & (f x1 = x)" by auto
  2.2587 +    from this obtain e where e_def: "e>1 & (1 - e) *\<^sub>R x1 + e *\<^sub>R z1 : S"
  2.2588 +       using convex_rel_interior_iff[of S z1] `convex S` x1_def z1_def by auto
  2.2589 +    moreover have "f ((1 - e) *\<^sub>R x1 + e *\<^sub>R z1) = (1 - e) *\<^sub>R x + e *\<^sub>R z"
  2.2590 +        using x1_def z1_def `linear f` by (simp add: linear_add_cmul)
  2.2591 +    ultimately have "(1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S"
  2.2592 +        using imageI[of "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1" S f] by auto
  2.2593 +    hence "EX e. (e>1 & (1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S)" using e_def by auto
  2.2594 +  } from this have "z : rel_interior (f ` S)" using convex_rel_interior_iff[of "f ` S" z] `convex S` 
  2.2595 +       `linear f` `S ~= {}` convex_linear_image[of S f]  linear_conv_bounded_linear[of f] by auto
  2.2596 +} ultimately have ?thesis by auto
  2.2597 +} ultimately show ?thesis by blast
  2.2598 +qed
  2.2599 +
  2.2600 +
  2.2601 +lemma convex_linear_preimage:
  2.2602 +  assumes c:"convex S" and l:"bounded_linear f"
  2.2603 +  shows "convex(f -` S)"
  2.2604 +proof(auto simp add: convex_def)
  2.2605 +  interpret f: bounded_linear f by fact
  2.2606 +  fix x y assume xy:"f x : S" "f y : S"
  2.2607 +  fix u v ::real assume uv:"0 <= u" "0 <= v" "u + v = 1"
  2.2608 +  show "f (u *\<^sub>R x + v *\<^sub>R y) : S" unfolding image_iff
  2.2609 +    using bexI[of _ "u *\<^sub>R x + v *\<^sub>R y"] f.add f.scaleR
  2.2610 +      c[unfolded convex_def] xy uv by auto
  2.2611 +qed
  2.2612 +
  2.2613 +
  2.2614 +lemma rel_interior_convex_linear_preimage:
  2.2615 +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
  2.2616 +assumes "linear f"
  2.2617 +assumes "convex S"
  2.2618 +assumes "f -` (rel_interior S) ~= {}"
  2.2619 +shows "rel_interior (f -` S) = f -` (rel_interior S)"
  2.2620 +proof-
  2.2621 +have "S ~= {}" using assms rel_interior_empty by auto
  2.2622 +have nonemp: "f -` S ~= {}" by (metis assms(3) rel_interior_subset subset_empty vimage_mono) 
  2.2623 +hence "S Int (range f) ~= {}" by auto
  2.2624 +have conv: "convex (f -` S)" using convex_linear_preimage assms linear_conv_bounded_linear by auto
  2.2625 +hence "convex (S Int (range f))"
  2.2626 +  by (metis assms(1) assms(2) convex_Int subspace_UNIV subspace_imp_convex subspace_linear_image)
  2.2627 +{ fix z assume "z : f -` (rel_interior S)"
  2.2628 +  hence z_def: "f z : rel_interior S" by auto
  2.2629 +  { fix x assume "x : f -` S" from this have x_def: "f x : S" by auto
  2.2630 +    from this obtain e where e_def: "e>1 & (1-e)*\<^sub>R (f x)+ e *\<^sub>R (f z) : S"
  2.2631 +      using convex_rel_interior_iff[of S "f z"] z_def assms `S ~= {}` by auto
  2.2632 +    moreover have "(1-e)*\<^sub>R (f x)+ e *\<^sub>R (f z) = f ((1-e)*\<^sub>R x + e *\<^sub>R z)"
  2.2633 +      using `linear f` by (simp add: linear_def)
  2.2634 +    ultimately have "EX e. e>1 & (1-e)*\<^sub>R x + e *\<^sub>R z : f -` S" using e_def by auto
  2.2635 +  } hence "z : rel_interior (f -` S)" 
  2.2636 +       using convex_rel_interior_iff[of "f -` S" z] conv nonemp by auto
  2.2637 +} 
  2.2638 +moreover
  2.2639 +{ fix z assume z_def: "z : rel_interior (f -` S)" 
  2.2640 +  { fix x assume x_def: "x: S Int (range f)"
  2.2641 +    from this obtain y where y_def: "(f y = x) & (y : f -` S)" by auto
  2.2642 +    from this obtain e where e_def: "e>1 & (1-e)*\<^sub>R y+ e *\<^sub>R z : f -` S"
  2.2643 +      using convex_rel_interior_iff[of "f -` S" z] z_def conv by auto
  2.2644 +    moreover have "(1-e)*\<^sub>R x+ e *\<^sub>R (f z) = f ((1-e)*\<^sub>R y + e *\<^sub>R z)"
  2.2645 +      using `linear f` y_def by (simp add: linear_def)
  2.2646 +    ultimately have "EX e. e>1 & (1-e)*\<^sub>R x + e *\<^sub>R (f z) : S Int (range f)"
  2.2647 +      using e_def by auto
  2.2648 +  } hence "f z : rel_interior (S Int (range f))" using `convex (S Int (range f))`
  2.2649 +    `S Int (range f) ~= {}` convex_rel_interior_iff[of "S Int (range f)" "f z"] by auto
  2.2650 +  moreover have "affine (range f)"
  2.2651 +    by (metis assms(1) subspace_UNIV subspace_imp_affine subspace_linear_image)
  2.2652 +  ultimately have "f z : rel_interior S" 
  2.2653 +    using convex_affine_rel_interior_inter[of S "range f"] assms by auto
  2.2654 +  hence "z : f -` (rel_interior S)" by auto
  2.2655 +}
  2.2656 +ultimately show ?thesis by auto
  2.2657 +qed
  2.2658 +    
  2.2659 +
  2.2660 +lemma convex_direct_sum:
  2.2661 +fixes S :: "('n::euclidean_space) set"
  2.2662 +fixes T :: "('m::euclidean_space) set"
  2.2663 +assumes "convex S" "convex T"
  2.2664 +shows "convex (S <*> T)"
  2.2665 +proof-
  2.2666 +{
  2.2667 +fix x assume "x : S <*> T"
  2.2668 +from this obtain xs xt where xst_def: "xs : S & xt : T & (xs,xt) = x" by auto
  2.2669 +fix y assume "y : S <*> T"
  2.2670 +from this obtain ys yt where yst_def: "ys : S & yt : T & (ys,yt) = y" by auto
  2.2671 +fix u v assume uv_def: "(u :: real)>=0 & (v :: real)>=0 & u+v=1"
  2.2672 +have "u *\<^sub>R x + v *\<^sub>R y = (u *\<^sub>R xs + v *\<^sub>R ys, u *\<^sub>R xt + v *\<^sub>R yt)" using xst_def yst_def by auto
  2.2673 +moreover have "u *\<^sub>R xs + v *\<^sub>R ys : S"
  2.2674 +   using uv_def xst_def yst_def convex_def[of S] assms by auto
  2.2675 +moreover have "u *\<^sub>R xt + v *\<^sub>R yt : T"
  2.2676 +   using uv_def xst_def yst_def convex_def[of T] assms by auto
  2.2677 +ultimately have "u *\<^sub>R x + v *\<^sub>R y : S <*> T" by auto
  2.2678 +} from this show ?thesis unfolding convex_def by auto
  2.2679 +qed
  2.2680 +
  2.2681 +
  2.2682 +lemma convex_hull_direct_sum:
  2.2683 +fixes S :: "('n::euclidean_space) set"
  2.2684 +fixes T :: "('m::euclidean_space) set"
  2.2685 +shows "convex hull (S <*> T) = (convex hull S) <*> (convex hull T)"
  2.2686 +proof-
  2.2687 +{ fix x assume "x : (convex hull S) <*> (convex hull T)"
  2.2688 +  from this obtain xs xt where xst_def: "xs : convex hull S & xt : convex hull T & (xs,xt) = x" by auto
  2.2689 +  from xst_def obtain sI su where s: "finite sI & sI <= S & (ALL x:sI. 0 <= su x) & setsum su sI = 1 
  2.2690 +     & (SUM v:sI. su v *\<^sub>R v) = xs" using convex_hull_explicit[of S] by auto
  2.2691 +  from xst_def obtain tI tu where t: "finite tI & tI <= T & (ALL x:tI. 0 <= tu x) & setsum tu tI = 1 
  2.2692 +     & (SUM v:tI. tu v *\<^sub>R v) = xt" using convex_hull_explicit[of T] by auto
  2.2693 +  def I == "(sI <*> tI)"
  2.2694 +  def u == "(%i. (su (fst i))*(tu(snd i)))"
  2.2695 +  have "fst (SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)=
  2.2696 +     (SUM vs:sI. SUM vt:tI. (su vs * tu vt) *\<^sub>R vs)"
  2.2697 +     using fst_setsum[of "(%v. (su (fst v) * tu (snd v)) *\<^sub>R v)" "sI <*> tI"]
  2.2698 +     by (simp add: split_def scaleR_prod_def setsum_cartesian_product)
  2.2699 +  also have "...=(SUM vt:tI. tu vt *\<^sub>R (SUM vs:sI. su vs *\<^sub>R vs))"
  2.2700 +     using setsum_commute[of "(%vt vs. (su vs * tu vt) *\<^sub>R vs)" sI tI]
  2.2701 +     by (simp add: mult_commute scaleR_right.setsum)
  2.2702 +  also have "...=(SUM vt:tI. tu vt *\<^sub>R xs)" using s by auto
  2.2703 +  also have "...=(SUM vt:tI. tu vt) *\<^sub>R xs" by (simp add: scaleR_left.setsum)
  2.2704 +  also have "...=xs" using t by auto
  2.2705 +  finally have h1: "fst (SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)=xs" by auto
  2.2706 +  have "snd (SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)=
  2.2707 +     (SUM vs:sI. SUM vt:tI. (su vs * tu vt) *\<^sub>R vt)"
  2.2708 +     using snd_setsum[of "(%v. (su (fst v) * tu (snd v)) *\<^sub>R v)" "sI <*> tI"]
  2.2709 +     by (simp add: split_def scaleR_prod_def setsum_cartesian_product)
  2.2710 +  also have "...=(SUM vs:sI. su vs *\<^sub>R (SUM vt:tI. tu vt *\<^sub>R vt))"
  2.2711 +     by (simp add: mult_commute scaleR_right.setsum)
  2.2712 +  also have "...=(SUM vs:sI. su vs *\<^sub>R xt)" using t by auto
  2.2713 +  also have "...=(SUM vs:sI. su vs) *\<^sub>R xt" by (simp add: scaleR_left.setsum)
  2.2714 +  also have "...=xt" using s by auto
  2.2715 +  finally have h2: "snd (SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)=xt" by auto
  2.2716 +  from h1 h2 have "(SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) = x" using xst_def by auto
  2.2717 +
  2.2718 +  moreover have "finite I & (I <= S <*> T)" using s t I_def by auto 
  2.2719 +  moreover have "!i:I. 0 <= u i" using s t I_def u_def by (simp add: mult_nonneg_nonneg)
  2.2720 +  moreover have "setsum u I = 1" using u_def I_def setsum_cartesian_product[of "(% x y. (su x)*(tu y))"] 
  2.2721 +     s t setsum_product[of su sI tu tI] by (auto simp add: split_def)
  2.2722 +  ultimately have "x : convex hull (S <*> T)" 
  2.2723 +     apply (subst convex_hull_explicit[of "S <*> T"]) apply rule
  2.2724 +     apply (rule_tac x="I" in exI) apply (rule_tac x="u" in exI)
  2.2725 +     using I_def u_def by auto
  2.2726 +}
  2.2727 +hence "convex hull (S <*> T) >= (convex hull S) <*> (convex hull T)" by auto
  2.2728 +moreover have "(convex hull S) <*> (convex hull T) : convex" 
  2.2729 +   unfolding mem_def by (simp add: convex_direct_sum convex_convex_hull)
  2.2730 +ultimately show ?thesis 
  2.2731 +   using hull_minimal[of "S <*> T" "(convex hull S) <*> (convex hull T)" "convex"] 
  2.2732 +         hull_subset[of S convex] hull_subset[of T convex] by auto
  2.2733 +qed
  2.2734 +
  2.2735 +lemma rel_interior_direct_sum:
  2.2736 +fixes S :: "('n::euclidean_space) set"
  2.2737 +fixes T :: "('m::euclidean_space) set"
  2.2738 +assumes "convex S" "convex T"
  2.2739 +shows "rel_interior (S <*> T) = rel_interior S <*> rel_interior T"
  2.2740 +proof-
  2.2741 +{ assume "S={}" hence ?thesis apply auto using rel_interior_empty by auto }
  2.2742 +moreover
  2.2743 +{ assume "T={}" hence ?thesis apply auto using rel_interior_empty by auto }
  2.2744 +moreover {
  2.2745 +assume "S ~={}" "T ~={}"
  2.2746 +hence ri: "rel_interior S ~= {}" "rel_interior T ~= {}" using rel_interior_convex_nonempty assms by auto
  2.2747 +hence "fst -` rel_interior S ~= {}" using fst_vimage_eq_Times[of "rel_interior S"] by auto
  2.2748 +hence "rel_interior ((fst :: 'n * 'm => 'n) -` S) = fst -` rel_interior S"
  2.2749 +  using fst_linear `convex S` rel_interior_convex_linear_preimage[of fst S] by auto 
  2.2750 +hence s: "rel_interior (S <*> (UNIV :: 'm set)) = rel_interior S <*> UNIV" by (simp add: fst_vimage_eq_Times)
  2.2751 +from ri have "snd -` rel_interior T ~= {}" using snd_vimage_eq_Times[of "rel_interior T"] by auto
  2.2752 +hence "rel_interior ((snd :: 'n * 'm => 'm) -` T) = snd -` rel_interior T"
  2.2753 +  using snd_linear `convex T` rel_interior_convex_linear_preimage[of snd T] by auto 
  2.2754 +hence t: "rel_interior ((UNIV :: 'n set) <*> T) = UNIV <*> rel_interior T" by (simp add: snd_vimage_eq_Times)
  2.2755 +from s t have *: "rel_interior (S <*> (UNIV :: 'm set)) Int rel_interior ((UNIV :: 'n set) <*> T) 
  2.2756 +  = rel_interior S <*> rel_interior T" by auto
  2.2757 +have "(S <*> T) = (S <*> (UNIV :: 'm set)) Int ((UNIV :: 'n set) <*> T)" by auto
  2.2758 +hence "rel_interior (S <*> T) = rel_interior ((S <*> (UNIV :: 'm set)) Int ((UNIV :: 'n set) <*> T))" by auto
  2.2759 +also have "...=rel_interior (S <*> (UNIV :: 'm set)) Int rel_interior ((UNIV :: 'n set) <*> T)" 
  2.2760 +   apply (subst convex_rel_interior_inter_two[of "S <*> (UNIV :: 'm set)" "(UNIV :: 'n set) <*> T"]) 
  2.2761 +   using * ri assms convex_direct_sum by auto
  2.2762 +finally have ?thesis using * by auto
  2.2763 +}
  2.2764 +ultimately show ?thesis by blast
  2.2765 +qed
  2.2766 +
  2.2767 +lemma rel_interior_scaleR: 
  2.2768 +fixes S :: "('n::euclidean_space) set"
  2.2769 +assumes "c ~= 0"
  2.2770 +shows "(op *\<^sub>R c) ` (rel_interior S) = rel_interior ((op *\<^sub>R c) ` S)"
  2.2771 +using rel_interior_injective_linear_image[of "(op *\<^sub>R c)" S]
  2.2772 +      linear_conv_bounded_linear[of "op *\<^sub>R c"] linear_scaleR injective_scaleR[of c] assms by auto
  2.2773 +
  2.2774 +lemma rel_interior_convex_scaleR: 
  2.2775 +fixes S :: "('n::euclidean_space) set"
  2.2776 +assumes "convex S"
  2.2777 +shows "(op *\<^sub>R c) ` (rel_interior S) = rel_interior ((op *\<^sub>R c) ` S)"
  2.2778 +by (metis assms linear_scaleR rel_interior_convex_linear_image)
  2.2779 +
  2.2780 +lemma convex_rel_open_scaleR: 
  2.2781 +fixes S :: "('n::euclidean_space) set"
  2.2782 +assumes "convex S" "rel_open S"
  2.2783 +shows "convex ((op *\<^sub>R c) ` S) & rel_open ((op *\<^sub>R c) ` S)"
  2.2784 +by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)
  2.2785 +
  2.2786 +
  2.2787 +lemma convex_rel_open_finite_inter: 
  2.2788 +assumes "!S : I. (convex (S :: ('n::euclidean_space) set) & rel_open S)"
  2.2789 +assumes "finite I"
  2.2790 +shows "convex (Inter I) & rel_open (Inter I)"
  2.2791 +proof-
  2.2792 +{ assume "Inter {rel_interior S |S. S : I} = {}"
  2.2793 +  hence "Inter I = {}" using assms unfolding rel_open_def by auto
  2.2794 +  hence ?thesis unfolding rel_open_def using rel_interior_empty by auto
  2.2795 +}
  2.2796 +moreover
  2.2797 +{ assume "Inter {rel_interior S |S. S : I} ~= {}"
  2.2798 +  hence "rel_open (Inter I)" using assms unfolding rel_open_def
  2.2799 +    using convex_rel_interior_finite_inter[of I] by auto
  2.2800 +  hence ?thesis using convex_Inter assms by auto
  2.2801 +} ultimately show ?thesis by auto
  2.2802 +qed
  2.2803 +
  2.2804 +lemma convex_rel_open_linear_image:
  2.2805 +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
  2.2806 +assumes "linear f"
  2.2807 +assumes "convex S" "rel_open S"
  2.2808 +shows "convex (f ` S) & rel_open (f ` S)"
  2.2809 +by (metis assms convex_linear_image rel_interior_convex_linear_image 
  2.2810 +   linear_conv_bounded_linear rel_open_def)
  2.2811 +
  2.2812 +lemma convex_rel_open_linear_preimage:
  2.2813 +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
  2.2814 +assumes "linear f"
  2.2815 +assumes "convex S" "rel_open S"
  2.2816 +shows "convex (f -` S) & rel_open (f -` S)" 
  2.2817 +proof-
  2.2818 +{ assume "f -` (rel_interior S) = {}"
  2.2819 +  hence "f -` S = {}" using assms unfolding rel_open_def by auto
  2.2820 +  hence ?thesis unfolding rel_open_def using rel_interior_empty by auto
  2.2821 +}
  2.2822 +moreover
  2.2823 +{ assume "f -` (rel_interior S) ~= {}"
  2.2824 +  hence "rel_open (f -` S)" using assms unfolding rel_open_def
  2.2825 +    using rel_interior_convex_linear_preimage[of f S] by auto
  2.2826 +  hence ?thesis using convex_linear_preimage assms linear_conv_bounded_linear by auto
  2.2827 +} ultimately show ?thesis by auto
  2.2828 +qed
  2.2829 +
  2.2830 +lemma rel_interior_projection:
  2.2831 +fixes S :: "('m::euclidean_space*'n::euclidean_space) set"
  2.2832 +fixes f :: "'m::euclidean_space => ('n::euclidean_space) set"
  2.2833 +assumes "convex S"
  2.2834 +assumes "f = (%y. {z. (y,z) : S})"
  2.2835 +shows "(y,z) : rel_interior S <-> (y : rel_interior {y. (f y ~= {})} & z : rel_interior (f y))"
  2.2836 +proof-
  2.2837 +{ fix y assume "y : {y. (f y ~= {})}" from this obtain z where "(y,z) : S" using assms by auto
  2.2838 +  hence "EX x. x : S & y = fst x" apply (rule_tac x="(y,z)" in exI) by auto
  2.2839 +  from this obtain x where "x : S & y = fst x" by blast
  2.2840 +  hence "y : fst ` S" unfolding image_def by auto
  2.2841 +}
  2.2842 +hence "fst ` S = {y. (f y ~= {})}" unfolding fst_def using assms by auto
  2.2843 +hence h1: "fst ` rel_interior S = rel_interior {y. (f y ~= {})}"
  2.2844 +   using rel_interior_convex_linear_image[of fst S] assms fst_linear by auto
  2.2845 +{ fix y assume "y : rel_interior {y. (f y ~= {})}"
  2.2846 +  hence "y : fst ` rel_interior S" using h1 by auto
  2.2847 +  hence *: "rel_interior S Int fst -` {y} ~= {}" by auto
  2.2848 +  moreover have aff: "affine (fst -` {y})" unfolding affine_alt by (simp add: algebra_simps)
  2.2849 +  ultimately have **: "rel_interior (S Int fst -` {y}) = rel_interior S Int fst -` {y}"
  2.2850 +    using convex_affine_rel_interior_inter[of S "fst -` {y}"] assms by auto
  2.2851 +  have conv: "convex (S Int fst -` {y})" using convex_Int assms aff affine_imp_convex by auto
  2.2852 +  { fix x assume "x : f y"
  2.2853 +    hence "(y,x) : S Int (fst -` {y})" using assms by auto
  2.2854 +    moreover have "x = snd (y,x)" by auto
  2.2855 +    ultimately have "x : snd ` (S Int fst -` {y})" by blast
  2.2856 +  }
  2.2857 +  hence "snd ` (S Int fst -` {y}) = f y" using assms by auto
  2.2858 +  hence ***: "rel_interior (f y) = snd ` rel_interior (S Int fst -` {y})"
  2.2859 +    using rel_interior_convex_linear_image[of snd "S Int fst -` {y}"] snd_linear conv by auto 
  2.2860 +  { fix z assume "z : rel_interior (f y)"
  2.2861 +    hence "z : snd ` rel_interior (S Int fst -` {y})" using *** by auto
  2.2862 +    moreover have "{y} = fst ` rel_interior (S Int fst -` {y})" using * ** rel_interior_subset by auto   
  2.2863 +    ultimately have "(y,z) : rel_interior (S Int fst -` {y})" by force
  2.2864 +    hence "(y,z) : rel_interior S" using ** by auto
  2.2865 +  }
  2.2866 +  moreover
  2.2867 +  { fix z assume "(y,z) : rel_interior S"
  2.2868 +    hence "(y,z) : rel_interior (S Int fst -` {y})" using ** by auto
  2.2869 +    hence "z : snd ` rel_interior (S Int fst -` {y})" by (metis Range_iff snd_eq_Range) 
  2.2870 +    hence "z : rel_interior (f y)" using *** by auto
  2.2871 +  }
  2.2872 +  ultimately have "!!z. (y,z) : rel_interior S <-> z : rel_interior (f y)" by auto
  2.2873 +} 
  2.2874 +hence h2: "!!y z. y : rel_interior {t. f t ~= {}} ==> ((y, z) : rel_interior S) = (z : rel_interior (f y))"
  2.2875 +  by auto
  2.2876 +{ fix y z assume asm: "(y, z) : rel_interior S"
  2.2877 +  hence "y : fst ` rel_interior S" by (metis Domain_iff fst_eq_Domain)
  2.2878 +  hence "y : rel_interior {t. f t ~= {}}" using h1 by auto
  2.2879 +  hence "y : rel_interior {t. f t ~= {}} & (z : rel_interior (f y))" using h2 asm by auto
  2.2880 +} from this show ?thesis using h2 by blast
  2.2881 +qed
  2.2882 +
  2.2883 +subsection{* Relative interior of convex cone *}
  2.2884 +
  2.2885 +lemma cone_rel_interior:
  2.2886 +fixes S :: "('m::euclidean_space) set"
  2.2887 +assumes "cone S"
  2.2888 +shows "cone ({0} Un (rel_interior S))"
  2.2889 +proof-
  2.2890 +{ assume "S = {}" hence ?thesis by (simp add: rel_interior_empty cone_0) }
  2.2891 +moreover
  2.2892 +{ assume "S ~= {}" hence *: "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto
  2.2893 +  hence *: "0:({0} Un (rel_interior S)) &
  2.2894 +           (!c. c>0 --> op *\<^sub>R c ` ({0} Un rel_interior S) = ({0} Un rel_interior S))"
  2.2895 +           by (auto simp add: rel_interior_scaleR)
  2.2896 +  hence ?thesis using cone_iff[of "{0} Un rel_interior S"] by auto
  2.2897 +}
  2.2898 +ultimately show ?thesis by blast
  2.2899 +qed
  2.2900 +
  2.2901 +lemma rel_interior_convex_cone_aux:
  2.2902 +fixes S :: "('m::euclidean_space) set"
  2.2903 +assumes "convex S"
  2.2904 +shows "(c,x) : rel_interior (cone hull ({(1 :: real)} <*> S)) <-> 
  2.2905 +       c>0 & x : ((op *\<^sub>R c) ` (rel_interior S))"
  2.2906 +proof-
  2.2907 +{ assume "S={}" hence ?thesis by (simp add: rel_interior_empty cone_hull_empty) } 
  2.2908 +moreover
  2.2909 +{ assume "S ~= {}" from this obtain s where "s : S" by auto
  2.2910 +have conv: "convex ({(1 :: real)} <*> S)" using convex_direct_sum[of "{(1 :: real)}" S] 
  2.2911 +   assms convex_singleton[of "1 :: real"] by auto
  2.2912 +def f == "(%y. {z. (y,z) : cone hull ({(1 :: real)} <*> S)})"
  2.2913 +hence *: "(c, x) : rel_interior (cone hull ({(1 :: real)} <*> S)) =
  2.2914 +      (c : rel_interior {y. f y ~= {}} & x : rel_interior (f c))"
  2.2915 +  apply (subst rel_interior_projection[of "cone hull ({(1 :: real)} <*> S)" f c x])
  2.2916 +  using convex_cone_hull[of "{(1 :: real)} <*> S"] conv by auto
  2.2917 +{ fix y assume "(y :: real)>=0"
  2.2918 +  hence "y *\<^sub>R (1,s) : cone hull ({(1 :: real)} <*> S)"
  2.2919 +     using cone_hull_expl[of "{(1 :: real)} <*> S"] `s:S` by auto
  2.2920 +  hence "f y ~= {}" using f_def by auto
  2.2921 +}
  2.2922 +hence "{y. f y ~= {}} = {0..}" using f_def cone_hull_expl[of "{(1 :: real)} <*> S"] by auto
  2.2923 +hence **: "rel_interior {y. f y ~= {}} = {0<..}" using rel_interior_real_semiline by auto
  2.2924 +{ fix c assume "c>(0 :: real)"
  2.2925 +  hence "f c = (op *\<^sub>R c ` S)" using f_def cone_hull_expl[of "{(1 :: real)} <*> S"] by auto
  2.2926 +  hence "rel_interior (f c)= (op *\<^sub>R c ` rel_interior S)"
  2.2927 +     using rel_interior_convex_scaleR[of S c] assms by auto
  2.2928 +}
  2.2929 +hence ?thesis using * ** by auto
  2.2930 +} ultimately show ?thesis by blast
  2.2931 +qed
  2.2932 +
  2.2933 +
  2.2934 +lemma rel_interior_convex_cone:
  2.2935 +fixes S :: "('m::euclidean_space) set"
  2.2936 +assumes "convex S"
  2.2937 +shows "rel_interior (cone hull ({(1 :: real)} <*> S)) = 
  2.2938 +       {(c,c *\<^sub>R x) |c x. c>0 & x : (rel_interior S)}"
  2.2939 +(is "?lhs=?rhs")
  2.2940 +proof-
  2.2941 +{ fix z assume "z:?lhs" 
  2.2942 +  have *: "z=(fst z,snd z)" by auto 
  2.2943 +  have "z:?rhs" using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms `z:?lhs` apply auto
  2.2944 +     apply (rule_tac x="fst z" in exI) apply (rule_tac x="x" in exI) using * by auto
  2.2945 +}
  2.2946 +moreover
  2.2947 +{ fix z assume "z:?rhs" hence "z:?lhs" 
  2.2948 +  using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms by auto
  2.2949 +}
  2.2950 +ultimately show ?thesis by blast
  2.2951 +qed
  2.2952 +
  2.2953 +lemma convex_hull_finite_union:
  2.2954 +assumes "finite I"
  2.2955 +assumes "!i:I. (convex (S i) & (S i) ~= {})"
  2.2956 +shows "convex hull (Union (S ` I)) = 
  2.2957 +       {setsum (%i. c i *\<^sub>R s i) I |c s. (!i:I. c i >= 0) & (setsum c I = 1) & (!i:I. s i : S i)}"
  2.2958 +  (is "?lhs = ?rhs")
  2.2959 +proof-
  2.2960 +{ fix x assume "x : ?rhs" 
  2.2961 +  from this obtain c s 
  2.2962 +    where *: "setsum (%i. c i *\<^sub>R s i) I=x" "(setsum c I = 1)"
  2.2963 +     "(!i:I. c i >= 0) & (!i:I. s i : S i)" by auto
  2.2964 +  hence "!i:I. s i : convex hull (Union (S ` I))" using hull_subset[of "Union (S ` I)" convex] by auto
  2.2965 +  hence "x : ?lhs" unfolding *(1)[THEN sym]
  2.2966 +     apply (subst convex_setsum[of I "convex hull Union (S ` I)" c s])
  2.2967 +     using * assms convex_convex_hull by auto
  2.2968 +} hence "?lhs >= ?rhs" by auto
  2.2969 +
  2.2970 +{ fix i assume "i:I"
  2.2971 +    from this assms have "EX p. p : S i" by auto
  2.2972 +} 
  2.2973 +from this obtain p where p_def: "!i:I. p i : S i" by metis
  2.2974 +
  2.2975 +{ fix i assume "i:I"
  2.2976 +  { fix x assume "x : S i"
  2.2977 +    def c == "(%j. if (j=i) then (1::real) else 0)"
  2.2978 +    hence *: "setsum c I = 1" using `finite I` `i:I` setsum_delta[of I i "(%(j::'a). (1::real))"] by auto
  2.2979 +    def s == "(%j. if (j=i) then x else p j)"
  2.2980 +    hence "!j. c j *\<^sub>R s j = (if (j=i) then x else 0)" using c_def by (auto simp add: algebra_simps)
  2.2981 +    hence "x = setsum (%i. c i *\<^sub>R s i) I"
  2.2982 +       using s_def c_def `finite I` `i:I` setsum_delta[of I i "(%(j::'a). x)"] by auto 
  2.2983 +    hence "x : ?rhs" apply auto
  2.2984 +      apply (rule_tac x="c" in exI) 
  2.2985 +      apply (rule_tac x="s" in exI) using * c_def s_def p_def `x : S i` by auto 
  2.2986 +  } hence "?rhs >= S i" by auto
  2.2987 +} hence *: "?rhs >= Union (S ` I)" by auto
  2.2988 +
  2.2989 +{ fix u v assume uv: "(u :: real)>=0 & v>=0 & u+v=1"
  2.2990 +  fix x y assume xy: "(x : ?rhs) & (y : ?rhs)"
  2.2991 +  from xy obtain c s where xc: "x=setsum (%i. c i *\<^sub>R s i) I &
  2.2992 +     (!i:I. c i >= 0) & (setsum c I = 1) & (!i:I. s i : S i)" by auto
  2.2993 +  from xy obtain d t where yc: "y=setsum (%i. d i *\<^sub>R t i) I &
  2.2994 +     (!i:I. d i >= 0) & (setsum d I = 1) & (!i:I. t i : S i)" by auto
  2.2995 +  def e == "(%i. u * (c i)+v * (d i))"
  2.2996 +  have ge0: "!i:I. e i >= 0"  using e_def xc yc uv by (simp add: mult_nonneg_nonneg)
  2.2997 +  have "setsum (%i. u * c i) I = u * setsum c I" by (simp add: setsum_right_distrib)
  2.2998 +  moreover have "setsum (%i. v * d i) I = v * setsum d I" by (simp add: setsum_right_distrib)
  2.2999 +  ultimately have sum1: "setsum e I = 1" using e_def xc yc uv by (simp add: setsum_addf)
  2.3000 +  def q == "(%i. if (e i = 0) then (p i) 
  2.3001 +                 else (u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i))"
  2.3002 +  { fix i assume "i:I"
  2.3003 +    { assume "e i = 0" hence "q i : S i" using `i:I` p_def q_def by auto }
  2.3004 +    moreover
  2.3005 +    { assume "e i ~= 0" 
  2.3006 +      hence "q i : S i" using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"] 
  2.3007 +         mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"]
  2.3008 +         assms q_def e_def `i:I` `e i ~= 0` xc yc uv by auto
  2.3009 +    } ultimately have "q i : S i" by auto
  2.3010 +  } hence qs: "!i:I. q i : S i" by auto
  2.3011 +  { fix i assume "i:I"
  2.3012 +    { assume "e i = 0" 
  2.3013 +      have ge: "u * (c i) >= 0 & v * (d i) >= 0" using xc yc uv `i:I` by (simp add: mult_nonneg_nonneg)
  2.3014 +      moreover hence "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp 
  2.3015 +      ultimately have "u * (c i) = 0 & v * (d i) = 0" by auto
  2.3016 +      hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)"
  2.3017 +         using `e i = 0` by auto
  2.3018 +    }
  2.3019 +    moreover
  2.3020 +    { assume "e i ~= 0"
  2.3021 +      hence "(u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i) = q i"
  2.3022 +         using q_def by auto
  2.3023 +      hence "e i *\<^sub>R ((u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i))
  2.3024 +             = (e i) *\<^sub>R (q i)" by auto
  2.3025 +      hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)"
  2.3026 +         using `e i ~= 0` by (simp add: algebra_simps)
  2.3027 +    } ultimately have 
  2.3028 +      "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" by blast
  2.3029 +  } hence *: "!i:I.
  2.3030 +    (u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" by auto
  2.3031 +  have "u *\<^sub>R x + v *\<^sub>R y =
  2.3032 +       setsum (%i. (u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i)) I"
  2.3033 +          using xc yc by (simp add: algebra_simps scaleR_right.setsum setsum_addf)
  2.3034 +  also have "...=setsum (%i. (e i) *\<^sub>R (q i)) I" using * by auto
  2.3035 +  finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (%i. (e i) *\<^sub>R (q i)) I" by auto
  2.3036 +  hence "u *\<^sub>R x + v *\<^sub>R y : ?rhs" using ge0 sum1 qs by auto
  2.3037 +} hence "convex ?rhs" unfolding convex_def by auto
  2.3038 +hence "?rhs : convex" unfolding mem_def by auto
  2.3039 +from this show ?thesis using `?lhs >= ?rhs` * 
  2.3040 +   hull_minimal[of "Union (S ` I)" "?rhs" "convex"] by blast
  2.3041 +qed
  2.3042 +
  2.3043 +lemma convex_hull_union_two:
  2.3044 +fixes S T :: "('m::euclidean_space) set"
  2.3045 +assumes "convex S" "S ~= {}" "convex T" "T ~= {}"
  2.3046 +shows "convex hull (S Un T) = {u *\<^sub>R s + v *\<^sub>R t |u v s t. u>=0 & v>=0 & u+v=1 & s:S & t:T}"
  2.3047 +  (is "?lhs = ?rhs")
  2.3048 +proof-
  2.3049 +def I == "{(1::nat),2}"
  2.3050 +def s == "(%i. (if i=(1::nat) then S else T))"
  2.3051 +have "Union (s ` I) = S Un T" using s_def I_def by auto
  2.3052 +hence "convex hull (Union (s ` I)) = convex hull (S Un T)" by auto
  2.3053 +moreover have "convex hull Union (s ` I) =
  2.3054 +    {SUM i:I. c i *\<^sub>R sa i |c sa. (ALL i:I. 0 <= c i) & setsum c I = 1 & (ALL i:I. sa i : s i)}"
  2.3055 +    apply (subst convex_hull_finite_union[of I s]) using assms s_def I_def by auto
  2.3056 +moreover have 
  2.3057 +  "{SUM i:I. c i *\<^sub>R sa i |c sa. (ALL i:I. 0 <= c i) & setsum c I = 1 & (ALL i:I. sa i : s i)} <=
  2.3058 +  ?rhs"
  2.3059 +  using s_def I_def by auto
  2.3060 +ultimately have "?lhs<=?rhs" by auto 
  2.3061 +{ fix x assume "x : ?rhs" 
  2.3062 +  from this obtain u v s t 
  2.3063 +    where *: "x=u *\<^sub>R s + v *\<^sub>R t & u>=0 & v>=0 & u+v=1 & s:S & t:T" by auto
  2.3064 +  hence "x : convex hull {s,t}" using convex_hull_2[of s t] by auto
  2.3065 +  hence "x : convex hull (S Un T)" using * hull_mono[of "{s, t}" "S Un T"] by auto
  2.3066 +} hence "?lhs >= ?rhs" by blast
  2.3067 +from this show ?thesis using `?lhs<=?rhs` by auto
  2.3068 +qed
  2.3069 +
  2.3070  end
     3.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Nov 05 09:07:14 2010 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Nov 05 14:17:18 2010 +0100
     3.3 @@ -1065,10 +1065,16 @@
     3.4  
     3.5  text {* Individual closure properties. *}
     3.6  
     3.7 +lemma span_span: "span (span A) = span A"
     3.8 +  unfolding span_def hull_hull ..
     3.9 +
    3.10  lemma (in real_vector) span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses(1))
    3.11  
    3.12  lemma (in real_vector) span_0: "0 \<in> span S" by (metis subspace_span subspace_0)
    3.13  
    3.14 +lemma span_inc: "S \<subseteq> span S"
    3.15 +  by (metis subset_eq span_superset)
    3.16 +
    3.17  lemma (in real_vector) dependent_0: assumes "0\<in>A" shows "dependent A"
    3.18    unfolding dependent_def apply(rule_tac x=0 in bexI)
    3.19    using assms span_0 by auto
    3.20 @@ -1485,12 +1491,6 @@
    3.21  lemma mem_delete: "x \<in> (A - {a}) \<longleftrightarrow> x \<noteq> a \<and> x \<in> A"
    3.22    by blast
    3.23  
    3.24 -lemma span_span: "span (span A) = span A"
    3.25 -  unfolding span_def hull_hull ..
    3.26 -
    3.27 -lemma span_inc: "S \<subseteq> span S"
    3.28 -  by (metis subset_eq span_superset)
    3.29 -
    3.30  lemma spanning_subset_independent:
    3.31    assumes BA: "B \<subseteq> A" and iA: "independent A"
    3.32    and AsB: "A \<subseteq> span B"