(*  Title:      HOL/Library/Convex_Euclidean_Space.thy

     Author:     Robert Himmelmann, TU Muenchen

 *)

 header {* Convex sets, functions and related things. *}

 theory Convex_Euclidean_Space

 imports Topology_Euclidean_Space

 begin

 (* ------------------------------------------------------------------------- *)

 (* To be moved elsewhere                                                     *)

 (* ------------------------------------------------------------------------- *)

 declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp]

 declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp]

 declare dot_ladd[simp] dot_radd[simp] dot_lsub[simp] dot_rsub[simp]

 declare dot_lmult[simp] dot_rmult[simp] dot_lneg[simp] dot_rneg[simp]

 declare UNIV_1[simp]

 term "(x::real^'n \<Rightarrow> real) 0"

 lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto

 lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_less_eq_def Cart_lambda_beta dest_vec1_def basis_component vector_uminus_component

 lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id

 lemmas continuous_on_intros = continuous_on_add continuous_on_const continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg continuous_on_sub

   uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub

 lemma dest_vec1_simps[simp]: fixes a::"real^1"

   shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)

   "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"

   by(auto simp add:vector_component_simps all_1 Cart_eq)

 lemma nequals0I:"x\<in>A \<Longrightarrow> A \<noteq> {}" by auto

 lemma norm_not_0:"(x::real^'n::finite)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto

 lemma setsum_delta_notmem: assumes "x\<notin>s"

   shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s"

         "setsum (\<lambda>y. if (x = y) then P x else Q y) s = setsum Q s"

         "setsum (\<lambda>y. if (y = x) then P y else Q y) s = setsum Q s"

         "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"

   apply(rule_tac [!] setsum_cong2) using assms by auto

 lemma setsum_delta'':

   fixes s::"'a::real_vector set" assumes "finite s"

   shows "(\<Sum>x\<in>s. (if y = x then f x else 0) *\<^sub>R x) = (if y\<in>s then (f y) *\<^sub>R y else 0)"

 proof-

   have *:"\<And>x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)" by auto

   show ?thesis unfolding * using setsum_delta[OF assms, of y "\<lambda>x. f x *\<^sub>R x"] by auto

 qed

 lemma not_disjointI:"x\<in>A \<Longrightarrow> x\<in>B \<Longrightarrow> A \<inter> B \<noteq> {}" by blast

 lemma if_smult:"(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by auto

 lemma mem_interval_1: fixes x :: "real^1" shows

  "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"

  "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"

 by(simp_all add: Cart_eq vector_less_def vector_less_eq_def dest_vec1_def all_1)

 lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n::finite)) ` {a..b} =

   (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"

   using image_affinity_interval[of m 0 a b] by auto

 lemma dest_vec1_inverval:

   "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"

   "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"

   "dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"

   "dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"

   apply(rule_tac [!] equalityI)

   unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff

   apply(rule_tac [!] allI)apply(rule_tac [!] impI)

   apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)

   apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)

   by (auto simp add: vector_less_def vector_less_eq_def all_1 dest_vec1_def

     vec1_dest_vec1[unfolded dest_vec1_def One_nat_def])

 lemma dest_vec1_setsum: assumes "finite S"

   shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"

   using dest_vec1_sum[OF assms] by auto

 lemma dist_triangle_eq:

   fixes x y z :: "real ^ _"

   shows "dist x z = dist x y + dist y z \<longleftrightarrow> norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"

 proof- have *:"x - y + (y - z) = x - z" by auto

   show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded smult_conv_scaleR *]

     by(auto simp add:norm_minus_commute) qed

 lemma norm_eqI:"x = y \<Longrightarrow> norm x = norm y" by auto 

 lemma norm_minus_eqI:"(x::real^'n::finite) = - y \<Longrightarrow> norm x = norm y" by auto

 lemma Min_grI: assumes "finite A" "A \<noteq> {}" "\<forall>a\<in>A. x < a" shows "x < Min A"

   unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto

 lemma dimindex_ge_1:"CARD(_::finite) \<ge> 1"

   using one_le_card_finite by auto

 lemma real_dimindex_ge_1:"real (CARD('n::finite)) \<ge> 1" 

   by(metis dimindex_ge_1 linorder_not_less real_eq_of_nat real_le_trans real_of_nat_1 real_of_nat_le_iff) 

 lemma real_dimindex_gt_0:"real (CARD('n::finite)) > 0" apply(rule less_le_trans[OF _ real_dimindex_ge_1]) by auto

 subsection {* Affine set and affine hull.*}

 definition

   affine :: "'a::real_vector set \<Rightarrow> bool" where

   "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"

 lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"

 proof- have *:"\<And>u v ::real. u + v = 1 \<longleftrightarrow> v = 1 - u" by auto

   { fix x y assume "x\<in>s" "y\<in>s"

     hence "(\<forall>u v::real. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s) \<longleftrightarrow> (\<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)" apply auto 

       apply(erule_tac[!] x="1 - u" in allE) unfolding * by auto  }

   thus ?thesis unfolding affine_def by auto qed

 lemma affine_empty[intro]: "affine {}"

   unfolding affine_def by auto

 lemma affine_sing[intro]: "affine {x}"

   unfolding affine_alt by (auto simp add: scaleR_left_distrib [symmetric])

 lemma affine_UNIV[intro]: "affine UNIV"

   unfolding affine_def by auto

 lemma affine_Inter: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter> f)"

   unfolding affine_def by auto 

 lemma affine_Int: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"

   unfolding affine_def by auto

 lemma affine_affine_hull: "affine(affine hull s)"

   unfolding hull_def using affine_Inter[of "{t \<in> affine. s \<subseteq> t}"]

   unfolding mem_def by auto

 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"

 proof-

   { fix f assume "f \<subseteq> affine"

     hence "affine (\<Inter>f)" using affine_Inter[of f] unfolding subset_eq mem_def by auto  }

   thus ?thesis using hull_eq[unfolded mem_def, of affine s] by auto

 qed

 lemma setsum_restrict_set'': assumes "finite A"

   shows "setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"

   unfolding mem_def[of _ P, symmetric] unfolding setsum_restrict_set'[OF assms] ..

 subsection {* Some explicit formulations (from Lars Schewe). *}

 lemma affine: fixes V::"'a::real_vector set"

   shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)"

 unfolding affine_def apply rule apply(rule, rule, rule) apply(erule conjE)+ 

 defer apply(rule, rule, rule, rule, rule) proof-

   fix x y u v assume as:"x \<in> V" "y \<in> V" "u + v = (1::real)"

     "\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V"

   thus "u *\<^sub>R x + v *\<^sub>R y \<in> V" apply(cases "x=y")

     using as(4)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>w. if w = x then u else v"]] and as(1-3) 

     by(auto simp add: scaleR_left_distrib[THEN sym])

 next

   fix s u assume as:"\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"

     "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = (1::real)"

   def n \<equiv> "card s"

   have "card s = 0 \<or> card s = 1 \<or> card s = 2 \<or> card s > 2" by auto

   thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" proof(auto simp only: disjE)

     assume "card s = 2" hence "card s = Suc (Suc 0)" by auto

     then obtain a b where "s = {a, b}" unfolding card_Suc_eq by auto

     thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5)

       by(auto simp add: setsum_clauses(2))

   next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s)

       case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real"

       assume IA:"\<And>u s.  \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s;

                s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n \<equiv> card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and

         as:"Suc n \<equiv> card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"

            "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1"

       have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr)

         assume " \<not> (\<exists>x\<in>s. u x \<noteq> 1)" hence "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto

         thus False using as(7) and `card s > 2` by (metis Numeral1_eq1_nat less_0_number_of less_int_code(15)

           less_nat_number_of not_less_iff_gr_or_eq of_nat_1 of_nat_eq_iff pos2 rel_simps(4)) qed

       then obtain x where x:"x\<in>s" "u x \<noteq> 1" by auto

       have c:"card (s - {x}) = card s - 1" apply(rule card_Diff_singleton) using `x\<in>s` as(4) by auto

       have *:"s = insert x (s - {x})" "finite (s - {x})" using `x\<in>s` and as(4) by auto

       have **:"setsum u (s - {x}) = 1 - u x"

         using setsum_clauses(2)[OF *(2), of u x, unfolded *(1)[THEN sym] as(7)] by auto

       have ***:"inverse (1 - u x) * setsum u (s - {x}) = 1" unfolding ** using `u x \<noteq> 1` by auto

       have "(\<Sum>xa\<in>s - {x}. (inverse (1 - u x) * u xa) *\<^sub>R xa) \<in> V" proof(cases "card (s - {x}) > 2")

         case True hence "s - {x} \<noteq> {}" "card (s - {x}) = n" unfolding c and as(1)[symmetric] proof(rule_tac ccontr) 

           assume "\<not> s - {x} \<noteq> {}" hence "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp 

           thus False using True by auto qed auto

         thus ?thesis apply(rule_tac IA[of "s - {x}" "\<lambda>y. (inverse (1 - u x) * u y)"])

         unfolding setsum_right_distrib[THEN sym] using as and *** and True by auto

       next case False hence "card (s - {x}) = Suc (Suc 0)" using as(2) and c by auto

         then obtain a b where "(s - {x}) = {a, b}" "a\<noteq>b" unfolding card_Suc_eq by auto

         thus ?thesis using as(3)[THEN bspec[where x=a], THEN bspec[where x=b]]

           using *** *(2) and `s \<subseteq> V` unfolding setsum_right_distrib by(auto simp add: setsum_clauses(2)) qed

       thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric]

          apply(subst *) unfolding setsum_clauses(2)[OF *(2)]

          using as(3)[THEN bspec[where x=x], THEN bspec[where x="(inverse (1 - u x)) *\<^sub>R (\<Sum>xa\<in>s - {x}. u xa *\<^sub>R xa)"], 

          THEN spec[where x="u x"], THEN spec[where x="1 - u x"]] and rev_subsetD[OF `x\<in>s` `s\<subseteq>V`] and `u x \<noteq> 1` by auto

     qed auto

   next assume "card s = 1" then obtain a where "s={a}" by(auto simp add: card_Suc_eq)

     thus ?thesis using as(4,5) by simp

   qed(insert `s\<noteq>{}` `finite s`, auto)

 qed

 lemma affine_hull_explicit:

   "affine hull p = {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> setsum (\<lambda>v. (u v) *\<^sub>R v) s = y}"

   apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq and mem_def[of _ affine]

   apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof-

   fix x assume "x\<in>p" thus "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"

     apply(rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) by auto

 next

   fix t x s u assume as:"p \<subseteq> t" "affine t" "finite s" "s \<noteq> {}" "s \<subseteq> p" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" 

   thus "x \<in> t" using as(2)[unfolded affine, THEN spec[where x=s], THEN spec[where x=u]] by auto

 next

   show "affine {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y}" unfolding affine_def

     apply(rule,rule,rule,rule,rule) unfolding mem_Collect_eq proof-

     fix u v ::real assume uv:"u + v = 1"

     fix x assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"

     then obtain sx ux where x:"finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "setsum ux sx = 1" "(\<Sum>v\<in>sx. ux v *\<^sub>R v) = x" by auto

     fix y assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"

     then obtain sy uy where y:"finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "setsum uy sy = 1" "(\<Sum>v\<in>sy. uy v *\<^sub>R v) = y" by auto

     have xy:"finite (sx \<union> sy)" using x(1) y(1) by auto

     have **:"(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy" by auto

     show "\<exists>s ua. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum ua s = 1 \<and> (\<Sum>v\<in>s. ua v *\<^sub>R v) = u *\<^sub>R x + v *\<^sub>R y"

       apply(rule_tac x="sx \<union> sy" in exI)

       apply(rule_tac x="\<lambda>a. (if a\<in>sx then u * ux a else 0) + (if a\<in>sy then v * uy a else 0)" in exI)

       unfolding scaleR_left_distrib setsum_addf if_smult scaleR_zero_left  ** setsum_restrict_set[OF xy, THEN sym]

       unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and setsum_right_distrib[THEN sym]

       unfolding x y using x(1-3) y(1-3) uv by simp qed qed

 lemma affine_hull_finite:

   assumes "finite s"

   shows "affine hull s = {y. \<exists>u. setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"

   unfolding affine_hull_explicit and expand_set_eq and mem_Collect_eq apply (rule,rule)

   apply(erule exE)+ apply(erule conjE)+ defer apply(erule exE) apply(erule conjE) proof-

   fix x u assume "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"

   thus "\<exists>sa u. finite sa \<and> \<not> (\<forall>x. (x \<in> sa) = (x \<in> {})) \<and> sa \<subseteq> s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = x"

     apply(rule_tac x=s in exI, rule_tac x=u in exI) using assms by auto

 next

   fix x t u assume "t \<subseteq> s" hence *:"s \<inter> t = t" by auto

   assume "finite t" "\<not> (\<forall>x. (x \<in> t) = (x \<in> {}))" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"

   thus "\<exists>u. setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)

     unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms, THEN sym] and * by auto qed

 subsection {* Stepping theorems and hence small special cases. *}

 lemma affine_hull_empty[simp]: "affine hull {} = {}"

   apply(rule hull_unique) unfolding mem_def by auto

 lemma affine_hull_finite_step:

   fixes y :: "'a::real_vector"

   shows "(\<exists>u. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1)

   "finite s \<Longrightarrow> (\<exists>u. setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y) \<longleftrightarrow>

                 (\<exists>v u. setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?as \<Longrightarrow> (?lhs = ?rhs)")

 proof-

   show ?th1 by simp

   assume ?as 

   { assume ?lhs

     then obtain u where u:"setsum u (insert a s) = w \<and> (\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto

     have ?rhs proof(cases "a\<in>s")

       case True hence *:"insert a s = s" by auto

       show ?thesis using u[unfolded *] apply(rule_tac x=0 in exI) by auto

     next

       case False thus ?thesis apply(rule_tac x="u a" in exI) using u and `?as` by auto 

     qed  } moreover

   { assume ?rhs

     then obtain v u where vu:"setsum u s = w - v"  "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto

     have *:"\<And>x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)" by auto

     have ?lhs proof(cases "a\<in>s")

       case True thus ?thesis

         apply(rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI)

         unfolding setsum_clauses(2)[OF `?as`]  apply simp

         unfolding scaleR_left_distrib and setsum_addf 

         unfolding vu and * and scaleR_zero_left

         by (auto simp add: setsum_delta[OF `?as`])

     next

       case False 

       hence **:"\<And>x. x \<in> s \<Longrightarrow> u x = (if x = a then v else u x)"

                "\<And>x. x \<in> s \<Longrightarrow> u x *\<^sub>R x = (if x = a then v *\<^sub>R x else u x *\<^sub>R x)" by auto

       from False show ?thesis

         apply(rule_tac x="\<lambda>x. if x=a then v else u x" in exI)

         unfolding setsum_clauses(2)[OF `?as`] and * using vu

         using setsum_cong2[of s "\<lambda>x. u x *\<^sub>R x" "\<lambda>x. if x = a then v *\<^sub>R x else u x *\<^sub>R x", OF **(2)]

         using setsum_cong2[of s u "\<lambda>x. if x = a then v else u x", OF **(1)] by auto  

     qed }

   ultimately show "?lhs = ?rhs" by blast

 qed

 lemma affine_hull_2:

   fixes a b :: "'a::real_vector"

   shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs")

 proof-

   have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 

          "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto

   have "?lhs = {y. \<exists>u. setsum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}"

     using affine_hull_finite[of "{a,b}"] by auto

   also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}"

     by(simp add: affine_hull_finite_step(2)[of "{b}" a]) 

   also have "\<dots> = ?rhs" unfolding * by auto

   finally show ?thesis by auto

 qed

 lemma affine_hull_3:

   fixes a b c :: "'a::real_vector"

   shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs")

 proof-

   have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 

          "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto

   show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step)

     unfolding * apply auto

     apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto

     apply(rule_tac x=u in exI) by(auto intro!: exI)

 qed

 subsection {* Some relations between affine hull and subspaces. *}

 lemma affine_hull_insert_subset_span:

   fixes a :: "real ^ _"

   shows "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"

   unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq smult_conv_scaleR

   apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof-

   fix x t u assume as:"finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"

   have "(\<lambda>x. x - a) ` (t - {a}) \<subseteq> {x - a |x. x \<in> s}" using as(3) by auto

   thus "\<exists>v. x = a + v \<and> (\<exists>S u. finite S \<and> S \<subseteq> {x - a |x. x \<in> s} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = v)"

     apply(rule_tac x="x - a" in exI)

     apply (rule conjI, simp)

     apply(rule_tac x="(\<lambda>x. x - a) ` (t - {a})" in exI)

     apply(rule_tac x="\<lambda>x. u (x + a)" in exI)

     apply (rule conjI) using as(1) apply simp

     apply (erule conjI)

     using as(1)

     apply (simp add: setsum_reindex[unfolded inj_on_def] scaleR_right_diff_distrib setsum_subtractf scaleR_left.setsum[THEN sym] setsum_diff1 scaleR_left_diff_distrib)

     unfolding as by simp qed

 lemma affine_hull_insert_span:

   fixes a :: "real ^ _"

   assumes "a \<notin> s"

   shows "affine hull (insert a s) =

             {a + v | v . v \<in> span {x - a | x.  x \<in> s}}"

   apply(rule, rule affine_hull_insert_subset_span) unfolding subset_eq Ball_def

   unfolding affine_hull_explicit and mem_Collect_eq proof(rule,rule,erule exE,erule conjE)

   fix y v assume "y = a + v" "v \<in> span {x - a |x. x \<in> s}"

   then obtain t u where obt:"finite t" "t \<subseteq> {x - a |x. x \<in> s}" "a + (\<Sum>v\<in>t. u v *\<^sub>R v) = y" unfolding span_explicit smult_conv_scaleR by auto

   def f \<equiv> "(\<lambda>x. x + a) ` t"

   have f:"finite f" "f \<subseteq> s" "(\<Sum>v\<in>f. u (v - a) *\<^sub>R (v - a)) = y - a" unfolding f_def using obt 

     by(auto simp add: setsum_reindex[unfolded inj_on_def])

   have *:"f \<inter> {a} = {}" "f \<inter> - {a} = f" using f(2) assms by auto

   show "\<exists>sa u. finite sa \<and> sa \<noteq> {} \<and> sa \<subseteq> insert a s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y"

     apply(rule_tac x="insert a f" in exI)

     apply(rule_tac x="\<lambda>x. if x=a then 1 - setsum (\<lambda>x. u (x - a)) f else u (x - a)" in exI)

     using assms and f unfolding setsum_clauses(2)[OF f(1)] and if_smult

     unfolding setsum_cases[OF f(1), of "{a}", unfolded singleton_iff] and *

     by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps) qed

 lemma affine_hull_span:

   fixes a :: "real ^ _"

   assumes "a \<in> s"

   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 {* Convexity. *}

 definition

   convex :: "'a::real_vector set \<Rightarrow> bool" where

   "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"

 lemma convex_alt: "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> ((1 - u) *\<^sub>R x + u *\<^sub>R y) \<in> s)"

 proof- have *:"\<And>u v::real. u + v = 1 \<longleftrightarrow> u = 1 - v" by auto

   show ?thesis unfolding convex_def apply auto

     apply(erule_tac x=x in ballE) apply(erule_tac x=y in ballE) apply(erule_tac x="1 - u" in allE)

     by (auto simp add: *) qed

 lemma mem_convex:

   assumes "convex s" "a \<in> s" "b \<in> s" "0 \<le> u" "u \<le> 1"

   shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"

   using assms unfolding convex_alt by auto

 lemma convex_empty[intro]: "convex {}"

   unfolding convex_def by simp

 lemma convex_singleton[intro]: "convex {a}"

   unfolding convex_def by (auto simp add:scaleR_left_distrib[THEN sym])

 lemma convex_UNIV[intro]: "convex UNIV"

   unfolding convex_def by auto

 lemma convex_Inter: "(\<forall>s\<in>f. convex s) ==> convex(\<Inter> f)"

   unfolding convex_def by auto

 lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"

   unfolding convex_def by auto

 lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"

   unfolding convex_def apply auto

   unfolding inner_add inner_scaleR

   by (metis real_convex_bound_le)

 lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"

 proof- have *:"{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}" by auto

   show ?thesis apply(unfold *) using convex_halfspace_le[of "-a" "-b"] by auto qed

 lemma convex_hyperplane: "convex {x. inner a x = b}"

 proof-

   have *:"{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}" by auto

   show ?thesis unfolding * apply(rule convex_Int)

     using convex_halfspace_le convex_halfspace_ge by auto

 qed

 lemma convex_halfspace_lt: "convex {x. inner a x < b}"

   unfolding convex_def

   by(auto simp add: real_convex_bound_lt inner_add)

 lemma convex_halfspace_gt: "convex {x. inner a x > b}"

    using convex_halfspace_lt[of "-a" "-b"] by auto

 lemma convex_positive_orthant: "convex {x::real^'n::finite. (\<forall>i. 0 \<le> x$i)}"

   unfolding convex_def apply auto apply(erule_tac x=i in allE)+

   apply(rule add_nonneg_nonneg) by(auto simp add: mult_nonneg_nonneg)

 subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}

 lemma convex: "convex s \<longleftrightarrow>

   (\<forall>(k::nat) u x. (\<forall>i. 1\<le>i \<and> i\<le>k \<longrightarrow> 0 \<le> u i \<and> x i \<in>s) \<and> (setsum u {1..k} = 1)

            \<longrightarrow> setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} \<in> s)"

   unfolding convex_def apply rule apply(rule allI)+ defer apply(rule ballI)+ apply(rule allI)+ proof(rule,rule,rule,rule)

   fix x y u v assume as:"\<forall>(k::nat) u x. (\<forall>i. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R x i) \<in> s"

     "x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"

   show "u *\<^sub>R x + v *\<^sub>R y \<in> s" using as(1)[THEN spec[where x=2], THEN spec[where x="\<lambda>n. if n=1 then u else v"], THEN spec[where x="\<lambda>n. if n=1 then x else y"]] and as(2-)

     by (auto simp add: setsum_head_Suc) 

 next

   fix k u x assume as:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" 

   show "(\<forall>i::nat. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R x i) \<in> s" apply(rule,erule conjE) proof(induct k arbitrary: u)

   case (Suc k) show ?case proof(cases "u (Suc k) = 1")

     case True hence "(\<Sum>i = Suc 0..k. u i *\<^sub>R x i) = 0" apply(rule_tac setsum_0') apply(rule ccontr) unfolding ball_simps apply(erule bexE) proof-

       fix i assume i:"i \<in> {Suc 0..k}" "u i *\<^sub>R x i \<noteq> 0"

       hence ui:"u i \<noteq> 0" by auto

       hence "setsum (\<lambda>k. if k=i then u i else 0) {1 .. k} \<le> setsum u {1 .. k}" apply(rule_tac setsum_mono) using Suc(2) by auto

       hence "setsum u {1 .. k} \<ge> u i" using i(1) by(auto simp add: setsum_delta) 

       hence "setsum u {1 .. k} > 0"  using ui apply(rule_tac less_le_trans[of _ "u i"]) using Suc(2)[THEN spec[where x=i]] and i(1) by auto

       thus False using Suc(3) unfolding setsum_cl_ivl_Suc and True by simp qed

     thus ?thesis unfolding setsum_cl_ivl_Suc using True and Suc(2) by auto

   next

     have *:"setsum u {1..k} = 1 - u (Suc k)" using Suc(3)[unfolded setsum_cl_ivl_Suc] by auto

     have **:"u (Suc k) \<le> 1" apply(rule ccontr) unfolding not_le using Suc(3) using setsum_nonneg[of "{1..k}" u] using Suc(2) by auto

     have ***:"\<And>i k. (u i / (1 - u (Suc k))) *\<^sub>R x i = (inverse (1 - u (Suc k))) *\<^sub>R (u i *\<^sub>R x i)" unfolding real_divide_def by (auto simp add: algebra_simps)

     case False hence nn:"1 - u (Suc k) \<noteq> 0" by auto

     have "(\<Sum>i = 1..k. (u i / (1 - u (Suc k))) *\<^sub>R x i) \<in> s" apply(rule Suc(1)) unfolding setsum_divide_distrib[THEN sym] and *

       apply(rule_tac allI) apply(rule,rule) apply(rule divide_nonneg_pos) using nn Suc(2) ** by auto

     hence "(1 - u (Suc k)) *\<^sub>R (\<Sum>i = 1..k. (u i / (1 - u (Suc k))) *\<^sub>R x i) + u (Suc k) *\<^sub>R x (Suc k) \<in> s"

       apply(rule as[THEN bspec, THEN bspec, THEN spec, THEN mp, THEN spec, THEN mp, THEN mp]) using Suc(2)[THEN spec[where x="Suc k"]] and ** by auto

     thus ?thesis unfolding setsum_cl_ivl_Suc and *** and scaleR_right.setsum [symmetric] using nn by auto qed qed auto qed

 lemma convex_explicit:

   fixes s :: "'a::real_vector set"

   shows "convex s \<longleftrightarrow>

   (\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) t \<in> s)"

   unfolding convex_def apply(rule,rule,rule) apply(subst imp_conjL,rule) defer apply(rule,rule,rule,rule,rule,rule,rule) proof-

   fix x y u v assume as:"\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" "x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"

   show "u *\<^sub>R x + v *\<^sub>R y \<in> s" proof(cases "x=y")

     case True show ?thesis unfolding True and scaleR_left_distrib[THEN sym] using as(3,6) by auto next

     case False thus ?thesis using as(1)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>z. if z=x then u else v"]] and as(2-) by auto qed

 next 

   fix t u assume asm:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" "finite (t::'a set)"

   (*"finite t" "t \<subseteq> s" "\<forall>x\<in>t. (0::real) \<le> u x" "setsum u t = 1"*)

   from this(2) have "\<forall>u. t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" apply(induct_tac t rule:finite_induct)

     prefer 3 apply (rule,rule) apply(erule conjE)+ proof-

     fix x f u assume ind:"\<forall>u. f \<subseteq> s \<and> (\<forall>x\<in>f. 0 \<le> u x) \<and> setsum u f = 1 \<longrightarrow> (\<Sum>x\<in>f. u x *\<^sub>R x) \<in> s"

     assume as:"finite f" "x \<notin> f" "insert x f \<subseteq> s" "\<forall>x\<in>insert x f. 0 \<le> u x" "setsum u (insert x f) = (1::real)"

     show "(\<Sum>x\<in>insert x f. u x *\<^sub>R x) \<in> s" proof(cases "u x = 1")

       case True hence "setsum (\<lambda>x. u x *\<^sub>R x) f = 0" apply(rule_tac setsum_0') apply(rule ccontr) unfolding ball_simps apply(erule bexE) proof-

         fix y assume y:"y \<in> f" "u y *\<^sub>R y \<noteq> 0"

         hence uy:"u y \<noteq> 0" by auto

         hence "setsum (\<lambda>k. if k=y then u y else 0) f \<le> setsum u f" apply(rule_tac setsum_mono) using as(4) by auto

         hence "setsum u f \<ge> u y" using y(1) and as(1) by(auto simp add: setsum_delta) 

         hence "setsum u f > 0" using uy apply(rule_tac less_le_trans[of _ "u y"]) using as(4) and y(1) by auto

         thus False using as(2,5) unfolding setsum_clauses(2)[OF as(1)] and True by auto qed

       thus ?thesis unfolding setsum_clauses(2)[OF as(1)] using as(2,3) unfolding True by auto

     next

       have *:"setsum u f = setsum u (insert x f) - u x" using as(2) unfolding setsum_clauses(2)[OF as(1)] by auto

       have **:"u x \<le> 1" apply(rule ccontr) unfolding not_le using as(5)[unfolded setsum_clauses(2)[OF as(1)]] and as(2)

         using setsum_nonneg[of f u] and as(4) by auto

       case False hence "inverse (1 - u x) *\<^sub>R (\<Sum>x\<in>f. u x *\<^sub>R x) \<in> s" unfolding scaleR_right.setsum and scaleR_scaleR

         apply(rule_tac ind[THEN spec, THEN mp]) apply rule defer apply rule apply rule apply(rule mult_nonneg_nonneg)

         unfolding setsum_right_distrib[THEN sym] and * using as and ** by auto

       hence "u x *\<^sub>R x + (1 - u x) *\<^sub>R ((inverse (1 - u x)) *\<^sub>R setsum (\<lambda>x. u x *\<^sub>R x) f) \<in>s" 

         apply(rule_tac asm(1)[THEN bspec, THEN bspec, THEN spec, THEN mp, THEN spec, THEN mp, THEN mp]) using as and ** False by auto 

       thus ?thesis unfolding setsum_clauses(2)[OF as(1)] using as(2) and False by auto qed

   qed auto thus "t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" by auto

 qed

 lemma convex_finite: assumes "finite s"

   shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1

                       \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"

   unfolding convex_explicit apply(rule, rule, rule) defer apply(rule,rule,rule)apply(erule conjE)+ proof-

   fix t u assume as:"\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s" " finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"

   have *:"s \<inter> t = t" using as(3) by auto

   show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" using as(1)[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]]

     unfolding if_smult and setsum_cases[OF assms] and * using as(2-) by auto

 qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)

 subsection {* Cones. *}

 definition

   cone :: "'a::real_vector set \<Rightarrow> bool" where

   "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)"

 lemma cone_empty[intro, simp]: "cone {}"

   unfolding cone_def by auto

 lemma cone_univ[intro, simp]: "cone UNIV"

   unfolding cone_def by auto

 lemma cone_Inter[intro]: "(\<forall>s\<in>f. cone s) \<Longrightarrow> cone(\<Inter> f)"

   unfolding cone_def by auto

 subsection {* Conic hull. *}

 lemma cone_cone_hull: "cone (cone hull s)"

   unfolding hull_def using cone_Inter[of "{t \<in> conic. s \<subseteq> t}"] 

   by (auto simp add: mem_def)

 lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s"

   apply(rule hull_eq[unfolded mem_def])

   using cone_Inter unfolding subset_eq by (auto simp add: mem_def)

 subsection {* Affine dependence and consequential theorems (from Lars Schewe). *}

 definition

   affine_dependent :: "'a::real_vector set \<Rightarrow> bool" where

   "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> (affine hull (s - {x})))"

 lemma affine_dependent_explicit:

   "affine_dependent p \<longleftrightarrow>

     (\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and>

     (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)"

   unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq apply(rule)

   apply(erule bexE,erule exE,erule exE) apply(erule conjE)+ defer apply(erule exE,erule exE) apply(erule conjE)+ apply(erule bexE)

 proof-

   fix x s u assume as:"x \<in> p" "finite s" "s \<noteq> {}" "s \<subseteq> p - {x}" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"

   have "x\<notin>s" using as(1,4) by auto

   show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0"

     apply(rule_tac x="insert x s" in exI, rule_tac x="\<lambda>v. if v = x then - 1 else u v" in exI)

     unfolding if_smult and setsum_clauses(2)[OF as(2)] and setsum_delta_notmem[OF `x\<notin>s`] and as using as by auto 

 next

   fix s u v assume as:"finite s" "s \<subseteq> p" "setsum u s = 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" "v \<in> s" "u v \<noteq> 0"

   have "s \<noteq> {v}" using as(3,6) by auto

   thus "\<exists>x\<in>p. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p - {x} \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" 

     apply(rule_tac x=v in bexI, rule_tac x="s - {v}" in exI, rule_tac x="\<lambda>x. - (1 / u v) * u x" in exI)

     unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)] using as by auto

 qed

 lemma affine_dependent_explicit_finite:

   fixes s :: "'a::real_vector set" assumes "finite s"

   shows "affine_dependent s \<longleftrightarrow> (\<exists>u. setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)"

   (is "?lhs = ?rhs")

 proof

   have *:"\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))" by auto

   assume ?lhs

   then obtain t u v where "finite t" "t \<subseteq> s" "setsum u t = 0" "v\<in>t" "u v \<noteq> 0"  "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0"

     unfolding affine_dependent_explicit by auto

   thus ?rhs apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)

     apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym]

     unfolding Int_absorb1[OF `t\<subseteq>s`] by auto

 next

   assume ?rhs

   then obtain u v where "setsum u s = 0"  "v\<in>s" "u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" by auto

   thus ?lhs unfolding affine_dependent_explicit using assms by auto

 qed

 subsection {* A general lemma. *}

 lemma convex_connected:

   fixes s :: "'a::real_normed_vector set"

   assumes "convex s" shows "connected s"

 proof-

   { fix e1 e2 assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2" 

     assume "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}"

     then obtain x1 x2 where x1:"x1\<in>e1" "x1\<in>s" and x2:"x2\<in>e2" "x2\<in>s" by auto

     hence n:"norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto

     { fix x e::real assume as:"0 \<le> x" "x \<le> 1" "0 < e"

       { fix y have *:"(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2"

           by (simp add: algebra_simps)

         assume "\<bar>y - x\<bar> < e / norm (x1 - x2)"

         hence "norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"

           unfolding * and scaleR_right_diff_distrib[THEN sym]

           unfolding less_divide_eq using n by auto  }

       hence "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"

         apply(rule_tac x="e / norm (x1 - x2)" in exI) using as

         apply auto unfolding zero_less_divide_iff using n by simp  }  note * = this

     have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2"

       apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+

       using * apply(simp add: dist_norm)

       using as(1,2)[unfolded open_dist] apply simp

       using as(1,2)[unfolded open_dist] apply simp

       using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2

       using as(3) by auto

     then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1"  "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2" by auto

     hence False using as(4) 

       using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]]

       using x1(2) x2(2) by auto  }

   thus ?thesis unfolding connected_def by auto

 qed

 subsection {* One rather trivial consequence. *}

 lemma connected_UNIV: "connected (UNIV :: 'a::real_normed_vector set)"

   by(simp add: convex_connected convex_UNIV)

 subsection {* Convex functions into the reals. *}

 definition

   convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" where

   "convex_on s f \<longleftrightarrow>

   (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"

 lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"

   unfolding convex_on_def by auto

 lemma convex_add:

   assumes "convex_on s f" "convex_on s g"

   shows "convex_on s (\<lambda>x. f x + g x)"

 proof-

   { fix x y assume "x\<in>s" "y\<in>s" moreover

     fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"

     ultimately have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> (u * f x + v * f y) + (u * g x + v * g y)"

       using assms(1)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]

       using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]

       apply - apply(rule add_mono) by auto

     hence "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)" by (simp add: ring_simps)  }

   thus ?thesis unfolding convex_on_def by auto 

 qed

 lemma convex_cmul: 

   assumes "0 \<le> (c::real)" "convex_on s f"

   shows "convex_on s (\<lambda>x. c * f x)"

 proof-

   have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: ring_simps)

   show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto

 qed

 lemma convex_lower:

   assumes "convex_on s f"  "x\<in>s"  "y \<in> s"  "0 \<le> u"  "0 \<le> v"  "u + v = 1"

   shows "f (u *\<^sub>R x + v *\<^sub>R y) \<le> max (f x) (f y)"

 proof-

   let ?m = "max (f x) (f y)"

   have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)" apply(rule add_mono) 

     using assms(4,5) by(auto simp add: mult_mono1)

   also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto

   finally show ?thesis using assms(1)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]

     using assms(2-6) by auto 

 qed

 lemma convex_local_global_minimum:

   fixes s :: "'a::real_normed_vector set"

   assumes "0<e" "convex_on s f" "ball x e \<subseteq> s" "\<forall>y\<in>ball x e. f x \<le> f y"

   shows "\<forall>y\<in>s. f x \<le> f y"

 proof(rule ccontr)

   have "x\<in>s" using assms(1,3) by auto

   assume "\<not> (\<forall>y\<in>s. f x \<le> f y)"

   then obtain y where "y\<in>s" and y:"f x > f y" by auto

   hence xy:"0 < dist x y" by (auto simp add: dist_nz[THEN sym])

   then obtain u where "0 < u" "u \<le> 1" and u:"u < e / dist x y"

     using real_lbound_gt_zero[of 1 "e / dist x y"] using xy `e>0` and divide_pos_pos[of e "dist x y"] by auto

   hence "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y" using `x\<in>s` `y\<in>s`

     using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto

   moreover

   have *:"x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" by (simp add: algebra_simps)

   have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0<u`] unfolding dist_norm[THEN sym]

     using u unfolding pos_less_divide_eq[OF xy] by auto

   hence "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto

   ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto

 qed

 lemma convex_distance:

   fixes s :: "'a::real_normed_vector set"

   shows "convex_on s (\<lambda>x. dist a x)"

 proof(auto simp add: convex_on_def dist_norm)

   fix x y assume "x\<in>s" "y\<in>s"

   fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"

   have "a = u *\<^sub>R a + v *\<^sub>R a" unfolding scaleR_left_distrib[THEN sym] and `u+v=1` by simp

   hence *:"a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))"

     by (auto simp add: algebra_simps)

   show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)"

     unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"]

     using `0 \<le> u` `0 \<le> v` by auto

 qed

 subsection {* Arithmetic operations on sets preserve convexity. *}

 lemma convex_scaling: "convex s \<Longrightarrow> convex ((\<lambda>x. c *\<^sub>R x) ` s)"

   unfolding convex_def and image_iff apply auto

   apply (rule_tac x="u *\<^sub>R x+v *\<^sub>R y" in bexI) by (auto simp add: algebra_simps)

 lemma convex_negations: "convex s \<Longrightarrow> convex ((\<lambda>x. -x)` s)"

   unfolding convex_def and image_iff apply auto

   apply (rule_tac x="u *\<^sub>R x+v *\<^sub>R y" in bexI) by auto

 lemma convex_sums:

   assumes "convex s" "convex t"

   shows "convex {x + y| x y. x \<in> s \<and> y \<in> t}"

 proof(auto simp add: convex_def image_iff scaleR_right_distrib)

   fix xa xb ya yb assume xy:"xa\<in>s" "xb\<in>s" "ya\<in>t" "yb\<in>t"

   fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"

   show "\<exists>x y. u *\<^sub>R xa + u *\<^sub>R ya + (v *\<^sub>R xb + v *\<^sub>R yb) = x + y \<and> x \<in> s \<and> y \<in> t"

     apply(rule_tac x="u *\<^sub>R xa + v *\<^sub>R xb" in exI) apply(rule_tac x="u *\<^sub>R ya + v *\<^sub>R yb" in exI)

     using assms(1)[unfolded convex_def, THEN bspec[where x=xa], THEN bspec[where x=xb]]

     using assms(2)[unfolded convex_def, THEN bspec[where x=ya], THEN bspec[where x=yb]]

     using uv xy by auto

 qed

 lemma convex_differences: 

   assumes "convex s" "convex t"

   shows "convex {x - y| x y. x \<in> s \<and> y \<in> t}"

 proof-

   have "{x - y| x y. x \<in> s \<and> y \<in> t} = {x + y |x y. x \<in> s \<and> y \<in> uminus ` t}" unfolding image_iff apply auto

     apply(rule_tac x=xa in exI) apply(rule_tac x="-y" in exI) apply simp

     apply(rule_tac x=xa in exI) apply(rule_tac x=xb in exI) by simp

   thus ?thesis using convex_sums[OF assms(1)  convex_negations[OF assms(2)]] by auto

 qed

 lemma convex_translation: assumes "convex s" shows "convex ((\<lambda>x. a + x) ` s)"

 proof- have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s" by auto

   thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed

 lemma convex_affinity: assumes "convex s" shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)"

 proof- have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto

   thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed

 lemma convex_linear_image:

   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:"x \<in> s" "y \<in> s"

   fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"

   show "u *\<^sub>R f x + v *\<^sub>R f y \<in> f ` s" unfolding image_iff

     apply(rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in bexI)

     unfolding f.add f.scaleR

     using c[unfolded convex_def] xy uv by auto

 qed

 subsection {* Balls, being convex, are connected. *}

 lemma convex_ball:

   fixes x :: "'a::real_normed_vector"

   shows "convex (ball x e)" 

 proof(auto simp add: convex_def)

   fix y z assume yz:"dist x y < e" "dist x z < e"

   fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"

   have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz

     using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto

   thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using real_convex_bound_lt[OF yz uv] by auto 

 qed

 lemma convex_cball:

   fixes x :: "'a::real_normed_vector"

   shows "convex(cball x e)"

 proof(auto simp add: convex_def Ball_def mem_cball)

   fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e"

   fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"

   have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz

     using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto

   thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using real_convex_bound_le[OF yz uv] by auto 

 qed

 lemma connected_ball:

   fixes x :: "'a::real_normed_vector"

   shows "connected (ball x e)"

   using convex_connected convex_ball by auto

 lemma connected_cball:

   fixes x :: "'a::real_normed_vector"

   shows "connected(cball x e)"

   using convex_connected convex_cball by auto

 subsection {* Convex hull. *}

 lemma convex_convex_hull: "convex(convex hull s)"

   unfolding hull_def using convex_Inter[of "{t\<in>convex. s\<subseteq>t}"]

   unfolding mem_def by auto

 lemma convex_hull_eq: "(convex hull s = s) \<longleftrightarrow> convex s" apply(rule hull_eq[unfolded mem_def])

   using convex_Inter[unfolded Ball_def mem_def] by auto

 lemma bounded_convex_hull:

   fixes s :: "'a::real_normed_vector set"

   assumes "bounded s" shows "bounded(convex hull s)"

 proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto

   show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])

     unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]

     unfolding subset_eq mem_cball dist_norm using B by auto qed

 lemma finite_imp_bounded_convex_hull:

   fixes s :: "'a::real_normed_vector set"

   shows "finite s \<Longrightarrow> bounded(convex hull s)"

   using bounded_convex_hull finite_imp_bounded by auto

 subsection {* Stepping theorems for convex hulls of finite sets. *}

 lemma convex_hull_empty[simp]: "convex hull {} = {}"

   apply(rule hull_unique) unfolding mem_def by auto

 lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"

   apply(rule hull_unique) unfolding mem_def by auto

 lemma convex_hull_insert:

   fixes s :: "'a::real_vector set"

   assumes "s \<noteq> {}"

   shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>

                                     b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")

  apply(rule,rule hull_minimal,rule) unfolding mem_def[of _ convex] and insert_iff prefer 3 apply rule proof-

  fix x assume x:"x = a \<or> x \<in> s"

  thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer 

    apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto

 next

   fix x assume "x\<in>?hull"

   then obtain u v b where obt:"u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b" by auto

   have "a\<in>convex hull insert a s" "b\<in>convex hull insert a s"

     using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) by auto

   thus "x\<in> convex hull insert a s" unfolding obt(5) using convex_convex_hull[of "insert a s", unfolded convex_def]

     apply(erule_tac x=a in ballE) apply(erule_tac x=b in ballE) apply(erule_tac x=u in allE) using obt by auto

 next

   show "convex ?hull" unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof-

     fix x y u v assume as:"(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"

     from as(4) obtain u1 v1 b1 where obt1:"u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto

     from as(5) obtain u2 v2 b2 where obt2:"u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto

     have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)

     have "\<exists>b \<in> convex hull s. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"

     proof(cases "u * v1 + v * v2 = 0")

       have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)

       case True hence **:"u * v1 = 0" "v * v2 = 0" apply- apply(rule_tac [!] ccontr)

         using mult_nonneg_nonneg[OF `u\<ge>0` `v1\<ge>0`] mult_nonneg_nonneg[OF `v\<ge>0` `v2\<ge>0`] by auto

       hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto

       thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: ** scaleR_right_distrib)

     next

       have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)

       also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) 

       also have "\<dots> = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto

       case False have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2" apply -

         apply(rule add_nonneg_nonneg) prefer 4 apply(rule add_nonneg_nonneg) apply(rule_tac [!] mult_nonneg_nonneg)

         using as(1,2) obt1(1,2) obt2(1,2) by auto 

       thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False

         apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer

         apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4)

         unfolding add_divide_distrib[THEN sym] and real_0_le_divide_iff

         by (auto simp add: scaleR_left_distrib scaleR_right_distrib)

     qed note * = this

     have u1:"u1 \<le> 1" apply(rule ccontr) unfolding obt1(3)[THEN sym] and not_le using obt1(2) by auto

     have u2:"u2 \<le> 1" apply(rule ccontr) unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto

     have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)

       apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto

     also have "\<dots> \<le> 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto

     finally 

     show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)

       apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def

       using as(1,2) obt1(1,2) obt2(1,2) * by(auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps)

   qed

 qed

 subsection {* Explicit expression for convex hull. *}

 lemma convex_hull_indexed:

   fixes s :: "'a::real_vector set"

   shows "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>

                             (setsum u {1..k} = 1) \<and>

                             (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")

   apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer

   apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule)

 proof-

   fix x assume "x\<in>s"

   thus "x \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI) by auto

 next

   fix t assume as:"s \<subseteq> t" "convex t"

   show "?hull \<subseteq> t" apply(rule) unfolding mem_Collect_eq apply(erule exE | erule conjE)+ proof-

     fix x k u y assume assm:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> s" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"

     show "x\<in>t" unfolding assm(3)[THEN sym] apply(rule as(2)[unfolded convex, rule_format])

       using assm(1,2) as(1) by auto qed

 next

   fix x y u v assume uv:"0\<le>u" "0\<le>v" "u+v=(1::real)" and xy:"x\<in>?hull" "y\<in>?hull"

   from xy obtain k1 u1 x1 where x:"\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto

   from xy obtain k2 u2 x2 where y:"\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto

   have *:"\<And>P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"

     "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"

     prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le)

   have inj:"inj_on (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto  

   show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" apply(rule)

     apply(rule_tac x="k1 + k2" in exI, rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)

     apply(rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)" in exI) apply(rule,rule) defer apply(rule)

     unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def

     unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] setsum_right_distrib[THEN sym] proof-

     fix i assume i:"i \<in> {1..k1+k2}"

     show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and> (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"

     proof(cases "i\<in>{1..k1}")

       case True thus ?thesis using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto

     next def j \<equiv> "i - k1"

       case False with i have "j \<in> {1..k2}" unfolding j_def by auto

       thus ?thesis unfolding j_def[symmetric] using False

         using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]] by auto qed

   qed(auto simp add: not_le x(2,3) y(2,3) uv(3))

 qed

 lemma convex_hull_finite:

   fixes s :: "'a::real_vector set"

   assumes "finite s"

   shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>

          setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")

 proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set])

   fix x assume "x\<in>s" thus " \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x" 

     apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto

     unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto 

 next

   fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"

   fix ux assume ux:"\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"

   fix uy assume uy:"\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)"

   { fix x assume "x\<in>s"

     hence "0 \<le> u * ux x + v * uy x" using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)

       by (auto, metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2))  }

   moreover have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"

     unfolding setsum_addf and setsum_right_distrib[THEN sym] and ux(2) uy(2) using uv(3) by auto

   moreover have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"

     unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] by auto

   ultimately show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and> (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"

     apply(rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI) by auto 

 next

   fix t assume t:"s \<subseteq> t" "convex t" 

   fix u assume u:"\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)"

   thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]]

     using assms and t(1) by auto

 qed

 subsection {* Another formulation from Lars Schewe. *}

 lemma setsum_constant_scaleR:

   fixes y :: "'a::real_vector"

   shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"

 apply (cases "finite A")

 apply (induct set: finite)

 apply (simp_all add: algebra_simps)

 done

 lemma convex_hull_explicit:

   fixes p :: "'a::real_vector set"

   shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and>

              (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")

 proof-

   { fix x assume "x\<in>?lhs"

     then obtain k u y where obt:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> p" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"

       unfolding convex_hull_indexed by auto

     have fin:"finite {1..k}" by auto

     have fin':"\<And>v. finite {i \<in> {1..k}. y i = v}" by auto

     { fix j assume "j\<in>{1..k}"

       hence "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> y i = y j}"

         using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp

         apply(rule setsum_nonneg) using obt(1) by auto } 

     moreover

     have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v}) = 1"  

       unfolding setsum_image_gen[OF fin, THEN sym] using obt(2) by auto

     moreover have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v} *\<^sub>R v) = x"

       using setsum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, THEN sym]

       unfolding scaleR_left.setsum using obt(3) by auto

     ultimately have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"

       apply(rule_tac x="y ` {1..k}" in exI)

       apply(rule_tac x="\<lambda>v. setsum u {i\<in>{1..k}. y i = v}" in exI) by auto

     hence "x\<in>?rhs" by auto  }

   moreover

   { fix y assume "y\<in>?rhs"

     then obtain s u where obt:"finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto

     obtain f where f:"inj_on f {1..card s}" "f ` {1..card s} = s" using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto

     { fix i::nat assume "i\<in>{1..card s}"

       hence "f i \<in> s"  apply(subst f(2)[THEN sym]) by auto

       hence "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto  }

     moreover have *:"finite {1..card s}" by auto

     { fix y assume "y\<in>s"

       then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto

       hence "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] apply(erule_tac x=x in ballE) by auto

       hence "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto

       hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"

             "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"

         by (auto simp add: setsum_constant_scaleR)   }

     hence "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"

       unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f] 

       unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]

       using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto

     ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"

       apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastsimp

     hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto  }

   ultimately show ?thesis unfolding expand_set_eq by blast

 qed

 subsection {* A stepping theorem for that expansion. *}

 lemma convex_hull_finite_step:

   fixes s :: "'a::real_vector set" assumes "finite s"

   shows "(\<exists>u. (\<forall>x\<in>insert a s. 0 \<le> u x) \<and> setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y)

      \<longleftrightarrow> (\<exists>v\<ge>0. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?lhs = ?rhs")

 proof(rule, case_tac[!] "a\<in>s")

   assume "a\<in>s" hence *:"insert a s = s" by auto

   assume ?lhs thus ?rhs unfolding * apply(rule_tac x=0 in exI) by auto

 next

   assume ?lhs then obtain u where u:"\<forall>x\<in>insert a s. 0 \<le> u x" "setsum u (insert a s) = w" "(\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto

   assume "a\<notin>s" thus ?rhs apply(rule_tac x="u a" in exI) using u(1)[THEN bspec[where x=a]] apply simp

     apply(rule_tac x=u in exI) using u[unfolded setsum_clauses(2)[OF assms]] and `a\<notin>s` by auto

 next

   assume "a\<in>s" hence *:"insert a s = s" by auto

   have fin:"finite (insert a s)" using assms by auto

   assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto

   show ?lhs apply(rule_tac x="\<lambda>x. (if a = x then v else 0) + u x" in exI) unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin]

     unfolding setsum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and `a\<in>s` by auto

 next

   assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto

   moreover assume "a\<notin>s" moreover have "(\<Sum>x\<in>s. if a = x then v else u x) = setsum u s" "(\<Sum>x\<in>s. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)"

     apply(rule_tac setsum_cong2) defer apply(rule_tac setsum_cong2) using `a\<notin>s` by auto

   ultimately show ?lhs apply(rule_tac x="\<lambda>x. if a = x then v else u x" in exI)  unfolding setsum_clauses(2)[OF assms] by auto

 qed

 subsection {* Hence some special cases. *}

 lemma convex_hull_2:

   "convex hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b | u v. 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1}"

 proof- have *:"\<And>u. (\<forall>x\<in>{a, b}. 0 \<le> u x) \<longleftrightarrow> 0 \<le> u a \<and> 0 \<le> u b" by auto have **:"finite {b}" by auto

 show ?thesis apply(simp add: convex_hull_finite) unfolding convex_hull_finite_step[OF **, of a 1, unfolded * conj_assoc]

   apply auto apply(rule_tac x=v in exI) apply(rule_tac x="1 - v" in exI) apply simp

   apply(rule_tac x=u in exI) apply simp apply(rule_tac x="\<lambda>x. v" in exI) by simp qed

 lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *\<^sub>R (b - a) | u.  0 \<le> u \<and> u \<le> 1}"

   unfolding convex_hull_2 unfolding Collect_def 

 proof(rule ext) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto

   fix x show "(\<exists>v u. x = v *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> v \<and> 0 \<le> u \<and> v + u = 1) = (\<exists>u. x = a + u *\<^sub>R (b - a) \<and> 0 \<le> u \<and> u \<le> 1)"

     unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed

 lemma convex_hull_3:

   "convex hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \<le> u \<and> 0 \<le> v \<and> 0 \<le> w \<and> u + v + w = 1}"

 proof-

   have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto

   have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"

          "\<And>x y z ::real^'n. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: ring_simps)

   show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and *

     unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto

     apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp

     apply(rule_tac x="1 - v - w" in exI) apply simp apply(rule_tac x=v in exI) apply simp apply(rule_tac x="\<lambda>x. w" in exI) by simp qed

 lemma convex_hull_3_alt:

   "convex hull {a,b,c} = {a + u *\<^sub>R (b - a) + v *\<^sub>R (c - a) | u v.  0 \<le> u \<and> 0 \<le> v \<and> u + v \<le> 1}"

 proof- have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by auto

   show ?thesis unfolding convex_hull_3 apply (auto simp add: *) apply(rule_tac x=v in exI) apply(rule_tac x=w in exI) apply (simp add: algebra_simps)

     apply(rule_tac x=u in exI) apply(rule_tac x=v in exI) by (simp add: algebra_simps) qed

 subsection {* Relations among closure notions and corresponding hulls. *}

 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 :: "(real ^ _) set" shows "subspace s \<Longrightarrow> affine s"

   unfolding subspace_def affine_def smult_conv_scaleR by auto

 lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"

   unfolding affine_def convex_def by auto

 lemma subspace_imp_convex:

   fixes s :: "(real ^ _) set" shows "subspace s \<Longrightarrow> convex s"

   using subspace_imp_affine affine_imp_convex by auto

 lemma affine_hull_subset_span:

   fixes s :: "(real ^ _) set" shows "(affine hull s) \<subseteq> (span s)"

   unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def

   using subspace_imp_affine  by auto

 lemma convex_hull_subset_span:

   fixes s :: "(real ^ _) set" shows "(convex hull s) \<subseteq> (span s)"

   unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def

   using subspace_imp_convex by auto

 lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"

   unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def

   using affine_imp_convex by auto

 lemma affine_dependent_imp_dependent:

   fixes s :: "(real ^ _) set" shows "affine_dependent s \<Longrightarrow> dependent s"

   unfolding affine_dependent_def dependent_def 

   using affine_hull_subset_span by auto

 lemma dependent_imp_affine_dependent:

   fixes s :: "(real ^ _) set"

   assumes "dependent {x - a| x . x \<in> s}" "a \<notin> s"

   shows "affine_dependent (insert a s)"

 proof-

   from assms(1)[unfolded dependent_explicit smult_conv_scaleR] obtain S u v 

     where obt:"finite S" "S \<subseteq> {x - a |x. x \<in> s}" "v\<in>S" "u v  \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0" by auto

   def t \<equiv> "(\<lambda>x. x + a) ` S"

   have inj:"inj_on (\<lambda>x. x + a) S" unfolding inj_on_def by auto

   have "0\<notin>S" using obt(2) assms(2) unfolding subset_eq by auto

   have fin:"finite t" and  "t\<subseteq>s" unfolding t_def using obt(1,2) by auto 

   hence "finite (insert a t)" and "insert a t \<subseteq> insert a s" by auto 

   moreover have *:"\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x)) = (\<Sum>x\<in>t. Q x)"

     apply(rule setsum_cong2) using `a\<notin>s` `t\<subseteq>s` by auto

   have "(\<Sum>x\<in>insert a t. if x = a then - (\<Sum>x\<in>t. u (x - a)) else u (x - a)) = 0"

     unfolding setsum_clauses(2)[OF fin] using `a\<notin>s` `t\<subseteq>s` apply auto unfolding * by auto

   moreover have "\<exists>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) \<noteq> 0"

     apply(rule_tac x="v + a" in bexI) using obt(3,4) and `0\<notin>S` unfolding t_def by auto

   moreover have *:"\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x) *\<^sub>R x) = (\<Sum>x\<in>t. Q x *\<^sub>R x)"

     apply(rule setsum_cong2) using `a\<notin>s` `t\<subseteq>s` by auto

   have "(\<Sum>x\<in>t. u (x - a)) *\<^sub>R a = (\<Sum>v\<in>t. u (v - a) *\<^sub>R v)" 

     unfolding scaleR_left.setsum unfolding t_def and setsum_reindex[OF inj] and o_def

     using obt(5) by (auto simp add: setsum_addf scaleR_right_distrib)

   hence "(\<Sum>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0"

     unfolding setsum_clauses(2)[OF fin] using `a\<notin>s` `t\<subseteq>s` by (auto simp add: *  vector_smult_lneg) 

   ultimately show ?thesis unfolding affine_dependent_explicit

     apply(rule_tac x="insert a t" in exI) by auto 

 qed

 lemma convex_cone:

   "convex s \<and> cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. (x + y) \<in> s) \<and> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)" (is "?lhs = ?rhs")

 proof-

   { fix x y assume "x\<in>s" "y\<in>s" and ?lhs

     hence "2 *\<^sub>R x \<in>s" "2 *\<^sub>R y \<in> s" unfolding cone_def by auto

     hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1]

       apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE)

       apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto  }

   thus ?thesis unfolding convex_def cone_def by blast