Theory Starlike

theory Starlike
imports Convex_Euclidean_Space
(* Title:      HOL/Analysis/Starlike.thy
   Author:     L C Paulson, University of Cambridge
   Author:     Robert Himmelmann, TU Muenchen
   Author:     Bogdan Grechuk, University of Edinburgh
   Author:     Armin Heller, TU Muenchen
   Author:     Johannes Hoelzl, TU Muenchen
*)

section ‹Line segments, Starlike Sets, etc.›

theory Starlike
  imports Convex_Euclidean_Space

begin

definition midpoint :: "'a::real_vector ⇒ 'a ⇒ 'a"
  where "midpoint a b = (inverse (2::real)) *R (a + b)"

definition closed_segment :: "'a::real_vector ⇒ 'a ⇒ 'a set"
  where "closed_segment a b = {(1 - u) *R a + u *R b | u::real. 0 ≤ u ∧ u ≤ 1}"

definition open_segment :: "'a::real_vector ⇒ 'a ⇒ 'a set" where
  "open_segment a b ≡ closed_segment a b - {a,b}"

lemmas segment = open_segment_def closed_segment_def

lemma in_segment:
    "x ∈ closed_segment a b ⟷ (∃u. 0 ≤ u ∧ u ≤ 1 ∧ x = (1 - u) *R a + u *R b)"
    "x ∈ open_segment a b ⟷ a ≠ b ∧ (∃u. 0 < u ∧ u < 1 ∧ x = (1 - u) *R a + u *R b)"
  using less_eq_real_def by (auto simp: segment algebra_simps)

lemma closed_segment_linear_image:
    "linear f ⟹ closed_segment (f a) (f b) = f ` (closed_segment a b)"
  by (force simp add: in_segment linear_add_cmul)

lemma open_segment_linear_image:
    "⟦linear f; inj f⟧ ⟹ open_segment (f a) (f b) = f ` (open_segment a b)"
  by (force simp: open_segment_def closed_segment_linear_image inj_on_def)

lemma closed_segment_translation:
    "closed_segment (c + a) (c + b) = image (λx. c + x) (closed_segment a b)"
apply safe
apply (rule_tac x="x-c" in image_eqI)
apply (auto simp: in_segment algebra_simps)
done

lemma open_segment_translation:
    "open_segment (c + a) (c + b) = image (λx. c + x) (open_segment a b)"
by (simp add: open_segment_def closed_segment_translation translation_diff)

lemma closed_segment_of_real:
    "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y"
  apply (auto simp: image_iff in_segment scaleR_conv_of_real)
    apply (rule_tac x="(1-u)*x + u*y" in bexI)
  apply (auto simp: in_segment)
  done

lemma open_segment_of_real:
    "open_segment (of_real x) (of_real y) = of_real ` open_segment x y"
  apply (auto simp: image_iff in_segment scaleR_conv_of_real)
    apply (rule_tac x="(1-u)*x + u*y" in bexI)
  apply (auto simp: in_segment)
  done

lemma closed_segment_Reals:
    "⟦x ∈ Reals; y ∈ Reals⟧ ⟹ closed_segment x y = of_real ` closed_segment (Re x) (Re y)"
  by (metis closed_segment_of_real of_real_Re)

lemma open_segment_Reals:
    "⟦x ∈ Reals; y ∈ Reals⟧ ⟹ open_segment x y = of_real ` open_segment (Re x) (Re y)"
  by (metis open_segment_of_real of_real_Re)

lemma open_segment_PairD:
    "(x, x') ∈ open_segment (a, a') (b, b')
     ⟹ (x ∈ open_segment a b ∨ a = b) ∧ (x' ∈ open_segment a' b' ∨ a' = b')"
  by (auto simp: in_segment)

lemma closed_segment_PairD:
  "(x, x') ∈ closed_segment (a, a') (b, b') ⟹ x ∈ closed_segment a b ∧ x' ∈ closed_segment a' b'"
  by (auto simp: closed_segment_def)

lemma closed_segment_translation_eq [simp]:
    "d + x ∈ closed_segment (d + a) (d + b) ⟷ x ∈ closed_segment a b"
proof -
  have *: "⋀d x a b. x ∈ closed_segment a b ⟹ d + x ∈ closed_segment (d + a) (d + b)"
    apply (simp add: closed_segment_def)
    apply (erule ex_forward)
    apply (simp add: algebra_simps)
    done
  show ?thesis
  using * [where d = "-d"] *
  by (fastforce simp add:)
qed

lemma open_segment_translation_eq [simp]:
    "d + x ∈ open_segment (d + a) (d + b) ⟷ x ∈ open_segment a b"
  by (simp add: open_segment_def)

lemma of_real_closed_segment [simp]:
  "of_real x ∈ closed_segment (of_real a) (of_real b) ⟷ x ∈ closed_segment a b"
  apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward)
  using of_real_eq_iff by fastforce

lemma of_real_open_segment [simp]:
  "of_real x ∈ open_segment (of_real a) (of_real b) ⟷ x ∈ open_segment a b"
  apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
  using of_real_eq_iff by fastforce

lemma midpoint_idem [simp]: "midpoint x x = x"
  unfolding midpoint_def
  unfolding scaleR_right_distrib
  unfolding scaleR_left_distrib[symmetric]
  by auto

lemma midpoint_sym: "midpoint a b = midpoint b a"
  unfolding midpoint_def by (auto simp add: scaleR_right_distrib)

lemma midpoint_eq_iff: "midpoint a b = c ⟷ a + b = c + c"
proof -
  have "midpoint a b = c ⟷ scaleR 2 (midpoint a b) = scaleR 2 c"
    by simp
  then show ?thesis
    unfolding midpoint_def scaleR_2 [symmetric] by simp
qed

lemma
  fixes a::real
  assumes "a ≤ b" shows ge_midpoint_1: "a ≤ midpoint a b"
                    and le_midpoint_1: "midpoint a b ≤ b"
  by (simp_all add: midpoint_def assms)

lemma dist_midpoint:
  fixes a b :: "'a::real_normed_vector" shows
  "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
  "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
  "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
  "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
proof -
  have *: "⋀x y::'a. 2 *R x = - y ⟹ norm x = (norm y) / 2"
    unfolding equation_minus_iff by auto
  have **: "⋀x y::'a. 2 *R x =   y ⟹ norm x = (norm y) / 2"
    by auto
  note scaleR_right_distrib [simp]
  show ?t1
    unfolding midpoint_def dist_norm
    apply (rule **)
    apply (simp add: scaleR_right_diff_distrib)
    apply (simp add: scaleR_2)
    done
  show ?t2
    unfolding midpoint_def dist_norm
    apply (rule *)
    apply (simp add: scaleR_right_diff_distrib)
    apply (simp add: scaleR_2)
    done
  show ?t3
    unfolding midpoint_def dist_norm
    apply (rule *)
    apply (simp add: scaleR_right_diff_distrib)
    apply (simp add: scaleR_2)
    done
  show ?t4
    unfolding midpoint_def dist_norm
    apply (rule **)
    apply (simp add: scaleR_right_diff_distrib)
    apply (simp add: scaleR_2)
    done
qed

lemma midpoint_eq_endpoint [simp]:
  "midpoint a b = a ⟷ a = b"
  "midpoint a b = b ⟷ a = b"
  unfolding midpoint_eq_iff by auto

lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
  using midpoint_eq_iff by metis

lemma midpoint_linear_image:
   "linear f ⟹ midpoint(f a)(f b) = f(midpoint a b)"
by (simp add: linear_iff midpoint_def)

subsection‹Starlike sets›

definition "starlike S ⟷ (∃a∈S. ∀x∈S. closed_segment a x ⊆ S)"

lemma starlike_UNIV [simp]: "starlike UNIV"
  by (simp add: starlike_def)

lemma convex_contains_segment:
  "convex S ⟷ (∀a∈S. ∀b∈S. closed_segment a b ⊆ S)"
  unfolding convex_alt closed_segment_def by auto

lemma closed_segment_subset: "⟦x ∈ S; y ∈ S; convex S⟧ ⟹ closed_segment x y ⊆ S"
  by (simp add: convex_contains_segment)

lemma closed_segment_subset_convex_hull:
    "⟦x ∈ convex hull S; y ∈ convex hull S⟧ ⟹ closed_segment x y ⊆ convex hull S"
  using convex_contains_segment by blast

lemma convex_imp_starlike:
  "convex S ⟹ S ≠ {} ⟹ starlike S"
  unfolding convex_contains_segment starlike_def by auto

lemma segment_convex_hull:
  "closed_segment a b = convex hull {a,b}"
proof -
  have *: "⋀x. {x} ≠ {}" by auto
  show ?thesis
    unfolding segment convex_hull_insert[OF *] convex_hull_singleton
    by (safe; rule_tac x="1 - u" in exI; force)
qed

lemma open_closed_segment: "u ∈ open_segment w z ⟹ u ∈ closed_segment w z"
  by (auto simp add: closed_segment_def open_segment_def)

lemma segment_open_subset_closed:
   "open_segment a b ⊆ closed_segment a b"
  by (auto simp: closed_segment_def open_segment_def)

lemma bounded_closed_segment:
    fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)"
  by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded)

lemma bounded_open_segment:
    fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)"
  by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed])

lemmas bounded_segment = bounded_closed_segment open_closed_segment

lemma ends_in_segment [iff]: "a ∈ closed_segment a b" "b ∈ closed_segment a b"
  unfolding segment_convex_hull
  by (auto intro!: hull_subset[unfolded subset_eq, rule_format])

lemma eventually_closed_segment:
  fixes x0::"'a::real_normed_vector"
  assumes "open X0" "x0 ∈ X0"
  shows "∀F x in at x0 within U. closed_segment x0 x ⊆ X0"
proof -
  from openE[OF assms]
  obtain e where e: "0 < e" "ball x0 e ⊆ X0" .
  then have "∀F x in at x0 within U. x ∈ ball x0 e"
    by (auto simp: dist_commute eventually_at)
  then show ?thesis
  proof eventually_elim
    case (elim x)
    have "x0 ∈ ball x0 e" using ‹e > 0› by simp
    from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim]
    have "closed_segment x0 x ⊆ ball x0 e" .
    also note ‹… ⊆ X0›
    finally show ?case .
  qed
qed

lemma segment_furthest_le:
  fixes a b x y :: "'a::euclidean_space"
  assumes "x ∈ closed_segment a b"
  shows "norm (y - x) ≤ norm (y - a) ∨  norm (y - x) ≤ norm (y - b)"
proof -
  obtain z where "z ∈ {a, b}" "norm (x - y) ≤ norm (z - y)"
    using simplex_furthest_le[of "{a, b}" y]
    using assms[unfolded segment_convex_hull]
    by auto
  then show ?thesis
    by (auto simp add:norm_minus_commute)
qed

lemma closed_segment_commute: "closed_segment a b = closed_segment b a"
proof -
  have "{a, b} = {b, a}" by auto
  thus ?thesis
    by (simp add: segment_convex_hull)
qed

lemma segment_bound1:
  assumes "x ∈ closed_segment a b"
  shows "norm (x - a) ≤ norm (b - a)"
proof -
  obtain u where "x = (1 - u) *R a + u *R b" "0 ≤ u" "u ≤ 1"
    using assms by (auto simp add: closed_segment_def)
  then show "norm (x - a) ≤ norm (b - a)"
    apply clarify
    apply (auto simp: algebra_simps)
    apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le)
    done
qed

lemma segment_bound:
  assumes "x ∈ closed_segment a b"
  shows "norm (x - a) ≤ norm (b - a)" "norm (x - b) ≤ norm (b - a)"
apply (simp add: assms segment_bound1)
by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)

lemma open_segment_commute: "open_segment a b = open_segment b a"
proof -
  have "{a, b} = {b, a}" by auto
  thus ?thesis
    by (simp add: closed_segment_commute open_segment_def)
qed

lemma closed_segment_idem [simp]: "closed_segment a a = {a}"
  unfolding segment by (auto simp add: algebra_simps)

lemma open_segment_idem [simp]: "open_segment a a = {}"
  by (simp add: open_segment_def)

lemma closed_segment_eq_open: "closed_segment a b = open_segment a b ∪ {a,b}"
  using open_segment_def by auto

lemma convex_contains_open_segment:
  "convex s ⟷ (∀a∈s. ∀b∈s. open_segment a b ⊆ s)"
  by (simp add: convex_contains_segment closed_segment_eq_open)

lemma closed_segment_eq_real_ivl:
  fixes a b::real
  shows "closed_segment a b = (if a ≤ b then {a .. b} else {b .. a})"
proof -
  have "b ≤ a ⟹ closed_segment b a = {b .. a}"
    and "a ≤ b ⟹ closed_segment a b = {a .. b}"
    by (auto simp: convex_hull_eq_real_cbox segment_convex_hull)
  thus ?thesis
    by (auto simp: closed_segment_commute)
qed

lemma open_segment_eq_real_ivl:
  fixes a b::real
  shows "open_segment a b = (if a ≤ b then {a<..<b} else {b<..<a})"
by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm)

lemma closed_segment_real_eq:
  fixes u::real shows "closed_segment u v = (λx. (v - u) * x + u) ` {0..1}"
  by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)

lemma dist_in_closed_segment:
  fixes a :: "'a :: euclidean_space"
  assumes "x ∈ closed_segment a b"
    shows "dist x a ≤ dist a b ∧ dist x b ≤ dist a b"
proof (intro conjI)
  obtain u where u: "0 ≤ u" "u ≤ 1" and x: "x = (1 - u) *R a + u *R b"
    using assms by (force simp: in_segment algebra_simps)
  have "dist x a = u * dist a b"
    apply (simp add: dist_norm algebra_simps x)
    by (metis ‹0 ≤ u› abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib)
  also have "...  ≤ dist a b"
    by (simp add: mult_left_le_one_le u)
  finally show "dist x a ≤ dist a b" .
  have "dist x b = norm ((1-u) *R a - (1-u) *R b)"
    by (simp add: dist_norm algebra_simps x)
  also have "... = (1-u) * dist a b"
  proof -
    have "norm ((1 - 1 * u) *R (a - b)) = (1 - 1 * u) * norm (a - b)"
      using ‹u ≤ 1› by force
    then show ?thesis                     
      by (simp add: dist_norm real_vector.scale_right_diff_distrib)
  qed
  also have "... ≤ dist a b"
    by (simp add: mult_left_le_one_le u)
  finally show "dist x b ≤ dist a b" .
qed

lemma dist_in_open_segment:
  fixes a :: "'a :: euclidean_space"
  assumes "x ∈ open_segment a b"
    shows "dist x a < dist a b ∧ dist x b < dist a b"
proof (intro conjI)
  obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *R a + u *R b"
    using assms by (force simp: in_segment algebra_simps)
  have "dist x a = u * dist a b"
    apply (simp add: dist_norm algebra_simps x)
    by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib ‹0 < u›)
  also have *: "...  < dist a b"
    by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 ‹u < 1›)
  finally show "dist x a < dist a b" .
  have ab_ne0: "dist a b ≠ 0"
    using * by fastforce
  have "dist x b = norm ((1-u) *R a - (1-u) *R b)"
    by (simp add: dist_norm algebra_simps x)
  also have "... = (1-u) * dist a b"
  proof -
    have "norm ((1 - 1 * u) *R (a - b)) = (1 - 1 * u) * norm (a - b)"
      using ‹u < 1› by force
    then show ?thesis
      by (simp add: dist_norm real_vector.scale_right_diff_distrib)
  qed
  also have "... < dist a b"
    using ab_ne0 ‹0 < u› by simp
  finally show "dist x b < dist a b" .
qed

lemma dist_decreases_open_segment_0:
  fixes x :: "'a :: euclidean_space"
  assumes "x ∈ open_segment 0 b"
    shows "dist c x < dist c 0 ∨ dist c x < dist c b"
proof (rule ccontr, clarsimp simp: not_less)
  obtain u where u: "0 ≠ b" "0 < u" "u < 1" and x: "x = u *R b"
    using assms by (auto simp: in_segment)
  have xb: "x ∙ b < b ∙ b"
    using u x by auto
  assume "norm c ≤ dist c x"
  then have "c ∙ c ≤ (c - x) ∙ (c - x)"
    by (simp add: dist_norm norm_le)
  moreover have "0 < x ∙ b"
    using u x by auto
  ultimately have less: "c ∙ b < x ∙ b"
    by (simp add: x algebra_simps inner_commute u)
  assume "dist c b ≤ dist c x"
  then have "(c - b) ∙ (c - b) ≤ (c - x) ∙ (c - x)"
    by (simp add: dist_norm norm_le)
  then have "(b ∙ b) * (1 - u*u) ≤ 2 * (b ∙ c) * (1-u)"
    by (simp add: x algebra_simps inner_commute)
  then have "(1+u) * (b ∙ b) * (1-u) ≤ 2 * (b ∙ c) * (1-u)"
    by (simp add: algebra_simps)
  then have "(1+u) * (b ∙ b) ≤ 2 * (b ∙ c)"
    using ‹u < 1› by auto
  with xb have "c ∙ b ≥ x ∙ b"
    by (auto simp: x algebra_simps inner_commute)
  with less show False by auto
qed

proposition dist_decreases_open_segment:
  fixes a :: "'a :: euclidean_space"
  assumes "x ∈ open_segment a b"
    shows "dist c x < dist c a ∨ dist c x < dist c b"
proof -
  have *: "x - a ∈ open_segment 0 (b - a)" using assms
    by (metis diff_self open_segment_translation_eq uminus_add_conv_diff)
  show ?thesis
    using dist_decreases_open_segment_0 [OF *, of "c-a"] assms
    by (simp add: dist_norm)
qed

corollary open_segment_furthest_le:
  fixes a b x y :: "'a::euclidean_space"
  assumes "x ∈ open_segment a b"
  shows "norm (y - x) < norm (y - a) ∨  norm (y - x) < norm (y - b)"
  by (metis assms dist_decreases_open_segment dist_norm)

corollary dist_decreases_closed_segment:
  fixes a :: "'a :: euclidean_space"
  assumes "x ∈ closed_segment a b"
    shows "dist c x ≤ dist c a ∨ dist c x ≤ dist c b"
apply (cases "x ∈ open_segment a b")
 using dist_decreases_open_segment less_eq_real_def apply blast
by (metis DiffI assms empty_iff insertE open_segment_def order_refl)

lemma convex_intermediate_ball:
  fixes a :: "'a :: euclidean_space"
  shows "⟦ball a r ⊆ T; T ⊆ cball a r⟧ ⟹ convex T"
apply (simp add: convex_contains_open_segment, clarify)
by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)

lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b ⊆ closed_segment a b"
  apply (clarsimp simp: midpoint_def in_segment)
  apply (rule_tac x="(1 + u) / 2" in exI)
  apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib)
  by (metis real_sum_of_halves scaleR_left.add)

lemma notin_segment_midpoint:
  fixes a :: "'a :: euclidean_space"
  shows "a ≠ b ⟹ a ∉ closed_segment (midpoint a b) b"
by (auto simp: dist_midpoint dest!: dist_in_closed_segment)

