# Theory Polytope

```section ‹Faces, Extreme Points, Polytopes, Polyhedra etc›

text‹Ported from HOL Light by L C Paulson›

theory Polytope
imports Cartesian_Euclidean_Space Path_Connected
begin

subsection ‹Faces of a (usually convex) set›

definition✐‹tag important› face_of :: "['a::real_vector set, 'a set] ⇒ bool" (infixr "(face'_of)" 50)
where
"T face_of S ⟷
T ⊆ S ∧ convex T ∧
(∀a ∈ S. ∀b ∈ S. ∀x ∈ T. x ∈ open_segment a b ⟶ a ∈ T ∧ b ∈ T)"

lemma face_ofD: "⟦T face_of S; x ∈ open_segment a b; a ∈ S; b ∈ S; x ∈ T⟧ ⟹ a ∈ T ∧ b ∈ T"
unfolding face_of_def by blast

lemma face_of_translation_eq [simp]:
"((+) a ` T face_of (+) a ` S) ⟷ T face_of S"
proof -
have *: "⋀a T S. T face_of S ⟹ ((+) a ` T face_of (+) a ` S)"
show ?thesis
by (force simp: image_comp o_def dest: * [where a = "-a"] intro: *)
qed

lemma face_of_linear_image:
assumes "linear f" "inj f"
shows "(f ` c face_of f ` S) ⟷ c face_of S"
by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)

lemma faces_of_linear_image:
"⟦linear f; inj f⟧ ⟹ {T. T face_of (f ` S)} = (image f) ` {T. T face_of S}"
by (smt (verit) Collect_cong face_of_def face_of_linear_image setcompr_eq_image subset_imageE)

lemma face_of_refl: "convex S ⟹ S face_of S"
by (auto simp: face_of_def)

lemma face_of_refl_eq: "S face_of S ⟷ convex S"
by (auto simp: face_of_def)

lemma empty_face_of [iff]: "{} face_of S"

lemma face_of_empty [simp]: "S face_of {} ⟷ S = {}"
by (meson empty_face_of face_of_def subset_empty)

lemma face_of_trans [trans]: "⟦S face_of T; T face_of u⟧ ⟹ S face_of u"
unfolding face_of_def by (safe; blast)

lemma face_of_face: "T face_of S ⟹ (f face_of T ⟷ f face_of S ∧ f ⊆ T)"
unfolding face_of_def by (safe; blast)

lemma face_of_subset: "⟦F face_of S; F ⊆ T; T ⊆ S⟧ ⟹ F face_of T"
unfolding face_of_def by (safe; blast)

lemma face_of_slice: "⟦F face_of S; convex T⟧ ⟹ (F ∩ T) face_of (S ∩ T)"
unfolding face_of_def by (blast intro: convex_Int)

lemma face_of_Int: "⟦t1 face_of S; t2 face_of S⟧ ⟹ (t1 ∩ t2) face_of S"
unfolding face_of_def by (blast intro: convex_Int)

lemma face_of_Inter: "⟦A ≠ {}; ⋀T. T ∈ A ⟹ T face_of S⟧ ⟹ (⋂ A) face_of S"
unfolding face_of_def by (blast intro: convex_Inter)

lemma face_of_Int_Int: "⟦F face_of T; F' face_of t'⟧ ⟹ (F ∩ F') face_of (T ∩ t')"
unfolding face_of_def by (blast intro: convex_Int)

lemma face_of_imp_subset: "T face_of S ⟹ T ⊆ S"
unfolding face_of_def by blast

proposition face_of_imp_eq_affine_Int:
fixes S :: "'a::euclidean_space set"
assumes S: "convex S"  and T: "T face_of S"
shows "T = (affine hull T) ∩ S"
proof -
have "convex T" using T by (simp add: face_of_def)
have *: False if x: "x ∈ affine hull T" and "x ∈ S" "x ∉ T" and y: "y ∈ rel_interior T" for x y
proof -
obtain e where "e>0" and e: "cball y e ∩ affine hull T ⊆ T"
using y by (auto simp: rel_interior_cball)
have "y ≠ x" "y ∈ S" "y ∈ T"
using face_of_imp_subset rel_interior_subset T that by blast+
then have zne: "⋀u. ⟦u ∈ {0<..<1}; (1 - u) *⇩R y + u *⇩R x ∈ T⟧ ⟹ False"
using ‹x ∈ S› ‹x ∉ T› ‹T face_of S› unfolding face_of_def
by (meson greaterThanLessThan_iff in_segment(2))
define u where "u ≡ min (1/2) (e / norm (x - y))"
have in01: "u ∈ {0<..<1}"
using ‹y ≠ x› ‹e > 0› by (simp add: u_def)
have "norm (u *⇩R y - u *⇩R x) ≤ e"
using ‹e > 0›
by (simp add: u_def norm_minus_commute min_mult_distrib_right flip: scaleR_diff_right)
then have "dist y ((1 - u) *⇩R y + u *⇩R x) ≤ e"
then show False
using zne [OF in01 e [THEN subsetD]] by (simp add: ‹y ∈ T› hull_inc mem_affine x)
qed
show ?thesis
proof (rule subset_antisym)
show "T ⊆ affine hull T ∩ S"
using assms by (simp add: hull_subset face_of_imp_subset)
show "affine hull T ∩ S ⊆ T"
using "*" ‹convex T› rel_interior_eq_empty by fastforce
qed
qed

lemma face_of_imp_closed:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "closed S" "T face_of S" shows "closed T"
by (metis affine_affine_hull affine_closed closed_Int face_of_imp_eq_affine_Int assms)

lemma face_of_Int_supporting_hyperplane_le_strong:
assumes "convex(S ∩ {x. a ∙ x = b})" and aleb: "⋀x. x ∈ S ⟹ a ∙ x ≤ b"
shows "(S ∩ {x. a ∙ x = b}) face_of S"
proof -
have *: "a ∙ u = a ∙ x" if "x ∈ open_segment u v" "u ∈ S" "v ∈ S" and b: "b = a ∙ x"
for u v x
proof (rule antisym)
show "a ∙ u ≤ a ∙ x"
using aleb ‹u ∈ S› ‹b = a ∙ x› by blast
next
obtain ξ where "b = a ∙ ((1 - ξ) *⇩R u + ξ *⇩R v)" "0 < ξ" "ξ < 1"
using ‹b = a ∙ x› ‹x ∈ open_segment u v› in_segment
by (auto simp: open_segment_image_interval split: if_split_asm)
then have "b + ξ * (a ∙ u) ≤ a ∙ u + ξ * b"
using aleb [OF ‹v ∈ S›] by (simp add: algebra_simps)
then have "(1 - ξ) * b ≤ (1 - ξ) * (a ∙ u)"
then have "b ≤ a ∙ u"
using ‹ξ < 1› by auto
with b show "a ∙ x ≤ a ∙ u" by simp
qed
show ?thesis
using "*" open_segment_commute by (fastforce simp add: face_of_def assms)
qed

lemma face_of_Int_supporting_hyperplane_ge_strong:
"⟦convex(S ∩ {x. a ∙ x = b}); ⋀x. x ∈ S ⟹ a ∙ x ≥ b⟧
⟹ (S ∩ {x. a ∙ x = b}) face_of S"
using face_of_Int_supporting_hyperplane_le_strong [of S "-a" "-b"] by simp

lemma face_of_Int_supporting_hyperplane_le:
"⟦convex S; ⋀x. x ∈ S ⟹ a ∙ x ≤ b⟧ ⟹ (S ∩ {x. a ∙ x = b}) face_of S"
by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_le_strong)

lemma face_of_Int_supporting_hyperplane_ge:
"⟦convex S; ⋀x. x ∈ S ⟹ a ∙ x ≥ b⟧ ⟹ (S ∩ {x. a ∙ x = b}) face_of S"
by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_ge_strong)

lemma face_of_imp_convex: "T face_of S ⟹ convex T"
using face_of_def by blast

lemma face_of_imp_compact:
fixes S :: "'a::euclidean_space set"
shows "⟦convex S; compact S; T face_of S⟧ ⟹ compact T"
by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset)

lemma face_of_Int_subface:
"⟦A ∩ B face_of A; A ∩ B face_of B; C face_of A; D face_of B⟧
⟹ (C ∩ D) face_of C ∧ (C ∩ D) face_of D"
by (meson face_of_Int_Int face_of_face inf_le1 inf_le2)

lemma subset_of_face_of:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "u ⊆ S" "T ∩ (rel_interior u) ≠ {}"
shows "u ⊆ T"
proof
fix c
assume "c ∈ u"
obtain b where "b ∈ T" "b ∈ rel_interior u" using assms by auto
then obtain e where "e>0" "b ∈ u" and e: "cball b e ∩ affine hull u ⊆ u"
by (auto simp: rel_interior_cball)
show "c ∈ T"
proof (cases "b=c")
case True with ‹b ∈ T› show ?thesis by blast
next
case False
define d where "d = b + (e / norm(b - c)) *⇩R (b - c)"
have "d ∈ cball b e ∩ affine hull u"
using ‹e > 0› ‹b ∈ u› ‹c ∈ u›
by (simp add: d_def dist_norm hull_inc mem_affine_3_minus False)
with e have "d ∈ u" by blast
have nbc: "norm (b - c) + e > 0" using ‹e > 0›
then have [simp]: "d ≠ c" using False scaleR_cancel_left [of "1 + (e / norm (b - c))" b c]
have [simp]: "((e - e * e / (e + norm (b - c))) / norm (b - c)) = (e / (e + norm (b - c)))"
using False nbc
have "b ∈ open_segment d c"
apply (rule_tac x="e / (e + norm (b - c))" in image_eqI)
using False nbc ‹0 < e› by (auto simp: algebra_simps)
then have "d ∈ T ∧ c ∈ T"
by (meson ‹b ∈ T› ‹c ∈ u› ‹d ∈ u› assms face_ofD subset_iff)
then show ?thesis ..
qed
qed

lemma face_of_eq:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "U face_of S" "(rel_interior T) ∩ (rel_interior U) ≠ {}"
shows "T = U"
using assms
unfolding disjoint_iff_not_equal
by (metis IntI empty_iff face_of_imp_subset mem_rel_interior_ball subset_antisym subset_of_face_of)

lemma face_of_disjoint_rel_interior:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "T ≠ S"
shows "T ∩ rel_interior S = {}"
by (meson assms subset_of_face_of face_of_imp_subset order_refl subset_antisym)

lemma face_of_disjoint_interior:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "T ≠ S"
shows "T ∩ interior S = {}"
using assms face_of_disjoint_rel_interior interior_subset_rel_interior by fastforce

lemma face_of_subset_rel_boundary:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "T ≠ S"
shows "T ⊆ (S - rel_interior S)"
by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset subset_iff)

lemma face_of_subset_rel_frontier:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "T ≠ S"
shows "T ⊆ rel_frontier S"
using assms closure_subset face_of_disjoint_rel_interior face_of_imp_subset rel_frontier_def by fastforce

lemma face_of_aff_dim_lt:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "T face_of S" "T ≠ S"
shows "aff_dim T < aff_dim S"
proof -
have "aff_dim T ≤ aff_dim S"
by (simp add: face_of_imp_subset aff_dim_subset assms)
moreover have "aff_dim T ≠ aff_dim S"
by (metis aff_dim_empty assms convex_rel_frontier_aff_dim face_of_imp_convex
face_of_subset_rel_frontier order_less_irrefl)
ultimately show ?thesis
by simp
qed

lemma subset_of_face_of_affine_hull:
fixes S :: "'a::euclidean_space set"
assumes T: "T face_of S" and "convex S" "U ⊆ S" and dis: "¬ disjnt (affine hull T) (rel_interior U)"
shows "U ⊆ T"
proof (rule subset_of_face_of [OF T ‹U ⊆ S›])
show "T ∩ rel_interior U ≠ {}"
using face_of_imp_eq_affine_Int [OF ‹convex S› T] rel_interior_subset dis ‹U ⊆ S› disjnt_def
by fastforce
qed

lemma affine_hull_face_of_disjoint_rel_interior:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "F face_of S" "F ≠ S"
shows "affine hull F ∩ rel_interior S = {}"
by (meson antisym assms disjnt_def equalityD2 face_of_def subset_of_face_of_affine_hull)

lemma affine_diff_divide:
assumes "affine S" "k ≠ 0" "k ≠ 1" and xy: "x ∈ S" "y /⇩R (1 - k) ∈ S"
shows "(x - y) /⇩R k ∈ S"
proof -
have "inverse(k) *⇩R (x - y) = (1 - inverse k) *⇩R inverse(1 - k) *⇩R y + inverse(k) *⇩R x"
using assms
then show ?thesis
using ‹affine S› xy by (auto simp: affine_alt)
qed

proposition face_of_conic:
assumes "conic S" "f face_of S"
shows "conic f"
unfolding conic_def
proof (intro strip)
fix x and c::real
assume "x ∈ f" and "0 ≤ c"
have f: "⋀a b x. ⟦a ∈ S; b ∈ S; x ∈ f; x ∈ open_segment a b⟧ ⟹ a ∈ f ∧ b ∈ f"
using ‹f face_of S› face_ofD by blast
show "c *⇩R x ∈ f"
proof (cases "x=0 ∨ c=1")
case True
then show ?thesis
using ‹x ∈ f› by auto
next
case False
with ‹0 ≤ c› obtain d e where de: "0 ≤ d" "0 ≤ e" "d < 1" "1 < e" "d < e" "(d = c ∨ e = c)"
by (metis gt_ex less_eq_real_def order_less_le_trans zero_less_one)
then obtain [simp]: "c *⇩R x ∈ S" "e *⇩R x ∈ S" ‹x ∈ S›
using ‹x ∈ f› assms conic_mul face_of_imp_subset by blast
have "x ∈ open_segment (d *⇩R x) (e *⇩R x)" if "c *⇩R x ∉ f"
using de False that
apply (rule_tac x="(1 - d) / (e - d)" in exI)
by (smt (verit, del_insts) add_divide_distrib divide_self scaleR_collapse)
then show ?thesis
using ‹conic S› f [of "d *⇩R x" "e *⇩R x" x] de ‹x ∈ f›
by (force simp: conic_def in_segment)
qed
qed

proposition face_of_convex_hulls:
assumes S: "finite S" "T ⊆ S" and disj: "affine hull T ∩ convex hull (S - T) = {}"
shows  "(convex hull T) face_of (convex hull S)"
proof -
have fin: "finite T" "finite (S - T)" using assms
by (auto simp: finite_subset)
have *: "x ∈ convex hull T"
if x: "x ∈ convex hull S" and y: "y ∈ convex hull S" and w: "w ∈ convex hull T" "w ∈ open_segment x y"
for x y w
proof -
have waff: "w ∈ affine hull T"
using convex_hull_subset_affine_hull w by blast
obtain a b where a: "⋀i. i ∈ S ⟹ 0 ≤ a i" and asum: "sum a S = 1" and aeqx: "(∑i∈S. a i *⇩R i) = x"
and b: "⋀i. i ∈ S ⟹ 0 ≤ b i" and bsum: "sum b S = 1" and beqy: "(∑i∈S. b i *⇩R i) = y"
using x y by (auto simp: assms convex_hull_finite)
obtain u where "(1 - u) *⇩R x + u *⇩R y ∈ convex hull T" "x ≠ y" and weq: "w = (1 - u) *⇩R x + u *⇩R y"
and u01: "0 < u" "u < 1"
using w by (auto simp: open_segment_image_interval split: if_split_asm)
define c where "c i = (1 - u) * a i + u * b i" for i
have cge0: "⋀i. i ∈ S ⟹ 0 ≤ c i"
using a b u01 by (simp add: c_def)
have sumc1: "sum c S = 1"
by (simp add: c_def sum.distrib sum_distrib_left [symmetric] asum bsum)
have sumci_xy: "(∑i∈S. c i *⇩R i) = (1 - u) *⇩R x + u *⇩R y"
apply (simp add: c_def sum.distrib scaleR_left_distrib)
by (simp only: scaleR_scaleR [symmetric] Real_Vector_Spaces.scaleR_right.sum [symmetric] aeqx beqy)
show ?thesis
proof (cases "sum c (S - T) = 0")
case True
have ci0: "⋀i. i ∈ (S - T) ⟹ c i = 0"
using True cge0 fin(2) sum_nonneg_eq_0_iff by auto
have a0: "a i = 0" if "i ∈ (S - T)" for i
using ci0 [OF that] u01 a [of i] b [of i] that
have  "sum a T = 1"
using assms by (metis sum.mono_neutral_cong_right a0 asum)
moreover have "(∑x∈T. a x *⇩R x) = x"
using a0 assms by (auto simp: cge0 a aeqx [symmetric] sum.mono_neutral_right)
ultimately show ?thesis
using a assms(2) by (auto simp add: convex_hull_finite ‹finite T› )
next
case False
define k where "k = sum c (S - T)"
have "k > 0" using False
unfolding k_def by (metis DiffD1 antisym_conv cge0 sum_nonneg not_less)
have weq_sumsum: "w = sum (λx. c x *⇩R x) T + sum (λx. c x *⇩R x) (S - T)"
by (metis (no_types) add.commute S(1) S(2) sum.subset_diff sumci_xy weq)
show ?thesis
proof (cases "k = 1")
case True
then have "sum c T = 0"
by (simp add: S k_def sum_diff sumc1)
then have "sum c (S - T) = 1"
by (simp add: S sum_diff sumc1)
moreover have ci0: "⋀i. i ∈ T ⟹ c i = 0"
by (meson ‹finite T› ‹sum c T = 0› ‹T ⊆ S› cge0 sum_nonneg_eq_0_iff subsetCE)
then have "(∑i∈S-T. c i *⇩R i) = w"
ultimately have "w ∈ convex hull (S - T)"
using cge0 by (auto simp add: convex_hull_finite fin)
then show ?thesis
using disj waff by blast
next
case False
then have sumcf: "sum c T = 1 - k"
by (simp add: S k_def sum_diff sumc1)
have "⋀x. x ∈ T ⟹ 0 ≤ inverse (1 - k) * c x"
by (metis ‹T ⊆ S› cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg subsetD sum_nonneg sumcf)
moreover have "(∑x∈T. inverse (1 - k) * c x) = 1"
by (metis False eq_iff_diff_eq_0 mult.commute right_inverse sum_distrib_left sumcf)
ultimately have "(∑i∈T. c i *⇩R i) /⇩R (1 - k) ∈ convex hull T"
by (metis (mono_tags, lifting) scaleR_right.sum scaleR_scaleR sum.cong)
with ‹0 < k›  have "inverse(k) *⇩R (w - sum (λi. c i *⇩R i) T) ∈ affine hull T"
by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
moreover have "inverse(k) *⇩R (w - sum (λx. c x *⇩R x) T) ∈ convex hull (S - T)"
apply (simp add: weq_sumsum convex_hull_finite fin)
apply (rule_tac x="λi. inverse k * c i" in exI)
using ‹k > 0› cge0
apply (auto simp: scaleR_right.sum simp flip: sum_distrib_left k_def)
done
ultimately show ?thesis
using disj by blast
qed
qed
qed
have [simp]: "convex hull T ⊆ convex hull S"
by (simp add: ‹T ⊆ S› hull_mono)
show ?thesis
using open_segment_commute by (auto simp: face_of_def intro: *)
qed

proposition face_of_convex_hull_insert:
assumes "finite S" "a ∉ affine hull S" and T: "T face_of convex hull S"
shows "T face_of convex hull insert a S"
proof -
have "convex hull S face_of convex hull insert a S"
by (simp add: assms face_of_convex_hulls insert_Diff_if subset_insertI)
then show ?thesis
using T face_of_trans by blast
qed

proposition face_of_affine_trivial:
assumes "affine S" "T face_of S"
shows "T = {} ∨ T = S"
proof (rule ccontr, clarsimp)
assume "T ≠ {}" "T ≠ S"
then obtain a where "a ∈ T" by auto
then have "a ∈ S"
using ‹T face_of S› face_of_imp_subset by blast
have "S ⊆ T"
proof
fix b  assume "b ∈ S"
show "b ∈ T"
proof (cases "a = b")
case True with ‹a ∈ T› show ?thesis by auto
next
case False
then have "a ∈ open_segment (2 *⇩R a - b) b"
by (metis diff_add_cancel inverse_eq_divide midpoint_def midpoint_in_open_segment
scaleR_2 scaleR_half_double)
moreover have "2 *⇩R a - b ∈ S"
by (rule mem_affine [OF ‹affine S› ‹a ∈ S› ‹b ∈ S›, of 2 "-1", simplified])
moreover note ‹b ∈ S› ‹a ∈ T›
ultimately show ?thesis
by (rule face_ofD [OF ‹T face_of S›, THEN conjunct2])
qed
qed
then show False
using ‹T ≠ S› ‹T face_of S› face_of_imp_subset by blast
qed

lemma face_of_affine_eq:
"affine S ⟹ (T face_of S ⟷ T = {} ∨ T = S)"
using affine_imp_convex face_of_affine_trivial face_of_refl by auto

proposition Inter_faces_finite_altbound:
fixes T :: "'a::euclidean_space set set"
assumes cfaI: "⋀c. c ∈ T ⟹ c face_of S"
shows "∃F'. finite F' ∧ F' ⊆ T ∧ card F' ≤ DIM('a) + 2 ∧ ⋂F' = ⋂T"
proof (cases "∀F'. finite F' ∧ F' ⊆ T ∧ card F' ≤ DIM('a) + 2 ⟶ (∃c. c ∈ T ∧ c ∩ (⋂F') ⊂ (⋂F'))")
case True
then obtain c where c:
"⋀F'. ⟦finite F'; F' ⊆ T; card F' ≤ DIM('a) + 2⟧ ⟹ c F' ∈ T ∧ c F' ∩ (⋂F') ⊂ (⋂F')"
by metis
define d where "d ≡ λn. ((λr. insert (c r) r)^^n) {c{}}"
note d_def [simp]
have dSuc: "⋀n. d (Suc n) = insert (c (d n)) (d n)"
by simp
have dn_notempty: "d n ≠ {}" for n
by (induction n) auto
have dn_le_Suc: "d n ⊆ T ∧ finite(d n) ∧ card(d n) ≤ Suc n" if "n ≤ DIM('a) + 2" for n
using that
proof (induction n)
case 0
then show ?case by (simp add: c)
next
case (Suc n)
then show ?case by (auto simp: c card_insert_if)
qed
have aff_dim_le: "aff_dim(⋂(d n)) ≤ DIM('a) - int n" if "n ≤ DIM('a) + 2" for n
using that
proof (induction n)
case 0
then show ?case
next
case (Suc n)
have fs: "⋂(d (Suc n)) face_of S"
by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE)
have condn: "convex (⋂(d n))"
using Suc.prems nat_le_linear not_less_eq_eq
by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc)
have fdn: "⋂(d (Suc n)) face_of ⋂(d n)"
by (metis (no_types, lifting) Inter_anti_mono Suc.prems dSuc cfaI dn_le_Suc dn_notempty face_of_Inter face_of_imp_subset face_of_subset subset_iff subset_insertI)
have ne: "⋂(d (Suc n)) ≠ ⋂(d n)"
by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans)
have *: "⋀m::int. ⋀d. ⋀d'::int. d < d' ∧ d' ≤ m - n ⟹ d ≤ m - of_nat(n+1)"
by arith
have "aff_dim (⋂(d (Suc n))) < aff_dim (⋂(d n))"
by (rule face_of_aff_dim_lt [OF condn fdn ne])
moreover have "aff_dim (⋂(d n)) ≤ int (DIM('a)) - int n"
using Suc by auto
ultimately
have "aff_dim (⋂(d (Suc n))) ≤ int (DIM('a)) - (n+1)" by arith
then show ?case by linarith
qed
have "aff_dim (⋂(d (DIM('a) + 2))) ≤ -2"
using aff_dim_le [OF order_refl] by simp
with aff_dim_geq [of "⋂(d (DIM('a) + 2))"] show ?thesis
using order.trans by fastforce
next
case False
then show ?thesis by fastforce
qed

lemma faces_of_translation:
"{F. F face_of (+) a ` S} = (image ((+) a)) ` {F. F face_of S}"
proof -
have "⋀F. F face_of (+) a ` S ⟹ ∃G. G face_of S ∧ F = (+) a ` G"
by (metis face_of_imp_subset face_of_translation_eq subset_imageE)
then show ?thesis
by (auto simp: image_iff)
qed

proposition face_of_Times:
assumes "F face_of S" and "F' face_of S'"
shows "(F × F') face_of (S × S')"
proof -
have "F × F' ⊆ S × S'"
using assms [unfolded face_of_def] by blast
moreover
have "convex (F × F')"
using assms [unfolded face_of_def] by (blast intro: convex_Times)
moreover
have "a ∈ F ∧ a' ∈ F' ∧ b ∈ F ∧ b' ∈ F'"
if "a ∈ S" "b ∈ S" "a' ∈ S'" "b' ∈ S'" "x ∈ F × F'" "x ∈ open_segment (a,a') (b,b')"
for a b a' b' x
proof (cases "b=a ∨ b'=a'")
case True with that show ?thesis
using assms
by (force simp: in_segment dest: face_ofD)
next
case False with assms [unfolded face_of_def] that show ?thesis
by (blast dest!: open_segment_PairD)
qed
ultimately show ?thesis
unfolding face_of_def by blast
qed

corollary face_of_Times_decomp:
fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
shows "C face_of (S × S') ⟷ (∃F F'. F face_of S ∧ F' face_of S' ∧ C = F × F')"
(is "?lhs = ?rhs")
proof
assume C: ?lhs
show ?rhs
proof (cases "C = {}")
case True then show ?thesis by auto
next
case False
have 1: "fst ` C ⊆ S" "snd ` C ⊆ S'"
using C face_of_imp_subset by fastforce+
have "convex C"
using C by (metis face_of_imp_convex)
have conv: "convex (fst ` C)" "convex (snd ` C)"
by (simp_all add: ‹convex C› convex_linear_image linear_fst linear_snd)
have fstab: "a ∈ fst ` C ∧ b ∈ fst ` C"
if "a ∈ S" "b ∈ S" "x ∈ open_segment a b" "(x,x') ∈ C" for a b x x'
proof -
have *: "(x,x') ∈ open_segment (a,x') (b,x')"
using that by (auto simp: in_segment)
show ?thesis
using face_ofD [OF C *] that face_of_imp_subset [OF C] by force
qed
have fst: "fst ` C face_of S"
by (force simp: face_of_def 1 conv fstab)
have sndab: "a' ∈ snd ` C ∧ b' ∈ snd ` C"
if "a' ∈ S'" "b' ∈ S'" "x' ∈ open_segment a' b'" "(x,x') ∈ C" for a' b' x x'
proof -
have *: "(x,x') ∈ open_segment (x,a') (x,b')"
using that by (auto simp: in_segment)
show ?thesis
using face_ofD [OF C *] that face_of_imp_subset [OF C] by force
qed
have snd: "snd ` C face_of S'"
by (force simp: face_of_def 1 conv sndab)
have cc: "rel_interior C ⊆ rel_interior (fst ` C) × rel_interior (snd ` C)"
by (force simp: face_of_Times rel_interior_Times conv fst snd ‹convex C› linear_fst linear_snd rel_interior_convex_linear_image [symmetric])
have "C = fst ` C × snd ` C"
proof (rule face_of_eq [OF C])
show "fst ` C × snd ` C face_of S × S'"
by (simp add: face_of_Times rel_interior_Times conv fst snd)
show "rel_interior C ∩ rel_interior (fst ` C × snd ` C) ≠ {}"
using False rel_interior_eq_empty ‹convex C› cc
by (auto simp: face_of_Times rel_interior_Times conv fst)
qed
with fst snd show ?thesis by metis
qed
qed (use face_of_Times in auto)

lemma face_of_Times_eq:
fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
shows "(F × F') face_of (S × S') ⟷ F = {} ∨ F' = {} ∨ F face_of S ∧ F' face_of S'"
by (auto simp: face_of_Times_decomp times_eq_iff)

lemma hyperplane_face_of_halfspace_le: "{x. a ∙ x = b} face_of {x. a ∙ x ≤ b}"
proof -
have "{x. a ∙ x ≤ b} ∩ {x. a ∙ x = b} = {x. a ∙ x = b}"
by auto
with face_of_Int_supporting_hyperplane_le [OF convex_halfspace_le [of a b], of a b]
show ?thesis by auto
qed

lemma hyperplane_face_of_halfspace_ge: "{x. a ∙ x = b} face_of {x. a ∙ x ≥ b}"
proof -
have "{x. a ∙ x ≥ b} ∩ {x. a ∙ x = b} = {x. a ∙ x = b}"
by auto
with face_of_Int_supporting_hyperplane_ge [OF convex_halfspace_ge [of b a], of b a]
show ?thesis by auto
qed

lemma face_of_halfspace_le:
fixes a :: "'n::euclidean_space"
shows "F face_of {x. a ∙ x ≤ b} ⟷ F = {} ∨ F = {x. a ∙ x = b} ∨ F = {x. a ∙ x ≤ b}"
(is "?lhs = ?rhs")
proof (cases "a = 0")
case True then show ?thesis
using face_of_affine_eq affine_UNIV by auto
next
case False
then have ine: "interior {x. a ∙ x ≤ b} ≠ {}"
using halfspace_eq_empty_lt interior_halfspace_le by blast
show ?thesis
proof
assume L: ?lhs
have "F face_of {x. a ∙ x = b}" if "F ≠ {x. a ∙ x ≤ b}"
proof -
have "F face_of rel_frontier {x. a ∙ x ≤ b}"
proof (rule face_of_subset [OF L])
show "F ⊆ rel_frontier {x. a ∙ x ≤ b}"
by (simp add: L face_of_subset_rel_frontier that)
qed (force simp: rel_frontier_def closed_halfspace_le)
then show ?thesis
using False
by (simp add: frontier_halfspace_le rel_frontier_nonempty_interior [OF ine])
qed
with L show ?rhs
using affine_hyperplane face_of_affine_eq by blast
next
assume ?rhs
then show ?lhs
by (metis convex_halfspace_le empty_face_of face_of_refl hyperplane_face_of_halfspace_le)
qed
qed

lemma face_of_halfspace_ge:
fixes a :: "'n::euclidean_space"
shows "F face_of {x. a ∙ x ≥ b} ⟷ F = {} ∨ F = {x. a ∙ x = b} ∨ F = {x. a ∙ x ≥ b}"
using face_of_halfspace_le [of F "-a" "-b"] by simp

subsection‹Exposed faces›

text‹That is, faces that are intersection with supporting hyperplane›

definition✐‹tag important› exposed_face_of :: "['a::euclidean_space set, 'a set] ⇒ bool"
(infixr "(exposed'_face'_of)" 50)
where "T exposed_face_of S ⟷
T face_of S ∧ (∃a b. S ⊆ {x. a ∙ x ≤ b} ∧ T = S ∩ {x. a ∙ x = b})"

lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
proof -
have "S ⊆ {x. 0 ∙ x ≤ 1} ∧ {} = S ∩ {x. 0 ∙ x = 1}"
by force
then show ?thesis
using exposed_face_of_def by blast
qed

lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S ⟷ convex S"
proof
assume S: "convex S"
have "S ⊆ {x. 0 ∙ x ≤ 0} ∧ S = S ∩ {x. 0 ∙ x = 0}"
by auto
with S show "S exposed_face_of S"
using exposed_face_of_def face_of_refl_eq by blast

lemma exposed_face_of_refl: "convex S ⟹ S exposed_face_of S"
by simp

lemma exposed_face_of:
"T exposed_face_of S ⟷
T face_of S ∧ (T = {} ∨ T = S ∨
(∃a b. a ≠ 0 ∧ S ⊆ {x. a ∙ x ≤ b} ∧ T = S ∩ {x. a ∙ x = b}))"
(is "?lhs = ?rhs")
proof
show "?lhs ⟹ ?rhs"
by (smt (verit) Collect_cong exposed_face_of_def hyperplane_eq_empty inf.absorb_iff1
inf_bot_right inner_zero_left)
show "?rhs ⟹ ?lhs"
using exposed_face_of_def face_of_imp_convex by fastforce
qed

lemma exposed_face_of_Int_supporting_hyperplane_le:
"⟦convex S; ⋀x. x ∈ S ⟹ a ∙ x ≤ b⟧ ⟹ (S ∩ {x. a ∙ x = b}) exposed_face_of S"
by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)

