Quelle Starlike.thy Sprache: Isabelle

(* 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
*)
chapter \<open>Unsorted\<close>

theory Starlike
  imports
    Convex_Euclidean_Space
    Line_Segment
begin

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) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>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  \<Union>x \<in> 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)
  { 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 \<open>convex C\<close> \<open>T \<subseteq> C\<close> closure_subset contra_subsetD convex_hull_eq hull_mono)
    moreover have "x \ rel_interior C"
      by (meson \<open>x \<in> S\<close> dis disjnt_iff)
    moreover have "x \ open_segment z y \ {z, y}"
      using \<open>x \<in> closed_segment z y\<close> closed_segment_eq_open by blast
    ultimately have "x \ convex hull T"
      using rel_interior_closure_convex_segment [OF \<open>convex C\<close> z]
      using y z by blast
  }
  with * show "?lhs \ ?rhs"
    by (auto simp add: convex_hull_insert_segments)
  show "?rhs \ ?lhs"
    by (meson hull_mono inf_mono subset_insertI subset_refl)
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Shrinking towards the interior of a convex set\<close>

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 *\<^sub>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
  proof (intro exI subsetI conjI)
    fix y
    assume "y \ ball (x - e *\<^sub>R (x - c)) (e*d)"
    then have as: "dist (x - e *\<^sub>R (x - c)) y < e * d"
      by simp
    have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x"
      using \<open>e > 0\<close> by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
    have "c - ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = (1 / e) *\<^sub>R (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
      using \<open>e > 0\<close>
      by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
    then have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \1/e\ * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
      by (simp add: dist_norm)
    also have "\ = \1/e\ * norm (x - e *\<^sub>R (x - c) - y)"
      by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
    also have "\ < d"
      using as[unfolded dist_norm] and \<open>e > 0\<close>
      by (auto simp add:pos_divide_less_eq[OF \<open>e > 0\<close>] mult.commute)
    finally have "(1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x \ S"
      using assms(3-5) d
      by (intro convexD_alt [OF \<open>convex S\<close>]) (auto intro: convexD_alt [OF \<open>convex S\<close>])
    with \<open>e > 0\<close> show "y \<in> S"
      by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
  qed (use \<open>e>0\<close> \<open>d>0\<close> in 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 *\<^sub>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 \<open>e > 0\<close> \<open>d > 0\<close> by force
  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
        using True \<open>0 < d\<close> by auto
    next
      case False
      then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
        using \<open>e \<le> 1\<close> \<open>e > 0\<close> \<open>d > 0\<close> by auto
      then obtain y where "y \ S" "y \ x" "dist y x < e * d / (1 - e)"
        using islimpt_approachable x by blast
      then have "norm (y - x) * (1 - e) < e * d"
        by (metis "*" dist_norm mult_imp_div_pos_le not_less)
      then show ?thesis
        using \<open>y \<in> S\<close> by blast
    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) *\<^sub>R (x - y)"
  have *: "x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)"
    unfolding z_def using \<open>e > 0\<close>
    by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
  have "(1 - e) * norm (x - y) / e < d"
    using y \<open>0 < e\<close> by (simp add: field_simps norm_minus_commute)
  then have "z \ interior (ball c d)"
    using \<open>0 < e\<close> \<open>e \<le> 1\<close> by (simp add: interior_open[OF open_ball] z_def dist_norm)
  then have "z \ interior S"
    using d interiorI interior_ball by blast
  then show ?thesis
    unfolding * using mem_interior_convex_shrink \<open>y \<in> S\<close> assms by blast
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 -
  { fix u::real
    assume u: "0 < u" "u < 1"
    have "(1 - u) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>R (b - a)"
      by (simp add: algebra_simps)
    also have "... \ interior S" using mem_interior_closure_convex_shrink [OF assms] u
      by simp
    finally have "(1 - u) *\<^sub>R a + u *\<^sub>R b \ interior S" .
  }
  then show ?thesis
    by (clarsimp simp: in_segment)
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 \<open>a \<in> interior S\<close> closure_subset by blast
    next
      case False
      { fix e::real
        assume xnotS: "x \ interior S" and "0 < e"
        have "\x'\interior S. x' \ x \ dist x' x < e"
        proof (intro bexI conjI)
          show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \ x"
            using False \<open>0 < e\<close> by (auto simp: algebra_simps min_def)
          show "dist (x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a)) x < e"
            using \<open>0 < e\<close> by (auto simp: dist_norm min_def)
          show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \ interior S"
            using \<open>0 < e\<close> False
            by (auto simp add: min_def a intro: mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x])
        qed
      }
      then show ?thesis
        by (auto simp add: closure_def islimpt_approachable)
    qed
  qed
  then show ?thesis
    by (simp add: closure_mono interior_subset subset_antisym)