lemma segment_to_closest_point:
  fixes S :: "'a :: euclidean_space set"
  shows "⟦closed S; S ≠ {}⟧ ⟹ open_segment a (closest_point S a) ∩ S = {}"
  apply (subst disjoint_iff_not_equal)
  apply (clarify dest!: dist_in_open_segment)
  by (metis closest_point_le dist_commute le_less_trans less_irrefl)

lemma segment_to_point_exists:
  fixes S :: "'a :: euclidean_space set"
    assumes "closed S" "S ≠ {}"
    obtains b where "b ∈ S" "open_segment a b ∩ S = {}"
  by (metis assms segment_to_closest_point closest_point_exists that)

subsubsection‹More lemmas, especially for working with the underlying formula›

lemma segment_eq_compose:
  fixes a :: "'a :: real_vector"
  shows "(λu. (1 - u) *R a + u *R b) = (λx. a + x) o (λu. u *R (b - a))"
    by (simp add: o_def algebra_simps)

lemma segment_degen_1:
  fixes a :: "'a :: real_vector"
  shows "(1 - u) *R a + u *R b = b ⟷ a=b ∨ u=1"
proof -
  { assume "(1 - u) *R a + u *R b = b"
    then have "(1 - u) *R a = (1 - u) *R b"
      by (simp add: algebra_simps)
    then have "a=b ∨ u=1"
      by simp
  } then show ?thesis
      by (auto simp: algebra_simps)
qed

lemma segment_degen_0:
    fixes a :: "'a :: real_vector"
    shows "(1 - u) *R a + u *R b = a ⟷ a=b ∨ u=0"
  using segment_degen_1 [of "1-u" b a]
  by (auto simp: algebra_simps)

lemma add_scaleR_degen:
  fixes a b ::"'a::real_vector"
  assumes  "(u *R b + v *R a) = (u *R a + v *R b)"  "u ≠ v"
  shows "a=b"
  by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms)
  
lemma closed_segment_image_interval:
     "closed_segment a b = (λu. (1 - u) *R a + u *R b) ` {0..1}"
  by (auto simp: set_eq_iff image_iff closed_segment_def)

lemma open_segment_image_interval:
     "open_segment a b = (if a=b then {} else (λu. (1 - u) *R a + u *R b) ` {0<..<1})"
  by (auto simp:  open_segment_def closed_segment_def segment_degen_0 segment_degen_1)

lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval

lemma open_segment_bound1:
  assumes "x ∈ open_segment a b"
  shows "norm (x - a) < norm (b - a)"
proof -
  obtain u where "x = (1 - u) *R a + u *R b" "0 < u" "u < 1" "a ≠ b"
    using assms by (auto simp add: open_segment_image_interval split: if_split_asm)
  then show "norm (x - a) < norm (b - a)"
    apply clarify
    apply (auto simp: algebra_simps)
    apply (simp add: scaleR_diff_right [symmetric])
    done
qed

lemma compact_segment [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "compact (closed_segment a b)"
  by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros)

lemma closed_segment [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "closed (closed_segment a b)"
  by (simp add: compact_imp_closed)

lemma closure_closed_segment [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "closure(closed_segment a b) = closed_segment a b"
  by simp

lemma open_segment_bound:
  assumes "x ∈ open_segment a b"
  shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)"
apply (simp add: assms open_segment_bound1)
by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute)

lemma closure_open_segment [simp]:
    fixes a :: "'a::euclidean_space"
    shows "closure(open_segment a b) = (if a = b then {} else closed_segment a b)"
proof -
  have "closure ((λu. u *R (b - a)) ` {0<..<1}) = (λu. u *R (b - a)) ` closure {0<..<1}" if "a ≠ b"
    apply (rule closure_injective_linear_image [symmetric])
    apply (simp add:)
    using that by (simp add: inj_on_def)
  then show ?thesis
    by (simp add: segment_image_interval segment_eq_compose closure_greaterThanLessThan [symmetric]
         closure_translation image_comp [symmetric] del: closure_greaterThanLessThan)
qed

lemma closed_open_segment_iff [simp]:
    fixes a :: "'a::euclidean_space"  shows "closed(open_segment a b) ⟷ a = b"
  by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2))

lemma compact_open_segment_iff [simp]:
    fixes a :: "'a::euclidean_space"  shows "compact(open_segment a b) ⟷ a = b"
  by (simp add: bounded_open_segment compact_eq_bounded_closed)

lemma convex_closed_segment [iff]: "convex (closed_segment a b)"
  unfolding segment_convex_hull by(rule convex_convex_hull)

lemma convex_open_segment [iff]: "convex(open_segment a b)"
proof -
  have "convex ((λu. u *R (b-a)) ` {0<..<1})"
    by (rule convex_linear_image) auto
  then show ?thesis
    apply (simp add: open_segment_image_interval segment_eq_compose)
    by (metis image_comp convex_translation)
qed


lemmas convex_segment = convex_closed_segment convex_open_segment

lemma connected_segment [iff]:
  fixes x :: "'a :: real_normed_vector"
  shows "connected (closed_segment x y)"
  by (simp add: convex_connected)

lemma affine_hull_closed_segment [simp]:
     "affine hull (closed_segment a b) = affine hull {a,b}"
  by (simp add: segment_convex_hull)

lemma affine_hull_open_segment [simp]:
    fixes a :: "'a::euclidean_space"
    shows "affine hull (open_segment a b) = (if a = b then {} else affine hull {a,b})"
by (metis affine_hull_convex_hull affine_hull_empty closure_open_segment closure_same_affine_hull segment_convex_hull)

lemma rel_interior_closure_convex_segment:
  fixes S :: "_::euclidean_space set"
  assumes "convex S" "a ∈ rel_interior S" "b ∈ closure S"
    shows "open_segment a b ⊆ rel_interior S"
proof
  fix x
  have [simp]: "(1 - u) *R a + u *R b = b - (1 - u) *R (b - a)" for u
    by (simp add: algebra_simps)
  assume "x ∈ open_segment a b"
  then show "x ∈ rel_interior S"
    unfolding closed_segment_def open_segment_def  using assms
    by (auto intro: rel_interior_closure_convex_shrink)
qed

lemma convex_hull_insert_segments:
   "convex hull (insert a S) =
    (if S = {} then {a} else  ⋃x ∈ convex hull S. closed_segment a x)"
  by (force simp add: convex_hull_insert_alt in_segment)

lemma Int_convex_hull_insert_rel_exterior:
  fixes z :: "'a::euclidean_space"
  assumes "convex C" "T ⊆ C" and z: "z ∈ rel_interior C" and dis: "disjnt S (rel_interior C)"
  shows "S ∩ (convex hull (insert z T)) = S ∩ (convex hull T)" (is "?lhs = ?rhs")
proof
  have "T = {} ⟹ z ∉ S"
    using dis z by (auto simp add: disjnt_def)
  then show "?lhs ⊆ ?rhs"
  proof (clarsimp simp add: convex_hull_insert_segments)
    fix x y
    assume "x ∈ S" and y: "y ∈ convex hull T" and "x ∈ closed_segment z y"
    have "y ∈ closure C"
      by (metis y ‹convex C› ‹T ⊆ C› closure_subset contra_subsetD convex_hull_eq hull_mono)
    moreover have "x ∉ rel_interior C"
      by (meson ‹x ∈ S› dis disjnt_iff)
    moreover have "x ∈ open_segment z y ∪ {z, y}"
      using ‹x ∈ closed_segment z y› closed_segment_eq_open by blast
    ultimately show "x ∈ convex hull T"
      using rel_interior_closure_convex_segment [OF ‹convex C› z]
      using y z by blast
  qed
  show "?rhs ⊆ ?lhs"
    by (meson hull_mono inf_mono subset_insertI subset_refl)
qed

subsection‹More results about segments›

lemma dist_half_times2:
  fixes a :: "'a :: real_normed_vector"
  shows "dist ((1 / 2) *R (a + b)) x * 2 = dist (a+b) (2 *R x)"
proof -
  have "norm ((1 / 2) *R (a + b) - x) * 2 = norm (2 *R ((1 / 2) *R (a + b) - x))"
    by simp
  also have "... = norm ((a + b) - 2 *R x)"
    by (simp add: real_vector.scale_right_diff_distrib)
  finally show ?thesis
    by (simp only: dist_norm)
qed

lemma closed_segment_as_ball:
    "closed_segment a b = affine hull {a,b} ∩ cball(inverse 2 *R (a + b))(norm(b - a) / 2)"
proof (cases "b = a")
  case True then show ?thesis by (auto simp: hull_inc)
next
  case False
  then have *: "((∃u v. x = u *R a + v *R b ∧ u + v = 1) ∧
                  dist ((1 / 2) *R (a + b)) x * 2 ≤ norm (b - a)) =
                 (∃u. x = (1 - u) *R a + u *R b ∧ 0 ≤ u ∧ u ≤ 1)" for x
  proof -
    have "((∃u v. x = u *R a + v *R b ∧ u + v = 1) ∧
                  dist ((1 / 2) *R (a + b)) x * 2 ≤ norm (b - a)) =
          ((∃u. x = (1 - u) *R a + u *R b) ∧
                  dist ((1 / 2) *R (a + b)) x * 2 ≤ norm (b - a))"
      unfolding eq_diff_eq [symmetric] by simp
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧
                          norm ((a+b) - (2 *R x)) ≤ norm (b - a))"
      by (simp add: dist_half_times2) (simp add: dist_norm)
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧
            norm ((a+b) - (2 *R ((1 - u) *R a + u *R b))) ≤ norm (b - a))"
      by auto
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧
                norm ((1 - u * 2) *R (b - a)) ≤ norm (b - a))"
      by (simp add: algebra_simps scaleR_2)
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧
                          ¦1 - u * 2¦ * norm (b - a) ≤ norm (b - a))"
      by simp
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧ ¦1 - u * 2¦ ≤ 1)"
      by (simp add: mult_le_cancel_right2 False)
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧ 0 ≤ u ∧ u ≤ 1)"
      by auto
    finally show ?thesis .
  qed
  show ?thesis
    by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
qed

lemma open_segment_as_ball:
    "open_segment a b =
     affine hull {a,b} ∩ ball(inverse 2 *R (a + b))(norm(b - a) / 2)"
proof (cases "b = a")
  case True then show ?thesis by (auto simp: hull_inc)
next
  case False
  then have *: "((∃u v. x = u *R a + v *R b ∧ u + v = 1) ∧
                  dist ((1 / 2) *R (a + b)) x * 2 < norm (b - a)) =
                 (∃u. x = (1 - u) *R a + u *R b ∧ 0 < u ∧ u < 1)" for x
  proof -
    have "((∃u v. x = u *R a + v *R b ∧ u + v = 1) ∧
                  dist ((1 / 2) *R (a + b)) x * 2 < norm (b - a)) =
          ((∃u. x = (1 - u) *R a + u *R b) ∧
                  dist ((1 / 2) *R (a + b)) x * 2 < norm (b - a))"
      unfolding eq_diff_eq [symmetric] by simp
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧
                          norm ((a+b) - (2 *R x)) < norm (b - a))"
      by (simp add: dist_half_times2) (simp add: dist_norm)
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧
            norm ((a+b) - (2 *R ((1 - u) *R a + u *R b))) < norm (b - a))"
      by auto
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧
                norm ((1 - u * 2) *R (b - a)) < norm (b - a))"
      by (simp add: algebra_simps scaleR_2)
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧
                          ¦1 - u * 2¦ * norm (b - a) < norm (b - a))"
      by simp
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧ ¦1 - u * 2¦ < 1)"
      by (simp add: mult_le_cancel_right2 False)
    also have "... = (∃u. x = (1 - u) *R a + u *R b ∧ 0 < u ∧ u < 1)"
      by auto
    finally show ?thesis .
  qed
  show ?thesis
    using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
qed

lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball

lemma closed_segment_neq_empty [simp]: "closed_segment a b ≠ {}"
  by auto

lemma open_segment_eq_empty [simp]: "open_segment a b = {} ⟷ a = b"
proof -
  { assume a1: "open_segment a b = {}"
    have "{} ≠ {0::real<..<1}"
      by simp
    then have "a = b"
      using a1 open_segment_image_interval by fastforce
  } then show ?thesis by auto
qed

lemma open_segment_eq_empty' [simp]: "{} = open_segment a b ⟷ a = b"
  using open_segment_eq_empty by blast

lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty

lemma inj_segment:
  fixes a :: "'a :: real_vector"
  assumes "a ≠ b"
    shows "inj_on (λu. (1 - u) *R a + u *R b) I"
proof
  fix x y
  assume "(1 - x) *R a + x *R b = (1 - y) *R a + y *R b"
  then have "x *R (b - a) = y *R (b - a)"
    by (simp add: algebra_simps)
  with assms show "x = y"
    by (simp add: real_vector.scale_right_imp_eq)
qed

lemma finite_closed_segment [simp]: "finite(closed_segment a b) ⟷ a = b"
  apply auto
  apply (rule ccontr)
  apply (simp add: segment_image_interval)
  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
  done

lemma finite_open_segment [simp]: "finite(open_segment a b) ⟷ a = b"
  by (auto simp: open_segment_def)

lemmas finite_segment = finite_closed_segment finite_open_segment

lemma closed_segment_eq_sing: "closed_segment a b = {c} ⟷ a = c ∧ b = c"
  by auto

lemma open_segment_eq_sing: "open_segment a b ≠ {c}"
  by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)

lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing

lemma subset_closed_segment:
    "closed_segment a b ⊆ closed_segment c d ⟷
     a ∈ closed_segment c d ∧ b ∈ closed_segment c d"
  by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)

lemma subset_co_segment:
    "closed_segment a b ⊆ open_segment c d ⟷
     a ∈ open_segment c d ∧ b ∈ open_segment c d"
using closed_segment_subset by blast

lemma subset_open_segment:
  fixes a :: "'a::euclidean_space"
  shows "open_segment a b ⊆ open_segment c d ⟷
         a = b ∨ a ∈ closed_segment c d ∧ b ∈ closed_segment c d"
        (is "?lhs = ?rhs")
proof (cases "a = b")
  case True then show ?thesis by simp
next
  case False show ?thesis
  proof
    assume rhs: ?rhs
    with ‹a ≠ b› have "c ≠ d"
      using closed_segment_idem singleton_iff by auto
    have "∃uc. (1 - u) *R ((1 - ua) *R c + ua *R d) + u *R ((1 - ub) *R c + ub *R d) =
               (1 - uc) *R c + uc *R d ∧ 0 < uc ∧ uc < 1"
        if neq: "(1 - ua) *R c + ua *R d ≠ (1 - ub) *R c + ub *R d" "c ≠ d"
           and "a = (1 - ua) *R c + ua *R d" "b = (1 - ub) *R c + ub *R d"
           and u: "0 < u" "u < 1" and uab: "0 ≤ ua" "ua ≤ 1" "0 ≤ ub" "ub ≤ 1"
        for u ua ub
    proof -
      have "ua ≠ ub"
        using neq by auto
      moreover have "(u - 1) * ua ≤ 0" using u uab
        by (simp add: mult_nonpos_nonneg)
      ultimately have lt: "(u - 1) * ua < u * ub" using u uab
        by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
      have "p * ua + q * ub < p+q" if p: "0 < p" and  q: "0 < q" for p q
      proof -
        have "¬ p ≤ 0" "¬ q ≤ 0"
          using p q not_less by blast+
        then show ?thesis
          by (metis ‹ua ≠ ub› add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
                    less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
      qed
      then have "(1 - u) * ua + u * ub < 1" using u ‹ua ≠ ub›
        by (metis diff_add_cancel diff_gt_0_iff_gt)
      with lt show ?thesis
        by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
    qed
    with rhs ‹a ≠ b› ‹c ≠ d› show ?lhs
      unfolding open_segment_image_interval closed_segment_def
      by (fastforce simp add:)
  next
    assume lhs: ?lhs
    with ‹a ≠ b› have "c ≠ d"
      by (meson finite_open_segment rev_finite_subset)
    have "closure (open_segment a b) ⊆ closure (open_segment c d)"
      using lhs closure_mono by blast
    then have "closed_segment a b ⊆ closed_segment c d"
      by (simp add: ‹a ≠ b› ‹c ≠ d›)
    then show ?rhs
      by (force simp: ‹a ≠ b›)
  qed
qed

lemma subset_oc_segment:
  fixes a :: "'a::euclidean_space"
  shows "open_segment a b ⊆ closed_segment c d ⟷
         a = b ∨ a ∈ closed_segment c d ∧ b ∈ closed_segment c d"
apply (simp add: subset_open_segment [symmetric])
apply (rule iffI)
 apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
apply (meson dual_order.trans segment_open_subset_closed)
done

lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment


subsection‹Betweenness›

definition "between = (λ(a,b) x. x ∈ closed_segment a b)"

lemma betweenI:
  assumes "0 ≤ u" "u ≤ 1" "x = (1 - u) *R a + u *R b"
  shows "between (a, b) x"
using assms unfolding between_def closed_segment_def by auto

lemma betweenE:
  assumes "between (a, b) x"
  obtains u where "0 ≤ u" "u ≤ 1" "x = (1 - u) *R a + u *R b"
using assms unfolding between_def closed_segment_def by auto

lemma between_implies_scaled_diff:
  assumes "between (S, T) X" "between (S, T) Y" "S ≠ Y"
  obtains c where "(X - Y) = c *R (S - Y)"
proof -
  from ‹between (S, T) X› obtain uX where X: "X = uX *R S + (1 - uX) *R T"
    by (metis add.commute betweenE eq_diff_eq)
  from ‹between (S, T) Y› obtain uY where Y: "Y = uY *R S + (1 - uY) *R T"
    by (metis add.commute betweenE eq_diff_eq)
  have "X - Y = (uX - uY) *R (S - T)"
  proof -
    from X Y have "X - Y =  uX *R S - uY *R S + ((1 - uX) *R T - (1 - uY) *R T)" by simp
    also have "… = (uX - uY) *R S - (uX - uY) *R T" by (simp add: scaleR_left.diff)
    finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib)
  qed
  moreover from Y have "S - Y = (1 - uY) *R (S - T)"
    by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
  moreover note ‹S ≠ Y›
  ultimately have "(X - Y) = ((uX - uY) / (1 - uY)) *R (S - Y)" by auto
  from this that show thesis by blast
qed

lemma between_mem_segment: "between (a,b) x ⟷ x ∈ closed_segment a b"
  unfolding between_def by auto

lemma between: "between (a, b) (x::'a::euclidean_space) ⟷ dist a b = (dist a x) + (dist x b)"
proof (cases "a = b")
  case True
  then show ?thesis
    unfolding between_def split_conv
    by (auto simp add: dist_commute)
