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"