src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.

(*  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 Convex
begin


(* ------------------------------------------------------------------------- *)
(* To be moved elsewhere                                                     *)
(* ------------------------------------------------------------------------- *)

lemma basis_0[simp]:"(basis i::'a::euclidean_space) = 0 \<longleftrightarrow> i\<ge>DIM('a)"
  using norm_basis[of i, where 'a='a] unfolding norm_eq_zero[where 'a='a,THEN sym] by auto

lemma scaleR_2:
  fixes x :: "'a::real_vector"
  shows "scaleR 2 x = x + x"
unfolding one_add_one_is_two [symmetric] scaleR_left_distrib by simp

declare euclidean_simps[simp]

lemma vector_choose_size: "0 <= c ==> \<exists>(x::'a::euclidean_space). norm x = c"
  apply (rule exI[where x="c *\<^sub>R basis 0 ::'a"]) using DIM_positive[where 'a='a] 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 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::'a::ordered_euclidean_space)) ` {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 :: "'a::euclidean_space"
  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 *]
    by(auto simp add:norm_minus_commute) qed

lemma norm_minus_eqI:"x = - 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 norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y"
  unfolding norm_eq_sqrt_inner by simp

lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
  unfolding norm_eq_sqrt_inner by simp



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
      hence "u x + (1 - u x) = 1 \<Longrightarrow> u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\<Sum>xa\<in>s - {x}. u xa *\<^sub>R xa) /\<^sub>R (1 - u x)) \<in> V"
        apply-apply(rule as(3)[rule_format]) 
        unfolding  RealVector.scaleR_right.setsum using x(1) as(6) by auto
      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 `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] RealVector.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 :: "'a::euclidean_space"
  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
  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 :: "'a::euclidean_space"
  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 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 :: "'a::euclidean_space"
  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 {* 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 {* Balls, being convex, are connected. *}

lemma convex_box: fixes a::"'a::euclidean_space"
  assumes "\<And>i. i<DIM('a) \<Longrightarrow> convex {x. P i x}"
  shows "convex {x. \<forall>i<DIM('a). P i (x$$i)}"
  using assms unfolding convex_def by(auto simp add:euclidean_simps)

lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\<forall>i<DIM('a). 0 \<le> x$$i)}"
  by (rule convex_box) (simp add: atLeast_def[symmetric] convex_real_interval)

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_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 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 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
  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 ::_::euclidean_space. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: field_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 :: "(_::euclidean_space) set" shows "subspace s \<Longrightarrow> affine s"
  unfolding subspace_def affine_def by auto

lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
  unfolding affine_def convex_def by auto

lemma subspace_imp_convex:
  fixes s :: "(_::euclidean_space) set" shows "subspace s \<Longrightarrow> convex s"
  using subspace_imp_affine affine_imp_convex by auto

lemma affine_hull_subset_span:
  fixes s :: "(_::euclidean_space) set" shows "(affine hull s) \<subseteq> (span s)"
by (metis hull_minimal mem_def span_inc subspace_imp_affine subspace_span)

lemma convex_hull_subset_span:
  fixes s :: "(_::euclidean_space) set" shows "(convex hull s) \<subseteq> (span s)"
by (metis hull_minimal mem_def span_inc subspace_imp_convex subspace_span)

lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset mem_def)


lemma affine_dependent_imp_dependent:
  fixes s :: "(_::euclidean_space) 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 :: "(_::euclidean_space) 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] 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: *)
  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
qed

lemma affine_dependent_biggerset: fixes s::"('a::euclidean_space) set"
  assumes "finite s" "card s \<ge> DIM('a) + 2"
  shows "affine_dependent s"
proof-
  have "s\<noteq>{}" using assms by auto then obtain a where "a\<in>s" by auto
  have *:"{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})" by auto
  have "card {x - a |x. x \<in> s - {a}} = card (s - {a})" unfolding * 
    apply(rule card_image) unfolding inj_on_def by auto
  also have "\<dots> > DIM('a)" using assms(2)
    unfolding card_Diff_singleton[OF assms(1) `a\<in>s`] by auto
  finally show ?thesis apply(subst insert_Diff[OF `a\<in>s`, THEN sym])
    apply(rule dependent_imp_affine_dependent)
    apply(rule dependent_biggerset) by auto qed

lemma affine_dependent_biggerset_general:
  assumes "finite (s::('a::euclidean_space) set)" "card s \<ge> dim s + 2"
  shows "affine_dependent s"
proof-
  from assms(2) have "s \<noteq> {}" by auto
  then obtain a where "a\<in>s" by auto
  have *:"{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})" by auto
  have **:"card {x - a |x. x \<in> s - {a}} = card (s - {a})" unfolding * 
    apply(rule card_image) unfolding inj_on_def by auto
  have "dim {x - a |x. x \<in> s - {a}} \<le> dim s"
    apply(rule subset_le_dim) unfolding subset_eq
    using `a\<in>s` by (auto simp add:span_superset span_sub)
  also have "\<dots> < dim s + 1" by auto
  also have "\<dots> \<le> card (s - {a})" using assms
    using card_Diff_singleton[OF assms(1) `a\<in>s`] by auto
  finally show ?thesis apply(subst insert_Diff[OF `a\<in>s`, THEN sym])
    apply(rule dependent_imp_affine_dependent) apply(rule dependent_biggerset_general) unfolding ** by auto qed

subsection {* Caratheodory's theorem. *}

lemma convex_hull_caratheodory: fixes p::"('a::euclidean_space) set"
  shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<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}"
  unfolding convex_hull_explicit expand_set_eq mem_Collect_eq
proof(rule,rule)
  fix y let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<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) = y"
  assume "\<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) = y"
  then obtain N where "?P N" by auto
  hence "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n" apply(rule_tac ex_least_nat_le) by auto
  then obtain n where "?P n" and smallest:"\<forall>k<n. \<not> ?P k" by blast
  then obtain s u where obt:"finite s" "card s = n" "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

  have "card s \<le> DIM('a) + 1" proof(rule ccontr, simp only: not_le)
    assume "DIM('a) + 1 < card s"
    hence "affine_dependent s" using affine_dependent_biggerset[OF obt(1)] by auto
    then obtain w v where wv:"setsum w s = 0" "v\<in>s" "w v \<noteq> 0" "(\<Sum>v\<in>s. w v *\<^sub>R v) = 0"
      using affine_dependent_explicit_finite[OF obt(1)] by auto
    def i \<equiv> "(\<lambda>v. (u v) / (- w v)) ` {v\<in>s. w v < 0}"  def t \<equiv> "Min i"
    have "\<exists>x\<in>s. w x < 0" proof(rule ccontr, simp add: not_less)
      assume as:"\<forall>x\<in>s. 0 \<le> w x"
      hence "setsum w (s - {v}) \<ge> 0" apply(rule_tac setsum_nonneg) by auto
      hence "setsum w s > 0" unfolding setsum_diff1'[OF obt(1) `v\<in>s`]
        using as[THEN bspec[where x=v]] and `v\<in>s` using `w v \<noteq> 0` by auto
      thus False using wv(1) by auto
    qed hence "i\<noteq>{}" unfolding i_def by auto

    hence "t \<ge> 0" using Min_ge_iff[of i 0 ] and obt(1) unfolding t_def i_def
      using obt(4)[unfolded le_less] apply auto unfolding divide_le_0_iff by auto 
    have t:"\<forall>v\<in>s. u v + t * w v \<ge> 0" proof
      fix v assume "v\<in>s" hence v:"0\<le>u v" using obt(4)[THEN bspec[where x=v]] by auto
      show"0 \<le> u v + t * w v" proof(cases "w v < 0")
        case False thus ?thesis apply(rule_tac add_nonneg_nonneg) 
          using v apply simp apply(rule mult_nonneg_nonneg) using `t\<ge>0` by auto next
        case True hence "t \<le> u v / (- w v)" using `v\<in>s`
          unfolding t_def i_def apply(rule_tac Min_le) using obt(1) by auto 
        thus ?thesis unfolding real_0_le_add_iff
          using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[THEN sym]]] by auto
      qed qed

    obtain a where "a\<in>s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
      using Min_in[OF _ `i\<noteq>{}`] and obt(1) unfolding i_def t_def by auto
    hence a:"a\<in>s" "u a + t * w a = 0" by auto
    have *:"\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
      unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto 
    have "(\<Sum>v\<in>s. u v + t * w v) = 1"
      unfolding setsum_addf wv(1) setsum_right_distrib[THEN sym] obt(5) by auto
    moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y" 
      unfolding setsum_addf obt(6) scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] wv(4)
      using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp
    ultimately have "?P (n - 1)" apply(rule_tac x="(s - {a})" in exI)
      apply(rule_tac x="\<lambda>v. u v + t * w v" in exI) using obt(1-3) and t and a
      by (auto simp add: * scaleR_left_distrib)
    thus False using smallest[THEN spec[where x="n - 1"]] by auto qed
  thus "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1
    \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y" using obt by auto
