(*  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]

(*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_le_def Cart_lambda_beta basis_component vector_uminus_component

lemma norm_not_0:"(x::real^'n)\<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 image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n)) ` {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 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) = - 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 real_eq_of_nat 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)"

unfolding affine_def by(metis eq_diff_eq')

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"

by (metis affine_affine_hull hull_same mem_def)

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 = card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and

        as:"Suc n = 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 "\<lambda>x. x = a"]

    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_real_interval:

  fixes a b :: "real"

  shows "convex {a..}" and "convex {..b}"

  and "convex {a<..}" and "convex {..<b}"

  and "convex {a..b}" and "convex {a<..b}"

  and "convex {a..<b}" and "convex {a<..<b}"

proof -

  have "{a..} = {x. a \<le> inner 1 x}" by auto

  thus 1: "convex {a..}" by (simp only: convex_halfspace_ge)

  have "{..b} = {x. inner 1 x \<le> b}" by auto

  thus 2: "convex {..b}" by (simp only: convex_halfspace_le)

  have "{a<..} = {x. a < inner 1 x}" by auto

  thus 3: "convex {a<..}" by (simp only: convex_halfspace_gt)

  have "{..<b} = {x. inner 1 x < b}" by auto

  thus 4: "convex {..<b}" by (simp only: convex_halfspace_lt)

  have "{a..b} = {a..} \<inter> {..b}" by auto

  thus "convex {a..b}" by (simp only: convex_Int 1 2)

  have "{a<..b} = {a<..} \<inter> {..b}" by auto

  thus "convex {a<..b}" by (simp only: convex_Int 3 2)

  have "{a..<b} = {a..} \<inter> {..<b}" by auto

  thus "convex {a..<b}" by (simp only: convex_Int 1 4)

  have "{a<..<b} = {a<..} \<inter> {..<b}" by auto

  thus "convex {a<..<b}" by (simp only: convex_Int 3 4)

qed

lemma convex_box:

  assumes "\<And>i. convex {x. P i x}"

  shows "convex {x. \<forall>i. P i (x$i)}"

using assms unfolding convex_def by auto

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

by (rule convex_box, simp add: atLeast_def [symmetric] convex_real_interval)

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" 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 t rule:finite_induct)

    prefer 2 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" 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] 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[intro]: "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[intro]:

  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: field_simps)  }

  thus ?thesis unfolding convex_on_def by auto 

qed

lemma convex_cmul[intro]:

  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: field_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[intro]:

  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)

  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"

by (metis convex_convex_hull hull_same mem_def)

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"

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

      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" unfolding obt1(3)[THEN sym] and not_le using obt1(2) by auto

    have u2:"u2 \<le> 1" 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 Collect_mem_eq

    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