# Theory Starlike

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

section ‹Line segments, Starlike Sets, etc›

theory Starlike
imports Convex_Euclidean_Space
begin

subsection ‹Midpoint›

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

lemma midpoint_idem [simp]: "midpoint x x = x"
unfolding midpoint_def  by simp

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

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

lemma
fixes a::real
assumes "a ≤ b" shows ge_midpoint_1: "a ≤ midpoint a b"
and le_midpoint_1: "midpoint a b ≤ b"

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

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

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

lemma midpoint_linear_image:
"linear f ⟹ midpoint(f a)(f b) = f(midpoint a b)"

subsection ‹Line segments›

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

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

lemmas segment = open_segment_def closed_segment_def

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

lemma closed_segment_linear_image:
"closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f"
proof -
interpret linear f by fact
show ?thesis
qed

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma closed_segment_in_Reals:
"⟦x ∈ closed_segment a b; a ∈ Reals; b ∈ Reals⟧ ⟹ x ∈ Reals"
by (meson subsetD convex_Reals convex_contains_segment)

lemma open_segment_in_Reals:
"⟦x ∈ open_segment a b; a ∈ Reals; b ∈ Reals⟧ ⟹ x ∈ Reals"
by (metis Diff_iff closed_segment_in_Reals open_segment_def)

lemma closed_segment_subset: "⟦x ∈ S; y ∈ S; convex S⟧ ⟹ closed_segment x y ⊆ S"

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

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

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

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

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

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

lemmas bounded_segment = bounded_closed_segment open_closed_segment

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

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

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

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

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

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

lemma open_segment_commute: "open_segment a b = open_segment b a"
proof -
have "{a, b} = {b, a}" by auto
thus ?thesis
qed

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

lemma open_segment_idem [simp]: "open_segment a a = {}"

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

lemma convex_contains_open_segment:
"convex s ⟷ (∀a∈s. ∀b∈s. open_segment a b ⊆ s)"

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

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

lemma closed_segment_real_eq:
fixes u::real shows "closed_segment u v = (λx. (v - u) * x + u) ` {0..1}"

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

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

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

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

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

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

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

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

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

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

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

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

lemma segment_eq_compose:
fixes a :: "'a :: real_vector"
shows "(λu. (1 - u) *⇩R a + u *⇩R b) = (λx. a + x) o (λu. u *⇩R (b - a))"

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

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

fixes a b ::"'a::real_vector"
assumes  "(u *⇩R b + v *⇩R a) = (u *⇩R a + v *⇩R b)"  "u ≠ v"
shows "a=b"

lemma closed_segment_image_interval:
"closed_segment a b = (λu. (1 - u) *⇩R a + u *⇩R b) ` {0..1}"
by (auto simp: set_eq_iff image_iff closed_segment_def)

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

lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval

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

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

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

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

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

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

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

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

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

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

lemmas convex_segment = convex_closed_segment convex_open_segment

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

lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real
by (auto simp: is_interval_convex_1)

lemma IVT'_closed_segment_real:
fixes f :: "real ⇒ real"
assumes "y ∈ closed_segment (f a) (f b)"
assumes "continuous_on (closed_segment a b) f"
shows "∃x ∈ closed_segment a b. f x = y"
using IVT'[of f a y b]
IVT'[of "-f" a "-y" b]
IVT'[of f b y a]
IVT'[of "-f" b "-y" a] assms
by (cases "a ≤ b"; cases "f b ≥ f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)

subsection‹Starlike sets›

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

lemma starlike_UNIV [simp]: "starlike UNIV"

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

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)
then show "?lhs ⊆ ?rhs"
fix x y
assume "x ∈ S" and y: "y ∈ convex hull T" and "x ∈ closed_segment z y"
have "y ∈ closure C"
by (metis y ‹convex C› ‹T ⊆ C› closure_subset contra_subsetD convex_hull_eq hull_mono)
moreover have "x ∉ rel_interior C"
by (meson ‹x ∈ S› dis disjnt_iff)
moreover have "x ∈ open_segment z y ∪ {z, y}"
using ‹x ∈ closed_segment z y› closed_segment_eq_open by blast
ultimately show "x ∈ convex hull T"
using rel_interior_closure_convex_segment [OF ‹convex C› z]
using y z by blast
qed
show "?rhs ⊆ ?lhs"
by (meson hull_mono inf_mono subset_insertI subset_refl)
qed

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

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

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

lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball

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

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

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

lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty

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

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

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

lemmas finite_segment = finite_closed_segment finite_open_segment

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

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

lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing

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

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

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

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

lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment

subsection‹Betweenness›

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

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

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

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

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

lemma between: "between (a, b) (x::'a::euclidean_space) ⟷ dist a b = (dist a x) + (dist x b)"
proof (cases "a = b")
case True
then show ?thesis
by (auto simp add: between_def dist_commute)
next
case False
then have Fal: "norm (a - b) ≠ 0" and Fal2: "norm (a - b) > 0"
by auto
have *: "⋀u. a - ((1 - u) *⇩R a + u *⇩R b) = u *⇩R (a - b)"
have "norm (a - x) *⇩R (x - b) = norm (x - b) *⇩R (a - x)" if "x = (1 - u) *⇩R a + u *⇩R b" "0 ≤ u" "u ≤ 1" for u
proof -
have *: "a - x = u *⇩R (a - b)" "x - b = (1 - u) *⇩R (a - b)"
unfolding that(1) by (auto simp add:algebra_simps)
show "norm (a - x) *⇩R (x - b) = norm (x - b) *⇩R (a - x)"
unfolding norm_minus_commute[of x a] * using ‹0 ≤ u› ‹u ≤ 1›
qed
moreover have "∃u. x = (1 - u) *⇩R a + u *⇩R b ∧ 0 ≤ u ∧ u ≤ 1" if "dist a b = dist a x + dist x b"
proof -
let ?β = "norm (a - x) / norm (a - b)"
show "∃u. x = (1 - u) *⇩R a + u *⇩R b ∧ 0 ≤ u ∧ u ≤ 1"
proof (intro exI conjI)
show "?β ≤ 1"
using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto
show "x = (1 - ?β) *⇩R a + (?β) *⇩R b"
proof (subst euclidean_eq_iff; intro ballI)
fix i :: 'a
assume i: "i ∈ Basis"
have "((1 - ?β) *⇩R a + (?β) *⇩R b) ∙ i
= ((norm (a - b) - norm (a - x)) * (a ∙ i) + norm (a - x) * (b ∙ i)) / norm (a - b)"
using Fal by (auto simp add: field_simps inner_simps)
also have "… = x∙i"
apply (rule divide_eq_imp[OF Fal])
unfolding that[unfolded dist_norm]
using that[unfolded dist_triangle_eq] i
apply (subst (asm) euclidean_eq_iff)
apply (auto simp add: field_simps inner_simps)
done
finally show "x ∙ i = ((1 - ?β) *⇩R a + (?β) *⇩R b) ∙ i"
by auto
qed
qed (use Fal2 in auto)
qed
ultimately show ?thesis
by (force simp add: between_def closed_segment_def dist_triangle_eq)
qed

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection%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 "dist c ((1 / e) *⇩R y - ((1 - e) / e) *⇩R x) = ¦1/e¦ * norm (e *⇩R c - y + (1 - e) *⇩R x)"
unfolding dist_norm
unfolding norm_scaleR[symmetric]
apply (rule arg_cong[where f=norm])
using ‹e > 0›
by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
also have "… = ¦1/e¦ * norm (x - e *⇩R (x - c) - y)"
by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
also have "… < d"
using as[unfolded dist_norm] and ‹e > 0›
by (auto simp add:pos_divide_less_eq[OF ‹e > 0›] mult.commute)
finally show "y ∈ S"
apply (subst *)
apply (rule assms(1)[unfolded convex_alt,rule_format])
apply (rule d[unfolded subset_eq,rule_format])
unfolding mem_ball
using assms(3-5)
apply auto
done
qed (insert ‹e>0› ‹d>0›, auto)
qed

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

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

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

