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)" by (simp add: face_of_def) 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" by (simp add: face_of_def) 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" by (simp add: dist_norm algebra_simps) 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)" by (simp add: algebra_simps) 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› by (metis add.commute le_less_trans less_add_same_cancel2 norm_ge_zero) then have [simp]: "d ≠ c" using False scaleR_cancel_left [of "1 + (e / norm (b - c))" b c] by (simp add: algebra_simps d_def) (simp add: field_split_simps) have [simp]: "((e - e * e / (e + norm (b - c))) / norm (b - c)) = (e / (e + norm (b - c)))" using False nbc by (simp add: divide_simps) (simp add: algebra_simps) have "b ∈ open_segment d c" apply (simp add: open_segment_image_interval) apply (simp add: d_def algebra_simps) 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 by (simp add: algebra_simps) (simp add: scaleR_left_distrib [symmetric] field_split_simps) 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)" apply (simp add: neq_iff) 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 (simp add: in_segment) apply (rule_tac x="(1 - d) / (e - d)" in exI) apply (simp add: field_simps) 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 by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff) 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" by (simp add: weq_sumsum) 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" apply (simp add: convex_hull_finite fin) 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 by (simp add: aff_dim_le_DIM) 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 qed (simp add: exposed_face_of_def face_of_refl_eq) 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 by (simp add: IntQ) 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] by (force simp add: extreme_point_of_stillconvex) 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 {})" by (simp add: extreme_point_of_def) 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)" by (simp add: extreme_point_of_def) 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" by (simp add: face_of_singleton x) 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 {}" by (simp add: facet_of_def) lemma facet_of_irrefl [simp]: "¬ S facet_of S " by (simp add: facet_of_def) lemma facet_of_imp_face_of: "F facet_of S ⟹ F face_of S" by (simp add: facet_of_def) lemma facet_of_imp_subset: "F facet_of S ⟹ F ⊆ S" by (simp add: face_of_imp_subset facet_of_def) 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 by (simp add: hyperplane_facet_of_halfspace_le) 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" by (simp add: edge_of_def face_of_imp_subset) 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))" by (simp add: algebra_simps) 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" by (simp add: face_of_singleton) 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" by (simp add: face_of_singleton) 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 ≠ {}" by (simp add: rel_interior_convex_nonempty_aux less) 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)}" by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull) 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" by (simp add: extreme_point_of_convex_hull_affine_independent) lemma extreme_point_of_segment: fixes x :: "'a::euclidean_space" shows "x extreme_point_of closed_segment a b ⟷ x = a ∨ x = b" by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull) 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" by (simp add: S hull_minimal) moreover have "(u *⇩_{R}a + v *⇩_{R}b + w *⇩_{R}c) /⇩_{R}x ∈ affine hull {a,b,c}" apply (simp add: affine_hull_3) 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)" by (simp add: FeqT hull_mono) 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)