lemma exposed_face_of_Int_supporting_hyperplane_ge:
"⟦convex S; ⋀x. x ∈ S ⟹ a ∙ x ≥ b⟧ ⟹ (S ∩ {x. a ∙ x = b}) exposed_face_of S"
using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp

proposition exposed_face_of_Int:
assumes "T exposed_face_of S"
and "U exposed_face_of S"
shows "(T ∩ U) exposed_face_of S"
proof -
obtain a b where T: "S ∩ {x. a ∙ x = b} face_of S"
and S: "S ⊆ {x. a ∙ x ≤ b}"
and teq: "T = S ∩ {x. a ∙ x = b}"
using assms by (auto simp: exposed_face_of_def)
obtain a' b' where U: "S ∩ {x. a' ∙ x = b'} face_of S"
and s': "S ⊆ {x. a' ∙ x ≤ b'}"
and ueq: "U = S ∩ {x. a' ∙ x = b'}"
using assms by (auto simp: exposed_face_of_def)
have tu: "T ∩ U face_of S"
using T teq U ueq by (simp add: face_of_Int)
have ss: "S ⊆ {x. (a + a') ∙ x ≤ b + b'}"
using S s' by (force simp: inner_left_distrib)
have "S ⊆ {x. (a + a') ∙ x ≤ b + b'} ∧ T ∩ U = S ∩ {x. (a + a') ∙ x = b + b'}"
using S s' by (fastforce simp: ss inner_left_distrib teq ueq)
then show ?thesis
using exposed_face_of_def tu by auto
qed