lemma closure_convex_Int_superset:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "interior S ≠ {}" "interior S ⊆ closure T"
shows "closure(S ∩ T) = closure S"
proof -
have "closure S ⊆ closure(interior S)"
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%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 (simp add: convex_hull_finite set_eq_iff assms, safe)
fix x and u :: "'a ⇒ real"
assume "0 ≤ u 0" "∀x∈S. 0 ≤ u x" "u 0 + sum u S = 1"
then show "∃v. (∀x∈S. 0 ≤ v x) ∧ sum v S ≤ 1 ∧ (∑x∈S. v x *⇩R x) = (∑x∈S. u x *⇩R x)"
by force
next
fix x and u :: "'a ⇒ real"
assume "∀x∈S. 0 ≤ u x" "sum u S ≤ 1"
then show "∃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)
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) < MINIMUM Basis ((∙) x)"
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
apply (rule that[of ?a])
unfolding interior_std_simplex mem_Collect_eq
proof safe
fix i :: 'a
assume i: "i ∈ Basis"
show "0 < ?a ∙ i"
unfolding **[OF i] by (auto simp add: Suc_le_eq DIM_positive)
next
have "sum ((∙) ?a) ?D = sum (λi. inverse (2 * real DIM('a))) ?D"
apply (rule sum.cong)
apply rule
apply auto
done
also have "… < 1"
unfolding sum_constant divide_inverse[symmetric]
finally show "sum ((∙) ?a) ?D < 1" by auto
qed
qed