qed

lemma openin_subset_relative_interior:
  fixes S :: "'a::euclidean_space set"
  shows "openin (top_of_set (affine hull T)) S \ (S \ rel_interior T) = (S \ T)"
  by (meson order.trans rel_interior_maximal rel_interior_subset)

lemma conic_hull_eq_span_affine_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "0 \ rel_interior S"
  shows "conic hull S = span S \ conic hull S = affine hull S"
proof -
  obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "cball 0 \<epsilon> \<inter> affine hull S \<subseteq> S"
    using assms mem_rel_interior_cball by blast
  have *: "affine hull S = span S"
    by (meson affine_hull_span_0 assms hull_inc mem_rel_interior_cball)
  moreover
  have "conic hull S \ span S"
    by (simp add: hull_minimal span_superset)
  moreover
  { fix x
    assume "x \ affine hull S"
    have "x \ conic hull S"
    proof (cases "x=0")
      case True
      then show ?thesis
        using \<open>x \<in> affine hull S\<close> by auto
    next
      case False
      then have "(\ / norm x) *\<^sub>R x \ cball 0 \ \ affine hull S"
        using \<open>0 < \<epsilon>\<close> \<open>x \<in> affine hull S\<close> * span_mul by fastforce
      then have "(\ / norm x) *\<^sub>R x \ S"
        by (meson \<epsilon> subsetD)
      then have "\c xa. x = c *\<^sub>R xa \ 0 \ c \ xa \ S"
        by (smt (verit, del_insts) \<open>0 < \<epsilon>\<close> divide_nonneg_nonneg eq_vector_fraction_iff norm_eq_zero norm_ge_zero)
      then show ?thesis
        by (simp add: conic_hull_explicit)
    qed
  }
  then have "affine hull S \ conic hull S"
    by auto
  ultimately show ?thesis
    by blast
qed

lemma conic_hull_eq_span:
  fixes S :: "'a::euclidean_space set"
  assumes "0 \ rel_interior S"
  shows "conic hull S = span S"
  by (simp add: assms conic_hull_eq_span_affine_hull)

lemma conic_hull_eq_affine_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "0 \ rel_interior S"
  shows "conic hull S = affine hull S"
  using assms conic_hull_eq_span_affine_hull by blast

lemma conic_hull_eq_span_eq:
  fixes S :: "'a::euclidean_space set"
  shows "0 \ rel_interior(conic hull S) \ conic hull S = span S" (is "?lhs = ?rhs")
proof
  show "?lhs \ ?rhs"
    by (metis conic_hull_eq_span conic_span hull_hull hull_minimal hull_subset span_eq)
  show "?rhs \ ?lhs"
  by (metis rel_interior_affine subspace_affine subspace_span)
qed

lemma aff_dim_psubset:
   "(affine hull S) \ (affine hull T) \ aff_dim S < aff_dim T"
  by (metis aff_dim_affine_hull aff_dim_empty aff_dim_subset affine_affine_hull affine_dim_equal order_less_le)

lemma aff_dim_eq_full_gen:
   "S \ T \ (aff_dim S = aff_dim T \ affine hull S = affine hull T)"
  by (smt (verit, del_insts) aff_dim_affine_hull2 aff_dim_psubset hull_mono psubsetI)

lemma aff_dim_eq_full:
  fixes S :: "'n::euclidean_space set"
  shows "aff_dim S = (DIM('n)) \ affine hull S = UNIV"
  by (metis aff_dim_UNIV aff_dim_affine_hull affine_hull_UNIV)

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\<^marker>\<open>tag unimportant\<close> \<open>Some obvious but surprisingly hard simplex lemmas\<close>

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 *\<^sub>R x) S = y}"
proof -
  { fix x and u :: "'a \ real"
    assume "\x\S. 0 \ u x" "sum u S \ 1"
    then have "\v. 0 \ v 0 \ (\x\S. 0 \ v x) \ v 0 + sum v S = 1 \ (\x\S. v x *\<^sub>R x) = (\x\S. u x *\<^sub>R x)"
      by (rule_tac x="\x. if x = 0 then 1 - sum u S else u x" in exI) (auto simp: sum_delta_notmem assms if_smult)
  }
  then show ?thesis by (auto simp: convex_hull_finite set_eq_iff assms)
qed