next
  case False
  then have Fal: "norm (a - b) ≠ 0" and Fal2: "norm (a - b) > 0"
    by auto
  have *: "⋀u. a - ((1 - u) *R a + u *R b) = u *R (a - b)"
    by (auto simp add: algebra_simps)
  show ?thesis
    unfolding between_def split_conv closed_segment_def mem_Collect_eq
    apply rule
    apply (elim exE conjE)
    apply (subst dist_triangle_eq)
  proof -
    fix u
    assume as: "x = (1 - u) *R a + u *R b" "0 ≤ u" "u ≤ 1"
    then have *: "a - x = u *R (a - b)" "x - b = (1 - u) *R (a - b)"
      unfolding as(1) by (auto simp add:algebra_simps)
    show "norm (a - x) *R (x - b) = norm (x - b) *R (a - x)"
      unfolding norm_minus_commute[of x a] * using as(2,3)
      by (auto simp add: field_simps)
  next
    assume as: "dist a b = dist a x + dist x b"
    have "norm (a - x) / norm (a - b) ≤ 1"
      using Fal2 unfolding as[unfolded dist_norm] norm_ge_zero by auto
    then show "∃u. x = (1 - u) *R a + u *R b ∧ 0 ≤ u ∧ u ≤ 1"
      apply (rule_tac x="dist a x / dist a b" in exI)
      unfolding dist_norm
      apply (subst euclidean_eq_iff)
      apply rule
      defer
      apply rule
      prefer 3
      apply rule
    proof -
      fix i :: 'a
      assume i: "i ∈ Basis"
      have "((1 - norm (a - x) / norm (a - b)) *R a + (norm (a - x) / norm (a - b)) *R b) ∙ i =
        ((norm (a - b) - norm (a - x)) * (a ∙ i) + norm (a - x) * (b ∙ i)) / norm (a - b)"
        using Fal by (auto simp add: field_simps inner_simps)
      also have "… = x∙i"
        apply (rule divide_eq_imp[OF Fal])
        unfolding as[unfolded dist_norm]
        using as[unfolded dist_triangle_eq]
        apply -
        apply (subst (asm) euclidean_eq_iff)
        using i
        apply (erule_tac x=i in ballE)
        apply (auto simp add: field_simps inner_simps)
        done
      finally show "x ∙ i =
        ((1 - norm (a - x) / norm (a - b)) *R a + (norm (a - x) / norm (a - b)) *R b) ∙ i"
        by auto
    qed (insert Fal2, auto)
  qed
qed

lemma between_midpoint:
  fixes a :: "'a::euclidean_space"
  shows "between (a,b) (midpoint a b)" (is ?t1)
    and "between (b,a) (midpoint a b)" (is ?t2)
proof -
  have *: "⋀x y z. x = (1/2::real) *R z ⟹ y = (1/2) *R z ⟹ norm z = norm x + norm y"
    by auto
  show ?t1 ?t2
    unfolding between midpoint_def dist_norm
    apply(rule_tac[!] *)
    unfolding euclidean_eq_iff[where 'a='a]
    apply (auto simp add: field_simps inner_simps)
    done
qed

lemma between_mem_convex_hull:
  "between (a,b) x ⟷ x ∈ convex hull {a,b}"
  unfolding between_mem_segment segment_convex_hull ..

lemma between_triv_iff [simp]: "between (a,a) b ⟷ a=b"
  by (auto simp: between_def)

lemma between_triv1 [simp]: "between (a,b) a"
  by (auto simp: between_def)

lemma between_triv2 [simp]: "between (a,b) b"
  by (auto simp: between_def)

lemma between_commute:
   "between (a,b) = between (b,a)"
by (auto simp: between_def closed_segment_commute)

lemma between_antisym:
  fixes a :: "'a :: euclidean_space"
  shows "⟦between (b,c) a; between (a,c) b⟧ ⟹ a = b"
by (auto simp: between dist_commute)

lemma between_trans:
    fixes a :: "'a :: euclidean_space"
    shows "⟦between (b,c) a; between (a,c) d⟧ ⟹ between (b,c) d"
  using dist_triangle2 [of b c d] dist_triangle3 [of b d a]
  by (auto simp: between dist_commute)

lemma between_norm:
    fixes a :: "'a :: euclidean_space"
    shows "between (a,b) x ⟷ norm(x - a) *R (b - x) = norm(b - x) *R (x - a)"
  by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps)

lemma between_swap:
  fixes A B X Y :: "'a::euclidean_space"
  assumes "between (A, B) X"
  assumes "between (A, B) Y"
  shows "between (X, B) Y ⟷ between (A, Y) X"
using assms by (auto simp add: between)

lemma between_translation [simp]: "between (a + y,a + z) (a + x) ⟷ between (y,z) x"
  by (auto simp: between_def)

lemma between_trans_2:
  fixes a :: "'a :: euclidean_space"
  shows "⟦between (b,c) a; between (a,b) d⟧ ⟹ between (c,d) a"
  by (metis between_commute between_swap between_trans)

lemma between_scaleR_lift [simp]:
  fixes v :: "'a::euclidean_space"
  shows "between (a *R v, b *R v) (c *R v) ⟷ v = 0 ∨ between (a, b) c"
  by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric])

lemma between_1:
  fixes x::real
  shows "between (a,b) x ⟷ (a ≤ x ∧ x ≤ b) ∨ (b ≤ x ∧ x ≤ a)"
  by (auto simp: between_mem_segment closed_segment_eq_real_ivl)


subsection ‹Shrinking towards the interior of a convex set›

lemma mem_interior_convex_shrink:
  fixes s :: "'a::euclidean_space set"
  assumes "convex s"
    and "c ∈ interior s"
    and "x ∈ s"
    and "0 < e"
    and "e ≤ 1"
  shows "x - e *R (x - c) ∈ interior s"
proof -
  obtain d where "d > 0" and d: "ball c d ⊆ s"
    using assms(2) unfolding mem_interior by auto
  show ?thesis
    unfolding mem_interior
    apply (rule_tac x="e*d" in exI)
    apply rule
    defer
    unfolding subset_eq Ball_def mem_ball
  proof (rule, rule)
    fix y
    assume as: "dist (x - e *R (x - c)) y < e * d"
    have *: "y = (1 - (1 - e)) *R ((1 / e) *R y - ((1 - e) / e) *R x) + (1 - e) *R x"
      using ‹e > 0› by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
    have "dist c ((1 / e) *R y - ((1 - e) / e) *R x) = ¦1/e¦ * norm (e *R c - y + (1 - e) *R x)"
      unfolding dist_norm
      unfolding norm_scaleR[symmetric]
      apply (rule arg_cong[where f=norm])
      using ‹e > 0›
      by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
    also have "… = ¦1/e¦ * norm (x - e *R (x - c) - y)"
      by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
    also have "… < d"
      using as[unfolded dist_norm] and ‹e > 0›
      by (auto simp add:pos_divide_less_eq[OF ‹e > 0›] mult.commute)
    finally show "y ∈ s"
      apply (subst *)
      apply (rule assms(1)[unfolded convex_alt,rule_format])
      apply (rule d[unfolded subset_eq,rule_format])
      unfolding mem_ball
      using assms(3-5)
      apply auto
      done
  qed (insert ‹e>0› ‹d>0›, auto)
qed

lemma mem_interior_closure_convex_shrink:
  fixes s :: "'a::euclidean_space set"
  assumes "convex s"
    and "c ∈ interior s"
    and "x ∈ closure s"
    and "0 < e"
    and "e ≤ 1"
  shows "x - e *R (x - c) ∈ interior s"
proof -
  obtain d where "d > 0" and d: "ball c d ⊆ s"
    using assms(2) unfolding mem_interior by auto
  have "∃y∈s. norm (y - x) * (1 - e) < e * d"
  proof (cases "x ∈ s")
    case True
    then show ?thesis
      using ‹e > 0› ‹d > 0›
      apply (rule_tac bexI[where x=x])
      apply (auto)
      done
  next
    case False
    then have x: "x islimpt s"
      using assms(3)[unfolded closure_def] by auto
    show ?thesis
    proof (cases "e = 1")
      case True
      obtain y where "y ∈ s" "y ≠ x" "dist y x < 1"
        using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto
      then show ?thesis
        apply (rule_tac x=y in bexI)
        unfolding True
        using ‹d > 0›
        apply auto
        done
    next
      case False
      then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
        using ‹e ≤ 1› ‹e > 0› ‹d > 0› by auto
      then obtain y where "y ∈ s" "y ≠ x" "dist y x < e * d / (1 - e)"
        using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
      then show ?thesis
        apply (rule_tac x=y in bexI)
        unfolding dist_norm
        using pos_less_divide_eq[OF *]
        apply auto
        done
    qed
  qed
  then obtain y where "y ∈ s" and y: "norm (y - x) * (1 - e) < e * d"
    by auto
  define z where "z = c + ((1 - e) / e) *R (x - y)"
  have *: "x - e *R (x - c) = y - e *R (y - z)"
    unfolding z_def using ‹e > 0›
    by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
  have "z ∈ interior s"
    apply (rule interior_mono[OF d,unfolded subset_eq,rule_format])
    unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
    apply (auto simp add:field_simps norm_minus_commute)
    done
  then show ?thesis
    unfolding *
    apply -
    apply (rule mem_interior_convex_shrink)
    using assms(1,4-5) ‹y∈s›
    apply auto
    done
qed

lemma in_interior_closure_convex_segment:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" and a: "a ∈ interior S" and b: "b ∈ closure S"
    shows "open_segment a b ⊆ interior S"
proof (clarsimp simp: in_segment)
  fix u::real
  assume u: "0 < u" "u < 1"
  have "(1 - u) *R a + u *R b = b - (1 - u) *R (b - a)"
    by (simp add: algebra_simps)
  also have "... ∈ interior S" using mem_interior_closure_convex_shrink [OF assms] u
    by simp
  finally show "(1 - u) *R a + u *R b ∈ interior S" .
qed

lemma closure_open_Int_superset:
  assumes "open S" "S ⊆ closure T"
  shows "closure(S ∩ T) = closure S"
proof -
  have "closure S ⊆ closure(S ∩ T)"
    by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
  then show ?thesis
    by (simp add: closure_mono dual_order.antisym)
qed

lemma convex_closure_interior:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" and int: "interior S ≠ {}"
  shows "closure(interior S) = closure S"
proof -
  obtain a where a: "a ∈ interior S"
    using int by auto
  have "closure S ⊆ closure(interior S)"
  proof
    fix x
    assume x: "x ∈ closure S"
    show "x ∈ closure (interior S)"
    proof (cases "x=a")
      case True
      then show ?thesis
        using ‹a ∈ interior S› closure_subset by blast
    next
      case False
      show ?thesis
      proof (clarsimp simp add: closure_def islimpt_approachable)
        fix e::real
        assume xnotS: "x ∉ interior S" and "0 < e"
        show "∃x'∈interior S. x' ≠ x ∧ dist x' x < e"
        proof (intro bexI conjI)
          show "x - min (e/2 / norm (x - a)) 1 *R (x - a) ≠ x"
            using False ‹0 < e› by (auto simp: algebra_simps min_def)
          show "dist (x - min (e/2 / norm (x - a)) 1 *R (x - a)) x < e"
            using ‹0 < e› by (auto simp: dist_norm min_def)
          show "x - min (e/2 / norm (x - a)) 1 *R (x - a) ∈ interior S"
            apply (clarsimp simp add: min_def a)
            apply (rule mem_interior_closure_convex_shrink [OF ‹convex S› a x])
            using ‹0 < e› False apply (auto simp: divide_simps)
            done
        qed
      qed
    qed
  qed
  then show ?thesis
    by (simp add: closure_mono interior_subset subset_antisym)
qed

lemma closure_convex_Int_superset:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "interior S ≠ {}" "interior S ⊆ closure T"
  shows "closure(S ∩ T) = closure S"
proof -
  have "closure S ⊆ closure(interior S)"
    by (simp add: convex_closure_interior assms)
  also have "... ⊆ closure (S ∩ T)"
    using interior_subset [of S] assms
    by (metis (no_types, lifting) Int_assoc Int_lower2 closure_mono closure_open_Int_superset inf.orderE open_interior)
  finally show ?thesis
    by (simp add: closure_mono dual_order.antisym)
qed


subsection ‹Some obvious but surprisingly hard simplex lemmas›

lemma simplex:
  assumes "finite s"
    and "0 ∉ s"
  shows "convex hull (insert 0 s) =
    {y. (∃u. (∀x∈s. 0 ≤ u x) ∧ sum u s ≤ 1 ∧ sum (λx. u x *R x) s = y)}"
  unfolding convex_hull_finite[OF finite.insertI[OF assms(1)]]
  apply (rule set_eqI, rule)
  unfolding mem_Collect_eq
  apply (erule_tac[!] exE)
  apply (erule_tac[!] conjE)+
  unfolding sum_clauses(2)[OF ‹finite s›]
  apply (rule_tac x=u in exI)
  defer
  apply (rule_tac x="λx. if x = 0 then 1 - sum u s else u x" in exI)
  using assms(2)
  unfolding if_smult and sum_delta_notmem[OF assms(2)]
  apply auto
  done

lemma substd_simplex:
  assumes d: "d ⊆ Basis"
  shows "convex hull (insert 0 d) =
    {x. (∀i∈Basis. 0 ≤ x∙i) ∧ (∑i∈d. x∙i) ≤ 1 ∧ (∀i∈Basis. i ∉ d ⟶ x∙i = 0)}"
  (is "convex hull (insert 0 ?p) = ?s")
proof -
  let ?D = d
  have "0 ∉ ?p"
    using assms by (auto simp: image_def)
  from d have "finite d"
    by (blast intro: finite_subset finite_Basis)
  show ?thesis
    unfolding simplex[OF ‹finite d› ‹0 ∉ ?p›]
    apply (rule set_eqI)
    unfolding mem_Collect_eq
    apply rule
    apply (elim exE conjE)
    apply (erule_tac[2] conjE)+
  proof -
    fix x :: "'a::euclidean_space"
    fix u
    assume as: "∀x∈?D. 0 ≤ u x" "sum u ?D ≤ 1" "(∑x∈?D. u x *R x) = x"
    have *: "∀i∈Basis. i:d ⟶ u i = x∙i"
      and "(∀i∈Basis. i ∉ d ⟶ x ∙ i = 0)"
      using as(3)
      unfolding substdbasis_expansion_unique[OF assms]
      by auto
    then have **: "sum u ?D = sum (op ∙ x) ?D"
      apply -
      apply (rule sum.cong)
      using assms
      apply auto
      done
    have "(∀i∈Basis. 0 ≤ x∙i) ∧ sum (op ∙ x) ?D ≤ 1"
    proof (rule,rule)
      fix i :: 'a
      assume i: "i ∈ Basis"
      have "i ∈ d ⟹ 0 ≤ x∙i"
        unfolding *[rule_format,OF i,symmetric]
         apply (rule_tac as(1)[rule_format])
         apply auto
         done
      moreover have "i ∉ d ⟹ 0 ≤ x∙i"
        using ‹(∀i∈Basis. i ∉ d ⟶ x ∙ i = 0)›[rule_format, OF i] by auto
      ultimately show "0 ≤ x∙i" by auto
    qed (insert as(2)[unfolded **], auto)
    then show "(∀i∈Basis. 0 ≤ x∙i) ∧ sum (op ∙ x) ?D ≤ 1 ∧ (∀i∈Basis. i ∉ d ⟶ x ∙ i = 0)"
      using ‹(∀i∈Basis. i ∉ d ⟶ x ∙ i = 0)› by auto
  next
    fix x :: "'a::euclidean_space"
    assume as: "∀i∈Basis. 0 ≤ x ∙ i" "sum (op ∙ x) ?D ≤ 1" "(∀i∈Basis. i ∉ d ⟶ x ∙ i = 0)"
    show "∃u. (∀x∈?D. 0 ≤ u x) ∧ sum u ?D ≤ 1 ∧ (∑x∈?D. u x *R x) = x"
      using as d
      unfolding substdbasis_expansion_unique[OF assms]
      apply (rule_tac x="inner x" in exI)
      apply auto
      done
  qed
qed