proposition exposed_face_of_Inter:
fixes P :: "'a::euclidean_space set set"
assumes "P ≠ {}"
and "⋀T. T ∈ P ⟹ T exposed_face_of S"
shows "⋂P exposed_face_of S"
proof -
obtain Q where "finite Q" and QsubP: "Q ⊆ P" "card Q ≤ DIM('a) + 2" and IntQ: "⋂Q = ⋂P"
using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of]
by force
show ?thesis
proof (cases "Q = {}")
case True then show ?thesis
by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv)
next
case False
have "Q ⊆ {T. T exposed_face_of S}"
using QsubP assms by blast
moreover have "Q ⊆ {T. T exposed_face_of S} ⟹ ⋂Q exposed_face_of S"
using ‹finite Q› False
by (induction Q rule: finite_induct; use exposed_face_of_Int in fastforce)
ultimately show ?thesis
qed
qed

proposition exposed_face_of_sums:
assumes "convex S" and "convex T"
and "F exposed_face_of {x + y | x y. x ∈ S ∧ y ∈ T}"
(is "F exposed_face_of ?ST")
obtains k l
where "k exposed_face_of S" "l exposed_face_of T"
"F = {x + y | x y. x ∈ k ∧ y ∈ l}"
proof (cases "F = {}")
case True then show ?thesis
using that by blast
next
case False
show ?thesis
proof (cases "F = ?ST")
case True then show ?thesis
using assms exposed_face_of_refl_eq that by blast
next
case False
obtain p where "p ∈ F" using ‹F ≠ {}› by blast
moreover
obtain u z where T: "?ST ∩ {x. u ∙ x = z} face_of ?ST"
and S: "?ST ⊆ {x. u ∙ x ≤ z}"
and feq: "F = ?ST ∩ {x. u ∙ x = z}"
using assms by (auto simp: exposed_face_of_def)
ultimately obtain a0 b0
where p: "p = a0 + b0" and "a0 ∈ S" "b0 ∈ T" and z: "u ∙ p = z"
by auto
have lez: "u ∙ (x + y) ≤ z" if "x ∈ S" "y ∈ T" for x y
using S that by auto
have sef: "S ∩ {x. u ∙ x = u ∙ a0} exposed_face_of S"
proof (rule exposed_face_of_Int_supporting_hyperplane_le [OF ‹convex S›])
show "⋀x. x ∈ S ⟹ u ∙ x ≤ u ∙ a0"
by (metis p z add_le_cancel_right inner_right_distrib lez [OF _ ‹b0 ∈ T›])
qed
have tef: "T ∩ {x. u ∙ x = u ∙ b0} exposed_face_of T"
proof (rule exposed_face_of_Int_supporting_hyperplane_le [OF ‹convex T›])
show "⋀x. x ∈ T ⟹ u ∙ x ≤ u ∙ b0"
by (metis p z add.commute add_le_cancel_right inner_right_distrib lez [OF ‹a0 ∈ S›])
qed
have "{x + y |x y. x ∈ S ∧ u ∙ x = u ∙ a0 ∧ y ∈ T ∧ u ∙ y = u ∙ b0} ⊆ F"
by (auto simp: feq) (metis inner_right_distrib p z)
moreover have "F ⊆ {x + y |x y. x ∈ S ∧ u ∙ x = u ∙ a0 ∧ y ∈ T ∧ u ∙ y = u ∙ b0}"
proof -
have "⋀x y. ⟦z = u ∙ (x + y); x ∈ S; y ∈ T⟧
⟹ u ∙ x = u ∙ a0 ∧ u ∙ y = u ∙ b0"
by (smt (verit, best) z p ‹a0 ∈ S› ‹b0 ∈ T› inner_right_distrib lez)
then show ?thesis
using feq by blast
qed
ultimately have "F = {x + y |x y. x ∈ S ∩ {x. u ∙ x = u ∙ a0} ∧ y ∈ T ∩ {x. u ∙ x = u ∙ b0}}"
by blast
then show ?thesis
by (rule that [OF sef tef])
qed
qed

