# HG changeset patch # User hoelzl # Date 1288963038 -3600 # Node ID 0e5d48096f58fad397f4250ecd773dd46534d058 # Parent 6fb991dc074b974abce1e6b482707f740a902b03 Extend convex analysis by Bogdan Grechuk diff -r 6fb991dc074b -r 0e5d48096f58 CONTRIBUTORS --- a/CONTRIBUTORS Fri Nov 05 09:07:14 2010 +0100 +++ b/CONTRIBUTORS Fri Nov 05 14:17:18 2010 +0100 @@ -21,6 +21,9 @@ * July 2010: Florian Haftmann, TUM Reworking and extension of the Imperative HOL framework. +* October 2010: Bogdan Grechuck, University of Edinburgh + Extended convex analysis in Multivariate Analysis + Contributions to Isabelle2009-2 -------------------------------------- diff -r 6fb991dc074b -r 0e5d48096f58 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 05 09:07:14 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 05 14:17:18 2010 +0100 @@ -13,9 +13,307 @@ (* To be moved elsewhere *) (* ------------------------------------------------------------------------- *) +lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)" + by (metis linear_conv_bounded_linear scaleR.bounded_linear_right) + +lemma injective_scaleR: +assumes "(c :: real) ~= 0" +shows "inj (%(x :: 'n::euclidean_space). scaleR c x)" +by (metis assms datatype_injI injI real_vector.scale_cancel_left) + +lemma linear_add_cmul: +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" +assumes "linear f" +shows "f(a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x + b *\<^sub>R f y" +using linear_add[of f] linear_cmul[of f] assms by (simp) + +lemma mem_convex_2: + assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v=1" + shows "(u *\<^sub>R x + v *\<^sub>R y) : S" + using assms convex_def[of S] by auto + +lemma mem_convex_alt: + assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v>0" + shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) : S" +apply (subst mem_convex_2) +using assms apply (auto simp add: algebra_simps zero_le_divide_iff) +using add_divide_distrib[of u v "u+v"] by auto + +lemma card_ge1: assumes "d ~= {}" "finite d" shows "card d >= 1" +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) + +lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)" +by (blast dest: inj_onD) + +lemma independent_injective_on_span_image: + assumes iS: "independent (S::(_::euclidean_space) set)" + and lf: "linear f" and fi: "inj_on f (span S)" + shows "independent (f ` S)" +proof- + {fix a assume a: "a : S" "f a : span (f ` S - {f a})" + have eq: "f ` S - {f a} = f ` (S - {a})" using fi a span_inc + by (auto simp add: inj_on_def) + from a have "f a : f ` span (S -{a})" + unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast + moreover have "span (S -{a}) <= span S" using span_mono[of "S-{a}" S] by auto + ultimately have "a : span (S -{a})" using fi a span_inc by (auto simp add: inj_on_def) + with a(1) iS have False by (simp add: dependent_def) } + then show ?thesis unfolding dependent_def by blast +qed + +lemma dim_image_eq: +fixes f :: "'n::euclidean_space => 'm::euclidean_space" +assumes lf: "linear f" and fi: "inj_on f (span S)" +shows "dim (f ` S) = dim (S:: ('n::euclidean_space) set)" +proof- +obtain B where B_def: "B<=S & independent B & S <= span B & card B = dim S" + using basis_exists[of S] by auto +hence "span S = span B" using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto +hence "independent (f ` B)" using independent_injective_on_span_image[of B f] B_def assms by auto +moreover have "card (f ` B) = card B" using assms card_image[of f B] subset_inj_on[of f "span S" B] + B_def span_inc by auto +moreover have "(f ` B) <= (f ` S)" using B_def by auto +ultimately have "dim (f ` S) >= dim S" + using independent_card_le_dim[of "f ` B" "f ` S"] B_def by auto +from this show ?thesis using dim_image_le[of f S] assms by auto +qed + +lemma linear_injective_on_subspace_0: +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" +assumes lf: "linear f" and "subspace S" + shows "inj_on f S <-> (!x : S. f x = 0 --> x = 0)" +proof- + have "inj_on f S <-> (!x : S. !y : S. f x = f y --> x = y)" by (simp add: inj_on_def) + also have "... <-> (!x : S. !y : S. f x - f y = 0 --> x - y = 0)" by simp + also have "... <-> (!x : S. !y : S. f (x - y) = 0 --> x - y = 0)" + by (simp add: linear_sub[OF lf]) + also have "... <-> (! x : S. f x = 0 --> x = 0)" + using `subspace S` subspace_def[of S] subspace_sub[of S] by auto + finally show ?thesis . +qed + +lemma subspace_Inter: "(!s : f. subspace s) ==> subspace (Inter f)" + unfolding subspace_def by auto + +lemma span_eq[simp]: "(span s = s) <-> subspace s" +proof- + { fix f assume "f <= subspace" + hence "subspace (Inter f)" using subspace_Inter[of f] unfolding subset_eq mem_def by auto } + thus ?thesis using hull_eq[unfolded mem_def, of subspace s] span_def by auto +qed + +lemma basis_inj_on: "d \ {.. inj_on (basis :: nat => 'n::euclidean_space) d" + by(auto simp add: inj_on_def euclidean_eq[where 'a='n]) + +lemma finite_substdbasis: "finite {basis i ::'n::euclidean_space |i. i : (d:: nat set)}" (is "finite ?S") +proof- + have eq: "?S = basis ` d" by blast + show ?thesis unfolding eq apply(rule finite_subset[OF _ range_basis_finite]) by auto +qed + +lemma card_substdbasis: assumes "d \ {..{..R basis i) d = (x::'a::euclidean_space) + <-> (!i f i = x$$i) & (i ~: d --> x $$ i = 0))" +proof- have *:"\x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto + have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp + have ***:"\i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\x\d. if x = i then f x else 0)" + unfolding euclidean_component.setsum euclidean_scaleR basis_component * + apply(rule setsum_cong2) using assms by auto + show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto +qed + +lemma independent_substdbasis: assumes "d\{..R x" + hence "y : cball 0 e" using cball_def dist_norm[of 0 y] assms by auto + moreover have "x = (norm x/e) *\<^sub>R y" using y_def assms by simp + moreover hence "x = (norm x/e) *\<^sub>R y" by auto + ultimately have "x : span (cball 0 e)" + using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto +} hence "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto +from this show ?thesis using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp add: dim_UNIV) +qed + +lemma indep_card_eq_dim_span: +fixes B :: "('n::euclidean_space) set" +assumes "independent B" +shows "finite B & card B = dim (span B)" + using assms basis_card_eq_dim[of B "span B"] span_inc by auto + +lemma setsum_not_0: "setsum f A ~= 0 ==> EX a:A. f a ~= 0" + apply(rule ccontr) by auto + +lemma translate_inj_on: +fixes A :: "('n::euclidean_space) set" +shows "inj_on (%x. a+x) A" unfolding inj_on_def by auto + +lemma translation_assoc: + fixes a b :: "'a::ab_group_add" + shows "(\x. b+x) ` ((\x. a+x) ` S) = (\x. (a+b)+x) ` S" by auto + +lemma translation_invert: + fixes a :: "'a::ab_group_add" + assumes "(\x. a+x) ` A = (\x. a+x) ` B" + shows "A=B" +proof- + have "(%x. -a+x) ` ((%x. a+x) ` A) = (%x. -a+x) ` ((%x. a+x) ` B)" using assms by auto + from this show ?thesis using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto +qed + +lemma translation_galois: + fixes a :: "'a::ab_group_add" + shows "T=((\x. a+x) ` S) <-> S=((\x. (-a)+x) ` T)" + using translation_assoc[of "-a" a S] apply auto + using translation_assoc[of a "-a" T] by auto + +lemma translation_inverse_subset: + assumes "((%x. -a+x) ` V) <= (S :: 'n::ab_group_add set)" + shows "V <= ((%x. a+x) ` S)" +proof- +{ fix x assume "x:V" hence "x-a : S" using assms by auto + hence "x : {a + v |v. v : S}" apply auto apply (rule exI[of _ "x-a"]) apply simp done + hence "x : ((%x. a+x) ` S)" by auto } + from this show ?thesis by auto +qed + lemma basis_0[simp]:"(basis i::'a::euclidean_space) = 0 \ i\DIM('a)" using norm_basis[of i, where 'a='a] unfolding norm_eq_zero[where 'a='a,THEN sym] by auto +lemma basis_to_basis_subspace_isomorphism: + assumes s: "subspace (S:: ('n::euclidean_space) set)" + and t: "subspace (T :: ('m::euclidean_space) set)" + and d: "dim S = dim T" + and B: "B <= S" "independent B" "S <= span B" "card B = dim S" + and C: "C <= T" "independent C" "T <= span C" "card C = dim T" + shows "EX f. linear f & f ` B = C & f ` S = T & inj_on f S" +proof- +(* Proof is a modified copy of the proof of similar lemma subspace_isomorphism +*) + from B independent_bound have fB: "finite B" by blast + from C independent_bound have fC: "finite C" by blast + from B(4) C(4) card_le_inj[of B C] d obtain f where + f: "f ` B \ C" "inj_on f B" using `finite B` `finite C` by auto + from linear_independent_extend[OF B(2)] obtain g where + g: "linear g" "\x\ B. g x = f x" by blast + from inj_on_iff_eq_card[OF fB, of f] f(2) + have "card (f ` B) = card B" by simp + with B(4) C(4) have ceq: "card (f ` B) = card C" using d + by simp + have "g ` B = f ` B" using g(2) + by (auto simp add: image_iff) + also have "\ = C" using card_subset_eq[OF fC f(1) ceq] . + finally have gBC: "g ` B = C" . + have gi: "inj_on g B" using f(2) g(2) + by (auto simp add: inj_on_def) + note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi] + {fix x y assume x: "x \ S" and y: "y \ S" and gxy:"g x = g y" + from B(3) x y have x': "x \ span B" and y': "y \ span B" by blast+ + from gxy have th0: "g (x - y) = 0" by (simp add: linear_sub[OF g(1)]) + have th1: "x - y \ span B" using x' y' by (metis span_sub) + have "x=y" using g0[OF th1 th0] by simp } + then have giS: "inj_on g S" + unfolding inj_on_def by blast + from span_subspace[OF B(1,3) s] + have "g ` S = span (g ` B)" by (simp add: span_linear_image[OF g(1)]) + also have "\ = span C" unfolding gBC .. + also have "\ = T" using span_subspace[OF C(1,3) t] . + finally have gS: "g ` S = T" . + from g(1) gS giS gBC show ?thesis by blast +qed + +lemma closure_linear_image: +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" +assumes "linear f" +shows "f ` (closure S) <= closure (f ` S)" +using image_closure_subset[of S f "closure (f ` S)"] assms linear_conv_bounded_linear[of f] +linear_continuous_on[of f "closure S"] closed_closure[of "f ` S"] closure_subset[of "f ` S"] by auto + +lemma closure_injective_linear_image: +fixes f :: "('n::euclidean_space) => ('n::euclidean_space)" +assumes "linear f" "inj f" +shows "f ` (closure S) = closure (f ` S)" +proof- +obtain f' where f'_def: "linear f' & f o f' = id & f' o f = id" + using assms linear_injective_isomorphism[of f] isomorphism_expand by auto +hence "f' ` closure (f ` S) <= closure (S)" + using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto +hence "f ` f' ` closure (f ` S) <= f ` closure (S)" by auto +hence "closure (f ` S) <= f ` closure (S)" using image_compose[of f f' "closure (f ` S)"] f'_def by auto +from this show ?thesis using closure_linear_image[of f S] assms by auto +qed + +lemma closure_direct_sum: +fixes S :: "('n::euclidean_space) set" +fixes T :: "('m::euclidean_space) set" +shows "closure (S <*> T) = closure S <*> closure T" +proof- +{ fix x assume "x : closure S <*> closure T" + from this obtain xs xt where xst_def: "xs : closure S & xt : closure T & (xs,xt) = x" by auto + { fix ee assume ee_def: "(ee :: real) > 0" + def e == "ee/2" hence e_def: "(e :: real)>0 & 2*e=ee" using ee_def by auto + from this obtain e where e_def: "(e :: real)>0 & 2*e=ee" by auto + obtain ys where ys_def: "ys : S & (dist ys xs < e)" + using e_def xst_def closure_approachable[of xs S] by auto + obtain yt where yt_def: "yt : T & (dist yt xt < e)" + using e_def xst_def closure_approachable[of xt T] by auto + from ys_def yt_def have "dist (ys,yt) (xs,xt) < sqrt (2*e^2)" + unfolding dist_norm apply (auto simp add: norm_Pair) + using mult_strict_mono'[of "norm (ys - xs)" e "norm (ys - xs)" e] e_def + mult_strict_mono'[of "norm (yt - xt)" e "norm (yt - xt)" e] by (simp add: power2_eq_square) + hence "((ys,yt) : S <*> T) & (dist (ys,yt) x < 2*e)" + using e_def sqrt_add_le_add_sqrt[of "e^2" "e^2"] xst_def ys_def yt_def by auto + hence "EX y: S <*> T. dist y x < ee" using e_def by auto + } hence "x : closure (S <*> T)" using closure_approachable[of x "S <*> T"] by auto +} +hence "closure (S <*> T) >= closure S <*> closure T" by auto +moreover have "closed (closure S <*> closure T)" using closed_Times by auto +ultimately show ?thesis using closure_minimal[of "S <*> T" "closure S <*> closure T"] + closure_subset[of S] closure_subset[of T] by auto +qed + +lemma closure_scaleR: +fixes S :: "('n::euclidean_space) set" +shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)" +proof- +{ assume "c ~= 0" hence ?thesis using closure_injective_linear_image[of "(op *\<^sub>R c)" S] + linear_scaleR injective_scaleR by auto +} +moreover +{ assume zero: "c=0 & S ~= {}" + hence "closure S ~= {}" using closure_subset by auto + hence "op *\<^sub>R c ` (closure S) = {0}" using zero by auto + moreover have "op *\<^sub>R 0 ` S = {0}" using zero by auto + ultimately have ?thesis using zero by auto +} +moreover +{ assume "S={}" hence ?thesis by auto } +ultimately show ?thesis by blast +qed + +lemma fst_linear: "linear fst" unfolding linear_def by (simp add: algebra_simps) + +lemma snd_linear: "linear snd" unfolding linear_def by (simp add: algebra_simps) + +lemma fst_snd_linear: "linear (%z. fst z + snd z)" unfolding linear_def by (simp add: algebra_simps) + lemma scaleR_2: fixes x :: "'a::real_vector" shows "scaleR 2 x = x + x" @@ -272,6 +570,30 @@ apply(rule_tac x=u in exI) by(auto intro!: exI) qed +lemma mem_affine: + assumes "affine S" "x : S" "y : S" "u+v=1" + shows "(u *\<^sub>R x + v *\<^sub>R y) : S" + using assms affine_def[of S] by auto + +lemma mem_affine_3: + assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1" + shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S" +proof- +have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}" + using affine_hull_3[of x y z] assms by auto +moreover have " affine hull {x, y, z} <= affine hull S" + using hull_mono[of "{x, y, z}" "S"] assms by auto +moreover have "affine hull S = S" + using assms affine_hull_eq[of S] by auto +ultimately show ?thesis by auto +qed + +lemma mem_affine_3_minus: + assumes "affine S" "x : S" "y : S" "z : S" + shows "x + v *\<^sub>R (y-z) : S" +using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps) + + subsection {* Some relations between affine hull and subspaces. *} lemma affine_hull_insert_subset_span: @@ -318,6 +640,163 @@ shows "affine hull s = {a + v | v. v \ span {x - a | x. x \ s - {a}}}" using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto +subsection{* Parallel Affine Sets *} + +definition affine_parallel :: "'a::real_vector set => 'a::real_vector set => bool" +where "affine_parallel S T = (? a. T = ((%x. a + x) ` S))" + +lemma affine_parallel_expl_aux: + fixes S T :: "'a::real_vector set" + assumes "!x. (x : S <-> (a+x) : T)" + shows "T = ((%x. a + x) ` S)" +proof- +{ fix x assume "x : T" hence "(-a)+x : S" using assms by auto + hence " x : ((%x. a + x) ` S)" using imageI[of "-a+x" S "(%x. a+x)"] by auto} +moreover have "T >= ((%x. a + x) ` S)" using assms by auto +ultimately show ?thesis by auto +qed + +lemma affine_parallel_expl: + "affine_parallel S T = (? a. !x. (x : S <-> (a+x) : T))" + unfolding affine_parallel_def using affine_parallel_expl_aux[of S _ T] by auto + +lemma affine_parallel_reflex: "affine_parallel S S" unfolding affine_parallel_def apply (rule exI[of _ "0"]) by auto + +lemma affine_parallel_commut: +assumes "affine_parallel A B" shows "affine_parallel B A" +proof- +from assms obtain a where "B=((%x. a + x) ` A)" unfolding affine_parallel_def by auto +from this show ?thesis using translation_galois[of B a A] unfolding affine_parallel_def by auto +qed + +lemma affine_parallel_assoc: +assumes "affine_parallel A B" "affine_parallel B C" +shows "affine_parallel A C" +proof- +from assms obtain ab where "B=((%x. ab + x) ` A)" unfolding affine_parallel_def by auto +moreover +from assms obtain bc where "C=((%x. bc + x) ` B)" unfolding affine_parallel_def by auto +ultimately show ?thesis using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto +qed + +lemma affine_translation_aux: + fixes a :: "'a::real_vector" + assumes "affine ((%x. a + x) ` S)" shows "affine S" +proof- +{ fix x y u v + assume xy: "x : S" "y : S" "(u :: real)+v=1" + hence "(a+x):((%x. a + x) ` S)" "(a+y):((%x. a + x) ` S)" by auto + hence h1: "u *\<^sub>R (a+x) + v *\<^sub>R (a+y) : ((%x. a + x) ` S)" using xy assms unfolding affine_def by auto + 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) + also have "...= a + (u *\<^sub>R x + v *\<^sub>R y)" using `u+v=1` by auto + ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) : ((%x. a + x) ` S)" using h1 by auto + hence "u *\<^sub>R x + v *\<^sub>R y : S" by auto +} from this show ?thesis unfolding affine_def by auto +qed + +lemma affine_translation: + fixes a :: "'a::real_vector" + shows "affine S <-> affine ((%x. a + x) ` S)" +proof- +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 +from this show ?thesis using affine_translation_aux by auto +qed + +lemma parallel_is_affine: +fixes S T :: "'a::real_vector set" +assumes "affine S" "affine_parallel S T" +shows "affine T" +proof- + from assms obtain a where "T=((%x. a + x) ` S)" unfolding affine_parallel_def by auto + from this show ?thesis using affine_translation assms by auto +qed + +lemma subspace_imp_affine: + fixes s :: "(_::euclidean_space) set" shows "subspace s \ affine s" + unfolding subspace_def affine_def by auto + +subsection{* Subspace Parallel to an Affine Set *} + +lemma subspace_affine: + fixes S :: "('n::euclidean_space) set" + shows "subspace S <-> (affine S & 0 : S)" +proof- +have h0: "subspace S ==> (affine S & 0 : S)" using subspace_imp_affine[of S] subspace_0 by auto +{ assume assm: "affine S & 0 : S" + { fix c :: real + fix x assume x_def: "x : S" + have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto + moreover have "(1-c) *\<^sub>R 0 + c *\<^sub>R x : S" using affine_alt[of S] assm x_def by auto + ultimately have "c *\<^sub>R x : S" by auto + } hence h1: "!c. !x : S. c *\<^sub>R x : S" by auto + { fix x y assume xy_def: "x : S" "y : S" + def u == "(1 :: real)/2" + have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" by auto + moreover have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" by (simp add: algebra_simps) + moreover have "(1-u) *\<^sub>R x + u *\<^sub>R y : S" using affine_alt[of S] assm xy_def by auto + ultimately have "(1/2) *\<^sub>R (x+y) : S" using u_def by auto + moreover have "(x+y) = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" by auto + ultimately have "(x+y) : S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto + } hence "!x : S. !y : S. (x+y) : S" by auto + hence "subspace S" using h1 assm unfolding subspace_def by auto +} from this show ?thesis using h0 by metis +qed + +lemma affine_diffs_subspace: + fixes S :: "('n::euclidean_space) set" + assumes "affine S" "a : S" + shows "subspace ((%x. (-a)+x) ` S)" +proof- +have "affine ((%x. (-a)+x) ` S)" using affine_translation assms by auto +moreover have "0 : ((%x. (-a)+x) ` S)" using assms exI[of "(%x. x:S & -a+x=0)" a] by auto +ultimately show ?thesis using subspace_affine by auto +qed + +lemma parallel_subspace_explicit: +fixes a :: "'n::euclidean_space" +assumes "affine S" "a : S" +assumes "L == {y. ? x : S. (-a)+x=y}" +shows "subspace L & affine_parallel S L" +proof- +have par: "affine_parallel S L" unfolding affine_parallel_def using assms by auto +hence "affine L" using assms parallel_is_affine by auto +moreover have "0 : L" using assms apply auto using exI[of "(%x. x:S & -a+x=0)" a] by auto +ultimately show ?thesis using subspace_affine par by auto +qed + +lemma parallel_subspace_aux: +fixes A B :: "('n::euclidean_space) set" +assumes "subspace A" "subspace B" "affine_parallel A B" +shows "A>=B" +proof- +from assms obtain a where a_def: "!x. (x : A <-> (a+x) : B)" using affine_parallel_expl[of A B] by auto +hence "-a : A" using assms subspace_0[of B] by auto +hence "a : A" using assms subspace_neg[of A "-a"] by auto +from this show ?thesis using assms a_def unfolding subspace_def by auto +qed + +lemma parallel_subspace: +fixes A B :: "('n::euclidean_space) set" +assumes "subspace A" "subspace B" "affine_parallel A B" +shows "A=B" +proof- +have "A>=B" using assms parallel_subspace_aux by auto +moreover have "A<=B" using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto +ultimately show ?thesis by auto +qed + +lemma affine_parallel_subspace: +fixes S :: "('n::euclidean_space) set" +assumes "affine S" "S ~= {}" +shows "?!L. subspace L & affine_parallel S L" +proof- +have ex: "? L. subspace L & affine_parallel S L" using assms parallel_subspace_explicit by auto +{ fix L1 L2 assume ass: "subspace L1 & affine_parallel S L1" "subspace L2 & affine_parallel S L2" + hence "affine_parallel L1 L2" using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto + hence "L1=L2" using ass parallel_subspace by auto +} from this show ?thesis using ex by auto +qed + subsection {* Cones. *} definition @@ -343,6 +822,116 @@ apply(rule hull_eq[unfolded mem_def]) using cone_Inter unfolding subset_eq by (auto simp add: mem_def) +lemma mem_cone: + assumes "cone S" "x : S" "c>=0" + shows "c *\<^sub>R x : S" + using assms cone_def[of S] by auto + +lemma cone_contains_0: +fixes S :: "('m::euclidean_space) set" +assumes "cone S" +shows "(S ~= {}) <-> (0 : S)" +proof- +{ assume "S ~= {}" from this obtain a where "a:S" by auto + hence "0 : S" using assms mem_cone[of S a 0] by auto +} from this show ?thesis by auto +qed + +lemma cone_0: +shows "cone {(0 :: 'm::euclidean_space)}" +unfolding cone_def by auto + +lemma cone_Union[intro]: "(!s:f. cone s) --> (cone (Union f))" + unfolding cone_def by blast + +lemma cone_iff: +fixes S :: "('m::euclidean_space) set" +assumes "S ~= {}" +shows "cone S <-> 0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" +proof- +{ assume "cone S" + { fix c assume "(c :: real)>0" + { fix x assume "x : S" hence "x : (op *\<^sub>R c) ` S" unfolding image_def + using `cone S` `c>0` mem_cone[of S x "1/c"] + exI[of "(%t. t:S & x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] by auto + } + moreover + { fix x assume "x : (op *\<^sub>R c) ` S" + (*from this obtain t where "t:S & x = c *\<^sub>R t" by auto*) + hence "x:S" using `cone S` `c>0` unfolding cone_def image_def `c>0` by auto + } + ultimately have "((op *\<^sub>R c) ` S) = S" by auto + } hence "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" using `cone S` cone_contains_0[of S] assms by auto +} +moreover +{ assume a: "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" + { fix x assume "x:S" + fix c1 assume "(c1 :: real)>=0" + hence "(c1=0) | (c1>0)" by auto + hence "c1 *\<^sub>R x : S" using a `x:S` by auto + } + hence "cone S" unfolding cone_def by auto +} ultimately show ?thesis by blast +qed + +lemma cone_hull_empty: +"cone hull {} = {}" +by (metis cone_empty cone_hull_eq) + +lemma cone_hull_empty_iff: +fixes S :: "('m::euclidean_space) set" +shows "(S = {}) <-> (cone hull S = {})" +by (metis bot_least cone_hull_empty hull_subset xtrans(5)) + +lemma cone_hull_contains_0: +fixes S :: "('m::euclidean_space) set" +shows "(S ~= {}) <-> (0 : cone hull S)" +using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S] by auto + +lemma mem_cone_hull: + assumes "x : S" "c>=0" + shows "c *\<^sub>R x : cone hull S" +by (metis assms cone_cone_hull hull_inc mem_cone mem_def) + +lemma cone_hull_expl: +fixes S :: "('m::euclidean_space) set" +shows "cone hull S = {c *\<^sub>R x | c x. c>=0 & x : S}" (is "?lhs = ?rhs") +proof- +{ fix x assume "x : ?rhs" + from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto + fix c assume c_def: "(c :: real)>=0" + hence "c *\<^sub>R x = (c*cx) *\<^sub>R xx" using x_def by (simp add: algebra_simps) + moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto + ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto +} hence "cone ?rhs" unfolding cone_def by auto + hence "?rhs : cone" unfolding mem_def by auto +{ fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto + hence "x : ?rhs" by auto +} hence "S <= ?rhs" by auto +hence "?lhs <= ?rhs" using `?rhs : cone` hull_minimal[of S "?rhs" "cone"] by auto +moreover +{ fix x assume "x : ?rhs" + from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto + hence "xx : cone hull S" using hull_subset[of S] by auto + hence "x : ?lhs" using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto +} ultimately show ?thesis by auto +qed + +lemma cone_closure: +fixes S :: "('m::euclidean_space) set" +assumes "cone S" +shows "cone (closure S)" +proof- +{ assume "S = {}" hence ?thesis by auto } +moreover +{ assume "S ~= {}" hence "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto + hence "0:(closure S) & (!c. c>0 --> op *\<^sub>R c ` (closure S) = (closure S))" + using closure_subset by (auto simp add: closure_scaleR) + hence ?thesis using cone_iff[of "closure S"] by auto +} +ultimately show ?thesis by blast +qed + subsection {* Affine dependence and consequential theorems (from Lars Schewe). *} definition @@ -514,6 +1103,28 @@ shows "finite s \ bounded(convex hull s)" using bounded_convex_hull finite_imp_bounded by auto +subsection {* Convex hull is "preserved" by a linear function. *} + +lemma convex_hull_linear_image: + assumes "bounded_linear f" + shows "f ` (convex hull s) = convex hull (f ` s)" + apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 + apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption + apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption +proof- + interpret f: bounded_linear f by fact + show "convex {x. f x \ convex hull f ` s}" + unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next + interpret f: bounded_linear f by fact + show "convex {x. x \ f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s] + unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric]) +qed auto + +lemma in_convex_hull_linear_image: + assumes "bounded_linear f" "x \ convex hull s" + shows "(f x) \ convex hull (f ` s)" +using convex_hull_linear_image[OF assms(1)] assms(2) by auto + subsection {* Stepping theorems for convex hulls of finite sets. *} lemma convex_hull_empty[simp]: "convex hull {} = {}" @@ -775,10 +1386,6 @@ text {* TODO: Generalize linear algebra concepts defined in @{text Euclidean_Space.thy} so that we can generalize these lemmas. *} -lemma subspace_imp_affine: - fixes s :: "(_::euclidean_space) set" shows "subspace s \ affine s" - unfolding subspace_def affine_def by auto - lemma affine_imp_convex: "affine s \ convex s" unfolding affine_def convex_def by auto @@ -952,6 +1559,979 @@ thus "x \ convex hull p" using hull_mono[OF `s\p`] by auto qed + +subsection {* Some Properties of Affine Dependent Sets *} + +lemma affine_independent_empty: "~(affine_dependent {})" + by (simp add: affine_dependent_def) + +lemma affine_independent_sing: +fixes a :: "'n::euclidean_space" +shows "~(affine_dependent {a})" + by (simp add: affine_dependent_def) + +lemma affine_hull_translation: +"affine hull ((%x. a + x) ` S) = (%x. a + x) ` (affine hull S)" +proof- +have "affine ((%x. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by auto +moreover have "(%x. a + x) ` S <= (%x. a + x) ` (affine hull S)" using hull_subset[of S] by auto +ultimately have h1: "affine hull ((%x. a + x) ` S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal mem_def) +have "affine((%x. -a + x) ` (affine hull ((%x. a + x) ` S)))" using affine_translation affine_affine_hull by auto +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 +moreover have "S=(%x. -a + x) ` (%x. a + x) ` S" using translation_assoc[of "-a" a] by auto +ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal mem_def) +hence "affine hull ((%x. a + x) ` S) >= (%x. a + x) ` (affine hull S)" by auto +from this show ?thesis using h1 by auto +qed + +lemma affine_dependent_translation: + assumes "affine_dependent S" + shows "affine_dependent ((%x. a + x) ` S)" +proof- +obtain x where x_def: "x : S & x : affine hull (S - {x})" using assms affine_dependent_def by auto +have "op + a ` (S - {x}) = op + a ` S - {a + x}" by auto +hence "a+x : affine hull ((%x. a + x) ` S - {a+x})" using affine_hull_translation[of a "S-{x}"] x_def by auto +moreover have "a+x : (%x. a + x) ` S" using x_def by auto +ultimately show ?thesis unfolding affine_dependent_def by auto +qed + +lemma affine_dependent_translation_eq: + "affine_dependent S <-> affine_dependent ((%x. a + x) ` S)" +proof- +{ assume "affine_dependent ((%x. a + x) ` S)" + hence "affine_dependent S" using affine_dependent_translation[of "((%x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] by auto +} from this show ?thesis using affine_dependent_translation by auto +qed + +lemma affine_hull_0_dependent: + fixes S :: "('n::euclidean_space) set" + assumes "0 : affine hull S" + shows "dependent S" +proof- +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 +hence "EX v:s. u v ~= 0" using setsum_not_0[of "u" "s"] by auto +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 +from this show ?thesis unfolding dependent_explicit[of S] by auto +qed + +lemma affine_dependent_imp_dependent2: + fixes S :: "('n::euclidean_space) set" + assumes "affine_dependent (insert 0 S)" + shows "dependent S" +proof- +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 +hence "x : span (insert 0 S - {x})" using affine_hull_subset_span by auto +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 +ultimately have "x : span (S - {x})" by auto +hence "(x~=0) ==> dependent S" using x_def dependent_def by auto +moreover +{ assume "x=0" hence "0 : affine hull S" using x_def hull_mono[of "S - {0}" S] by auto + hence "dependent S" using affine_hull_0_dependent by auto +} ultimately show ?thesis by auto +qed + +lemma affine_dependent_iff_dependent: + fixes S :: "('n::euclidean_space) set" + assumes "a ~: S" + shows "affine_dependent (insert a S) <-> dependent ((%x. -a + x) ` S)" +proof- +have "(op + (- a) ` S)={x - a| x . x : S}" by auto +from this show ?thesis using affine_dependent_translation_eq[of "(insert a S)" "-a"] + affine_dependent_imp_dependent2 assms + dependent_imp_affine_dependent[of a S] by auto +qed + +lemma affine_dependent_iff_dependent2: + fixes S :: "('n::euclidean_space) set" + assumes "a : S" + shows "affine_dependent S <-> dependent ((%x. -a + x) ` (S-{a}))" +proof- +have "insert a (S - {a})=S" using assms by auto +from this show ?thesis using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto +qed + +lemma affine_hull_insert_span_gen: + fixes a :: "_::euclidean_space" + shows "affine hull (insert a s) = (%x. a+x) ` span ((%x. -a+x) ` s)" +proof- +have h1: "{x - a |x. x : s}=((%x. -a+x) ` s)" by auto +{ assume "a ~: s" hence ?thesis using affine_hull_insert_span[of a s] h1 by auto} +moreover +{ assume a1: "a : s" + have "EX x. x:s & -a+x=0" apply (rule exI[of _ a]) using a1 by auto + hence "insert 0 ((%x. -a+x) ` (s - {a}))=(%x. -a+x) ` s" by auto + hence "span ((%x. -a+x) ` (s - {a}))=span ((%x. -a+x) ` s)" + using span_insert_0[of "op + (- a) ` (s - {a})"] by auto + moreover have "{x - a |x. x : (s - {a})}=((%x. -a+x) ` (s - {a}))" by auto + moreover have "insert a (s - {a})=(insert a s)" using assms by auto + ultimately have ?thesis using assms affine_hull_insert_span[of "a" "s-{a}"] by auto +} +ultimately show ?thesis by auto +qed + +lemma affine_hull_span2: + fixes a :: "_::euclidean_space" + assumes "a : s" + shows "affine hull s = (%x. a+x) ` span ((%x. -a+x) ` (s-{a}))" + using affine_hull_insert_span_gen[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto + +lemma affine_hull_span_gen: + fixes a :: "_::euclidean_space" + assumes "a : affine hull s" + shows "affine hull s = (%x. a+x) ` span ((%x. -a+x) ` s)" +proof- +have "affine hull (insert a s) = affine hull s" using hull_redundant[of a affine s] assms by auto +from this show ?thesis using affine_hull_insert_span_gen[of a "s"] by auto +qed + +lemma affine_hull_span_0: + assumes "(0 :: _::euclidean_space) : affine hull S" + shows "affine hull S = span S" +using affine_hull_span_gen[of "0" S] assms by auto + + +lemma extend_to_affine_basis: +fixes S V :: "('n::euclidean_space) set" +assumes "~(affine_dependent S)" "S <= V" "S~={}" +shows "? T. ~(affine_dependent T) & S<=T & T<=V & affine hull T = affine hull V" +proof- +obtain a where a_def: "a : S" using assms by auto +hence h0: "independent ((%x. -a + x) ` (S-{a}))" using affine_dependent_iff_dependent2 assms by auto +from this obtain B + where B_def: "(%x. -a+x) ` (S - {a}) <= B & B <= (%x. -a+x) ` V & independent B & (%x. -a+x) ` V <= span B" + using maximal_independent_subset_extend[of "(%x. -a+x) ` (S-{a})" "(%x. -a + x) ` V"] assms by blast +def T == "(%x. a+x) ` (insert 0 B)" hence "T=insert a ((%x. a+x) ` B)" by auto +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 +hence "V <= affine hull T" using B_def assms translation_inverse_subset[of a V "span B"] by auto +moreover have "T<=V" using T_def B_def a_def assms by auto +ultimately have "affine hull T = affine hull V" + by (metis Int_absorb1 Int_absorb2 Int_commute Int_lower2 assms hull_hull hull_mono) +moreover have "S<=T" using T_def B_def translation_inverse_subset[of a "S-{a}" B] by auto +moreover have "~(affine_dependent T)" using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B_def by auto +ultimately show ?thesis using `T<=V` by auto +qed + +lemma affine_basis_exists: +fixes V :: "('n::euclidean_space) set" +shows "? B. B <= V & ~(affine_dependent B) & affine hull V = affine hull B" +proof- +{ assume empt: "V={}" have "? B. B <= V & ~(affine_dependent B) & (affine hull V=affine hull B)" using empt affine_independent_empty by auto +} +moreover +{ assume nonempt: "V~={}" obtain x where "x:V" using nonempt by auto + hence "? B. B <= V & ~(affine_dependent B) & (affine hull V=affine hull B)" + using affine_dependent_def[of "{x}"] extend_to_affine_basis[of "{x}:: ('n::euclidean_space) set" V] by auto +} +ultimately show ?thesis by auto +qed + +subsection {* Affine Dimension of a Set *} + +definition "aff_dim V = (SOME d :: int. ? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = d+1))" + +lemma aff_dim_basis_exists: + fixes V :: "('n::euclidean_space) set" + shows "? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)" +proof- +obtain B where B_def: "~(affine_dependent B) & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto +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 +qed + +lemma affine_hull_nonempty: "(S ~= {}) <-> affine hull S ~= {}" +proof- +fix S have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto +moreover have "affine hull S = {} ==> S = {}" unfolding hull_def by auto +ultimately show "(S ~= {}) <-> affine hull S ~= {}" by blast +qed + +lemma aff_dim_parallel_subspace_aux: +fixes B :: "('n::euclidean_space) set" +assumes "~(affine_dependent B)" "a:B" +shows "finite B & ((card B) - 1 = dim (span ((%x. -a+x) ` (B-{a}))))" +proof- +have "independent ((%x. -a + x) ` (B-{a}))" using affine_dependent_iff_dependent2 assms by auto +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 +{ assume emp: "(%x. -a + x) ` (B - {a}) = {}" + have "B=insert a ((%x. a + x) ` (%x. -a + x) ` (B - {a}))" using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto + hence "B={a}" using emp by auto + hence ?thesis using assms fin by auto +} +moreover +{ assume "(%x. -a + x) ` (B - {a}) ~= {}" + hence "card ((%x. -a + x) ` (B - {a}))>0" using fin by auto + moreover have h1: "card ((%x. -a + x) ` (B-{a})) = card (B-{a})" + apply (rule card_image) using translate_inj_on by auto + ultimately have "card (B-{a})>0" by auto + hence "finite(B-{a})" using card_gt_0_iff[of "(B - {a})"] by auto + moreover hence "(card (B-{a})= (card B) - 1)" using card_Diff_singleton assms by auto + ultimately have ?thesis using fin h1 by auto +} ultimately show ?thesis by auto +qed + +lemma aff_dim_parallel_subspace: +fixes V L :: "('n::euclidean_space) set" +assumes "V ~= {}" +assumes "subspace L" "affine_parallel (affine hull V) L" +shows "aff_dim V=int(dim L)" +proof- +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 +hence "B~={}" using assms B_def affine_hull_nonempty[of V] affine_hull_nonempty[of B] by auto +from this obtain a where a_def: "a : B" by auto +def Lb == "span ((%x. -a+x) ` (B-{a}))" + moreover have "affine_parallel (affine hull B) Lb" + 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 + moreover have "subspace Lb" using Lb_def subspace_span by auto + moreover have "affine hull B ~= {}" using assms B_def affine_hull_nonempty[of V] by auto + ultimately have "L=Lb" using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B_def by auto + hence "dim L=dim Lb" by auto + moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def B_def by auto +(* hence "card B=dim Lb+1" using `B~={}` card_gt_0_iff[of B] by auto *) + ultimately show ?thesis using B_def `B~={}` card_gt_0_iff[of B] by auto +qed + +lemma aff_independent_finite: +fixes B :: "('n::euclidean_space) set" +assumes "~(affine_dependent B)" +shows "finite B" +proof- +{ assume "B~={}" from this obtain a where "a:B" by auto + hence ?thesis using aff_dim_parallel_subspace_aux assms by auto +} from this show ?thesis by auto +qed + +lemma independent_finite: +fixes B :: "('n::euclidean_space) set" +assumes "independent B" +shows "finite B" +using affine_dependent_imp_dependent[of B] aff_independent_finite[of B] assms by auto + +lemma subspace_dim_equal: +assumes "subspace (S :: ('n::euclidean_space) set)" "subspace T" "S <= T" "dim S >= dim T" +shows "S=T" +proof- +obtain B where B_def: "B <= S & independent B & S <= span B & (card B = dim S)" using basis_exists[of S] by auto +hence "span B <= S" using span_mono[of B S] span_eq[of S] assms by metis +hence "span B = S" using B_def by auto +have "dim S = dim T" using assms dim_subset[of S T] by auto +hence "T <= span B" using card_eq_dim[of B T] B_def independent_finite assms by auto +from this show ?thesis using assms `span B=S` by auto +qed + +lemma span_substd_basis: assumes "d\{.. x$$i = 0)}" + (is "span ?A = ?B") +proof- +have "?A <= ?B" by auto +moreover have s: "subspace ?B" using subspace_substandard[of "%i. i ~: d"] . +ultimately have "span ?A <= ?B" using span_mono[of "?A" "?B"] span_eq[of "?B"] by blast +moreover have "card d <= dim (span ?A)" using independent_card_le_dim[of "?A" "span ?A"] + independent_substdbasis[OF assms] card_substdbasis[OF assms] span_inc[of "?A"] by auto +moreover hence "dim ?B <= dim (span ?A)" using dim_substandard[OF assms] by auto +ultimately show ?thesis using s subspace_dim_equal[of "span ?A" "?B"] + subspace_span[of "?A"] by auto +qed + +lemma basis_to_substdbasis_subspace_isomorphism: +fixes B :: "('a::euclidean_space) set" +assumes "independent B" +shows "EX f d. card d = card B & linear f & f ` B = {basis i::'a |i. i : (d :: nat set)} & + f ` span B = {x. ALL i x $$ i = (0::real)} & inj_on f (span B) \ d\{.. "{..{.. aff_dim S = -1" +proof- +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 +moreover hence "S={} <-> B={}" using affine_hull_nonempty[of B] affine_hull_nonempty[of S] by auto +ultimately show ?thesis using aff_independent_finite[of B] card_gt_0_iff[of B] by auto +qed + +lemma aff_dim_affine_hull: +fixes S :: "('n::euclidean_space) set" +shows "aff_dim (affine hull S)=aff_dim S" +unfolding aff_dim_def using hull_hull[of _ S] by auto + +lemma aff_dim_affine_hull2: +fixes S T :: "('n::euclidean_space) set" +assumes "affine hull S=affine hull T" +shows "aff_dim S=aff_dim T" unfolding aff_dim_def using assms by auto + +lemma aff_dim_unique: +fixes B V :: "('n::euclidean_space) set" +assumes "(affine hull B=affine hull V) & ~(affine_dependent B)" +shows "of_nat(card B) = aff_dim V+1" +proof- +{ assume "B={}" hence "V={}" using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms by auto + hence "aff_dim V = (-1::int)" using aff_dim_empty by auto + hence ?thesis using `B={}` by auto +} +moreover +{ assume "B~={}" from this obtain a where a_def: "a:B" by auto + def Lb == "span ((%x. -a+x) ` (B-{a}))" + have "affine_parallel (affine hull B) Lb" + using Lb_def affine_hull_span2[of a B] a_def affine_parallel_commut[of "Lb" "(affine hull B)"] + unfolding affine_parallel_def by auto + moreover have "subspace Lb" using Lb_def subspace_span by auto + ultimately have "aff_dim B=int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] `B~={}` by auto + moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def assms by auto + ultimately have "(of_nat(card B) = aff_dim B+1)" using `B~={}` card_gt_0_iff[of B] by auto + hence ?thesis using aff_dim_affine_hull2 assms by auto +} ultimately show ?thesis by blast +qed + +lemma aff_dim_affine_independent: +fixes B :: "('n::euclidean_space) set" +assumes "~(affine_dependent B)" +shows "of_nat(card B) = aff_dim B+1" + using aff_dim_unique[of B B] assms by auto + +lemma aff_dim_sing: +fixes a :: "'n::euclidean_space" +shows "aff_dim {a}=0" + using aff_dim_affine_independent[of "{a}"] affine_independent_sing by auto + +lemma aff_dim_inner_basis_exists: + fixes V :: "('n::euclidean_space) set" + shows "? B. B<=V & (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)" +proof- +obtain B where B_def: "~(affine_dependent B) & B<=V & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto +moreover hence "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto +ultimately show ?thesis by auto +qed + +lemma aff_dim_le_card: +fixes V :: "('n::euclidean_space) set" +assumes "finite V" +shows "aff_dim V <= of_nat(card V) - 1" + proof- + 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 + moreover hence "card B <= card V" using assms card_mono by auto + ultimately show ?thesis by auto +qed + +lemma aff_dim_parallel_eq: +fixes S T :: "('n::euclidean_space) set" +assumes "affine_parallel (affine hull S) (affine hull T)" +shows "aff_dim S=aff_dim T" +proof- +{ assume "T~={}" "S~={}" + from this obtain L where L_def: "subspace L & affine_parallel (affine hull T) L" + using affine_parallel_subspace[of "affine hull T"] affine_affine_hull[of T] affine_hull_nonempty by auto + hence "aff_dim T = int(dim L)" using aff_dim_parallel_subspace `T~={}` by auto + moreover have "subspace L & affine_parallel (affine hull S) L" + using L_def affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto + moreover hence "aff_dim S = int(dim L)" using aff_dim_parallel_subspace `S~={}` by auto + ultimately have ?thesis by auto +} +moreover +{ assume "S={}" hence "S={} & T={}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto + hence ?thesis using aff_dim_empty by auto +} +moreover +{ assume "T={}" hence "S={} & T={}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto + hence ?thesis using aff_dim_empty by auto +} +ultimately show ?thesis by blast +qed + +lemma aff_dim_translation_eq: +fixes a :: "'n::euclidean_space" +shows "aff_dim ((%x. a + x) ` S)=aff_dim S" +proof- +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 +from this show ?thesis using aff_dim_parallel_eq[of S "(%x. a + x) ` S"] by auto +qed + +lemma aff_dim_affine: +fixes S L :: "('n::euclidean_space) set" +assumes "S ~= {}" "affine S" +assumes "subspace L" "affine_parallel S L" +shows "aff_dim S=int(dim L)" +proof- +have 1: "(affine hull S) = S" using assms affine_hull_eq[of S] by auto +hence "affine_parallel (affine hull S) L" using assms by (simp add:1) +from this show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast +qed + +lemma dim_affine_hull: +fixes S :: "('n::euclidean_space) set" +shows "dim (affine hull S)=dim S" +proof- +have "dim (affine hull S)>=dim S" using dim_subset by auto +moreover have "dim(span S) >= dim (affine hull S)" using dim_subset affine_hull_subset_span by auto +moreover have "dim(span S)=dim S" using dim_span by auto +ultimately show ?thesis by auto +qed + +lemma aff_dim_subspace: +fixes S :: "('n::euclidean_space) set" +assumes "S ~= {}" "subspace S" +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 + +lemma aff_dim_zero: +fixes S :: "('n::euclidean_space) set" +assumes "0 : affine hull S" +shows "aff_dim S=int(dim S)" +proof- +have "subspace(affine hull S)" using subspace_affine[of "affine hull S"] affine_affine_hull assms by auto +hence "aff_dim (affine hull S) =int(dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto +from this show ?thesis using aff_dim_affine_hull[of S] dim_affine_hull[of S] by auto +qed + +lemma aff_dim_univ: "aff_dim (UNIV :: ('n::euclidean_space) set) = int(DIM('n))" + using aff_dim_subspace[of "(UNIV :: ('n::euclidean_space) set)"] + dim_UNIV[where 'a="'n::euclidean_space"] by auto + +lemma aff_dim_geq: + fixes V :: "('n::euclidean_space) set" + shows "aff_dim V >= -1" +proof- +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 +from this show ?thesis by auto +qed + +lemma independent_card_le_aff_dim: + assumes "(B::('n::euclidean_space) set) <= V" + assumes "~(affine_dependent B)" + shows "int(card B) <= aff_dim V+1" +proof- +{ assume "B~={}" + from this obtain T where T_def: "~(affine_dependent T) & B<=T & T<=V & affine hull T = affine hull V" + using assms extend_to_affine_basis[of B V] by auto + hence "of_nat(card T) = aff_dim V+1" using aff_dim_unique by auto + hence ?thesis using T_def card_mono[of T B] aff_independent_finite[of T] by auto +} +moreover +{ assume "B={}" + moreover have "-1<= aff_dim V" using aff_dim_geq by auto + ultimately have ?thesis by auto +} ultimately show ?thesis by blast +qed + +lemma aff_dim_subset: + fixes S T :: "('n::euclidean_space) set" + assumes "S <= T" + shows "aff_dim S <= aff_dim T" +proof- +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 +moreover hence "int (card B) <= aff_dim T + 1" using assms independent_card_le_aff_dim[of B T] by auto +ultimately show ?thesis by auto +qed + +lemma aff_dim_subset_univ: +fixes S :: "('n::euclidean_space) set" +shows "aff_dim S <= int(DIM('n))" +proof - + have "aff_dim (UNIV :: ('n::euclidean_space) set) = int(DIM('n))" using aff_dim_univ by auto + 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 +qed + +lemma affine_dim_equal: +assumes "affine (S :: ('n::euclidean_space) set)" "affine T" "S ~= {}" "S <= T" "aff_dim S = aff_dim T" +shows "S=T" +proof- +obtain a where "a : S" using assms by auto +hence "a : T" using assms by auto +def LS == "{y. ? x : S. (-a)+x=y}" +hence ls: "subspace LS & affine_parallel S LS" using assms parallel_subspace_explicit[of S a LS] `a : S` by auto +hence h1: "int(dim LS) = aff_dim S" using assms aff_dim_affine[of S LS] by auto +have "T ~= {}" using assms by auto +def LT == "{y. ? x : T. (-a)+x=y}" +hence lt: "subspace LT & affine_parallel T LT" using assms parallel_subspace_explicit[of T a LT] `a : T` by auto +hence "int(dim LT) = aff_dim T" using assms aff_dim_affine[of T LT] `T ~= {}` by auto +hence "dim LS = dim LT" using h1 assms by auto +moreover have "LS <= LT" using LS_def LT_def assms by auto +ultimately have "LS=LT" using subspace_dim_equal[of LS LT] ls lt by auto +moreover have "S = {x. ? y : LS. a+y=x}" using LS_def by auto +moreover have "T = {x. ? y : LT. a+y=x}" using LT_def by auto +ultimately show ?thesis by auto +qed + +lemma affine_hull_univ: +fixes S :: "('n::euclidean_space) set" +assumes "aff_dim S = int(DIM('n))" +shows "affine hull S = (UNIV :: ('n::euclidean_space) set)" +proof- +have "S ~= {}" using assms aff_dim_empty[of S] by auto +have h0: "S <= affine hull S" using hull_subset[of S _] by auto +have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S" using aff_dim_univ assms by auto +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 +have h3: "aff_dim S <= aff_dim (affine hull S)" using h0 aff_dim_subset[of S "affine hull S"] assms by auto +hence h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)" using h0 h1 h2 by auto +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 +qed + +lemma aff_dim_convex_hull: +fixes S :: "('n::euclidean_space) set" +shows "aff_dim (convex hull S)=aff_dim S" + using aff_dim_affine_hull[of S] convex_hull_subset_affine_hull[of S] + hull_subset[of S "convex"] aff_dim_subset[of S "convex hull S"] + aff_dim_subset[of "convex hull S" "affine hull S"] by auto + +lemma aff_dim_cball: +fixes a :: "'n::euclidean_space" +assumes "00 & cball x e <= S" using open_contains_cball[of S] assms by auto +from this have "aff_dim (cball x e) <= aff_dim S" using aff_dim_subset by auto +from this show ?thesis using aff_dim_cball[of e x] aff_dim_subset_univ[of S] e_def by auto +qed + +lemma low_dim_interior: +fixes S :: "('n::euclidean_space) set" +assumes "~(aff_dim S = int (DIM('n)))" +shows "interior S = {}" +proof- +have "aff_dim(interior S) <= aff_dim S" + using interior_subset aff_dim_subset[of "interior S" S] by auto +from this show ?thesis using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto +qed + +subsection{* Relative Interior of a Set *} + +definition "rel_interior S = {x. ? T. openin (subtopology euclidean (affine hull S)) T & x : T & T <= S}" + +lemma rel_interior: "rel_interior S = {x : S. ? T. open T & x : T & (T Int (affine hull S)) <= S}" + unfolding rel_interior_def[of S] openin_open[of "affine hull S"] apply auto +proof- +fix x T assume a: "x:S" "open T" "x : T" "(T Int (affine hull S)) <= S" +hence h1: "x : T Int affine hull S" using hull_inc by auto +show "EX Tb. (EX Ta. open Ta & Tb = affine hull S Int Ta) & x : Tb & Tb <= S" +apply (rule_tac x="T Int (affine hull S)" in exI) +using a h1 by auto +qed + +lemma mem_rel_interior: + "x : rel_interior S <-> (? T. open T & x : (T Int S) & (T Int (affine hull S)) <= S)" + by (auto simp add: rel_interior) + +lemma mem_rel_interior_ball: "x : rel_interior S <-> x : S & (? e. 0 < e & ((ball x e) Int (affine hull S)) <= S)" + apply (simp add: rel_interior, safe) + apply (force simp add: open_contains_ball) + apply (rule_tac x="ball x e" in exI) + apply (simp add: open_ball centre_in_ball) + done + +lemma rel_interior_ball: + "rel_interior S = {x : S. ? e. e>0 & ((ball x e) Int (affine hull S)) <= S}" + using mem_rel_interior_ball [of _ S] by auto + +lemma mem_rel_interior_cball: "x : rel_interior S <-> x : S & (? e. 0 < e & ((cball x e) Int (affine hull S)) <= S)" + apply (simp add: rel_interior, safe) + apply (force simp add: open_contains_cball) + apply (rule_tac x="ball x e" in exI) + apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball]) + apply auto + done + +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 + +lemma rel_interior_empty: "rel_interior {} = {}" + by (auto simp add: rel_interior_def) + +lemma affine_hull_sing: "affine hull {a :: 'n::euclidean_space} = {a}" +by (metis affine_hull_eq affine_sing) + +lemma rel_interior_sing: "rel_interior {a :: 'n::euclidean_space} = {a}" + unfolding rel_interior_ball affine_hull_sing apply auto + apply(rule_tac x="1 :: real" in exI) apply simp + done + +lemma subset_rel_interior: +fixes S T :: "('n::euclidean_space) set" +assumes "S<=T" "affine hull S=affine hull T" +shows "rel_interior S <= rel_interior T" + using assms by (auto simp add: rel_interior_def) + +lemma rel_interior_subset: "rel_interior S <= S" + by (auto simp add: rel_interior_def) + +lemma rel_interior_subset_closure: "rel_interior S <= closure S" + using rel_interior_subset by (auto simp add: closure_def) + +lemma interior_subset_rel_interior: "interior S <= rel_interior S" + by (auto simp add: rel_interior interior_def) + +lemma interior_rel_interior: +fixes S :: "('n::euclidean_space) set" +assumes "aff_dim S = int(DIM('n))" +shows "rel_interior S = interior S" +proof - +have "affine hull S = UNIV" using assms affine_hull_univ[of S] by auto +from this show ?thesis unfolding rel_interior interior_def by auto +qed + +lemma rel_interior_open: +fixes S :: "('n::euclidean_space) set" +assumes "open S" +shows "rel_interior S = S" +by (metis assms interior_eq interior_subset_rel_interior rel_interior_subset set_eq_subset) + +lemma interior_rel_interior_gen: +fixes S :: "('n::euclidean_space) set" +shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})" +by (metis interior_rel_interior low_dim_interior) + +lemma rel_interior_univ: +fixes S :: "('n::euclidean_space) set" +shows "rel_interior (affine hull S) = affine hull S" +proof- +have h1: "rel_interior (affine hull S) <= affine hull S" using rel_interior_subset by auto +{ fix x assume x_def: "x : affine hull S" + obtain e :: real where "e=1" by auto + hence "e>0 & ball x e Int affine hull (affine hull S) <= affine hull S" using hull_hull[of _ S] by auto + hence "x : rel_interior (affine hull S)" using x_def rel_interior_ball[of "affine hull S"] by auto +} from this show ?thesis using h1 by auto +qed + +lemma rel_interior_univ2: "rel_interior (UNIV :: ('n::euclidean_space) set) = UNIV" +by (metis open_UNIV rel_interior_open) + +lemma rel_interior_convex_shrink: + fixes S :: "('a::euclidean_space) set" + assumes "convex S" "c : rel_interior S" "x : S" "0 < e" "e <= 1" + shows "x - e *\<^sub>R (x - c) : rel_interior S" +proof- +(* Proof is a modified copy of the proof of similar lemma mem_interior_convex_shrink +*) +obtain d where "d>0" and d:"ball c d Int affine hull S <= S" + using assms(2) unfolding mem_rel_interior_ball by auto +{ fix y assume as:"dist (x - e *\<^sub>R (x - c)) y < e * d & y : affine hull S" + 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) + have "x : affine hull S" using assms hull_subset[of S] by auto + moreover have "1 / e + - ((1 - e) / e) = 1" + using `e>0` mult_left.diff[of "1" "(1-e)" "1/e"] by auto + ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S" + 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) + 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)" + unfolding dist_norm unfolding norm_scaleR[THEN sym] apply(rule arg_cong[where f=norm]) using `e>0` + by(auto simp add:euclidean_eq[where 'a='a] field_simps) + 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) + also have "... < d" using as[unfolded dist_norm] and `e>0` + by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute) + finally have "y : S" apply(subst *) +apply(rule assms(1)[unfolded convex_alt,rule_format]) + apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) ** by auto +} hence "ball (x - e *\<^sub>R (x - c)) (e*d) Int affine hull S <= S" by auto +moreover have "0 < e*d" using `0R (x - c) : S" + using mem_convex[of S x c e] apply (simp add: algebra_simps) using assms by auto +ultimately show ?thesis + using mem_rel_interior_ball[of "x - e *\<^sub>R (x - c)" S] `e>0` by auto +qed + +lemma interior_real_semiline: +fixes a :: real +shows "interior {a..} = {a<..}" +proof- +{ fix y assume "a0 & cball y e \ {a..}" + using mem_interior_cball[of y "{a..}"] by auto + moreover hence "y-e : cball y e" by (auto simp add: cball_def dist_norm) + ultimately have "a<=y-e" by auto + hence "a {}" using assms unfolding set_eq_iff by (auto intro!: exI[of _ "(a + b) / 2"]) + then show ?thesis + using interior_rel_interior_gen[of "{a..b}", symmetric] + by (simp split: split_if_asm add: interior_closed_interval) +qed + +lemma rel_interior_real_semiline: + fixes a :: real shows "rel_interior {a..} = {a<..}" +proof- + have *: "{a<..} \ {}" unfolding set_eq_iff by (auto intro!: exI[of _ "a + 1"]) + then show ?thesis using interior_real_semiline + interior_rel_interior_gen[of "{a..}"] + by (auto split: split_if_asm) +qed + +subsection "Relative open" + +definition "rel_open S <-> (rel_interior S) = S" + +lemma rel_open: "rel_open S <-> openin (subtopology euclidean (affine hull S)) S" + unfolding rel_open_def rel_interior_def apply auto + using openin_subopen[of "subtopology euclidean (affine hull S)" S] by auto + +lemma opein_rel_interior: + "openin (subtopology euclidean (affine hull S)) (rel_interior S)" + apply (simp add: rel_interior_def) + apply (subst openin_subopen) by blast + +lemma affine_rel_open: + fixes S :: "('n::euclidean_space) set" + assumes "affine S" shows "rel_open S" + unfolding rel_open_def using assms rel_interior_univ[of S] affine_hull_eq[of S] by metis + +lemma affine_closed: + fixes S :: "('n::euclidean_space) set" + assumes "affine S" shows "closed S" +proof- +{ assume "S ~= {}" + from this obtain L where L_def: "subspace L & affine_parallel S L" + using assms affine_parallel_subspace[of S] by auto + from this obtain "a" where a_def: "S=(op + a ` L)" + using affine_parallel_def[of L S] affine_parallel_commut by auto + have "closed L" using L_def closed_subspace by auto + hence "closed S" using closed_translation a_def by auto +} from this show ?thesis by auto +qed + +lemma closure_affine_hull: + fixes S :: "('n::euclidean_space) set" + shows "closure S <= affine hull S" +proof- +have "closure S <= closure (affine hull S)" using subset_closure by auto +moreover have "closure (affine hull S) = affine hull S" + using affine_affine_hull affine_closed[of "affine hull S"] closure_eq by auto +ultimately show ?thesis by auto +qed + +lemma closure_same_affine_hull: + fixes S :: "('n::euclidean_space) set" + shows "affine hull (closure S) = affine hull S" +proof- +have "affine hull (closure S) <= affine hull S" + using hull_mono[of "closure S" "affine hull S" "affine"] closure_affine_hull[of S] hull_hull[of "affine" S] by auto +moreover have "affine hull (closure S) >= affine hull S" + using hull_mono[of "S" "closure S" "affine"] closure_subset by auto +ultimately show ?thesis by auto +qed + +lemma closure_aff_dim: + fixes S :: "('n::euclidean_space) set" + shows "aff_dim (closure S) = aff_dim S" +proof- +have "aff_dim S <= aff_dim (closure S)" using aff_dim_subset closure_subset by auto +moreover have "aff_dim (closure S) <= aff_dim (affine hull S)" + using aff_dim_subset closure_affine_hull by auto +moreover have "aff_dim (affine hull S) = aff_dim S" using aff_dim_affine_hull by auto +ultimately show ?thesis by auto +qed + +lemma rel_interior_closure_convex_shrink: + fixes S :: "(_::euclidean_space) set" + assumes "convex S" "c : rel_interior S" "x : closure S" "0 < e" "e <= 1" + shows "x - e *\<^sub>R (x - c) : rel_interior S" +proof- +(* Proof is a modified copy of the proof of similar lemma mem_interior_closure_convex_shrink +*) +obtain d where "d>0" and d:"ball c d Int affine hull S <= S" + using assms(2) unfolding mem_rel_interior_ball by auto +have "EX y : S. norm (y - x) * (1 - e) < e * d" proof(cases "x : S") + case True thus ?thesis using `e>0` `d>0` by(rule_tac bexI[where x=x], auto intro!: mult_pos_pos) next + case False hence x:"x islimpt S" using assms(3)[unfolded closure_def] by auto + show ?thesis proof(cases "e=1") + case True obtain y where "y : S" "y ~= x" "dist y x < 1" + using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto + thus ?thesis apply(rule_tac x=y in bexI) unfolding True using `d>0` by auto next + case False hence "0 < e * d / (1 - e)" and *:"1 - e > 0" + using `e<=1` `e>0` `d>0` by(auto intro!:mult_pos_pos divide_pos_pos) + then obtain y where "y : S" "y ~= x" "dist y x < e * d / (1 - e)" + using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto + thus ?thesis apply(rule_tac x=y in bexI) unfolding dist_norm using pos_less_divide_eq[OF *] by auto qed qed + then obtain y where "y : S" and y:"norm (y - x) * (1 - e) < e * d" by auto + def z == "c + ((1 - e) / e) *\<^sub>R (x - y)" + 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) + have zball: "z\ball c d" + using mem_ball z_def dist_norm[of c] using y and assms(4,5) by (auto simp add:field_simps norm_minus_commute) + have "x : affine hull S" using closure_affine_hull assms by auto + moreover have "y : affine hull S" using `y : S` hull_subset[of S] by auto + moreover have "c : affine hull S" using assms rel_interior_subset hull_subset[of S] by auto + ultimately have "z : affine hull S" + using z_def affine_affine_hull[of S] + mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"] + assms by (auto simp add: field_simps) + hence "z : S" using d zball by auto + obtain d1 where "d1>0" and d1:"ball z d1 <= ball c d" + using zball open_ball[of c d] openE[of "ball c d" z] by auto + hence "(ball z d1) Int (affine hull S) <= (ball c d) Int (affine hull S)" by auto + hence "(ball z d1) Int (affine hull S) <= S" using d by auto + hence "z : rel_interior S" using mem_rel_interior_ball using `d1>0` `z : S` by auto + 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 + thus ?thesis using * by auto +qed + +subsection{* Relative interior preserves under linear transformations *} + +lemma rel_interior_translation_aux: +fixes a :: "'n::euclidean_space" +shows "((%x. a + x) ` rel_interior S) <= rel_interior ((%x. a + x) ` S)" +proof- +{ fix x assume x_def: "x : rel_interior S" + 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 + from this have "open ((%x. a + x) ` T)" and + "(a + x) : (((%x. a + x) ` T) Int ((%x. a + x) ` S))" and + "(((%x. a + x) ` T) Int (affine hull ((%x. a + x) ` S))) <= ((%x. a + x) ` S)" + using affine_hull_translation[of a S] open_translation[of T a] x_def by auto + from this have "(a+x) : rel_interior ((%x. a + x) ` S)" + using mem_rel_interior[of "a+x" "((%x. a + x) ` S)"] by auto +} from this show ?thesis by auto +qed + +lemma rel_interior_translation: +fixes a :: "'n::euclidean_space" +shows "rel_interior ((%x. a + x) ` S) = ((%x. a + x) ` rel_interior S)" +proof- +have "(%x. (-a) + x) ` rel_interior ((%x. a + x) ` S) <= rel_interior S" + using rel_interior_translation_aux[of "-a" "(%x. a + x) ` S"] + translation_assoc[of "-a" "a"] by auto +hence "((%x. a + x) ` rel_interior S) >= rel_interior ((%x. a + x) ` S)" + using translation_inverse_subset[of a "rel_interior (op + a ` S)" "rel_interior S"] + by auto +from this show ?thesis using rel_interior_translation_aux[of a S] by auto +qed + + +lemma affine_hull_linear_image: +assumes "bounded_linear f" +shows "f ` (affine hull s) = affine hull f ` s" +(* Proof is a modified copy of the proof of similar lemma convex_hull_linear_image +*) + apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 + apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption + apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption +proof- + interpret f: bounded_linear f by fact + show "affine {x. f x : affine hull f ` s}" + unfolding affine_def by(auto simp add: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format]) next + interpret f: bounded_linear f by fact + show "affine {x. x : f ` (affine hull s)}" using affine_affine_hull[unfolded affine_def, of s] + unfolding affine_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric]) +qed auto + + +lemma rel_interior_injective_on_span_linear_image: +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" +fixes S :: "('m::euclidean_space) set" +assumes "bounded_linear f" and "inj_on f (span S)" +shows "rel_interior (f ` S) = f ` (rel_interior S)" +proof- +{ fix z assume z_def: "z : rel_interior (f ` S)" + have "z : f ` S" using z_def rel_interior_subset[of "f ` S"] by auto + from this obtain x where x_def: "x : S & (f x = z)" by auto + obtain e2 where e2_def: "e2>0 & cball z e2 Int affine hull (f ` S) <= (f ` S)" + using z_def rel_interior_cball[of "f ` S"] by auto + obtain K where K_def: "K>0 & (! x. norm (f x) <= norm x * K)" + using assms RealVector.bounded_linear.pos_bounded[of f] by auto + def e1 == "1/K" hence e1_def: "e1>0 & (! x. e1 * norm (f x) <= norm x)" + using K_def pos_le_divide_eq[of e1] by auto + def e == "e1 * e2" hence "e>0" using e1_def e2_def real_mult_order by auto + { fix y assume y_def: "y : cball x e Int affine hull S" + from this have h1: "f y : affine hull (f ` S)" + using affine_hull_linear_image[of f S] assms by auto + from y_def have "norm (x-y)<=e1 * e2" + using cball_def[of x e] dist_norm[of x y] e_def by auto + moreover have "(f x)-(f y)=f (x-y)" + using assms linear_sub[of f x y] linear_conv_bounded_linear[of f] by auto + moreover have "e1 * norm (f (x-y)) <= norm (x-y)" using e1_def by auto + ultimately have "e1 * norm ((f x)-(f y)) <= e1 * e2" by auto + hence "(f y) : (cball z e2)" + using cball_def[of "f x" e2] dist_norm[of "f x" "f y"] e1_def x_def by auto + hence "f y : (f ` S)" using y_def e2_def h1 by auto + hence "y : S" using assms y_def hull_subset[of S] affine_hull_subset_span + inj_on_image_mem_iff[of f "span S" S y] by auto + } + hence "z : f ` (rel_interior S)" using mem_rel_interior_cball[of x S] `e>0` x_def by auto +} +moreover +{ fix x assume x_def: "x : rel_interior S" + from this obtain e2 where e2_def: "e2>0 & cball x e2 Int affine hull S <= S" + using rel_interior_cball[of S] by auto + have "x : S" using x_def rel_interior_subset by auto + hence *: "f x : f ` S" by auto + have "! x:span S. f x = 0 --> x = 0" + using assms subspace_span linear_conv_bounded_linear[of f] + linear_injective_on_subspace_0[of f "span S"] by auto + from this obtain e1 where e1_def: "e1>0 & (! x : span S. e1 * norm x <= norm (f x))" + using assms injective_imp_isometric[of "span S" f] + subspace_span[of S] closed_subspace[of "span S"] by auto + def e == "e1 * e2" hence "e>0" using e1_def e2_def real_mult_order by auto + { fix y assume y_def: "y : cball (f x) e Int affine hull (f ` S)" + from this have "y : f ` (affine hull S)" using affine_hull_linear_image[of f S] assms by auto + from this obtain xy where xy_def: "xy : affine hull S & (f xy = y)" by auto + from this y_def have "norm ((f x)-(f xy))<=e1 * e2" + using cball_def[of "f x" e] dist_norm[of "f x" y] e_def by auto + moreover have "(f x)-(f xy)=f (x-xy)" + using assms linear_sub[of f x xy] linear_conv_bounded_linear[of f] by auto + moreover have "x-xy : span S" + using subspace_sub[of "span S" x xy] subspace_span `x : S` xy_def + affine_hull_subset_span[of S] span_inc by auto + moreover hence "e1 * norm (x-xy) <= norm (f (x-xy))" using e1_def by auto + ultimately have "e1 * norm (x-xy) <= e1 * e2" by auto + hence "xy : (cball x e2)" using cball_def[of x e2] dist_norm[of x xy] e1_def by auto + hence "y : (f ` S)" using xy_def e2_def by auto + } + hence "(f x) : rel_interior (f ` S)" + using mem_rel_interior_cball[of "(f x)" "(f ` S)"] * `e>0` by auto +} +ultimately show ?thesis by auto +qed + +lemma rel_interior_injective_linear_image: +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" +assumes "bounded_linear f" and "inj f" +shows "rel_interior (f ` S) = f ` (rel_interior S)" +using assms rel_interior_injective_on_span_linear_image[of f S] + subset_inj_on[of f "UNIV" "span S"] by auto + +subsection{* Some Properties of subset of standard basis *} + +lemma affine_hull_substd_basis: assumes "d\{.. x$$i = 0)}" + (is "affine hull (insert 0 ?A) = ?B") +proof- have *:"\A. op + (0\'a) ` A = A" "\A. op + (- (0\'a)) ` A = A" by auto + show ?thesis unfolding affine_hull_insert_span_gen span_substd_basis[OF assms,THEN sym] * .. +qed + +lemma affine_hull_convex_hull: "affine hull (convex hull S) = affine hull S" +by (metis Int_absorb1 Int_absorb2 convex_hull_subset_affine_hull hull_hull hull_mono hull_subset) + subsection {* Openness and compactness are preserved by convex hull operation. *} lemma open_convex_hull[intro]: @@ -1525,6 +3105,61 @@ "convex hull ((\x. a + c *\<^sub>R x) ` s) = (\x. a + c *\<^sub>R x) ` (convex hull s)" by(simp only: image_image[THEN sym] convex_hull_scaling convex_hull_translation) +subsection {* Convexity of cone hulls *} + +lemma convex_cone_hull: +fixes S :: "('m::euclidean_space) set" +assumes "convex S" +shows "convex (cone hull S)" +proof- +{ fix x y assume xy_def: "x : cone hull S & y : cone hull S" + hence "S ~= {}" using cone_hull_empty_iff[of S] by auto + fix u v assume uv_def: "u>=0 & v>=0 & (u :: real)+v=1" + hence *: "u *\<^sub>R x : cone hull S & v *\<^sub>R y : cone hull S" + using cone_cone_hull[of S] xy_def cone_def[of "cone hull S"] by auto + from * obtain cx xx where x_def: "u *\<^sub>R x = cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" + using cone_hull_expl[of S] by auto + from * obtain cy yy where y_def: "v *\<^sub>R y = cy *\<^sub>R yy & (cy :: real)>=0 & yy : S" + using cone_hull_expl[of S] by auto + { assume "cx+cy<=0" hence "u *\<^sub>R x=0 & v *\<^sub>R y=0" using x_def y_def by auto + hence "u *\<^sub>R x+ v *\<^sub>R y = 0" by auto + hence "u *\<^sub>R x+ v *\<^sub>R y : cone hull S" using cone_hull_contains_0[of S] `S ~= {}` by auto + } + moreover + { assume "cx+cy>0" + hence "(cx/(cx+cy)) *\<^sub>R xx + (cy/(cx+cy)) *\<^sub>R yy : S" + using assms mem_convex_alt[of S xx yy cx cy] x_def y_def by auto + hence "cx *\<^sub>R xx + cy *\<^sub>R yy : cone hull S" + using mem_cone_hull[of "(cx/(cx+cy)) *\<^sub>R xx + (cy/(cx+cy)) *\<^sub>R yy" S "cx+cy"] + `cx+cy>0` by (auto simp add: scaleR_right_distrib) + hence "u *\<^sub>R x+ v *\<^sub>R y : cone hull S" using x_def y_def by auto + } + moreover have "(cx+cy<=0) | (cx+cy>0)" by auto + ultimately have "u *\<^sub>R x+ v *\<^sub>R y : cone hull S" by blast +} from this show ?thesis unfolding convex_def by auto +qed + +lemma cone_convex_hull: +fixes S :: "('m::euclidean_space) set" +assumes "cone S" +shows "cone (convex hull S)" +proof- +{ assume "S = {}" hence ?thesis by auto } +moreover +{ assume "S ~= {}" hence *: "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto + { fix c assume "(c :: real)>0" + hence "op *\<^sub>R c ` (convex hull S) = convex hull (op *\<^sub>R c ` S)" + using convex_hull_scaling[of _ S] by auto + also have "...=convex hull S" using * `c>0` by auto + finally have "op *\<^sub>R c ` (convex hull S) = convex hull S" by auto + } + hence "0 : convex hull S & (!c. c>0 --> (op *\<^sub>R c ` (convex hull S)) = (convex hull S))" + using * hull_subset[of S convex] by auto + hence ?thesis using `S ~= {}` cone_iff[of "convex hull S"] by auto +} +ultimately show ?thesis by blast +qed + subsection {* Convex set as intersection of halfspaces. *} lemma convex_halfspace_intersection: @@ -1653,28 +3288,6 @@ shows "\ f \{}" apply(rule helly_induct) using assms by auto -subsection {* Convex hull is "preserved" by a linear function. *} - -lemma convex_hull_linear_image: - assumes "bounded_linear f" - shows "f ` (convex hull s) = convex hull (f ` s)" - apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 - apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption - apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption -proof- - interpret f: bounded_linear f by fact - show "convex {x. f x \ convex hull f ` s}" - unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next - interpret f: bounded_linear f by fact - show "convex {x. x \ f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s] - unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric]) -qed auto - -lemma in_convex_hull_linear_image: - assumes "bounded_linear f" "x \ convex hull s" - shows "(f x) \ convex hull (f ` s)" -using convex_hull_linear_image[OF assms(1)] assms(2) by auto - subsection {* Homeomorphism of all convex compact sets with nonempty interior. *} lemma compact_frontier_line_lemma: @@ -2459,43 +4072,49 @@ apply(rule_tac x=u in exI) defer apply(rule_tac x="\x. if x = 0 then 1 - setsum u s else u x" in exI) using assms(2) unfolding if_smult and setsum_delta_notmem[OF assms(2)] by auto +lemma substd_simplex: assumes "d\{.. x$$i = 0)}" + (is "convex hull (insert 0 ?p) = ?s") +(* Proof is a modified copy of the proof of similar lemma std_simplex in Convex_Euclidean_Space.thy *) +proof- let ?D = d (*"{.. ?D} = basis ` ?D" by auto + note sumbas = this setsum_reindex[OF basis_inj_on[of d], unfolded o_def, OF assms] + show ?thesis unfolding simplex[OF finite_substdbasis `0 ~: ?p`] + apply(rule set_eqI) unfolding mem_Collect_eq apply rule + apply(erule exE, (erule conjE)+) apply(erule_tac[2] conjE)+ proof- + fix x::"'a::euclidean_space" and u assume as: "\x\{basis i |i. i \?D}. 0 \ u x" + "setsum u {basis i |i. i \ ?D} \ 1" "(\x\{basis i |i. i \?D}. u x *\<^sub>R x) = x" + have *:"\i u (basis i) = x$$i" and "(!i x $$ i = 0)" using as(3) + unfolding sumbas unfolding substdbasis_expansion_unique[OF assms] by auto + hence **:"setsum u {basis i |i. i \ ?D} = setsum (op $$ x) ?D" unfolding sumbas + apply-apply(rule setsum_cong2) using assms by auto + have " (\i x$$i) \ setsum (op $$ x) ?D \ 1" + apply - proof(rule,rule,rule) + fix i assume i:"i 0 \ x$$i" unfolding *[rule_format,OF i,THEN sym] + apply(rule_tac as(1)[rule_format]) by auto + moreover have "i ~: d ==> 0 \ x$$i" + using `(!i x $$ i = 0)`[rule_format, OF i] by auto + ultimately show "0 \ x$$i" by auto + qed(insert as(2)[unfolded **], auto) + from this show " (\i x$$i) \ setsum (op $$ x) ?D \ 1 & (!i x $$ i = 0)" + using `(!i x $$ i = 0)` by auto + next fix x::"'a::euclidean_space" assume as:"\i x $$ i" "setsum (op $$ x) ?D \ 1" + "(!i x $$ i = 0)" + show "\u. (\x\{basis i |i. i \ ?D}. 0 \ u x) \ + setsum u {basis i |i. i \ ?D} \ 1 \ (\x\{basis i |i. i \ ?D}. u x *\<^sub>R x) = x" + apply(rule_tac x="\y. inner y x" in exI) apply(rule,rule) unfolding mem_Collect_eq apply(erule exE) + using as(1) apply(erule_tac x=i in allE) unfolding sumbas apply safe unfolding not_less basis_zero + unfolding substdbasis_expansion_unique[OF assms] euclidean_component_def[THEN sym] + using as(2,3) by(auto simp add:dot_basis not_less basis_zero) + qed qed + lemma std_simplex: "convex hull (insert 0 { basis i | i. ii x$$i) \ setsum (\i. x$$i) {.. 1 }" - (is "convex hull (insert 0 ?p) = ?s") -proof- let ?D = "{..?p" by auto - have "{(basis i)::'a |i. ix\{basis i |i. i u x" - "setsum u {basis i |i. i 1" "(\x\{basis i |i. iR x) = x" - have *:"\iji x $$ i) \ setsum (op $$ x) ?D \ 1" apply - proof(rule,rule,rule) - fix i assume i:"i x$$i" unfolding *[rule_format,OF i,THEN sym] - apply(rule_tac as(1)[rule_format]) using i by auto - qed(insert as(2)[unfolded **], auto) - next fix x::"'a" assume as:"\i x $$ i" "setsum (op $$ x) ?D \ 1" - show "\u. (\x\{basis i |i. i u x) \ - setsum u {basis i |i. i 1 \ (\x\{basis i |i. iR x) = x" - apply(rule_tac x="\y. inner y x" in exI) apply safe using as(1) - proof- show "(\y\{basis i |i. i < DIM('a)}. y \ x) \ 1" unfolding sumbas - using as(2) unfolding euclidean_component_def[THEN sym] . - show "(\xa\{basis i |i. i < DIM('a)}. (xa \ x) *\<^sub>R xa) = x" unfolding sumbas - apply(subst (7) euclidean_representation) apply(rule setsum_cong2) - unfolding euclidean_component_def by auto - qed (auto simp add:euclidean_component_def) - qed qed + using substd_simplex[of "{.. < 1" unfolding setsum_constant card_enum real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps) finally show "setsum (op $$ ?a) ?D < 1" by auto qed qed +lemma rel_interior_substd_simplex: assumes "d\{..i\d. 0 < x$$i) & setsum (%i. x$$i) d < 1 & (!i x$$i = 0)}" + (is "rel_interior (convex hull (insert 0 ?p)) = ?s") +(* Proof is a modified copy of the proof of similar lemma interior_std_simplex in Convex_Euclidean_Space.thy *) +proof- +have "finite d" apply(rule finite_subset) using assms by auto +{ assume "d={}" hence ?thesis using rel_interior_sing using euclidean_eq[of _ 0] by auto } +moreover +{ assume "d~={}" +have h0: "affine hull (convex hull (insert 0 ?p))={x::'a::euclidean_space. (!i x$$i = 0)}" + using affine_hull_convex_hull affine_hull_substd_basis assms by auto +have aux: "!x::'n::euclidean_space. !i. ((! i:d. 0 <= x$$i) & (!i. i ~: d --> x$$i = 0))--> 0 <= x$$i" by auto +{ fix x::"'a::euclidean_space" assume x_def: "x : rel_interior (convex hull (insert 0 ?p))" + from this obtain e where e0: "e>0" and + "ball x e Int {xa. (!i xa$$i = 0)} <= convex hull (insert 0 ?p)" + using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto + hence as: "ALL xa. (dist x xa < e & (!i xa$$i = 0)) --> + (!i : d. 0 <= xa $$ i) & setsum (op $$ xa) d <= 1" + unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto + have x0: "(!i x$$i = 0)" + using x_def rel_interior_subset substd_simplex[OF assms] by auto + have "(!i : d. 0 < x $$ i) & setsum (op $$ x) d < 1 & (!i x$$i = 0)" apply(rule,rule) + proof- + fix i::nat assume "i:d" + hence "\ia\d. 0 \ (x - (e / 2) *\<^sub>R basis i) $$ ia" apply-apply(rule as[rule_format,THEN conjunct1]) + unfolding dist_norm using assms `e>0` x0 by auto + thus "0 < x $$ i" apply(erule_tac x=i in ballE) using `e>0` `i\d` assms by auto + next obtain a where a:"a:d" using `d ~= {}` by auto + have **:"dist x (x + (e / 2) *\<^sub>R basis a) < e" + using `e>0` and Euclidean_Space.norm_basis[of a] + unfolding dist_norm by auto + have "\i. (x + (e / 2) *\<^sub>R basis a) $$ i = x$$i + (if i = a then e/2 else 0)" + unfolding euclidean_simps using a assms by auto + hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis a)) d = + setsum (\i. x$$i + (if a = i then e/2 else 0)) d" by(rule_tac setsum_cong, auto) + have h1: "(ALL i (x + (e / 2) *\<^sub>R basis a) $$ i = 0)" + using as[THEN spec[where x="x + (e / 2) *\<^sub>R basis a"]] `a:d` using x0 + by(auto simp add: norm_basis elim:allE[where x=a]) + have "setsum (op $$ x) d < setsum (op $$ (x + (e / 2) *\<^sub>R basis a)) d" unfolding * setsum_addf + using `0 \ 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R basis a"] by auto + finally show "setsum (op $$ x) d < 1 & (!i x$$i = 0)" using x0 by auto + qed +} +moreover +{ + fix x::"'a::euclidean_space" assume as: "x : ?s" + have "!i. ((0 0<=x$$i)" by auto + moreover have "!i. (i:d) | (i ~: d)" by auto + ultimately + have "!i. ( (ALL i:d. 0 < x$$i) & (ALL i. i ~: d --> x$$i = 0) ) --> 0 <= x$$i" by metis + hence h2: "x : convex hull (insert 0 ?p)" using as assms + unfolding substd_simplex[OF assms] by fastsimp + obtain a where a:"a:d" using `d ~= {}` by auto + let ?d = "(1 - setsum (op $$ x) d) / real (card d)" + have "card d >= 1" using `d ~={}` card_ge1[of d] using `finite d` by auto + have "Min ((op $$ x) ` d) > 0" apply(rule Min_grI) using as `card d >= 1` `finite d` by auto + moreover have "?d > 0" apply(rule divide_pos_pos) using as using `card d >= 1` by(auto simp add: Suc_le_eq) + ultimately have h3: "min (Min ((op $$ x) ` d)) ?d > 0" by auto + + have "x : rel_interior (convex hull (insert 0 ?p))" + unfolding rel_interior_ball mem_Collect_eq h0 apply(rule,rule h2) + unfolding substd_simplex[OF assms] + apply(rule_tac x="min (Min ((op $$ x) ` d)) ?d" in exI) apply(rule,rule h3) apply safe unfolding mem_ball + proof- fix y::'a assume y:"dist x y < min (Min (op $$ x ` d)) ?d" and y2:"(!i y$$i = 0)" + have "setsum (op $$ y) d \ setsum (\i. x$$i + ?d) d" proof(rule setsum_mono) + fix i assume i:"i\d" + have "abs (y$$i - x$$i) < ?d" apply(rule le_less_trans) using component_le_norm[of "y - x" i] + using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] + by(auto simp add: norm_minus_commute) + thus "y $$ i \ x $$ i + ?d" by auto qed + also have "\ \ 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat + using `card d >= 1` by(auto simp add: Suc_le_eq) + finally show "setsum (op $$ y) d \ 1" . + + fix i assume "i y$$i" + proof(cases "i\d") case True + have "norm (x - y) < x$$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1] + using Min_gr_iff[of "op $$ x ` d" "norm (x - y)"] `card d >= 1` `i:d` + apply auto by (metis Suc_n_not_le_n True card_eq_0_iff finite_imageI) + thus "0 \ y$$i" using component_le_norm[of "x - y" i] and as(1)[rule_format] by auto + qed(insert y2, auto) + qed +} ultimately have + "!!x :: 'a::euclidean_space. (x : rel_interior (convex hull insert 0 {basis i |i. i : d})) = + (x : {x. (ALL i:d. 0 < x $$ i) & + setsum (op $$ x) d < 1 & (ALL i x $$ i = 0)})" by blast +from this have ?thesis by (rule set_eqI) +} ultimately show ?thesis by blast +qed + +lemma rel_interior_substd_simplex_nonempty: assumes "d ~={}" "d\{.. ?D} = basis ` ?D" by auto + have "finite d" apply(rule finite_subset) using assms(2) by auto + hence d1: "real(card d) >= 1" using `d ~={}` card_ge1[of d] by auto + { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))" + unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def + apply(rule trans[of _ "setsum (\j. if i = j then inverse (2 * real (card d)) else 0) ?D"]) + unfolding euclidean_component.setsum + apply(rule setsum_cong2) + using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2) + by (auto simp add: Euclidean_Space.basis_component[of i])} + note ** = this + show ?thesis apply(rule that[of ?a]) unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq + proof safe fix i assume "i:d" + have "0 < inverse (2 * real (card d))" using d1 by(auto simp add: Suc_le_eq) + also have "...=?a $$ i" using **[of i] `i:d` by auto + finally show "0 < ?a $$ i" by auto + next have "setsum (op $$ ?a) ?D = setsum (\i. inverse (2 * real (card d))) ?D" + by(rule setsum_cong2, rule **) + also have "\ < 1" unfolding setsum_constant card_enum real_eq_of_nat real_divide_def[THEN sym] + by (auto simp add:field_simps) + finally show "setsum (op $$ ?a) ?D < 1" by auto + next fix i assume "iR (2 * real (card d)))" "{basis i |i. i : d}"]) + using finite_substdbasis[of d] apply blast + proof- + { fix x assume "(x :: 'a::euclidean_space): {basis i |i. i : d}" + hence "x : span {basis i |i. i : d}" + using span_superset[of _ "{basis i |i. i : d}"] by auto + hence "(x /\<^sub>R (2 * real (card d))) : (span {basis i |i. i : d})" + using span_mul[of x "{basis i |i. i : d}" "(inverse (real (card d)) / 2)"] by auto + } thus "\x\{basis i |i. i \ d}. x /\<^sub>R (2 * real (card d)) \ span {basis i ::'a |i. i \ d}" by auto + qed + thus "?a $$ i = 0 " using `i~:d` unfolding span_substd_basis[OF assms(2)] using `i'n" where fd: "card d = card B & linear f & f ` B = {basis i |i. i : (d :: nat set)} & + f ` span B = {x. ALL i x $$ i = (0::real)} & inj_on f (span B)" and d:"d\{.. S = {}" +proof- +{ assume "S ~= {}" from this obtain a where "a : S" by auto + hence "0 : op + (-a) ` S" using assms exI[of "(%x. x:S & -a+x=0)" a] by auto + hence "rel_interior (op + (-a) ` S) ~= {}" + using rel_interior_convex_nonempty_aux[of "op + (-a) ` S"] + convex_translation[of S "-a"] assms by auto + hence "rel_interior S ~= {}" using rel_interior_translation by auto +} from this show ?thesis using rel_interior_empty by auto +qed + +lemma convex_rel_interior: +fixes S :: "(_::euclidean_space) set" +assumes "convex S" +shows "convex (rel_interior S)" +proof- +{ fix "x" "y" "u" + assume assm: "x:rel_interior S" "y:rel_interior S" "0<=u" "(u :: real) <= 1" + hence "x:S" using rel_interior_subset by auto + have "x - u *\<^sub>R (x-y) : rel_interior S" + proof(cases "0=u") + case False hence "0R x + u *\<^sub>R y : rel_interior S" by (simp add: algebra_simps) +} from this show ?thesis unfolding convex_alt by auto +qed + +lemma convex_closure_rel_interior: +fixes S :: "('n::euclidean_space) set" +assumes "convex S" +shows "closure(rel_interior S) = closure S" +proof- +have h1: "closure(rel_interior S) <= closure S" + using subset_closure[of "rel_interior S" S] rel_interior_subset[of S] by auto +{ assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S" + using rel_interior_convex_nonempty assms by auto + { fix x assume x_def: "x : closure S" + { assume "x=a" hence "x : closure(rel_interior S)" using a_def unfolding closure_def by auto } + moreover + { assume "x ~= a" + { fix e :: real assume e_def: "e>0" + def e1 == "min 1 (e/norm (x - a))" hence e1_def: "e1>0 & e1<=1 & e1*norm(x-a)<=e" + using `x ~= a` `e>0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm(x-a)"] by simp + hence *: "x - e1 *\<^sub>R (x - a) : rel_interior S" + using rel_interior_closure_convex_shrink[of S a x e1] assms x_def a_def e1_def by auto + have "EX y. y:rel_interior S & y ~= x & (dist y x) <= e" + apply (rule_tac x="x - e1 *\<^sub>R (x - a)" in exI) + using * e1_def dist_norm[of "x - e1 *\<^sub>R (x - a)" x] `x ~= a` by simp + } hence "x islimpt rel_interior S" unfolding islimpt_approachable_le by auto + hence "x : closure(rel_interior S)" unfolding closure_def by auto + } ultimately have "x : closure(rel_interior S)" by auto + } hence ?thesis using h1 by auto +} +moreover +{ assume "S = {}" hence "rel_interior S = {}" using rel_interior_empty by auto + hence "closure(rel_interior S) = {}" using closure_empty by auto + hence ?thesis using `S={}` by auto +} ultimately show ?thesis by blast +qed + +lemma rel_interior_same_affine_hull: + fixes S :: "('n::euclidean_space) set" + assumes "convex S" + shows "affine hull (rel_interior S) = affine hull S" +by (metis assms closure_same_affine_hull convex_closure_rel_interior) + +lemma rel_interior_aff_dim: + fixes S :: "('n::euclidean_space) set" + assumes "convex S" + shows "aff_dim (rel_interior S) = aff_dim S" +by (metis aff_dim_affine_hull2 assms rel_interior_same_affine_hull) + +lemma rel_interior_rel_interior: + fixes S :: "('n::euclidean_space) set" + assumes "convex S" + shows "rel_interior (rel_interior S) = rel_interior S" +proof- +have "openin (subtopology euclidean (affine hull (rel_interior S))) (rel_interior S)" + using opein_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto +from this show ?thesis using rel_interior_def by auto +qed + +lemma rel_interior_rel_open: + fixes S :: "('n::euclidean_space) set" + assumes "convex S" + shows "rel_open (rel_interior S)" +unfolding rel_open_def using rel_interior_rel_interior assms by auto + +lemma convex_rel_interior_closure_aux: + fixes x y z :: "_::euclidean_space" + assumes "0 < a" "0 < b" "(a+b) *\<^sub>R z = a *\<^sub>R x + b *\<^sub>R y" + obtains e where "0 < e" "e <= 1" "z = y - e *\<^sub>R (y-x)" +proof- +def e == "a/(a+b)" +have "z = (1 / (a + b)) *\<^sub>R ((a + b) *\<^sub>R z)" apply auto using assms by simp +also have "... = (1 / (a + b)) *\<^sub>R (a *\<^sub>R x + b *\<^sub>R y)" using assms + scaleR_cancel_left[of "1/(a+b)" "(a + b) *\<^sub>R z" "a *\<^sub>R x + b *\<^sub>R y"] by auto +also have "... = y - e *\<^sub>R (y-x)" using e_def apply (simp add: algebra_simps) + using scaleR_left_distrib[of "a/(a+b)" "b/(a+b)" y] assms add_divide_distrib[of a b "a+b"] by auto +finally have "z = y - e *\<^sub>R (y-x)" by auto +moreover have "0= rel_interior S" + using subset_rel_interior[of S "closure S"] closure_same_affine_hull closure_subset by auto + moreover + { fix z assume z_def: "z : rel_interior (closure S)" + obtain x where x_def: "x : rel_interior S" + using `S ~= {}` assms rel_interior_convex_nonempty by auto + { assume "x=z" hence "z : rel_interior S" using x_def by auto } + moreover + { assume "x ~= z" + obtain e where e_def: "e > 0 & cball z e Int affine hull closure S <= closure S" + using z_def rel_interior_cball[of "closure S"] by auto + hence *: "0 < e/norm(z-x)" using e_def `x ~= z` divide_pos_pos[of e "norm(z-x)"] by auto + def y == "z + (e/norm(z-x)) *\<^sub>R (z-x)" + have yball: "y : cball z e" + using mem_cball y_def dist_norm[of z y] e_def by auto + have "x : affine hull closure S" + using x_def rel_interior_subset_closure hull_inc[of x "closure S"] by auto + moreover have "z : affine hull closure S" + using z_def rel_interior_subset hull_subset[of "closure S"] by auto + ultimately have "y : affine hull closure S" + using y_def affine_affine_hull[of "closure S"] + mem_affine_3_minus [of "affine hull closure S" z z x "e/norm(z-x)"] by auto + hence "y : closure S" using e_def yball by auto + have "(1+(e/norm(z-x))) *\<^sub>R z = (e/norm(z-x)) *\<^sub>R x + y" + using y_def by (simp add: algebra_simps) + from this obtain e1 where "0 < e1 & e1 <= 1 & z = y - e1 *\<^sub>R (y - x)" + using * convex_rel_interior_closure_aux[of "e / norm (z - x)" 1 z x y] + by (auto simp add: algebra_simps) + hence "z : rel_interior S" + using rel_interior_closure_convex_shrink assms x_def `y : closure S` by auto + } ultimately have "z : rel_interior S" by auto + } ultimately have ?thesis by auto +} ultimately show ?thesis by blast +qed + +lemma convex_interior_closure: +fixes S :: "('n::euclidean_space) set" +assumes "convex S" +shows "interior (closure S) = interior S" +using closure_aff_dim[of S] interior_rel_interior_gen[of S] interior_rel_interior_gen[of "closure S"] + convex_rel_interior_closure[of S] assms by auto + +lemma closure_eq_rel_interior_eq: +fixes S1 S2 :: "('n::euclidean_space) set" +assumes "convex S1" "convex S2" +shows "(closure S1 = closure S2) <-> (rel_interior S1 = rel_interior S2)" + by (metis convex_rel_interior_closure convex_closure_rel_interior assms) + + +lemma closure_eq_between: +fixes S1 S2 :: "('n::euclidean_space) set" +assumes "convex S1" "convex S2" +shows "(closure S1 = closure S2) <-> + ((rel_interior S1 <= S2) & (S2 <= closure S1))" (is "?A <-> ?B") +proof- +have "?A --> ?B" by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset) +moreover have "?B --> (closure S1 <= closure S2)" + by (metis assms(1) convex_closure_rel_interior subset_closure) +moreover have "?B --> (closure S1 >= closure S2)" by (metis closed_closure closure_minimal) +ultimately show ?thesis by blast +qed + +lemma open_inter_closure_rel_interior: +fixes S A :: "('n::euclidean_space) set" +assumes "convex S" "open A" +shows "((A Int closure S) = {}) <-> ((A Int rel_interior S) = {})" +by (metis assms convex_closure_rel_interior open_inter_closure_eq_empty) + +definition "rel_frontier S = closure S - rel_interior S" + +lemma closed_affine_hull: "closed (affine hull ((S :: ('n::euclidean_space) set)))" +by (metis affine_affine_hull affine_closed) + +lemma closed_rel_frontier: "closed(rel_frontier (S :: ('n::euclidean_space) set))" +proof- +have *: "closedin (subtopology euclidean (affine hull S)) (closure S - rel_interior S)" +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] + closure_affine_hull[of S] opein_rel_interior[of S] by auto +show ?thesis apply (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"]) + unfolding rel_frontier_def using * closed_affine_hull by auto +qed + + +lemma convex_rel_frontier_aff_dim: +fixes S1 S2 :: "('n::euclidean_space) set" +assumes "convex S1" "convex S2" "S2 ~= {}" +assumes "S1 <= rel_frontier S2" +shows "aff_dim S1 < aff_dim S2" +proof- +have "S1 <= closure S2" using assms unfolding rel_frontier_def by auto +hence *: "affine hull S1 <= affine hull S2" + using hull_mono[of "S1" "closure S2"] closure_same_affine_hull[of S2] by auto +hence "aff_dim S1 <= aff_dim S2" using * aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2] + aff_dim_subset[of "affine hull S1" "affine hull S2"] by auto +moreover +{ assume eq: "aff_dim S1 = aff_dim S2" + hence "S1 ~= {}" using aff_dim_empty[of S1] aff_dim_empty[of S2] `S2 ~= {}` by auto + have **: "affine hull S1 = affine hull S2" + apply (rule affine_dim_equal) using * affine_affine_hull apply auto + using `S1 ~= {}` hull_subset[of S1] apply auto + using eq aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2] by auto + obtain a where a_def: "a : rel_interior S1" + using `S1 ~= {}` rel_interior_convex_nonempty assms by auto + obtain T where T_def: "open T & a : T Int S1 & T Int affine hull S1 <= S1" + using mem_rel_interior[of a S1] a_def by auto + hence "a : T Int closure S2" using a_def assms unfolding rel_frontier_def by auto + from this obtain b where b_def: "b : T Int rel_interior S2" + using open_inter_closure_rel_interior[of S2 T] assms T_def by auto + hence "b : affine hull S1" using rel_interior_subset hull_subset[of S2] ** by auto + hence "b : S1" using T_def b_def by auto + hence False using b_def assms unfolding rel_frontier_def by auto +} ultimately show ?thesis using zless_le by auto +qed + + +lemma convex_rel_interior_if: +fixes S :: "('n::euclidean_space) set" +assumes "convex S" +assumes "z : rel_interior S" +shows "(!x:affine hull S. EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S ))" +proof- +obtain e1 where e1_def: "e1>0 & cball z e1 Int affine hull S <= S" + using mem_rel_interior_cball[of z S] assms by auto +{ fix x assume x_def: "x:affine hull S" + { assume "x ~= z" + def m == "1+e1/norm(x-z)" + hence "m>1" using e1_def `x ~= z` divide_pos_pos[of e1 "norm (x - z)"] by auto + { fix e assume e_def: "e>1 & e<=m" + have "z : affine hull S" using assms rel_interior_subset hull_subset[of S] by auto + hence *: "(1-e)*\<^sub>R x+ e *\<^sub>R z : affine hull S" + using mem_affine[of "affine hull S" x z "(1-e)" e] affine_affine_hull[of S] x_def by auto + have "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) = norm ((e - 1) *\<^sub>R (x-z))" by (simp add: algebra_simps) + also have "...= (e - 1) * norm(x-z)" using norm_scaleR e_def by auto + also have "...<=(m - 1) * norm(x-z)" using e_def mult_right_mono[of _ _ "norm(x-z)"] by auto + also have "...= (e1 / norm (x - z)) * norm (x - z)" using m_def by auto + also have "...=e1" using `x ~= z` e1_def by simp + finally have **: "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) <= e1" by auto + have "(1-e)*\<^sub>R x+ e *\<^sub>R z : cball z e1" + using m_def ** unfolding cball_def dist_norm by (auto simp add: algebra_simps) + hence "(1-e)*\<^sub>R x+ e *\<^sub>R z : S" using e_def * e1_def by auto + } 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 + } + moreover + { assume "x=z" def m == "1+e1" hence "m>1" using e1_def by auto + { fix e assume e_def: "e>1 & e<=m" + hence "(1-e)*\<^sub>R x+ e *\<^sub>R z : S" + using e1_def x_def `x=z` by (auto simp add: algebra_simps) + hence "(1-e)*\<^sub>R x+ e *\<^sub>R z : S" using e_def by auto + } 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 + } ultimately have "EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S )" by auto +} from this show ?thesis by auto +qed + +lemma convex_rel_interior_if2: +fixes S :: "('n::euclidean_space) set" +assumes "convex S" +assumes "z : rel_interior S" +shows "(!x:affine hull S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)" +using convex_rel_interior_if[of S z] assms by auto + +lemma convex_rel_interior_only_if: +fixes S :: "('n::euclidean_space) set" +assumes "convex S" "S ~= {}" +assumes "(!x:S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)" +shows "z : rel_interior S" +proof- +obtain x where x_def: "x : rel_interior S" using rel_interior_convex_nonempty assms by auto +hence "x:S" using rel_interior_subset by auto +from this obtain e where e_def: "e>1 & (1 - e) *\<^sub>R x + e *\<^sub>R z : S" using assms by auto +def y == "(1 - e) *\<^sub>R x + e *\<^sub>R z" hence "y:S" using e_def by auto +def e1 == "1/e" hence "0R (y-x)" using e1_def y_def by (auto simp add: algebra_simps) +from this show ?thesis + using rel_interior_convex_shrink[of S x y "1-e1"] `0 (!x:S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)" +using assms hull_subset[of S "affine"] + convex_rel_interior_if[of S z] convex_rel_interior_only_if[of S z] by auto + +lemma convex_rel_interior_iff2: +fixes S :: "('n::euclidean_space) set" +assumes "convex S" "S ~= {}" +shows "z : rel_interior S <-> (!x:affine hull S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)" +using assms hull_subset[of S] + convex_rel_interior_if2[of S z] convex_rel_interior_only_if[of S z] by auto + + +lemma convex_interior_iff: +fixes S :: "('n::euclidean_space) set" +assumes "convex S" +shows "z : interior S <-> (!x. EX e. e>0 & z+ e *\<^sub>R x : S)" +proof- +{ assume a: "~(aff_dim S = int DIM('n))" + { assume "z : interior S" + hence False using a interior_rel_interior_gen[of S] by auto + } + moreover + { assume r: "!x. EX e. e>0 & z+ e *\<^sub>R x : S" + { fix x obtain e1 where e1_def: "e1>0 & z+ e1 *\<^sub>R (x-z) : S" using r by auto + obtain e2 where e2_def: "e2>0 & z+ e2 *\<^sub>R (z-x) : S" using r by auto + def x1 == "z+ e1 *\<^sub>R (x-z)" + hence x1: "x1 : affine hull S" using e1_def hull_subset[of S] by auto + def x2 == "z+ e2 *\<^sub>R (z-x)" + hence x2: "x2 : affine hull S" using e2_def hull_subset[of S] by auto + have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using divide.add[of e1 e2 "e1+e2"] e1_def e2_def by simp + hence "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2" + using x1_def x2_def apply (auto simp add: algebra_simps) + using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] by auto + hence z: "z : affine hull S" + using mem_affine[of "affine hull S" x1 x2 "e2/(e1+e2)" "e1/(e1+e2)"] + x1 x2 affine_affine_hull[of S] * by auto + have "x1-x2 = (e1+e2) *\<^sub>R (x-z)" + using x1_def x2_def by (auto simp add: algebra_simps) + hence "x=z+(1/(e1+e2)) *\<^sub>R (x1-x2)" using e1_def e2_def by simp + hence "x : affine hull S" using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"] + x1 x2 z affine_affine_hull[of S] by auto + } hence "affine hull S = UNIV" by auto + hence "aff_dim S = int DIM('n)" using aff_dim_affine_hull[of S] by (simp add: aff_dim_univ) + hence False using a by auto + } ultimately have ?thesis by auto +} +moreover +{ assume a: "aff_dim S = int DIM('n)" + hence "S ~= {}" using aff_dim_empty[of S] by auto + have *: "affine hull S=UNIV" using a affine_hull_univ by auto + { assume "z : interior S" + hence "z : rel_interior S" using a interior_rel_interior_gen[of S] by auto + hence **: "(!x. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)" + using convex_rel_interior_iff2[of S z] assms `S~={}` * by auto + fix x obtain e1 where e1_def: "e1>1 & (1-e1)*\<^sub>R (z-x)+ e1 *\<^sub>R z : S" + using **[rule_format, of "z-x"] by auto + def e == "e1 - 1" + hence "(1-e1)*\<^sub>R (z-x)+ e1 *\<^sub>R z = z+ e *\<^sub>R x" by (simp add: algebra_simps) + hence "e>0 & z+ e *\<^sub>R x : S" using e1_def e_def by auto + hence "EX e. e>0 & z+ e *\<^sub>R x : S" by auto + } + moreover + { assume r: "(!x. EX e. e>0 & z+ e *\<^sub>R x : S)" + { fix x obtain e1 where e1_def: "e1>0 & z + e1*\<^sub>R (z-x) : S" + using r[rule_format, of "z-x"] by auto + def e == "e1 + 1" + hence "z + e1*\<^sub>R (z-x) = (1-e)*\<^sub>R x+ e *\<^sub>R z" by (simp add: algebra_simps) + hence "e > 1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S" using e1_def e_def by auto + hence "EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S" by auto + } + hence "z : rel_interior S" using convex_rel_interior_iff2[of S z] assms `S~={}` by auto + hence "z : interior S" using a interior_rel_interior_gen[of S] by auto + } ultimately have ?thesis by auto +} ultimately show ?thesis by auto +qed + +subsection{* Relative interior and closure under commom operations *} + +lemma rel_interior_inter_aux: "Inter {rel_interior S |S. S : I} <= Inter I" +proof- +{ fix y assume "y : Inter {rel_interior S |S. S : I}" + hence y_def: "!S : I. y : rel_interior S" by auto + { fix S assume "S : I" hence "y : S" using rel_interior_subset y_def by auto } + hence "y : Inter I" by auto +} thus ?thesis by auto +qed + +lemma closure_inter: "closure (Inter I) <= Inter {closure S |S. S : I}" +proof- +{ fix y assume "y : Inter I" hence y_def: "!S : I. y : S" by auto + { fix S assume "S : I" hence "y : closure S" using closure_subset y_def by auto } + hence "y : Inter {closure S |S. S : I}" by auto +} hence "Inter I <= Inter {closure S |S. S : I}" by auto +moreover have "Inter {closure S |S. S : I} : closed" + unfolding mem_def closed_Inter closed_closure by auto +ultimately show ?thesis using closure_hull[of "Inter I"] + hull_minimal[of "Inter I" "Inter {closure S |S. S : I}" "closed"] by auto +qed + +lemma convex_closure_rel_interior_inter: +assumes "!S : I. convex (S :: ('n::euclidean_space) set)" +assumes "Inter {rel_interior S |S. S : I} ~= {}" +shows "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})" +proof- +obtain x where x_def: "!S : I. x : rel_interior S" using assms by auto +{ fix y assume "y : Inter {closure S |S. S : I}" hence y_def: "!S : I. y : closure S" by auto + { assume "y = x" + hence "y : closure (Inter {rel_interior S |S. S : I})" + using x_def closure_subset[of "Inter {rel_interior S |S. S : I}"] by auto + } + moreover + { assume "y ~= x" + { fix e :: real assume e_def: "0 < e" + def e1 == "min 1 (e/norm (y - x))" hence e1_def: "e1>0 & e1<=1 & e1*norm(y-x)<=e" + using `y ~= x` `e>0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm(y-x)"] by simp + def z == "y - e1 *\<^sub>R (y - x)" + { fix S assume "S : I" + hence "z : rel_interior S" using rel_interior_closure_convex_shrink[of S x y e1] + assms x_def y_def e1_def z_def by auto + } hence *: "z : Inter {rel_interior S |S. S : I}" by auto + have "EX z. z:Inter {rel_interior S |S. S : I} & z ~= y & (dist z y) <= e" + apply (rule_tac x="z" in exI) using `y ~= x` z_def * e1_def e_def dist_norm[of z y] by simp + } hence "y islimpt Inter {rel_interior S |S. S : I}" unfolding islimpt_approachable_le by blast + hence "y : closure (Inter {rel_interior S |S. S : I})" unfolding closure_def by auto + } ultimately have "y : closure (Inter {rel_interior S |S. S : I})" by auto +} from this show ?thesis by auto +qed + + +lemma convex_closure_inter: +assumes "!S : I. convex (S :: ('n::euclidean_space) set)" +assumes "Inter {rel_interior S |S. S : I} ~= {}" +shows "closure (Inter I) = Inter {closure S |S. S : I}" +proof- +have "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})" + using convex_closure_rel_interior_inter assms by auto +moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" + using rel_interior_inter_aux + subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto +ultimately show ?thesis using closure_inter[of I] by auto +qed + +lemma convex_inter_rel_interior_same_closure: +assumes "!S : I. convex (S :: ('n::euclidean_space) set)" +assumes "Inter {rel_interior S |S. S : I} ~= {}" +shows "closure (Inter {rel_interior S |S. S : I}) = closure (Inter I)" +proof- +have "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})" + using convex_closure_rel_interior_inter assms by auto +moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" + using rel_interior_inter_aux + subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto +ultimately show ?thesis using closure_inter[of I] by auto +qed + +lemma convex_rel_interior_inter: +assumes "!S : I. convex (S :: ('n::euclidean_space) set)" +assumes "Inter {rel_interior S |S. S : I} ~= {}" +shows "rel_interior (Inter I) <= Inter {rel_interior S |S. S : I}" +proof- +have "convex(Inter I)" using assms convex_Inter by auto +moreover have "convex(Inter {rel_interior S |S. S : I})" apply (rule convex_Inter) + using assms convex_rel_interior by auto +ultimately have "rel_interior (Inter {rel_interior S |S. S : I}) = rel_interior (Inter I)" + using convex_inter_rel_interior_same_closure assms + closure_eq_rel_interior_eq[of "Inter {rel_interior S |S. S : I}" "Inter I"] by blast +from this show ?thesis using rel_interior_subset[of "Inter {rel_interior S |S. S : I}"] by auto +qed + +lemma convex_rel_interior_finite_inter: +assumes "!S : I. convex (S :: ('n::euclidean_space) set)" +assumes "Inter {rel_interior S |S. S : I} ~= {}" +assumes "finite I" +shows "rel_interior (Inter I) = Inter {rel_interior S |S. S : I}" +proof- +have "Inter I ~= {}" using assms rel_interior_inter_aux[of I] by auto +have "convex (Inter I)" using convex_Inter assms by auto +{ assume "I={}" hence ?thesis using Inter_empty rel_interior_univ2 by auto } +moreover +{ assume "I ~= {}" +{ fix z assume z_def: "z : Inter {rel_interior S |S. S : I}" + { fix x assume x_def: "x : Inter I" + { fix S assume S_def: "S : I" hence "z : rel_interior S" "x : S" using z_def x_def by auto + (*from this obtain e where e_def: "e>1 & (1 - e) *\<^sub>R x + e *\<^sub>R z : S"*) + hence "EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S )" + using convex_rel_interior_if[of S z] S_def assms hull_subset[of S] by auto + } from this obtain mS where mS_def: "!S : I. (mS(S) > (1 :: real) & + (!e. (e>1 & e<=mS(S)) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S))" by metis + obtain e where e_def: "e=Min (mS ` I)" by auto + have "e : (mS ` I)" using e_def assms `I ~= {}` by (simp add: Min_in) + hence "e>(1 :: real)" using mS_def by auto + moreover have "!S : I. e<=mS(S)" using e_def assms by auto + ultimately have "EX e>1. (1 - e) *\<^sub>R x + e *\<^sub>R z : Inter I" using mS_def by auto + } hence "z : rel_interior (Inter I)" using convex_rel_interior_iff[of "Inter I" z] + `Inter I ~= {}` `convex (Inter I)` by auto +} from this have ?thesis using convex_rel_interior_inter[of I] assms by auto +} ultimately show ?thesis by blast +qed + +lemma convex_closure_inter_two: +fixes S T :: "('n::euclidean_space) set" +assumes "convex S" "convex T" +assumes "(rel_interior S) Int (rel_interior T) ~= {}" +shows "closure (S Int T) = (closure S) Int (closure T)" +using convex_closure_inter[of "{S,T}"] assms by auto + +lemma convex_rel_interior_inter_two: +fixes S T :: "('n::euclidean_space) set" +assumes "convex S" "convex T" +assumes "(rel_interior S) Int (rel_interior T) ~= {}" +shows "rel_interior (S Int T) = (rel_interior S) Int (rel_interior T)" +using convex_rel_interior_finite_inter[of "{S,T}"] assms by auto + + +lemma convex_affine_closure_inter: +fixes S T :: "('n::euclidean_space) set" +assumes "convex S" "affine T" +assumes "(rel_interior S) Int T ~= {}" +shows "closure (S Int T) = (closure S) Int T" +proof- +have "affine hull T = T" using assms by auto +hence "rel_interior T = T" using rel_interior_univ[of T] by metis +moreover have "closure T = T" using assms affine_closed[of T] by auto +ultimately show ?thesis using convex_closure_inter_two[of S T] assms affine_imp_convex by auto +qed + +lemma convex_affine_rel_interior_inter: +fixes S T :: "('n::euclidean_space) set" +assumes "convex S" "affine T" +assumes "(rel_interior S) Int T ~= {}" +shows "rel_interior (S Int T) = (rel_interior S) Int T" +proof- +have "affine hull T = T" using assms by auto +hence "rel_interior T = T" using rel_interior_univ[of T] by metis +moreover have "closure T = T" using assms affine_closed[of T] by auto +ultimately show ?thesis using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto +qed + +lemma subset_rel_interior_convex: +fixes S T :: "('n::euclidean_space) set" +assumes "convex S" "convex T" +assumes "S <= closure T" +assumes "~(S <= rel_frontier T)" +shows "rel_interior S <= rel_interior T" +proof- +have *: "S Int closure T = S" using assms by auto +have "~(rel_interior S <= rel_frontier T)" + using subset_closure[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] + closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto +hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}" + using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto +hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure + convex_rel_interior_inter_two[of S "closure T"] convex_rel_interior_closure[of T] by auto +also have "...=rel_interior (S)" using * by auto +finally show ?thesis by auto +qed + + +lemma rel_interior_convex_linear_image: +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" +assumes "linear f" +assumes "convex S" +shows "f ` (rel_interior S) = rel_interior (f ` S)" +proof- +{ assume "S = {}" hence ?thesis using assms rel_interior_empty rel_interior_convex_nonempty by auto } +moreover +{ assume "S ~= {}" +have *: "f ` (rel_interior S) <= f ` S" unfolding image_mono using rel_interior_subset by auto +have "f ` S <= f ` (closure S)" unfolding image_mono using closure_subset by auto +also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto +also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto +finally have "closure (f ` S) = closure (f ` rel_interior S)" + using subset_closure[of "f ` S" "closure (f ` rel_interior S)"] closure_closure + subset_closure[of "f ` rel_interior S" "f ` S"] * by auto +hence "rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior + linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"] + closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"] by auto +hence "rel_interior (f ` S) <= f ` rel_interior S" using rel_interior_subset by auto +moreover +{ fix z assume z_def: "z : f ` rel_interior S" + from this obtain z1 where z1_def: "z1 : rel_interior S & (f z1 = z)" by auto + { fix x assume "x : f ` S" + from this obtain x1 where x1_def: "x1 : S & (f x1 = x)" by auto + from this obtain e where e_def: "e>1 & (1 - e) *\<^sub>R x1 + e *\<^sub>R z1 : S" + using convex_rel_interior_iff[of S z1] `convex S` x1_def z1_def by auto + moreover have "f ((1 - e) *\<^sub>R x1 + e *\<^sub>R z1) = (1 - e) *\<^sub>R x + e *\<^sub>R z" + using x1_def z1_def `linear f` by (simp add: linear_add_cmul) + ultimately have "(1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S" + using imageI[of "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1" S f] by auto + hence "EX e. (e>1 & (1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S)" using e_def by auto + } from this have "z : rel_interior (f ` S)" using convex_rel_interior_iff[of "f ` S" z] `convex S` + `linear f` `S ~= {}` convex_linear_image[of S f] linear_conv_bounded_linear[of f] by auto +} ultimately have ?thesis by auto +} ultimately show ?thesis by blast +qed + + +lemma convex_linear_preimage: + assumes c:"convex S" and l:"bounded_linear f" + shows "convex(f -` S)" +proof(auto simp add: convex_def) + interpret f: bounded_linear f by fact + fix x y assume xy:"f x : S" "f y : S" + fix u v ::real assume uv:"0 <= u" "0 <= v" "u + v = 1" + show "f (u *\<^sub>R x + v *\<^sub>R y) : S" unfolding image_iff + using bexI[of _ "u *\<^sub>R x + v *\<^sub>R y"] f.add f.scaleR + c[unfolded convex_def] xy uv by auto +qed + + +lemma rel_interior_convex_linear_preimage: +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" +assumes "linear f" +assumes "convex S" +assumes "f -` (rel_interior S) ~= {}" +shows "rel_interior (f -` S) = f -` (rel_interior S)" +proof- +have "S ~= {}" using assms rel_interior_empty by auto +have nonemp: "f -` S ~= {}" by (metis assms(3) rel_interior_subset subset_empty vimage_mono) +hence "S Int (range f) ~= {}" by auto +have conv: "convex (f -` S)" using convex_linear_preimage assms linear_conv_bounded_linear by auto +hence "convex (S Int (range f))" + by (metis assms(1) assms(2) convex_Int subspace_UNIV subspace_imp_convex subspace_linear_image) +{ fix z assume "z : f -` (rel_interior S)" + hence z_def: "f z : rel_interior S" by auto + { fix x assume "x : f -` S" from this have x_def: "f x : S" by auto + from this obtain e where e_def: "e>1 & (1-e)*\<^sub>R (f x)+ e *\<^sub>R (f z) : S" + using convex_rel_interior_iff[of S "f z"] z_def assms `S ~= {}` by auto + moreover have "(1-e)*\<^sub>R (f x)+ e *\<^sub>R (f z) = f ((1-e)*\<^sub>R x + e *\<^sub>R z)" + using `linear f` by (simp add: linear_def) + ultimately have "EX e. e>1 & (1-e)*\<^sub>R x + e *\<^sub>R z : f -` S" using e_def by auto + } hence "z : rel_interior (f -` S)" + using convex_rel_interior_iff[of "f -` S" z] conv nonemp by auto +} +moreover +{ fix z assume z_def: "z : rel_interior (f -` S)" + { fix x assume x_def: "x: S Int (range f)" + from this obtain y where y_def: "(f y = x) & (y : f -` S)" by auto + from this obtain e where e_def: "e>1 & (1-e)*\<^sub>R y+ e *\<^sub>R z : f -` S" + using convex_rel_interior_iff[of "f -` S" z] z_def conv by auto + moreover have "(1-e)*\<^sub>R x+ e *\<^sub>R (f z) = f ((1-e)*\<^sub>R y + e *\<^sub>R z)" + using `linear f` y_def by (simp add: linear_def) + ultimately have "EX e. e>1 & (1-e)*\<^sub>R x + e *\<^sub>R (f z) : S Int (range f)" + using e_def by auto + } hence "f z : rel_interior (S Int (range f))" using `convex (S Int (range f))` + `S Int (range f) ~= {}` convex_rel_interior_iff[of "S Int (range f)" "f z"] by auto + moreover have "affine (range f)" + by (metis assms(1) subspace_UNIV subspace_imp_affine subspace_linear_image) + ultimately have "f z : rel_interior S" + using convex_affine_rel_interior_inter[of S "range f"] assms by auto + hence "z : f -` (rel_interior S)" by auto +} +ultimately show ?thesis by auto +qed + + +lemma convex_direct_sum: +fixes S :: "('n::euclidean_space) set" +fixes T :: "('m::euclidean_space) set" +assumes "convex S" "convex T" +shows "convex (S <*> T)" +proof- +{ +fix x assume "x : S <*> T" +from this obtain xs xt where xst_def: "xs : S & xt : T & (xs,xt) = x" by auto +fix y assume "y : S <*> T" +from this obtain ys yt where yst_def: "ys : S & yt : T & (ys,yt) = y" by auto +fix u v assume uv_def: "(u :: real)>=0 & (v :: real)>=0 & u+v=1" +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 +moreover have "u *\<^sub>R xs + v *\<^sub>R ys : S" + using uv_def xst_def yst_def convex_def[of S] assms by auto +moreover have "u *\<^sub>R xt + v *\<^sub>R yt : T" + using uv_def xst_def yst_def convex_def[of T] assms by auto +ultimately have "u *\<^sub>R x + v *\<^sub>R y : S <*> T" by auto +} from this show ?thesis unfolding convex_def by auto +qed + + +lemma convex_hull_direct_sum: +fixes S :: "('n::euclidean_space) set" +fixes T :: "('m::euclidean_space) set" +shows "convex hull (S <*> T) = (convex hull S) <*> (convex hull T)" +proof- +{ fix x assume "x : (convex hull S) <*> (convex hull T)" + from this obtain xs xt where xst_def: "xs : convex hull S & xt : convex hull T & (xs,xt) = x" by auto + from xst_def obtain sI su where s: "finite sI & sI <= S & (ALL x:sI. 0 <= su x) & setsum su sI = 1 + & (SUM v:sI. su v *\<^sub>R v) = xs" using convex_hull_explicit[of S] by auto + from xst_def obtain tI tu where t: "finite tI & tI <= T & (ALL x:tI. 0 <= tu x) & setsum tu tI = 1 + & (SUM v:tI. tu v *\<^sub>R v) = xt" using convex_hull_explicit[of T] by auto + def I == "(sI <*> tI)" + def u == "(%i. (su (fst i))*(tu(snd i)))" + have "fst (SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)= + (SUM vs:sI. SUM vt:tI. (su vs * tu vt) *\<^sub>R vs)" + using fst_setsum[of "(%v. (su (fst v) * tu (snd v)) *\<^sub>R v)" "sI <*> tI"] + by (simp add: split_def scaleR_prod_def setsum_cartesian_product) + also have "...=(SUM vt:tI. tu vt *\<^sub>R (SUM vs:sI. su vs *\<^sub>R vs))" + using setsum_commute[of "(%vt vs. (su vs * tu vt) *\<^sub>R vs)" sI tI] + by (simp add: mult_commute scaleR_right.setsum) + also have "...=(SUM vt:tI. tu vt *\<^sub>R xs)" using s by auto + also have "...=(SUM vt:tI. tu vt) *\<^sub>R xs" by (simp add: scaleR_left.setsum) + also have "...=xs" using t by auto + finally have h1: "fst (SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)=xs" by auto + have "snd (SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)= + (SUM vs:sI. SUM vt:tI. (su vs * tu vt) *\<^sub>R vt)" + using snd_setsum[of "(%v. (su (fst v) * tu (snd v)) *\<^sub>R v)" "sI <*> tI"] + by (simp add: split_def scaleR_prod_def setsum_cartesian_product) + also have "...=(SUM vs:sI. su vs *\<^sub>R (SUM vt:tI. tu vt *\<^sub>R vt))" + by (simp add: mult_commute scaleR_right.setsum) + also have "...=(SUM vs:sI. su vs *\<^sub>R xt)" using t by auto + also have "...=(SUM vs:sI. su vs) *\<^sub>R xt" by (simp add: scaleR_left.setsum) + also have "...=xt" using s by auto + finally have h2: "snd (SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)=xt" by auto + from h1 h2 have "(SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) = x" using xst_def by auto + + moreover have "finite I & (I <= S <*> T)" using s t I_def by auto + moreover have "!i:I. 0 <= u i" using s t I_def u_def by (simp add: mult_nonneg_nonneg) + moreover have "setsum u I = 1" using u_def I_def setsum_cartesian_product[of "(% x y. (su x)*(tu y))"] + s t setsum_product[of su sI tu tI] by (auto simp add: split_def) + ultimately have "x : convex hull (S <*> T)" + apply (subst convex_hull_explicit[of "S <*> T"]) apply rule + apply (rule_tac x="I" in exI) apply (rule_tac x="u" in exI) + using I_def u_def by auto +} +hence "convex hull (S <*> T) >= (convex hull S) <*> (convex hull T)" by auto +moreover have "(convex hull S) <*> (convex hull T) : convex" + unfolding mem_def by (simp add: convex_direct_sum convex_convex_hull) +ultimately show ?thesis + using hull_minimal[of "S <*> T" "(convex hull S) <*> (convex hull T)" "convex"] + hull_subset[of S convex] hull_subset[of T convex] by auto +qed + +lemma rel_interior_direct_sum: +fixes S :: "('n::euclidean_space) set" +fixes T :: "('m::euclidean_space) set" +assumes "convex S" "convex T" +shows "rel_interior (S <*> T) = rel_interior S <*> rel_interior T" +proof- +{ assume "S={}" hence ?thesis apply auto using rel_interior_empty by auto } +moreover +{ assume "T={}" hence ?thesis apply auto using rel_interior_empty by auto } +moreover { +assume "S ~={}" "T ~={}" +hence ri: "rel_interior S ~= {}" "rel_interior T ~= {}" using rel_interior_convex_nonempty assms by auto +hence "fst -` rel_interior S ~= {}" using fst_vimage_eq_Times[of "rel_interior S"] by auto +hence "rel_interior ((fst :: 'n * 'm => 'n) -` S) = fst -` rel_interior S" + using fst_linear `convex S` rel_interior_convex_linear_preimage[of fst S] by auto +hence s: "rel_interior (S <*> (UNIV :: 'm set)) = rel_interior S <*> UNIV" by (simp add: fst_vimage_eq_Times) +from ri have "snd -` rel_interior T ~= {}" using snd_vimage_eq_Times[of "rel_interior T"] by auto +hence "rel_interior ((snd :: 'n * 'm => 'm) -` T) = snd -` rel_interior T" + using snd_linear `convex T` rel_interior_convex_linear_preimage[of snd T] by auto +hence t: "rel_interior ((UNIV :: 'n set) <*> T) = UNIV <*> rel_interior T" by (simp add: snd_vimage_eq_Times) +from s t have *: "rel_interior (S <*> (UNIV :: 'm set)) Int rel_interior ((UNIV :: 'n set) <*> T) + = rel_interior S <*> rel_interior T" by auto +have "(S <*> T) = (S <*> (UNIV :: 'm set)) Int ((UNIV :: 'n set) <*> T)" by auto +hence "rel_interior (S <*> T) = rel_interior ((S <*> (UNIV :: 'm set)) Int ((UNIV :: 'n set) <*> T))" by auto +also have "...=rel_interior (S <*> (UNIV :: 'm set)) Int rel_interior ((UNIV :: 'n set) <*> T)" + apply (subst convex_rel_interior_inter_two[of "S <*> (UNIV :: 'm set)" "(UNIV :: 'n set) <*> T"]) + using * ri assms convex_direct_sum by auto +finally have ?thesis using * by auto +} +ultimately show ?thesis by blast +qed + +lemma rel_interior_scaleR: +fixes S :: "('n::euclidean_space) set" +assumes "c ~= 0" +shows "(op *\<^sub>R c) ` (rel_interior S) = rel_interior ((op *\<^sub>R c) ` S)" +using rel_interior_injective_linear_image[of "(op *\<^sub>R c)" S] + linear_conv_bounded_linear[of "op *\<^sub>R c"] linear_scaleR injective_scaleR[of c] assms by auto + +lemma rel_interior_convex_scaleR: +fixes S :: "('n::euclidean_space) set" +assumes "convex S" +shows "(op *\<^sub>R c) ` (rel_interior S) = rel_interior ((op *\<^sub>R c) ` S)" +by (metis assms linear_scaleR rel_interior_convex_linear_image) + +lemma convex_rel_open_scaleR: +fixes S :: "('n::euclidean_space) set" +assumes "convex S" "rel_open S" +shows "convex ((op *\<^sub>R c) ` S) & rel_open ((op *\<^sub>R c) ` S)" +by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def) + + +lemma convex_rel_open_finite_inter: +assumes "!S : I. (convex (S :: ('n::euclidean_space) set) & rel_open S)" +assumes "finite I" +shows "convex (Inter I) & rel_open (Inter I)" +proof- +{ assume "Inter {rel_interior S |S. S : I} = {}" + hence "Inter I = {}" using assms unfolding rel_open_def by auto + hence ?thesis unfolding rel_open_def using rel_interior_empty by auto +} +moreover +{ assume "Inter {rel_interior S |S. S : I} ~= {}" + hence "rel_open (Inter I)" using assms unfolding rel_open_def + using convex_rel_interior_finite_inter[of I] by auto + hence ?thesis using convex_Inter assms by auto +} ultimately show ?thesis by auto +qed + +lemma convex_rel_open_linear_image: +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" +assumes "linear f" +assumes "convex S" "rel_open S" +shows "convex (f ` S) & rel_open (f ` S)" +by (metis assms convex_linear_image rel_interior_convex_linear_image + linear_conv_bounded_linear rel_open_def) + +lemma convex_rel_open_linear_preimage: +fixes f :: "('m::euclidean_space) => ('n::euclidean_space)" +assumes "linear f" +assumes "convex S" "rel_open S" +shows "convex (f -` S) & rel_open (f -` S)" +proof- +{ assume "f -` (rel_interior S) = {}" + hence "f -` S = {}" using assms unfolding rel_open_def by auto + hence ?thesis unfolding rel_open_def using rel_interior_empty by auto +} +moreover +{ assume "f -` (rel_interior S) ~= {}" + hence "rel_open (f -` S)" using assms unfolding rel_open_def + using rel_interior_convex_linear_preimage[of f S] by auto + hence ?thesis using convex_linear_preimage assms linear_conv_bounded_linear by auto +} ultimately show ?thesis by auto +qed + +lemma rel_interior_projection: +fixes S :: "('m::euclidean_space*'n::euclidean_space) set" +fixes f :: "'m::euclidean_space => ('n::euclidean_space) set" +assumes "convex S" +assumes "f = (%y. {z. (y,z) : S})" +shows "(y,z) : rel_interior S <-> (y : rel_interior {y. (f y ~= {})} & z : rel_interior (f y))" +proof- +{ fix y assume "y : {y. (f y ~= {})}" from this obtain z where "(y,z) : S" using assms by auto + hence "EX x. x : S & y = fst x" apply (rule_tac x="(y,z)" in exI) by auto + from this obtain x where "x : S & y = fst x" by blast + hence "y : fst ` S" unfolding image_def by auto +} +hence "fst ` S = {y. (f y ~= {})}" unfolding fst_def using assms by auto +hence h1: "fst ` rel_interior S = rel_interior {y. (f y ~= {})}" + using rel_interior_convex_linear_image[of fst S] assms fst_linear by auto +{ fix y assume "y : rel_interior {y. (f y ~= {})}" + hence "y : fst ` rel_interior S" using h1 by auto + hence *: "rel_interior S Int fst -` {y} ~= {}" by auto + moreover have aff: "affine (fst -` {y})" unfolding affine_alt by (simp add: algebra_simps) + ultimately have **: "rel_interior (S Int fst -` {y}) = rel_interior S Int fst -` {y}" + using convex_affine_rel_interior_inter[of S "fst -` {y}"] assms by auto + have conv: "convex (S Int fst -` {y})" using convex_Int assms aff affine_imp_convex by auto + { fix x assume "x : f y" + hence "(y,x) : S Int (fst -` {y})" using assms by auto + moreover have "x = snd (y,x)" by auto + ultimately have "x : snd ` (S Int fst -` {y})" by blast + } + hence "snd ` (S Int fst -` {y}) = f y" using assms by auto + hence ***: "rel_interior (f y) = snd ` rel_interior (S Int fst -` {y})" + using rel_interior_convex_linear_image[of snd "S Int fst -` {y}"] snd_linear conv by auto + { fix z assume "z : rel_interior (f y)" + hence "z : snd ` rel_interior (S Int fst -` {y})" using *** by auto + moreover have "{y} = fst ` rel_interior (S Int fst -` {y})" using * ** rel_interior_subset by auto + ultimately have "(y,z) : rel_interior (S Int fst -` {y})" by force + hence "(y,z) : rel_interior S" using ** by auto + } + moreover + { fix z assume "(y,z) : rel_interior S" + hence "(y,z) : rel_interior (S Int fst -` {y})" using ** by auto + hence "z : snd ` rel_interior (S Int fst -` {y})" by (metis Range_iff snd_eq_Range) + hence "z : rel_interior (f y)" using *** by auto + } + ultimately have "!!z. (y,z) : rel_interior S <-> z : rel_interior (f y)" by auto +} +hence h2: "!!y z. y : rel_interior {t. f t ~= {}} ==> ((y, z) : rel_interior S) = (z : rel_interior (f y))" + by auto +{ fix y z assume asm: "(y, z) : rel_interior S" + hence "y : fst ` rel_interior S" by (metis Domain_iff fst_eq_Domain) + hence "y : rel_interior {t. f t ~= {}}" using h1 by auto + hence "y : rel_interior {t. f t ~= {}} & (z : rel_interior (f y))" using h2 asm by auto +} from this show ?thesis using h2 by blast +qed + +subsection{* Relative interior of convex cone *} + +lemma cone_rel_interior: +fixes S :: "('m::euclidean_space) set" +assumes "cone S" +shows "cone ({0} Un (rel_interior S))" +proof- +{ assume "S = {}" hence ?thesis by (simp add: rel_interior_empty cone_0) } +moreover +{ assume "S ~= {}" hence *: "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto + hence *: "0:({0} Un (rel_interior S)) & + (!c. c>0 --> op *\<^sub>R c ` ({0} Un rel_interior S) = ({0} Un rel_interior S))" + by (auto simp add: rel_interior_scaleR) + hence ?thesis using cone_iff[of "{0} Un rel_interior S"] by auto +} +ultimately show ?thesis by blast +qed + +lemma rel_interior_convex_cone_aux: +fixes S :: "('m::euclidean_space) set" +assumes "convex S" +shows "(c,x) : rel_interior (cone hull ({(1 :: real)} <*> S)) <-> + c>0 & x : ((op *\<^sub>R c) ` (rel_interior S))" +proof- +{ assume "S={}" hence ?thesis by (simp add: rel_interior_empty cone_hull_empty) } +moreover +{ assume "S ~= {}" from this obtain s where "s : S" by auto +have conv: "convex ({(1 :: real)} <*> S)" using convex_direct_sum[of "{(1 :: real)}" S] + assms convex_singleton[of "1 :: real"] by auto +def f == "(%y. {z. (y,z) : cone hull ({(1 :: real)} <*> S)})" +hence *: "(c, x) : rel_interior (cone hull ({(1 :: real)} <*> S)) = + (c : rel_interior {y. f y ~= {}} & x : rel_interior (f c))" + apply (subst rel_interior_projection[of "cone hull ({(1 :: real)} <*> S)" f c x]) + using convex_cone_hull[of "{(1 :: real)} <*> S"] conv by auto +{ fix y assume "(y :: real)>=0" + hence "y *\<^sub>R (1,s) : cone hull ({(1 :: real)} <*> S)" + using cone_hull_expl[of "{(1 :: real)} <*> S"] `s:S` by auto + hence "f y ~= {}" using f_def by auto +} +hence "{y. f y ~= {}} = {0..}" using f_def cone_hull_expl[of "{(1 :: real)} <*> S"] by auto +hence **: "rel_interior {y. f y ~= {}} = {0<..}" using rel_interior_real_semiline by auto +{ fix c assume "c>(0 :: real)" + hence "f c = (op *\<^sub>R c ` S)" using f_def cone_hull_expl[of "{(1 :: real)} <*> S"] by auto + hence "rel_interior (f c)= (op *\<^sub>R c ` rel_interior S)" + using rel_interior_convex_scaleR[of S c] assms by auto +} +hence ?thesis using * ** by auto +} ultimately show ?thesis by blast +qed + + +lemma rel_interior_convex_cone: +fixes S :: "('m::euclidean_space) set" +assumes "convex S" +shows "rel_interior (cone hull ({(1 :: real)} <*> S)) = + {(c,c *\<^sub>R x) |c x. c>0 & x : (rel_interior S)}" +(is "?lhs=?rhs") +proof- +{ fix z assume "z:?lhs" + have *: "z=(fst z,snd z)" by auto + have "z:?rhs" using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms `z:?lhs` apply auto + apply (rule_tac x="fst z" in exI) apply (rule_tac x="x" in exI) using * by auto +} +moreover +{ fix z assume "z:?rhs" hence "z:?lhs" + using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms by auto +} +ultimately show ?thesis by blast +qed + +lemma convex_hull_finite_union: +assumes "finite I" +assumes "!i:I. (convex (S i) & (S i) ~= {})" +shows "convex hull (Union (S ` I)) = + {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)}" + (is "?lhs = ?rhs") +proof- +{ fix x assume "x : ?rhs" + from this obtain c s + where *: "setsum (%i. c i *\<^sub>R s i) I=x" "(setsum c I = 1)" + "(!i:I. c i >= 0) & (!i:I. s i : S i)" by auto + hence "!i:I. s i : convex hull (Union (S ` I))" using hull_subset[of "Union (S ` I)" convex] by auto + hence "x : ?lhs" unfolding *(1)[THEN sym] + apply (subst convex_setsum[of I "convex hull Union (S ` I)" c s]) + using * assms convex_convex_hull by auto +} hence "?lhs >= ?rhs" by auto + +{ fix i assume "i:I" + from this assms have "EX p. p : S i" by auto +} +from this obtain p where p_def: "!i:I. p i : S i" by metis + +{ fix i assume "i:I" + { fix x assume "x : S i" + def c == "(%j. if (j=i) then (1::real) else 0)" + hence *: "setsum c I = 1" using `finite I` `i:I` setsum_delta[of I i "(%(j::'a). (1::real))"] by auto + def s == "(%j. if (j=i) then x else p j)" + hence "!j. c j *\<^sub>R s j = (if (j=i) then x else 0)" using c_def by (auto simp add: algebra_simps) + hence "x = setsum (%i. c i *\<^sub>R s i) I" + using s_def c_def `finite I` `i:I` setsum_delta[of I i "(%(j::'a). x)"] by auto + hence "x : ?rhs" apply auto + apply (rule_tac x="c" in exI) + apply (rule_tac x="s" in exI) using * c_def s_def p_def `x : S i` by auto + } hence "?rhs >= S i" by auto +} hence *: "?rhs >= Union (S ` I)" by auto + +{ fix u v assume uv: "(u :: real)>=0 & v>=0 & u+v=1" + fix x y assume xy: "(x : ?rhs) & (y : ?rhs)" + from xy obtain c s where xc: "x=setsum (%i. c i *\<^sub>R s i) I & + (!i:I. c i >= 0) & (setsum c I = 1) & (!i:I. s i : S i)" by auto + from xy obtain d t where yc: "y=setsum (%i. d i *\<^sub>R t i) I & + (!i:I. d i >= 0) & (setsum d I = 1) & (!i:I. t i : S i)" by auto + def e == "(%i. u * (c i)+v * (d i))" + have ge0: "!i:I. e i >= 0" using e_def xc yc uv by (simp add: mult_nonneg_nonneg) + have "setsum (%i. u * c i) I = u * setsum c I" by (simp add: setsum_right_distrib) + moreover have "setsum (%i. v * d i) I = v * setsum d I" by (simp add: setsum_right_distrib) + ultimately have sum1: "setsum e I = 1" using e_def xc yc uv by (simp add: setsum_addf) + def q == "(%i. if (e i = 0) then (p i) + else (u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i))" + { fix i assume "i:I" + { assume "e i = 0" hence "q i : S i" using `i:I` p_def q_def by auto } + moreover + { assume "e i ~= 0" + hence "q i : S i" using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"] + mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"] + assms q_def e_def `i:I` `e i ~= 0` xc yc uv by auto + } ultimately have "q i : S i" by auto + } hence qs: "!i:I. q i : S i" by auto + { fix i assume "i:I" + { assume "e i = 0" + have ge: "u * (c i) >= 0 & v * (d i) >= 0" using xc yc uv `i:I` by (simp add: mult_nonneg_nonneg) + moreover hence "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp + ultimately have "u * (c i) = 0 & v * (d i) = 0" by auto + hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" + using `e i = 0` by auto + } + moreover + { assume "e i ~= 0" + hence "(u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i) = q i" + using q_def by auto + hence "e i *\<^sub>R ((u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i)) + = (e i) *\<^sub>R (q i)" by auto + hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" + using `e i ~= 0` by (simp add: algebra_simps) + } ultimately have + "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" by blast + } hence *: "!i:I. + (u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" by auto + have "u *\<^sub>R x + v *\<^sub>R y = + setsum (%i. (u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i)) I" + using xc yc by (simp add: algebra_simps scaleR_right.setsum setsum_addf) + also have "...=setsum (%i. (e i) *\<^sub>R (q i)) I" using * by auto + finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (%i. (e i) *\<^sub>R (q i)) I" by auto + hence "u *\<^sub>R x + v *\<^sub>R y : ?rhs" using ge0 sum1 qs by auto +} hence "convex ?rhs" unfolding convex_def by auto +hence "?rhs : convex" unfolding mem_def by auto +from this show ?thesis using `?lhs >= ?rhs` * + hull_minimal[of "Union (S ` I)" "?rhs" "convex"] by blast +qed + +lemma convex_hull_union_two: +fixes S T :: "('m::euclidean_space) set" +assumes "convex S" "S ~= {}" "convex T" "T ~= {}" +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}" + (is "?lhs = ?rhs") +proof- +def I == "{(1::nat),2}" +def s == "(%i. (if i=(1::nat) then S else T))" +have "Union (s ` I) = S Un T" using s_def I_def by auto +hence "convex hull (Union (s ` I)) = convex hull (S Un T)" by auto +moreover have "convex hull Union (s ` I) = + {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)}" + apply (subst convex_hull_finite_union[of I s]) using assms s_def I_def by auto +moreover have + "{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)} <= + ?rhs" + using s_def I_def by auto +ultimately have "?lhs<=?rhs" by auto +{ fix x assume "x : ?rhs" + from this obtain u v s t + where *: "x=u *\<^sub>R s + v *\<^sub>R t & u>=0 & v>=0 & u+v=1 & s:S & t:T" by auto + hence "x : convex hull {s,t}" using convex_hull_2[of s t] by auto + hence "x : convex hull (S Un T)" using * hull_mono[of "{s, t}" "S Un T"] by auto +} hence "?lhs >= ?rhs" by blast +from this show ?thesis using `?lhs<=?rhs` by auto +qed + end diff -r 6fb991dc074b -r 0e5d48096f58 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Nov 05 09:07:14 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Nov 05 14:17:18 2010 +0100 @@ -1065,10 +1065,16 @@ text {* Individual closure properties. *} +lemma span_span: "span (span A) = span A" + unfolding span_def hull_hull .. + lemma (in real_vector) span_superset: "x \ S ==> x \ span S" by (metis span_clauses(1)) lemma (in real_vector) span_0: "0 \ span S" by (metis subspace_span subspace_0) +lemma span_inc: "S \ span S" + by (metis subset_eq span_superset) + lemma (in real_vector) dependent_0: assumes "0\A" shows "dependent A" unfolding dependent_def apply(rule_tac x=0 in bexI) using assms span_0 by auto @@ -1485,12 +1491,6 @@ lemma mem_delete: "x \ (A - {a}) \ x \ a \ x \ A" by blast -lemma span_span: "span (span A) = span A" - unfolding span_def hull_hull .. - -lemma span_inc: "S \ span S" - by (metis subset_eq span_superset) - lemma spanning_subset_independent: assumes BA: "B \ A" and iA: "independent A" and AsB: "A \ span B"