lemma std_simplex:
  "convex hull (insert 0 Basis) =
    {x::'a::euclidean_space. (∀i∈Basis. 0 ≤ x∙i) ∧ sum (λi. x∙i) Basis ≤ 1}"
  using substd_simplex[of Basis] by auto

lemma interior_std_simplex:
  "interior (convex hull (insert 0 Basis)) =
    {x::'a::euclidean_space. (∀i∈Basis. 0 < x∙i) ∧ sum (λi. x∙i) Basis < 1}"
  apply (rule set_eqI)
  unfolding mem_interior std_simplex
  unfolding subset_eq mem_Collect_eq Ball_def mem_ball
  unfolding Ball_def[symmetric]
  apply rule
  apply (elim exE conjE)
  defer
  apply (erule conjE)
proof -
  fix x :: 'a
  fix e
  assume "e > 0" and as: "∀xa. dist x xa < e ⟶ (∀x∈Basis. 0 ≤ xa ∙ x) ∧ sum (op ∙ xa) Basis ≤ 1"
  show "(∀xa∈Basis. 0 < x ∙ xa) ∧ sum (op ∙ x) Basis < 1"
    apply safe
  proof -
    fix i :: 'a
    assume i: "i ∈ Basis"
    then show "0 < x ∙ i"
      using as[THEN spec[where x="x - (e / 2) *R i"]] and ‹e > 0›
      unfolding dist_norm
      by (auto elim!: ballE[where x=i] simp: inner_simps)
  next
    have **: "dist x (x + (e / 2) *R (SOME i. i∈Basis)) < e" using ‹e > 0›
      unfolding dist_norm
      by (auto intro!: mult_strict_left_mono simp: SOME_Basis)
    have "⋀i. i ∈ Basis ⟹ (x + (e / 2) *R (SOME i. i∈Basis)) ∙ i =
      x∙i + (if i = (SOME i. i∈Basis) then e/2 else 0)"
      by (auto simp: SOME_Basis inner_Basis inner_simps)
    then have *: "sum (op ∙ (x + (e / 2) *R (SOME i. i∈Basis))) Basis =
      sum (λi. x∙i + (if (SOME i. i∈Basis) = i then e/2 else 0)) Basis"
      apply (rule_tac sum.cong)
      apply auto
      done
    have "sum (op ∙ x) Basis < sum (op ∙ (x + (e / 2) *R (SOME i. i∈Basis))) Basis"
      unfolding * sum.distrib
      using ‹e > 0› DIM_positive[where 'a='a]
      apply (subst sum.delta')
      apply (auto simp: SOME_Basis)
      done
    also have "… ≤ 1"
      using **
      apply (drule_tac as[rule_format])
      apply auto
      done
    finally show "sum (op ∙ x) Basis < 1" by auto
  qed
next
  fix x :: 'a
  assume as: "∀i∈Basis. 0 < x ∙ i" "sum (op ∙ x) Basis < 1"
  obtain a :: 'b where "a ∈ UNIV" using UNIV_witness ..
  let ?d = "(1 - sum (op ∙ x) Basis) / real (DIM('a))"
  show "∃e>0. ∀y. dist x y < e ⟶ (∀i∈Basis. 0 ≤ y ∙ i) ∧ sum (op ∙ y) Basis ≤ 1"
  proof (rule_tac x="min (Min ((op ∙ x) ` Basis)) D" for D in exI, intro conjI impI allI)
    fix y
    assume y: "dist x y < min (Min (op ∙ x ` Basis)) ?d"
    have "sum (op ∙ y) Basis ≤ sum (λi. x∙i + ?d) Basis"
    proof (rule sum_mono)
      fix i :: 'a
      assume i: "i ∈ Basis"
      then have "¦y∙i - x∙i¦ < ?d"
        apply -
        apply (rule le_less_trans)
        using Basis_le_norm[OF i, of "y - x"]
        using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2]
        apply (auto simp add: norm_minus_commute inner_diff_left)
        done
      then show "y ∙ i ≤ x ∙ i + ?d" by auto
    qed
    also have "… ≤ 1"
      unfolding sum.distrib sum_constant
      by (auto simp add: Suc_le_eq)
    finally show "sum (op ∙ y) Basis ≤ 1" .
    show "(∀i∈Basis. 0 ≤ y ∙ i)"
    proof safe
      fix i :: 'a
      assume i: "i ∈ Basis"
      have "norm (x - y) < x∙i"
        apply (rule less_le_trans)
        apply (rule y[unfolded min_less_iff_conj dist_norm, THEN conjunct1])
        using i
        apply auto
        done
      then show "0 ≤ y∙i"
        using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i]
        by (auto simp: inner_simps)
    qed
  next
    have "Min ((op ∙ x) ` Basis) > 0"
      using as by simp
    moreover have "?d > 0"
      using as by (auto simp: Suc_le_eq)
    ultimately show "0 < min (Min (op ∙ x ` Basis)) ((1 - sum (op ∙ x) Basis) / real DIM('a))"
      by linarith
  qed 
qed

lemma interior_std_simplex_nonempty:
  obtains a :: "'a::euclidean_space" where
    "a ∈ interior(convex hull (insert 0 Basis))"
proof -
  let ?D = "Basis :: 'a set"
  let ?a = "sum (λb::'a. inverse (2 * real DIM('a)) *R b) Basis"
  {
    fix i :: 'a
    assume i: "i ∈ Basis"
    have "?a ∙ i = inverse (2 * real DIM('a))"
      by (rule trans[of _ "sum (λj. if i = j then inverse (2 * real DIM('a)) else 0) ?D"])
         (simp_all add: sum.If_cases i) }
  note ** = this
  show ?thesis
    apply (rule that[of ?a])
    unfolding interior_std_simplex mem_Collect_eq
  proof safe
    fix i :: 'a
    assume i: "i ∈ Basis"
    show "0 < ?a ∙ i"
      unfolding **[OF i] by (auto simp add: Suc_le_eq DIM_positive)
  next
    have "sum (op ∙ ?a) ?D = sum (λi. inverse (2 * real DIM('a))) ?D"
      apply (rule sum.cong)
      apply rule
      apply auto
      done
    also have "… < 1"
      unfolding sum_constant divide_inverse[symmetric]
      by (auto simp add: field_simps)
    finally show "sum (op ∙ ?a) ?D < 1" by auto
  qed
qed

lemma rel_interior_substd_simplex:
  assumes d: "d ⊆ Basis"
  shows "rel_interior (convex hull (insert 0 d)) =
    {x::'a::euclidean_space. (∀i∈d. 0 < x∙i) ∧ (∑i∈d. x∙i) < 1 ∧ (∀i∈Basis. i ∉ d ⟶ x∙i = 0)}"
  (is "rel_interior (convex hull (insert 0 ?p)) = ?s")
proof -
  have "finite d"
    apply (rule finite_subset)
    using assms
    apply auto
    done
  show ?thesis
  proof (cases "d = {}")
    case True
    then show ?thesis
      using rel_interior_sing using euclidean_eq_iff[of _ 0] by auto
  next
    case False
    have h0: "affine hull (convex hull (insert 0 ?p)) =
      {x::'a::euclidean_space. (∀i∈Basis. i ∉ d ⟶ x∙i = 0)}"
      using affine_hull_convex_hull affine_hull_substd_basis assms by auto
    have aux: "⋀x::'a. ∀i∈Basis. (∀i∈d. 0 ≤ x∙i) ∧ (∀i∈Basis. i ∉ d ⟶ x∙i = 0) ⟶ 0 ≤ x∙i"
      by auto
    {
      fix x :: "'a::euclidean_space"
      assume x: "x ∈ rel_interior (convex hull (insert 0 ?p))"
      then obtain e where e0: "e > 0" and
        "ball x e ∩ {xa. (∀i∈Basis. i ∉ d ⟶ xa∙i = 0)} ⊆ convex hull (insert 0 ?p)"
        using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto
      then have as: "∀xa. dist x xa < e ∧ (∀i∈Basis. i ∉ d ⟶ xa∙i = 0) ⟶
        (∀i∈d. 0 ≤ xa ∙ i) ∧ sum (op ∙ xa) d ≤ 1"
        unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto
      have x0: "(∀i∈Basis. i ∉ d ⟶ x∙i = 0)"
        using x rel_interior_subset  substd_simplex[OF assms] by auto
      have "(∀i∈d. 0 < x ∙ i) ∧ sum (op ∙ x) d < 1 ∧ (∀i∈Basis. i ∉ d ⟶ x∙i = 0)"
        apply rule
        apply rule
      proof -
        fix i :: 'a
        assume "i ∈ d"
        then have "∀ia∈d. 0 ≤ (x - (e / 2) *R i) ∙ ia"
          apply -
          apply (rule as[rule_format,THEN conjunct1])
          unfolding dist_norm
          using d ‹e > 0› x0
          apply (auto simp: inner_simps inner_Basis)
          done
        then show "0 < x ∙ i"
          apply (erule_tac x=i in ballE)
          using ‹e > 0› ‹i ∈ d› d
          apply (auto simp: inner_simps inner_Basis)
          done
      next
        obtain a where a: "a ∈ d"
          using ‹d ≠ {}› by auto
        then have **: "dist x (x + (e / 2) *R a) < e"
          using ‹e > 0› norm_Basis[of a] d
          unfolding dist_norm
          by auto
        have "⋀i. i ∈ Basis ⟹ (x + (e / 2) *R a) ∙ i = x∙i + (if i = a then e/2 else 0)"
          using a d by (auto simp: inner_simps inner_Basis)
        then have *: "sum (op ∙ (x + (e / 2) *R a)) d =
          sum (λi. x∙i + (if a = i then e/2 else 0)) d"
          using d by (intro sum.cong) auto
        have "a ∈ Basis"
          using ‹a ∈ d› d by auto
        then have h1: "(∀i∈Basis. i ∉ d ⟶ (x + (e / 2) *R a) ∙ i = 0)"
          using x0 d ‹a∈d› by (auto simp add: inner_add_left inner_Basis)
        have "sum (op ∙ x) d < sum (op ∙ (x + (e / 2) *R a)) d"
          unfolding * sum.distrib
          using ‹e > 0› ‹a ∈ d›
          using ‹finite d›
          by (auto simp add: sum.delta')
        also have "… ≤ 1"
          using ** h1 as[rule_format, of "x + (e / 2) *R a"]
          by auto
        finally show "sum (op ∙ x) d < 1 ∧ (∀i∈Basis. i ∉ d ⟶ x∙i = 0)"
          using x0 by auto
      qed
    }
    moreover
    {
      fix x :: "'a::euclidean_space"
      assume as: "x ∈ ?s"
      have "∀i. 0 < x∙i ∨ 0 = x∙i ⟶ 0 ≤ x∙i"
        by auto
      moreover have "∀i. i ∈ d ∨ i ∉ d" by auto
      ultimately
      have "∀i. (∀i∈d. 0 < x∙i) ∧ (∀i. i ∉ d ⟶ x∙i = 0) ⟶ 0 ≤ x∙i"
        by metis
      then have h2: "x ∈ convex hull (insert 0 ?p)"
        using as assms
        unfolding substd_simplex[OF assms] by fastforce
      obtain a where a: "a ∈ d"
        using ‹d ≠ {}› by auto
      let ?d = "(1 - sum (op ∙ x) d) / real (card d)"
      have "0 < card d" using ‹d ≠ {}› ‹finite d›
        by (simp add: card_gt_0_iff)
      have "Min ((op ∙ x) ` d) > 0"
        using as ‹d ≠ {}› ‹finite d› by (simp add: Min_gr_iff)
      moreover have "?d > 0" using as using ‹0 < card d› by auto
      ultimately have h3: "min (Min ((op ∙ x) ` d)) ?d > 0"
        by auto

      have "x ∈ rel_interior (convex hull (insert 0 ?p))"
        unfolding rel_interior_ball mem_Collect_eq h0
        apply (rule,rule h2)
        unfolding substd_simplex[OF assms]
        apply (rule_tac x="min (Min ((op ∙ x) ` d)) ?d" in exI)
        apply (rule, rule h3)
        apply safe
        unfolding mem_ball
      proof -
        fix y :: 'a
        assume y: "dist x y < min (Min (op ∙ x ` d)) ?d"
        assume y2: "∀i∈Basis. i ∉ d ⟶ y∙i = 0"
        have "sum (op ∙ y) d ≤ sum (λi. x∙i + ?d) d"
        proof (rule sum_mono)
          fix i
          assume "i ∈ d"
          with d have i: "i ∈ Basis"
            by auto
          have "¦y∙i - x∙i¦ < ?d"
            apply (rule le_less_trans)
            using Basis_le_norm[OF i, of "y - x"]
            using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2]
            apply (auto simp add: norm_minus_commute inner_simps)
            done
          then show "y ∙ i ≤ x ∙ i + ?d" by auto
        qed
        also have "… ≤ 1"
          unfolding sum.distrib sum_constant  using ‹0 < card d›
          by auto
        finally show "sum (op ∙ y) d ≤ 1" .

        fix i :: 'a
        assume i: "i ∈ Basis"
        then show "0 ≤ y∙i"
        proof (cases "i∈d")
          case True
          have "norm (x - y) < x∙i"
            using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
            using Min_gr_iff[of "op ∙ x ` d" "norm (x - y)"] ‹0 < card d› ‹i:d›
            by (simp add: card_gt_0_iff)
          then show "0 ≤ y∙i"
            using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format]
            by (auto simp: inner_simps)
        qed (insert y2, auto)
      qed
    }
    ultimately have
      "⋀x. x ∈ rel_interior (convex hull insert 0 d) ⟷
        x ∈ {x. (∀i∈d. 0 < x ∙ i) ∧ sum (op ∙ x) d < 1 ∧ (∀i∈Basis. i ∉ d ⟶ x ∙ i = 0)}"
      by blast
    then show ?thesis by (rule set_eqI)
  qed
qed

lemma rel_interior_substd_simplex_nonempty:
  assumes "d ≠ {}"
    and "d ⊆ Basis"
  obtains a :: "'a::euclidean_space"
    where "a ∈ rel_interior (convex hull (insert 0 d))"
proof -
  let ?D = d
  let ?a = "sum (λb::'a::euclidean_space. inverse (2 * real (card d)) *R b) ?D"
  have "finite d"
    apply (rule finite_subset)
    using assms(2)
    apply auto
    done
  then have d1: "0 < real (card d)"
    using ‹d ≠ {}› by auto
  {
    fix i
    assume "i ∈ d"
    have "?a ∙ i = inverse (2 * real (card d))"
      apply (rule trans[of _ "sum (λj. if i = j then inverse (2 * real (card d)) else 0) ?D"])
      unfolding inner_sum_left
      apply (rule sum.cong)
      using ‹i ∈ d› ‹finite d› sum.delta'[of d i "(λk. inverse (2 * real (card d)))"]
        d1 assms(2)
      by (auto simp: inner_Basis set_rev_mp[OF _ assms(2)])
  }
  note ** = this
  show ?thesis
    apply (rule that[of ?a])
    unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq
  proof safe
    fix i
    assume "i ∈ d"
    have "0 < inverse (2 * real (card d))"
      using d1 by auto
    also have "… = ?a ∙ i" using **[of i] ‹i ∈ d›
      by auto
    finally show "0 < ?a ∙ i" by auto
  next
    have "sum (op ∙ ?a) ?D = sum (λi. inverse (2 * real (card d))) ?D"
      by (rule sum.cong) (rule refl, rule **)
    also have "… < 1"
      unfolding sum_constant divide_real_def[symmetric]
      by (auto simp add: field_simps)
    finally show "sum (op ∙ ?a) ?D < 1" by auto
  next
    fix i
    assume "i ∈ Basis" and "i ∉ d"
    have "?a ∈ span d"
    proof (rule span_sum[of d "(λb. b /R (2 * real (card d)))" d])
      {
        fix x :: "'a::euclidean_space"
        assume "x ∈ d"
        then have "x ∈ span d"
          using span_superset[of _ "d"] by auto
        then have "x /R (2 * real (card d)) ∈ span d"
          using span_mul[of x "d" "(inverse (real (card d)) / 2)"] by auto
      }
      then show "⋀x. x∈d ⟹ x /R (2 * real (card d)) ∈ span d"
        by auto
    qed
    then show "?a ∙ i = 0 "
      using ‹i ∉ d› unfolding span_substd_basis[OF assms(2)] using ‹i ∈ Basis› by auto
  qed
qed


subsection ‹Relative interior of convex set›

lemma rel_interior_convex_nonempty_aux:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
    and "0 ∈ S"
  shows "rel_interior S ≠ {}"
proof (cases "S = {0}")
  case True
  then show ?thesis using rel_interior_sing by auto
next
  case False
  obtain B where B: "independent B ∧ B ≤ S ∧ S ≤ span B ∧ card B = dim S"
    using basis_exists[of S] by auto
  then have "B ≠ {}"
    using B assms ‹S ≠ {0}› span_empty by auto
  have "insert 0 B ≤ span B"
    using subspace_span[of B] subspace_0[of "span B"] span_inc by auto
  then have "span (insert 0 B) ≤ span B"
    using span_span[of B] span_mono[of "insert 0 B" "span B"] by blast
  then have "convex hull insert 0 B ≤ span B"
    using convex_hull_subset_span[of "insert 0 B"] by auto
  then have "span (convex hull insert 0 B) ≤ span B"
    using span_span[of B] span_mono[of "convex hull insert 0 B" "span B"] by blast
  then have *: "span (convex hull insert 0 B) = span B"
    using span_mono[of B "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
  then have "span (convex hull insert 0 B) = span S"
    using B span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
  moreover have "0 ∈ affine hull (convex hull insert 0 B)"
    using hull_subset[of "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
  ultimately have **: "affine hull (convex hull insert 0 B) = affine hull S"
    using affine_hull_span_0[of "convex hull insert 0 B"] affine_hull_span_0[of "S"]
      assms hull_subset[of S]
    by auto
  obtain d and f :: "'n ⇒ 'n" where
    fd: "card d = card B" "linear f" "f ` B = d"
      "f ` span B = {x. ∀i∈Basis. i ∉ d ⟶ x ∙ i = (0::real)} ∧ inj_on f (span B)"
    and d: "d ⊆ Basis"
    using basis_to_substdbasis_subspace_isomorphism[of B,OF _ ] B by auto
  then have "bounded_linear f"
    using linear_conv_bounded_linear by auto
  have "d ≠ {}"
    using fd B ‹B ≠ {}› by auto
  have "insert 0 d = f ` (insert 0 B)"
    using fd linear_0 by auto
  then have "(convex hull (insert 0 d)) = f ` (convex hull (insert 0 B))"
    using convex_hull_linear_image[of f "(insert 0 d)"]
      convex_hull_linear_image[of f "(insert 0 B)"] ‹linear f›
    by auto
  moreover have "rel_interior (f ` (convex hull insert 0 B)) =
    f ` rel_interior (convex hull insert 0 B)"
    apply (rule  rel_interior_injective_on_span_linear_image[of f "(convex hull insert 0 B)"])
    using ‹bounded_linear f› fd *
    apply auto
    done
  ultimately have "rel_interior (convex hull insert 0 B) ≠ {}"
    using rel_interior_substd_simplex_nonempty[OF ‹d ≠ {}› d]
    apply auto
    apply blast
    done
  moreover have "convex hull (insert 0 B) ⊆ S"
    using B assms hull_mono[of "insert 0 B" "S" "convex"] convex_hull_eq
    by auto
  ultimately show ?thesis
    using subset_rel_interior[of "convex hull insert 0 B" S] ** by auto
qed

lemma rel_interior_eq_empty:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "rel_interior S = {} ⟷ S = {}"
proof -
  {
    assume "S ≠ {}"
    then obtain a where "a ∈ S" by auto
    then have "0 ∈ op + (-a) ` S"
      using assms exI[of "(λx. x ∈ S ∧ - a + x = 0)" a] by auto
    then have "rel_interior (op + (-a) ` S) ≠ {}"
      using rel_interior_convex_nonempty_aux[of "op + (-a) ` S"]
        convex_translation[of S "-a"] assms
      by auto
    then have "rel_interior S ≠ {}"
      using rel_interior_translation by auto
  }
  then show ?thesis
    using rel_interior_empty by auto
qed

lemma interior_simplex_nonempty:
  fixes S :: "'N :: euclidean_space set"
  assumes "independent S" "finite S" "card S = DIM('N)"
  obtains a where "a ∈ interior (convex hull (insert 0 S))"
proof -
  have "affine hull (insert 0 S) = UNIV"
    apply (simp add: hull_inc affine_hull_span_0)
    using assms dim_eq_full indep_card_eq_dim_span by fastforce
  moreover have "rel_interior (convex hull insert 0 S) ≠ {}"
    using rel_interior_eq_empty [of "convex hull (insert 0 S)"] by auto
  ultimately have "interior (convex hull insert 0 S) ≠ {}"
    by (simp add: rel_interior_interior)
  with that show ?thesis
    by auto
qed

lemma convex_rel_interior:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "convex (rel_interior S)"
proof -
  {
    fix x y and u :: real
    assume assm: "x ∈ rel_interior S" "y ∈ rel_interior S" "0 ≤ u" "u ≤ 1"
    then have "x ∈ S"
      using rel_interior_subset by auto
    have "x - u *R (x-y) ∈ rel_interior S"
    proof (cases "0 = u")
      case False
      then have "0 < u" using assm by auto
      then show ?thesis
        using assm rel_interior_convex_shrink[of S y x u] assms ‹x ∈ S› by auto
    next
      case True
      then show ?thesis using assm by auto
    qed
    then have "(1 - u) *R x + u *R y ∈ rel_interior S"
      by (simp add: algebra_simps)
  }
  then show ?thesis
    unfolding convex_alt by auto
qed

lemma convex_closure_rel_interior:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "closure (rel_interior S) = closure S"
proof -
  have h1: "closure (rel_interior S) ≤ closure S"
    using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
  show ?thesis
  proof (cases "S = {}")
    case False
    then obtain a where a: "a ∈ rel_interior S"
      using rel_interior_eq_empty assms by auto
    { fix x
      assume x: "x ∈ closure S"
      {
        assume "x = a"
        then have "x ∈ closure (rel_interior S)"
          using a unfolding closure_def by auto
      }
      moreover
      {
        assume "x ≠ a"
         {
           fix e :: real
           assume "e > 0"
           define e1 where "e1 = min 1 (e/norm (x - a))"
           then have e1: "e1 > 0" "e1 ≤ 1" "e1 * norm (x - a) ≤ e"
             using ‹x ≠ a› ‹e > 0› le_divide_eq[of e1 e "norm (x - a)"]
             by simp_all
           then have *: "x - e1 *R (x - a) : rel_interior S"
             using rel_interior_closure_convex_shrink[of S a x e1] assms x a e1_def
             by auto
           have "∃y. y ∈ rel_interior S ∧ y ≠ x ∧ dist y x ≤ e"
              apply (rule_tac x="x - e1 *R (x - a)" in exI)
              using * e1 dist_norm[of "x - e1 *R (x - a)" x] ‹x ≠ a›
              apply simp
              done
        }
        then have "x islimpt rel_interior S"
          unfolding islimpt_approachable_le by auto
        then have "x ∈ closure(rel_interior S)"
          unfolding closure_def by auto
      }
      ultimately have "x ∈ closure(rel_interior S)" by auto
    }
    then show ?thesis using h1 by auto
  next
    case True
    then have "rel_interior S = {}"
      using rel_interior_empty by auto
    then have "closure (rel_interior S) = {}"
      using closure_empty by auto
    with True show ?thesis by auto
  qed
qed

lemma rel_interior_same_affine_hull:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "affine hull (rel_interior S) = affine hull S"
  by (metis assms closure_same_affine_hull convex_closure_rel_interior)

lemma rel_interior_aff_dim:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "aff_dim (rel_interior S) = aff_dim S"
  by (metis aff_dim_affine_hull2 assms rel_interior_same_affine_hull)

lemma rel_interior_rel_interior:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "rel_interior (rel_interior S) = rel_interior S"
proof -
  have "openin (subtopology euclidean (affine hull (rel_interior S))) (rel_interior S)"
    using openin_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
  then show ?thesis
    using rel_interior_def by auto
qed

lemma rel_interior_rel_open:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "rel_open (rel_interior S)"
  unfolding rel_open_def using rel_interior_rel_interior assms by auto

lemma convex_rel_interior_closure_aux:
  fixes x y z :: "'n::euclidean_space"
  assumes "0 < a" "0 < b" "(a + b) *R z = a *R x + b *R y"
  obtains e where "0 < e" "e ≤ 1" "z = y - e *R (y - x)"
proof -
  define e where "e = a / (a + b)"
  have "z = (1 / (a + b)) *R ((a + b) *R z)"
    apply auto
    using assms
    apply simp
    done
  also have "… = (1 / (a + b)) *R (a *R x + b *R y)"
    using assms scaleR_cancel_left[of "1/(a+b)" "(a + b) *R z" "a *R x + b *R y"]
    by auto
  also have "… = y - e *R (y-x)"
    using e_def
    apply (simp add: algebra_simps)
    using scaleR_left_distrib[of "a/(a+b)" "b/(a+b)" y] assms add_divide_distrib[of a b "a+b"]
    apply auto
    done
  finally have "z = y - e *R (y-x)"
    by auto
  moreover have "e > 0" using e_def assms by auto
  moreover have "e ≤ 1" using e_def assms by auto
  ultimately show ?thesis using that[of e] by auto
qed

lemma convex_rel_interior_closure:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "rel_interior (closure S) = rel_interior S"
proof (cases "S = {}")
  case True
  then show ?thesis
    using assms rel_interior_eq_empty by auto
next
  case False
  have "rel_interior (closure S) ⊇ rel_interior S"
    using subset_rel_interior[of S "closure S"] closure_same_affine_hull closure_subset
    by auto
  moreover
  {
    fix z
    assume z: "z ∈ rel_interior (closure S)"
    obtain x where x: "x ∈ rel_interior S"
      using ‹S ≠ {}› assms rel_interior_eq_empty by auto
    have "z ∈ rel_interior S"
    proof (cases "x = z")
      case True
      then show ?thesis using x by auto
    next
      case False
      obtain e where e: "e > 0" "cball z e ∩ affine hull closure S ≤ closure S"
        using z rel_interior_cball[of "closure S"] by auto
      hence *: "0 < e/norm(z-x)" using e False by auto
      define y where "y = z + (e/norm(z-x)) *R (z-x)"
      have yball: "y ∈ cball z e"
        using mem_cball y_def dist_norm[of z y] e by auto
      have "x ∈ affine hull closure S"
        using x rel_interior_subset_closure hull_inc[of x "closure S"] by blast
      moreover have "z ∈ affine hull closure S"
        using z rel_interior_subset hull_subset[of "closure S"] by blast
      ultimately have "y ∈ affine hull closure S"
        using y_def affine_affine_hull[of "closure S"]
          mem_affine_3_minus [of "affine hull closure S" z z x "e/norm(z-x)"] by auto
      then have "y ∈ closure S" using e yball by auto
      have "(1 + (e/norm(z-x))) *R z = (e/norm(z-x)) *R x + y"
        using y_def by (simp add: algebra_simps)
      then obtain e1 where "0 < e1" "e1 ≤ 1" "z = y - e1 *R (y - x)"
        using * convex_rel_interior_closure_aux[of "e / norm (z - x)" 1 z x y]
        by (auto simp add: algebra_simps)
      then show ?thesis
        using rel_interior_closure_convex_shrink assms x ‹y ∈ closure S›
        by auto
    qed
  }
  ultimately show ?thesis by auto
qed

lemma convex_interior_closure:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "interior (closure S) = interior S"
  using closure_aff_dim[of S] interior_rel_interior_gen[of S]
    interior_rel_interior_gen[of "closure S"]
    convex_rel_interior_closure[of S] assms
  by auto

lemma closure_eq_rel_interior_eq:
  fixes S1 S2 :: "'n::euclidean_space set"
  assumes "convex S1"
    and "convex S2"
  shows "closure S1 = closure S2 ⟷ rel_interior S1 = rel_interior S2"
  by (metis convex_rel_interior_closure convex_closure_rel_interior assms)

lemma closure_eq_between:
  fixes S1 S2 :: "'n::euclidean_space set"
  assumes "convex S1"
    and "convex S2"
  shows "closure S1 = closure S2 ⟷ rel_interior S1 ≤ S2 ∧ S2 ⊆ closure S1"
  (is "?A ⟷ ?B")
proof
  assume ?A
  then show ?B
    by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
next
  assume ?B
  then have "closure S1 ⊆ closure S2"
    by (metis assms(1) convex_closure_rel_interior closure_mono)
  moreover from ‹?B› have "closure S1 ⊇ closure S2"
    by (metis closed_closure closure_minimal)
  ultimately show ?A ..
qed

lemma open_inter_closure_rel_interior:
  fixes S A :: "'n::euclidean_space set"
  assumes "convex S"
    and "open A"
  shows "A ∩ closure S = {} ⟷ A ∩ rel_interior S = {}"
  by (metis assms convex_closure_rel_interior open_Int_closure_eq_empty)

lemma rel_interior_open_segment:
  fixes a :: "'a :: euclidean_space"
  shows "rel_interior(open_segment a b) = open_segment a b"
proof (cases "a = b")
  case True then show ?thesis by auto
next
  case False then show ?thesis
    apply (simp add: rel_interior_eq openin_open)
    apply (rule_tac x="ball (inverse 2 *R (a + b)) (norm(b - a) / 2)" in exI)
    apply (simp add: open_segment_as_ball)
    done
qed

lemma rel_interior_closed_segment:
  fixes a :: "'a :: euclidean_space"
  shows "rel_interior(closed_segment a b) =
         (if a = b then {a} else open_segment a b)"
proof (cases "a = b")
  case True then show ?thesis by auto
next
  case False then show ?thesis
    by simp
       (metis closure_open_segment convex_open_segment convex_rel_interior_closure
              rel_interior_open_segment)
qed

lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment

lemma starlike_convex_tweak_boundary_points:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "S ≠ {}" and ST: "rel_interior S ⊆ T" and TS: "T ⊆ closure S"
  shows "starlike T"
proof -
  have "rel_interior S ≠ {}"
    by (simp add: assms rel_interior_eq_empty)
  then obtain a where a: "a ∈ rel_interior S"  by blast
  with ST have "a ∈ T"  by blast
  have *: "⋀x. x ∈ T ⟹ open_segment a x ⊆ rel_interior S"
    apply (rule rel_interior_closure_convex_segment [OF ‹convex S› a])
    using assms by blast
  show ?thesis
    unfolding starlike_def
    apply (rule bexI [OF _ ‹a ∈ T›])
    apply (simp add: closed_segment_eq_open)
    apply (intro conjI ballI a ‹a ∈ T› rel_interior_closure_convex_segment [OF ‹convex S› a])
    apply (simp add: order_trans [OF * ST])
    done
qed

subsection‹The relative frontier of a set›

definition "rel_frontier S = closure S - rel_interior S"

lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
  by (simp add: rel_frontier_def)

lemma rel_frontier_eq_empty:
    fixes S :: "'n::euclidean_space set"
    shows "rel_frontier S = {} ⟷ affine S"
  apply (simp add: rel_frontier_def)
  apply (simp add: rel_interior_eq_closure [symmetric])
  using rel_interior_subset_closure by blast

lemma rel_frontier_sing [simp]:
    fixes a :: "'n::euclidean_space"
    shows "rel_frontier {a} = {}"
  by (simp add: rel_frontier_def)

lemma rel_frontier_affine_hull:
  fixes S :: "'a::euclidean_space set"
  shows "rel_frontier S ⊆ affine hull S"
using closure_affine_hull rel_frontier_def by fastforce

lemma rel_frontier_cball [simp]:
    fixes a :: "'n::euclidean_space"
    shows "rel_frontier(cball a r) = (if r = 0 then {} else sphere a r)"
proof (cases rule: linorder_cases [of r 0])
  case less then show ?thesis
    by (force simp: sphere_def)
next
  case equal then show ?thesis by simp
next
  case greater then show ?thesis
    apply simp
    by (metis centre_in_ball empty_iff frontier_cball frontier_def interior_cball interior_rel_interior_gen rel_frontier_def)
qed

lemma rel_frontier_translation:
  fixes a :: "'a::euclidean_space"
  shows "rel_frontier((λx. a + x) ` S) = (λx. a + x) ` (rel_frontier S)"
by (simp add: rel_frontier_def translation_diff rel_interior_translation closure_translation)

lemma closed_affine_hull [iff]:
  fixes S :: "'n::euclidean_space set"
  shows "closed (affine hull S)"
  by (metis affine_affine_hull affine_closed)

lemma rel_frontier_nonempty_interior:
  fixes S :: "'n::euclidean_space set"
  shows "interior S ≠ {} ⟹ rel_frontier S = frontier S"
by (metis frontier_def interior_rel_interior_gen rel_frontier_def)

lemma rel_frontier_frontier:
  fixes S :: "'n::euclidean_space set"
  shows "affine hull S = UNIV ⟹ rel_frontier S = frontier S"
by (simp add: frontier_def rel_frontier_def rel_interior_interior)

lemma closest_point_in_rel_frontier:
   "⟦closed S; S ≠ {}; x ∈ affine hull S - rel_interior S⟧
   ⟹ closest_point S x ∈ rel_frontier S"
  by (simp add: closest_point_in_rel_interior closest_point_in_set rel_frontier_def)

lemma closed_rel_frontier [iff]:
  fixes S :: "'n::euclidean_space set"
  shows "closed (rel_frontier S)"
proof -
  have *: "closedin (subtopology euclidean (affine hull S)) (closure S - rel_interior S)"
    by (simp add: closed_subset closedin_diff closure_affine_hull openin_rel_interior)
  show ?thesis
    apply (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"])
    unfolding rel_frontier_def
    using * closed_affine_hull
    apply auto
    done
qed

lemma closed_rel_boundary:
  fixes S :: "'n::euclidean_space set"
  shows "closed S ⟹ closed(S - rel_interior S)"
by (metis closed_rel_frontier closure_closed rel_frontier_def)

lemma compact_rel_boundary:
  fixes S :: "'n::euclidean_space set"
  shows "compact S ⟹ compact(S - rel_interior S)"
by (metis bounded_diff closed_rel_boundary closure_eq compact_closure compact_imp_closed)

lemma bounded_rel_frontier:
  fixes S :: "'n::euclidean_space set"
  shows "bounded S ⟹ bounded(rel_frontier S)"
by (simp add: bounded_closure bounded_diff rel_frontier_def)

lemma compact_rel_frontier_bounded:
  fixes S :: "'n::euclidean_space set"
  shows "bounded S ⟹ compact(rel_frontier S)"
using bounded_rel_frontier closed_rel_frontier compact_eq_bounded_closed by blast

lemma compact_rel_frontier:
  fixes S :: "'n::euclidean_space set"
  shows "compact S ⟹ compact(rel_frontier S)"
by (meson compact_eq_bounded_closed compact_rel_frontier_bounded)

lemma convex_same_rel_interior_closure:
  fixes S :: "'n::euclidean_space set"
  shows "⟦convex S; convex T⟧
         ⟹ rel_interior S = rel_interior T ⟷ closure S = closure T"
by (simp add: closure_eq_rel_interior_eq)

lemma convex_same_rel_interior_closure_straddle:
  fixes S :: "'n::euclidean_space set"
  shows "⟦convex S; convex T⟧
         ⟹ rel_interior S = rel_interior T ⟷
             rel_interior S ⊆ T ∧ T ⊆ closure S"
by (simp add: closure_eq_between convex_same_rel_interior_closure)

lemma convex_rel_frontier_aff_dim:
  fixes S1 S2 :: "'n::euclidean_space set"
  assumes "convex S1"
    and "convex S2"
    and "S2 ≠ {}"
    and "S1 ≤ rel_frontier S2"
  shows "aff_dim S1 < aff_dim S2"
proof -
  have "S1 ⊆ closure S2"
    using assms unfolding rel_frontier_def by auto
  then have *: "affine hull S1 ⊆ affine hull S2"
    using hull_mono[of "S1" "closure S2"] closure_same_affine_hull[of S2] by blast
  then have "aff_dim S1 ≤ aff_dim S2"
    using * aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2]
      aff_dim_subset[of "affine hull S1" "affine hull S2"]
    by auto
  moreover
  {
    assume eq: "aff_dim S1 = aff_dim S2"
    then have "S1 ≠ {}"
      using aff_dim_empty[of S1] aff_dim_empty[of S2] ‹S2 ≠ {}› by auto
    have **: "affine hull S1 = affine hull S2"
       apply (rule affine_dim_equal)
       using * affine_affine_hull
       apply auto
       using ‹S1 ≠ {}› hull_subset[of S1]
       apply auto
       using eq aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2]
       apply auto
       done
    obtain a where a: "a ∈ rel_interior S1"
      using ‹S1 ≠ {}› rel_interior_eq_empty assms by auto
    obtain T where T: "open T" "a ∈ T ∩ S1" "T ∩ affine hull S1 ⊆ S1"
       using mem_rel_interior[of a S1] a by auto
    then have "a ∈ T ∩ closure S2"
      using a assms unfolding rel_frontier_def by auto
    then obtain b where b: "b ∈ T ∩ rel_interior S2"
      using open_inter_closure_rel_interior[of S2 T] assms T by auto
    then have "b ∈ affine hull S1"
      using rel_interior_subset hull_subset[of S2] ** by auto
    then have "b ∈ S1"
      using T b by auto
    then have False
      using b assms unfolding rel_frontier_def by auto
  }
  ultimately show ?thesis
    using less_le by auto
qed

lemma convex_rel_interior_if:
  fixes S ::  "'n::euclidean_space set"
  assumes "convex S"
    and "z ∈ rel_interior S"
  shows "∀x∈affine hull S. ∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e) *R x + e *R z ∈ S)"
proof -
  obtain e1 where e1: "e1 > 0 ∧ cball z e1 ∩ affine hull S ⊆ S"
    using mem_rel_interior_cball[of z S] assms by auto
  {
    fix x
    assume x: "x ∈ affine hull S"
    {
      assume "x ≠ z"
      define m where "m = 1 + e1/norm(x-z)"
      hence "m > 1" using e1 ‹x ≠ z› by auto
      {
        fix e
        assume e: "e > 1 ∧ e ≤ m"
        have "z ∈ affine hull S"
          using assms rel_interior_subset hull_subset[of S] by auto
        then have *: "(1 - e)*R x + e *R z ∈ affine hull S"
          using mem_affine[of "affine hull S" x z "(1-e)" e] affine_affine_hull[of S] x
          by auto
        have "norm (z + e *R x - (x + e *R z)) = norm ((e - 1) *R (x - z))"
          by (simp add: algebra_simps)
        also have "… = (e - 1) * norm (x-z)"
          using norm_scaleR e by auto
        also have "… ≤ (m - 1) * norm (x - z)"
          using e mult_right_mono[of _ _ "norm(x-z)"] by auto
        also have "… = (e1 / norm (x - z)) * norm (x - z)"
          using m_def by auto
        also have "… = e1"
          using ‹x ≠ z› e1 by simp
        finally have **: "norm (z + e *R x - (x + e *R z)) ≤ e1"
          by auto
        have "(1 - e)*R x+ e *R z ∈ cball z e1"
          using m_def **
          unfolding cball_def dist_norm
          by (auto simp add: algebra_simps)
        then have "(1 - e) *R x+ e *R z ∈ S"
          using e * e1 by auto
      }
      then have "∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e) *R x + e *R z ∈ S )"
        using ‹m> 1 › by auto
    }
    moreover
    {
      assume "x = z"
      define m where "m = 1 + e1"
      then have "m > 1"
        using e1 by auto
      {
        fix e
        assume e: "e > 1 ∧ e ≤ m"
        then have "(1 - e) *R x + e *R z ∈ S"
          using e1 x ‹x = z› by (auto simp add: algebra_simps)
        then have "(1 - e) *R x + e *R z ∈ S"
          using e by auto
      }
      then have "∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e) *R x + e *R z ∈ S)"
        using ‹m > 1› by auto
    }
    ultimately have "∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e) *R x + e *R z ∈ S )"
      by blast
  }
  then show ?thesis by auto
qed

lemma convex_rel_interior_if2:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  assumes "z ∈ rel_interior S"
  shows "∀x∈affine hull S. ∃e. e > 1 ∧ (1 - e)*R x + e *R z ∈ S"
  using convex_rel_interior_if[of S z] assms by auto

lemma convex_rel_interior_only_if:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
    and "S ≠ {}"
  assumes "∀x∈S. ∃e. e > 1 ∧ (1 - e) *R x + e *R z ∈ S"
  shows "z ∈ rel_interior S"
proof -
  obtain x where x: "x ∈ rel_interior S"
    using rel_interior_eq_empty assms by auto
  then have "x ∈ S"
    using rel_interior_subset by auto
  then obtain e where e: "e > 1 ∧ (1 - e) *R x + e *R z ∈ S"
    using assms by auto
  define y where [abs_def]: "y = (1 - e) *R x + e *R z"
  then have "y ∈ S" using e by auto
  define e1 where "e1 = 1/e"
  then have "0 < e1 ∧ e1 < 1" using e by auto
  then have "z  =y - (1 - e1) *R (y - x)"
    using e1_def y_def by (auto simp add: algebra_simps)
  then show ?thesis
    using rel_interior_convex_shrink[of S x y "1-e1"] ‹0 < e1 ∧ e1 < 1› ‹y ∈ S› x assms
    by auto
qed

lemma convex_rel_interior_iff:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
    and "S ≠ {}"
  shows "z ∈ rel_interior S ⟷ (∀x∈S. ∃e. e > 1 ∧ (1 - e) *R x + e *R z ∈ S)"
  using assms hull_subset[of S "affine"]
    convex_rel_interior_if[of S z] convex_rel_interior_only_if[of S z]
  by auto

lemma convex_rel_interior_iff2:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
    and "S ≠ {}"
  shows "z ∈ rel_interior S ⟷ (∀x∈affine hull S. ∃e. e > 1 ∧ (1 - e) *R x + e *R z ∈ S)"
  using assms hull_subset[of S] convex_rel_interior_if2[of S z] convex_rel_interior_only_if[of S z]
  by auto

lemma convex_interior_iff:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "z ∈ interior S ⟷ (∀x. ∃e. e > 0 ∧ z + e *R x ∈ S)"
proof (cases "aff_dim S = int DIM('n)")
  case False
  {
    assume "z ∈ interior S"
    then have False
      using False interior_rel_interior_gen[of S] by auto
  }
  moreover
  {
    assume r: "∀x. ∃e. e > 0 ∧ z + e *R x ∈ S"
    {
      fix x
      obtain e1 where e1: "e1 > 0 ∧ z + e1 *R (x - z) ∈ S"
        using r by auto
      obtain e2 where e2: "e2 > 0 ∧ z + e2 *R (z - x) ∈ S"
        using r by auto
      define x1 where [abs_def]: "x1 = z + e1 *R (x - z)"
      then have x1: "x1 ∈ affine hull S"
        using e1 hull_subset[of S] by auto
      define x2 where [abs_def]: "x2 = z + e2 *R (z - x)"
      then have x2: "x2 ∈ affine hull S"
        using e2 hull_subset[of S] by auto
      have *: "e1/(e1+e2) + e2/(e1+e2) = 1"
        using add_divide_distrib[of e1 e2 "e1+e2"] e1 e2 by simp
      then have "z = (e2/(e1+e2)) *R x1 + (e1/(e1+e2)) *R x2"
        using x1_def x2_def
        apply (auto simp add: algebra_simps)
        using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z]
        apply auto
        done
      then have z: "z ∈ affine hull S"
        using mem_affine[of "affine hull S" x1 x2 "e2/(e1+e2)" "e1/(e1+e2)"]
          x1 x2 affine_affine_hull[of S] *
        by auto
      have "x1 - x2 = (e1 + e2) *R (x - z)"
        using x1_def x2_def by (auto simp add: algebra_simps)
      then have "x = z+(1/(e1+e2)) *R (x1-x2)"
        using e1 e2 by simp
      then have "x ∈ affine hull S"
        using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"]
          x1 x2 z affine_affine_hull[of S]
        by auto
    }
    then have "affine hull S = UNIV"
      by auto
    then have "aff_dim S = int DIM('n)"
      using aff_dim_affine_hull[of S] by (simp add: aff_dim_UNIV)
    then have False
      using False by auto
  }
  ultimately show ?thesis by auto
next
  case True
  then have "S ≠ {}"
    using aff_dim_empty[of S] by auto
  have *: "affine hull S = UNIV"
    using True affine_hull_UNIV by auto
  {
    assume "z ∈ interior S"
    then have "z ∈ rel_interior S"
      using True interior_rel_interior_gen[of S] by auto
    then have **: "∀x. ∃e. e > 1 ∧ (1 - e) *R x + e *R z ∈ S"
      using convex_rel_interior_iff2[of S z] assms ‹S ≠ {}› * by auto
    fix x
    obtain e1 where e1: "e1 > 1" "(1 - e1) *R (z - x) + e1 *R z ∈ S"
      using **[rule_format, of "z-x"] by auto
    define e where [abs_def]: "e = e1 - 1"
    then have "(1 - e1) *R (z - x) + e1 *R z = z + e *R x"
      by (simp add: algebra_simps)
    then have "e > 0" "z + e *R x ∈ S"
      using e1 e_def by auto
    then have "∃e. e > 0 ∧ z + e *R x ∈ S"
      by auto
  }
  moreover
  {
    assume r: "∀x. ∃e. e > 0 ∧ z + e *R x ∈ S"
    {
      fix x
      obtain e1 where e1: "e1 > 0" "z + e1 *R (z - x) ∈ S"
        using r[rule_format, of "z-x"] by auto
      define e where "e = e1 + 1"
      then have "z + e1 *R (z - x) = (1 - e) *R x + e *R z"
        by (simp add: algebra_simps)
      then have "e > 1" "(1 - e)*R x + e *R z ∈ S"
        using e1 e_def by auto
      then have "∃e. e > 1 ∧ (1 - e) *R x + e *R z ∈ S" by auto
    }
    then have "z ∈ rel_interior S"
      using convex_rel_interior_iff2[of S z] assms ‹S ≠ {}› by auto
    then have "z ∈ interior S"
      using True interior_rel_interior_gen[of S] by auto
  }
  ultimately show ?thesis by auto
qed


subsubsection ‹Relative interior and closure under common operations›

lemma rel_interior_inter_aux: "⋂{rel_interior S |S. S : I} ⊆ ⋂I"
proof -
  {
    fix y
    assume "y ∈ ⋂{rel_interior S |S. S : I}"
    then have y: "∀S ∈ I. y ∈ rel_interior S"
      by auto
    {
      fix S
      assume "S ∈ I"
      then have "y ∈ S"
        using rel_interior_subset y by auto
    }
    then have "y ∈ ⋂I" by auto
  }
  then show ?thesis by auto
qed

lemma closure_Int: "closure (⋂I) ≤ ⋂{closure S |S. S ∈ I}"
proof -
  {
    fix y
    assume "y ∈ ⋂I"
    then have y: "∀S ∈ I. y ∈ S" by auto
    {
      fix S
      assume "S ∈ I"
      then have "y ∈ closure S"
        using closure_subset y by auto
    }
    then have "y ∈ ⋂{closure S |S. S ∈ I}"
      by auto
  }
  then have "⋂I ⊆ ⋂{closure S |S. S ∈ I}"
    by auto
  moreover have "closed (⋂{closure S |S. S ∈ I})"
    unfolding closed_Inter closed_closure by auto
  ultimately show ?thesis using closure_hull[of "⋂I"]
    hull_minimal[of "⋂I" "⋂{closure S |S. S ∈ I}" "closed"] by auto
qed

lemma convex_closure_rel_interior_inter:
  assumes "∀S∈I. convex (S :: 'n::euclidean_space set)"
    and "⋂{rel_interior S |S. S ∈ I} ≠ {}"
  shows "⋂{closure S |S. S ∈ I} ≤ closure (⋂{rel_interior S |S. S ∈ I})"
proof -
  obtain x where x: "∀S∈I. x ∈ rel_interior S"
    using assms by auto
  {
    fix y
    assume "y ∈ ⋂{closure S |S. S ∈ I}"
    then have y: "∀S ∈ I. y ∈ closure S"
      by auto
    {
      assume "y = x"
      then have "y ∈ closure (⋂{rel_interior S |S. S ∈ I})"
        using x closure_subset[of "⋂{rel_interior S |S. S ∈ I}"] by auto
    }
    moreover
    {
      assume "y ≠ x"
      { fix e :: real
        assume e: "e > 0"
        define e1 where "e1 = min 1 (e/norm (y - x))"
        then have e1: "e1 > 0" "e1 ≤ 1" "e1 * norm (y - x) ≤ e"
          using ‹y ≠ x› ‹e > 0› le_divide_eq[of e1 e "norm (y - x)"]
          by simp_all
        define z where "z = y - e1 *R (y - x)"
        {
          fix S
          assume "S ∈ I"
          then have "z ∈ rel_interior S"
            using rel_interior_closure_convex_shrink[of S x y e1] assms x y e1 z_def
            by auto
        }
        then have *: "z ∈ ⋂{rel_interior S |S. S ∈ I}"
          by auto
        have "∃z. z ∈ ⋂{rel_interior S |S. S ∈ I} ∧ z ≠ y ∧ dist z y ≤ e"
          apply (rule_tac x="z" in exI)
          using ‹y ≠ x› z_def * e1 e dist_norm[of z y]
          apply simp
          done
      }
      then have "y islimpt ⋂{rel_interior S |S. S ∈ I}"
        unfolding islimpt_approachable_le by blast
      then have "y ∈ closure (⋂{rel_interior S |S. S ∈ I})"
        unfolding closure_def by auto
    }
    ultimately have "y ∈ closure (⋂{rel_interior S |S. S ∈ I})"
      by auto
  }
  then show ?thesis by auto
qed

lemma convex_closure_inter:
  assumes "∀S∈I. convex (S :: 'n::euclidean_space set)"
    and "⋂{rel_interior S |S. S ∈ I} ≠ {}"
  shows "closure (⋂I) = ⋂{closure S |S. S ∈ I}"
proof -
  have "⋂{closure S |S. S ∈ I} ≤ closure (⋂{rel_interior S |S. S ∈ I})"
    using convex_closure_rel_interior_inter assms by auto
  moreover
  have "closure (⋂{rel_interior S |S. S ∈ I}) ≤ closure (⋂I)"
    using rel_interior_inter_aux closure_mono[of "⋂{rel_interior S |S. S ∈ I}" "⋂I"]
    by auto
  ultimately show ?thesis
    using closure_Int[of I] by auto
qed

lemma convex_inter_rel_interior_same_closure:
  assumes "∀S∈I. convex (S :: 'n::euclidean_space set)"
    and "⋂{rel_interior S |S. S ∈ I} ≠ {}"
  shows "closure (⋂{rel_interior S |S. S ∈ I}) = closure (⋂I)"
proof -
  have "⋂{closure S |S. S ∈ I} ≤ closure (⋂{rel_interior S |S. S ∈ I})"
    using convex_closure_rel_interior_inter assms by auto
  moreover
  have "closure (⋂{rel_interior S |S. S ∈ I}) ≤ closure (⋂I)"
    using rel_interior_inter_aux closure_mono[of "⋂{rel_interior S |S. S ∈ I}" "⋂I"]
    by auto
  ultimately show ?thesis
    using closure_Int[of I] by auto
qed

lemma convex_rel_interior_inter:
  assumes "∀S∈I. convex (S :: 'n::euclidean_space set)"
    and "⋂{rel_interior S |S. S ∈ I} ≠ {}"
  shows "rel_interior (⋂I) ⊆ ⋂{rel_interior S |S. S ∈ I}"
proof -
  have "convex (⋂I)"
    using assms convex_Inter by auto
  moreover
  have "convex (⋂{rel_interior S |S. S ∈ I})"
    apply (rule convex_Inter)
    using assms convex_rel_interior
    apply auto
    done
  ultimately
  have "rel_interior (⋂{rel_interior S |S. S ∈ I}) = rel_interior (⋂I)"
    using convex_inter_rel_interior_same_closure assms
      closure_eq_rel_interior_eq[of "⋂{rel_interior S |S. S ∈ I}" "⋂I"]
    by blast
  then show ?thesis
    using rel_interior_subset[of "⋂{rel_interior S |S. S ∈ I}"] by auto
qed

lemma convex_rel_interior_finite_inter:
  assumes "∀S∈I. convex (S :: 'n::euclidean_space set)"
    and "⋂{rel_interior S |S. S ∈ I} ≠ {}"
    and "finite I"
  shows "rel_interior (⋂I) = ⋂{rel_interior S |S. S ∈ I}"
proof -
  have "⋂I ≠ {}"
    using assms rel_interior_inter_aux[of I] by auto
  have "convex (⋂I)"
    using convex_Inter assms by auto
  show ?thesis
  proof (cases "I = {}")
    case True
    then show ?thesis
      using Inter_empty rel_interior_UNIV by auto
  next
    case False
    {
      fix z
      assume z: "z ∈ ⋂{rel_interior S |S. S ∈ I}"
      {
        fix x
        assume x: "x ∈ ⋂I"
        {
          fix S
          assume S: "S ∈ I"
          then have "z ∈ rel_interior S" "x ∈ S"
            using z x by auto
          then have "∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e)*R x + e *R z ∈ S)"
            using convex_rel_interior_if[of S z] S assms hull_subset[of S] by auto
        }
        then obtain mS where
          mS: "∀S∈I. mS S > 1 ∧ (∀e. e > 1 ∧ e ≤ mS S ⟶ (1 - e) *R x + e *R z ∈ S)" by metis
        define e where "e = Min (mS ` I)"
        then have "e ∈ mS ` I" using assms ‹I ≠ {}› by simp
        then have "e > 1" using mS by auto
        moreover have "∀S∈I. e ≤ mS S"
          using e_def assms by auto
        ultimately have "∃e > 1. (1 - e) *R x + e *R z ∈ ⋂I"
          using mS by auto
      }
      then have "z ∈ rel_interior (⋂I)"
        using convex_rel_interior_iff[of "⋂I" z] ‹⋂I ≠ {}› ‹convex (⋂I)› by auto
    }
    then show ?thesis
      using convex_rel_interior_inter[of I] assms by auto
  qed
qed

lemma convex_closure_inter_two:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "convex T"
  assumes "rel_interior S ∩ rel_interior T ≠ {}"
  shows "closure (S ∩ T) = closure S ∩ closure T"
  using convex_closure_inter[of "{S,T}"] assms by auto

lemma convex_rel_interior_inter_two:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "convex T"
    and "rel_interior S ∩ rel_interior T ≠ {}"
  shows "rel_interior (S ∩ T) = rel_interior S ∩ rel_interior T"
  using convex_rel_interior_finite_inter[of "{S,T}"] assms by auto

lemma convex_affine_closure_Int:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "affine T"
    and "rel_interior S ∩ T ≠ {}"
  shows "closure (S ∩ T) = closure S ∩ T"
proof -
  have "affine hull T = T"
    using assms by auto
  then have "rel_interior T = T"
    using rel_interior_affine_hull[of T] by metis
  moreover have "closure T = T"
    using assms affine_closed[of T] by auto
  ultimately show ?thesis
    using convex_closure_inter_two[of S T] assms affine_imp_convex by auto
qed

lemma connected_component_1_gen:
  fixes S :: "'a :: euclidean_space set"
  assumes "DIM('a) = 1"
  shows "connected_component S a b ⟷ closed_segment a b ⊆ S"
unfolding connected_component_def
by (metis (no_types, lifting) assms subsetD subsetI convex_contains_segment convex_segment(1)
            ends_in_segment connected_convex_1_gen)

lemma connected_component_1:
  fixes S :: "real set"
  shows "connected_component S a b ⟷ closed_segment a b ⊆ S"
by (simp add: connected_component_1_gen)

lemma convex_affine_rel_interior_Int:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "affine T"
    and "rel_interior S ∩ T ≠ {}"
  shows "rel_interior (S ∩ T) = rel_interior S ∩ T"
proof -
  have "affine hull T = T"
    using assms by auto
  then have "rel_interior T = T"
    using rel_interior_affine_hull[of T] by metis
  moreover have "closure T = T"
    using assms affine_closed[of T] by auto
  ultimately show ?thesis
    using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto
qed

lemma convex_affine_rel_frontier_Int:
   fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "affine T"
    and "interior S ∩ T ≠ {}"
  shows "rel_frontier(S ∩ T) = frontier S ∩ T"
using assms
apply (simp add: rel_frontier_def convex_affine_closure_Int frontier_def)
by (metis Diff_Int_distrib2 Int_emptyI convex_affine_closure_Int convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen)

lemma rel_interior_convex_Int_affine:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "affine T" "interior S ∩ T ≠ {}"
    shows "rel_interior(S ∩ T) = interior S ∩ T"
proof -
  obtain a where aS: "a ∈ interior S" and aT:"a ∈ T"
    using assms by force
  have "rel_interior S = interior S"
    by (metis (no_types) aS affine_hull_nonempty_interior equals0D rel_interior_interior)
  then show ?thesis
    by (metis (no_types) affine_imp_convex assms convex_rel_interior_inter_two hull_same rel_interior_affine_hull)
qed

lemma closure_convex_Int_affine:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "affine T" "rel_interior S ∩ T ≠ {}"
  shows "closure(S ∩ T) = closure S ∩ T"
proof
  have "closure (S ∩ T) ⊆ closure T"
    by (simp add: closure_mono)
  also have "... ⊆ T"
    by (simp add: affine_closed assms)
  finally show "closure(S ∩ T) ⊆ closure S ∩ T"
    by (simp add: closure_mono)
next
  obtain a where "a ∈ rel_interior S" "a ∈ T"
    using assms by auto
  then have ssT: "subspace ((λx. (-a)+x) ` T)" and "a ∈ S"
    using affine_diffs_subspace rel_interior_subset assms by blast+
  show "closure S ∩ T ⊆ closure (S ∩ T)"
  proof
    fix x  assume "x ∈ closure S ∩ T"
    show "x ∈ closure (S ∩ T)"
    proof (cases "x = a")
      case True
      then show ?thesis
        using ‹a ∈ S› ‹a ∈ T› closure_subset by fastforce
    next
      case False
      then have "x ∈ closure(open_segment a x)"
        by auto
      then show ?thesis
        using ‹x ∈ closure S ∩ T› assms convex_affine_closure_Int by blast
    qed
  qed
qed

lemma subset_rel_interior_convex:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "convex T"
    and "S ≤ closure T"
    and "¬ S ⊆ rel_frontier T"
  shows "rel_interior S ⊆ rel_interior T"
proof -
  have *: "S ∩ closure T = S"
    using assms by auto
  have "¬ rel_interior S ⊆ rel_frontier T"
    using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
      closure_closed[of S] convex_closure_rel_interior[of S] closure_subset[of S] assms
    by auto
  then have "rel_interior S ∩ rel_interior (closure T) ≠ {}"
    using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T]
    by auto
  then have "rel_interior S ∩ rel_interior T = rel_interior (S ∩ closure T)"
    using assms convex_closure convex_rel_interior_inter_two[of S "closure T"]
      convex_rel_interior_closure[of T]
    by auto
  also have "… = rel_interior S"
    using * by auto
  finally show ?thesis
    by auto