proposition exposed_face_of_parallel:
"T exposed_face_of S ⟷
T face_of S ∧
(∃a b. S ⊆ {x. a ∙ x ≤ b} ∧ T = S ∩ {x. a ∙ x = b} ∧
(T ≠ {} ⟶ T ≠ S ⟶ a ≠ 0) ∧
(T ≠ S ⟶ (∀w ∈ affine hull S. (w + a) ∈ affine hull S)))"
(is "?lhs = ?rhs")
proof
assume ?lhs then show ?rhs
proof (clarsimp simp: exposed_face_of_def)
fix a b
assume faceS: "S ∩ {x. a ∙ x = b} face_of S" and Ssub: "S ⊆ {x. a ∙ x ≤ b}"
show "∃c d. S ⊆ {x. c ∙ x ≤ d} ∧
S ∩ {x. a ∙ x = b} = S ∩ {x. c ∙ x = d} ∧
(S ∩ {x. a ∙ x = b} ≠ {} ⟶ S ∩ {x. a ∙ x = b} ≠ S ⟶ c ≠ 0) ∧
(S ∩ {x. a ∙ x = b} ≠ S ⟶ (∀w ∈ affine hull S. w + c ∈ affine hull S))"
proof (cases "affine hull S ∩ {x. -a ∙ x ≤ -b} = {} ∨ affine hull S ⊆ {x. - a ∙ x ≤ - b}")
case True
then show ?thesis
proof
assume "affine hull S ∩ {x. - a ∙ x ≤ - b} = {}"
then show ?thesis
apply (rule_tac x="0" in exI)
apply (rule_tac x="1" in exI)
using hull_subset by fastforce
next
assume "affine hull S ⊆ {x. - a ∙ x ≤ - b}"
then show ?thesis
apply (rule_tac x="0" in exI)
apply (rule_tac x="0" in exI)
using Ssub hull_subset by fastforce
qed
next
case False
then obtain a' b' where "a' ≠ 0"
and le: "affine hull S ∩ {x. a' ∙ x ≤ b'} = affine hull S ∩ {x. - a ∙ x ≤ - b}"
and eq: "affine hull S ∩ {x. a' ∙ x = b'} = affine hull S ∩ {x. - a ∙ x = - b}"
and mem: "⋀w. w ∈ affine hull S ⟹ w + a' ∈ affine hull S"
using affine_parallel_slice affine_affine_hull by metis
show ?thesis
proof (intro conjI impI allI ballI exI)
have *: "S ⊆ - (affine hull S ∩ {x. P x}) ∪ affine hull S ∩ {x. Q x} ⟹ S ⊆ {x. ¬ P x ∨ Q x}"
for P Q
using hull_subset by fastforce
have "S ⊆ {x. ¬ (a' ∙ x ≤ b') ∨ a' ∙ x = b'}"
by (rule *) (use le eq Ssub in auto)
then show "S ⊆ {x. - a' ∙ x ≤ - b'}"
by auto
show "S ∩ {x. a ∙ x = b} = S ∩ {x. - a' ∙ x = - b'}"
using eq hull_subset [of S affine] by force
show "⟦S ∩ {x. a ∙ x = b} ≠ {}; S ∩ {x. a ∙ x = b} ≠ S⟧ ⟹ - a' ≠ 0"
using ‹a' ≠ 0› by auto
show "w + - a' ∈ affine hull S"
if "S ∩ {x. a ∙ x = b} ≠ S" "w ∈ affine hull S" for w
proof -
have "w + 1 *⇩R (w - (w + a')) ∈ affine hull S"
using affine_affine_hull mem mem_affine_3_minus that(2) by blast
then show ?thesis  by simp
qed
qed
qed
qed
next
assume ?rhs then show ?lhs
unfolding exposed_face_of_def by blast
qed