qed auto

lemma caratheodory:
 "convex hull p = {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
      card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
  unfolding expand_set_eq apply(rule, rule) unfolding mem_Collect_eq proof-
  fix x assume "x \<in> convex hull p"
  then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
     "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"unfolding convex_hull_caratheodory by auto
  thus "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
    apply(rule_tac x=s in exI) using hull_subset[of s convex]
  using convex_convex_hull[unfolded convex_explicit, of s, THEN spec[where x=s], THEN spec[where x=u]] by auto
next
  fix x assume "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s"
  then obtain s where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1" "x \<in> convex hull s" by auto
  thus "x \<in> convex hull p" using hull_mono[OF `s\<subseteq>p`] by auto
qed

subsection {* Openness and compactness are preserved by convex hull operation. *}

lemma open_convex_hull[intro]:
  fixes s :: "'a::real_normed_vector set"
  assumes "open s"
  shows "open(convex hull s)"
  unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10)
proof(rule, rule) fix a
  assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a"
  then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto

  from assms[unfolded open_contains_cball] obtain b where b:"\<forall>x\<in>s. 0 < b x \<and> cball x (b x) \<subseteq> s"
    using bchoice[of s "\<lambda>x e. e>0 \<and> cball x e \<subseteq> s"] by auto
  have "b ` t\<noteq>{}" unfolding i_def using obt by auto  def i \<equiv> "b ` t"

  show "\<exists>e>0. cball a e \<subseteq> {y. \<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y}"
    apply(rule_tac x="Min i" in exI) unfolding subset_eq apply rule defer apply rule unfolding mem_Collect_eq
  proof-
    show "0 < Min i" unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] `b \` t\<noteq>{}`]
      using b apply simp apply rule apply(erule_tac x=x in ballE) using `t\<subseteq>s` by auto
  next  fix y assume "y \<in> cball a (Min i)"
    hence y:"norm (a - y) \<le> Min i" unfolding dist_norm[THEN sym] by auto
    { fix x assume "x\<in>t"
      hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto
      hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_norm by auto
      moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto
      ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast }
    moreover
    have *:"inj_on (\<lambda>v. v + (y - a)) t" unfolding inj_on_def by auto
    have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a))) = 1"
      unfolding setsum_reindex[OF *] o_def using obt(4) by auto
    moreover have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a)) *\<^sub>R v) = y"
      unfolding setsum_reindex[OF *] o_def using obt(4,5)
      by (simp add: setsum_addf setsum_subtractf scaleR_left.setsum[THEN sym] scaleR_right_distrib)
    ultimately show "\<exists>sa u. finite sa \<and> (\<forall>x\<in>sa. x \<in> s) \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y"
      apply(rule_tac x="(\<lambda>v. v + (y - a)) ` t" in exI) apply(rule_tac x="\<lambda>v. u (v - (y - a))" in exI)
      using obt(1, 3) by auto
  qed