qed

lemma rel_interior_convex_linear_image:
  fixes f :: "'m::euclidean_space ⇒ 'n::euclidean_space"
  assumes "linear f"
    and "convex S"
  shows "f ` (rel_interior S) = rel_interior (f ` S)"
proof (cases "S = {}")
  case True
  then show ?thesis
    using assms rel_interior_empty rel_interior_eq_empty by auto
next
  case False
  have *: "f ` (rel_interior S) ⊆ f ` S"
    unfolding image_mono using rel_interior_subset by auto
  have "f ` S ⊆ f ` (closure S)"
    unfolding image_mono using closure_subset by auto
  also have "… = f ` (closure (rel_interior S))"
    using convex_closure_rel_interior assms by auto
  also have "… ⊆ closure (f ` (rel_interior S))"
    using closure_linear_image_subset assms by auto
  finally have "closure (f ` S) = closure (f ` rel_interior S)"
    using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
      closure_mono[of "f ` rel_interior S" "f ` S"] *
    by auto
  then have "rel_interior (f ` S) = rel_interior (f ` rel_interior S)"
    using assms convex_rel_interior
      linear_conv_bounded_linear[of f] convex_linear_image[of _ S]
      convex_linear_image[of _ "rel_interior S"]
      closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"]
    by auto
  then have "rel_interior (f ` S) ⊆ f ` rel_interior S"
    using rel_interior_subset by auto
  moreover
  {
    fix z
    assume "z ∈ f ` rel_interior S"
    then obtain z1 where z1: "z1 ∈ rel_interior S" "f z1 = z" by auto
    {
      fix x
      assume "x ∈ f ` S"
      then obtain x1 where x1: "x1 ∈ S" "f x1 = x" by auto
      then obtain e where e: "e > 1" "(1 - e) *R x1 + e *R z1 : S"
        using convex_rel_interior_iff[of S z1] ‹convex S› x1 z1 by auto
      moreover have "f ((1 - e) *R x1 + e *R z1) = (1 - e) *R x + e *R z"
        using x1 z1 ‹linear f› by (simp add: linear_add_cmul)
      ultimately have "(1 - e) *R x + e *R z : f ` S"
        using imageI[of "(1 - e) *R x1 + e *R z1" S f] by auto
      then have "∃e. e > 1 ∧ (1 - e) *R x + e *R z : f ` S"
        using e by auto
    }
    then have "z ∈ rel_interior (f ` S)"
      using convex_rel_interior_iff[of "f ` S" z] ‹convex S›
        ‹linear f› ‹S ≠ {}› convex_linear_image[of f S]  linear_conv_bounded_linear[of f]
      by auto
  }
  ultimately show ?thesis by auto