subsection‹Extreme points of a set: its singleton faces›

definition✐‹tag important› extreme_point_of :: "['a::real_vector, 'a set] ⇒ bool"
(infixr "(extreme'_point'_of)" 50)
where "x extreme_point_of S ⟷
x ∈ S ∧ (∀a ∈ S. ∀b ∈ S. x ∉ open_segment a b)"

lemma extreme_point_of_stillconvex:
"convex S ⟹ (x extreme_point_of S ⟷ x ∈ S ∧ convex(S - {x}))"
by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)

lemma face_of_singleton:
"{x} face_of S ⟷ x extreme_point_of S"
by (fastforce simp add: extreme_point_of_def face_of_def)

lemma extreme_point_not_in_REL_INTERIOR:
fixes S :: "'a::real_normed_vector set"
shows "⟦x extreme_point_of S; S ≠ {x}⟧ ⟹ x ∉ rel_interior S"
by (metis disjoint_iff face_of_disjoint_rel_interior face_of_singleton insertI1)

lemma extreme_point_not_in_interior:
fixes S :: "'a::{real_normed_vector, perfect_space} set"
assumes "x extreme_point_of S" shows "x ∉ interior S"
using assms extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior by fastforce

lemma extreme_point_of_face:
"F face_of S ⟹ v extreme_point_of F ⟷ v extreme_point_of S ∧ v ∈ F"
by (meson empty_subsetI face_of_face face_of_singleton insert_subset)