qed

lemma compact_convex_combinations:
  fixes s t :: "'a::real_normed_vector set"
  assumes "compact s" "compact t"
  shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t}"
proof-
  let ?X = "{0..1} \<times> s \<times> t"
  let ?h = "(\<lambda>z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))"
  have *:"{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t} = ?h ` ?X"
    apply(rule set_ext) unfolding image_iff mem_Collect_eq
    apply rule apply auto
    apply (rule_tac x=u in rev_bexI, simp)
    apply (erule rev_bexI, erule rev_bexI, simp)
    by auto
  have "continuous_on ({0..1} \<times> s \<times> t)
     (\<lambda>z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))"
    unfolding continuous_on by (rule ballI) (intro tendsto_intros)
  thus ?thesis unfolding *
    apply (rule compact_continuous_image)
    apply (intro compact_Times compact_interval assms)
    done
qed

lemma compact_convex_hull: fixes s::"('a::euclidean_space) set"
  assumes "compact s"  shows "compact(convex hull s)"
proof(cases "s={}")
  case True thus ?thesis using compact_empty by simp
next
  case False then obtain w where "w\<in>s" by auto
  show ?thesis unfolding caratheodory[of s]
  proof(induct ("DIM('a) + 1"))
    have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}" 
      using compact_empty by auto
    case 0 thus ?case unfolding * by simp
  next
    case (Suc n)
    show ?case proof(cases "n=0")
      case True have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} = s"
        unfolding expand_set_eq and mem_Collect_eq proof(rule, rule)
        fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
        then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto
        show "x\<in>s" proof(cases "card t = 0")
          case True thus ?thesis using t(4) unfolding card_0_eq[OF t(1)] by simp
        next
          case False hence "card t = Suc 0" using t(3) `n=0` by auto
          then obtain a where "t = {a}" unfolding card_Suc_eq by auto
          thus ?thesis using t(2,4) by simp
        qed
      next
        fix x assume "x\<in>s"
        thus "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
          apply(rule_tac x="{x}" in exI) unfolding convex_hull_singleton by auto 
      qed thus ?thesis using assms by simp
    next
      case False have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} =
        { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 
        0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> {x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> x \<in> convex hull t}}"
        unfolding expand_set_eq and mem_Collect_eq proof(rule,rule)
        fix x assume "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
          0 \<le> c \<and> c \<le> 1 \<and> u \<in> s \<and> (\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> v \<in> convex hull t)"
        then obtain u v c t where obt:"x = (1 - c) *\<^sub>R u + c *\<^sub>R v"
          "0 \<le> c \<and> c \<le> 1" "u \<in> s" "finite t" "t \<subseteq> s" "card t \<le> n"  "v \<in> convex hull t" by auto
        moreover have "(1 - c) *\<^sub>R u + c *\<^sub>R v \<in> convex hull insert u t"
          apply(rule mem_convex) using obt(2) and convex_convex_hull and hull_subset[of "insert u t" convex]
          using obt(7) and hull_mono[of t "insert u t"] by auto
        ultimately show "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
          apply(rule_tac x="insert u t" in exI) by (auto simp add: card_insert_if)
      next
        fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
        then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto
        let ?P = "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
          0 \<le> c \<and> c \<le> 1 \<and> u \<in> s \<and> (\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> v \<in> convex hull t)"
        show ?P proof(cases "card t = Suc n")
          case False hence "card t \<le> n" using t(3) by auto
          thus ?P apply(rule_tac x=w in exI, rule_tac x=x in exI, rule_tac x=1 in exI) using `w\<in>s` and t
            by(auto intro!: exI[where x=t])
        next
          case True then obtain a u where au:"t = insert a u" "a\<notin>u" apply(drule_tac card_eq_SucD) by auto
          show ?P proof(cases "u={}")
            case True hence "x=a" using t(4)[unfolded au] by auto
            show ?P unfolding `x=a` apply(rule_tac x=a in exI, rule_tac x=a in exI, rule_tac x=1 in exI)
              using t and `n\<noteq>0` unfolding au by(auto intro!: exI[where x="{a}"])
          next
            case False obtain ux vx b where obt:"ux\<ge>0" "vx\<ge>0" "ux + vx = 1" "b \<in> convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b"
              using t(4)[unfolded au convex_hull_insert[OF False]] by auto
            have *:"1 - vx = ux" using obt(3) by auto
            show ?P apply(rule_tac x=a in exI, rule_tac x=b in exI, rule_tac x=vx in exI)
              using obt and t(1-3) unfolding au and * using card_insert_disjoint[OF _ au(2)]
              by(auto intro!: exI[where x=u])
          qed
        qed
      qed
      thus ?thesis using compact_convex_combinations[OF assms Suc] by simp 
    qed
  qed