lemma substd_simplex:
  assumes d: "d \ Basis"
  shows "convex hull (insert 0 d) =
    {x. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> (\<Sum>i\<in>d. x\<bullet>i) \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>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 \<open>finite d\<close> \<open>0 \<notin> ?p\<close>]
  proof (intro set_eqI; safe)
    fix u :: "'a \ real"
    assume as: "\x\?D. 0 \ u x" "sum u ?D \ 1"
    let ?x = "(\x\?D. u x *\<^sub>R x)"
    have ind: "\i\Basis. i \ d \ u i = ?x \ i"
      and notind: "(\i\Basis. i \ d \ ?x \ i = 0)"
      using substdbasis_expansion_unique[OF assms] by blast+
    then have **: "sum u ?D = sum ((\) ?x) ?D"
      using assms by (meson subset_iff sum.cong)
    show "0 \ ?x \ i" if "i \ Basis" for i
      using as(1) ind notind that by fastforce
    show "sum ((\) ?x) ?D \ 1"
      using "**" as(2) by linarith
    show "?x \ i = 0" if "i \ Basis" "i \ d" for i
      using notind that by blast
  next
    fix x
    assume "\i\Basis. 0 \ x \ i" "sum ((\) x) ?D \ 1" "(\i\Basis. i \ d \ x \ i = 0)"
    with d show "\u. (\x\?D. 0 \ u x) \ sum u ?D \ 1 \ (\x\?D. u x *\<^sub>R x) = x"
      unfolding substdbasis_expansion_unique[OF assms]
      by (rule_tac x="inner x" in exI) auto
  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}"
  unfolding set_eq_iff mem_interior std_simplex
proof (intro allI iffI CollectI; clarify)
  fix x :: 'a
  fix e
  assume "e > 0" and as: "ball x e \ {x. (\i\Basis. 0 \ x \ i) \ sum ((\) x) Basis \ 1}"
  show "(\i\Basis. 0 < x \ i) \ sum ((\) x) Basis < 1"
  proof (intro strip conjI)
    fix i :: 'a
    assume i: "i \ Basis"
    then show "0 < x \ i"
      using as[THEN subsetD[where c="x - (e/2) *\<^sub>R i"]] and \e > 0\
      by (force simp add: inner_simps)
  next
    obtain i::'a where i: "i \ Basis"
      using nonempty_Basis by blast
    have **: "dist x (x + (e/2) *\<^sub>R i) < e" using \e > 0\
      unfolding dist_norm
      by (auto intro!: mult_strict_left_mono simp: i)
    have "\i. i \ Basis \ (x + (e/2) *\<^sub>R i) \ i = x\i + (if i = i then e/2 else 0)"
      by (auto simp: inner_simps)
    then have *: "sum ((\) (x + (e/2) *\<^sub>R i)) Basis = sum (\j. x\j + (if j = i then e/2 else 0)) Basis"
      using i by (auto simp: inner_Basis inner_left_distrib intro!: sum.cong)
    have "sum ((\) x) Basis < sum ((\) (x + (e/2) *\<^sub>R i)) Basis"
      using \<open>e > 0\<close> DIM_positive by (auto simp: i sum.distrib *)
    also have "\ \ 1"
      using ** as by force
    finally show "sum ((\) x) Basis < 1" by auto
  qed
next
  fix x :: 'a
  assume as: "\i\Basis. 0 < x \ i" "sum ((\) x) Basis < 1"
  obtain a :: 'b where "a \ UNIV" using UNIV_witness ..
  let ?d = "(1 - sum ((\) x) Basis) / real (DIM('a))"
  show "\e>0. ball x e \ {x. (\i\Basis. 0 \ x \ i) \ sum ((\) x) Basis \ 1}"
  proof (intro exI conjI subsetI CollectI)
    fix y
    assume y: "y \ ball x (min (Min ((\) x ` Basis)) ?d)"
    have "sum ((\) y) Basis \ sum (\i. x\i + ?d) Basis"
    proof (rule sum_mono)
      fix i :: 'a
      assume i: "i \ Basis"
      have "\y\i - x\i\ \ norm (y - x)"
        by (metis Basis_le_norm i inner_commute inner_diff_right)
      also have "... < ?d"
        using y by (simp add: dist_norm norm_minus_commute)
      finally have "\y\i - x\i\ < ?d" .
      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 ((\) y) Basis \ 1" .
    show "(\i\Basis. 0 \ y \ i)"
    proof (intro strip)
      fix i :: 'a
      assume i: "i \ Basis"
      have "norm (x - y) < Min (((\) x) ` Basis)"
        using y by (auto simp: dist_norm less_eq_real_def)
      also have "... \ x\i"
        using i by auto
      finally have "norm (x - y) < x\i" .
      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 (((\) x) ` Basis) > 0"
      using as by simp
    moreover have "?d > 0"
      using as by (auto simp: Suc_le_eq)
    ultimately show "0 < min (Min ((\) x ` Basis)) ((1 - sum ((\) 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)) *\<^sub>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
  proof
    show "?a \ interior(convex hull (insert 0 Basis))"
      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)
    next
      have "sum ((\) ?a) ?D = sum (\i. inverse (2 * real DIM('a))) ?D"
        by simp
      also have "\ < 1"
        unfolding sum_constant divide_inverse[symmetric]
        by (auto simp add: field_simps)
      finally show "sum ((\) ?a) ?D < 1" by auto
    qed
  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 "_ = ?s")