lemma extreme_point_of_convex_hull:
"x extreme_point_of (convex hull S) ⟹ x ∈ S"
using hull_minimal [of S "(convex hull S) - {x}" convex]
using hull_subset [of S convex]

proposition extreme_points_of_convex_hull:
"{x. x extreme_point_of (convex hull S)} ⊆ S"
using extreme_point_of_convex_hull by auto

lemma extreme_point_of_empty [simp]: "¬ (x extreme_point_of {})"

lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} ⟷ x = a"
using extreme_point_of_stillconvex by auto

lemma extreme_point_of_translation_eq:
"(a + x) extreme_point_of (image (λx. a + x) S) ⟷ x extreme_point_of S"
by (auto simp: extreme_point_of_def)

lemma extreme_points_of_translation:
"{x. x extreme_point_of (image (λx. a + x) S)} =
(λx. a + x) ` {x. x extreme_point_of S}"
using extreme_point_of_translation_eq
by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)

lemma extreme_points_of_translation_subtract:
"{x. x extreme_point_of (image (λx. x - a) S)} =
(λx. x - a) ` {x. x extreme_point_of S}"
using extreme_points_of_translation [of "- a" S]
by simp

lemma extreme_point_of_Int:
"⟦x extreme_point_of S; x extreme_point_of T⟧ ⟹ x extreme_point_of (S ∩ T)"

lemma extreme_point_of_Int_supporting_hyperplane_le:
"⟦S ∩ {x. a ∙ x = b} = {c}; ⋀x. x ∈ S ⟹ a ∙ x ≤ b⟧ ⟹ c extreme_point_of S"
by (metis convex_singleton face_of_Int_supporting_hyperplane_le_strong face_of_singleton)

lemma extreme_point_of_Int_supporting_hyperplane_ge:
"⟦S ∩ {x. a ∙ x = b} = {c}; ⋀x. x ∈ S ⟹ a ∙ x ≥ b⟧ ⟹ c extreme_point_of S"
using extreme_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
by simp

lemma exposed_point_of_Int_supporting_hyperplane_le:
"⟦S ∩ {x. a ∙ x = b} = {c}; ⋀x. x ∈ S ⟹ a ∙ x ≤ b⟧ ⟹ {c} exposed_face_of S"
unfolding exposed_face_of_def
by (force simp: face_of_singleton extreme_point_of_Int_supporting_hyperplane_le)

lemma exposed_point_of_Int_supporting_hyperplane_ge:
"⟦S ∩ {x. a ∙ x = b} = {c}; ⋀x. x ∈ S ⟹ a ∙ x ≥ b⟧ ⟹ {c} exposed_face_of S"
using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
by simp

lemma extreme_point_of_convex_hull_insert:
assumes "finite S" "a ∉ convex hull S"
shows "a extreme_point_of (convex hull (insert a S))"
proof (cases "a ∈ S")
case False
then show ?thesis
using face_of_convex_hulls [of "insert a S" "{a}"] assms
by (auto simp: face_of_singleton hull_same)
qed (use assms  in ‹simp add: hull_inc›)

lemma extreme_point_of_conic:
assumes "conic S" and x: "x extreme_point_of S"
shows "x = 0"
proof -
have "{x} face_of S"
then have "conic{x}"
using assms(1) face_of_conic by blast
then show ?thesis
by (force simp: conic_def)
qed

subsection‹Facets›

definition✐‹tag important› facet_of :: "['a::euclidean_space set, 'a set] ⇒ bool"
(infixr "(facet'_of)" 50)
where "F facet_of S ⟷ F face_of S ∧ F ≠ {} ∧ aff_dim F = aff_dim S - 1"

lemma facet_of_empty [simp]: "¬ S facet_of {}"

lemma facet_of_irrefl [simp]: "¬ S facet_of S "

lemma facet_of_imp_face_of: "F facet_of S ⟹ F face_of S"

lemma facet_of_imp_subset: "F facet_of S ⟹ F ⊆ S"

lemma hyperplane_facet_of_halfspace_le:
"a ≠ 0 ⟹ {x. a ∙ x = b} facet_of {x. a ∙ x ≤ b}"
unfolding facet_of_def hyperplane_eq_empty
by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
Suc_leI of_nat_diff aff_dim_halfspace_le)

lemma hyperplane_facet_of_halfspace_ge:
"a ≠ 0 ⟹ {x. a ∙ x = b} facet_of {x. a ∙ x ≥ b}"
unfolding facet_of_def hyperplane_eq_empty
by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
Suc_leI of_nat_diff aff_dim_halfspace_ge)

lemma facet_of_halfspace_le:
"F facet_of {x. a ∙ x ≤ b} ⟷ a ≠ 0 ∧ F = {x. a ∙ x = b}"
(is "?lhs = ?rhs")
proof
assume c: ?lhs
with c facet_of_irrefl show ?rhs
by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm)
next
assume ?rhs then show ?lhs
qed

