Theory Starlike

```(* 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 ‹Unsorted›

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}"

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
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)
{ 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 have "x ∈ convex hull T"
using rel_interior_closure_convex_segment [OF ‹convex C› z]
using y z by blast
}
with * show "?lhs ⊆ ?rhs"
show "?rhs ⊆ ?lhs"
by (meson hull_mono inf_mono subset_insertI subset_refl)
qed

subsection✐‹tag unimportant› ‹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
proof (intro exI subsetI conjI)
fix y
assume "y ∈ ball (x - e *⇩R (x - c)) (e*d)"
then have as: "dist (x - e *⇩R (x - c)) y < e * d"
by simp
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 "c - ((1 / e) *⇩R y - ((1 - e) / e) *⇩R x) = (1 / e) *⇩R (e *⇩R c - y + (1 - e) *⇩R x)"
using ‹e > 0›
by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
then have "dist c ((1 / e) *⇩R y - ((1 - e) / e) *⇩R x) = ¦1/e¦ * norm (e *⇩R c - y + (1 - e) *⇩R x)"
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 have "(1 - (1 - e)) *⇩R ((1 / e) *⇩R y - ((1 - e) / e) *⇩R x) + (1 - e) *⇩R x ∈ S"
using assms(3-5) d
by (intro convexD_alt [OF ‹convex S›]) (auto intro: convexD_alt [OF ‹convex S›])
with ‹e > 0› show "y ∈ S"
by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
qed (use ‹e>0› ‹d>0› 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 *⇩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› 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 ‹0 < d› by auto
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 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 ‹y ∈ S› 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) *⇩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 "(1 - e) * norm (x - y) / e < d"
using y ‹0 < e› by (simp add: field_simps norm_minus_commute)
then have "z ∈ interior (ball c d)"
using ‹0 < e› ‹e ≤ 1› 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 ‹y ∈ S› 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) *⇩R a + u *⇩R b = b - (1 - u) *⇩R (b - a)"
also have "... ∈ interior S" using mem_interior_closure_convex_shrink [OF assms] u
by simp
finally have "(1 - u) *⇩R a + u *⇩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 ‹a ∈ interior S› 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 *⇩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"
using ‹0 < e› False
by (auto simp add: min_def a intro: mem_interior_closure_convex_shrink [OF ‹convex S› 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 ε where "ε>0" and ε: "cball 0 ε ∩ affine hull S ⊆ 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"
moreover
{ fix x
assume "x ∈ affine hull S"
have "x ∈ conic hull S"
proof (cases "x=0")
case True
then show ?thesis
using ‹x ∈ affine hull S› by auto
next
case False
then have "(ε / norm x) *⇩R x ∈ cball 0 ε ∩ affine hull S"
using ‹0 < ε› ‹x ∈ affine hull S› * span_mul by fastforce
then have "(ε / norm x) *⇩R x ∈ S"
by (meson ε subsetD)
then have "∃c xa. x = c *⇩R xa ∧ 0 ≤ c ∧ xa ∈ S"
by (smt (verit, del_insts) ‹0 < ε› divide_nonneg_nonneg eq_vector_fraction_iff norm_eq_zero norm_ge_zero)
then show ?thesis
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"

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)"
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
qed

subsection✐‹tag unimportant› ‹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}"
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 *⇩R x) = (∑x∈S. u x *⇩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. (∀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›]
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 *⇩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 (auto intro!: 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 *⇩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 safe
fix i :: 'a
assume i: "i ∈ Basis"
then show "0 < x ∙ i"
using as[THEN subsetD[where c="x - (e/2) *⇩R i"]] and ‹e > 0›
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 ((∙) (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"
by (auto simp: intro!: sum.cong)
have "sum ((∙) x) Basis < sum ((∙) (x + (e/2) *⇩R (SOME i. i∈Basis))) Basis"
using ‹e > 0› DIM_positive by (auto simp: SOME_Basis 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 (rule_tac x="min (Min (((∙) x) ` Basis)) D" for D in exI, intro 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
finally show "sum ((∙) y) Basis ≤ 1" .
show "(∀i∈Basis. 0 ≤ y ∙ i)"
proof safe
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)) *⇩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"])
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 (auto intro: sum.cong)
also have "… < 1"
unfolding sum_constant divide_inverse[symmetric]
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)⟧ ⟹
(∀i∈D. 0 ≤ y ∙ i) ∧ sum ((∙) y) D ≤ 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) *⇩R i) ∙ j"
using D ‹e > 0› x0
by (intro as[THEN conjunct1]) (force simp: dist_norm inner_simps inner_Basis)
then show "0 < x ∙ i"
using ‹e > 0› ‹i ∈ D› D  by (force simp: inner_simps inner_Basis)
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 by (auto simp: dist_norm)
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 ((∙) (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)"
have "sum ((∙) x) D < sum ((∙) (x + (e/2) *⇩R a)) D"
using ‹e > 0› ‹a ∈ D› ‹finite D› by (auto simp add: * sum.distrib)
also have "… ≤ 1"
using ** h1 as[rule_format, of "x + (e/2) *⇩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 ‹D ≠ {}› 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 ‹D ≠ {}› ‹finite D›
have "Min (((∙) x) ` D) > 0"
using as ‹D ≠ {}› ‹finite D› by (simp)
moreover have "d > 0"
using as ‹0 < card D› 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 ‹0 < card D›
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›
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 ∈ {x. (∀i∈D. 0 < x ∙ i) ∧ sum ((∙) 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 ?a = "sum (λb::'a::euclidean_space. inverse (2 * real (card D)) *⇩R b) D"
have "finite D"
using assms finite_Basis infinite_super by blast
then have d1: "0 < real (card D)"
using ‹D ≠ {}› by auto
{
fix i
assume "i ∈ D"
have "?a ∙ i = sum (λj. if i = j then inverse (2 * real (card D)) else 0) D"
unfolding inner_sum_left
using ‹i ∈ D› by (auto simp: inner_Basis subsetD[OF assms(2)] intro: sum.cong)
also have "... = inverse (2 * real (card D))"
using ‹i ∈ D› ‹finite D› 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) (rule refl, rule **)
also have "… < 1"
unfolding sum_constant divide_real_def[symmetric]
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 /⇩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 /⇩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
qed

subsection✐‹tag unimportant› ‹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 metis
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_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 ‹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)"
proof (rule rel_interior_injective_on_span_linear_image[OF ‹bounded_linear f›])
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 ‹d ≠ {}› 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) ≠ {}"
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"
}
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"
using "*" ‹x ≠ a› 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 ‹0 ∈ S› 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: ‹0 ∈ S› hull_inc affine_hull_span_0)
ultimately show False
using ‹rel_interior S ≠ {}› 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 ‹convex S› by force
show "0 ∈ (λx. x - u) ` S"
by (simp add: ‹u ∈ S›)
show "interior ((λx. x - u) ` S) = {}"
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 ‹a ≠ 0› 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) *⇩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)"
using assms  by (simp add: eq_vector_fraction_iff)
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 assms
finally have "z = y - e *⇩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 ‹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 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]
then show ?thesis
using rel_interior_closure_convex_shrink assms x ‹y ∈ closure S›
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 ‹?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
have "open_segment a b = affine hull {a, b} ∩ ball ((a + b) /⇩R 2) (norm (b - a) / 2)"
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‹The relative frontier of a set›

definition✐‹tag important› "rel_frontier S = closure S - rel_interior S"

lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"

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} = {}"

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⟧
⟹ 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 (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)"
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⟧
⟹ rel_interior S = rel_interior T ⟷ closure S = closure T"

fixes S :: "'n::euclidean_space set"
shows "⟦convex S; convex T⟧
⟹ rel_interior S = rel_interior T ⟷
rel_interior S ⊆ T ∧ T ⊆ closure S"

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"
by (simp_all add: * eq ‹S1 ≠ {}› affine_dim_equal)
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))"
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
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```