proof -
  have "finite D"
    using D finite_Basis finite_subset by blast
  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 D)) =
              {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 D))"
      then obtain e where "e > 0" and
        "ball x e \ {xa. (\i\Basis. i \ D \ xa\i = 0)} \ convex hull (insert 0 D)"
        using mem_rel_interior_ball[of x "convex hull (insert 0 D)"] h0 by auto
      then have as: "\y. \dist x y < e \ (\i\Basis. i \ D \ y\i = 0)\ \
                            (\<forall>i\<in>D. 0 \<le> y \<bullet> i) \<and> sum ((\<bullet>) y) D \<le> 1"
        using assms by (force simp: substd_simplex)
      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 ((\) x) D < 1 \ (\i\Basis. i \ D \ x\i = 0)"
      proof (intro conjI ballI)
        fix i :: 'a
        assume "i \ D"
        then have "\j\D. 0 \ (x - (e/2) *\<^sub>R i) \ j"
          using D \<open>e > 0\<close> x0
          by (intro as[THEN conjunct1]) (force simp: dist_norm inner_simps inner_Basis)
        then show "0 < x \ i"
          using \<open>e > 0\<close> \<open>i \<in> D\<close> D  by (force simp: inner_simps inner_Basis)
      next
        obtain a where a: "a \ D"
          using \<open>D \<noteq> {}\<close> by auto
        then have **: "dist x (x + (e/2) *\<^sub>R a) < e"
          using \<open>e > 0\<close> norm_Basis[of a] D by (auto simp: dist_norm)
        have "\i. i \ Basis \ (x + (e/2) *\<^sub>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 ((\) (x + (e/2) *\<^sub>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 \<open>a \<in> D\<close> D by auto
        then have h1: "(\i\Basis. i \ D \ (x + (e/2) *\<^sub>R a) \ i = 0)"
          using x0 D \<open>a\<in>D\<close> by (auto simp add: inner_add_left inner_Basis)
        have "sum ((\) x) D < sum ((\) (x + (e/2) *\<^sub>R a)) D"
          using \<open>e > 0\<close> \<open>a \<in> D\<close> \<open>finite D\<close> by (auto simp add: * sum.distrib)
        also have "\ \ 1"
          using ** h1 as[rule_format, of "x + (e/2) *\<^sub>R a"]
          by auto
        finally show "sum ((\) x) D < 1" "\i. 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 D)"
        using as assms by (force simp add: substd_simplex)
      obtain a where a: "a \ D"
        using \<open>D \<noteq> {}\<close> by auto
      define d where "d \ (1 - sum ((\) x) D) / real (card D)"
      have "\e>0. ball x e \ {x. \i\Basis. i \ D \ x \ i = 0} \ convex hull insert 0 D"
        unfolding substd_simplex[OF assms]
      proof (intro exI; safe)
        have "0 < card D" using \<open>D \<noteq> {}\<close> \<open>finite D\<close>
          by (simp add: card_gt_0_iff)
        have "Min (((\) x) ` D) > 0"
          using as \<open>D \<noteq> {}\<close> \<open>finite D\<close> by (simp)
        moreover have "d > 0"
          using as \<open>0 < card D\<close> by (auto simp: d_def)
        ultimately show "min (Min (((\) x) ` D)) d > 0"
          by auto
        fix y :: 'a
        assume y2: "\i\Basis. i \ D \ y\i = 0"
        assume "y \ ball x (min (Min ((\) x ` D)) d)"
        then have y: "dist x y < min (Min ((\) x ` D)) d"
          by auto
        have "sum ((\) 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\ \ norm (y - x)"
            by (metis i inner_commute inner_diff_right norm_bound_Basis_le order_refl)
          also have "... < d"
            by (metis dist_norm min_less_iff_conj norm_minus_commute y)
          finally have "\y\i - x\i\ < d" .
          then show "y \ i \ x \ i + d" by auto
        qed
        also have "\ \ 1"
          unfolding sum.distrib sum_constant d_def using \<open>0 < card D\<close>
          by auto
        finally show "sum ((\) 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 Min_gr_iff[of "(\) x ` D" "norm (x - y)"] \0 < card D\ \i \ D\
            by (simp add: dist_norm 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 (use y2 in auto)
      qed
      then have "x \ rel_interior (convex hull (insert 0 D))"
        using h0 h2 rel_interior_ball by force
    }
    ultimately have
      "\x. x \ rel_interior (convex hull insert 0 D) \
        x \<in> {x. (\<forall>i\<in>D. 0 < x \<bullet> i) \<and> sum ((\<bullet>) x) D < 1 \<and> (\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> x \<bullet> 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 ?a = "(\b\D. b /\<^sub>R (2 * real (card D)))"
  have "finite D"
    using assms finite_Basis infinite_super by blast
  then have d1: "0 < real (card D)"
    using \<open>D \<noteq> {}\<close> by auto
  {
    fix i
    assume "i \ D"
    have "?a \ i = (\j\D. if i = j then inverse (2 * real (card D)) else 0)"
      unfolding inner_sum_left
      using \<open>i \<in> D\<close> by (auto simp: inner_Basis subsetD[OF assms(2)] intro: sum.cong)
    also have "... = inverse (2 * real (card D))"
      using \<open>i \<in> D\<close> \<open>finite D\<close> by auto
    finally have "?a \ i = inverse (2 * real (card D))" .
  }
  note ** = this
  show ?thesis
  proof
    show "?a \ rel_interior (convex hull (insert 0 D))"
      unfolding rel_interior_substd_simplex[OF assms(2)]
    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 ((\) ?a) D = sum (\i. inverse (2 * real (card D))) D"
        by (rule sum.cong [OF refl **])
      also have "\ < 1"
        unfolding sum_constant divide_real_def[symmetric]
        by (auto simp add: field_simps)
      finally show "sum ((\) ?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 /\<^sub>R (2 * real (card D)))" D])
        {
          fix x :: "'a::euclidean_space"
          assume "x \ D"
          then have "x \ span D"
            using span_base[of _ "D"] by auto
          then have "x /\<^sub>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 /\<^sub>R (2 * real (card D)) \ span D"
          by auto
      qed
      then show "?a \ i = 0 "
        using \<open>i \<notin> D\<close> unfolding span_substd_basis[OF assms(2)] using \<open>i \<in> Basis\<close> by auto
    qed
  qed
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Relative interior of convex set\<close>

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 metis
  then have "B \ {}"
    using B assms \<open>S \<noteq> {0}\<close> span_empty by auto
  have "insert 0 B \ span B"
    using subspace_span[of B] subspace_0[of "span B"]
      span_superset 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 \<open>B \<noteq> {}\<close> 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)"] \<open>linear f\<close>
    by auto
  moreover have "rel_interior (f ` (convex hull insert 0 B)) = f ` rel_interior (convex hull insert 0 B)"
  proof (rule rel_interior_injective_on_span_linear_image[OF \<open>bounded_linear f\<close>])
    show "inj_on f (span (convex hull insert 0 B))"
      using fd * by auto
  qed
  ultimately have "rel_interior (convex hull insert 0 B) \ {}"
    using rel_interior_substd_simplex_nonempty[OF \<open>d \<noteq> {}\<close> d] by fastforce
  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 \ (+) (-a) ` S"
      using assms exI[of "(\x. x \ S \ - a + x = 0)" a] by auto
    then have "rel_interior ((+) (-a) ` S) \ {}"
      using rel_interior_convex_nonempty_aux[of "(+) (-a) ` S"]
        convex_translation[of S "-a"] assms
      by auto
    then have "rel_interior S \ {}"
      using rel_interior_translation [of "- a"] by simp
  }
  then show ?thesis 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"
    by (simp add: hull_inc affine_hull_span_0 dim_eq_full[symmetric]
         assms(1) assms(3) dim_eq_card_independent)
  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 *\<^sub>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 \<open>x \<in> S\<close> by auto
    next
      case True
      then show ?thesis using assm by auto
    qed
    then have "(1 - u) *\<^sub>R x + u *\<^sub>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 \<open>x \<noteq> a\<close> \<open>e > 0\<close> le_divide_eq[of e1 e "norm (x - a)"]
             by simp_all
           then have *: "x - e1 *\<^sub>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"
             using "*" \<open>x \<noteq> a\<close> e1 by force
        }
        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
  qed auto
