--- 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 \<subseteq> {..<DIM('n)} \<Longrightarrow> 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 \<subseteq> {..<DIM('n::euclidean_space)}"
+ shows "card {basis i ::'n::euclidean_space | i. i : d} = card d" (is "card ?S = _")
+proof-
+ have eq: "?S = basis ` d" by blast
+ show ?thesis unfolding eq using card_image[OF basis_inj_on[of d]] assms by auto
+qed
+
+lemma substdbasis_expansion_unique: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
+ shows "setsum (%i. f i *\<^sub>R basis i) d = (x::'a::euclidean_space)
+ <-> (!i<DIM('a). (i:d --> f i = x$$i) & (i ~: d --> x $$ i = 0))"
+proof- have *:"\<And>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 ***:"\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)"
+ 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\<subseteq>{..<DIM('a::euclidean_space)}"
+ shows "independent {basis i ::'a::euclidean_space |i. i : (d :: nat set)}" (is "independent ?A")
+proof -
+ have *: "{basis i |i. i < DIM('a)} = basis ` {..<DIM('a)}" by auto
+ show ?thesis
+ apply(intro independent_mono[of "{basis i ::'a |i. i : {..<DIM('a::euclidean_space)}}" "?A"] )
+ using independent_basis[where 'a='a] assms by (auto simp: *)
+qed
+
+lemma dim_cball:
+assumes "0<e"
+shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)"
+proof-
+{ fix x :: "'n::euclidean_space" def y == "(e/norm x) *\<^sub>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 "(\<lambda>x. b+x) ` ((\<lambda>x. a+x) ` S) = (\<lambda>x. (a+b)+x) ` S" by auto
+
+lemma translation_invert:
+ fixes a :: "'a::ab_group_add"
+ assumes "(\<lambda>x. a+x) ` A = (\<lambda>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=((\<lambda>x. a+x) ` S) <-> S=((\<lambda>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 \<longleftrightarrow> i\<ge>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 \<subseteq> 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" "\<forall>x\<in> 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 "\<dots> = 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 \<in> S" and y: "y \<in> S" and gxy:"g x = g y"
+ from B(3) x y have x': "x \<in> span B" and y': "y \<in> span B" by blast+
+ from gxy have th0: "g (x - y) = 0" by (simp add: linear_sub[OF g(1)])
+ have th1: "x - y \<in> 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 "\<dots> = span C" unfolding gBC ..
+ also have "\<dots> = 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 \<in> span {x - a | x. x \<in> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<in> 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 \<in> 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 \<in> convex hull s"
+ shows "(f x) \<in> 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 \<Longrightarrow> affine s"
- unfolding subspace_def affine_def by auto
-
lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
unfolding affine_def convex_def by auto
@@ -952,6 +1559,979 @@
thus "x \<in> convex hull p" using hull_mono[OF `s\<subseteq>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\<subseteq>{..<DIM('a::euclidean_space)}"
+ shows "(span {basis i | i. i : d}) = {x::'a::euclidean_space. (!i<DIM('a). i ~: 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<DIM('a). i ~: d --> x $$ i = (0::real)} & inj_on f (span B) \<and> d\<subseteq>{..<DIM('a)}"
+proof-
+ have B:"card B=dim B" using dim_unique[of B B "card B"] assms span_inc[of B] by auto
+ def d \<equiv> "{..<dim B}" have t:"card d = dim B" unfolding d_def by auto
+ have "dim B <= DIM('a)" using dim_subset_UNIV[of B] by auto
+ hence d:"d\<subseteq>{..<DIM('a)}" unfolding d_def by auto
+ let ?t = "{x::'a::euclidean_space. !i<DIM('a). i ~: d --> x$$i = 0}"
+ have "EX f. linear f & f ` B = {basis i |i. i : d} &
+ f ` span B = ?t & inj_on f (span B)"
+ apply (rule basis_to_basis_subspace_isomorphism[of "span B" ?t B "{basis i |i. i : d}"])
+ apply(rule subspace_span) apply(rule subspace_substandard) defer
+ apply(rule span_inc) apply(rule assms) defer unfolding dim_span[of B] apply(rule B)
+ unfolding span_substd_basis[OF d,THEN sym] card_substdbasis[OF d] apply(rule span_inc)
+ apply(rule independent_substdbasis[OF d]) apply(rule,assumption)
+ unfolding t[THEN sym] span_substd_basis[OF d] dim_substandard[OF d] by auto
+ from this t `card B=dim B` show ?thesis using d by auto
+qed
+
+lemma aff_dim_empty:
+fixes S :: "('n::euclidean_space) set"
+shows "S = {} <-> 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 "0<e"
+shows "aff_dim (cball a e) = int (DIM('n))"
+proof-
+have "(%x. a + x) ` (cball 0 e)<=cball a e" unfolding cball_def dist_norm by auto
+hence "aff_dim (cball (0 :: 'n::euclidean_space) e) <= aff_dim (cball a e)"
+ using aff_dim_translation_eq[of a "cball 0 e"]
+ aff_dim_subset[of "op + a ` cball 0 e" "cball a e"] by auto
+moreover have "aff_dim (cball (0 :: 'n::euclidean_space) e) = int (DIM('n))"
+ using hull_inc[of "(0 :: 'n::euclidean_space)" "cball 0 e"] centre_in_cball[of "(0 :: 'n::euclidean_space)"] assms
+ by (simp add: dim_cball[of e] aff_dim_zero[of "cball 0 e"])
+ultimately show ?thesis using aff_dim_subset_univ[of "cball a e"] by auto
+qed
+
+lemma aff_dim_open:
+fixes S :: "('n::euclidean_space) set"
+assumes "open S" "S ~= {}"
+shows "aff_dim S = int (DIM('n))"
+proof-
+obtain x where "x:S" using assms by auto
+from this obtain e where e_def: "e>0 & 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 `0<e` `0<d` using real_mult_order by auto
+moreover have "c : S" using assms rel_interior_subset by auto
+moreover hence "x - e *\<^sub>R (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 "a<y" hence "y : interior {a..}"
+ apply (simp add: mem_interior) apply (rule_tac x="(y-a)" in exI) apply (auto simp add: dist_norm)
+ done }
+moreover
+{ fix y assume "y : interior {a..}" (*hence "a<=y" using interior_subset by auto*)
+ from this obtain e where e_def: "e>0 & cball y e \<subseteq> {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<y" using e_def by auto
+} ultimately show ?thesis by auto
+qed
+
+lemma rel_interior_real_interval:
+ fixes a b :: real assumes "a < b" shows "rel_interior {a..b} = {a<..<b}"
+proof-
+ have "{a<..<b} \<noteq> {}" 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<..} \<noteq> {}" 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\<in>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\<subseteq>{..<DIM('a::euclidean_space)}"
+ shows "affine hull (insert 0 {basis i | i. i : d}) =
+ {x::'a::euclidean_space. (!i<DIM('a). i ~: d --> x$$i = 0)}"
+ (is "affine hull (insert 0 ?A) = ?B")
+proof- have *:"\<And>A. op + (0\<Colon>'a) ` A = A" "\<And>A. op + (- (0\<Colon>'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 ((\<lambda>x. a + c *\<^sub>R x) ` s) = (\<lambda>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 "\<Inter> f \<noteq>{}"
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 \<in> 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 \<in> 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 \<in> convex hull s"
- shows "(f x) \<in> 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="\<lambda>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\<subseteq>{..<DIM('a::euclidean_space)}"
+ shows "convex hull (insert 0 { basis i | i. i : d}) =
+ {x::'a::euclidean_space . (!i<DIM('a). 0 <= x$$i) & setsum (%i. x$$i) d <= 1 &
+ (!i<DIM('a). i ~: 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 (*"{..<DIM('a::euclidean_space)}"*)
+ have "0 ~: ?p" using assms by (auto simp: image_def)
+ have "{(basis i)::'n::euclidean_space |i. i \<in> ?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: "\<forall>x\<in>{basis i |i. i \<in>?D}. 0 \<le> u x"
+ "setsum u {basis i |i. i \<in> ?D} \<le> 1" "(\<Sum>x\<in>{basis i |i. i \<in>?D}. u x *\<^sub>R x) = x"
+ have *:"\<forall>i<DIM('a). i:d --> u (basis i) = x$$i" and "(!i<DIM('a). i ~: d --> x $$ i = 0)" using as(3)
+ unfolding sumbas unfolding substdbasis_expansion_unique[OF assms] by auto
+ hence **:"setsum u {basis i |i. i \<in> ?D} = setsum (op $$ x) ?D" unfolding sumbas
+ apply-apply(rule setsum_cong2) using assms by auto
+ have " (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (op $$ x) ?D \<le> 1"
+ apply - proof(rule,rule,rule)
+ fix i assume i:"i<DIM('a)" have "i : d ==> 0 \<le> x$$i" unfolding *[rule_format,OF i,THEN sym]
+ apply(rule_tac as(1)[rule_format]) by auto
+ moreover have "i ~: d ==> 0 \<le> x$$i"
+ using `(!i<DIM('a). i ~: d --> x $$ i = 0)`[rule_format, OF i] by auto
+ ultimately show "0 \<le> x$$i" by auto
+ qed(insert as(2)[unfolded **], auto)
+ from this show " (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (op $$ x) ?D \<le> 1 & (!i<DIM('a). i ~: d --> x $$ i = 0)"
+ using `(!i<DIM('a). i ~: d --> x $$ i = 0)` by auto
+ next fix x::"'a::euclidean_space" assume as:"\<forall>i<DIM('a). 0 \<le> x $$ i" "setsum (op $$ x) ?D \<le> 1"
+ "(!i<DIM('a). i ~: d --> x $$ i = 0)"
+ show "\<exists>u. (\<forall>x\<in>{basis i |i. i \<in> ?D}. 0 \<le> u x) \<and>
+ setsum u {basis i |i. i \<in> ?D} \<le> 1 \<and> (\<Sum>x\<in>{basis i |i. i \<in> ?D}. u x *\<^sub>R x) = x"
+ apply(rule_tac x="\<lambda>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. i<DIM('a)}) =
{x::'a::euclidean_space . (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (\<lambda>i. x$$i) {..<DIM('a)} \<le> 1 }"
- (is "convex hull (insert 0 ?p) = ?s")
-proof- let ?D = "{..<DIM('a)}"
- have *:"finite ?p" "0\<notin>?p" by auto
- have "{(basis i)::'a |i. i<DIM('a)} = basis ` ?D" by auto
- note sumbas = this setsum_reindex[OF basis_inj, unfolded o_def]
- show ?thesis unfolding simplex[OF *] apply(rule set_eqI) unfolding mem_Collect_eq apply rule
- apply(erule exE, (erule conjE)+) apply(erule_tac[2] conjE)+ proof-
- fix x::"'a" and u assume as: "\<forall>x\<in>{basis i |i. i<DIM('a)}. 0 \<le> u x"
- "setsum u {basis i |i. i<DIM('a)} \<le> 1" "(\<Sum>x\<in>{basis i |i. i<DIM('a)}. u x *\<^sub>R x) = x"
- have *:"\<forall>i<DIM('a). u (basis i) = x$$i"
- proof safe case goal1
- have "x$$i = (\<Sum>j<DIM('a). (if j = i then u (basis j) else 0))"
- unfolding as(3)[THEN sym] euclidean_component.setsum unfolding sumbas
- apply(rule setsum_cong2) by(auto simp add: basis_component)
- also have "... = u (basis i)" apply(subst setsum_delta) using goal1 by auto
- finally show ?case by auto
- qed
- hence **:"setsum u {basis i |i. i<DIM('a)} = setsum (op $$ x) ?D" unfolding sumbas
- apply-apply(rule setsum_cong2) by auto
- show "(\<forall>i<DIM('a). 0 \<le> x $$ i) \<and> setsum (op $$ x) ?D \<le> 1" apply - proof(rule,rule,rule)
- fix i assume i:"i<DIM('a)" show "0 \<le> 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:"\<forall>i<DIM('a). 0 \<le> x $$ i" "setsum (op $$ x) ?D \<le> 1"
- show "\<exists>u. (\<forall>x\<in>{basis i |i. i<DIM('a)}. 0 \<le> u x) \<and>
- setsum u {basis i |i. i<DIM('a)} \<le> 1 \<and> (\<Sum>x\<in>{basis i |i. i<DIM('a)}. u x *\<^sub>R x) = x"
- apply(rule_tac x="\<lambda>y. inner y x" in exI) apply safe using as(1)
- proof- show "(\<Sum>y\<in>{basis i |i. i < DIM('a)}. y \<bullet> x) \<le> 1" unfolding sumbas
- using as(2) unfolding euclidean_component_def[THEN sym] .
- show "(\<Sum>xa\<in>{basis i |i. i < DIM('a)}. (xa \<bullet> 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 "{..<DIM('a)}"] by auto
lemma interior_std_simplex:
"interior (convex hull (insert 0 { basis i| i. i<DIM('a)})) =
@@ -2552,4 +4171,1252 @@
also have "\<dots> < 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\<subseteq>{..<DIM('a::euclidean_space)}"
+ shows "rel_interior (convex hull (insert 0 { basis i| i. i : d})) =
+ {x::'a::euclidean_space. (\<forall>i\<in>d. 0 < x$$i) & setsum (%i. x$$i) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)}"
+ (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<DIM('a). i ~: d --> 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<DIM('a). i ~: d --> 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<DIM('a). i ~: d --> 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<DIM('a). i ~: d --> 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<DIM('a). i ~: d --> x$$i = 0)" apply(rule,rule)
+ proof-
+ fix i::nat assume "i:d"
+ hence "\<forall>ia\<in>d. 0 \<le> (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\<in>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 "\<And>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 (\<lambda>i. x$$i + (if a = i then e/2 else 0)) d" by(rule_tac setsum_cong, auto)
+ have h1: "(ALL i<DIM('a). i ~: d --> (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<e` `a:d` using `finite d` by(auto simp add: setsum_delta')
+ also have "\<dots> \<le> 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R basis a"] by auto
+ finally show "setsum (op $$ x) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)" using x0 by auto
+ qed
+}
+moreover
+{
+ fix x::"'a::euclidean_space" assume as: "x : ?s"
+ have "!i. ((0<x$$i) | (0=x$$i) --> 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<DIM('a). i ~: d --> y$$i = 0)"
+ have "setsum (op $$ y) d \<le> setsum (\<lambda>i. x$$i + ?d) d" proof(rule setsum_mono)
+ fix i assume i:"i\<in>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 \<le> x $$ i + ?d" by auto qed
+ also have "\<dots> \<le> 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 \<le> 1" .
+
+ fix i assume "i<DIM('a)" thus "0 \<le> y$$i"
+ proof(cases "i\<in>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 \<le> 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<DIM('a). i ~: d --> 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\<subseteq>{..<DIM('a::euclidean_space)}"
+ obtains a::"'a::euclidean_space" where
+ "a : rel_interior(convex hull (insert 0 {basis i | i . i : d}))" proof-
+(* Proof is a modified copy of the proof of similar lemma interior_std_simplex_nonempty in Convex_Euclidean_Space.thy *)
+ let ?D = d let ?a = "setsum (\<lambda>b::'a::euclidean_space. inverse (2 * real (card d)) *\<^sub>R b) {(basis i) | i. i \<in> ?D}"
+ have *:"{basis i :: 'a | i. i \<in> ?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 (\<lambda>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 (\<lambda>i. inverse (2 * real (card d))) ?D"
+ by(rule setsum_cong2, rule **)
+ also have "\<dots> < 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 "i<DIM('a)" and "i~:d"
+ have "?a : (span {basis i | i. i : d})"
+ apply (rule span_setsum[of "{basis i |i. i : d}" "(%b. b /\<^sub>R (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 "\<forall>x\<in>{basis i |i. i \<in> d}. x /\<^sub>R (2 * real (card d)) \<in> span {basis i ::'a |i. i \<in> d}" by auto
+ qed
+ thus "?a $$ i = 0 " using `i~:d` unfolding span_substd_basis[OF assms(2)] using `i<DIM('a)` by auto
+ qed
+qed
+
+subsection{* Relative Interior of Convex Set *}
+
+lemma rel_interior_convex_nonempty_aux:
+fixes S :: "('n::euclidean_space) set"
+assumes "convex S" and "0 : S"
+shows "rel_interior S ~= {}"
+proof-
+{ assume "S = {0}" hence ?thesis using rel_interior_sing by auto }
+moreover {
+assume "S ~= {0}"
+obtain B where B_def: "independent B & B<=S & (S <= span B) & card B = dim S" using basis_exists[of S] by auto
+hence "B~={}" using B_def assms `S ~= {0}` span_empty by auto
+have "insert 0 B <= span B" using subspace_span[of B] subspace_0[of "span B"] span_inc by auto
+hence "span (insert 0 B) <= span B"
+ using span_span[of B] span_mono[of "insert 0 B" "span B"] by blast
+hence "convex hull insert 0 B <= span B"
+ using convex_hull_subset_span[of "insert 0 B"] by auto
+hence "span (convex hull insert 0 B) <= span B"
+ using span_span[of B] span_mono[of "convex hull insert 0 B" "span B"] by blast
+hence *: "span (convex hull insert 0 B) = span B"
+ using span_mono[of B "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
+hence "span (convex hull insert 0 B) = span S"
+ using B_def span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
+moreover have "0 : affine hull (convex hull insert 0 B)"
+ using hull_subset[of "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
+ultimately have **: "affine hull (convex hull insert 0 B) = affine hull S"
+ using affine_hull_span_0[of "convex hull insert 0 B"] affine_hull_span_0[of "S"]
+ assms hull_subset[of S] by auto
+obtain d and f::"'n=>'n" where fd: "card d = card B & linear f & f ` B = {basis i |i. i : (d :: nat set)} &
+ f ` span B = {x. ALL i<DIM('n). i ~: d --> x $$ i = (0::real)} & inj_on f (span B)" and d:"d\<subseteq>{..<DIM('n)}"
+ using basis_to_substdbasis_subspace_isomorphism[of B,OF _ ] B_def by auto
+hence "bounded_linear f" using linear_conv_bounded_linear by auto
+have "d ~={}" using fd B_def `B ~={}` by auto
+have "(insert 0 {basis i |i. i : d}) = f ` (insert 0 B)" using fd linear_0 by auto
+hence "(convex hull (insert 0 {basis i |i. i : d})) = f ` (convex hull (insert 0 B))"
+ using convex_hull_linear_image[of f "(insert 0 {basis i |i. i : d})"]
+ convex_hull_linear_image[of f "(insert 0 B)"] `bounded_linear f` by auto
+moreover have "rel_interior (f ` (convex hull insert 0 B)) =
+ f ` rel_interior (convex hull insert 0 B)"
+ apply (rule rel_interior_injective_on_span_linear_image[of f "(convex hull insert 0 B)"])
+ using `bounded_linear f` fd * by auto
+ultimately have "rel_interior (convex hull insert 0 B) ~= {}"
+ using rel_interior_substd_simplex_nonempty[OF `d~={}` d] apply auto by blast
+moreover have "convex hull (insert 0 B) <= S"
+ using B_def assms hull_mono[of "insert 0 B" "S" "convex"] convex_hull_eq by auto
+ultimately have ?thesis using subset_rel_interior[of "convex hull insert 0 B" S] ** by auto
+} ultimately show ?thesis by auto
+qed
+
+lemma rel_interior_convex_nonempty:
+fixes S :: "('n::euclidean_space) set"
+assumes "convex S"
+shows "rel_interior S = {} <-> 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 "0<u" using assm by auto
+ thus ?thesis
+ using assm rel_interior_convex_shrink[of S y x u] assms `x:S` by auto
+ next
+ case True thus ?thesis using assm by auto
+ qed
+ hence "(1-u) *\<^sub>R 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<e" using e_def assms divide_pos_pos[of a "a+b"] by auto
+moreover have "e<=1" using e_def assms by auto
+ultimately show ?thesis using that[of e] by auto
+qed
+
+lemma convex_rel_interior_closure:
+ fixes S :: "('n::euclidean_space) set"
+ assumes "convex S"
+ shows "rel_interior (closure S) = rel_interior S"
+proof-
+{ assume "S={}" hence ?thesis using assms rel_interior_convex_nonempty by auto }
+moreover
+{ assume "S ~= {}"
+ have "rel_interior (closure S) >= 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 "0<e1 & e1<1" using e_def by auto
+hence "z=y-(1-e1)*\<^sub>R (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<e1 & e1<1` `y:S` x_def assms by auto
+qed
+
+lemma convex_rel_interior_iff:
+fixes S :: "('n::euclidean_space) set"
+assumes "convex S" "S ~= {}"
+shows "z : rel_interior S <-> (!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