lemma rel_interior_substd_simplex:
assumes D: "D ⊆ Basis"
shows "rel_interior (convex hull (insert 0 D)) =
{x::'a::euclidean_space. (∀i∈D. 0 < x∙i) ∧ (∑i∈D. x∙i) < 1 ∧ (∀i∈Basis. i ∉ D ⟶ x∙i = 0)}"
(is "rel_interior (convex hull (insert 0 ?p)) = ?s")
proof -
have "finite D"
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 ?p)) =
{x::'a::euclidean_space. (∀i∈Basis. i ∉ D ⟶ x∙i = 0)}"
using affine_hull_convex_hull affine_hull_substd_basis assms by auto
have aux: "⋀x::'a. ∀i∈Basis. (∀i∈D. 0 ≤ x∙i) ∧ (∀i∈Basis. i ∉ D ⟶ x∙i = 0) ⟶ 0 ≤ x∙i"
by auto
{
fix x :: "'a::euclidean_space"
assume x: "x ∈ rel_interior (convex hull (insert 0 ?p))"
then obtain e where "e > 0" and
"ball x e ∩ {xa. (∀i∈Basis. i ∉ D ⟶ xa∙i = 0)} ⊆ convex hull (insert 0 ?p)"
using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto
then have as [rule_format]: "⋀y. dist x y < e ∧ (∀i∈Basis. i ∉ D ⟶ y∙i = 0) ⟶
(∀i∈D. 0 ≤ y ∙ i) ∧ sum ((∙) y) D ≤ 1"
unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto
have x0: "(∀i∈Basis. i ∉ D ⟶ x∙i = 0)"
using x rel_interior_subset  substd_simplex[OF assms] by auto
have "(∀i∈D. 0 < x ∙ i) ∧ sum ((∙) 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"
apply -
apply (rule as[THEN conjunct1])
using D ‹e > 0› x0
apply (auto simp: dist_norm inner_simps inner_Basis)
done
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
unfolding dist_norm
by auto
have "⋀i. i ∈ Basis ⟹ (x + (e / 2) *⇩R a) ∙ i = x∙i + (if i = a then e/2 else 0)"
using a D by (auto simp: inner_simps inner_Basis)
then have *: "sum ((∙) (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 ?p)"
using as assms
unfolding substd_simplex[OF assms] by fastforce
obtain a where a: "a ∈ D"
using ‹D ≠ {}› by auto
let ?d = "(1 - sum ((∙) x) D) / real (card D)"
have "0 < card D" using ‹D ≠ {}› ‹finite D›
have "Min (((∙) x) ` D) > 0"
using as ‹D ≠ {}› ‹finite D› by (simp add: Min_gr_iff)
moreover have "?d > 0" using as using ‹0 < card D› by auto
ultimately have h3: "min (Min (((∙) x) ` D)) ?d > 0"
by auto

have "x ∈ rel_interior (convex hull (insert 0 ?p))"
unfolding rel_interior_ball mem_Collect_eq h0
apply (rule,rule h2)
unfolding substd_simplex[OF assms]
apply (rule_tac x="min (Min (((∙) x) ` D)) ?d" in exI)
apply (rule, rule h3)
apply safe
unfolding mem_ball
proof -
fix y :: 'a
assume y: "dist x y < min (Min ((∙) x ` D)) ?d"
assume y2: "∀i∈Basis. i ∉ D ⟶ y∙i = 0"
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  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[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
using 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 (insert y2, auto)
qed
}
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 ?D = D
let ?a = "sum (λb::'a::euclidean_space. inverse (2 * real (card D)) *⇩R b) ?D"
have "finite D"
apply (rule finite_subset)
using assms(2)
apply auto
done
then have d1: "0 < real (card D)"
using ‹D ≠ {}› by auto
{
fix i
assume "i ∈ D"
have "?a ∙ i = inverse (2 * real (card D))"
apply (rule trans[of _ "sum (λj. if i = j then inverse (2 * real (card D)) else 0) ?D"])
unfolding inner_sum_left
apply (rule sum.cong)
using ‹i ∈ D› ‹finite D› sum.delta'[of D i "(λk. inverse (2 * real (card D)))"]
d1 assms(2)
by (auto simp: inner_Basis set_rev_mp[OF _ assms(2)])
}
note ** = this
show ?thesis
apply (rule that[of ?a])
unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq
proof safe
fix i
assume "i ∈ D"
have "0 < inverse (2 * real (card D))"
using d1 by auto
also have "… = ?a ∙ i" using **[of i] ‹i ∈ D›
by auto
finally show "0 < ?a ∙ i" by auto
next
have "sum ((∙) ?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

subsection%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)"
apply (rule  rel_interior_injective_on_span_linear_image[of f "(convex hull insert 0 B)"])
using ‹bounded_linear f› fd *
apply auto
done
ultimately have "rel_interior (convex hull insert 0 B) ≠ {}"
using rel_interior_substd_simplex_nonempty[OF ‹d ≠ {}› d]
apply auto
apply blast
done
moreover have "convex hull (insert 0 B) ⊆ S"
using B assms hull_mono[of "insert 0 B" "S" "convex"] convex_hull_eq
by auto
ultimately show ?thesis
using subset_rel_interior[of "convex hull insert 0 B" S] ** by auto
qed

lemma rel_interior_eq_empty:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "rel_interior S = {} ⟷ S = {}"
proof -
{
assume "S ≠ {}"
then obtain a where "a ∈ S" by auto
then have "0 ∈ (+) (-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 by auto
}
then show ?thesis
using rel_interior_empty by auto
qed

lemma interior_simplex_nonempty:
fixes S :: "'N :: euclidean_space set"
assumes "independent S" "finite S" "card S = DIM('N)"
obtains a where "a ∈ interior (convex hull (insert 0 S))"
proof -
have "affine hull (insert 0 S) = UNIV"
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"
apply (rule_tac x="x - e1 *⇩R (x - a)" in exI)
using * e1 dist_norm[of "x - e1 *⇩R (x - a)" x] ‹x ≠ a›
apply simp
done
}
then have "x islimpt rel_interior S"
unfolding islimpt_approachable_le by auto
then have "x ∈ closure(rel_interior S)"
unfolding closure_def by auto
}
ultimately have "x ∈ closure(rel_interior S)" by auto
}
then show ?thesis using h1 by auto
next
case True
then have "rel_interior S = {}"
using rel_interior_empty by auto
then have "closure (rel_interior S) = {}"
using closure_empty by auto
with True show ?thesis by auto
qed
qed

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

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

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

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

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

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

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

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

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

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

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

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

lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment

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

subsection‹The relative frontier of a set›

definition%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
apply simp
by (metis centre_in_ball empty_iff frontier_cball frontier_def interior_cball interior_rel_interior_gen rel_frontier_def)
qed

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

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

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

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

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

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

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

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

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

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

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

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

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"
apply (rule affine_dim_equal)
using * affine_affine_hull
apply auto
using ‹S1 ≠ {}› hull_subset[of S1]
apply auto
using eq aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2]
apply auto
done
obtain a where a: "a ∈ rel_interior S1"
using ‹S1 ≠ {}› rel_interior_eq_empty assms by auto
obtain T where T: "open T" "a ∈ T ∩ S1" "T ∩ affine hull S1 ⊆ S1"
using mem_rel_interior[of a S1] a by auto
then have "a ∈ T ∩ closure S2"
using a assms unfolding rel_frontier_def by auto
then obtain b where b: "b ∈ T ∩ rel_interior S2"
using open_inter_closure_rel_interior[of S2 T] assms T by auto
then have "b ∈ affine hull S1"
using rel_interior_subset hull_subset[of S2] ** by auto
then have "b ∈ S1"
using T b by auto
then have False
using b assms unfolding rel_frontier_def by auto
}
ultimately show ?thesis
using less_le by auto
qed

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

subsubsection%unimportant ‹Relative interior and closure under common operations›

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

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

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

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

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

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

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

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

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

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

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

lemma connected_component_1:
fixes S :: "real set"
shows "connected_component S a b ⟷ closed_segment a b ⊆ S"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsubsection%unimportant ‹Relative interior of convex cone›

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

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

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

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

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

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

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

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

subsection%unimportant ‹Convexity on direct sums›

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

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

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

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

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

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

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

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

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

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

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

have "(f x - f y) / (x - y) ≤ Inf (?F x)"
proof (rule cInf_greatest)
have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
using ‹y < x› by (auto simp: field_simps)
also
fix z
assume "z ∈ ?F x"
with order_trans[OF convex_on_diff[OF ‹convex_on I f› ‹y ∈ I› _ ‹y < x›]]
have "(f y - f x) / (y - x) ≤ z"
by auto
finally show "(f x - f y) / (x - y) ≤ z" .
next
have "open (interior I)" by auto
from openE[OF this ‹x ∈ interior I›]
obtain e where e: "0 < e" "ball x e ⊆ interior I" .
then have "x + e / 2 ∈ ball x e"
by (auto simp: dist_real_def)
with e interior_subset[of I] have "x + e / 2 ∈ {x<..} ∩ I"
by auto
then show "?F x ≠ {}"
by blast
qed
then show ?thesis
using ‹y < x› by (simp add: field_simps)
qed simp

subsection%unimportant‹Explicit formulas for interior and relative interior of convex hull›

lemma at_within_cbox_finite:
assumes "x ∈ box a b" "x ∉ S" "finite S"
shows "(at x within cbox a b - S) = at x"
proof -
have "interior (cbox a b - S) = box a b - S"
using ‹finite S› by (simp add: interior_diff finite_imp_closed)
then show ?thesis
using at_within_interior assms by fastforce
qed