qed

lemma empty_interior_subset_hyperplane_aux:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "0 \ S" and empty_int: "interior S = {}"
  shows "\a b. a\0 \ S \ {x. a \ x = b}"
proof -
  have False if "\a. a = 0 \ (\b. \T \ S. a \ T \ b)"
  proof -
    have rel_int: "rel_interior S \ {}"
      using assms rel_interior_eq_empty by auto
    moreover
    have "dim S \ dim (UNIV::'a set)"
      by (metis aff_dim_zero affine_hull_UNIV \<open>0 \<in> S\<close> dim_UNIV empty_int hull_inc rel_int rel_interior_interior)
    then obtain a where "a \ 0" and a: "span S \ {x. a \ x = 0}"
      using lowdim_subset_hyperplane
      by (metis dim_UNIV dim_subset_UNIV order_less_le)
    have "span UNIV = span S"
      by (metis span_base span_not_UNIV_orthogonal that)
    then have "UNIV \ affine hull S"
      by (simp add: \<open>0 \<in> S\<close> hull_inc affine_hull_span_0)
    ultimately show False
      using \<open>rel_interior S \<noteq> {}\<close> empty_int rel_interior_interior by blast
  qed
  then show ?thesis
    by blast
qed

lemma empty_interior_subset_hyperplane:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" and int: "interior S = {}"
  obtains a b where "a \ 0" "S \ {x. a \ x = b}"