lemma facet_of_halfspace_ge:
"F facet_of {x. a ∙ x ≥ b} ⟷ a ≠ 0 ∧ F = {x. a ∙ x = b}"
using facet_of_halfspace_le [of F "-a" "-b"] by simp

subsection ‹Edges: faces of affine dimension 1› (*FIXME too small subsection, rearrange? *)

definition✐‹tag important› edge_of :: "['a::euclidean_space set, 'a set] ⇒ bool"  (infixr "(edge'_of)" 50)
where "e edge_of S ⟷ e face_of S ∧ aff_dim e = 1"

lemma edge_of_imp_subset:
"S edge_of T ⟹ S ⊆ T"

subsection‹Existence of extreme points›

proposition different_norm_3_collinear_points:
fixes a :: "'a::euclidean_space"
assumes "x ∈ open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)"
shows False
proof -
obtain u where "norm ((1 - u) *⇩R a + u *⇩R b) = norm b"
and "a ≠ b"
and u01: "0 < u" "u < 1"
using assms by (auto simp: open_segment_image_interval if_splits)
then have "(1 - u) *⇩R a ∙ (1 - u) *⇩R a + ((1 - u) * 2) *⇩R a ∙ u *⇩R b =
(1 - u * u) *⇩R (a ∙ a)"
using assms by (simp add: norm_eq algebra_simps inner_commute)
then have "(1 - u) *⇩R ((1 - u) *⇩R a ∙ a + (2 * u) *⇩R  a ∙ b) =
(1 - u) *⇩R ((1 + u) *⇩R (a ∙ a))"
then have "(1 - u) *⇩R (a ∙ a) + (2 * u) *⇩R (a ∙ b) = (1 + u) *⇩R (a ∙ a)"
using u01 by auto
then have "a ∙ b = a ∙ a"
using u01 by (simp add: algebra_simps)
then have "a = b"
using ‹norm(a) = norm(b)› norm_eq vector_eq by fastforce
then show ?thesis
using ‹a ≠ b› by force
qed

proposition extreme_point_exists_convex:
fixes S :: "'a::euclidean_space set"
assumes "compact S" "convex S" "S ≠ {}"
obtains x where "x extreme_point_of S"
proof -
obtain x where "x ∈ S" and xsup: "⋀y. y ∈ S ⟹ norm y ≤ norm x"
using distance_attains_sup [of S 0] assms by auto
have False if "a ∈ S" "b ∈ S" and x: "x ∈ open_segment a b" for a b
proof -
have noax: "norm a ≤ norm x" and nobx: "norm b ≤ norm x" using xsup that by auto
have "a ≠ b"
using empty_iff open_segment_idem x by auto
show False
by (metis dist_0_norm dist_decreases_open_segment noax nobx not_le x)
qed
then show ?thesis
by (meson ‹x ∈ S› extreme_point_of_def that)
qed

subsection‹Krein-Milman, the weaker form›

proposition Krein_Milman:
fixes S :: "'a::euclidean_space set"
assumes "compact S" "convex S"
shows "S = closure(convex hull {x. x extreme_point_of S})"
proof (cases "S = {}")
case True then show ?thesis   by simp
next
case False
have "closed S"
by (simp add: ‹compact S› compact_imp_closed)
have "closure (convex hull {x. x extreme_point_of S}) ⊆ S"
by (simp add: ‹closed S› assms closure_minimal extreme_point_of_def hull_minimal)
moreover have "u ∈ closure (convex hull {x. x extreme_point_of S})"
if "u ∈ S" for u
proof (rule ccontr)
assume unot: "u ∉ closure(convex hull {x. x extreme_point_of S})"
then obtain a b where "a ∙ u < b"
and ab: "⋀x. x ∈ closure(convex hull {x. x extreme_point_of S}) ⟹ b < a ∙ x"
using separating_hyperplane_closed_point [of "closure(convex hull {x. x extreme_point_of S})"]
by blast
have "continuous_on S ((∙) a)"
by (rule continuous_intros)+
then obtain m where "m ∈ S" and m: "⋀y. y ∈ S ⟹ a ∙ m ≤ a ∙ y"
using continuous_attains_inf [of S "λx. a ∙ x"] ‹compact S› ‹u ∈ S›
by auto
define T where "T = S ∩ {x. a ∙ x = a ∙ m}"
have "m ∈ T"
by (simp add: T_def ‹m ∈ S›)
moreover have "compact T"
by (simp add: T_def compact_Int_closed [OF ‹compact S› closed_hyperplane])
moreover have "convex T"
by (simp add: T_def convex_Int [OF ‹convex S› convex_hyperplane])
ultimately obtain v where v: "v extreme_point_of T"
using extreme_point_exists_convex [of T] by auto
then have "{v} face_of T"
also have "T face_of S"
by (simp add: T_def m face_of_Int_supporting_hyperplane_ge [OF ‹convex S›])
finally have "v extreme_point_of S"
then have "b < a ∙ v"
using closure_subset by (simp add: closure_hull hull_inc ab)
then show False
using ‹a ∙ u < b› ‹{v} face_of T› face_of_imp_subset m T_def that by fastforce
qed
ultimately show ?thesis
by blast
qed

text‹Now the sharper form.›

lemma Krein_Milman_Minkowski_aux:
fixes S :: "'a::euclidean_space set"
assumes n: "dim S = n" and S: "compact S" "convex S" "0 ∈ S"
shows "0 ∈ convex hull {x. x extreme_point_of S}"
using n S
proof (induction n arbitrary: S rule: less_induct)
case (less n S) show ?case
proof (cases "0 ∈ rel_interior S")
case True with Krein_Milman less.prems
show ?thesis
by (metis subsetD convex_convex_hull convex_rel_interior_closure rel_interior_subset)
next
case False
have "rel_interior S ≠ {}"
then obtain c where c: "c ∈ rel_interior S" by blast
obtain a where "a ≠ 0"
and le_ay: "⋀y. y ∈ S ⟹ a ∙ 0 ≤ a ∙ y"
and less_ay: "⋀y. y ∈ rel_interior S ⟹ a ∙ 0 < a ∙ y"
by (blast intro: supporting_hyperplane_rel_boundary intro!: less False)
have face: "S ∩ {x. a ∙ x = 0} face_of S"
using face_of_Int_supporting_hyperplane_ge le_ay ‹convex S› by auto
then have co: "compact (S ∩ {x. a ∙ x = 0})" "convex (S ∩ {x. a ∙ x = 0})"
using less.prems by (blast intro: face_of_imp_compact face_of_imp_convex)+
have "a ∙ y = 0" if "y ∈ span (S ∩ {x. a ∙ x = 0})" for y
proof -
have "y ∈ span {x. a ∙ x = 0}"
by (metis inf.cobounded2 span_mono subsetCE that)
then show ?thesis
by (blast intro: span_induct [OF _ subspace_hyperplane])
qed
then have "dim (S ∩ {x. a ∙ x = 0}) < n"
by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
inf_le1 ‹dim S = n› not_le rel_interior_subset span_0 span_base)
then have "0 ∈ convex hull {x. x extreme_point_of (S ∩ {x. a ∙ x = 0})}"
by (rule less.IH) (auto simp: co less.prems)
then show ?thesis
by (metis (mono_tags, lifting) Collect_mono_iff face extreme_point_of_face hull_mono subset_iff)
qed
qed

theorem Krein_Milman_Minkowski:
fixes S :: "'a::euclidean_space set"
assumes "compact S" "convex S"
shows "S = convex hull {x. x extreme_point_of S}"
proof
show "S ⊆ convex hull {x. x extreme_point_of S}"
proof
fix a assume [simp]: "a ∈ S"
have 1: "compact ((+) (- a) ` S)"
by (simp add: ‹compact S› compact_translation_subtract cong: image_cong_simp)
have 2: "convex ((+) (- a) ` S)"
by (simp add: ‹convex S› compact_translation_subtract)
show a_invex: "a ∈ convex hull {x. x extreme_point_of S}"
using Krein_Milman_Minkowski_aux [OF refl 1 2]
convex_hull_translation [of "-a"]
by (auto simp: extreme_points_of_translation_subtract translation_assoc cong: image_cong_simp)
qed
next
show "convex hull {x. x extreme_point_of S} ⊆ S"
using ‹convex S› extreme_point_of_stillconvex subset_hull by fastforce
qed