lemma affine_independent_convex_affine_hull:
fixes s :: "'a::euclidean_space set"
assumes "~affine_dependent s" "t ⊆ s"
shows "convex hull t = affine hull t ∩ convex hull s"
proof -
have fin: "finite s" "finite t" using assms aff_independent_finite finite_subset by auto
{ fix u v x
assume uv: "sum u t = 1" "∀x∈s. 0 ≤ v x" "sum v s = 1"
"(∑x∈s. v x *⇩R x) = (∑v∈t. u v *⇩R v)" "x ∈ t"
then have s: "s = (s - t) ∪ t" ― ‹split into separate cases›
using assms by auto
have [simp]: "(∑x∈t. v x *⇩R x) + (∑x∈s - t. v x *⇩R x) = (∑x∈t. u x *⇩R x)"
"sum v t + sum v (s - t) = 1"
using uv fin s
by (auto simp: sum.union_disjoint [symmetric] Un_commute)
have "(∑x∈s. if x ∈ t then v x - u x else v x) = 0"
"(∑x∈s. (if x ∈ t then v x - u x else v x) *⇩R x) = 0"
using uv fin
by (subst s, subst sum.union_disjoint, auto simp: algebra_simps sum_subtractf)+
} note [simp] = this
have "convex hull t ⊆ affine hull t"
using convex_hull_subset_affine_hull by blast
moreover have "convex hull t ⊆ convex hull s"
using assms hull_mono by blast
moreover have "affine hull t ∩ convex hull s ⊆ convex hull t"
using assms
apply (simp add: convex_hull_finite affine_hull_finite fin affine_dependent_explicit)
apply (drule_tac x=s in spec)
apply (auto simp: fin)
apply (rule_tac x=u in exI)
apply (rename_tac v)
apply (drule_tac x="λx. if x ∈ t then v x - u x else v x" in spec)
apply (force)+
done
ultimately show ?thesis
by blast
qed

lemma affine_independent_span_eq:
fixes s :: "'a::euclidean_space set"
assumes "~affine_dependent s" "card s = Suc (DIM ('a))"
shows "affine hull s = UNIV"
proof (cases "s = {}")
case True then show ?thesis
using assms by simp
next
case False
then obtain a t where t: "a ∉ t" "s = insert a t"
by blast
then have fin: "finite t" using assms
by (metis finite_insert aff_independent_finite)
show ?thesis
using assms t fin
apply (rule subset_antisym)
apply force
apply (rule Fun.vimage_subsetD)
apply (rule card_ge_dim_independent)
apply (auto simp: card_image inj_on_def dim_subset_UNIV)
done
qed