qed

lemma rel_interior_convex_linear_preimage:
  fixes f :: "'m::euclidean_space ⇒ 'n::euclidean_space"
  assumes "linear f"
    and "convex S"
    and "f -` (rel_interior S) ≠ {}"
  shows "rel_interior (f -` S) = f -` (rel_interior S)"
proof -
  have "S ≠ {}"
    using assms rel_interior_empty by auto
  have nonemp: "f -` S ≠ {}"
    by (metis assms(3) rel_interior_subset subset_empty vimage_mono)
  then have "S ∩ (range f) ≠ {}"
    by auto
  have conv: "convex (f -` S)"
    using convex_linear_vimage assms by auto
  then have "convex (S ∩ range f)"
    by (metis assms(1) assms(2) convex_Int subspace_UNIV subspace_imp_convex subspace_linear_image)
  {
    fix z
    assume "z ∈ f -` (rel_interior S)"
    then have z: "f z : rel_interior S"
      by auto
    {
      fix x
      assume "x ∈ f -` S"
      then have "f x ∈ S" by auto
      then obtain e where e: "e > 1" "(1 - e) *R f x + e *R f z ∈ S"
        using convex_rel_interior_iff[of S "f z"] z assms ‹S ≠ {}› by auto
      moreover have "(1 - e) *R f x + e *R f z = f ((1 - e) *R x + e *R z)"
        using ‹linear f› by (simp add: linear_iff)
      ultimately have "∃e. e > 1 ∧ (1 - e) *R x + e *R z ∈ f -` S"
        using e by auto
    }
    then have "z ∈ rel_interior (f -` S)"
      using convex_rel_interior_iff[of "f -` S" z] conv nonemp by auto
  }
  moreover
  {
    fix z
    assume z: "z ∈ rel_interior (f -` S)"
    {
      fix x
      assume "x ∈ S ∩ range f"
      then obtain y where y: "f y = x" "y ∈ f -` S" by auto
      then obtain e where e: "e > 1" "(1 - e) *R y + e *R z ∈ f -` S"
        using convex_rel_interior_iff[of "f -` S" z] z conv by auto
      moreover have "(1 - e) *R x + e *R f z = f ((1 - e) *R y + e *R z)"
        using ‹linear f› y by (simp add: linear_iff)
      ultimately have "∃e. e > 1 ∧ (1 - e) *R x + e *R f z ∈ S ∩ range f"
        using e by auto
    }
    then have "f z ∈ rel_interior (S ∩ range f)"
      using ‹convex (S ∩ (range f))› ‹S ∩ range f ≠ {}›
        convex_rel_interior_iff[of "S ∩ (range f)" "f z"]
      by auto
    moreover have "affine (range f)"
      by (metis assms(1) subspace_UNIV subspace_imp_affine subspace_linear_image)
    ultimately have "f z ∈ rel_interior S"
      using convex_affine_rel_interior_Int[of S "range f"] assms by auto
    then have "z ∈ f -` (rel_interior S)"
      by auto
  }
  ultimately show ?thesis by auto