subsection‹Applying it to convex hulls of explicitly indicated finite sets›

corollary Krein_Milman_polytope:
fixes S :: "'a::euclidean_space set"
shows
"finite S
⟹ convex hull S =
convex hull {x. x extreme_point_of (convex hull S)}"

lemma extreme_points_of_convex_hull_eq:
fixes S :: "'a::euclidean_space set"
shows
"⟦compact S; ⋀T. T ⊂ S ⟹ convex hull T ≠ convex hull S⟧
⟹ {x. x extreme_point_of (convex hull S)} = S"
by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)

lemma extreme_point_of_convex_hull_eq:
fixes S :: "'a::euclidean_space set"
shows
"⟦compact S; ⋀T. T ⊂ S ⟹ convex hull T ≠ convex hull S⟧
⟹ (x extreme_point_of (convex hull S) ⟷ x ∈ S)"
using extreme_points_of_convex_hull_eq by auto

lemma extreme_point_of_convex_hull_convex_independent:
fixes S :: "'a::euclidean_space set"
assumes "compact S" and S: "⋀a. a ∈ S ⟹ a ∉ convex hull (S - {a})"
shows "(x extreme_point_of (convex hull S) ⟷ x ∈ S)"
proof -
have "convex hull T ≠ convex hull S" if "T ⊂ S" for T
proof -
obtain a where  "T ⊆ S" "a ∈ S" "a ∉ T" using ‹T ⊂ S› by blast
then show ?thesis
by (metis (full_types) Diff_eq_empty_iff Diff_insert0 S hull_mono hull_subset insert_Diff_single subsetCE)
qed
then show ?thesis
by (rule extreme_point_of_convex_hull_eq [OF ‹compact S›])
qed

lemma extreme_point_of_convex_hull_affine_independent:
fixes S :: "'a::euclidean_space set"
shows
"¬ affine_dependent S
⟹ (x extreme_point_of (convex hull S) ⟷ x ∈ S)"
by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc)

text‹Elementary proofs exist, not requiring Euclidean spaces and all this development›
lemma extreme_point_of_convex_hull_2:
fixes x :: "'a::euclidean_space"
shows "x extreme_point_of (convex hull {a,b}) ⟷ x = a ∨ x = b"

lemma extreme_point_of_segment:
fixes x :: "'a::euclidean_space"
shows "x extreme_point_of closed_segment a b ⟷ x = a ∨ x = b"

lemma face_of_convex_hull_subset:
fixes S :: "'a::euclidean_space set"
assumes "compact S" and T: "T face_of (convex hull S)"
obtains S' where "S' ⊆ S" "T = convex hull S'"
proof
show "{x. x extreme_point_of T} ⊆ S"
using T extreme_point_of_convex_hull extreme_point_of_face by blast
show "T = convex hull {x. x extreme_point_of T}"
by (metis Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull
face_of_imp_compact face_of_imp_convex)
qed

lemma face_of_convex_hull_aux:
assumes eq: "x *⇩R p = u *⇩R a + v *⇩R b + w *⇩R c"
and x: "u + v + w = x" "x ≠ 0" and S: "affine S" "a ∈ S" "b ∈ S" "c ∈ S"
shows "p ∈ S"
proof -
have "p = (u *⇩R a + v *⇩R b + w *⇩R c) /⇩R x"
by (metis ‹x ≠ 0› eq mult.commute right_inverse scaleR_one scaleR_scaleR)
moreover have "affine hull {a,b,c} ⊆ S"
moreover have "(u *⇩R a + v *⇩R b + w *⇩R c) /⇩R x ∈ affine hull {a,b,c}"
apply (rule_tac x="u/x" in exI)
apply (rule_tac x="v/x" in exI)
apply (rule_tac x="w/x" in exI)
using x apply (auto simp: field_split_simps)
done
ultimately show ?thesis by force
qed

proposition face_of_convex_hull_insert_eq:
fixes a :: "'a :: euclidean_space"
assumes "finite S" and a: "a ∉ affine hull S"
shows "(F face_of (convex hull (insert a S)) ⟷
F face_of (convex hull S) ∨
(∃F'. F' face_of (convex hull S) ∧ F = convex hull (insert a F')))"
(is "F face_of ?CAS ⟷ _")
proof safe
assume F: "F face_of ?CAS"
and *: "∄F'. F' face_of convex hull S ∧ F = convex hull insert a F'"
obtain T where T: "T ⊆ insert a S" and FeqT: "F = convex hull T"
by (metis F ‹finite S› compact_insert finite_imp_compact face_of_convex_hull_subset)
show "F face_of convex hull S"
proof (cases "a ∈ T")
case True
have "F = convex hull insert a (convex hull T ∩ convex hull S)"
proof
have "T ⊆ insert a (convex hull T ∩ convex hull S)"
using T hull_subset by fastforce
then show "F ⊆ convex hull insert a (convex hull T ∩ convex hull S)"
show "convex hull insert a (convex hull T ∩ convex hull S) ⊆ F"
by (simp add: FeqT True hull_inc hull_minimal)
qed
moreover have "convex hull T ∩ convex hull S face_of convex hull S"
by (metis F FeqT convex_convex_hull face_of_slice hull_mono inf.absorb_iff2 subset_insertI)
ultimately show ?thesis
using * by force
next
case False
then show ?thesis
by (metis FeqT F T face_of_subset hull_mono subset_insert subset_insertI)
qed
next
assume "F face_of convex hull S"
show "F face_of ?CAS"
by (simp add: ‹F face_of convex hull S› a face_of_convex_hull_insert ‹finite S›)
next
fix F
assume F: "F face_of convex hull S"
show "convex hull insert a F face_of ?CAS"
proof (cases "S = {}")
case True
then show ?thesis
using F face_of_affine_eq by auto
next
case False
have anotc: "a ∉ convex hull S"
by (metis (no_types) a affine_hull_convex_hull hull_inc)
show ?thesis
proof (cases "F = {}")
case True show ?thesis
using anotc by (simp add: ‹F = {}› ‹finite S› extreme_point_of_convex_hull_insert face_of_singleton)
next
case False
have "convex hull insert a F ⊆ ?CAS"
by (simp add: F a ‹finite S› convex_hull_subset face_of_convex_hull_insert face_of_imp_subset hull_inc)
moreover
have "(∃y v. (1 - ub) *⇩R a + ub *⇩R b = (1 - v) *⇩R a + v *⇩R y ∧
0 ≤ v ∧ v ≤ 1 ∧ y ∈ F) ∧
(∃x u. (1 - uc) *⇩R a + uc *⇩R c = (1 - u) *⇩R a + u *⇩R x ∧
0 ≤ u ∧ u ≤ 1 ∧ x ∈ F)"
if *: "(1 - ux) *⇩R a + ux *⇩R x
∈ open_segment ((1 - ub) *⇩R a + ub *⇩R b) ((1 - uc) *⇩R a + uc *⇩R c)"
and "0 ≤ ub" "ub ≤ 1" "0 ≤ uc" "uc ≤ 1" "0 ≤ ux" "ux ≤ 1"
and b: "b ∈ convex hull S" and c: "c ∈ convex hull S" and "x ∈ F"
for b c ub uc ux x
proof -
have xah: "x ∈ affine hull S"
using F convex_hull_subset_affine_hull face_of_imp_subset ‹x ∈ F› by blast
have ah: "b ∈ affine hull S" "c ∈ affine hull S"
using b c convex_hull_subset_affine_hull by blast+
obtain v where ne: "(1 - ub) *⇩R a + ub *⇩R b ≠ (1 - uc) *⇩R a + uc *⇩R c"
and eq: "(1 - ux) *⇩R a + ux *⇩R x =
(1 - v) *⇩R ((1 - ub) *⇩R a + ub *⇩R b) + v *⇩R ((1 - uc) *⇩R a + uc *⇩R c)"
and "0 < v" "v < 1"
using * by (auto simp: in_segment)
then have 0: "((1 - ux) - ((1 - v) * (1 - ub) ```