proof (cases "S = {}")
  case True
  then show ?thesis
    using that by blast
next
  case False
  then obtain u where "u \ S"
    by blast
  have "\a b. a \ 0 \ (\x. x - u) ` S \ {x. a \ x = b}"
  proof (rule empty_interior_subset_hyperplane_aux)
    show "convex ((\x. x - u) ` S)"
      using \<open>convex S\<close> by force
    show "0 \ (\x. x - u) ` S"
      by (simp add: \<open>u \<in> S\<close>)
    show "interior ((\x. x - u) ` S) = {}"
      by (simp add: int interior_translation_subtract)
  qed
  then obtain a b where "a \ 0" and ab: "(\x. x - u) ` S \ {x. a \ x = b}"
    by metis
  then have "S \ {x. a \ x = b + (a \ u)}"
    using ab by (auto simp: algebra_simps)
  then show ?thesis
    using \<open>a \<noteq> 0\<close> that by auto
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 (top_of_set (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) *\<^sub>R z = a *\<^sub>R x + b *\<^sub>R y"
  obtains e where "0 < e" "e < 1" "z = y - e *\<^sub>R (y - x)"
proof -
  define e where "e = a / (a + b)"
  have "z = (1 / (a + b)) *\<^sub>R ((a + b) *\<^sub>R z)"
    using assms  by (simp add: eq_vector_fraction_iff)
  also have "\ = (1 / (a + b)) *\<^sub>R (a *\<^sub>R x + b *\<^sub>R y)"
    using assms scaleR_cancel_left[of "1/(a+b)" "(a + b) *\<^sub>R z" "a *\<^sub>R x + b *\<^sub>R y"]
    by auto
  also have "\ = y - e *\<^sub>R (y-x)"
    using e_def assms
    by (simp add: divide_simps vector_fraction_eq_iff) (simp add: algebra_simps)
  finally have "z = y - e *\<^sub>R (y-x)"
    by auto
  moreover have "e > 0" "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 \<open>S \<noteq> {}\<close> 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)) *\<^sub>R (z-x)"
      have yball: "y \ cball z e"
        using 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))) *\<^sub>R z = (e/norm(z-x)) *\<^sub>R x + y"
        using y_def by (simp add: algebra_simps)
      then obtain e1 where "0 < e1" "e1 < 1" "z = y - e1 *\<^sub>R (y - x)"
        using * convex_rel_interior_closure_aux[of "e / norm (z - x)" 1 z x y]
        by (auto simp add: algebra_simps)
      then show ?thesis
        using rel_interior_closure_convex_shrink assms x \<open>y \<in> closure S\<close>
        by fastforce
    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 open_subset_closure_of_interval:
  assumes "open U" "is_interval S"
  shows "U \ closure S \ U \ interior S"
  by (metis assms convex_interior_closure is_interval_convex open_subset_interior)

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 \<open>?B\<close> have "closure S1 \<supseteq> 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
  have "open_segment a b = affine hull {a, b} \ ball ((a + b) /\<^sub>R 2) (norm (b - a) / 2)"
    by (simp add: open_segment_as_ball)
  then show ?thesis
    unfolding rel_interior_eq openin_open
    by (metis Elementary_Metric_Spaces.open_ball False affine_hull_open_segment)
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

subsection\<open>The relative frontier of a set\<close>