lemma affine_independent_span_gt:
fixes s :: "'a::euclidean_space set"
assumes ind: "~ affine_dependent s" and dim: "DIM ('a) < card s"
shows "affine hull s = UNIV"
apply (rule affine_independent_span_eq [OF ind])
apply (rule antisym)
using assms
apply auto
apply (metis add_2_eq_Suc' not_less_eq_eq affine_dependent_biggerset aff_independent_finite)
done

lemma empty_interior_affine_hull:
fixes s :: "'a::euclidean_space set"
assumes "finite s" and dim: "card s ≤ DIM ('a)"
shows "interior(affine hull s) = {}"
using assms
apply (induct s rule: finite_induct)
apply (simp_all add:  affine_dependent_iff_dependent affine_hull_insert_span_gen interior_translation)
apply (rule empty_interior_lowdim)
by (auto simp: Suc_le_lessD card_image_le dual_order.trans intro!: dim_le_card'[THEN le_less_trans])

lemma empty_interior_convex_hull:
fixes s :: "'a::euclidean_space set"
assumes "finite s" and dim: "card s ≤ DIM ('a)"
shows "interior(convex hull s) = {}"
by (metis Diff_empty Diff_eq_empty_iff convex_hull_subset_affine_hull
interior_mono empty_interior_affine_hull [OF assms])

lemma explicit_subset_rel_interior_convex_hull:
fixes s :: "'a::euclidean_space set"
shows "finite s
⟹ {y. ∃u. (∀x ∈ s. 0 < u x ∧ u x < 1) ∧ sum u s = 1 ∧ sum (λx. u x *⇩R x) s = y}
⊆ rel_interior (convex hull s)"
by (force simp add:  rel_interior_convex_hull_union [where S="λx. {x}" and I=s, simplified])

lemma explicit_subset_rel_interior_convex_hull_minimal:
fixes s :: "'a::euclidean_space set"
shows "finite s
⟹ {y. ∃u. (∀x ∈ s. 0 < u x) ∧ sum u s = 1 ∧ sum (λx. u x *⇩R x) s = y}
⊆ rel_interior (convex hull s)"
by (force simp add:  rel_interior_convex_hull_union [where S="λx. {x}" and I=s, simplified])

lemma rel_interior_convex_hull_explicit:
fixes s :: "'a::euclidean_space set"
assumes "~ affine_dependent s"
shows "rel_interior(convex hull s) =
{y. ∃u. (∀x ∈ s. 0 < u x) ∧ sum u s = 1 ∧ sum (λx. u x *⇩R x) s = y}"
(is "?lhs = ?rhs")
proof
show "?rhs ≤ ?lhs"
by (simp add: aff_independent_finite explicit_subset_rel_interior_convex_hull_minimal assms)
next
show "?lhs ≤ ?rhs"
proof (cases "∃a. s = {a}")
case True then show "?lhs ≤ ?rhs"
by force
next
case False
have fs: "finite s"
using assms by (simp add: aff_independent_finite)
{ fix a b and d::real
assume ab: "a ∈ s" "b ∈ s" "a ≠ b"
then have s: "s = (s - {a,b}) ∪ {a,b}" ― ‹split into separate cases›
by auto
have "(∑x∈s. if x = a then - d else if x = b then d else 0) = 0"
"(∑x∈s. (if x = a then - d else if x = b then d else 0) *⇩R x) = d *⇩R b - d *⇩R a"
using ab fs
by (subst s, subst sum.union_disjoint, auto)+
} note [simp] = this
{ fix y
assume y: "y ∈ convex hull s" "y ∉ ?rhs"
{ fix u T a
assume ua: "∀x∈s. 0 ≤ u x" "sum u s = 1" "¬ 0 < u a" "a ∈ s"
and yT: "y = (∑x∈s. u x *⇩R x)" "y ∈ T" "open T"
and sb: "T ∩ affine hull s ⊆ {w. ∃u. (∀x∈s. 0 ≤ u x) ∧ sum u s = 1 ∧ (∑x∈s. u x *⇩R x) = w}"
have ua0: "u a = 0"
using ua by auto
obtain b where b: "b∈s" "a ≠ b"
using ua False by auto
obtain e where e: "0 < e" "ball (∑x∈s. u x *⇩R x) e ⊆ T"
using yT by (auto elim: openE)
with b obtain d where d: "0 < d" "norm(d *⇩R (a-b)) < e"
by (auto intro: that [of "e / 2 / norm(a-b)"])
have "(∑x∈s. u x *⇩R x) ∈ affine hull s"
using yT y by (metis affine_hull_convex_hull hull_redundant_eq)
then have "(∑x∈s. u x *⇩R x) - d *⇩R (a - b) ∈ affine hull s"
using ua b by (auto simp: hull_inc intro: mem_affine_3_minus2)
then have "y - d *⇩R (a - b) ∈ T ∩ affine hull s"
using d e yT by auto
then obtain v where "∀x∈s. 0 ≤ v x"
"sum v s = 1"
"(∑x∈s. v x *⇩R x) = (∑x∈s. u x *⇩R x) - d *⇩R (a - b)"
using subsetD [OF sb] yT
by auto
then have False
using assms
apply (drule_tac x="λx. (v x - u x) - (if x = a then -d else if x = b then d else 0)" in spec)
using ua b d
apply (auto simp: algebra_simps sum_subtractf sum.distrib)
done
} note * = this
have "y ∉ rel_interior (convex hull s)"
using y
apply (auto simp: convex_hull_finite [OF fs])
apply (drule_tac x=u in spec)
apply (auto intro: *)
done
} with rel_interior_subset show "?lhs ≤ ?rhs"
by blast
qed
qed

lemma interior_convex_hull_explicit_minimal:
fixes s :: "'a::euclidean_space set"
shows
"~ affine_dependent s
==> interior(convex hull s) =
(if card(s) ≤ DIM('a) then {}
else {y. ∃u. (∀x ∈ s. 0 < u x) ∧ sum u s = 1 ∧ (∑x∈s. u x *⇩R x) = y})"
apply (simp add: aff_independent_finite empty_interior_convex_hull, clarify)
apply (rule trans [of _ "rel_interior(convex hull s)"])
apply (simp add: affine_hull_convex_hull affine_independent_span_gt rel_interior_interior)

lemma interior_convex_hull_explicit:
fixes s :: "'a::euclidean_space set"
assumes "~ affine_dependent s"
shows
"interior(convex hull s) =
(if card(s) ≤ DIM('a) then {}
else {y. ∃u. (∀x ∈ s. 0 < u x ∧ u x < 1) ∧ sum u s = 1 ∧ (∑x∈s. u x *⇩R x) = y})"
proof -
{ fix u :: "'a ⇒ real" and a
assume "card Basis < card s" and u: "⋀x. x∈s ⟹ 0 < u x" "sum u s = 1" and a: "a ∈ s"
then have cs: "Suc 0 < card s"
by (metis DIM_positive less_trans_Suc)
obtain b where b: "b ∈ s" "a ≠ b"
proof (cases "s ≤ {a}")
case True
then show thesis
using cs subset_singletonD by fastforce
next
case False
then show thesis
by (blast intro: that)
qed
have "u a + u b ≤ sum u {a,b}"
using a b by simp
also have "... ≤ sum u s"
apply (rule Groups_Big.sum_mono2)
using a b u
apply (auto simp: less_imp_le aff_independent_finite assms)
done
finally have "u a < 1"
using ‹b ∈ s› u by fastforce
} note [simp] = this
show ?thesis
using assms
apply (auto simp: interior_convex_hull_explicit_minimal)
apply (rule_tac x=u in exI)
apply (auto simp: not_le)
done
qed

lemma interior_closed_segment_ge2:
fixes a :: "'a::euclidean_space"
assumes "2 ≤ DIM('a)"
shows  "interior(closed_segment a b) = {}"
using assms unfolding segment_convex_hull
proof -
have "card {a, b} ≤ DIM('a)"
using assms
by (simp add: card_insert_if linear not_less_eq_eq numeral_2_eq_2)
then show "interior (convex hull {a, b}) = {}"
by (metis empty_interior_convex_hull finite.insertI finite.emptyI)
qed

lemma interior_open_segment:
fixes a :: "'a::euclidean_space"
shows  "interior(open_segment a b) =
(if 2 ≤ DIM('a) then {} else open_segment a b)"
proof (simp add: not_le, intro conjI impI)
assume "2 ≤ DIM('a)"
then show "interior (open_segment a b) = {}"
apply (metis Diff_subset interior_mono segment_convex_hull subset_empty interior_closed_segment_ge2)
done
next
assume le2: "DIM('a) < 2"
show "interior (open_segment a b) = open_segment a b"
proof (cases "a = b")
case True then show ?thesis by auto
next
case False
with le2 have "affine hull (open_segment a b) = UNIV"
apply simp
apply (rule affine_independent_span_gt)
done
then show "interior (open_segment a b) = open_segment a b"
using rel_interior_interior rel_interior_open_segment by blast
qed
qed

lemma interior_closed_segment:
fixes a :: "'a::euclidean_space"
shows "interior(closed_segment a b) =
(if 2 ≤ DIM('a) then {} else open_segment a b)"
proof (cases "a = b")
case True then show ?thesis by simp
next
case False
then have "closure (open_segment a b) = closed_segment a b"
by simp
then show ?thesis
by (metis (no_types) convex_interior_closure convex_open_segment interior_open_segment)
qed

lemmas interior_segment = interior_closed_segment interior_open_segment

lemma closed_segment_eq [simp]:
fixes a :: "'a::euclidean_space"
shows "closed_segment a b = closed_segment c d ⟷ {a,b} = {c,d}"
proof
assume abcd: "closed_segment a b = closed_segment c d"
show "{a,b} = {c,d}"```