qed

lemma finite_imp_compact_convex_hull:
  fixes s :: "('a::euclidean_space) set"
  shows "finite s \<Longrightarrow> compact(convex hull s)"
by (metis compact_convex_hull finite_imp_compact)

subsection {* Extremal points of a simplex are some vertices. *}

lemma dist_increases_online:
  fixes a b d :: "'a::real_inner"
  assumes "d \<noteq> 0"
  shows "dist a (b + d) > dist a b \<or> dist a (b - d) > dist a b"
proof(cases "inner a d - inner b d > 0")
  case True hence "0 < inner d d + (inner a d * 2 - inner b d * 2)" 
    apply(rule_tac add_pos_pos) using assms by auto
  thus ?thesis apply(rule_tac disjI2) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
    by (simp add: algebra_simps inner_commute)
next
  case False hence "0 < inner d d + (inner b d * 2 - inner a d * 2)" 
    apply(rule_tac add_pos_nonneg) using assms by auto
  thus ?thesis apply(rule_tac disjI1) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
    by (simp add: algebra_simps inner_commute)
qed

lemma norm_increases_online:
  fixes d :: "'a::real_inner"
  shows "d \<noteq> 0 \<Longrightarrow> norm(a + d) > norm a \<or> norm(a - d) > norm a"
  using dist_increases_online[of d a 0] unfolding dist_norm by auto