definition\<^marker>\<open>tag important\<close> "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"
  unfolding rel_frontier_def
  using rel_interior_subset_closure  by (auto simp add: rel_interior_eq_closure [symmetric])

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
    by simp (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 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\
   \<Longrightarrow> closest_point S x \<in> 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 (top_of_set (affine hull S)) (closure S - rel_interior S)"
    by (simp add: closed_subset closedin_diff closure_affine_hull openin_rel_interior)
  show ?thesis
  proof (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"])
    show "closedin (top_of_set (affine hull S)) (rel_frontier S)"
      by (simp add: "*" rel_frontier_def)
  qed simp
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\
         \<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow> 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\
         \<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow>
             rel_interior S \<subseteq> T \<and> T \<subseteq> 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] \<open>S2 \<noteq> {}\<close> by auto
    have **: "affine hull S1 = affine hull S2"
      by (simp_all add: * eq \<open>S1 \<noteq> {}\<close> affine_dim_equal)
    obtain a where a: "a \ rel_interior S1"
      using \<open>S1 \<noteq> {}\<close> 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) *\<^sub>R x + e *\<^sub>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 \<open>x \<noteq> z\<close> 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)*\<^sub>R x + e *\<^sub>R z \ affine hull S"
          using mem_affine[of "affine hull S" x z "(1-e)" e] affine_affine_hull[of S] x
          by auto
        have "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) = norm ((e - 1) *\<^sub>R (x - z))"
          by (simp add: algebra_simps)
        also have "\ = (e - 1) * norm (x-z)"
          using norm_scaleR e 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 \<open>x \<noteq> z\<close> e1 by simp
        finally have **: "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) \ e1"
          by auto
        have "(1 - e)*\<^sub>R x+ e *\<^sub>R z \ cball z e1"
          using m_def **
          unfolding cball_def dist_norm
          by (auto simp add: algebra_simps)
        then have "(1 - e) *\<^sub>R x+ e *\<^sub>R z \ S"
          using e * e1 by auto
      }
      then have "\m. m > 1 \ (\e. e > 1 \ e \ m \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S )"
        using \<open>m> 1 \<close> 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) *\<^sub>R x + e *\<^sub>R z \ S"
          using e1 x \<open>x = z\<close> by (auto simp add: algebra_simps)
        then have "(1 - e) *\<^sub>R x + e *\<^sub>R z \ S"
          using e by auto
      }
      then have "\m. m > 1 \ (\e. e > 1 \ e \ m \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S)"
        using \<open>m > 1\<close> by auto
    }
    ultimately have "\m. m > 1 \ (\e. e > 1 \ e \ m \ (1 - e) *\<^sub>R x + e *\<^sub>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)*\<^sub>R x + e *\<^sub>R z \ S"
  using convex_rel_interior_if[of S z] assms by auto

lemma convex_rel_interior_only_if:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
    and "S \ {}"
  assumes "\x\S. \e. e > 1 \ (1 - e) *\<^sub>R x + e *\<^sub>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) *\<^sub>R x + e *\<^sub>R z \ S"
    using assms by auto
  define y where [abs_def]: "y = (1 - e) *\<^sub>R x + e *\<^sub>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) *\<^sub>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"] \<open>0 < e1 \<and> e1 < 1\<close> \<open>y \<in> S\<close> 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) *\<^sub>R x + e *\<^sub>R z \ S)"
  using assms hull_subset[of S "affine"]
    convex_rel_interior_if[of S z] convex_rel_interior_only_if[of S z]
  by auto

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

lemma convex_interior_iff:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "z \ interior S \ (\x. \e. e > 0 \ z + e *\<^sub>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 *\<^sub>R x \ S"
    { fix x
      obtain e1 where e1: "e1 > 0 \ z + e1 *\<^sub>R (x - z) \ S"
        using r by auto
      obtain e2 where e2: "e2 > 0 \ z + e2 *\<^sub>R (z - x) \ S"
        using r by auto
      define x1 where [abs_def]: "x1 = z + e1 *\<^sub>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 *\<^sub>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)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
        by (simp add: x1_def x2_def algebra_simps) (simp add: "*" pth_8)
      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) *\<^sub>R (x - z)"
        using x1_def x2_def by (auto simp add: algebra_simps)
      then have "x = z+(1/(e1+e2)) *\<^sub>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)
    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) *\<^sub>R x + e *\<^sub>R z \ S"
      using convex_rel_interior_iff2[of S z] assms \<open>S \<noteq> {}\<close> * by auto
    fix x
    obtain e1 where e1: "e1 > 1" "(1 - e1) *\<^sub>R (z - x) + e1 *\<^sub>R z \ S"
      using **[rule_format, of "z-x"] by auto
    define e where [abs_def]: "e = e1 - 1"
    then have "(1 - e1) *\<^sub>R (z - x) + e1 *\<^sub>R z = z + e *\<^sub>R x"
      by (simp add: algebra_simps)
    then have "e > 0" "z + e *\<^sub>R x \ S"
      using e1 e_def by auto
    then have "\e. e > 0 \ z + e *\<^sub>R x \ S"
      by auto
  }
  moreover
  {
    assume r: "\x. \e. e > 0 \ z + e *\<^sub>R x \ S"
    {
      fix x
      obtain e1 where e1: "e1 > 0" "z + e1 *\<^sub>R (z - x) \ S"
        using r[rule_format, of "z-x"] by auto
      define e where "e = e1 + 1"
      then have "z + e1 *\<^sub>R (z - x) = (1 - e) *\<^sub>R x + e *\<^sub>R z"
        by (simp add: algebra_simps)
      then have "e > 1" "(1 - e)*\<^sub>R x + e *\<^sub>R z \ S"
        using e1 e_def by auto
      then have "\e. e > 1 \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S" by auto
    }
    then have "z \ rel_interior S"
      using convex_rel_interior_iff2[of S z] assms \<open>S \<noteq> {}\<close> by auto
    then have "z \ interior S"
      using True interior_rel_interior_gen[of S] by auto
  }
  ultimately show ?thesis by auto