qed

lemma rel_interior_Times:
  fixes S :: "'n::euclidean_space set"
    and T :: "'m::euclidean_space set"
  assumes "convex S"
    and "convex T"
  shows "rel_interior (S × T) = rel_interior S × rel_interior T"
proof -
  { assume "S = {}"
    then have ?thesis
      by auto
  }
  moreover
  { assume "T = {}"
    then have ?thesis
       by auto
  }
  moreover
  {
    assume "S ≠ {}" "T ≠ {}"
    then have ri: "rel_interior S ≠ {}" "rel_interior T ≠ {}"
      using rel_interior_eq_empty assms by auto
    then have "fst -` rel_interior S ≠ {}"
      using fst_vimage_eq_Times[of "rel_interior S"] by auto
    then have "rel_interior ((fst :: 'n * 'm ⇒ 'n) -` S) = fst -` rel_interior S"
      using fst_linear ‹convex S› rel_interior_convex_linear_preimage[of fst S] by auto
    then have s: "rel_interior (S × (UNIV :: 'm set)) = rel_interior S × UNIV"
      by (simp add: fst_vimage_eq_Times)
    from ri have "snd -` rel_interior T ≠ {}"
      using snd_vimage_eq_Times[of "rel_interior T"] by auto
    then have "rel_interior ((snd :: 'n * 'm ⇒ 'm) -` T) = snd -` rel_interior T"
      using snd_linear ‹convex T› rel_interior_convex_linear_preimage[of snd T] by auto
    then have t: "rel_interior ((UNIV :: 'n set) × T) = UNIV × rel_interior T"
      by (simp add: snd_vimage_eq_Times)
    from s t have *: "rel_interior (S × (UNIV :: 'm set)) ∩ rel_interior ((UNIV :: 'n set) × T) =
      rel_interior S × rel_interior T" by auto
    have "S × T = S × (UNIV :: 'm set) ∩ (UNIV :: 'n set) × T"
      by auto
    then have "rel_interior (S × T) = rel_interior ((S × (UNIV :: 'm set)) ∩ ((UNIV :: 'n set) × T))"
      by auto
    also have "… = rel_interior (S × (UNIV :: 'm set)) ∩ rel_interior ((UNIV :: 'n set) × T)"
       apply (subst convex_rel_interior_inter_two[of "S × (UNIV :: 'm set)" "(UNIV :: 'n set) × T"])
       using * ri assms convex_Times
       apply auto
       done
    finally have ?thesis using * by auto
  }
  ultimately show ?thesis by blast
qed

lemma rel_interior_scaleR:
  fixes S :: "'n::euclidean_space set"
  assumes "c ≠ 0"
  shows "(op *R c) ` (rel_interior S) = rel_interior ((op *R c) ` S)"
  using rel_interior_injective_linear_image[of "(op *R c)" S]
    linear_conv_bounded_linear[of "op *R c"] linear_scaleR injective_scaleR[of c] assms
  by auto

lemma rel_interior_convex_scaleR:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "(op *R c) ` (rel_interior S) = rel_interior ((op *R c) ` S)"
  by (metis assms linear_scaleR rel_interior_convex_linear_image)

lemma convex_rel_open_scaleR:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
    and "rel_open S"
  shows "convex ((op *R c) ` S) ∧ rel_open ((op *R c) ` S)"
  by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)

lemma convex_rel_open_finite_inter:
  assumes "∀S∈I. convex (S :: 'n::euclidean_space set) ∧ rel_open S"
    and "finite I"
  shows "convex (⋂I) ∧ rel_open (⋂I)"
proof (cases "⋂{rel_interior S |S. S ∈ I} = {}")
  case True
  then have "⋂I = {}"
    using assms unfolding rel_open_def by auto
  then show ?thesis
    unfolding rel_open_def using rel_interior_empty by auto
next
  case False
  then have "rel_open (⋂I)"
    using assms unfolding rel_open_def
    using convex_rel_interior_finite_inter[of I]
    by auto
  then show ?thesis
    using convex_Inter assms by auto
qed

lemma convex_rel_open_linear_image:
  fixes f :: "'m::euclidean_space ⇒ 'n::euclidean_space"
  assumes "linear f"
    and "convex S"
    and "rel_open S"
  shows "convex (f ` S) ∧ rel_open (f ` S)"
  by (metis assms convex_linear_image rel_interior_convex_linear_image rel_open_def)

lemma convex_rel_open_linear_preimage:
  fixes f :: "'m::euclidean_space ⇒ 'n::euclidean_space"
  assumes "linear f"
    and "convex S"
    and "rel_open S"
  shows "convex (f -` S) ∧ rel_open (f -` S)"
proof (cases "f -` (rel_interior S) = {}")
  case True
  then have "f -` S = {}"
    using assms unfolding rel_open_def by auto
  then show ?thesis
    unfolding rel_open_def using rel_interior_empty by auto
next
  case False
  then have "rel_open (f -` S)"
    using assms unfolding rel_open_def
    using rel_interior_convex_linear_preimage[of f S]
    by auto
  then show ?thesis
    using convex_linear_vimage assms
    by auto
qed

lemma rel_interior_projection:
  fixes S :: "('m::euclidean_space × 'n::euclidean_space) set"
    and f :: "'m::euclidean_space ⇒ 'n::euclidean_space set"
  assumes "convex S"
    and "f = (λy. {z. (y, z) ∈ S})"
  shows "(y, z) ∈ rel_interior S ⟷ (y ∈ rel_interior {y. (f y ≠ {})} ∧ z ∈ rel_interior (f y))"
proof -
  {
    fix y
    assume "y ∈ {y. f y ≠ {}}"
    then obtain z where "(y, z) ∈ S"
      using assms by auto
    then have "∃x. x ∈ S ∧ y = fst x"
      apply (rule_tac x="(y, z)" in exI)
      apply auto
      done
    then obtain x where "x ∈ S" "y = fst x"
      by blast
    then have "y ∈ fst ` S"
      unfolding image_def by auto
  }
  then have "fst ` S = {y. f y ≠ {}}"
    unfolding fst_def using assms by auto
  then have h1: "fst ` rel_interior S = rel_interior {y. f y ≠ {}}"
    using rel_interior_convex_linear_image[of fst S] assms fst_linear by auto
  {
    fix y
    assume "y ∈ rel_interior {y. f y ≠ {}}"
    then have "y ∈ fst ` rel_interior S"
      using h1 by auto
    then have *: "rel_interior S ∩ fst -` {y} ≠ {}"
      by auto
    moreover have aff: "affine (fst -` {y})"
      unfolding affine_alt by (simp add: algebra_simps)
    ultimately have **: "rel_interior (S ∩ fst -` {y}) = rel_interior S ∩ fst -` {y}"
      using convex_affine_rel_interior_Int[of S "fst -` {y}"] assms by auto
    have conv: "convex (S ∩ fst -` {y})"
      using convex_Int assms aff affine_imp_convex by auto
    {
      fix x
      assume "x ∈ f y"
      then have "(y, x) ∈ S ∩ (fst -` {y})"
        using assms by auto
      moreover have "x = snd (y, x)" by auto
      ultimately have "x ∈ snd ` (S ∩ fst -` {y})"
        by blast
    }
    then have "snd ` (S ∩ fst -` {y}) = f y"
      using assms by auto
    then have ***: "rel_interior (f y) = snd ` rel_interior (S ∩ fst -` {y})"
      using rel_interior_convex_linear_image[of snd "S ∩ fst -` {y}"] snd_linear conv
      by auto
    {
      fix z
      assume "z ∈ rel_interior (f y)"
      then have "z ∈ snd ` rel_interior (S ∩ fst -` {y})"
        using *** by auto
      moreover have "{y} = fst ` rel_interior (S ∩ fst -` {y})"
        using * ** rel_interior_subset by auto
      ultimately have "(y, z) ∈ rel_interior (S ∩ fst -` {y})"
        by force
      then have "(y,z) ∈ rel_interior S"
        using ** by auto
    }
    moreover
    {
      fix z
      assume "(y, z) ∈ rel_interior S"
      then have "(y, z) ∈ rel_interior (S ∩ fst -` {y})"
        using ** by auto
      then have "z ∈ snd ` rel_interior (S ∩ fst -` {y})"
        by (metis Range_iff snd_eq_Range)
      then have "z ∈ rel_interior (f y)"
        using *** by auto
    }
    ultimately have "⋀z. (y, z) ∈ rel_interior S ⟷ z ∈ rel_interior (f y)"
      by auto
  }
  then have h2: "⋀y z. y ∈ rel_interior {t. f t ≠ {}} ⟹
    (y, z) ∈ rel_interior S ⟷ z ∈ rel_interior (f y)"
    by auto
  {
    fix y z
    assume asm: "(y, z) ∈ rel_interior S"
    then have "y ∈ fst ` rel_interior S"
      by (metis Domain_iff fst_eq_Domain)
    then have "y ∈ rel_interior {t. f t ≠ {}}"
      using h1 by auto
    then have "y ∈ rel_interior {t. f t ≠ {}}" and "(z : rel_interior (f y))"
      using h2 asm by auto
  }
  then show ?thesis using h2 by blast
qed

lemma rel_frontier_Times:
  fixes S :: "'n::euclidean_space set"
    and T :: "'m::euclidean_space set"
  assumes "convex S"
    and "convex T"
  shows "rel_frontier S × rel_frontier T ⊆ rel_frontier (S × T)"
    by (force simp: rel_frontier_def rel_interior_Times assms closure_Times)


subsubsection ‹Relative interior of convex cone›

lemma cone_rel_interior:
  fixes S :: "'m::euclidean_space set"
  assumes "cone S"
  shows "cone ({0} ∪ rel_interior S)"
proof (cases "S = {}")
  case True
  then show ?thesis
    by (simp add: rel_interior_empty cone_0)
next
  case False
  then have *: "0 ∈ S ∧ (∀c. c > 0 ⟶ op *R c ` S = S)"
    using cone_iff[of S] assms by auto
  then have *: "0 ∈ ({0} ∪ rel_interior S)"
    and "∀c. c > 0 ⟶ op *R c ` ({0} ∪ rel_interior S) = ({0} ∪ rel_interior S)"
    by (auto simp add: rel_interior_scaleR)
  then show ?thesis
    using cone_iff[of "{0} ∪ rel_interior S"] by auto
qed

lemma rel_interior_convex_cone_aux:
  fixes S :: "'m::euclidean_space set"
  assumes "convex S"
  shows "(c, x) ∈ rel_interior (cone hull ({(1 :: real)} × S)) ⟷
    c > 0 ∧ x ∈ ((op *R c) ` (rel_interior S))"
proof (cases "S = {}")
  case True
  then show ?thesis
    by (simp add: rel_interior_empty cone_hull_empty)
next
  case False
  then obtain s where "s ∈ S" by auto
  have conv: "convex ({(1 :: real)} × S)"
    using convex_Times[of "{(1 :: real)}" S] assms convex_singleton[of "1 :: real"]
    by auto
  define f where "f y = {z. (y, z) ∈ cone hull ({1 :: real} × S)}" for y
  then have *: "(c, x) ∈ rel_interior (cone hull ({(1 :: real)} × S)) =
    (c ∈ rel_interior {y. f y ≠ {}} ∧ x ∈ rel_interior (f c))"
    apply (subst rel_interior_projection[of "cone hull ({(1 :: real)} × S)" f c x])
    using convex_cone_hull[of "{(1 :: real)} × S"] conv
    apply auto
    done
  {
    fix y :: real
    assume "y ≥ 0"
    then have "y *R (1,s) ∈ cone hull ({1 :: real} × S)"
      using cone_hull_expl[of "{(1 :: real)} × S"] ‹s ∈ S› by auto
    then have "f y ≠ {}"
      using f_def by auto
  }
  then have "{y. f y ≠ {}} = {0..}"
    using f_def cone_hull_expl[of "{1 :: real} × S"] by auto
  then have **: "rel_interior {y. f y ≠ {}} = {0<..}"
    using rel_interior_real_semiline by auto
  {
    fix c :: real
    assume "c > 0"
    then have "f c = (op *R c ` S)"
      using f_def cone_hull_expl[of "{1 :: real} × S"] by auto
    then have "rel_interior (f c) = op *R c ` rel_interior S"
      using rel_interior_convex_scaleR[of S c] assms by auto
  }
  then show ?thesis using * ** by auto
qed

lemma rel_interior_convex_cone:
  fixes S :: "'m::euclidean_space set"
  assumes "convex S"
  shows "rel_interior (cone hull ({1 :: real} × S)) =
    {(c, c *R x) | c x. c > 0 ∧ x ∈ rel_interior S}"
  (is "?lhs = ?rhs")
proof -
  {
    fix z
    assume "z ∈ ?lhs"
    have *: "z = (fst z, snd z)"
      by auto
    have "z ∈ ?rhs"
      using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms ‹z ∈ ?lhs›
      apply auto
      apply (rule_tac x = "fst z" in exI)
      apply (rule_tac x = x in exI)
      using *
      apply auto
      done
  }
  moreover
  {
    fix z
    assume "z ∈ ?rhs"
    then have "z ∈ ?lhs"
      using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms
      by auto
  }
  ultimately show ?thesis by blast
qed

lemma convex_hull_finite_union:
  assumes "finite I"
  assumes "∀i∈I. convex (S i) ∧ (S i) ≠ {}"
  shows "convex hull (⋃(S ` I)) =
    {sum (λi. c i *R s i) I | c s. (∀i∈I. c i ≥ 0) ∧ sum c I = 1 ∧ (∀i∈I. s i ∈ S i)}"
  (is "?lhs = ?rhs")