lemma simplex_furthest_lt:
  fixes s::"'a::real_inner set" assumes "finite s"
  shows "\<forall>x \<in> (convex hull s).  x \<notin> s \<longrightarrow> (\<exists>y\<in>(convex hull s). norm(x - a) < norm(y - a))"
proof(induct_tac rule: finite_induct[of s])
  fix x s assume as:"finite s" "x\<notin>s" "\<forall>x\<in>convex hull s. x \<notin> s \<longrightarrow> (\<exists>y\<in>convex hull s. norm (x - a) < norm (y - a))"
  show "\<forall>xa\<in>convex hull insert x s. xa \<notin> insert x s \<longrightarrow> (\<exists>y\<in>convex hull insert x s. norm (xa - a) < norm (y - a))"
  proof(rule,rule,cases "s = {}")
    case False fix y assume y:"y \<in> convex hull insert x s" "y \<notin> insert x s"
    obtain u v b where obt:"u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "y = u *\<^sub>R x + v *\<^sub>R b"
      using y(1)[unfolded convex_hull_insert[OF False]] by auto
    show "\<exists>z\<in>convex hull insert x s. norm (y - a) < norm (z - a)"
    proof(cases "y\<in>convex hull s")
      case True then obtain z where "z\<in>convex hull s" "norm (y - a) < norm (z - a)"
        using as(3)[THEN bspec[where x=y]] and y(2) by auto
      thus ?thesis apply(rule_tac x=z in bexI) unfolding convex_hull_insert[OF False] by auto
    next
      case False show ?thesis  using obt(3) proof(cases "u=0", case_tac[!] "v=0")
        assume "u=0" "v\<noteq>0" hence "y = b" using obt by auto
        thus ?thesis using False and obt(4) by auto
      next
        assume "u\<noteq>0" "v=0" hence "y = x" using obt by auto
        thus ?thesis using y(2) by auto
      next
        assume "u\<noteq>0" "v\<noteq>0"
        then obtain w where w:"w>0" "w<u" "w<v" using real_lbound_gt_zero[of u v] and obt(1,2) by auto
        have "x\<noteq>b" proof(rule ccontr) 
          assume "\<not> x\<noteq>b" hence "y=b" unfolding obt(5)
            using obt(3) by(auto simp add: scaleR_left_distrib[THEN sym])
          thus False using obt(4) and False by simp qed
        hence *:"w *\<^sub>R (x - b) \<noteq> 0" using w(1) by auto
        show ?thesis using dist_increases_online[OF *, of a y]
        proof(erule_tac disjE)
          assume "dist a y < dist a (y + w *\<^sub>R (x - b))"
          hence "norm (y - a) < norm ((u + w) *\<^sub>R x + (v - w) *\<^sub>R b - a)"
            unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps)
          moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \<in> convex hull insert x s"
            unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
            apply(rule_tac x="u + w" in exI) apply rule defer 
            apply(rule_tac x="v - w" in exI) using `u\<ge>0` and w and obt(3,4) by auto
          ultimately show ?thesis by auto
        next
          assume "dist a y < dist a (y - w *\<^sub>R (x - b))"
          hence "norm (y - a) < norm ((u - w) *\<^sub>R x + (v + w) *\<^sub>R b - a)"
            unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps)
          moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \<in> convex hull insert x s"
            unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
            apply(rule_tac x="u - w" in exI) apply rule defer 
            apply(rule_tac x="v + w" in exI) using `u\<ge>0` and w and obt(3,4) by auto
          ultimately show ?thesis by auto
        qed
      qed auto
    qed
  qed auto