qed

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Relative interior and closure under common operations\<close>

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 convex_closure_rel_interior_Int:
  assumes "\S. S\\ \ convex (S :: 'n::euclidean_space set)"
    and "\(rel_interior ` \) \ {}"
  shows "\(closure ` \) \ closure (\(rel_interior ` \))"
proof -
  obtain x where x: "\S\\. x \ rel_interior S"
    using assms by auto
  show ?thesis
  proof
    fix y
    assume y: "y \ \ (closure ` \)"
    show "y \ closure (\(rel_interior ` \))"
    proof (cases "y=x")
      case True
      with closure_subset x show ?thesis
        by fastforce
    next
      case False
      show ?thesis
      proof (clarsimp simp: closure_approachable_le)
        fix \<epsilon> :: real
        assume e: "\ > 0"
        define e1 where "e1 = min 1 (\/norm (y - x))"
        then have e1: "e1 > 0" "e1 \ 1" "e1 * norm (y - x) \ \"
          using \<open>y \<noteq> x\<close> \<open>\<epsilon> > 0\<close> le_divide_eq[of e1 \<epsilon> "norm (y - x)"]
          by simp_all
        define z where "z = y - e1 *\<^sub>R (y - x)"
        {
          fix S
          assume "S \ \"
          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 ` \)"
          by auto
        show "\x\\ (rel_interior ` \). dist x y \ \"
          using \<open>y \<noteq> x\<close> z_def * e1 e dist_norm[of z y]
          by force
      qed
    qed
  qed
qed

lemma closure_Inter_convex:
  fixes \<F> :: "'n::euclidean_space set set"
  assumes "\S. S \ \ \ convex S" and "\(rel_interior ` \) \ {}"
  shows "closure(\\) = \(closure ` \)"
proof -
  have "\(closure ` \) \ closure (\(rel_interior ` \))"
    by (meson assms convex_closure_rel_interior_Int)
  moreover
  have "closure (\(rel_interior ` \)) \ closure (\\)"
    using rel_interior_inter_aux closure_mono[of "\(rel_interior ` \)" "\\"]
    by auto
  ultimately show ?thesis
    using closure_Int[of \<F>] by blast
qed

lemma closure_Inter_convex_open:
    "(\S::'n::euclidean_space set. S \ \ \ convex S \ open S)
        \<Longrightarrow> closure(\<Inter>\<F>) = (if \<Inter>\<F> = {} then {} else \<Inter>(closure ` \<F>))"
  by (simp add: closure_Inter_convex rel_interior_open)

lemma convex_Inter_rel_interior_same_closure:
  fixes \<F> :: "'n::euclidean_space set set"
  assumes "\S. S \ \ \ convex S"
    and "\(rel_interior ` \) \ {}"
  shows "closure (\(rel_interior ` \)) = closure (\\)"
proof -
  have "\(closure ` \) \ closure (\(rel_interior ` \))"
    by (meson assms convex_closure_rel_interior_Int)
  moreover
  have "closure (\(rel_interior ` \)) \ closure (\\)"
    by (metis Setcompr_eq_image closure_mono rel_interior_inter_aux)
  ultimately show ?thesis
    by (simp add: assms closure_Inter_convex)
qed

lemma convex_rel_interior_Inter:
  fixes \<F> :: "'n::euclidean_space set set"
  assumes "\S. S \ \ \ convex S"
    and "\(rel_interior ` \) \ {}"
  shows "rel_interior (\\) \ \(rel_interior ` \)"
proof -
  have "convex (\\)"
--> --------------------

--> maximum size reached

--> --------------------

quality94%

¤ Dauer der Verarbeitung: 0.37 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.