proof -
  have "?lhs ⊇ ?rhs"
  proof
    fix x
    assume "x : ?rhs"
    then obtain c s where *: "sum (λi. c i *R s i) I = x" "sum c I = 1"
      "(∀i∈I. c i ≥ 0) ∧ (∀i∈I. s i ∈ S i)" by auto
    then have "∀i∈I. s i ∈ convex hull (⋃(S ` I))"
      using hull_subset[of "⋃(S ` I)" convex] by auto
    then show "x ∈ ?lhs"
      unfolding *(1)[symmetric]
      apply (subst convex_sum[of I "convex hull ⋃(S ` I)" c s])
      using * assms convex_convex_hull
      apply auto
      done
  qed

  {
    fix i
    assume "i ∈ I"
    with assms have "∃p. p ∈ S i" by auto
  }
  then obtain p where p: "∀i∈I. p i ∈ S i" by metis

  {
    fix i
    assume "i ∈ I"
    {
      fix x
      assume "x ∈ S i"
      define c where "c j = (if j = i then 1::real else 0)" for j
      then have *: "sum c I = 1"
        using ‹finite I› ‹i ∈ I› sum.delta[of I i "λj::'a. 1::real"]
        by auto
      define s where "s j = (if j = i then x else p j)" for j
      then have "∀j. c j *R s j = (if j = i then x else 0)"
        using c_def by (auto simp add: algebra_simps)
      then have "x = sum (λi. c i *R s i) I"
        using s_def c_def ‹finite I› ‹i ∈ I› sum.delta[of I i "λj::'a. x"]
        by auto
      then have "x ∈ ?rhs"
        apply auto
        apply (rule_tac x = c in exI)
        apply (rule_tac x = s in exI)
        using * c_def s_def p ‹x ∈ S i›
        apply auto
        done
    }
    then have "?rhs ⊇ S i" by auto
  }
  then have *: "?rhs ⊇ ⋃(S ` I)" by auto

  {
    fix u v :: real
    assume uv: "u ≥ 0 ∧ v ≥ 0 ∧ u + v = 1"
    fix x y
    assume xy: "x ∈ ?rhs ∧ y ∈ ?rhs"
    from xy obtain c s where
      xc: "x = sum (λi. c i *R s i) I ∧ (∀i∈I. c i ≥ 0) ∧ sum c I = 1 ∧ (∀i∈I. s i ∈ S i)"
      by auto
    from xy obtain d t where
      yc: "y = sum (λi. d i *R t i) I ∧ (∀i∈I. d i ≥ 0) ∧ sum d I = 1 ∧ (∀i∈I. t i ∈ S i)"
      by auto
    define e where "e i = u * c i + v * d i" for i
    have ge0: "∀i∈I. e i ≥ 0"
      using e_def xc yc uv by simp
    have "sum (λi. u * c i) I = u * sum c I"
      by (simp add: sum_distrib_left)
    moreover have "sum (λi. v * d i) I = v * sum d I"
      by (simp add: sum_distrib_left)
    ultimately have sum1: "sum e I = 1"
      using e_def xc yc uv by (simp add: sum.distrib)
    define q where "q i = (if e i = 0 then p i else (u * c i / e i) *R s i + (v * d i / e i) *R t i)"
      for i
    {
      fix i
      assume i: "i ∈ I"
      have "q i ∈ S i"
      proof (cases "e i = 0")
        case True
        then show ?thesis using i p q_def by auto
      next
        case False
        then show ?thesis
          using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"]
            mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"]
            assms q_def e_def i False xc yc uv
          by (auto simp del: mult_nonneg_nonneg)
      qed
    }
    then have qs: "∀i∈I. q i ∈ S i" by auto
    {
      fix i
      assume i: "i ∈ I"
      have "(u * c i) *R s i + (v * d i) *R t i = e i *R q i"
      proof (cases "e i = 0")
        case True
        have ge: "u * (c i) ≥ 0 ∧ v * d i ≥ 0"
          using xc yc uv i by simp
        moreover from ge have "u * c i ≤ 0 ∧ v * d i ≤ 0"
          using True e_def i by simp
        ultimately have "u * c i = 0 ∧ v * d i = 0" by auto
        with True show ?thesis by auto
      next
        case False
        then have "(u * (c i)/(e i))*R (s i)+(v * (d i)/(e i))*R (t i) = q i"
          using q_def by auto
        then have "e i *R ((u * (c i)/(e i))*R (s i)+(v * (d i)/(e i))*R (t i))
               = (e i) *R (q i)" by auto
        with False show ?thesis by (simp add: algebra_simps)
      qed
    }
    then have *: "∀i∈I. (u * c i) *R s i + (v * d i) *R t i = e i *R q i"
      by auto
    have "u *R x + v *R y = sum (λi. (u * c i) *R s i + (v * d i) *R t i) I"
      using xc yc by (simp add: algebra_simps scaleR_right.sum sum.distrib)
    also have "… = sum (λi. e i *R q i) I"
      using * by auto
    finally have "u *R x + v *R y = sum (λi. (e i) *R (q i)) I"
      by auto
    then have "u *R x + v *R y ∈ ?rhs"
      using ge0 sum1 qs by auto
  }
  then have "convex ?rhs" unfolding convex_def by auto
  then show ?thesis
    using ‹?lhs ⊇ ?rhs› * hull_minimal[of "⋃(S ` I)" ?rhs convex]
    by blast
qed

lemma convex_hull_union_two:
  fixes S T :: "'m::euclidean_space set"
  assumes "convex S"
    and "S ≠ {}"
    and "convex T"
    and "T ≠ {}"
  shows "convex hull (S ∪ T) =
    {u *R s + v *R t | u v s t. u ≥ 0 ∧ v ≥ 0 ∧ u + v = 1 ∧ s ∈ S ∧ t ∈ T}"
  (is "?lhs = ?rhs")
proof
  define I :: "nat set" where "I = {1, 2}"
  define s where "s i = (if i = (1::nat) then S else T)" for i
  have "⋃(s ` I) = S ∪ T"
    using s_def I_def by auto
  then have "convex hull (⋃(s ` I)) = convex hull (S ∪ T)"
    by auto
  moreover have "convex hull ⋃(s ` I) =
    {∑ i∈I. c i *R sa i | c sa. (∀i∈I. 0 ≤ c i) ∧ sum c I = 1 ∧ (∀i∈I. sa i ∈ s i)}"
      apply (subst convex_hull_finite_union[of I s])
      using assms s_def I_def
      apply auto
      done
  moreover have
    "{∑i∈I. c i *R sa i | c sa. (∀i∈I. 0 ≤ c i) ∧ sum c I = 1 ∧ (∀i∈I. sa i ∈ s i)} ≤ ?rhs"
    using s_def I_def by auto
  ultimately show "?lhs ⊆ ?rhs" by auto
  {
    fix x
    assume "x ∈ ?rhs"
    then obtain u v s t where *: "x = u *R s + v *R t ∧ u ≥ 0 ∧ v ≥ 0 ∧ u + v = 1 ∧ s ∈ S ∧ t ∈ T"
      by auto
    then have "x ∈ convex hull {s, t}"
      using convex_hull_2[of s t] by auto
    then have "x ∈ convex hull (S ∪ T)"
      using * hull_mono[of "{s, t}" "S ∪ T"] by auto
  }
  then show "?lhs ⊇ ?rhs" by blast
qed


subsection ‹Convexity on direct sums›

lemma closure_sum:
  fixes S T :: "'a::real_normed_vector set"
  shows "closure S + closure T ⊆ closure (S + T)"
  unfolding set_plus_image closure_Times [symmetric] split_def
  by (intro closure_bounded_linear_image_subset bounded_linear_add
    bounded_linear_fst bounded_linear_snd)

lemma rel_interior_sum:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "convex T"
  shows "rel_interior (S + T) = rel_interior S + rel_interior T"
proof -
  have "rel_interior S + rel_interior T = (λ(x,y). x + y) ` (rel_interior S × rel_interior T)"
    by (simp add: set_plus_image)
  also have "… = (λ(x,y). x + y) ` rel_interior (S × T)"
    using rel_interior_Times assms by auto
  also have "… = rel_interior (S + T)"
    using fst_snd_linear convex_Times assms
      rel_interior_convex_linear_image[of "(λ(x,y). x + y)" "S × T"]
    by (auto simp add: set_plus_image)
  finally show ?thesis ..
qed

lemma rel_interior_sum_gen:
  fixes S :: "'a ⇒ 'n::euclidean_space set"
  assumes "∀i∈I. convex (S i)"
  shows "rel_interior (sum S I) = sum (λi. rel_interior (S i)) I"
  apply (subst sum_set_cond_linear[of convex])
  using rel_interior_sum rel_interior_sing[of "0"] assms
  apply (auto simp add: convex_set_plus)
  done

lemma convex_rel_open_direct_sum:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "rel_open S"
    and "convex T"
    and "rel_open T"
  shows "convex (S × T) ∧ rel_open (S × T)"
  by (metis assms convex_Times rel_interior_Times rel_open_def)

lemma convex_rel_open_sum:
  fixes S T :: "'n::euclidean_space set"
  assumes "convex S"
    and "rel_open S"
    and "convex T"
    and "rel_open T"
  shows "convex (S + T) ∧ rel_open (S + T)"
  by (metis assms convex_set_plus rel_interior_sum rel_open_def)

lemma convex_hull_finite_union_cones:
  assumes "finite I"
    and "I ≠ {}"
  assumes "∀i∈I. convex (S i) ∧ cone (S i) ∧ S i ≠ {}"
  shows "convex hull (⋃(S ` I)) = sum S I"
  (is "?lhs = ?rhs")
proof -
  {
    fix x
    assume "x ∈ ?lhs"
    then obtain c xs where
      x: "x = sum (λi. c i *R xs i) I ∧ (∀i∈I. c i ≥ 0) ∧ sum c I = 1 ∧ (∀i∈I. xs i ∈ S i)"
      using convex_hull_finite_union[of I S] assms by auto
    define s where "s i = c i *R xs i" for i
    {
      fix i
      assume "i ∈ I"
      then have "s i ∈ S i"
        using s_def x assms mem_cone[of "S i" "xs i" "c i"] by auto
    }
    then have "∀i∈I. s i ∈ S i" by auto
    moreover have "x = sum s I" using x s_def by auto
    ultimately have "x ∈ ?rhs"
      using set_sum_alt[of I S] assms by auto
  }
  moreover
  {
    fix x
    assume "x ∈ ?rhs"
    then obtain s where x: "x = sum s I ∧ (∀i∈I. s i ∈ S i)"
      using set_sum_alt[of I S] assms by auto
    define xs where "xs i = of_nat(card I) *R s i" for i
    then have "x = sum (λi. ((1 :: real) / of_nat(card I)) *R xs i) I"
      using x assms by auto
    moreover have "∀i∈I. xs i ∈ S i"
      using x xs_def assms by (simp add: cone_def)
    moreover have "∀i∈I. (1 :: real) / of_nat (card I) ≥ 0"
      by auto
    moreover have "sum (λi. (1 :: real) / of_nat (card I)) I = 1"
      using assms by auto
    ultimately have "x ∈ ?lhs"
      apply (subst convex_hull_finite_union[of I S])
      using assms
      apply blast
      using assms
      apply blast
      apply rule
      apply (rule_tac x = "(λi. (1 :: real) / of_nat (card I))" in exI)
      apply auto
      done
  }
  ultimately show ?thesis by auto
qed

lemma convex_hull_union_cones_two:
  fixes S T :: "'m::euclidean_space set"
  assumes "convex S"
    and "cone S"
    and "S ≠ {}"
  assumes "convex T"
    and "cone T"
    and "T ≠ {}"
  shows "convex hull (S ∪ T) = S + T"
proof -
  define I :: "nat set" where "I = {1, 2}"
  define A where "A i = (if i = (1::nat) then S else T)" for i
  have "⋃(A ` I) = S ∪ T"
    using A_def I_def by auto
  then have "convex hull (⋃(A ` I)) = convex hull (S ∪ T)"
    by auto
  moreover have "convex hull ⋃(A ` I) = sum A I"
    apply (subst convex_hull_finite_union_cones[of I A])
    using assms A_def I_def
    apply auto
    done
  moreover have "sum A I = S + T"
    using A_def I_def
    unfolding set_plus_def
    apply auto
    unfolding set_plus_def
    apply auto
    done
  ultimately show ?thesis by auto
qed

lemma rel_interior_convex_hull_union:
  fixes S :: "'a ⇒ 'n::euclidean_space set"
  assumes "finite I"
    and "∀i∈I. convex (S i) ∧ S i ≠ {}"
  shows "rel_interior (convex hull (⋃(S ` I))) =
    {sum (λi. c i *R s i) I | c s. (∀i∈I. c i > 0) ∧ sum c I = 1 ∧
      (∀i∈I. s i ∈ rel_interior(S i))}"
  (is "?lhs = ?rhs")
proof (cases "I = {}")
  case True
  then show ?thesis
    using convex_hull_empty rel_interior_empty by auto
next
  case False
  define C0 where "C0 = convex hull (⋃(S ` I))"
  have "∀i∈I. C0 ≥ S i"
    unfolding C0_def using hull_subset[of "⋃(S ` I)"] by auto
  define K0 where "K0 = cone hull ({1 :: real} × C0)"
  define K where "K i = cone hull ({1 :: real} × S i)" for i
  have "∀i∈I. K i ≠ {}"
    unfolding K_def using assms
    by (simp add: cone_hull_empty_iff[symmetric])
  {
    fix i
    assume "i ∈ I"
    then have "convex (K i)"
      unfolding K_def
      apply (subst convex_cone_hull)
      apply (subst convex_Times)
      using assms
      apply auto
      done
  }
  then have convK: "∀i∈I. convex (K i)"
    by auto
  {
    fix i
    assume "i ∈ I"
    then have "K0 ⊇ K i"
      unfolding K0_def K_def
      apply (subst hull_mono)
      using ‹∀i∈I. C0 ≥ S i›
      apply auto
      done
  }
  then have "K0 ⊇ ⋃(K ` I)" by auto
  moreover have "convex K0"
    unfolding K0_def
    apply (subst convex_cone_hull)
    apply (subst convex_Times)
    unfolding C0_def
    using convex_convex_hull
    apply auto
    done
  ultimately have geq: "K0 ⊇ convex hull (⋃(K ` I))"
    using hull_minimal[of _ "K0" "convex"] by blast
  have "∀i∈I. K i ⊇ {1 :: real} × S i"
    using K_def by (simp add: hull_subset)
  then have "⋃(K ` I) ⊇ {1 :: real} × ⋃(S ` I)"
    by auto
  then have "convex hull ⋃(K ` I) ⊇ convex hull ({1 :: real} × ⋃(S ` I))"
    by (simp add: hull_mono)
  then have "convex hull ⋃(K ` I) ⊇ {1 :: real} × C0"
    unfolding C0_def
    using convex_hull_Times[of "{(1 :: real)}" "⋃(S ` I)"] convex_hull_singleton
    by auto
  moreover have "cone (convex hull (⋃(K ` I)))"
    apply (subst cone_convex_hull)
    using cone_Union[of "K ` I"]
    apply auto
    unfolding K_def
    using cone_cone_hull
    apply auto
    done
  ultimately have "convex hull (⋃(K ` I)) ⊇ K0"
    unfolding K0_def
    using hull_minimal[of _ "convex hull (⋃(K ` I))" "cone"]
    by blast
  then have "K0 = convex hull (⋃(K ` I))"
    using geq by auto
  also have "… = sum K I"
    apply (subst convex_hull_finite_union_cones[of I K])
    using assms
    apply blast
    using False
    apply blast
    unfolding K_def
    apply rule
    apply (subst convex_cone_hull)
    apply (subst convex_Times)
    using assms cone_cone_hull ‹∀i∈I. K i ≠ {}› K_def
    apply auto
    done
  finally have "K0 = sum K I" by auto
  then have *: "rel_interior K0 = sum (λi. (rel_interior (K i))) I"
    using rel_interior_sum_gen[of I K] convK by auto
  {
    fix x
    assume "x ∈ ?lhs"
    then have "(1::real, x) ∈ rel_interior K0"
      using K0_def C0_def rel_interior_convex_cone_aux[of C0 "1::real" x] convex_convex_hull
      by auto
    then obtain k where k: "(1::real, x) = sum k I ∧ (∀i∈I. k i ∈ rel_interior (K i))"
      using ‹finite I› * set_sum_alt[of I "λi. rel_interior (K i)"] by auto
    {
      fix i
      assume "i ∈ I"
      then have "convex (S i) ∧ k i ∈ rel_interior (cone hull {1} × S i)"
        using k K_def assms by auto
      then have "∃ci si. k i = (ci, ci *R si) ∧ 0 < ci ∧ si ∈ rel_interior (S i)"
        using rel_interior_convex_cone[of "S i"] by auto
    }
    then obtain c s where
      cs: "∀i∈I. k i = (c i, c i *R s i) ∧ 0 < c i ∧ s i ∈ rel_interior (S i)"
      by metis
    then have "x = (∑i∈I. c i *R s i) ∧ sum c I = 1"
      using k by (simp add: sum_prod)
    then have "x ∈ ?rhs"
      using k
      apply auto
      apply (rule_tac x = c in exI)
      apply (rule_tac x = s in exI)
      using cs
      apply auto
      done
  }
  moreover
  {
    fix x
    assume "x ∈ ?rhs"
    then obtain c s where cs: "x = sum (λi. c i *R s i) I ∧
        (∀i∈I. c i > 0) ∧ sum c I = 1 ∧ (∀i∈I. s i ∈ rel_interior (S i))"
      by auto
    define k where "k i = (c i, c i *R s i)" for i
    {
      fix i assume "i:I"
      then have "k i ∈ rel_interior (K i)"
        using k_def K_def assms cs rel_interior_convex_cone[of "S i"]
        by auto
    }
    then have "(1::real, x) ∈ rel_interior K0"
      using K0_def * set_sum_alt[of I "(λi. rel_interior (K i))"] assms k_def cs
      apply auto
      apply (rule_tac x = k in exI)
      apply (simp add: sum_prod)
      done
    then have "x ∈ ?lhs"
      using K0_def C0_def rel_interior_convex_cone_aux[of C0 1 x]
      by (auto simp add: convex_convex_hull)
  }
  ultimately show ?thesis by blast
qed


lemma convex_le_Inf_differential:
  fixes f :: "real ⇒ real"
  assumes "convex_on I f"
    and "x ∈ interior I"
    and "y ∈ I"
  shows "f y ≥ f x + Inf ((λt. (f x - f t) / (x - t)) ` ({x<..} ∩ I)) * (y - x)"
  (is "_ ≥ _ + Inf (?F x) * (y - x)")
proof (cases rule: linorder_cases)
  assume "x < y"
  moreover
  have "open (interior I)" by auto
  from openE[OF this ‹x ∈ interior I›]
  obtain e where e: "0 < e" "ball x e ⊆ interior I" .
  moreover define t where "t = min (x + e / 2) ((x + y) / 2)"
  ultimately have "x < t" "t < y" "t ∈ ball x e"
    by (auto simp: dist_real_def field_simps split: split_min)
  with ‹x ∈ interior I› e interior_subset[of I] have "t ∈ I" "x ∈ I" by auto

  have "open (interior I)" by auto
  from openE[OF this ‹x ∈ interior I›]
  obtain e where "0 < e" "ball x e ⊆ interior I" .
  moreover define K where "K = x - e / 2"
  with ‹0 < e› have "K ∈ ball x e" "K < x"
    by (auto simp: dist_real_def)
  ultimately have "K ∈ I" "K < x" "x ∈ I"
    using interior_subset[of I] ‹x ∈ interior I› by auto

  have "Inf (?F x) ≤ (f x - f y) / (x - y)"
  proof (intro bdd_belowI cInf_lower2)
    show "(f x - f t) / (x - t) ∈ ?F x"
      using ‹t ∈ I› ‹x < t› by auto
    show "(f x - f t) / (x - t) ≤ (f x - f y) / (x - y)"
      using ‹convex_on I f› ‹x ∈ I› ‹y ∈ I› ‹x < t› ‹t < y›
      by (rule convex_on_diff)
  next
    fix y
    assume "y ∈ ?F x"
    with order_trans[OF convex_on_diff[OF ‹convex_on I f› ‹K ∈ I› _ ‹K < x› _]]
    show "(f K - f x) / (K - x) ≤ y" by auto
  qed
  then show ?thesis
    using ‹x < y› by (simp add: field_simps)
next
  assume "y < x"
  moreover
  have "open (interior I)" by auto
  from openE[OF this ‹x ∈ interior I›]
  obtain e where e: "0 < e" "ball x e ⊆ interior I" .
  moreover define t where "t = x + e / 2"
  ultimately have "x < t" "t ∈ ball x e"
    by (auto simp: dist_real_def field_simps)
  with ‹x ∈ interior I› e interior_subset[of I] have "t ∈ I" "x ∈ I" by auto

  have "(f x - f y) / (x - y) ≤ Inf (?F x)"
  proof (rule cInf_greatest)
    have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
      using ‹y < x› by (auto simp: field_simps)
    also
    fix z
    assume "z ∈ ?F x"
    with order_trans[OF convex_on_diff[OF ‹convex_on I f› ‹y ∈ I› _ ‹y < x›]]
    have "(f y - f x) / (y - x) ≤ z"
      by auto
    finally show "(f x - f y) / (x - y) ≤ z" .
  ne