qed (auto simp add: assms)

lemma simplex_furthest_le:
  fixes s :: "('a::euclidean_space) set"
  assumes "finite s" "s \<noteq> {}"
  shows "\<exists>y\<in>s. \<forall>x\<in>(convex hull s). norm(x - a) \<le> norm(y - a)"
proof-
  have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
  then obtain x where x:"x\<in>convex hull s" "\<forall>y\<in>convex hull s. norm (y - a) \<le> norm (x - a)"
    using distance_attains_sup[OF finite_imp_compact_convex_hull[OF assms(1)], of a]
    unfolding dist_commute[of a] unfolding dist_norm by auto
  thus ?thesis proof(cases "x\<in>s")
    case False then obtain y where "y\<in>convex hull s" "norm (x - a) < norm (y - a)"
      using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1) by auto
    thus ?thesis using x(2)[THEN bspec[where x=y]] by auto
  qed auto
qed

lemma simplex_furthest_le_exists:
  fixes s :: "('a::euclidean_space) set"
  shows "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x - a) \<le> norm(y - a))"
  using simplex_furthest_le[of s] by (cases "s={}")auto

lemma simplex_extremal_le:
  fixes s :: "('a::euclidean_space) set"
  assumes "finite s" "s \<noteq> {}"
  shows "\<exists>u\<in>s. \<exists>v\<in>s. \<forall>x\<in>convex hull s. \<forall>y \<in> convex hull s. norm(x - y) \<le> norm(u - v)"
proof-
  have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
  then obtain u v where obt:"u\<in>convex hull s" "v\<in>convex hull s"
    "\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull s. norm (x - y) \<le> norm (u - v)"
    using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]] by auto
  thus ?thesis proof(cases "u\<notin>s \<or> v\<notin>s", erule_tac disjE)
    assume "u\<notin>s" then obtain y where "y\<in>convex hull s" "norm (u - v) < norm (y - v)"
      using simplex_furthest_lt[OF assms(1), THEN bspec[where x=u]] and obt(1) by auto
    thus ?thesis using obt(3)[THEN bspec[where x=y], THEN bspec[where x=v]] and obt(2) by auto
  next
    assume "v\<notin>s" then obtain y where "y\<in>convex hull s" "norm (v - u) < norm (y - u)"
      using simplex_furthest_lt[OF assms(1), THEN bspec[where x=v]] and obt(2) by auto
    thus ?thesis using obt(3)[THEN bspec[where x=u], THEN bspec[where x=y]] and obt(1)
      by (auto simp add: norm_minus_commute)
  qed auto
qed 

lemma simplex_extremal_le_exists:
  fixes s :: "('a::euclidean_space) set"
  shows "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s
  \<Longrightarrow> (\<exists>u\<in>s. \<exists>v\<in>s. norm(x - y) \<le> norm(u - v))"
  using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto

subsection {* Closest point of a convex set is unique, with a continuous projection. *}

definition
  closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a" where
 "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"

lemma closest_point_exists:
  assumes "closed s" "s \<noteq> {}"
  shows  "closest_point s a \<in> s" "\<forall>y\<in>s. dist a (closest_point s a) \<le> dist a y"
  unfolding closest_point_def apply(rule_tac[!] someI2_ex) 
  using distance_attains_inf[OF assms(1,2), of a] by auto

lemma closest_point_in_set:
  "closed s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> (closest_point s a) \<in> s"
  by(meson closest_point_exists)

lemma closest_point_le:
  "closed s \<Longrightarrow> x \<in> s \<Longrightarrow> dist a (closest_point s a) \<le> dist a x"
  using closest_point_exists[of s] by auto

lemma closest_point_self:
  assumes "x \<in> s"  shows "closest_point s x = x"
  unfolding closest_point_def apply(rule some1_equality, rule ex1I[of _ x])