src/HOL/Analysis/Polytope.thy
 author paulson Thu Jul 27 15:22:35 2017 +0100 (2017-07-27) changeset 66297 d425bdf419f5 parent 66287 005a30862ed0 child 66515 85c505c98332 permissions -rw-r--r--
polytopes: simplical subdivisions, etc.
 lp15@63078 ` 1` ```section \Faces, Extreme Points, Polytopes, Polyhedra etc.\ ``` lp15@63078 ` 2` lp15@63078 ` 3` ```text\Ported from HOL Light by L C Paulson\ ``` lp15@63078 ` 4` lp15@63078 ` 5` ```theory Polytope ``` lp15@63078 ` 6` ```imports Cartesian_Euclidean_Space ``` lp15@63078 ` 7` ```begin ``` lp15@63078 ` 8` lp15@63078 ` 9` ```subsection \Faces of a (usually convex) set\ ``` lp15@63078 ` 10` lp15@63078 ` 11` ```definition face_of :: "['a::real_vector set, 'a set] \ bool" (infixr "(face'_of)" 50) ``` lp15@63078 ` 12` ``` where ``` lp15@63078 ` 13` ``` "T face_of S \ ``` lp15@63078 ` 14` ``` T \ S \ convex T \ ``` lp15@63078 ` 15` ``` (\a \ S. \b \ S. \x \ T. x \ open_segment a b \ a \ T \ b \ T)" ``` lp15@63078 ` 16` lp15@63078 ` 17` ```lemma face_ofD: "\T face_of S; x \ open_segment a b; a \ S; b \ S; x \ T\ \ a \ T \ b \ T" ``` lp15@63078 ` 18` ``` unfolding face_of_def by blast ``` lp15@63078 ` 19` lp15@63078 ` 20` ```lemma face_of_translation_eq [simp]: ``` lp15@63078 ` 21` ``` "(op + a ` T face_of op + a ` S) \ T face_of S" ``` lp15@63078 ` 22` ```proof - ``` lp15@63078 ` 23` ``` have *: "\a T S. T face_of S \ (op + a ` T face_of op + a ` S)" ``` lp15@63078 ` 24` ``` apply (simp add: face_of_def Ball_def, clarify) ``` lp15@63078 ` 25` ``` apply (drule open_segment_translation_eq [THEN iffD1]) ``` lp15@63078 ` 26` ``` using inj_image_mem_iff inj_add_left apply metis ``` lp15@63078 ` 27` ``` done ``` lp15@63078 ` 28` ``` show ?thesis ``` lp15@63078 ` 29` ``` apply (rule iffI) ``` lp15@63078 ` 30` ``` apply (force simp: image_comp o_def dest: * [where a = "-a"]) ``` lp15@63078 ` 31` ``` apply (blast intro: *) ``` lp15@63078 ` 32` ``` done ``` lp15@63078 ` 33` ```qed ``` lp15@63078 ` 34` lp15@63078 ` 35` ```lemma face_of_linear_image: ``` lp15@63078 ` 36` ``` assumes "linear f" "inj f" ``` lp15@63078 ` 37` ``` shows "(f ` c face_of f ` S) \ c face_of S" ``` lp15@63078 ` 38` ```by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms) ``` lp15@63078 ` 39` lp15@63078 ` 40` ```lemma face_of_refl: "convex S \ S face_of S" ``` lp15@63078 ` 41` ``` by (auto simp: face_of_def) ``` lp15@63078 ` 42` lp15@63078 ` 43` ```lemma face_of_refl_eq: "S face_of S \ convex S" ``` lp15@63078 ` 44` ``` by (auto simp: face_of_def) ``` lp15@63078 ` 45` lp15@63078 ` 46` ```lemma empty_face_of [iff]: "{} face_of S" ``` lp15@63078 ` 47` ``` by (simp add: face_of_def) ``` lp15@63078 ` 48` lp15@63078 ` 49` ```lemma face_of_empty [simp]: "S face_of {} \ S = {}" ``` lp15@63078 ` 50` ``` by (meson empty_face_of face_of_def subset_empty) ``` lp15@63078 ` 51` lp15@63078 ` 52` ```lemma face_of_trans [trans]: "\S face_of T; T face_of u\ \ S face_of u" ``` lp15@63078 ` 53` ``` unfolding face_of_def by (safe; blast) ``` lp15@63078 ` 54` lp15@63078 ` 55` ```lemma face_of_face: "T face_of S \ (f face_of T \ f face_of S \ f \ T)" ``` lp15@63078 ` 56` ``` unfolding face_of_def by (safe; blast) ``` lp15@63078 ` 57` lp15@63078 ` 58` ```lemma face_of_subset: "\F face_of S; F \ T; T \ S\ \ F face_of T" ``` lp15@63078 ` 59` ``` unfolding face_of_def by (safe; blast) ``` lp15@63078 ` 60` lp15@63078 ` 61` ```lemma face_of_slice: "\F face_of S; convex T\ \ (F \ T) face_of (S \ T)" ``` lp15@63078 ` 62` ``` unfolding face_of_def by (blast intro: convex_Int) ``` lp15@63078 ` 63` lp15@63078 ` 64` ```lemma face_of_Int: "\t1 face_of S; t2 face_of S\ \ (t1 \ t2) face_of S" ``` lp15@63078 ` 65` ``` unfolding face_of_def by (blast intro: convex_Int) ``` lp15@63078 ` 66` lp15@63078 ` 67` ```lemma face_of_Inter: "\A \ {}; \T. T \ A \ T face_of S\ \ (\ A) face_of S" ``` lp15@63078 ` 68` ``` unfolding face_of_def by (blast intro: convex_Inter) ``` lp15@63078 ` 69` lp15@63078 ` 70` ```lemma face_of_Int_Int: "\F face_of T; F' face_of t'\ \ (F \ F') face_of (T \ t')" ``` lp15@63078 ` 71` ``` unfolding face_of_def by (blast intro: convex_Int) ``` lp15@63078 ` 72` lp15@63078 ` 73` ```lemma face_of_imp_subset: "T face_of S \ T \ S" ``` lp15@63078 ` 74` ``` unfolding face_of_def by blast ``` lp15@63078 ` 75` lp15@63078 ` 76` ```lemma face_of_imp_eq_affine_Int: ``` lp15@66287 ` 77` ``` fixes S :: "'a::euclidean_space set" ``` lp15@66287 ` 78` ``` assumes S: "convex S" and T: "T face_of S" ``` lp15@66287 ` 79` ``` shows "T = (affine hull T) \ S" ``` lp15@63078 ` 80` ```proof - ``` lp15@63078 ` 81` ``` have "convex T" using T by (simp add: face_of_def) ``` lp15@63078 ` 82` ``` have *: False if x: "x \ affine hull T" and "x \ S" "x \ T" and y: "y \ rel_interior T" for x y ``` lp15@63078 ` 83` ``` proof - ``` lp15@63078 ` 84` ``` obtain e where "e>0" and e: "cball y e \ affine hull T \ T" ``` lp15@63078 ` 85` ``` using y by (auto simp: rel_interior_cball) ``` lp15@63078 ` 86` ``` have "y \ x" "y \ S" "y \ T" ``` lp15@63078 ` 87` ``` using face_of_imp_subset rel_interior_subset T that by blast+ ``` lp15@63078 ` 88` ``` then have zne: "\u. \u \ {0<..<1}; (1 - u) *\<^sub>R y + u *\<^sub>R x \ T\ \ False" ``` lp15@63078 ` 89` ``` using \x \ S\ \x \ T\ \T face_of S\ unfolding face_of_def ``` lp15@63078 ` 90` ``` apply clarify ``` lp15@63078 ` 91` ``` apply (drule_tac x=x in bspec, assumption) ``` lp15@63078 ` 92` ``` apply (drule_tac x=y in bspec, assumption) ``` lp15@63078 ` 93` ``` apply (subst (asm) open_segment_commute) ``` lp15@63078 ` 94` ``` apply (force simp: open_segment_image_interval image_def) ``` lp15@63078 ` 95` ``` done ``` lp15@63078 ` 96` ``` have in01: "min (1/2) (e / norm (x - y)) \ {0<..<1}" ``` lp15@63078 ` 97` ``` using \y \ x\ \e > 0\ by simp ``` lp15@63078 ` 98` ``` show ?thesis ``` lp15@63078 ` 99` ``` apply (rule zne [OF in01]) ``` lp15@63078 ` 100` ``` apply (rule e [THEN subsetD]) ``` lp15@63078 ` 101` ``` apply (rule IntI) ``` wenzelm@63145 ` 102` ``` using \y \ x\ \e > 0\ ``` lp15@63078 ` 103` ``` apply (simp add: cball_def dist_norm algebra_simps) ``` lp15@63078 ` 104` ``` apply (simp add: Real_Vector_Spaces.scaleR_diff_right [symmetric] norm_minus_commute min_mult_distrib_right) ``` lp15@63078 ` 105` ``` apply (rule mem_affine [OF affine_affine_hull _ x]) ``` lp15@63078 ` 106` ``` using \y \ T\ apply (auto simp: hull_inc) ``` lp15@63078 ` 107` ``` done ``` lp15@63078 ` 108` ``` qed ``` lp15@63078 ` 109` ``` show ?thesis ``` lp15@63078 ` 110` ``` apply (rule subset_antisym) ``` lp15@63078 ` 111` ``` using assms apply (simp add: hull_subset face_of_imp_subset) ``` lp15@63078 ` 112` ``` apply (cases "T={}", simp) ``` lp15@63078 ` 113` ``` apply (force simp: rel_interior_eq_empty [symmetric] \convex T\ intro: *) ``` lp15@63078 ` 114` ``` done ``` lp15@63078 ` 115` ```qed ``` lp15@63078 ` 116` lp15@63078 ` 117` ```lemma face_of_imp_closed: ``` lp15@63078 ` 118` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 119` ``` assumes "convex S" "closed S" "T face_of S" shows "closed T" ``` lp15@63078 ` 120` ``` by (metis affine_affine_hull affine_closed closed_Int face_of_imp_eq_affine_Int assms) ``` lp15@63078 ` 121` lp15@63078 ` 122` ```lemma face_of_Int_supporting_hyperplane_le_strong: ``` lp15@63078 ` 123` ``` assumes "convex(S \ {x. a \ x = b})" and aleb: "\x. x \ S \ a \ x \ b" ``` lp15@63078 ` 124` ``` shows "(S \ {x. a \ x = b}) face_of S" ``` lp15@63078 ` 125` ```proof - ``` lp15@63078 ` 126` ``` have *: "a \ u = a \ x" if "x \ open_segment u v" "u \ S" "v \ S" and b: "b = a \ x" ``` lp15@63078 ` 127` ``` for u v x ``` lp15@63078 ` 128` ``` proof (rule antisym) ``` lp15@63078 ` 129` ``` show "a \ u \ a \ x" ``` lp15@63078 ` 130` ``` using aleb \u \ S\ \b = a \ x\ by blast ``` lp15@63078 ` 131` ``` next ``` lp15@63078 ` 132` ``` obtain \ where "b = a \ ((1 - \) *\<^sub>R u + \ *\<^sub>R v)" "0 < \" "\ < 1" ``` lp15@63078 ` 133` ``` using \b = a \ x\ \x \ open_segment u v\ in_segment ``` lp15@63078 ` 134` ``` by (auto simp: open_segment_image_interval split: if_split_asm) ``` lp15@63078 ` 135` ``` then have "b + \ * (a \ u) \ a \ u + \ * b" ``` lp15@63078 ` 136` ``` using aleb [OF \v \ S\] by (simp add: algebra_simps) ``` lp15@63078 ` 137` ``` then have "(1 - \) * b \ (1 - \) * (a \ u)" ``` lp15@63078 ` 138` ``` by (simp add: algebra_simps) ``` lp15@63078 ` 139` ``` then have "b \ a \ u" ``` lp15@63078 ` 140` ``` using \\ < 1\ by auto ``` lp15@63078 ` 141` ``` with b show "a \ x \ a \ u" by simp ``` lp15@63078 ` 142` ``` qed ``` lp15@63078 ` 143` ``` show ?thesis ``` lp15@63078 ` 144` ``` apply (simp add: face_of_def assms) ``` lp15@63078 ` 145` ``` using "*" open_segment_commute by blast ``` lp15@63078 ` 146` ```qed ``` lp15@63078 ` 147` lp15@63078 ` 148` ```lemma face_of_Int_supporting_hyperplane_ge_strong: ``` lp15@63078 ` 149` ``` "\convex(S \ {x. a \ x = b}); \x. x \ S \ a \ x \ b\ ``` lp15@63078 ` 150` ``` \ (S \ {x. a \ x = b}) face_of S" ``` lp15@63078 ` 151` ``` using face_of_Int_supporting_hyperplane_le_strong [of S "-a" "-b"] by simp ``` lp15@63078 ` 152` lp15@63078 ` 153` ```lemma face_of_Int_supporting_hyperplane_le: ``` lp15@63078 ` 154` ``` "\convex S; \x. x \ S \ a \ x \ b\ \ (S \ {x. a \ x = b}) face_of S" ``` lp15@63078 ` 155` ``` by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_le_strong) ``` lp15@63078 ` 156` lp15@63078 ` 157` ```lemma face_of_Int_supporting_hyperplane_ge: ``` lp15@63078 ` 158` ``` "\convex S; \x. x \ S \ a \ x \ b\ \ (S \ {x. a \ x = b}) face_of S" ``` lp15@63078 ` 159` ``` by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_ge_strong) ``` lp15@63078 ` 160` lp15@63078 ` 161` ```lemma face_of_imp_convex: "T face_of S \ convex T" ``` lp15@63078 ` 162` ``` using face_of_def by blast ``` lp15@63078 ` 163` lp15@63078 ` 164` ```lemma face_of_imp_compact: ``` lp15@63078 ` 165` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 166` ``` shows "\convex S; compact S; T face_of S\ \ compact T" ``` lp15@63078 ` 167` ``` by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset) ``` lp15@63078 ` 168` lp15@63078 ` 169` ```lemma face_of_Int_subface: ``` lp15@63469 ` 170` ``` "\A \ B face_of A; A \ B face_of B; C face_of A; D face_of B\ ``` lp15@63469 ` 171` ``` \ (C \ D) face_of C \ (C \ D) face_of D" ``` lp15@63078 ` 172` ``` by (meson face_of_Int_Int face_of_face inf_le1 inf_le2) ``` lp15@63078 ` 173` lp15@63078 ` 174` ```lemma subset_of_face_of: ``` lp15@63078 ` 175` ``` fixes S :: "'a::real_normed_vector set" ``` lp15@63078 ` 176` ``` assumes "T face_of S" "u \ S" "T \ (rel_interior u) \ {}" ``` lp15@63078 ` 177` ``` shows "u \ T" ``` lp15@63078 ` 178` ```proof ``` lp15@63078 ` 179` ``` fix c ``` lp15@63078 ` 180` ``` assume "c \ u" ``` lp15@63078 ` 181` ``` obtain b where "b \ T" "b \ rel_interior u" using assms by auto ``` lp15@63078 ` 182` ``` then obtain e where "e>0" "b \ u" and e: "cball b e \ affine hull u \ u" ``` lp15@63078 ` 183` ``` by (auto simp: rel_interior_cball) ``` lp15@63078 ` 184` ``` show "c \ T" ``` lp15@63078 ` 185` ``` proof (cases "b=c") ``` lp15@63078 ` 186` ``` case True with \b \ T\ show ?thesis by blast ``` lp15@63078 ` 187` ``` next ``` lp15@63078 ` 188` ``` case False ``` wenzelm@63148 ` 189` ``` define d where "d = b + (e / norm(b - c)) *\<^sub>R (b - c)" ``` lp15@63078 ` 190` ``` have "d \ cball b e \ affine hull u" ``` lp15@63078 ` 191` ``` using \e > 0\ \b \ u\ \c \ u\ ``` lp15@63078 ` 192` ``` by (simp add: d_def dist_norm hull_inc mem_affine_3_minus False) ``` lp15@63078 ` 193` ``` with e have "d \ u" by blast ``` lp15@63078 ` 194` ``` have nbc: "norm (b - c) + e > 0" using \e > 0\ ``` lp15@63078 ` 195` ``` by (metis add.commute le_less_trans less_add_same_cancel2 norm_ge_zero) ``` lp15@63078 ` 196` ``` then have [simp]: "d \ c" using False scaleR_cancel_left [of "1 + (e / norm (b - c))" b c] ``` lp15@63078 ` 197` ``` by (simp add: algebra_simps d_def) (simp add: divide_simps) ``` lp15@63078 ` 198` ``` have [simp]: "((e - e * e / (e + norm (b - c))) / norm (b - c)) = (e / (e + norm (b - c)))" ``` lp15@63078 ` 199` ``` using False nbc ``` lp15@63078 ` 200` ``` apply (simp add: algebra_simps divide_simps) ``` lp15@63078 ` 201` ``` by (metis mult_eq_0_iff norm_eq_zero norm_imp_pos_and_ge norm_pths(2) real_scaleR_def scaleR_left.add zero_less_norm_iff) ``` lp15@63078 ` 202` ``` have "b \ open_segment d c" ``` lp15@63078 ` 203` ``` apply (simp add: open_segment_image_interval) ``` lp15@63078 ` 204` ``` apply (simp add: d_def algebra_simps image_def) ``` lp15@63078 ` 205` ``` apply (rule_tac x="e / (e + norm (b - c))" in bexI) ``` lp15@63078 ` 206` ``` using False nbc \0 < e\ ``` lp15@63078 ` 207` ``` apply (auto simp: algebra_simps) ``` lp15@63078 ` 208` ``` done ``` lp15@63078 ` 209` ``` then have "d \ T \ c \ T" ``` lp15@63078 ` 210` ``` apply (rule face_ofD [OF \T face_of S\]) ``` wenzelm@63145 ` 211` ``` using \d \ u\ \c \ u\ \u \ S\ \b \ T\ apply auto ``` lp15@63078 ` 212` ``` done ``` lp15@63078 ` 213` ``` then show ?thesis .. ``` lp15@63078 ` 214` ``` qed ``` lp15@63078 ` 215` ```qed ``` lp15@63078 ` 216` lp15@63078 ` 217` ```lemma face_of_eq: ``` lp15@63078 ` 218` ``` fixes S :: "'a::real_normed_vector set" ``` lp15@63078 ` 219` ``` assumes "T face_of S" "u face_of S" "(rel_interior T) \ (rel_interior u) \ {}" ``` lp15@63078 ` 220` ``` shows "T = u" ``` lp15@63078 ` 221` ``` apply (rule subset_antisym) ``` lp15@63078 ` 222` ``` apply (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subsetCE subset_of_face_of) ``` lp15@63078 ` 223` ``` by (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subset_iff subset_of_face_of) ``` lp15@63078 ` 224` lp15@63078 ` 225` ```lemma face_of_disjoint_rel_interior: ``` lp15@63078 ` 226` ``` fixes S :: "'a::real_normed_vector set" ``` lp15@63078 ` 227` ``` assumes "T face_of S" "T \ S" ``` lp15@63078 ` 228` ``` shows "T \ rel_interior S = {}" ``` lp15@63078 ` 229` ``` by (meson assms subset_of_face_of face_of_imp_subset order_refl subset_antisym) ``` lp15@63078 ` 230` lp15@63078 ` 231` ```lemma face_of_disjoint_interior: ``` lp15@63078 ` 232` ``` fixes S :: "'a::real_normed_vector set" ``` lp15@63078 ` 233` ``` assumes "T face_of S" "T \ S" ``` lp15@63078 ` 234` ``` shows "T \ interior S = {}" ``` lp15@63078 ` 235` ```proof - ``` lp15@63078 ` 236` ``` have "T \ interior S \ rel_interior S" ``` lp15@63078 ` 237` ``` by (meson inf_sup_ord(2) interior_subset_rel_interior order.trans) ``` lp15@63078 ` 238` ``` thus ?thesis ``` lp15@63078 ` 239` ``` by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty) ``` lp15@63078 ` 240` ```qed ``` lp15@63078 ` 241` lp15@63078 ` 242` ```lemma face_of_subset_rel_boundary: ``` lp15@63078 ` 243` ``` fixes S :: "'a::real_normed_vector set" ``` lp15@63078 ` 244` ``` assumes "T face_of S" "T \ S" ``` lp15@63078 ` 245` ``` shows "T \ (S - rel_interior S)" ``` lp15@63078 ` 246` ```by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI) ``` lp15@63078 ` 247` lp15@63078 ` 248` ```lemma face_of_subset_rel_frontier: ``` lp15@63078 ` 249` ``` fixes S :: "'a::real_normed_vector set" ``` lp15@63078 ` 250` ``` assumes "T face_of S" "T \ S" ``` lp15@63078 ` 251` ``` shows "T \ rel_frontier S" ``` lp15@63078 ` 252` ``` using assms closure_subset face_of_disjoint_rel_interior face_of_imp_subset rel_frontier_def by fastforce ``` lp15@63078 ` 253` lp15@63078 ` 254` ```lemma face_of_aff_dim_lt: ``` lp15@63078 ` 255` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 256` ``` assumes "convex S" "T face_of S" "T \ S" ``` lp15@63078 ` 257` ``` shows "aff_dim T < aff_dim S" ``` lp15@63078 ` 258` ```proof - ``` lp15@63078 ` 259` ``` have "aff_dim T \ aff_dim S" ``` lp15@63078 ` 260` ``` by (simp add: face_of_imp_subset aff_dim_subset assms) ``` lp15@63078 ` 261` ``` moreover have "aff_dim T \ aff_dim S" ``` lp15@63078 ` 262` ``` proof (cases "T = {}") ``` lp15@63078 ` 263` ``` case True then show ?thesis ``` lp15@63078 ` 264` ``` by (metis aff_dim_empty \T \ S\) ``` lp15@63078 ` 265` ``` next case False then show ?thesis ``` lp15@63078 ` 266` ``` by (metis Set.set_insert assms convex_rel_frontier_aff_dim dual_order.irrefl face_of_imp_convex face_of_subset_rel_frontier insert_not_empty subsetI) ``` lp15@63078 ` 267` ``` qed ``` lp15@63078 ` 268` ``` ultimately show ?thesis ``` lp15@63078 ` 269` ``` by simp ``` lp15@63078 ` 270` ```qed ``` lp15@63078 ` 271` lp15@66287 ` 272` ```lemma subset_of_face_of_affine_hull: ``` lp15@66287 ` 273` ``` fixes S :: "'a::euclidean_space set" ``` lp15@66287 ` 274` ``` assumes T: "T face_of S" and "convex S" "U \ S" and dis: "~disjnt (affine hull T) (rel_interior U)" ``` lp15@66287 ` 275` ``` shows "U \ T" ``` lp15@66287 ` 276` ``` apply (rule subset_of_face_of [OF T \U \ S\]) ``` lp15@66287 ` 277` ``` using face_of_imp_eq_affine_Int [OF \convex S\ T] ``` lp15@66287 ` 278` ``` using rel_interior_subset [of U] dis ``` lp15@66287 ` 279` ``` using \U \ S\ disjnt_def by fastforce ``` lp15@66287 ` 280` lp15@66287 ` 281` ```lemma affine_hull_face_of_disjoint_rel_interior: ``` lp15@66287 ` 282` ``` fixes S :: "'a::euclidean_space set" ``` lp15@66287 ` 283` ``` assumes "convex S" "F face_of S" "F \ S" ``` lp15@66287 ` 284` ``` shows "affine hull F \ rel_interior S = {}" ``` lp15@66287 ` 285` ``` by (metis assms disjnt_def face_of_imp_subset order_refl subset_antisym subset_of_face_of_affine_hull) ``` lp15@63078 ` 286` lp15@63078 ` 287` ```lemma affine_diff_divide: ``` lp15@63078 ` 288` ``` assumes "affine S" "k \ 0" "k \ 1" and xy: "x \ S" "y /\<^sub>R (1 - k) \ S" ``` lp15@63078 ` 289` ``` shows "(x - y) /\<^sub>R k \ S" ``` lp15@63078 ` 290` ```proof - ``` lp15@63078 ` 291` ``` have "inverse(k) *\<^sub>R (x - y) = (1 - inverse k) *\<^sub>R inverse(1 - k) *\<^sub>R y + inverse(k) *\<^sub>R x" ``` lp15@63078 ` 292` ``` using assms ``` lp15@63078 ` 293` ``` by (simp add: algebra_simps) (simp add: scaleR_left_distrib [symmetric] divide_simps) ``` lp15@63078 ` 294` ``` then show ?thesis ``` lp15@63078 ` 295` ``` using \affine S\ xy by (auto simp: affine_alt) ``` lp15@63078 ` 296` ```qed ``` lp15@63078 ` 297` lp15@63078 ` 298` ```lemma face_of_convex_hulls: ``` lp15@63078 ` 299` ``` assumes S: "finite S" "T \ S" and disj: "affine hull T \ convex hull (S - T) = {}" ``` lp15@63078 ` 300` ``` shows "(convex hull T) face_of (convex hull S)" ``` lp15@63078 ` 301` ```proof - ``` lp15@63078 ` 302` ``` have fin: "finite T" "finite (S - T)" using assms ``` lp15@63078 ` 303` ``` by (auto simp: finite_subset) ``` lp15@63078 ` 304` ``` have *: "x \ convex hull T" ``` lp15@63078 ` 305` ``` if x: "x \ convex hull S" and y: "y \ convex hull S" and w: "w \ convex hull T" "w \ open_segment x y" ``` lp15@63078 ` 306` ``` for x y w ``` lp15@63078 ` 307` ``` proof - ``` lp15@63078 ` 308` ``` have waff: "w \ affine hull T" ``` lp15@63078 ` 309` ``` using convex_hull_subset_affine_hull w by blast ``` nipkow@64267 ` 310` ``` obtain a b where a: "\i. i \ S \ 0 \ a i" and asum: "sum a S = 1" and aeqx: "(\i\S. a i *\<^sub>R i) = x" ``` nipkow@64267 ` 311` ``` and b: "\i. i \ S \ 0 \ b i" and bsum: "sum b S = 1" and beqy: "(\i\S. b i *\<^sub>R i) = y" ``` lp15@63078 ` 312` ``` using x y by (auto simp: assms convex_hull_finite) ``` lp15@63078 ` 313` ``` obtain u where "(1 - u) *\<^sub>R x + u *\<^sub>R y \ convex hull T" "x \ y" and weq: "w = (1 - u) *\<^sub>R x + u *\<^sub>R y" ``` lp15@63078 ` 314` ``` and u01: "0 < u" "u < 1" ``` lp15@63078 ` 315` ``` using w by (auto simp: open_segment_image_interval split: if_split_asm) ``` wenzelm@63148 ` 316` ``` define c where "c i = (1 - u) * a i + u * b i" for i ``` lp15@63078 ` 317` ``` have cge0: "\i. i \ S \ 0 \ c i" ``` lp15@63078 ` 318` ``` using a b u01 by (simp add: c_def) ``` nipkow@64267 ` 319` ``` have sumc1: "sum c S = 1" ``` nipkow@64267 ` 320` ``` by (simp add: c_def sum.distrib sum_distrib_left [symmetric] asum bsum) ``` lp15@63078 ` 321` ``` have sumci_xy: "(\i\S. c i *\<^sub>R i) = (1 - u) *\<^sub>R x + u *\<^sub>R y" ``` nipkow@64267 ` 322` ``` apply (simp add: c_def sum.distrib scaleR_left_distrib) ``` nipkow@64267 ` 323` ``` by (simp only: scaleR_scaleR [symmetric] Real_Vector_Spaces.scaleR_right.sum [symmetric] aeqx beqy) ``` lp15@63078 ` 324` ``` show ?thesis ``` nipkow@64267 ` 325` ``` proof (cases "sum c (S - T) = 0") ``` lp15@63078 ` 326` ``` case True ``` lp15@63078 ` 327` ``` have ci0: "\i. i \ (S - T) \ c i = 0" ``` lp15@65680 ` 328` ``` using True cge0 fin(2) sum_nonneg_eq_0_iff by auto ``` lp15@63078 ` 329` ``` have a0: "a i = 0" if "i \ (S - T)" for i ``` lp15@63078 ` 330` ``` using ci0 [OF that] u01 a [of i] b [of i] that ``` lp15@63078 ` 331` ``` by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff) ``` nipkow@64267 ` 332` ``` have [simp]: "sum a T = 1" ``` nipkow@64267 ` 333` ``` using assms by (metis sum.mono_neutral_cong_right a0 asum) ``` lp15@63078 ` 334` ``` show ?thesis ``` lp15@63078 ` 335` ``` apply (simp add: convex_hull_finite \finite T\) ``` lp15@63078 ` 336` ``` apply (rule_tac x=a in exI) ``` lp15@63078 ` 337` ``` using a0 assms ``` nipkow@64267 ` 338` ``` apply (auto simp: cge0 a aeqx [symmetric] sum.mono_neutral_right) ``` lp15@63078 ` 339` ``` done ``` lp15@63078 ` 340` ``` next ``` lp15@63078 ` 341` ``` case False ``` nipkow@64267 ` 342` ``` define k where "k = sum c (S - T)" ``` lp15@63078 ` 343` ``` have "k > 0" using False ``` nipkow@64267 ` 344` ``` unfolding k_def by (metis DiffD1 antisym_conv cge0 sum_nonneg not_less) ``` nipkow@64267 ` 345` ``` have weq_sumsum: "w = sum (\x. c x *\<^sub>R x) T + sum (\x. c x *\<^sub>R x) (S - T)" ``` nipkow@64267 ` 346` ``` by (metis (no_types) add.commute S(1) S(2) sum.subset_diff sumci_xy weq) ``` lp15@63078 ` 347` ``` show ?thesis ``` lp15@63078 ` 348` ``` proof (cases "k = 1") ``` lp15@63078 ` 349` ``` case True ``` nipkow@64267 ` 350` ``` then have "sum c T = 0" ``` nipkow@64267 ` 351` ``` by (simp add: S k_def sum_diff sumc1) ``` nipkow@64267 ` 352` ``` then have [simp]: "sum c (S - T) = 1" ``` nipkow@64267 ` 353` ``` by (simp add: S sum_diff sumc1) ``` lp15@63078 ` 354` ``` have ci0: "\i. i \ T \ c i = 0" ``` nipkow@64267 ` 355` ``` by (meson \finite T\ \sum c T = 0\ \T \ S\ cge0 sum_nonneg_eq_0_iff subsetCE) ``` lp15@63078 ` 356` ``` then have [simp]: "(\i\S-T. c i *\<^sub>R i) = w" ``` lp15@63078 ` 357` ``` by (simp add: weq_sumsum) ``` lp15@63078 ` 358` ``` have "w \ convex hull (S - T)" ``` lp15@63078 ` 359` ``` apply (simp add: convex_hull_finite fin) ``` lp15@63078 ` 360` ``` apply (rule_tac x=c in exI) ``` lp15@63078 ` 361` ``` apply (auto simp: cge0 weq True k_def) ``` lp15@63078 ` 362` ``` done ``` lp15@63078 ` 363` ``` then show ?thesis ``` lp15@63078 ` 364` ``` using disj waff by blast ``` lp15@63078 ` 365` ``` next ``` lp15@63078 ` 366` ``` case False ``` nipkow@64267 ` 367` ``` then have sumcf: "sum c T = 1 - k" ``` nipkow@64267 ` 368` ``` by (simp add: S k_def sum_diff sumc1) ``` lp15@63078 ` 369` ``` have "(\i\T. c i *\<^sub>R i) /\<^sub>R (1 - k) \ convex hull T" ``` lp15@63078 ` 370` ``` apply (simp add: convex_hull_finite fin) ``` lp15@63078 ` 371` ``` apply (rule_tac x="\i. inverse (1-k) * c i" in exI) ``` lp15@63078 ` 372` ``` apply auto ``` nipkow@64267 ` 373` ``` apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) sum_nonneg subsetCE) ``` nipkow@64267 ` 374` ``` apply (metis False mult.commute right_inverse right_minus_eq sum_distrib_left sumcf) ``` nipkow@64267 ` 375` ``` by (metis (mono_tags, lifting) scaleR_right.sum scaleR_scaleR sum.cong) ``` nipkow@64267 ` 376` ``` with \0 < k\ have "inverse(k) *\<^sub>R (w - sum (\i. c i *\<^sub>R i) T) \ affine hull T" ``` lp15@63078 ` 377` ``` by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD]) ``` nipkow@64267 ` 378` ``` moreover have "inverse(k) *\<^sub>R (w - sum (\x. c x *\<^sub>R x) T) \ convex hull (S - T)" ``` lp15@63078 ` 379` ``` apply (simp add: weq_sumsum convex_hull_finite fin) ``` lp15@63078 ` 380` ``` apply (rule_tac x="\i. inverse k * c i" in exI) ``` lp15@63078 ` 381` ``` using \k > 0\ cge0 ``` nipkow@64267 ` 382` ``` apply (auto simp: scaleR_right.sum sum_distrib_left [symmetric] k_def [symmetric]) ``` lp15@63078 ` 383` ``` done ``` lp15@63078 ` 384` ``` ultimately show ?thesis ``` lp15@63078 ` 385` ``` using disj by blast ``` lp15@63078 ` 386` ``` qed ``` lp15@63078 ` 387` ``` qed ``` lp15@63078 ` 388` ``` qed ``` lp15@63078 ` 389` ``` have [simp]: "convex hull T \ convex hull S" ``` lp15@63078 ` 390` ``` by (simp add: \T \ S\ hull_mono) ``` lp15@63078 ` 391` ``` show ?thesis ``` lp15@63078 ` 392` ``` using open_segment_commute by (auto simp: face_of_def intro: *) ``` lp15@63078 ` 393` ```qed ``` lp15@63078 ` 394` lp15@63078 ` 395` ```proposition face_of_convex_hull_insert: ``` lp15@63078 ` 396` ``` "\finite S; a \ affine hull S; T face_of convex hull S\ \ T face_of convex hull insert a S" ``` lp15@63078 ` 397` ``` apply (rule face_of_trans, blast) ``` lp15@63078 ` 398` ``` apply (rule face_of_convex_hulls; force simp: insert_Diff_if) ``` lp15@63078 ` 399` ``` done ``` lp15@63078 ` 400` lp15@63078 ` 401` ```proposition face_of_affine_trivial: ``` lp15@63078 ` 402` ``` assumes "affine S" "T face_of S" ``` lp15@63078 ` 403` ``` shows "T = {} \ T = S" ``` lp15@63078 ` 404` ```proof (rule ccontr, clarsimp) ``` lp15@63078 ` 405` ``` assume "T \ {}" "T \ S" ``` lp15@63078 ` 406` ``` then obtain a where "a \ T" by auto ``` lp15@63078 ` 407` ``` then have "a \ S" ``` lp15@63078 ` 408` ``` using \T face_of S\ face_of_imp_subset by blast ``` lp15@63078 ` 409` ``` have "S \ T" ``` lp15@63078 ` 410` ``` proof ``` lp15@63078 ` 411` ``` fix b assume "b \ S" ``` lp15@63078 ` 412` ``` show "b \ T" ``` lp15@63078 ` 413` ``` proof (cases "a = b") ``` lp15@63078 ` 414` ``` case True with \a \ T\ show ?thesis by auto ``` lp15@63078 ` 415` ``` next ``` lp15@63078 ` 416` ``` case False ``` lp15@63078 ` 417` ``` then have "a \ open_segment (2 *\<^sub>R a - b) b" ``` lp15@63078 ` 418` ``` apply (auto simp: open_segment_def closed_segment_def) ``` lp15@63078 ` 419` ``` apply (rule_tac x="1/2" in exI) ``` lp15@63078 ` 420` ``` apply (simp add: algebra_simps) ``` lp15@63078 ` 421` ``` by (simp add: scaleR_2) ``` lp15@63078 ` 422` ``` moreover have "2 *\<^sub>R a - b \ S" ``` lp15@63078 ` 423` ``` by (rule mem_affine [OF \affine S\ \a \ S\ \b \ S\, of 2 "-1", simplified]) ``` lp15@63078 ` 424` ``` moreover note \b \ S\ \a \ T\ ``` lp15@63078 ` 425` ``` ultimately show ?thesis ``` lp15@63078 ` 426` ``` by (rule face_ofD [OF \T face_of S\, THEN conjunct2]) ``` lp15@63078 ` 427` ``` qed ``` lp15@63078 ` 428` ``` qed ``` lp15@63078 ` 429` ``` then show False ``` wenzelm@63145 ` 430` ``` using \T \ S\ \T face_of S\ face_of_imp_subset by blast ``` lp15@63078 ` 431` ```qed ``` lp15@63078 ` 432` lp15@63078 ` 433` lp15@63078 ` 434` ```lemma face_of_affine_eq: ``` lp15@63078 ` 435` ``` "affine S \ (T face_of S \ T = {} \ T = S)" ``` lp15@63078 ` 436` ```using affine_imp_convex face_of_affine_trivial face_of_refl by auto ``` lp15@63078 ` 437` lp15@63078 ` 438` lp15@63078 ` 439` ```lemma Inter_faces_finite_altbound: ``` lp15@63078 ` 440` ``` fixes T :: "'a::euclidean_space set set" ``` lp15@63078 ` 441` ``` assumes cfaI: "\c. c \ T \ c face_of S" ``` lp15@63078 ` 442` ``` shows "\F'. finite F' \ F' \ T \ card F' \ DIM('a) + 2 \ \F' = \T" ``` lp15@63078 ` 443` ```proof (cases "\F'. finite F' \ F' \ T \ card F' \ DIM('a) + 2 \ (\c. c \ T \ c \ (\F') \ (\F'))") ``` lp15@63078 ` 444` ``` case True ``` lp15@63078 ` 445` ``` then obtain c where c: ``` lp15@63078 ` 446` ``` "\F'. \finite F'; F' \ T; card F' \ DIM('a) + 2\ \ c F' \ T \ c F' \ (\F') \ (\F')" ``` lp15@63078 ` 447` ``` by metis ``` wenzelm@63148 ` 448` ``` define d where "d = rec_nat {c{}} (\n r. insert (c r) r)" ``` lp15@63078 ` 449` ``` have [simp]: "d 0 = {c {}}" ``` lp15@63078 ` 450` ``` by (simp add: d_def) ``` lp15@63078 ` 451` ``` have dSuc [simp]: "\n. d (Suc n) = insert (c (d n)) (d n)" ``` lp15@63078 ` 452` ``` by (simp add: d_def) ``` lp15@63078 ` 453` ``` have dn_notempty: "d n \ {}" for n ``` lp15@63078 ` 454` ``` by (induction n) auto ``` lp15@63078 ` 455` ``` have dn_le_Suc: "d n \ T \ finite(d n) \ card(d n) \ Suc n" if "n \ DIM('a) + 2" for n ``` lp15@63078 ` 456` ``` using that ``` lp15@63078 ` 457` ``` proof (induction n) ``` lp15@63078 ` 458` ``` case 0 ``` lp15@63078 ` 459` ``` then show ?case by (simp add: c) ``` lp15@63078 ` 460` ``` next ``` lp15@63078 ` 461` ``` case (Suc n) ``` lp15@63078 ` 462` ``` then show ?case by (auto simp: c card_insert_if) ``` lp15@63078 ` 463` ``` qed ``` lp15@63078 ` 464` ``` have aff_dim_le: "aff_dim(\(d n)) \ DIM('a) - int n" if "n \ DIM('a) + 2" for n ``` lp15@63078 ` 465` ``` using that ``` lp15@63078 ` 466` ``` proof (induction n) ``` lp15@63078 ` 467` ``` case 0 ``` lp15@63078 ` 468` ``` then show ?case ``` lp15@63078 ` 469` ``` by (simp add: aff_dim_le_DIM) ``` lp15@63078 ` 470` ``` next ``` lp15@63078 ` 471` ``` case (Suc n) ``` lp15@63078 ` 472` ``` have fs: "\d (Suc n) face_of S" ``` lp15@63078 ` 473` ``` by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE) ``` lp15@63078 ` 474` ``` have condn: "convex (\d n)" ``` lp15@63078 ` 475` ``` using Suc.prems nat_le_linear not_less_eq_eq ``` lp15@63078 ` 476` ``` by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc) ``` lp15@63078 ` 477` ``` have fdn: "\d (Suc n) face_of \d n" ``` lp15@63078 ` 478` ``` 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) ``` lp15@63078 ` 479` ``` have ne: "\d (Suc n) \ \d n" ``` lp15@63078 ` 480` ``` by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans) ``` lp15@63078 ` 481` ``` have *: "\m::int. \d. \d'::int. d < d' \ d' \ m - n \ d \ m - of_nat(n+1)" ``` lp15@63078 ` 482` ``` by arith ``` lp15@63078 ` 483` ``` have "aff_dim (\d (Suc n)) < aff_dim (\d n)" ``` lp15@63078 ` 484` ``` by (rule face_of_aff_dim_lt [OF condn fdn ne]) ``` lp15@63078 ` 485` ``` moreover have "aff_dim (\d n) \ int (DIM('a)) - int n" ``` lp15@63078 ` 486` ``` using Suc by auto ``` lp15@63078 ` 487` ``` ultimately ``` lp15@63078 ` 488` ``` have "aff_dim (\d (Suc n)) \ int (DIM('a)) - (n+1)" by arith ``` lp15@63078 ` 489` ``` then show ?case by linarith ``` lp15@63078 ` 490` ``` qed ``` lp15@63078 ` 491` ``` have "aff_dim (\d (DIM('a) + 2)) \ -2" ``` lp15@63078 ` 492` ``` using aff_dim_le [OF order_refl] by simp ``` lp15@63078 ` 493` ``` with aff_dim_geq [of "\d (DIM('a) + 2)"] show ?thesis ``` lp15@63078 ` 494` ``` using order.trans by fastforce ``` lp15@63078 ` 495` ```next ``` lp15@63078 ` 496` ``` case False ``` lp15@63078 ` 497` ``` then show ?thesis ``` lp15@63078 ` 498` ``` apply simp ``` lp15@63078 ` 499` ``` apply (erule ex_forward) ``` lp15@63078 ` 500` ``` by blast ``` lp15@63078 ` 501` ```qed ``` lp15@63078 ` 502` lp15@63078 ` 503` ```lemma faces_of_translation: ``` lp15@63078 ` 504` ``` "{F. F face_of image (\x. a + x) S} = image (image (\x. a + x)) {F. F face_of S}" ``` lp15@63078 ` 505` ```apply (rule subset_antisym, clarify) ``` lp15@63078 ` 506` ```apply (auto simp: image_iff) ``` lp15@63078 ` 507` ```apply (metis face_of_imp_subset face_of_translation_eq subset_imageE) ``` lp15@63078 ` 508` ```done ``` lp15@63078 ` 509` lp15@63078 ` 510` ```proposition face_of_Times: ``` lp15@63078 ` 511` ``` assumes "F face_of S" and "F' face_of S'" ``` lp15@63078 ` 512` ``` shows "(F \ F') face_of (S \ S')" ``` lp15@63078 ` 513` ```proof - ``` lp15@63078 ` 514` ``` have "F \ F' \ S \ S'" ``` lp15@63078 ` 515` ``` using assms [unfolded face_of_def] by blast ``` lp15@63078 ` 516` ``` moreover ``` lp15@63078 ` 517` ``` have "convex (F \ F')" ``` lp15@63078 ` 518` ``` using assms [unfolded face_of_def] by (blast intro: convex_Times) ``` lp15@63078 ` 519` ``` moreover ``` lp15@63078 ` 520` ``` have "a \ F \ a' \ F' \ b \ F \ b' \ F'" ``` lp15@63078 ` 521` ``` if "a \ S" "b \ S" "a' \ S'" "b' \ S'" "x \ F \ F'" "x \ open_segment (a,a') (b,b')" ``` lp15@63078 ` 522` ``` for a b a' b' x ``` lp15@63078 ` 523` ``` proof (cases "b=a \ b'=a'") ``` lp15@63078 ` 524` ``` case True with that show ?thesis ``` lp15@63078 ` 525` ``` using assms ``` lp15@63078 ` 526` ``` by (force simp: in_segment dest: face_ofD) ``` lp15@63078 ` 527` ``` next ``` lp15@63078 ` 528` ``` case False with assms [unfolded face_of_def] that show ?thesis ``` lp15@63078 ` 529` ``` by (blast dest!: open_segment_PairD) ``` lp15@63078 ` 530` ``` qed ``` lp15@63078 ` 531` ``` ultimately show ?thesis ``` lp15@63078 ` 532` ``` unfolding face_of_def by blast ``` lp15@63078 ` 533` ```qed ``` lp15@63078 ` 534` lp15@63078 ` 535` ```corollary face_of_Times_decomp: ``` lp15@63078 ` 536` ``` fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" ``` lp15@63078 ` 537` ``` shows "c face_of (S \ S') \ (\F F'. F face_of S \ F' face_of S' \ c = F \ F')" ``` lp15@63078 ` 538` ``` (is "?lhs = ?rhs") ``` lp15@63078 ` 539` ```proof ``` lp15@63078 ` 540` ``` assume c: ?lhs ``` lp15@63078 ` 541` ``` show ?rhs ``` lp15@63078 ` 542` ``` proof (cases "c = {}") ``` lp15@63078 ` 543` ``` case True then show ?thesis by auto ``` lp15@63078 ` 544` ``` next ``` lp15@63078 ` 545` ``` case False ``` lp15@63078 ` 546` ``` have 1: "fst ` c \ S" "snd ` c \ S'" ``` lp15@63078 ` 547` ``` using c face_of_imp_subset by fastforce+ ``` lp15@63078 ` 548` ``` have "convex c" ``` lp15@63078 ` 549` ``` using c by (metis face_of_imp_convex) ``` lp15@63078 ` 550` ``` have conv: "convex (fst ` c)" "convex (snd ` c)" ``` lp15@63078 ` 551` ``` by (simp_all add: \convex c\ convex_linear_image fst_linear snd_linear) ``` lp15@63078 ` 552` ``` have fstab: "a \ fst ` c \ b \ fst ` c" ``` lp15@63078 ` 553` ``` if "a \ S" "b \ S" "x \ open_segment a b" "(x,x') \ c" for a b x x' ``` lp15@63078 ` 554` ``` proof - ``` lp15@63078 ` 555` ``` have *: "(x,x') \ open_segment (a,x') (b,x')" ``` lp15@63078 ` 556` ``` using that by (auto simp: in_segment) ``` lp15@63078 ` 557` ``` show ?thesis ``` lp15@63078 ` 558` ``` using face_ofD [OF c *] that face_of_imp_subset [OF c] by force ``` lp15@63078 ` 559` ``` qed ``` lp15@63078 ` 560` ``` have fst: "fst ` c face_of S" ``` lp15@63078 ` 561` ``` by (force simp: face_of_def 1 conv fstab) ``` lp15@63078 ` 562` ``` have sndab: "a' \ snd ` c \ b' \ snd ` c" ``` lp15@63078 ` 563` ``` if "a' \ S'" "b' \ S'" "x' \ open_segment a' b'" "(x,x') \ c" for a' b' x x' ``` lp15@63078 ` 564` ``` proof - ``` lp15@63078 ` 565` ``` have *: "(x,x') \ open_segment (x,a') (x,b')" ``` lp15@63078 ` 566` ``` using that by (auto simp: in_segment) ``` lp15@63078 ` 567` ``` show ?thesis ``` lp15@63078 ` 568` ``` using face_ofD [OF c *] that face_of_imp_subset [OF c] by force ``` lp15@63078 ` 569` ``` qed ``` lp15@63078 ` 570` ``` have snd: "snd ` c face_of S'" ``` lp15@63078 ` 571` ``` by (force simp: face_of_def 1 conv sndab) ``` lp15@63078 ` 572` ``` have cc: "rel_interior c \ rel_interior (fst ` c) \ rel_interior (snd ` c)" ``` lp15@63078 ` 573` ``` by (force simp: face_of_Times rel_interior_Times conv fst snd \convex c\ fst_linear snd_linear rel_interior_convex_linear_image [symmetric]) ``` lp15@63078 ` 574` ``` have "c = fst ` c \ snd ` c" ``` lp15@63078 ` 575` ``` apply (rule face_of_eq [OF c]) ``` lp15@63078 ` 576` ``` apply (simp_all add: face_of_Times rel_interior_Times conv fst snd) ``` lp15@63078 ` 577` ``` using False rel_interior_eq_empty \convex c\ cc ``` lp15@63078 ` 578` ``` apply blast ``` lp15@63078 ` 579` ``` done ``` lp15@63078 ` 580` ``` with fst snd show ?thesis by metis ``` lp15@63078 ` 581` ``` qed ``` lp15@63078 ` 582` ```next ``` lp15@63078 ` 583` ``` assume ?rhs with face_of_Times show ?lhs by auto ``` lp15@63078 ` 584` ```qed ``` lp15@63078 ` 585` lp15@63078 ` 586` ```lemma face_of_Times_eq: ``` lp15@63078 ` 587` ``` fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" ``` lp15@63078 ` 588` ``` shows "(F \ F') face_of (S \ S') \ ``` lp15@63078 ` 589` ``` F = {} \ F' = {} \ F face_of S \ F' face_of S'" ``` lp15@63078 ` 590` ```by (auto simp: face_of_Times_decomp times_eq_iff) ``` lp15@63078 ` 591` lp15@63078 ` 592` ```lemma hyperplane_face_of_halfspace_le: "{x. a \ x = b} face_of {x. a \ x \ b}" ``` lp15@63078 ` 593` ```proof - ``` lp15@63078 ` 594` ``` have "{x. a \ x \ b} \ {x. a \ x = b} = {x. a \ x = b}" ``` lp15@63078 ` 595` ``` by auto ``` lp15@63078 ` 596` ``` with face_of_Int_supporting_hyperplane_le [OF convex_halfspace_le [of a b], of a b] ``` lp15@63078 ` 597` ``` show ?thesis by auto ``` lp15@63078 ` 598` ```qed ``` lp15@63078 ` 599` lp15@63078 ` 600` ```lemma hyperplane_face_of_halfspace_ge: "{x. a \ x = b} face_of {x. a \ x \ b}" ``` lp15@63078 ` 601` ```proof - ``` lp15@63078 ` 602` ``` have "{x. a \ x \ b} \ {x. a \ x = b} = {x. a \ x = b}" ``` lp15@63078 ` 603` ``` by auto ``` lp15@63078 ` 604` ``` with face_of_Int_supporting_hyperplane_ge [OF convex_halfspace_ge [of b a], of b a] ``` lp15@63078 ` 605` ``` show ?thesis by auto ``` lp15@63078 ` 606` ```qed ``` lp15@63078 ` 607` lp15@63078 ` 608` ```lemma face_of_halfspace_le: ``` lp15@63078 ` 609` ``` fixes a :: "'n::euclidean_space" ``` lp15@63078 ` 610` ``` shows "F face_of {x. a \ x \ b} \ ``` lp15@63078 ` 611` ``` F = {} \ F = {x. a \ x = b} \ F = {x. a \ x \ b}" ``` lp15@63078 ` 612` ``` (is "?lhs = ?rhs") ``` lp15@63078 ` 613` ```proof (cases "a = 0") ``` lp15@63078 ` 614` ``` case True then show ?thesis ``` lp15@63078 ` 615` ``` using face_of_affine_eq affine_UNIV by auto ``` lp15@63078 ` 616` ```next ``` lp15@63078 ` 617` ``` case False ``` lp15@63078 ` 618` ``` then have ine: "interior {x. a \ x \ b} \ {}" ``` lp15@63078 ` 619` ``` using halfspace_eq_empty_lt interior_halfspace_le by blast ``` lp15@63078 ` 620` ``` show ?thesis ``` lp15@63078 ` 621` ``` proof ``` lp15@63078 ` 622` ``` assume L: ?lhs ``` lp15@63078 ` 623` ``` have "F \ {x. a \ x \ b} \ F face_of {x. a \ x = b}" ``` lp15@63078 ` 624` ``` using False ``` lp15@63078 ` 625` ``` apply (simp add: frontier_halfspace_le [symmetric] rel_frontier_nonempty_interior [OF ine, symmetric]) ``` lp15@63078 ` 626` ``` apply (rule face_of_subset [OF L]) ``` lp15@63078 ` 627` ``` apply (simp add: face_of_subset_rel_frontier [OF L]) ``` lp15@63078 ` 628` ``` apply (force simp: rel_frontier_def closed_halfspace_le) ``` lp15@63078 ` 629` ``` done ``` lp15@63078 ` 630` ``` with L show ?rhs ``` lp15@63078 ` 631` ``` using affine_hyperplane face_of_affine_eq by blast ``` lp15@63078 ` 632` ``` next ``` lp15@63078 ` 633` ``` assume ?rhs ``` lp15@63078 ` 634` ``` then show ?lhs ``` lp15@63078 ` 635` ``` by (metis convex_halfspace_le empty_face_of face_of_refl hyperplane_face_of_halfspace_le) ``` lp15@63078 ` 636` ``` qed ``` lp15@63078 ` 637` ```qed ``` lp15@63078 ` 638` lp15@63078 ` 639` ```lemma face_of_halfspace_ge: ``` lp15@63078 ` 640` ``` fixes a :: "'n::euclidean_space" ``` lp15@63078 ` 641` ``` shows "F face_of {x. a \ x \ b} \ ``` lp15@63078 ` 642` ``` F = {} \ F = {x. a \ x = b} \ F = {x. a \ x \ b}" ``` lp15@63078 ` 643` ```using face_of_halfspace_le [of F "-a" "-b"] by simp ``` lp15@63078 ` 644` lp15@63078 ` 645` ```subsection\Exposed faces\ ``` lp15@63078 ` 646` lp15@63078 ` 647` ```text\That is, faces that are intersection with supporting hyperplane\ ``` lp15@63078 ` 648` lp15@63078 ` 649` ```definition exposed_face_of :: "['a::euclidean_space set, 'a set] \ bool" ``` lp15@63078 ` 650` ``` (infixr "(exposed'_face'_of)" 50) ``` lp15@63078 ` 651` ``` where "T exposed_face_of S \ ``` lp15@63078 ` 652` ``` T face_of S \ (\a b. S \ {x. a \ x \ b} \ T = S \ {x. a \ x = b})" ``` lp15@63078 ` 653` lp15@63078 ` 654` ```lemma empty_exposed_face_of [iff]: "{} exposed_face_of S" ``` lp15@63078 ` 655` ``` apply (simp add: exposed_face_of_def) ``` lp15@63078 ` 656` ``` apply (rule_tac x=0 in exI) ``` lp15@63078 ` 657` ``` apply (rule_tac x=1 in exI, force) ``` lp15@63078 ` 658` ``` done ``` lp15@63078 ` 659` lp15@63078 ` 660` ```lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \ convex S" ``` lp15@63078 ` 661` ``` apply (simp add: exposed_face_of_def face_of_refl_eq, auto) ``` lp15@63078 ` 662` ``` apply (rule_tac x=0 in exI)+ ``` lp15@63078 ` 663` ``` apply force ``` lp15@63078 ` 664` ``` done ``` lp15@63078 ` 665` lp15@63078 ` 666` ```lemma exposed_face_of_refl: "convex S \ S exposed_face_of S" ``` lp15@63078 ` 667` ``` by simp ``` lp15@63078 ` 668` lp15@63078 ` 669` ```lemma exposed_face_of: ``` lp15@63078 ` 670` ``` "T exposed_face_of S \ ``` lp15@63078 ` 671` ``` T face_of S \ ``` lp15@63078 ` 672` ``` (T = {} \ T = S \ ``` lp15@63078 ` 673` ``` (\a b. a \ 0 \ S \ {x. a \ x \ b} \ T = S \ {x. a \ x = b}))" ``` lp15@63078 ` 674` ```proof (cases "T = {}") ``` lp15@63078 ` 675` ``` case True then show ?thesis ``` lp15@63078 ` 676` ``` by simp ``` lp15@63078 ` 677` ```next ``` lp15@63078 ` 678` ``` case False ``` lp15@63078 ` 679` ``` show ?thesis ``` lp15@63078 ` 680` ``` proof (cases "T = S") ``` lp15@63078 ` 681` ``` case True then show ?thesis ``` lp15@63078 ` 682` ``` by (simp add: face_of_refl_eq) ``` lp15@63078 ` 683` ``` next ``` lp15@63078 ` 684` ``` case False ``` lp15@63078 ` 685` ``` with \T \ {}\ show ?thesis ``` lp15@63078 ` 686` ``` apply (auto simp: exposed_face_of_def) ``` lp15@63078 ` 687` ``` apply (metis inner_zero_left) ``` lp15@63078 ` 688` ``` done ``` lp15@63078 ` 689` ``` qed ``` lp15@63078 ` 690` ```qed ``` lp15@63078 ` 691` lp15@63078 ` 692` ```lemma exposed_face_of_Int_supporting_hyperplane_le: ``` lp15@63078 ` 693` ``` "\convex S; \x. x \ S \ a \ x \ b\ \ (S \ {x. a \ x = b}) exposed_face_of S" ``` lp15@63078 ` 694` ```by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le) ``` lp15@63078 ` 695` lp15@63078 ` 696` ```lemma exposed_face_of_Int_supporting_hyperplane_ge: ``` lp15@63078 ` 697` ``` "\convex S; \x. x \ S \ a \ x \ b\ \ (S \ {x. a \ x = b}) exposed_face_of S" ``` lp15@63078 ` 698` ```using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp ``` lp15@63078 ` 699` lp15@63078 ` 700` ```proposition exposed_face_of_Int: ``` lp15@63078 ` 701` ``` assumes "T exposed_face_of S" ``` lp15@63078 ` 702` ``` and "u exposed_face_of S" ``` lp15@63078 ` 703` ``` shows "(T \ u) exposed_face_of S" ``` lp15@63078 ` 704` ```proof - ``` lp15@63078 ` 705` ``` obtain a b where T: "S \ {x. a \ x = b} face_of S" ``` lp15@63078 ` 706` ``` and S: "S \ {x. a \ x \ b}" ``` lp15@63078 ` 707` ``` and teq: "T = S \ {x. a \ x = b}" ``` lp15@63078 ` 708` ``` using assms by (auto simp: exposed_face_of_def) ``` lp15@63078 ` 709` ``` obtain a' b' where u: "S \ {x. a' \ x = b'} face_of S" ``` lp15@63078 ` 710` ``` and s': "S \ {x. a' \ x \ b'}" ``` lp15@63078 ` 711` ``` and ueq: "u = S \ {x. a' \ x = b'}" ``` lp15@63078 ` 712` ``` using assms by (auto simp: exposed_face_of_def) ``` lp15@63078 ` 713` ``` have tu: "T \ u face_of S" ``` lp15@63078 ` 714` ``` using T teq u ueq by (simp add: face_of_Int) ``` lp15@63078 ` 715` ``` have ss: "S \ {x. (a + a') \ x \ b + b'}" ``` lp15@63078 ` 716` ``` using S s' by (force simp: inner_left_distrib) ``` lp15@63078 ` 717` ``` show ?thesis ``` lp15@63078 ` 718` ``` apply (simp add: exposed_face_of_def tu) ``` lp15@63078 ` 719` ``` apply (rule_tac x="a+a'" in exI) ``` lp15@63078 ` 720` ``` apply (rule_tac x="b+b'" in exI) ``` lp15@63078 ` 721` ``` using S s' ``` lp15@63078 ` 722` ``` apply (fastforce simp: ss inner_left_distrib teq ueq) ``` lp15@63078 ` 723` ``` done ``` lp15@63078 ` 724` ```qed ``` lp15@63078 ` 725` lp15@63078 ` 726` ```proposition exposed_face_of_Inter: ``` lp15@63078 ` 727` ``` fixes P :: "'a::euclidean_space set set" ``` lp15@63078 ` 728` ``` assumes "P \ {}" ``` lp15@63078 ` 729` ``` and "\T. T \ P \ T exposed_face_of S" ``` lp15@63078 ` 730` ``` shows "\P exposed_face_of S" ``` lp15@63078 ` 731` ```proof - ``` lp15@63078 ` 732` ``` obtain Q where "finite Q" and QsubP: "Q \ P" "card Q \ DIM('a) + 2" and IntQ: "\Q = \P" ``` lp15@63078 ` 733` ``` using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of] ``` lp15@63078 ` 734` ``` by force ``` lp15@63078 ` 735` ``` show ?thesis ``` lp15@63078 ` 736` ``` proof (cases "Q = {}") ``` lp15@63078 ` 737` ``` case True then show ?thesis ``` lp15@63078 ` 738` ``` by (metis Inf_empty Inf_lower IntQ assms ex_in_conv subset_antisym top_greatest) ``` lp15@63078 ` 739` ``` next ``` lp15@63078 ` 740` ``` case False ``` lp15@63078 ` 741` ``` have "Q \ {T. T exposed_face_of S}" ``` lp15@63078 ` 742` ``` using QsubP assms by blast ``` lp15@63078 ` 743` ``` moreover have "Q \ {T. T exposed_face_of S} \ \Q exposed_face_of S" ``` lp15@63078 ` 744` ``` using \finite Q\ False ``` lp15@63078 ` 745` ``` apply (induction Q rule: finite_induct) ``` lp15@63078 ` 746` ``` using exposed_face_of_Int apply fastforce+ ``` lp15@63078 ` 747` ``` done ``` lp15@63078 ` 748` ``` ultimately show ?thesis ``` lp15@63078 ` 749` ``` by (simp add: IntQ) ``` lp15@63078 ` 750` ``` qed ``` lp15@63078 ` 751` ```qed ``` lp15@63078 ` 752` lp15@63078 ` 753` ```proposition exposed_face_of_sums: ``` lp15@63078 ` 754` ``` assumes "convex S" and "convex T" ``` lp15@63078 ` 755` ``` and "F exposed_face_of {x + y | x y. x \ S \ y \ T}" ``` lp15@63078 ` 756` ``` (is "F exposed_face_of ?ST") ``` lp15@63078 ` 757` ``` obtains k l ``` lp15@63078 ` 758` ``` where "k exposed_face_of S" "l exposed_face_of T" ``` lp15@63078 ` 759` ``` "F = {x + y | x y. x \ k \ y \ l}" ``` lp15@63078 ` 760` ```proof (cases "F = {}") ``` lp15@63078 ` 761` ``` case True then show ?thesis ``` lp15@63078 ` 762` ``` using that by blast ``` lp15@63078 ` 763` ```next ``` lp15@63078 ` 764` ``` case False ``` lp15@63078 ` 765` ``` show ?thesis ``` lp15@63078 ` 766` ``` proof (cases "F = ?ST") ``` lp15@63078 ` 767` ``` case True then show ?thesis ``` lp15@63078 ` 768` ``` using assms exposed_face_of_refl_eq that by blast ``` lp15@63078 ` 769` ``` next ``` lp15@63078 ` 770` ``` case False ``` lp15@63078 ` 771` ``` obtain p where "p \ F" using \F \ {}\ by blast ``` lp15@63078 ` 772` ``` moreover ``` lp15@63078 ` 773` ``` obtain u z where T: "?ST \ {x. u \ x = z} face_of ?ST" ``` lp15@63078 ` 774` ``` and S: "?ST \ {x. u \ x \ z}" ``` lp15@63078 ` 775` ``` and feq: "F = ?ST \ {x. u \ x = z}" ``` lp15@63078 ` 776` ``` using assms by (auto simp: exposed_face_of_def) ``` lp15@63078 ` 777` ``` ultimately obtain a0 b0 ``` lp15@63078 ` 778` ``` where p: "p = a0 + b0" and "a0 \ S" "b0 \ T" and z: "u \ p = z" ``` lp15@63078 ` 779` ``` by auto ``` lp15@63078 ` 780` ``` have lez: "u \ (x + y) \ z" if "x \ S" "y \ T" for x y ``` lp15@63078 ` 781` ``` using S that by auto ``` lp15@63078 ` 782` ``` have sef: "S \ {x. u \ x = u \ a0} exposed_face_of S" ``` lp15@63078 ` 783` ``` apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF \convex S\]) ``` lp15@63078 ` 784` ``` apply (metis p z add_le_cancel_right inner_right_distrib lez [OF _ \b0 \ T\]) ``` lp15@63078 ` 785` ``` done ``` lp15@63078 ` 786` ``` have tef: "T \ {x. u \ x = u \ b0} exposed_face_of T" ``` lp15@63078 ` 787` ``` apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF \convex T\]) ``` lp15@63078 ` 788` ``` apply (metis p z add.commute add_le_cancel_right inner_right_distrib lez [OF \a0 \ S\]) ``` lp15@63078 ` 789` ``` done ``` lp15@63078 ` 790` ``` have "{x + y |x y. x \ S \ u \ x = u \ a0 \ y \ T \ u \ y = u \ b0} \ F" ``` lp15@63078 ` 791` ``` by (auto simp: feq) (metis inner_right_distrib p z) ``` lp15@63078 ` 792` ``` moreover have "F \ {x + y |x y. x \ S \ u \ x = u \ a0 \ y \ T \ u \ y = u \ b0}" ``` lp15@63078 ` 793` ``` apply (auto simp: feq) ``` lp15@63078 ` 794` ``` apply (rename_tac x y) ``` lp15@63078 ` 795` ``` apply (rule_tac x=x in exI) ``` lp15@63078 ` 796` ``` apply (rule_tac x=y in exI, simp) ``` lp15@63078 ` 797` ``` using z p \a0 \ S\ \b0 \ T\ ``` lp15@63078 ` 798` ``` apply clarify ``` lp15@63078 ` 799` ``` apply (simp add: inner_right_distrib) ``` lp15@63078 ` 800` ``` apply (metis add_le_cancel_right antisym lez [unfolded inner_right_distrib] add.commute) ``` lp15@63078 ` 801` ``` done ``` lp15@63078 ` 802` ``` ultimately have "F = {x + y |x y. x \ S \ {x. u \ x = u \ a0} \ y \ T \ {x. u \ x = u \ b0}}" ``` lp15@63078 ` 803` ``` by blast ``` lp15@63078 ` 804` ``` then show ?thesis ``` lp15@63078 ` 805` ``` by (rule that [OF sef tef]) ``` lp15@63078 ` 806` ``` qed ``` lp15@63078 ` 807` ```qed ``` lp15@63078 ` 808` lp15@63078 ` 809` ```subsection\Extreme points of a set: its singleton faces\ ``` lp15@63078 ` 810` lp15@63078 ` 811` ```definition extreme_point_of :: "['a::real_vector, 'a set] \ bool" ``` lp15@63078 ` 812` ``` (infixr "(extreme'_point'_of)" 50) ``` lp15@63078 ` 813` ``` where "x extreme_point_of S \ ``` lp15@63078 ` 814` ``` x \ S \ (\a \ S. \b \ S. x \ open_segment a b)" ``` lp15@63078 ` 815` lp15@63078 ` 816` ```lemma extreme_point_of_stillconvex: ``` lp15@63078 ` 817` ``` "convex S \ (x extreme_point_of S \ x \ S \ convex(S - {x}))" ``` lp15@63078 ` 818` ``` by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def) ``` lp15@63078 ` 819` lp15@63078 ` 820` ```lemma face_of_singleton: ``` lp15@63078 ` 821` ``` "{x} face_of S \ x extreme_point_of S" ``` lp15@63078 ` 822` ```by (fastforce simp add: extreme_point_of_def face_of_def) ``` lp15@63078 ` 823` lp15@63078 ` 824` ```lemma extreme_point_not_in_REL_INTERIOR: ``` lp15@63078 ` 825` ``` fixes S :: "'a::real_normed_vector set" ``` lp15@63078 ` 826` ``` shows "\x extreme_point_of S; S \ {x}\ \ x \ rel_interior S" ``` lp15@63078 ` 827` ```apply (simp add: face_of_singleton [symmetric]) ``` lp15@63078 ` 828` ```apply (blast dest: face_of_disjoint_rel_interior) ``` lp15@63078 ` 829` ```done ``` lp15@63078 ` 830` lp15@63078 ` 831` ```lemma extreme_point_not_in_interior: ``` lp15@63078 ` 832` ``` fixes S :: "'a::{real_normed_vector, perfect_space} set" ``` lp15@63078 ` 833` ``` shows "x extreme_point_of S \ x \ interior S" ``` lp15@63078 ` 834` ```apply (case_tac "S = {x}") ``` lp15@63078 ` 835` ```apply (simp add: empty_interior_finite) ``` lp15@63078 ` 836` ```by (meson contra_subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior) ``` lp15@63078 ` 837` lp15@63078 ` 838` ```lemma extreme_point_of_face: ``` lp15@63078 ` 839` ``` "F face_of S \ v extreme_point_of F \ v extreme_point_of S \ v \ F" ``` lp15@63078 ` 840` ``` by (meson empty_subsetI face_of_face face_of_singleton insert_subset) ``` lp15@63078 ` 841` lp15@63078 ` 842` ```lemma extreme_point_of_convex_hull: ``` lp15@63078 ` 843` ``` "x extreme_point_of (convex hull S) \ x \ S" ``` lp15@63078 ` 844` ```apply (simp add: extreme_point_of_stillconvex) ``` lp15@63078 ` 845` ```using hull_minimal [of S "(convex hull S) - {x}" convex] ``` lp15@63078 ` 846` ```using hull_subset [of S convex] ``` lp15@63078 ` 847` ```apply blast ``` lp15@63078 ` 848` ```done ``` lp15@63078 ` 849` lp15@63078 ` 850` ```lemma extreme_points_of_convex_hull: ``` lp15@63078 ` 851` ``` "{x. x extreme_point_of (convex hull S)} \ S" ``` lp15@63078 ` 852` ```using extreme_point_of_convex_hull by auto ``` lp15@63078 ` 853` lp15@63078 ` 854` ```lemma extreme_point_of_empty [simp]: "~ (x extreme_point_of {})" ``` lp15@63078 ` 855` ``` by (simp add: extreme_point_of_def) ``` lp15@63078 ` 856` lp15@63078 ` 857` ```lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} \ x = a" ``` lp15@63078 ` 858` ``` using extreme_point_of_stillconvex by auto ``` lp15@63078 ` 859` lp15@63078 ` 860` ```lemma extreme_point_of_translation_eq: ``` lp15@63078 ` 861` ``` "(a + x) extreme_point_of (image (\x. a + x) S) \ x extreme_point_of S" ``` lp15@63078 ` 862` ```by (auto simp: extreme_point_of_def) ``` lp15@63078 ` 863` lp15@63078 ` 864` ```lemma extreme_points_of_translation: ``` lp15@63078 ` 865` ``` "{x. x extreme_point_of (image (\x. a + x) S)} = ``` lp15@63078 ` 866` ``` (\x. a + x) ` {x. x extreme_point_of S}" ``` lp15@63078 ` 867` ```using extreme_point_of_translation_eq ``` lp15@63078 ` 868` ```by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel) ``` lp15@63078 ` 869` lp15@63078 ` 870` ```lemma extreme_point_of_Int: ``` lp15@63078 ` 871` ``` "\x extreme_point_of S; x extreme_point_of T\ \ x extreme_point_of (S \ T)" ``` lp15@63078 ` 872` ```by (simp add: extreme_point_of_def) ``` lp15@63078 ` 873` lp15@63078 ` 874` ```lemma extreme_point_of_Int_supporting_hyperplane_le: ``` lp15@63078 ` 875` ``` "\S \ {x. a \ x = b} = {c}; \x. x \ S \ a \ x \ b\ \ c extreme_point_of S" ``` lp15@63078 ` 876` ```apply (simp add: face_of_singleton [symmetric]) ``` lp15@63078 ` 877` ```by (metis face_of_Int_supporting_hyperplane_le_strong convex_singleton) ``` lp15@63078 ` 878` lp15@63078 ` 879` ```lemma extreme_point_of_Int_supporting_hyperplane_ge: ``` lp15@63078 ` 880` ``` "\S \ {x. a \ x = b} = {c}; \x. x \ S \ a \ x \ b\ \ c extreme_point_of S" ``` lp15@63078 ` 881` ```apply (simp add: face_of_singleton [symmetric]) ``` lp15@63078 ` 882` ```by (metis face_of_Int_supporting_hyperplane_ge_strong convex_singleton) ``` lp15@63078 ` 883` lp15@63078 ` 884` ```lemma exposed_point_of_Int_supporting_hyperplane_le: ``` lp15@63078 ` 885` ``` "\S \ {x. a \ x = b} = {c}; \x. x \ S \ a \ x \ b\ \ {c} exposed_face_of S" ``` lp15@63078 ` 886` ```apply (simp add: exposed_face_of_def face_of_singleton) ``` lp15@63078 ` 887` ```apply (force simp: extreme_point_of_Int_supporting_hyperplane_le) ``` lp15@63078 ` 888` ```done ``` lp15@63078 ` 889` lp15@63078 ` 890` ```lemma exposed_point_of_Int_supporting_hyperplane_ge: ``` lp15@63078 ` 891` ``` "\S \ {x. a \ x = b} = {c}; \x. x \ S \ a \ x \ b\ \ {c} exposed_face_of S" ``` lp15@63078 ` 892` ```using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c] ``` lp15@63078 ` 893` ```by simp ``` lp15@63078 ` 894` lp15@63078 ` 895` ```lemma extreme_point_of_convex_hull_insert: ``` lp15@63078 ` 896` ``` "\finite S; a \ convex hull S\ \ a extreme_point_of (convex hull (insert a S))" ``` lp15@63078 ` 897` ```apply (case_tac "a \ S") ``` lp15@63078 ` 898` ```apply (simp add: hull_inc) ``` lp15@63078 ` 899` ```using face_of_convex_hulls [of "insert a S" "{a}"] ``` lp15@63078 ` 900` ```apply (auto simp: face_of_singleton hull_same) ``` lp15@63078 ` 901` ```done ``` lp15@63078 ` 902` lp15@63078 ` 903` ```subsection\Facets\ ``` lp15@63078 ` 904` lp15@63078 ` 905` ```definition facet_of :: "['a::euclidean_space set, 'a set] \ bool" ``` lp15@63078 ` 906` ``` (infixr "(facet'_of)" 50) ``` lp15@63078 ` 907` ``` where "F facet_of S \ F face_of S \ F \ {} \ aff_dim F = aff_dim S - 1" ``` lp15@63078 ` 908` lp15@63078 ` 909` ```lemma facet_of_empty [simp]: "~ S facet_of {}" ``` lp15@63078 ` 910` ``` by (simp add: facet_of_def) ``` lp15@63078 ` 911` lp15@63078 ` 912` ```lemma facet_of_irrefl [simp]: "~ S facet_of S " ``` lp15@63078 ` 913` ``` by (simp add: facet_of_def) ``` lp15@63078 ` 914` lp15@63078 ` 915` ```lemma facet_of_imp_face_of: "F facet_of S \ F face_of S" ``` lp15@63078 ` 916` ``` by (simp add: facet_of_def) ``` lp15@63078 ` 917` lp15@63078 ` 918` ```lemma facet_of_imp_subset: "F facet_of S \ F \ S" ``` lp15@63078 ` 919` ``` by (simp add: face_of_imp_subset facet_of_def) ``` lp15@63078 ` 920` lp15@63078 ` 921` ```lemma hyperplane_facet_of_halfspace_le: ``` lp15@63078 ` 922` ``` "a \ 0 \ {x. a \ x = b} facet_of {x. a \ x \ b}" ``` lp15@63078 ` 923` ```unfolding facet_of_def hyperplane_eq_empty ``` lp15@63078 ` 924` ```by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le ``` lp15@63078 ` 925` ``` DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_le) ``` lp15@63078 ` 926` lp15@63078 ` 927` ```lemma hyperplane_facet_of_halfspace_ge: ``` lp15@63078 ` 928` ``` "a \ 0 \ {x. a \ x = b} facet_of {x. a \ x \ b}" ``` lp15@63078 ` 929` ```unfolding facet_of_def hyperplane_eq_empty ``` lp15@63078 ` 930` ```by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge ``` lp15@63078 ` 931` ``` DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_ge) ``` lp15@63078 ` 932` lp15@63078 ` 933` ```lemma facet_of_halfspace_le: ``` lp15@63078 ` 934` ``` "F facet_of {x. a \ x \ b} \ a \ 0 \ F = {x. a \ x = b}" ``` lp15@63078 ` 935` ``` (is "?lhs = ?rhs") ``` lp15@63078 ` 936` ```proof ``` lp15@63078 ` 937` ``` assume c: ?lhs ``` lp15@63078 ` 938` ``` with c facet_of_irrefl show ?rhs ``` lp15@63078 ` 939` ``` by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm) ``` lp15@63078 ` 940` ```next ``` lp15@63078 ` 941` ``` assume ?rhs then show ?lhs ``` lp15@63078 ` 942` ``` by (simp add: hyperplane_facet_of_halfspace_le) ``` lp15@63078 ` 943` ```qed ``` lp15@63078 ` 944` lp15@63078 ` 945` ```lemma facet_of_halfspace_ge: ``` lp15@63078 ` 946` ``` "F facet_of {x. a \ x \ b} \ a \ 0 \ F = {x. a \ x = b}" ``` lp15@63078 ` 947` ```using facet_of_halfspace_le [of F "-a" "-b"] by simp ``` lp15@63078 ` 948` lp15@63078 ` 949` ```subsection \Edges: faces of affine dimension 1\ ``` lp15@63078 ` 950` lp15@63078 ` 951` ```definition edge_of :: "['a::euclidean_space set, 'a set] \ bool" (infixr "(edge'_of)" 50) ``` lp15@63078 ` 952` ``` where "e edge_of S \ e face_of S \ aff_dim e = 1" ``` lp15@63078 ` 953` lp15@63078 ` 954` ```lemma edge_of_imp_subset: ``` lp15@63078 ` 955` ``` "S edge_of T \ S \ T" ``` lp15@63078 ` 956` ```by (simp add: edge_of_def face_of_imp_subset) ``` lp15@63078 ` 957` lp15@63078 ` 958` ```subsection\Existence of extreme points\ ``` lp15@63078 ` 959` lp15@63078 ` 960` ```lemma different_norm_3_collinear_points: ``` lp15@63078 ` 961` ``` fixes a :: "'a::euclidean_space" ``` lp15@63078 ` 962` ``` assumes "x \ open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)" ``` lp15@63078 ` 963` ``` shows False ``` lp15@63078 ` 964` ```proof - ``` lp15@63078 ` 965` ``` obtain u where "norm ((1 - u) *\<^sub>R a + u *\<^sub>R b) = norm b" ``` lp15@63078 ` 966` ``` and "a \ b" ``` lp15@63078 ` 967` ``` and u01: "0 < u" "u < 1" ``` lp15@63078 ` 968` ``` using assms by (auto simp: open_segment_image_interval if_splits) ``` lp15@63078 ` 969` ``` then have "(1 - u) *\<^sub>R a \ (1 - u) *\<^sub>R a + ((1 - u) * 2) *\<^sub>R a \ u *\<^sub>R b = ``` lp15@63078 ` 970` ``` (1 - u * u) *\<^sub>R (a \ a)" ``` lp15@63078 ` 971` ``` using assms by (simp add: norm_eq algebra_simps inner_commute) ``` lp15@63078 ` 972` ``` then have "(1 - u) *\<^sub>R ((1 - u) *\<^sub>R a \ a + (2 * u) *\<^sub>R a \ b) = ``` lp15@63078 ` 973` ``` (1 - u) *\<^sub>R ((1 + u) *\<^sub>R (a \ a))" ``` lp15@63078 ` 974` ``` by (simp add: algebra_simps) ``` lp15@63078 ` 975` ``` then have "(1 - u) *\<^sub>R (a \ a) + (2 * u) *\<^sub>R (a \ b) = (1 + u) *\<^sub>R (a \ a)" ``` lp15@63078 ` 976` ``` using u01 by auto ``` lp15@63078 ` 977` ``` then have "a \ b = a \ a" ``` lp15@63078 ` 978` ``` using u01 by (simp add: algebra_simps) ``` lp15@63078 ` 979` ``` then have "a = b" ``` lp15@63078 ` 980` ``` using \norm(a) = norm(b)\ norm_eq vector_eq by fastforce ``` lp15@63078 ` 981` ``` then show ?thesis ``` lp15@63078 ` 982` ``` using \a \ b\ by force ``` lp15@63078 ` 983` ```qed ``` lp15@63078 ` 984` lp15@63078 ` 985` ```proposition extreme_point_exists_convex: ``` lp15@63078 ` 986` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 987` ``` assumes "compact S" "convex S" "S \ {}" ``` lp15@63078 ` 988` ``` obtains x where "x extreme_point_of S" ``` lp15@63078 ` 989` ```proof - ``` lp15@63078 ` 990` ``` obtain x where "x \ S" and xsup: "\y. y \ S \ norm y \ norm x" ``` lp15@63078 ` 991` ``` using distance_attains_sup [of S 0] assms by auto ``` lp15@63078 ` 992` ``` have False if "a \ S" "b \ S" and x: "x \ open_segment a b" for a b ``` lp15@63078 ` 993` ``` proof - ``` lp15@63078 ` 994` ``` have noax: "norm a \ norm x" and nobx: "norm b \ norm x" using xsup that by auto ``` lp15@63078 ` 995` ``` have "a \ b" ``` lp15@63078 ` 996` ``` using empty_iff open_segment_idem x by auto ``` lp15@63078 ` 997` ``` have *: "(1 - u) * na + u * nb < norm x" if "na < norm x" "nb \ norm x" "0 < u" "u < 1" for na nb u ``` lp15@63078 ` 998` ``` proof - ``` lp15@63078 ` 999` ``` have "(1 - u) * na + u * nb < (1 - u) * norm x + u * nb" ``` lp15@63078 ` 1000` ``` by (simp add: that) ``` lp15@63078 ` 1001` ``` also have "... \ (1 - u) * norm x + u * norm x" ``` lp15@63078 ` 1002` ``` by (simp add: that) ``` lp15@63078 ` 1003` ``` finally have "(1 - u) * na + u * nb < (1 - u) * norm x + u * norm x" . ``` lp15@63078 ` 1004` ``` then show ?thesis ``` lp15@63078 ` 1005` ``` using scaleR_collapse [symmetric, of "norm x" u] by auto ``` lp15@63078 ` 1006` ``` qed ``` lp15@63078 ` 1007` ``` have "norm x < norm x" if "norm a < norm x" ``` lp15@63078 ` 1008` ``` using x ``` lp15@63078 ` 1009` ``` apply (clarsimp simp only: open_segment_image_interval \a \ b\ if_False) ``` lp15@63078 ` 1010` ``` apply (rule norm_triangle_lt) ``` lp15@63078 ` 1011` ``` apply (simp add: norm_mult) ``` lp15@63078 ` 1012` ``` using * [of "norm a" "norm b"] nobx that ``` lp15@63078 ` 1013` ``` apply blast ``` lp15@63078 ` 1014` ``` done ``` lp15@63078 ` 1015` ``` moreover have "norm x < norm x" if "norm b < norm x" ``` lp15@63078 ` 1016` ``` using x ``` lp15@63078 ` 1017` ``` apply (clarsimp simp only: open_segment_image_interval \a \ b\ if_False) ``` lp15@63078 ` 1018` ``` apply (rule norm_triangle_lt) ``` lp15@63078 ` 1019` ``` apply (simp add: norm_mult) ``` lp15@63078 ` 1020` ``` using * [of "norm b" "norm a" "1-u" for u] noax that ``` lp15@63078 ` 1021` ``` apply (simp add: add.commute) ``` lp15@63078 ` 1022` ``` done ``` lp15@63078 ` 1023` ``` ultimately have "~ (norm a < norm x) \ ~ (norm b < norm x)" ``` lp15@63078 ` 1024` ``` by auto ``` lp15@63078 ` 1025` ``` then show ?thesis ``` lp15@63078 ` 1026` ``` using different_norm_3_collinear_points noax nobx that(3) by fastforce ``` lp15@63078 ` 1027` ``` qed ``` lp15@63078 ` 1028` ``` then show ?thesis ``` lp15@63078 ` 1029` ``` apply (rule_tac x=x in that) ``` lp15@63078 ` 1030` ``` apply (force simp: extreme_point_of_def \x \ S\) ``` lp15@63078 ` 1031` ``` done ``` lp15@63078 ` 1032` ```qed ``` lp15@63078 ` 1033` lp15@63078 ` 1034` ```subsection\Krein-Milman, the weaker form\ ``` lp15@63078 ` 1035` lp15@63078 ` 1036` ```proposition Krein_Milman: ``` lp15@63078 ` 1037` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1038` ``` assumes "compact S" "convex S" ``` lp15@63078 ` 1039` ``` shows "S = closure(convex hull {x. x extreme_point_of S})" ``` lp15@63078 ` 1040` ```proof (cases "S = {}") ``` lp15@63078 ` 1041` ``` case True then show ?thesis by simp ``` lp15@63078 ` 1042` ```next ``` lp15@63078 ` 1043` ``` case False ``` lp15@63078 ` 1044` ``` have "closed S" ``` lp15@63078 ` 1045` ``` by (simp add: \compact S\ compact_imp_closed) ``` lp15@63078 ` 1046` ``` have "closure (convex hull {x. x extreme_point_of S}) \ S" ``` lp15@63078 ` 1047` ``` apply (rule closure_minimal [OF hull_minimal \closed S\]) ``` lp15@63078 ` 1048` ``` using assms ``` lp15@63078 ` 1049` ``` apply (auto simp: extreme_point_of_def) ``` lp15@63078 ` 1050` ``` done ``` lp15@63078 ` 1051` ``` moreover have "u \ closure (convex hull {x. x extreme_point_of S})" ``` lp15@63078 ` 1052` ``` if "u \ S" for u ``` lp15@63078 ` 1053` ``` proof (rule ccontr) ``` lp15@63078 ` 1054` ``` assume unot: "u \ closure(convex hull {x. x extreme_point_of S})" ``` lp15@63078 ` 1055` ``` then obtain a b where "a \ u < b" ``` lp15@63078 ` 1056` ``` and ab: "\x. x \ closure(convex hull {x. x extreme_point_of S}) \ b < a \ x" ``` lp15@63078 ` 1057` ``` using separating_hyperplane_closed_point [of "closure(convex hull {x. x extreme_point_of S})"] ``` lp15@63078 ` 1058` ``` by blast ``` lp15@63078 ` 1059` ``` have "continuous_on S (op \ a)" ``` lp15@63078 ` 1060` ``` by (rule continuous_intros)+ ``` lp15@63078 ` 1061` ``` then obtain m where "m \ S" and m: "\y. y \ S \ a \ m \ a \ y" ``` lp15@63078 ` 1062` ``` using continuous_attains_inf [of S "\x. a \ x"] \compact S\ \u \ S\ ``` lp15@63078 ` 1063` ``` by auto ``` wenzelm@63148 ` 1064` ``` define T where "T = S \ {x. a \ x = a \ m}" ``` lp15@63078 ` 1065` ``` have "m \ T" ``` lp15@63078 ` 1066` ``` by (simp add: T_def \m \ S\) ``` lp15@63078 ` 1067` ``` moreover have "compact T" ``` lp15@63078 ` 1068` ``` by (simp add: T_def compact_Int_closed [OF \compact S\ closed_hyperplane]) ``` lp15@63078 ` 1069` ``` moreover have "convex T" ``` lp15@63078 ` 1070` ``` by (simp add: T_def convex_Int [OF \convex S\ convex_hyperplane]) ``` lp15@63078 ` 1071` ``` ultimately obtain v where v: "v extreme_point_of T" ``` lp15@63078 ` 1072` ``` using extreme_point_exists_convex [of T] by auto ``` lp15@63078 ` 1073` ``` then have "{v} face_of T" ``` lp15@63078 ` 1074` ``` by (simp add: face_of_singleton) ``` lp15@63078 ` 1075` ``` also have "T face_of S" ``` lp15@63078 ` 1076` ``` by (simp add: T_def m face_of_Int_supporting_hyperplane_ge [OF \convex S\]) ``` lp15@63078 ` 1077` ``` finally have "v extreme_point_of S" ``` lp15@63078 ` 1078` ``` by (simp add: face_of_singleton) ``` lp15@63078 ` 1079` ``` then have "b < a \ v" ``` lp15@63078 ` 1080` ``` using closure_subset by (simp add: closure_hull hull_inc ab) ``` lp15@63078 ` 1081` ``` then show False ``` lp15@63078 ` 1082` ``` using \a \ u < b\ \{v} face_of T\ face_of_imp_subset m T_def that by fastforce ``` lp15@63078 ` 1083` ``` qed ``` lp15@63078 ` 1084` ``` ultimately show ?thesis ``` lp15@63078 ` 1085` ``` by blast ``` lp15@63078 ` 1086` ```qed ``` lp15@63078 ` 1087` lp15@63078 ` 1088` ```text\Now the sharper form.\ ``` lp15@63078 ` 1089` lp15@63078 ` 1090` ```lemma Krein_Milman_Minkowski_aux: ``` lp15@63078 ` 1091` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1092` ``` assumes n: "dim S = n" and S: "compact S" "convex S" "0 \ S" ``` lp15@63078 ` 1093` ``` shows "0 \ convex hull {x. x extreme_point_of S}" ``` lp15@63078 ` 1094` ```using n S ``` lp15@63078 ` 1095` ```proof (induction n arbitrary: S rule: less_induct) ``` lp15@63078 ` 1096` ``` case (less n S) show ?case ``` lp15@63078 ` 1097` ``` proof (cases "0 \ rel_interior S") ``` lp15@63078 ` 1098` ``` case True with Krein_Milman show ?thesis ``` lp15@63078 ` 1099` ``` by (metis subsetD convex_convex_hull convex_rel_interior_closure less.prems(2) less.prems(3) rel_interior_subset) ``` lp15@63078 ` 1100` ``` next ``` lp15@63078 ` 1101` ``` case False ``` lp15@63078 ` 1102` ``` have "rel_interior S \ {}" ``` lp15@63078 ` 1103` ``` by (simp add: rel_interior_convex_nonempty_aux less) ``` lp15@63078 ` 1104` ``` then obtain c where c: "c \ rel_interior S" by blast ``` lp15@63078 ` 1105` ``` obtain a where "a \ 0" ``` lp15@63078 ` 1106` ``` and le_ay: "\y. y \ S \ a \ 0 \ a \ y" ``` lp15@63078 ` 1107` ``` and less_ay: "\y. y \ rel_interior S \ a \ 0 < a \ y" ``` lp15@63078 ` 1108` ``` by (blast intro: supporting_hyperplane_rel_boundary intro!: less False) ``` lp15@63078 ` 1109` ``` have face: "S \ {x. a \ x = 0} face_of S" ``` lp15@63078 ` 1110` ``` apply (rule face_of_Int_supporting_hyperplane_ge [OF \convex S\]) ``` lp15@63078 ` 1111` ``` using le_ay by auto ``` lp15@63078 ` 1112` ``` then have co: "compact (S \ {x. a \ x = 0})" "convex (S \ {x. a \ x = 0})" ``` lp15@63078 ` 1113` ``` using less.prems by (blast intro: face_of_imp_compact face_of_imp_convex)+ ``` lp15@63078 ` 1114` ``` have "a \ y = 0" if "y \ span (S \ {x. a \ x = 0})" for y ``` lp15@63078 ` 1115` ``` proof - ``` lp15@63078 ` 1116` ``` have "y \ span {x. a \ x = 0}" ``` lp15@63078 ` 1117` ``` by (metis inf.cobounded2 span_mono subsetCE that) ``` lp15@63469 ` 1118` ``` then show ?thesis ``` lp15@63469 ` 1119` ``` by (blast intro: span_induct [OF _ subspace_hyperplane]) ``` lp15@63078 ` 1120` ``` qed ``` lp15@63078 ` 1121` ``` then have "dim (S \ {x. a \ x = 0}) < n" ``` lp15@63078 ` 1122` ``` by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff ``` lp15@63078 ` 1123` ``` inf_le1 \dim S = n\ not_le rel_interior_subset span_0 span_clauses(1)) ``` lp15@63078 ` 1124` ``` then have "0 \ convex hull {x. x extreme_point_of (S \ {x. a \ x = 0})}" ``` lp15@63078 ` 1125` ``` by (rule less.IH) (auto simp: co less.prems) ``` lp15@63078 ` 1126` ``` then show ?thesis ``` lp15@63078 ` 1127` ``` by (metis (mono_tags, lifting) Collect_mono_iff \S \ {x. a \ x = 0} face_of S\ extreme_point_of_face hull_mono subset_iff) ``` lp15@63078 ` 1128` ``` qed ``` lp15@63078 ` 1129` ```qed ``` lp15@63078 ` 1130` lp15@63078 ` 1131` lp15@63078 ` 1132` ```theorem Krein_Milman_Minkowski: ``` lp15@63078 ` 1133` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1134` ``` assumes "compact S" "convex S" ``` lp15@63078 ` 1135` ``` shows "S = convex hull {x. x extreme_point_of S}" ``` lp15@63078 ` 1136` ```proof ``` lp15@63078 ` 1137` ``` show "S \ convex hull {x. x extreme_point_of S}" ``` lp15@63078 ` 1138` ``` proof ``` lp15@63078 ` 1139` ``` fix a assume [simp]: "a \ S" ``` lp15@63078 ` 1140` ``` have 1: "compact (op + (- a) ` S)" ``` lp15@63078 ` 1141` ``` by (simp add: \compact S\ compact_translation) ``` lp15@63078 ` 1142` ``` have 2: "convex (op + (- a) ` S)" ``` lp15@63078 ` 1143` ``` by (simp add: \convex S\ convex_translation) ``` lp15@63078 ` 1144` ``` show a_invex: "a \ convex hull {x. x extreme_point_of S}" ``` lp15@63078 ` 1145` ``` using Krein_Milman_Minkowski_aux [OF refl 1 2] ``` lp15@63078 ` 1146` ``` convex_hull_translation [of "-a"] ``` lp15@63078 ` 1147` ``` by (auto simp: extreme_points_of_translation translation_assoc) ``` lp15@63078 ` 1148` ``` qed ``` lp15@63078 ` 1149` ```next ``` lp15@63078 ` 1150` ``` show "convex hull {x. x extreme_point_of S} \ S" ``` lp15@63078 ` 1151` ``` proof - ``` lp15@63078 ` 1152` ``` have "{a. a extreme_point_of S} \ S" ``` lp15@63078 ` 1153` ``` using extreme_point_of_def by blast ``` lp15@63078 ` 1154` ``` then show ?thesis ``` lp15@63078 ` 1155` ``` by (simp add: \convex S\ hull_minimal) ``` lp15@63078 ` 1156` ``` qed ``` lp15@63078 ` 1157` ```qed ``` lp15@63078 ` 1158` lp15@63078 ` 1159` lp15@63078 ` 1160` ```subsection\Applying it to convex hulls of explicitly indicated finite sets\ ``` lp15@63078 ` 1161` lp15@63078 ` 1162` ```lemma Krein_Milman_polytope: ``` lp15@63078 ` 1163` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1164` ``` shows ``` lp15@63078 ` 1165` ``` "finite S ``` lp15@63078 ` 1166` ``` \ convex hull S = ``` lp15@63078 ` 1167` ``` convex hull {x. x extreme_point_of (convex hull S)}" ``` lp15@63078 ` 1168` ```by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull) ``` lp15@63078 ` 1169` lp15@63078 ` 1170` ```lemma extreme_points_of_convex_hull_eq: ``` lp15@63078 ` 1171` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1172` ``` shows ``` lp15@63078 ` 1173` ``` "\compact S; \T. T \ S \ convex hull T \ convex hull S\ ``` lp15@63078 ` 1174` ``` \ {x. x extreme_point_of (convex hull S)} = S" ``` lp15@63078 ` 1175` ```by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI) ``` lp15@63078 ` 1176` lp15@63078 ` 1177` lp15@63078 ` 1178` ```lemma extreme_point_of_convex_hull_eq: ``` lp15@63078 ` 1179` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1180` ``` shows ``` lp15@63078 ` 1181` ``` "\compact S; \T. T \ S \ convex hull T \ convex hull S\ ``` lp15@63078 ` 1182` ``` \ (x extreme_point_of (convex hull S) \ x \ S)" ``` lp15@63078 ` 1183` ```using extreme_points_of_convex_hull_eq by auto ``` lp15@63078 ` 1184` lp15@63078 ` 1185` ```lemma extreme_point_of_convex_hull_convex_independent: ``` lp15@63078 ` 1186` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1187` ``` assumes "compact S" and S: "\a. a \ S \ a \ convex hull (S - {a})" ``` lp15@63078 ` 1188` ``` shows "(x extreme_point_of (convex hull S) \ x \ S)" ``` lp15@63078 ` 1189` ```proof - ``` lp15@63078 ` 1190` ``` have "convex hull T \ convex hull S" if "T \ S" for T ``` lp15@63078 ` 1191` ``` proof - ``` lp15@63078 ` 1192` ``` obtain a where "T \ S" "a \ S" "a \ T" using \T \ S\ by blast ``` lp15@63078 ` 1193` ``` then show ?thesis ``` lp15@63078 ` 1194` ``` by (metis (full_types) Diff_eq_empty_iff Diff_insert0 S hull_mono hull_subset insert_Diff_single subsetCE) ``` lp15@63078 ` 1195` ``` qed ``` lp15@63078 ` 1196` ``` then show ?thesis ``` lp15@63078 ` 1197` ``` by (rule extreme_point_of_convex_hull_eq [OF \compact S\]) ``` lp15@63078 ` 1198` ```qed ``` lp15@63078 ` 1199` lp15@63078 ` 1200` ```lemma extreme_point_of_convex_hull_affine_independent: ``` lp15@63078 ` 1201` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1202` ``` shows ``` lp15@63078 ` 1203` ``` "~ affine_dependent S ``` lp15@63078 ` 1204` ``` \ (x extreme_point_of (convex hull S) \ x \ S)" ``` lp15@63078 ` 1205` ```by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc) ``` lp15@63078 ` 1206` lp15@63078 ` 1207` ```text\Elementary proofs exist, not requiring Euclidean spaces and all this development\ ``` lp15@63078 ` 1208` ```lemma extreme_point_of_convex_hull_2: ``` lp15@63078 ` 1209` ``` fixes x :: "'a::euclidean_space" ``` lp15@63078 ` 1210` ``` shows "x extreme_point_of (convex hull {a,b}) \ x = a \ x = b" ``` lp15@63078 ` 1211` ```proof - ``` lp15@63078 ` 1212` ``` have "x extreme_point_of (convex hull {a,b}) \ x \ {a,b}" ``` lp15@63078 ` 1213` ``` by (intro extreme_point_of_convex_hull_affine_independent affine_independent_2) ``` lp15@63078 ` 1214` ``` then show ?thesis ``` lp15@63078 ` 1215` ``` by simp ``` lp15@63078 ` 1216` ```qed ``` lp15@63078 ` 1217` lp15@63078 ` 1218` ```lemma extreme_point_of_segment: ``` lp15@63078 ` 1219` ``` fixes x :: "'a::euclidean_space" ``` lp15@63078 ` 1220` ``` shows ``` lp15@63078 ` 1221` ``` "x extreme_point_of closed_segment a b \ x = a \ x = b" ``` lp15@63078 ` 1222` ```by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull) ``` lp15@63078 ` 1223` lp15@63078 ` 1224` ```lemma face_of_convex_hull_subset: ``` lp15@63078 ` 1225` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1226` ``` assumes "compact S" and T: "T face_of (convex hull S)" ``` lp15@63078 ` 1227` ``` obtains s' where "s' \ S" "T = convex hull s'" ``` lp15@63078 ` 1228` ```apply (rule_tac s' = "{x. x extreme_point_of T}" in that) ``` lp15@63078 ` 1229` ```using T extreme_point_of_convex_hull extreme_point_of_face apply blast ``` lp15@63078 ` 1230` ```by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex) ``` lp15@63078 ` 1231` lp15@63078 ` 1232` lp15@66297 ` 1233` ```lemma face_of_convex_hull_aux: ``` lp15@66297 ` 1234` ``` assumes eq: "x *\<^sub>R p = u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c" ``` lp15@66297 ` 1235` ``` and x: "u + v + w = x" "x \ 0" and S: "affine S" "a \ S" "b \ S" "c \ S" ``` lp15@66297 ` 1236` ``` shows "p \ S" ``` lp15@66297 ` 1237` ```proof - ``` lp15@66297 ` 1238` ``` have "p = (u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x" ``` lp15@66297 ` 1239` ``` by (metis \x \ 0\ eq mult.commute right_inverse scaleR_one scaleR_scaleR) ``` lp15@66297 ` 1240` ``` moreover have "affine hull {a,b,c} \ S" ``` lp15@66297 ` 1241` ``` by (simp add: S hull_minimal) ``` lp15@66297 ` 1242` ``` moreover have "(u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x \ affine hull {a,b,c}" ``` lp15@66297 ` 1243` ``` apply (simp add: affine_hull_3) ``` lp15@66297 ` 1244` ``` apply (rule_tac x="u/x" in exI) ``` lp15@66297 ` 1245` ``` apply (rule_tac x="v/x" in exI) ``` lp15@66297 ` 1246` ``` apply (rule_tac x="w/x" in exI) ``` lp15@66297 ` 1247` ``` using x apply (auto simp: algebra_simps divide_simps) ``` lp15@66297 ` 1248` ``` done ``` lp15@66297 ` 1249` ``` ultimately show ?thesis by force ``` lp15@66297 ` 1250` ```qed ``` lp15@66297 ` 1251` lp15@66297 ` 1252` ```proposition face_of_convex_hull_insert_eq: ``` lp15@66297 ` 1253` ``` fixes a :: "'a :: euclidean_space" ``` lp15@66297 ` 1254` ``` assumes "finite S" and a: "a \ affine hull S" ``` lp15@66297 ` 1255` ``` shows "(F face_of (convex hull (insert a S)) \ ``` lp15@66297 ` 1256` ``` F face_of (convex hull S) \ ``` lp15@66297 ` 1257` ``` (\F'. F' face_of (convex hull S) \ F = convex hull (insert a F')))" ``` lp15@66297 ` 1258` ``` (is "F face_of ?CAS \ _") ``` lp15@66297 ` 1259` ```proof safe ``` lp15@66297 ` 1260` ``` assume F: "F face_of ?CAS" ``` lp15@66297 ` 1261` ``` and *: "\F'. F' face_of convex hull S \ F = convex hull insert a F'" ``` lp15@66297 ` 1262` ``` obtain T where T: "T \ insert a S" and FeqT: "F = convex hull T" ``` lp15@66297 ` 1263` ``` by (metis F \finite S\ compact_insert finite_imp_compact face_of_convex_hull_subset) ``` lp15@66297 ` 1264` ``` show "F face_of convex hull S" ``` lp15@66297 ` 1265` ``` proof (cases "a \ T") ``` lp15@66297 ` 1266` ``` case True ``` lp15@66297 ` 1267` ``` have "F = convex hull insert a (convex hull T \ convex hull S)" ``` lp15@66297 ` 1268` ``` proof ``` lp15@66297 ` 1269` ``` have "T \ insert a (convex hull T \ convex hull S)" ``` lp15@66297 ` 1270` ``` using T hull_subset by fastforce ``` lp15@66297 ` 1271` ``` then show "F \ convex hull insert a (convex hull T \ convex hull S)" ``` lp15@66297 ` 1272` ``` by (simp add: FeqT hull_mono) ``` lp15@66297 ` 1273` ``` show "convex hull insert a (convex hull T \ convex hull S) \ F" ``` lp15@66297 ` 1274` ``` apply (rule hull_minimal) ``` lp15@66297 ` 1275` ``` using True by (auto simp: \F = convex hull T\ hull_inc) ``` lp15@66297 ` 1276` ``` qed ``` lp15@66297 ` 1277` ``` moreover have "convex hull T \ convex hull S face_of convex hull S" ``` lp15@66297 ` 1278` ``` by (metis F FeqT convex_convex_hull face_of_slice hull_mono inf.absorb_iff2 subset_insertI) ``` lp15@66297 ` 1279` ``` ultimately show ?thesis ``` lp15@66297 ` 1280` ``` using * by force ``` lp15@66297 ` 1281` ``` next ``` lp15@66297 ` 1282` ``` case False ``` lp15@66297 ` 1283` ``` then show ?thesis ``` lp15@66297 ` 1284` ``` by (metis FeqT F T face_of_subset hull_mono subset_insert subset_insertI) ``` lp15@66297 ` 1285` ``` qed ``` lp15@66297 ` 1286` ```next ``` lp15@66297 ` 1287` ``` assume "F face_of convex hull S" ``` lp15@66297 ` 1288` ``` show "F face_of ?CAS" ``` lp15@66297 ` 1289` ``` by (simp add: \F face_of convex hull S\ a face_of_convex_hull_insert \finite S\) ``` lp15@66297 ` 1290` ```next ``` lp15@66297 ` 1291` ``` fix F ``` lp15@66297 ` 1292` ``` assume F: "F face_of convex hull S" ``` lp15@66297 ` 1293` ``` show "convex hull insert a F face_of ?CAS" ``` lp15@66297 ` 1294` ``` proof (cases "S = {}") ``` lp15@66297 ` 1295` ``` case True ``` lp15@66297 ` 1296` ``` then show ?thesis ``` lp15@66297 ` 1297` ``` using F face_of_affine_eq by auto ``` lp15@66297 ` 1298` ``` next ``` lp15@66297 ` 1299` ``` case False ``` lp15@66297 ` 1300` ``` have anotc: "a \ convex hull S" ``` lp15@66297 ` 1301` ``` by (metis (no_types) a affine_hull_convex_hull hull_inc) ``` lp15@66297 ` 1302` ``` show ?thesis ``` lp15@66297 ` 1303` ``` proof (cases "F = {}") ``` lp15@66297 ` 1304` ``` case True show ?thesis ``` lp15@66297 ` 1305` ``` using anotc by (simp add: \F = {}\ \finite S\ extreme_point_of_convex_hull_insert face_of_singleton) ``` lp15@66297 ` 1306` ``` next ``` lp15@66297 ` 1307` ``` case False ``` lp15@66297 ` 1308` ``` have "convex hull insert a F \ ?CAS" ``` lp15@66297 ` 1309` ``` by (simp add: F a \finite S\ convex_hull_subset face_of_convex_hull_insert face_of_imp_subset hull_inc) ``` lp15@66297 ` 1310` ``` moreover ``` lp15@66297 ` 1311` ``` have "(\y v. (1 - ub) *\<^sub>R a + ub *\<^sub>R b = (1 - v) *\<^sub>R a + v *\<^sub>R y \ ``` lp15@66297 ` 1312` ``` 0 \ v \ v \ 1 \ y \ F) \ ``` lp15@66297 ` 1313` ``` (\x u. (1 - uc) *\<^sub>R a + uc *\<^sub>R c = (1 - u) *\<^sub>R a + u *\<^sub>R x \ ``` lp15@66297 ` 1314` ``` 0 \ u \ u \ 1 \ x \ F)" ``` lp15@66297 ` 1315` ``` if *: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x ``` lp15@66297 ` 1316` ``` \ open_segment ((1 - ub) *\<^sub>R a + ub *\<^sub>R b) ((1 - uc) *\<^sub>R a + uc *\<^sub>R c)" ``` lp15@66297 ` 1317` ``` and "0 \ ub" "ub \ 1" "0 \ uc" "uc \ 1" "0 \ ux" "ux \ 1" ``` lp15@66297 ` 1318` ``` and b: "b \ convex hull S" and c: "c \ convex hull S" and "x \ F" ``` lp15@66297 ` 1319` ``` for b c ub uc ux x ``` lp15@66297 ` 1320` ``` proof - ``` lp15@66297 ` 1321` ``` obtain v where ne: "(1 - ub) *\<^sub>R a + ub *\<^sub>R b \ (1 - uc) *\<^sub>R a + uc *\<^sub>R c" ``` lp15@66297 ` 1322` ``` and eq: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x = ``` lp15@66297 ` 1323` ``` (1 - v) *\<^sub>R ((1 - ub) *\<^sub>R a + ub *\<^sub>R b) + v *\<^sub>R ((1 - uc) *\<^sub>R a + uc *\<^sub>R c)" ``` lp15@66297 ` 1324` ``` and "0 < v" "v < 1" ``` lp15@66297 ` 1325` ``` using * by (auto simp: in_segment) ``` lp15@66297 ` 1326` ``` then have 0: "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a + ``` lp15@66297 ` 1327` ``` (ux *\<^sub>R x - (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)) = 0" ``` lp15@66297 ` 1328` ``` by (auto simp: algebra_simps) ``` lp15@66297 ` 1329` ``` then have "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a = ``` lp15@66297 ` 1330` ``` ((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c + (-ux) *\<^sub>R x" ``` lp15@66297 ` 1331` ``` by (auto simp: algebra_simps) ``` lp15@66297 ` 1332` ``` then have "a \ affine hull S" if "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) \ 0" ``` lp15@66297 ` 1333` ``` apply (rule face_of_convex_hull_aux) ``` lp15@66297 ` 1334` ``` using b c that apply (auto simp: algebra_simps) ``` lp15@66297 ` 1335` ``` using F convex_hull_subset_affine_hull face_of_imp_subset \x \ F\ apply blast+ ``` lp15@66297 ` 1336` ``` done ``` lp15@66297 ` 1337` ``` then have "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) = 0" ``` lp15@66297 ` 1338` ``` using a by blast ``` lp15@66297 ` 1339` ``` with 0 have equx: "(1 - v) * ub + v * uc = ux" ``` lp15@66297 ` 1340` ``` and uxx: "ux *\<^sub>R x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)" ``` lp15@66297 ` 1341` ``` by auto (auto simp: algebra_simps) ``` lp15@66297 ` 1342` ``` show ?thesis ``` lp15@66297 ` 1343` ``` proof (cases "uc = 0") ``` lp15@66297 ` 1344` ``` case True ``` lp15@66297 ` 1345` ``` then show ?thesis ``` lp15@66297 ` 1346` ``` using equx 0 \0 \ ub\ \ub \ 1\ \v < 1\ \x \ F\ ``` lp15@66297 ` 1347` ``` apply (auto simp: algebra_simps) ``` lp15@66297 ` 1348` ``` apply (rule_tac x=x in exI, simp) ``` lp15@66297 ` 1349` ``` apply (rule_tac x=ub in exI, auto) ``` lp15@66297 ` 1350` ``` apply (metis add.left_neutral diff_eq_eq less_irrefl mult.commute mult_cancel_right1 real_vector.scale_cancel_left real_vector.scale_left_diff_distrib) ``` lp15@66297 ` 1351` ``` using \x \ F\ \uc \ 1\ apply blast ``` lp15@66297 ` 1352` ``` done ``` lp15@66297 ` 1353` ``` next ``` lp15@66297 ` 1354` ``` case False ``` lp15@66297 ` 1355` ``` show ?thesis ``` lp15@66297 ` 1356` ``` proof (cases "ub = 0") ``` lp15@66297 ` 1357` ``` case True ``` lp15@66297 ` 1358` ``` then show ?thesis ``` lp15@66297 ` 1359` ``` using equx 0 \0 \ uc\ \uc \ 1\ \0 < v\ \x \ F\ \uc \ 0\ by (force simp: algebra_simps) ``` lp15@66297 ` 1360` ``` next ``` lp15@66297 ` 1361` ``` case False ``` lp15@66297 ` 1362` ``` then have "0 < ub" "0 < uc" ``` lp15@66297 ` 1363` ``` using \uc \ 0\ \0 \ ub\ \0 \ uc\ by auto ``` lp15@66297 ` 1364` ``` then have "ux \ 0" ``` lp15@66297 ` 1365` ``` by (metis \0 < v\ \v < 1\ diff_ge_0_iff_ge dual_order.strict_implies_order equx leD le_add_same_cancel2 zero_le_mult_iff zero_less_mult_iff) ``` lp15@66297 ` 1366` ``` have "b \ F \ c \ F" ``` lp15@66297 ` 1367` ``` proof (cases "b = c") ``` lp15@66297 ` 1368` ``` case True ``` lp15@66297 ` 1369` ``` then show ?thesis ``` lp15@66297 ` 1370` ``` by (metis \ux \ 0\ equx real_vector.scale_cancel_left scaleR_add_left uxx \x \ F\) ``` lp15@66297 ` 1371` ``` next ``` lp15@66297 ` 1372` ``` case False ``` lp15@66297 ` 1373` ``` have "x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c) /\<^sub>R ux" ``` lp15@66297 ` 1374` ``` by (metis \ux \ 0\ uxx mult.commute right_inverse scaleR_one scaleR_scaleR) ``` lp15@66297 ` 1375` ``` also have "... = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c" ``` lp15@66297 ` 1376` ``` using \ux \ 0\ equx apply (auto simp: algebra_simps divide_simps) ``` lp15@66297 ` 1377` ``` by (metis add.commute add_diff_eq add_divide_distrib diff_add_cancel scaleR_add_left) ``` lp15@66297 ` 1378` ``` finally have "x = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c" . ``` lp15@66297 ` 1379` ``` then have "x \ open_segment b c" ``` lp15@66297 ` 1380` ``` apply (simp add: in_segment \b \ c\) ``` lp15@66297 ` 1381` ``` apply (rule_tac x="(v * uc) / ux" in exI) ``` lp15@66297 ` 1382` ``` using \0 \ ux\ \ux \ 0\ \0 < uc\ \0 < v\ \0 < ub\ \v < 1\ equx ``` lp15@66297 ` 1383` ``` apply (force simp: algebra_simps divide_simps) ``` lp15@66297 ` 1384` ``` done ``` lp15@66297 ` 1385` ``` then show ?thesis ``` lp15@66297 ` 1386` ``` by (rule face_ofD [OF F _ b c \x \ F\]) ``` lp15@66297 ` 1387` ``` qed ``` lp15@66297 ` 1388` ``` with \0 \ ub\ \ub \ 1\ \0 \ uc\ \uc \ 1\ show ?thesis by blast ``` lp15@66297 ` 1389` ``` qed ``` lp15@66297 ` 1390` ``` qed ``` lp15@66297 ` 1391` ``` qed ``` lp15@66297 ` 1392` ``` moreover have "convex hull F = F" ``` lp15@66297 ` 1393` ``` by (meson F convex_hull_eq face_of_imp_convex) ``` lp15@66297 ` 1394` ``` ultimately show ?thesis ``` lp15@66297 ` 1395` ``` unfolding face_of_def by (fastforce simp: convex_hull_insert_alt \S \ {}\ \F \ {}\) ``` lp15@66297 ` 1396` ``` qed ``` lp15@66297 ` 1397` ``` qed ``` lp15@66297 ` 1398` ```qed ``` lp15@66297 ` 1399` lp15@66297 ` 1400` ```lemma face_of_convex_hull_insert2: ``` lp15@66297 ` 1401` ``` fixes a :: "'a :: euclidean_space" ``` lp15@66297 ` 1402` ``` assumes S: "finite S" and a: "a \ affine hull S" and F: "F face_of convex hull S" ``` lp15@66297 ` 1403` ``` shows "convex hull (insert a F) face_of convex hull (insert a S)" ``` lp15@66297 ` 1404` ``` by (metis F face_of_convex_hull_insert_eq [OF S a]) ``` lp15@66297 ` 1405` lp15@63078 ` 1406` ```proposition face_of_convex_hull_affine_independent: ``` lp15@63078 ` 1407` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1408` ``` assumes "~ affine_dependent S" ``` lp15@63078 ` 1409` ``` shows "(T face_of (convex hull S) \ (\c. c \ S \ T = convex hull c))" ``` lp15@63078 ` 1410` ``` (is "?lhs = ?rhs") ``` lp15@63078 ` 1411` ```proof ``` lp15@63078 ` 1412` ``` assume ?lhs ``` lp15@63078 ` 1413` ``` then show ?rhs ``` lp15@63078 ` 1414` ``` by (meson \T face_of convex hull S\ aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact) ``` lp15@63078 ` 1415` ```next ``` lp15@63078 ` 1416` ``` assume ?rhs ``` lp15@63078 ` 1417` ``` then obtain c where "c \ S" and T: "T = convex hull c" ``` lp15@63078 ` 1418` ``` by blast ``` lp15@63078 ` 1419` ``` have "affine hull c \ affine hull (S - c) = {}" ``` lp15@63078 ` 1420` ``` apply (rule disjoint_affine_hull [OF assms \c \ S\], auto) ``` lp15@63078 ` 1421` ``` done ``` lp15@63078 ` 1422` ``` then have "affine hull c \ convex hull (S - c) = {}" ``` lp15@63078 ` 1423` ``` using convex_hull_subset_affine_hull by fastforce ``` lp15@63078 ` 1424` ``` then show ?lhs ``` lp15@63078 ` 1425` ``` by (metis face_of_convex_hulls \c \ S\ aff_independent_finite assms T) ``` lp15@63078 ` 1426` ```qed ``` lp15@63078 ` 1427` lp15@63078 ` 1428` ```lemma facet_of_convex_hull_affine_independent: ``` lp15@63078 ` 1429` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1430` ``` assumes "~ affine_dependent S" ``` lp15@63078 ` 1431` ``` shows "T facet_of (convex hull S) \ ``` lp15@63078 ` 1432` ``` T \ {} \ (\u. u \ S \ T = convex hull (S - {u}))" ``` lp15@63078 ` 1433` ``` (is "?lhs = ?rhs") ``` lp15@63078 ` 1434` ```proof ``` lp15@63078 ` 1435` ``` assume ?lhs ``` lp15@63078 ` 1436` ``` then have "T face_of (convex hull S)" "T \ {}" ``` lp15@63078 ` 1437` ``` and afft: "aff_dim T = aff_dim (convex hull S) - 1" ``` lp15@63078 ` 1438` ``` by (auto simp: facet_of_def) ``` lp15@63078 ` 1439` ``` then obtain c where "c \ S" and c: "T = convex hull c" ``` lp15@63078 ` 1440` ``` by (auto simp: face_of_convex_hull_affine_independent [OF assms]) ``` lp15@63078 ` 1441` ``` then have affs: "aff_dim S = aff_dim c + 1" ``` lp15@63078 ` 1442` ``` by (metis aff_dim_convex_hull afft eq_diff_eq) ``` lp15@63078 ` 1443` ``` have "~ affine_dependent c" ``` lp15@63078 ` 1444` ``` using \c \ S\ affine_dependent_subset assms by blast ``` lp15@63078 ` 1445` ``` with affs have "card (S - c) = 1" ``` lp15@63078 ` 1446` ``` apply (simp add: aff_dim_affine_independent [symmetric] aff_dim_convex_hull) ``` lp15@63078 ` 1447` ``` by (metis aff_dim_affine_independent aff_independent_finite One_nat_def \c \ S\ add.commute ``` lp15@63078 ` 1448` ``` add_diff_cancel_right' assms card_Diff_subset card_mono of_nat_1 of_nat_diff of_nat_eq_iff) ``` lp15@63078 ` 1449` ``` then obtain u where u: "u \ S - c" ``` lp15@63078 ` 1450` ``` by (metis DiffI \c \ S\ aff_independent_finite assms cancel_comm_monoid_add_class.diff_cancel ``` lp15@63078 ` 1451` ``` card_Diff_subset subsetI subset_antisym zero_neq_one) ``` lp15@63078 ` 1452` ``` then have u: "S = insert u c" ``` lp15@63078 ` 1453` ``` by (metis Diff_subset \c \ S\ \card (S - c) = 1\ card_1_singletonE double_diff insert_Diff insert_subset singletonD) ``` lp15@63078 ` 1454` ``` have "T = convex hull (c - {u})" ``` lp15@63078 ` 1455` ``` by (metis Diff_empty Diff_insert0 \T facet_of convex hull S\ c facet_of_irrefl insert_absorb u) ``` lp15@63078 ` 1456` ``` with \T \ {}\ show ?rhs ``` lp15@63078 ` 1457` ``` using c u by auto ``` lp15@63078 ` 1458` ```next ``` lp15@63078 ` 1459` ``` assume ?rhs ``` lp15@63078 ` 1460` ``` then obtain u where "T \ {}" "u \ S" and u: "T = convex hull (S - {u})" ``` lp15@63078 ` 1461` ``` by (force simp: facet_of_def) ``` lp15@63078 ` 1462` ``` then have "\ S \ {u}" ``` lp15@63078 ` 1463` ``` using \T \ {}\ u by auto ``` lp15@63078 ` 1464` ``` have [simp]: "aff_dim (convex hull (S - {u})) = aff_dim (convex hull S) - 1" ``` lp15@63078 ` 1465` ``` using assms \u \ S\ ``` lp15@63078 ` 1466` ``` apply (simp add: aff_dim_convex_hull affine_dependent_def) ``` lp15@63078 ` 1467` ``` apply (drule bspec, assumption) ``` lp15@63078 ` 1468` ``` by (metis add_diff_cancel_right' aff_dim_insert insert_Diff [of u S]) ``` lp15@63078 ` 1469` ``` show ?lhs ``` lp15@63078 ` 1470` ``` apply (subst u) ``` lp15@63078 ` 1471` ``` apply (simp add: \\ S \ {u}\ facet_of_def face_of_convex_hull_affine_independent [OF assms], blast) ``` lp15@63078 ` 1472` ``` done ``` lp15@63078 ` 1473` ```qed ``` lp15@63078 ` 1474` lp15@63078 ` 1475` ```lemma facet_of_convex_hull_affine_independent_alt: ``` lp15@63078 ` 1476` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1477` ``` shows ``` lp15@63078 ` 1478` ``` "~affine_dependent S ``` lp15@63078 ` 1479` ``` \ (T facet_of (convex hull S) \ ``` lp15@63078 ` 1480` ``` 2 \ card S \ (\u. u \ S \ T = convex hull (S - {u})))" ``` lp15@63078 ` 1481` ```apply (simp add: facet_of_convex_hull_affine_independent) ``` lp15@63078 ` 1482` ```apply (auto simp: Set.subset_singleton_iff) ``` lp15@63078 ` 1483` ```apply (metis Diff_cancel Int_empty_right Int_insert_right_if1 aff_independent_finite card_eq_0_iff card_insert_if card_mono card_subset_eq convex_hull_eq_empty eq_iff equals0D finite_insert finite_subset inf.absorb_iff2 insert_absorb insert_not_empty not_less_eq_eq numeral_2_eq_2) ``` lp15@63078 ` 1484` ```done ``` lp15@63078 ` 1485` lp15@63078 ` 1486` ```lemma segment_face_of: ``` lp15@63078 ` 1487` ``` assumes "(closed_segment a b) face_of S" ``` lp15@63078 ` 1488` ``` shows "a extreme_point_of S" "b extreme_point_of S" ``` lp15@63078 ` 1489` ```proof - ``` lp15@63078 ` 1490` ``` have as: "{a} face_of S" ``` lp15@63078 ` 1491` ``` by (metis (no_types) assms convex_hull_singleton empty_iff extreme_point_of_convex_hull_insert face_of_face face_of_singleton finite.emptyI finite.insertI insert_absorb insert_iff segment_convex_hull) ``` lp15@63078 ` 1492` ``` moreover have "{b} face_of S" ``` lp15@63078 ` 1493` ``` proof - ``` lp15@63078 ` 1494` ``` have "b \ convex hull {a} \ b extreme_point_of convex hull {b, a}" ``` lp15@63078 ` 1495` ``` by (meson extreme_point_of_convex_hull_insert finite.emptyI finite.insertI) ``` lp15@63078 ` 1496` ``` moreover have "closed_segment a b = convex hull {b, a}" ``` lp15@63078 ` 1497` ``` using closed_segment_commute segment_convex_hull by blast ``` lp15@63078 ` 1498` ``` ultimately show ?thesis ``` lp15@63078 ` 1499` ``` by (metis as assms face_of_face convex_hull_singleton empty_iff face_of_singleton insertE) ``` lp15@63078 ` 1500` ``` qed ``` lp15@63078 ` 1501` ``` ultimately show "a extreme_point_of S" "b extreme_point_of S" ``` lp15@63078 ` 1502` ``` using face_of_singleton by blast+ ``` lp15@63078 ` 1503` ```qed ``` lp15@63078 ` 1504` lp15@63078 ` 1505` lp15@63078 ` 1506` ```lemma Krein_Milman_frontier: ``` lp15@63078 ` 1507` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1508` ``` assumes "convex S" "compact S" ``` lp15@63078 ` 1509` ``` shows "S = convex hull (frontier S)" ``` lp15@63078 ` 1510` ``` (is "?lhs = ?rhs") ``` lp15@63078 ` 1511` ```proof ``` lp15@63078 ` 1512` ``` have "?lhs \ convex hull {x. x extreme_point_of S}" ``` lp15@63078 ` 1513` ``` using Krein_Milman_Minkowski assms by blast ``` lp15@63078 ` 1514` ``` also have "... \ ?rhs" ``` lp15@63078 ` 1515` ``` apply (rule hull_mono) ``` lp15@63078 ` 1516` ``` apply (auto simp: frontier_def extreme_point_not_in_interior) ``` lp15@63078 ` 1517` ``` using closure_subset apply (force simp: extreme_point_of_def) ``` lp15@63078 ` 1518` ``` done ``` lp15@63078 ` 1519` ``` finally show "?lhs \ ?rhs" . ``` lp15@63078 ` 1520` ```next ``` lp15@63078 ` 1521` ``` have "?rhs \ convex hull S" ``` lp15@63078 ` 1522` ``` by (metis Diff_subset \compact S\ closure_closed compact_eq_bounded_closed frontier_def hull_mono) ``` lp15@63078 ` 1523` ``` also have "... \ ?lhs" ``` lp15@63078 ` 1524` ``` by (simp add: \convex S\ hull_same) ``` lp15@63078 ` 1525` ``` finally show "?rhs \ ?lhs" . ``` lp15@63078 ` 1526` ```qed ``` lp15@63078 ` 1527` lp15@63078 ` 1528` ```subsection\Polytopes\ ``` lp15@63078 ` 1529` lp15@63078 ` 1530` ```definition polytope where ``` lp15@63078 ` 1531` ``` "polytope S \ \v. finite v \ S = convex hull v" ``` lp15@63078 ` 1532` lp15@63078 ` 1533` ```lemma polytope_translation_eq: "polytope (image (\x. a + x) S) \ polytope S" ``` lp15@63078 ` 1534` ```apply (simp add: polytope_def, safe) ``` lp15@63078 ` 1535` ```apply (metis convex_hull_translation finite_imageI translation_galois) ``` lp15@63078 ` 1536` ```by (metis convex_hull_translation finite_imageI) ``` lp15@63078 ` 1537` lp15@63078 ` 1538` ```lemma polytope_linear_image: "\linear f; polytope p\ \ polytope(image f p)" ``` lp15@63078 ` 1539` ``` unfolding polytope_def using convex_hull_linear_image by blast ``` lp15@63078 ` 1540` lp15@63078 ` 1541` ```lemma polytope_empty: "polytope {}" ``` lp15@63078 ` 1542` ``` using convex_hull_empty polytope_def by blast ``` lp15@63078 ` 1543` lp15@63078 ` 1544` ```lemma polytope_convex_hull: "finite S \ polytope(convex hull S)" ``` lp15@63078 ` 1545` ``` using polytope_def by auto ``` lp15@63078 ` 1546` lp15@63078 ` 1547` ```lemma polytope_Times: "\polytope S; polytope T\ \ polytope(S \ T)" ``` lp15@63078 ` 1548` ``` unfolding polytope_def ``` lp15@63078 ` 1549` ``` by (metis finite_cartesian_product convex_hull_Times) ``` lp15@63078 ` 1550` lp15@63078 ` 1551` ```lemma face_of_polytope_polytope: ``` lp15@63078 ` 1552` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1553` ``` shows "\polytope S; F face_of S\ \ polytope F" ``` lp15@63078 ` 1554` ```unfolding polytope_def ``` lp15@63078 ` 1555` ```by (meson face_of_convex_hull_subset finite_imp_compact finite_subset) ``` lp15@63078 ` 1556` lp15@63078 ` 1557` ```lemma finite_polytope_faces: ``` lp15@63078 ` 1558` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63078 ` 1559` ``` assumes "polytope S" ``` lp15@63078 ` 1560` ``` shows "finite {F. F face_of S}" ``` lp15@63078 ` 1561` ```proof - ``` lp15@63078 ` 1562` ``` obtain v where "finite v" "S = convex hull v" ``` lp15@63078 ` 1563` ``` using assms polytope_def by auto ``` lp15@63078 ` 1564` ``` have "finite (op hull convex ` {T. T \ v})" ``` lp15@63078 ` 1565` ``` by (simp add: \finite v\) ``` lp15@63078 ` 1566` ``` moreover have "{F. F face_of S} \ (op hull convex ` {T. T \ v})" ``` lp15@63078 ` 1567` ``` by (metis (no_types, lifting) \finite v\ \S = convex hull v\ face_of_convex_hull_subset finite_imp_compact image_eqI mem_Collect_eq subsetI) ``` lp15@63078 ` 1568` ``` ultimately show ?thesis ``` lp15@63078 ` 1569` ``` by (blast intro: finite_subset) ``` lp15@63078 ` 1570` ```qed ``` lp15@63078 ` 1571` lp15@63078 ` 1572` ```lemma finite_polytope_facets: ``` lp15@63078 ` 1573` ``` assumes "polytope S" ``` lp15@63078 ` 1574` ``` shows "finite {T. T facet_of S}" ``` lp15@63078 ` 1575` ```by (simp add: assms facet_of_def finite_polytope_faces) ``` lp15@63078 ` 1576` lp15@63078 ` 1577` ```lemma polytope_scaling: ``` lp15@63078 ` 1578` ``` assumes "polytope S" shows "polytope (image (\x. c *\<^sub>R x) S)" ``` lp15@63078 ` 1579` ```by (simp add: assms polytope_linear_image) ``` lp15@63078 ` 1580` lp15@63078 ` 1581` ```lemma polytope_imp_compact: ``` lp15@63078 ` 1582` ``` fixes S :: "'a::real_normed_vector set" ``` lp15@63078 ` 1583` ``` shows "polytope S \ compact S" ``` lp15@63078 ` 1584` ```by (metis finite_imp_compact_convex_hull polytope_def) ``` lp15@63078 ` 1585` lp15@63078 ` 1586` ```lemma polytope_imp_convex: "polytope S \ convex S" ``` lp15@63078 ` 1587` ``` by (metis convex_convex_hull polytope_def) ``` lp15@63078 ` 1588` lp15@63078 ` 1589` ```lemma polytope_imp_closed: ``` lp15@63078 ` 1590` ``` fixes S :: "'a::real_normed_vector set" ``` lp15@63078 ` 1591` ``` shows "polytope S \ closed S" ``` lp15@63078 ` 1592` ```by (simp add: compact_imp_closed polytope_imp_compact) ``` lp15@63078 ` 1593` lp15@63078 ` 1594` ```lemma polytope_imp_bounded: ``` lp15@63078 ` 1595` ``` fixes S :: "'a::real_normed_vector set" ``` lp15@63078 ` 1596` ``` shows "polytope S \ bounded S" ``` lp15@63078 ` 1597` ```by (simp add: compact_imp_bounded polytope_imp_compact) ``` lp15@63078 ` 1598` lp15@63078 ` 1599` ```lemma polytope_interval: "polytope(cbox a b)" ``` lp15@63078 ` 1600` ``` unfolding polytope_def by (meson closed_interval_as_convex_hull) ``` lp15@63078 ` 1601` lp15@63078 ` 1602` ```lemma polytope_sing: "polytope {a}" ``` lp15@63078 ` 1603` ``` using polytope_def by force ``` lp15@63078 ` 1604` lp15@66297 ` 1605` ```lemma face_of_polytope_insert: ``` lp15@66297 ` 1606` ``` "\polytope S; a \ affine hull S; F face_of S\ \ F face_of convex hull (insert a S)" ``` lp15@66297 ` 1607` ``` by (metis (no_types, lifting) affine_hull_convex_hull face_of_convex_hull_insert hull_insert polytope_def) ``` lp15@66297 ` 1608` lp15@66297 ` 1609` ```lemma face_of_polytope_insert2: ``` lp15@66297 ` 1610` ``` fixes a :: "'a :: euclidean_space" ``` lp15@66297 ` 1611` ``` assumes "polytope S" "a \ affine hull S" "F face_of S" ``` lp15@66297 ` 1612` ``` shows "convex hull (insert a F) face_of convex hull (insert a S)" ``` lp15@66297 ` 1613` ```proof - ``` lp15@66297 ` 1614` ``` obtain V where "finite V" "S = convex hull V" ``` lp15@66297 ` 1615` ``` using assms by (auto simp: polytope_def) ``` lp15@66297 ` 1616` ``` then have "convex hull (insert a F) face_of convex hull (insert a V)" ``` lp15@66297 ` 1617` ``` using affine_hull_convex_hull assms face_of_convex_hull_insert2 by blast ``` lp15@66297 ` 1618` ``` then show ?thesis ``` lp15@66297 ` 1619` ``` by (metis \S = convex hull V\ hull_insert) ``` lp15@66297 ` 1620` ```qed ``` lp15@66297 ` 1621` lp15@63078 ` 1622` lp15@63078 ` 1623` ```subsection\Polyhedra\ ``` lp15@63078 ` 1624` lp15@63078 ` 1625` ```definition polyhedron where ``` lp15@63078 ` 1626` ``` "polyhedron S \ ``` lp15@63078 ` 1627` ``` \F. finite F \ ``` lp15@63078 ` 1628` ``` S = \ F \ ``` lp15@63078 ` 1629` ``` (\h \ F. \a b. a \ 0 \ h = {x. a \ x \ b})" ``` lp15@63078 ` 1630` lp15@63078 ` 1631` ```lemma polyhedron_Int [intro,simp]: ``` lp15@63078 ` 1632` ``` "\polyhedron S; polyhedron T\ \ polyhedron (S \ T)" ``` lp15@63078 ` 1633` ``` apply (simp add: polyhedron_def, clarify) ``` lp15@63078 ` 1634` ``` apply (rename_tac F G) ``` lp15@63078 ` 1635` ``` apply (rule_tac x="F \ G" in exI, auto) ``` lp15@63078 ` 1636` ``` done ``` lp15@63078 ` 1637` lp15@63078 ` 1638` ```lemma polyhedron_UNIV [iff]: "polyhedron UNIV" ``` lp15@63078 ` 1639` ``` unfolding polyhedron_def ``` lp15@63078 ` 1640` ``` by (rule_tac x="{}" in exI) auto ``` lp15@63078 ` 1641` lp15@63078 ` 1642` ```lemma polyhedron_Inter [intro,simp]: ``` lp15@63078 ` 1643` ``` "\finite F; \S. S \ F \ polyhedron S\ \ polyhedron(\F)" ``` lp15@63078 ` 1644` ```by (induction F rule: finite_induct) auto ``` lp15@63078 ` 1645` lp15@63078 ` 1646` lp15@63078 ` 1647` ```lemma polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)" ``` lp15@63078 ` 1648` ```proof - ``` lp15@63078 ` 1649` ``` have "\a. a \ 0 \ ``` lp15@63078 ` 1650` ``` (\b. {x. (SOME i. i \ Basis) \ x \ - 1} = {x. a \ x \ b})" ``` lp15@63078 ` 1651` ``` by (rule_tac x="(SOME i. i \ Basis)" in exI) (force simp: SOME_Basis nonzero_Basis) ``` lp15@63078 ` 1652` ``` moreover have "\a b. a \ 0 \ ``` lp15@63078 ` 1653` ``` {x. - (SOME i. i \ Basis) \ x \ - 1} = {x. a \ x \ b}" ``` lp15@63078 ` 1654` ``` apply (rule_tac x="-(SOME i. i \ Basis)" in exI) ``` lp15@63078 ` 1655` ``` apply (rule_tac x="-1" in exI) ``` lp15@63078 ` 1656` ``` apply (simp add: SOME_Basis nonzero_Basis) ``` lp15@63078 ` 1657` ``` done ``` lp15@63078 ` 1658` ``` ultimately show ?thesis ``` lp15@63078 ` 1659` ``` unfolding polyhedron_def ``` lp15@63078 ` 1660` ``` apply (rule_tac x="{{x. (SOME i. i \ Basis) \ x \ -1}, ``` lp15@63078 ` 1661` ``` {x. -(SOME i. i \ Basis) \ x \ -1}}" in exI) ``` lp15@63078 ` 1662` ``` apply force ``` lp15@63078 ` 1663` ``` done ``` lp15@63078 ` 1664` ```qed ``` lp15@63078 ` 1665` lp15@63078 ` 1666` ```lemma polyhedron_halfspace_le: ``` lp15@63078 ` 1667` ``` fixes a :: "'a :: euclidean_space" ``` lp15@63078 ` 1668` ``` shows "polyhedron {x. a \ x \ b}" ``` lp15@63078 ` 1669` ```proof (cases "a = 0") ``` lp15@63078 ` 1670` ``` case True then show ?thesis by auto ``` lp15@63078 ` 1671` ```next ``` lp15@63078 ` 1672` ``` case False ``` lp15@63078 ` 1673` ``` then show ?thesis ``` lp15@63078 ` 1674` ``` unfolding polyhedron_def ``` lp15@63078 ` 1675` ``` by (rule_tac x="{{x. a \ x \ b}}" in exI) auto ``` lp15@63078 ` 1676` ```qed ``` lp15@63078 ` 1677` lp15@63078 ` 1678` ```lemma polyhedron_halfspace_ge: ``` lp15@63078 ` 1679` ``` fixes a :: "'a :: euclidean_space" ``` lp15@63078 ` 1680` ``` shows "polyhedron {x. a \ x \ b}" ``` lp15@63078 ` 1681` ```using polyhedron_halfspace_le [of "-a" "-b"] by simp ``` lp15@63078 ` 1682` lp15@63078 ` 1683` ```lemma polyhedron_hyperplane: ``` lp15@63078 ` 1684` ``` fixes a :: "'a :: euclidean_space" ``` lp15@63078 ` 1685` ``` shows "polyhedron {x. a \ x = b}" ``` lp15@63078 ` 1686` ```proof - ``` lp15@63078 ` 1687` ``` have "{x. a \ x = b} = {x. a \ x \ b} \ {x. a \ x \ b}" ``` lp15@63078 ` 1688` ``` by force ``` lp15@63078 ` 1689` ``` then show ?thesis ``` lp15@63078 ` 1690` ``` by (simp add: polyhedron_halfspace_ge polyhedron_halfspace_le) ``` lp15@63078 ` 1691` ```qed ``` lp15@63078 ` 1692` lp15@63078 ` 1693` ```lemma affine_imp_polyhedron: ``` lp15@63078 ` 1694` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@63078 ` 1695` ``` shows "affine S \ polyhedron S" ``` lp15@63078 ` 1696` ```by (metis affine_hull_eq polyhedron_Inter polyhedron_hyperplane affine_hull_finite_intersection_hyperplanes [of S]) ``` lp15@63078 ` 1697` lp15@63078 ` 1698` ```lemma polyhedron_imp_closed: ``` lp15@63078 ` 1699` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@63078 ` 1700` ``` shows "polyhedron S \ closed S" ``` lp15@63078 ` 1701` ```apply (simp add: polyhedron_def) ``` lp15@63078 ` 1702` ```using closed_halfspace_le by fastforce ``` lp15@63078 ` 1703` lp15@63078 ` 1704` ```lemma polyhedron_imp_convex: ``` lp15@63078 ` 1705` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@63078 ` 1706` ``` shows "polyhedron S \ convex S" ``` lp15@63078 ` 1707` ```apply (simp add: polyhedron_def) ``` lp15@63078 ` 1708` ```using convex_Inter convex_halfspace_le by fastforce ``` lp15@63078 ` 1709` lp15@63078 ` 1710` ```lemma polyhedron_affine_hull: ``` lp15@63078 ` 1711` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@63078 ` 1712` ``` shows "polyhedron(affine hull S)" ``` lp15@63078 ` 1713` ```by (simp add: affine_imp_polyhedron) ``` lp15@63078 ` 1714` lp15@63078 ` 1715` lp15@63078 ` 1716` ```subsection\Canonical polyhedron representation making facial structure explicit\ ``` lp15@63078 ` 1717` lp15@63078 ` 1718` ```lemma polyhedron_Int_affine: ``` lp15@63078 ` 1719` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@63078 ` 1720` ``` shows "polyhedron S \ ``` lp15@63078 ` 1721` ``` (\F. finite F \ S = (affine hull S) \ \F \ ``` lp15@63078 ` 1722` ``` (\h \ F. \a b. a \ 0 \ h = {x. a \ x \ b}))" ``` lp15@63078 ` 1723` ``` (is "?lhs = ?rhs") ``` lp15@63078 ` 1724` ```proof ``` lp15@63078 ` 1725` ``` assume ?lhs then show ?rhs ``` lp15@63078 ` 1726` ``` apply (simp add: polyhedron_def) ``` lp15@63078 ` 1727` ``` apply (erule ex_forward) ``` lp15@63078 ` 1728` ``` using hull_subset apply force ``` lp15@63078 ` 1729` ``` done ``` lp15@63078 ` 1730` ```next ``` lp15@63078 ` 1731` ``` assume ?rhs then show ?lhs ``` lp15@63078 ` 1732` ``` apply clarify ``` lp15@63078 ` 1733` ``` apply (erule ssubst) ``` lp15@63078 ` 1734` ``` apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le) ``` lp15@63078 ` 1735` ``` done ``` lp15@63078 ` 1736` ```qed ``` lp15@63078 ` 1737` lp15@63078 ` 1738` ```proposition rel_interior_polyhedron_explicit: ``` lp15@63078 ` 1739` ``` assumes "finite F" ``` lp15@63078 ` 1740` ``` and seq: "S = affine hull S \ \F" ``` lp15@63078 ` 1741` ``` and faceq: "\h. h \ F \ a h \ 0 \ h = {x. a h \ x \ b h}" ``` lp15@63078 ` 1742` ``` and psub: "\F'. F' \ F \ S \ affine hull S \ \F'" ``` lp15@63078 ` 1743` ``` shows "rel_interior S = {x \ S. \h \ F. a h \ x < b h}" ``` lp15@63078 ` 1744` ```proof - ``` lp15@63078 ` 1745` ``` have rels: "\x. x \ rel_interior S \ x \ S" ``` lp15@63078 ` 1746` ``` by (meson IntE mem_rel_interior) ``` lp15@63078 ` 1747` ``` moreover have "a i \ x < b i" if x: "x \ rel_interior S" and "i \ F" for x i ``` lp15@63078 ` 1748` ``` proof - ``` lp15@63078 ` 1749` ``` have fif: "F - {i} \ F" ``` lp15@63078 ` 1750` ``` using \i \ F\ Diff_insert_absorb Diff_subset set_insert psubsetI by blast ``` lp15@63078 ` 1751` ``` then have "S \ affine hull S \ \(F - {i})" ``` lp15@63078 ` 1752` ``` by (rule psub) ``` lp15@63078 ` 1753` ``` then obtain z where ssub: "S \ \(F - {i})" and zint: "z \ \(F - {i})" ``` lp15@63078 ` 1754` ``` and "z \ S" and zaff: "z \ affine hull S" ``` lp15@63078 ` 1755` ``` by auto ``` lp15@63078 ` 1756` ``` have "z \ x" ``` lp15@63078 ` 1757` ``` using \z \ S\ rels x by blast ``` lp15@63078 ` 1758` ``` have "z \ affine hull S \ \F" ``` lp15@63078 ` 1759` ``` using \z \ S\ seq by auto ``` lp15@63078 ` 1760` ``` then have aiz: "a i \ z > b i" ``` lp15@63078 ` 1761` ``` using faceq zint zaff by fastforce ``` lp15@63078 ` 1762` ``` obtain e where "e > 0" "x \ S" and e: "ball x e \ affine hull S \ S" ``` lp15@63078 ` 1763` ``` using x by (auto simp: mem_rel_interior_ball) ``` lp15@63078 ` 1764` ``` then have ins: "\y. \norm (x - y) < e; y \ affine hull S\ \ y \ S" ``` lp15@63078 ` 1765` ``` by (metis IntI subsetD dist_norm mem_ball) ``` wenzelm@63148 ` 1766` ``` define \ where "\ = min (1/2) (e / 2 / norm(z - x))" ``` lp15@63078 ` 1767` ``` have "norm (\ *\<^sub>R x - \ *\<^sub>R z) = norm (\ *\<^sub>R (x - z))" ``` lp15@63078 ` 1768` ``` by (simp add: \_def algebra_simps norm_mult) ``` lp15@63078 ` 1769` ``` also have "... = \ * norm (x - z)" ``` lp15@63078 ` 1770` ``` using \e > 0\ by (simp add: \_def) ``` lp15@63078 ` 1771` ``` also have "... < e" ``` lp15@63078 ` 1772` ``` using \z \ x\ \e > 0\ by (simp add: \_def min_def divide_simps norm_minus_commute) ``` lp15@63078 ` 1773` ``` finally have lte: "norm (\ *\<^sub>R x - \ *\<^sub>R z) < e" . ``` lp15@63078 ` 1774` ``` have \_aff: "\ *\<^sub>R z + (1 - \) *\<^sub>R x \ affine hull S" ``` lp15@63078 ` 1775` ``` by (metis \x \ S\ add.commute affine_affine_hull diff_add_cancel hull_inc mem_affine zaff) ``` lp15@63078 ` 1776` ``` have "\ *\<^sub>R z + (1 - \) *\<^sub>R x \ S" ``` lp15@63078 ` 1777` ``` apply (rule ins [OF _ \_aff]) ``` lp15@63078 ` 1778` ``` apply (simp add: algebra_simps lte) ``` lp15@63078 ` 1779` ``` done ``` lp15@63078 ` 1780` ``` then obtain l where l: "0 < l" "l < 1" and ls: "(l *\<^sub>R z + (1 - l) *\<^sub>R x) \ S" ``` lp15@63078 ` 1781` ``` apply (rule_tac l = \ in that) ``` lp15@63078 ` 1782` ``` using \e > 0\ \z \ x\ apply (auto simp: \_def) ``` lp15@63078 ` 1783` ``` done ``` lp15@63078 ` 1784` ``` then have i: "l *\<^sub>R z + (1 - l) *\<^sub>R x \ i" ``` lp15@63078 ` 1785` ``` using seq \i \ F\ by auto ``` lp15@63078 ` 1786` ``` have "b i * l + (a i \ x) * (1 - l) < a i \ (l *\<^sub>R z + (1 - l) *\<^sub>R x)" ``` lp15@63078 ` 1787` ``` using l by (simp add: algebra_simps aiz) ``` lp15@63078 ` 1788` ``` also have "\ \ b i" using i l ``` lp15@63078 ` 1789` ``` using faceq mem_Collect_eq \i \ F\ by blast ``` lp15@63078 ` 1790` ``` finally have "(a i \ x) * (1 - l) < b i * (1 - l)" ``` lp15@63078 ` 1791` ``` by (simp add: algebra_simps) ``` lp15@63078 ` 1792` ``` with l show ?thesis ``` lp15@63078 ` 1793` ``` by simp ``` lp15@63078 ` 1794` ``` qed ``` lp15@63078 ` 1795` ``` moreover have "x \ rel_interior S" ``` lp15@63078 ` 1796` ``` if "x \ S" and less: "\h. h \ F \ a h \ x < b h" for x ``` lp15@63078 ` 1797` ``` proof - ``` lp15@63078 ` 1798` ``` have 1: "\h. h \ F \ x \ interior h" ``` lp15@63078 ` 1799` ``` by (metis interior_halfspace_le mem_Collect_eq less faceq) ``` lp15@63078 ` 1800` ``` have 2: "\y. \\h\F. y \ interior h; y \ affine hull S\ \ y \ S" ``` lp15@63078 ` 1801` ``` by (metis IntI Inter_iff contra_subsetD interior_subset seq) ``` lp15@63078 ` 1802` ``` show ?thesis ``` lp15@63078 ` 1803` ``` apply (simp add: rel_interior \x \ S\) ``` lp15@63078 ` 1804` ``` apply (rule_tac x="\h\F. interior h" in exI) ``` lp15@63078 ` 1805` ``` apply (auto simp: \finite F\ open_INT 1 2) ``` lp15@63078 ` 1806` ``` done ``` lp15@63078 ` 1807` ``` qed ``` lp15@63078 ` 1808` ``` ultimately show ?thesis by blast ``` lp15@63078 ` 1809` ```qed ``` lp15@63078 ` 1810` lp15@63078 ` 1811` lp15@63078 ` 1812` ```lemma polyhedron_Int_affine_parallel: ``` lp15@63078 ` 1813` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@63078 ` 1814` ``` shows "polyhedron S \ ``` lp15@63078 ` 1815` ``` (\F. finite F \ ``` lp15@63078 ` 1816` ``` S = (affine hull S) \ (\F) \ ``` lp15@63078 ` 1817` ``` (\h \ F. \a b. a \ 0 \ h = {x. a \ x \ b} \ ``` lp15@63078 ` 1818` ``` (\x \ affine hull S. (x + a) \ affine hull S)))" ``` lp15@63078 ` 1819` ``` (is "?lhs = ?rhs") ``` lp15@63078 ` 1820` ```proof ``` lp15@63078 ` 1821` ``` assume ?lhs ``` lp15@63078 ` 1822` ``` then obtain F where "finite F" and seq: "S = (affine hull S) \ \F" ``` lp15@63078 ` 1823` ``` and faces: "\h. h \ F \ \a b. a \ 0 \ h = {x. a \ x \ b}" ``` lp15@63078 ` 1824` ``` by (fastforce simp add: polyhedron_Int_affine) ``` lp15@63078 ` 1825` ``` then obtain a b where ab: "\h. h \ F \ a h \ 0 \ h = {x. a h \ x \ b h}" ``` lp15@63078 ` 1826` ``` by metis ``` lp15@63078 ` 1827` ``` show ?rhs ``` lp15@63078 ` 1828` ``` proof - ``` lp15@63078 ` 1829` ``` have "\a' b'. a' \ 0 \ ``` lp15@63078 ` 1830` ``` affine hull S \ {x. a' \ x \ b'} = affine hull S \ h \ ``` lp15@63078 ` 1831` ``` (\w \ affine hull S. (w + a') \ affine hull S)" ``` lp15@63078 ` 1832` ``` if "h \ F" "~(affine hull S \ h)" for h ``` lp15@63078 ` 1833` ``` proof - ``` lp15@63078 ` 1834` ``` have "a h \ 0" and "h = {x. a h \ x \ b h}" "h \ \F = \F" ``` lp15@63078 ` 1835` ``` using \h \ F\ ab by auto ``` lp15@63078 ` 1836` ``` then have "(affine hull S) \ {x. a h \ x \ b h} \ {}" ``` lp15@63078 ` 1837` ``` by (metis (no_types) affine_hull_eq_empty inf.absorb_iff2 inf_assoc inf_bot_right inf_commute seq that(2)) ``` lp15@63078 ` 1838` ``` moreover have "~ (affine hull S \ {x. a h \ x \ b h})" ``` lp15@63078 ` 1839` ``` using \h = {x. a h \ x \ b h}\ that(2) by blast ``` lp15@63078 ` 1840` ``` ultimately show ?thesis ``` lp15@63078 ` 1841` ``` using affine_parallel_slice [of "affine hull S"] ``` lp15@63078 ` 1842` ``` by (metis \h = {x. a h \ x \ b h}\ affine_affine_hull) ``` lp15@63078 ` 1843` ``` qed ``` lp15@63078 ` 1844` ``` then obtain a b ``` lp15@63078 ` 1845` ``` where ab: "\h. \h \ F; ~ (affine hull S \ h)\ ``` lp15@63078 ` 1846` ``` \ a h \ 0 \ ``` lp15@63078 ` 1847` ``` affine hull S \ {x. a h \ x \ b h} = affine hull S \ h \ ``` lp15@63078 ` 1848` ``` (\w \ affine hull S. (w + a h) \ affine hull S)" ``` lp15@63078 ` 1849` ``` by metis ``` lp15@63078 ` 1850` ``` have seq2: "S = affine hull S \ (\h\{h \ F. \ affine hull S \ h}. {x. a h \ x \ b h})" ``` lp15@63078 ` 1851` ``` by (subst seq) (auto simp: ab INT_extend_simps) ``` lp15@63078 ` 1852` ``` show ?thesis ``` lp15@63078 ` 1853` ``` apply (rule_tac x="(\h. {x. a h \ x \ b h}) ` {h. h \ F \ ~(affine hull S \ h)}" in exI) ``` lp15@63078 ` 1854` ``` apply (intro conjI seq2) ``` lp15@63078 ` 1855` ``` using \finite F\ apply force ``` lp15@63078 ` 1856` ``` using ab apply blast ``` lp15@63078 ` 1857` ``` done ``` lp15@63078 ` 1858` ``` qed ``` lp15@63078 ` 1859` ```next ``` lp15@63078 ` 1860` ``` assume ?rhs then show ?lhs ``` lp15@63078 ` 1861` ``` apply (simp add: polyhedron_Int_affine) ``` lp15@63078 ` 1862` ``` by metis ``` lp15@63078 ` 1863` ```qed ``` lp15@63078 ` 1864` lp15@63078 ` 1865` lp15@63078 ` 1866` ```proposition polyhedron_Int_affine_parallel_minimal: ``` lp15@63078 ` 1867` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@63078 ` 1868` ``` shows "polyhedron S \ ``` lp15@63078 ` 1869` ``` (\F. finite F \ ``` lp15@63078 ` 1870` ``` S = (affine hull S) \ (\F) \ ``` lp15@63078 ` 1871` ``` (\h \ F. \a b. a \ 0 \ h = {x. a \ x \ b} \ ``` lp15@63078 ` 1872` ``` (\x \ affine hull S. (x + a) \ affine hull S)) \ ``` lp15@63078 ` 1873` ``` (\F'. F' \ F \ S \ (affine hull S) \ (\F')))" ``` lp15@63078 ` 1874` ``` (is "?lhs = ?rhs") ``` lp15@63078 ` 1875` ```proof ``` lp15@63078 ` 1876` ``` assume ?lhs ``` lp15@63078 ` 1877` ``` then obtain f0 ``` lp15@63078 ` 1878` ``` where f0: "finite f0" ``` lp15@63078 ` 1879` ``` "S = (affine hull S) \ (\f0)" ``` lp15@63078 ` 1880` ``` (is "?P f0") ``` lp15@63078 ` 1881` ``` "\h \ f0. \a b. a \ 0 \ h = {x. a \ x \ b} \ ``` lp15@63078 ` 1882` ``` (\x \ affine hull S. (x + a) \ affine hull S)" ``` lp15@63078 ` 1883` ``` (is "?Q f0") ``` lp15@63078 ` 1884` ``` by (force simp: polyhedron_Int_affine_parallel) ``` wenzelm@63148 ` 1885` ``` define n where "n = (LEAST n. \F. card F = n \ finite F \ ?P F \ ?Q F)" ``` lp15@63078 ` 1886` ``` have nf: "\F. card F = n \ finite F \ ?P F \ ?Q F" ``` lp15@63078 ` 1887` ``` apply (simp add: n_def) ``` lp15@63078 ` 1888` ``` apply (rule LeastI [where k = "card f0"]) ``` lp15@63078 ` 1889` ``` using f0 apply auto ``` lp15@63078 ` 1890` ``` done ``` lp15@63078 ` 1891` ``` then obtain F where F: "card F = n" "finite F" and seq: "?P F" and aff: "?Q F" ``` lp15@63078 ` 1892` ``` by blast ``` lp15@63078 ` 1893` ``` then have "~ (finite g \ ?P g \ ?Q g)" if "card g < n" for g ``` lp15@63078 ` 1894` ``` using that by (auto simp: n_def dest!: not_less_Least) ``` lp15@63078 ` 1895` ``` then have *: "~ (?P g \ ?Q g)" if "g \ F" for g ``` lp15@63078 ` 1896` ``` using that \finite F\ psubset_card_mono \card F = n\ ``` lp15@63078 ` 1897` ``` by (metis finite_Int inf.strict_order_iff) ``` lp15@63078 ` 1898` ``` have 1: "\F'. F' \ F \ S \ affine hull S \ \F'" ``` lp15@63078 ` 1899` ``` by (subst seq) blast ``` lp15@63078 ` 1900` ``` have 2: "\F'. F' \ F \ S \ affine hull S \ \F'" ``` lp15@63078 ` 1901` ``` apply (frule *) ``` lp15@63078 ` 1902` ``` by (metis aff subsetCE subset_iff_psubset_eq) ``` lp15@63078 ` 1903` ``` show ?rhs ``` lp15@63078 ` 1904` ``` by (metis \finite F\ seq aff psubsetI 1 2) ``` lp15@63078 ` 1905` ```next ``` lp15@63078 ` 1906` ``` assume ?rhs then show ?lhs ``` lp15@63078 ` 1907` ``` by (auto simp: polyhedron_Int_affine_parallel) ``` lp15@63078 ` 1908` ```qed ``` lp15@63078 ` 1909` lp15@63078 ` 1910` lp15@63078 ` 1911` ```lemma polyhedron_Int_affine_minimal: ``` lp15@63078 ` 1912` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@63078 ` 1913` ``` shows "polyhedron S \ ``` lp15@63078 ` 1914` ``` (\F. finite F \ S = (affine hull S) \ \F \ ``` lp15@63078 ` 1915` ``` (\h \ F. \a b. a \ 0 \ h = {x. a \ x \ b}) \ ``` lp15@63078 ` 1916` ``` (\F'. F' \ F \ S \ (affine hull S) \ \F'))" ``` lp15@63078 ` 1917` ```apply (rule iffI) ``` lp15@63078 ` 1918` ``` apply (force simp: polyhedron_Int_affine_parallel_minimal elim!: ex_forward) ``` lp15@63078 ` 1919` ```apply (auto simp: polyhedron_Int_affine elim!: ex_forward) ``` lp15@63078 ` 1920` ```done ``` lp15@63078 ` 1921` lp15@63078 ` 1922` ```proposition facet_of_polyhedron_explicit: ``` lp15@63078 ` 1923` ``` assumes "finite F" ``` lp15@63078 ` 1924` ``` and seq: "S = affine hull S \ \F" ``` lp15@63078 ` 1925` ``` and faceq: "\h. h \ F \ a h \ 0 \ h = {x. a h \ x \ b h}" ``` lp15@63078 ` 1926` ``` and psub: "\F'. F' \ F \ S \ affine hull S \ \F'" ``` lp15@63078 ` 1927` ``` shows "c facet_of S \ (\h. h \ F \ c = S \ {x. a h \ x = b h})" ``` lp15@63078 ` 1928` ```proof (cases "S = {}") ``` lp15@63078 ` 1929` ``` case True with psub show ?thesis by force ``` lp15@63078 ` 1930` ```next ``` lp15@63078 ` 1931` ``` case False ``` lp15@63078 ` 1932` ``` have "polyhedron S" ``` lp15@63078 ` 1933` ``` apply (simp add: polyhedron_Int_affine) ``` lp15@63078 ` 1934` ``` apply (rule_tac x=F in exI) ``` lp15@63078 ` 1935` ``` using assms apply force ``` lp15@63078 ` 1936` ``` done ``` lp15@63078 ` 1937` ``` then have "convex S" ``` lp15@63078 ` 1938` ``` by (rule polyhedron_imp_convex) ``` lp15@63078 ` 1939` ``` with False rel_interior_eq_empty have "rel_interior S \ {}" by blast ``` lp15@63078 ` 1940` ``` then obtain x where "x \ rel_interior S" by auto ``` lp15@63078 ` 1941` ``` then obtain T where "open T" "x \ T" "x \ S" "T \ affine hull S \ S" ``` lp15@63078 ` 1942` ``` by (force simp: mem_rel_interior) ``` lp15@63078 ` 1943` ``` then have xaff: "x \ affine hull S" and xint: "x \ \F" ``` lp15@63078 ` 1944` ``` using seq hull_inc by auto ``` lp15@63078 ` 1945` ``` have "rel_interior S = {x \ S. \h\F. a h \ x < b h}" ``` lp15@63078 ` 1946` ``` by (rule rel_interior_polyhedron_explicit [OF \finite F\ seq faceq psub]) ``` lp15@63078 ` 1947` ``` with \x \ rel_interior S\ ``` lp15@63078 ` 1948` ``` have [simp]: "\h. h\F \ a h \ x < b h" by blast ``` lp15@63078 ` 1949` ``` have *: "(S \ {x. a h \ x = b h}) facet_of S" if "h \ F" for h ``` lp15@63078 ` 1950` ``` proof - ``` lp15@63078 ` 1951` ``` have "S \ affine hull S \ \(F - {h})" ``` lp15@63078 ` 1952` ``` using psub that by (metis Diff_disjoint Diff_subset insert_disjoint(2) psubsetI) ``` lp15@63078 ` 1953` ``` then obtain z where zaff: "z \ affine hull S" and zint: "z \ \(F - {h})" and "z \ S" ``` lp15@63078 ` 1954` ``` by force ``` lp15@63078 ` 1955` ``` then have "z \ x" "z \ h" using seq \x \ S\ by auto ``` lp15@63078 ` 1956` ``` have "x \ h" using that xint by auto ``` lp15@63078 ` 1957` ``` then have able: "a h \ x \ b h" ``` lp15@63078 ` 1958` ``` using faceq that by blast ``` lp15@63078 ` 1959` ``` also have "... < a h \ z" using \z \ h\ faceq [OF that] xint by auto ``` lp15@63078 ` 1960` ``` finally have xltz: "a h \ x < a h \ z" . ``` wenzelm@63148 ` 1961` ``` define l where "l = (b h - a h \ x) / (a h \ z - a h \ x)" ``` wenzelm@63148 ` 1962` ``` define w where "w = (1 - l) *\<^sub>R x + l *\<^sub>R z" ``` lp15@63078 ` 1963` ``` have "0 < l" "l < 1" ``` lp15@63078 ` 1964` ``` using able xltz \b h < a h \ z\ \h \ F\ ``` lp15@63078 ` 1965` ``` by (auto simp: l_def divide_simps) ``` lp15@63078 ` 1966` ``` have awlt: "a i \ w < b i" if "i \ F" "i \ h" for i ``` lp15@63078 ` 1967` ``` proof - ``` lp15@63078 ` 1968` ``` have "(1 - l) * (a i \ x) < (1 - l) * b i" ``` lp15@63078 ` 1969` ``` by (simp add: \l < 1\ \i \ F\) ``` lp15@63078 ` 1970` ``` moreover have "l * (a i \ z) \ l * b i" ``` lp15@63078 ` 1971` ``` apply (rule mult_left_mono) ``` lp15@63078 ` 1972` ``` apply (metis Diff_insert_absorb Inter_iff Set.set_insert \h \ F\ faceq insertE mem_Collect_eq that zint) ``` lp15@63078 ` 1973` ``` using \0 < l\ ``` lp15@63078 ` 1974` ``` apply simp ``` lp15@63078 ` 1975` ``` done ``` lp15@63078 ` 1976` ``` ultimately show ?thesis by (simp add: w_def algebra_simps) ``` lp15@63078 ` 1977` ``` qed ``` lp15@63078 ` 1978` ``` have weq: "a h \ w = b h" ``` lp15@63078 ` 1979` ``` using xltz unfolding w_def l_def ``` lp15@63078 ` 1980` ``` by (simp add: algebra_simps) (simp add: field_simps) ``` lp15@63078 ` 1981` ``` have "w \ affine hull S" ``` lp15@63078 ` 1982` ``` by (simp add: w_def mem_affine xaff zaff) ``` lp15@63078 ` 1983` ``` moreover have "w \ \F" ``` lp15@63078 ` 1984` ``` using \a h \ w = b h\ awlt faceq less_eq_real_def by blast ``` lp15@63078 ` 1985` ``` ultimately have "w \ S" ``` lp15@63078 ` 1986` ``` using seq by blast ``` lp15@63078 ` 1987` ``` with weq have "S \ {x. a h \ x = b h} \ {}" by blast ``` lp15@63078 ` 1988` ``` moreover have "S \ {x. a h \ x = b h} face_of S" ``` lp15@63078 ` 1989` ``` apply (rule face_of_Int_supporting_hyperplane_le) ``` lp15@63078 ` 1990` ``` apply (rule \convex S\) ``` lp15@63078 ` 1991` ``` apply (subst (asm) seq) ``` lp15@63078 ` 1992` ``` using faceq that apply fastforce ``` lp15@63078 ` 1993` ``` done ``` lp15@63078 ` 1994` ``` moreover have "affine hull (S \ {x. a h \ x = b h}) = ``` lp15@63078 ` 1995` ``` (affine hull S) \ {x. a h \ x = b h}" ``` lp15@63078 ` 1996` ``` proof ``` lp15@63078 ` 1997` ``` show "affine hull (S \ {x. a h \ x = b h}) \ affine hull S \ {x. a h \ x = b h}" ``` lp15@63078 ` 1998` ``` apply (intro Int_greatest hull_mono Int_lower1) ``` lp15@63078 ` 1999` ``` apply (metis affine_hull_eq affine_hyperplane hull_mono inf_le2) ``` lp15@63078 ` 2000` ``` done ``` lp15@63078 ` 2001` ``` next ``` lp15@63078 ` 2002` ``` show "affine hull S \ {x. a h \ x = b h} \ affine hull (S \ {x. a h \ x = b h})" ``` lp15@63078 ` 2003` ``` proof ``` lp15@63078 ` 2004` ``` fix y ``` lp15@63078 ` 2005` ``` assume yaff: "y \ affine hull S \ {y. a h \ y = b h}" ``` lp15@63078 ` 2006` ``` obtain T where "0 < T" ``` lp15@63078 ` 2007` ``` and T: "\j. \j \ F; j \ h\ \ T * (a j \ y - a j \ w) \ b j - a j \ w" ``` lp15@63078 ` 2008` ``` proof (cases "F - {h} = {}") ``` lp15@63078 ` 2009` ``` case True then show ?thesis ``` lp15@63078 ` 2010` ``` by (rule_tac T=1 in that) auto ``` lp15@63078 ` 2011` ``` next ``` lp15@63078 ` 2012` ``` case False ``` lp15@63078 ` 2013` ``` then obtain h' where h': "h' \ F - {h}" by auto ``` wenzelm@63148 ` 2014` ``` define inff where "inff = ``` wenzelm@63148 ` 2015` ``` (INF j:F - {h}. ``` wenzelm@63148 ` 2016` ``` if 0 < a j \ y - a j \ w ``` wenzelm@63148 ` 2017` ``` then (b j - a j \ w) / (a j \ y - a j \ w) ``` wenzelm@63148 ` 2018` ``` else 1)" ``` lp15@63078 ` 2019` ``` have "0 < inff" ``` lp15@63078 ` 2020` ``` apply (simp add: inff_def) ``` lp15@63078 ` 2021` ``` apply (rule finite_imp_less_Inf) ``` lp15@63078 ` 2022` ``` using \finite F\ apply blast ``` lp15@63078 ` 2023` ``` using h' apply blast ``` lp15@63078 ` 2024` ``` apply simp ``` lp15@63078 ` 2025` ``` using awlt apply (force simp: divide_simps) ``` lp15@63078 ` 2026` ``` done ``` lp15@63078 ` 2027` ``` moreover have "inff * (a j \ y - a j \ w) \ b j - a j \ w" ``` lp15@63078 ` 2028` ``` if "j \ F" "j \ h" for j ``` lp15@63078 ` 2029` ``` proof (cases "a j \ w < a j \ y") ``` lp15@63078 ` 2030` ``` case True ``` lp15@63078 ` 2031` ``` then have "inff \ (b j - a j \ w) / (a j \ y - a j \ w)" ``` lp15@63078 ` 2032` ``` apply (simp add: inff_def) ``` lp15@63078 ` 2033` ``` apply (rule cInf_le_finite) ``` lp15@63078 ` 2034` ``` using \finite F\ apply blast ``` lp15@63078 ` 2035` ``` apply (simp add: that split: if_split_asm) ``` lp15@63078 ` 2036` ``` done ``` lp15@63078 ` 2037` ``` then show ?thesis ``` lp15@63078 ` 2038` ``` using \0 < inff\ awlt [OF that] mult_strict_left_mono ``` lp15@63078 ` 2039` ``` by (fastforce simp add: algebra_simps divide_simps split: if_split_asm) ``` lp15@63078 ` 2040` ``` next ``` lp15@63078 ` 2041` ``` case False ``` lp15@63078 ` 2042` ``` with \0 < inff\ have "inff * (a j \ y - a j \ w) \ 0" ``` lp15@63078 ` 2043` ``` by (simp add: mult_le_0_iff) ``` lp15@63078 ` 2044` ``` also have "... < b j - a j \ w" ``` lp15@63078 ` 2045` ``` by (simp add: awlt that) ``` lp15@63078 ` 2046` ``` finally show ?thesis by simp ``` lp15@63078 ` 2047` ``` qed ``` lp15@63078 ` 2048` ``` ultimately show ?thesis ``` lp15@63078 ` 2049` ``` by (blast intro: that) ``` lp15@63078 ` 2050` ``` qed ``` wenzelm@63148 ` 2051` ``` define c where "c = (1 - T) *\<^sub>R w + T *\<^sub>R y" ``` lp15@63078 ` 2052` ``` have "(1 - T) *\<^sub>R w + T *\<^sub>R y \ j" if "j \ F" for j ``` lp15@63078 ` 2053` ``` proof (cases "j = h") ``` lp15@63078 ` 2054` ``` case True ``` lp15@63078 ` 2055` ``` have "(1 - T) *\<^sub>R w + T *\<^sub>R y \ {x. a h \ x \ b h}" ``` lp15@63078 ` 2056` ``` using weq yaff by (auto simp: algebra_simps) ``` lp15@63078 ` 2057` ``` with True faceq [OF that] show ?thesis by metis ``` lp15@63078 ` 2058` ``` next ``` lp15@63078 ` 2059` ``` case False ``` lp15@63078 ` 2060` ``` with T that have "(1 - T) *\<^sub>R w + T *\<^sub>R y \ {x. a j \ x \ b j}" ``` lp15@63078 ` 2061` ``` by (simp add: algebra_simps) ``` lp15@63078 ` 2062` ``` with faceq [OF that] show ?thesis by simp ``` lp15@63078 ` 2063` ``` qed ``` lp15@63078 ` 2064` ``` moreover have "(1 - T) *\<^sub>R w + T *\<^sub>R y \ affine hull S" ``` wenzelm@63170 ` 2065` ``` apply (rule affine_affine_hull [simplified affine_alt, rule_format]) ``` lp15@63078 ` 2066` ``` apply (simp add: \w \ affine hull S\) ``` lp15@63078 ` 2067` ``` using yaff apply blast ``` lp15@63078 ` 2068` ``` done ``` lp15@63078 ` 2069` ``` ultimately have "c \ S" ``` lp15@63078 ` 2070` ``` using seq by (force simp: c_def) ``` lp15@63078 ` 2071` ``` moreover have "a h \ c = b h" ``` lp15@63078 ` 2072` ``` using yaff by (force simp: c_def algebra_simps weq) ``` lp15@63078 ` 2073` ``` ultimately have caff: "c \ affine hull (S \ {y. a h \ y = b h})" ``` lp15@63078 ` 2074` ``` by (simp add: hull_inc) ``` lp15@63078 ` 2075` ``` have waff: "w \ affine hull (S \ {y. a h \ y = b h})" ``` lp15@63078 ` 2076` ``` using \w \ S\ weq by (blast intro: hull_inc) ``` lp15@63078 ` 2077` ``` have yeq: "y = (1 - inverse T) *\<^sub>R w + c /\<^sub>R T" ``` lp15@63078 ` 2078` ``` using \0 < T\ by (simp add: c_def algebra_simps) ``` lp15@63078 ` 2079` ``` show "y \ affine hull (S \ {y. a h \ y = b h})" ``` wenzelm@63170 ` 2080` ``` by (metis yeq affine_affine_hull [simplified affine_alt, rule_format, OF waff caff]) ``` lp15@63078 ` 2081` ``` qed ``` lp15@63078 ` 2082` ``` qed ``` lp15@63078 ` 2083` ``` ultimately show ?thesis ``` lp15@63078 ` 2084` ``` apply (simp add: facet_of_def) ``` lp15@63078 ` 2085` ``` apply (subst aff_dim_affine_hull [symmetric]) ``` lp15@63078 ` 2086` ``` using \b h < a h \ z\ zaff ``` lp15@63078 ` 2087` ``` apply (force simp: aff_dim_affine_Int_hyperplane) ``` lp15@63078 ` 2088` ``` done ``` lp15@63078 ` 2089` ``` qed ``` lp15@63078 ` 2090` ``` show ?thesis ``` lp15@63078 ` 2091` ``` proof ``` lp15@63078 ` 2092` ``` show "\h. h \ F \ c = S \ {x. a h \ x = b h} \ c facet_of S" ``` lp15@63078 ` 2093` ``` using * by blast ``` lp15@63078 ` 2094` ``` next ``` lp15@63078 ` 2095` ``` assume "c facet_of S" ``` lp15@63078 ` 2096` ``` then have "c face_of S" "convex c" "c \ {}" and affc: "aff_dim c = aff_dim S - 1" ``` lp15@63078 ` 2097` ``` by (auto simp: facet_of_def face_of_imp_convex) ``` lp15@63078 ` 2098` ``` then obtain x where x: "x \ rel_interior c" ``` lp15@63078 ` 2099` ``` by (force simp: rel_interior_eq_empty) ``` lp15@63078 ` 2100` ``` then have "x \ c" ``` lp15@63078 ` 2101` ``` by (meson subsetD rel_interior_subset) ``` lp15@63078 ` 2102` ``` then have "x \ S" ``` lp15@63078 ` 2103` ``` using \c facet_of S\ facet_of_imp_subset by blast ``` lp15@63078 ` 2104` ``` have rels: "rel_interior S = {x \ S. \h\F. a h \ x < b h}" ``` lp15@63078 ` 2105` ``` by (rule rel_interior_polyhedron_explicit [OF assms]) ``` lp15@63078 ` 2106` ``` have "c \ S" ``` lp15@63078 ` 2107` ``` using \c facet_of S\ facet_of_irrefl by blast ``` lp15@63078 ` 2108` ``` then have "x \ rel_interior S" ``` lp15@63078 ` 2109` ``` by (metis IntI empty_iff \x \ c\ \c \ S\ \c face_of S\ face_of_disjoint_rel_interior) ``` lp15@63078 ` 2110` ``` with rels \x \ S\ obtain i where "i \ F" and i: "a i \ x \ b i" ``` lp15@63078 ` 2111` ``` by force ``` lp15@63078 ` 2112` ``` have "x \ {u. a i \ u \ b i}" ``` lp15@63078 ` 2113` ``` by (metis IntD2 InterE \i \ F\ \x \ S\ faceq seq) ``` lp15@63078 ` 2114` ``` then have "a i \ x \ b i" by simp ``` lp15@63078 ` 2115` ``` then have "a i \ x = b i" using i by auto ``` lp15@63078 ` 2116` ``` have "c \ S \ {x. a i \ x = b i}" ``` lp15@63078 ` 2117` ``` apply (rule subset_of_face_of [of _ S]) ``` lp15@63078 ` 2118` ``` apply (simp add: "*" \i \ F\ facet_of_imp_face_of) ``` lp15@63078 ` 2119` ``` apply (simp add: \c face_of S\ face_of_imp_subset) ``` lp15@63078 ` 2120` ``` using \a i \ x = b i\ \x \ S\ x by blast ``` lp15@63078 ` 2121` ``` then have cface: "c face_of (S \ {x. a i \ x = b i})" ``` lp15@63078 ` 2122` ``` by (meson \c face_of S\ face_of_subset inf_le1) ``` lp15@63078 ` 2123` ``` have con: "convex (S \ {x. a i \ x = b i})" ``` lp15@63078 ` 2124` ``` by (simp add: \convex S\ convex_Int convex_hyperplane) ``` lp15@63078 ` 2125` ``` show "\h. h \ F \ c = S \ {x. a h \ x = b h}" ``` lp15@63078 ` 2126` ``` apply (rule_tac x=i in exI) ``` lp15@63078 ` 2127` ``` apply (simp add: \i \ F\) ``` lp15@63078 ` 2128` ``` by (metis (no_types) * \i \ F\ affc facet_of_def less_irrefl face_of_aff_dim_lt [OF con cface]) ``` lp15@63078 ` 2129` ``` qed ``` lp15@63078 ` 2130` ```qed ``` lp15@63078 ` 2131` lp15@63078 ` 2132` lp15@63078 ` 2133` ```lemma face_of_polyhedron_subset_explicit: ``` lp15@63078 ` 2134` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@63078 ` 2135` ``` assumes "finite F" ``` lp15@63078 ` 2136` ``` and seq: "S = affine hull S \ \F" ``` lp15@63078 ` 2137` ``` and faceq: "\h. h \ F \ a h \ 0 \ h = {x. a h \ x \ b h}" ``` lp15@63078 ` 2138` ``` and psub: "\F'. F' \ F \ S \ affine hull S \ \F'" ``` lp15@63078 ` 2139` ``` and c: "c face_of S" and "c \ {}" "c \ S" ``` lp15@63078 ` 2140` ``` obtains h where "h \ F" "c \ S \ {x. a h \ x = b h}" ``` lp15@63078 ` 2141` ```proof - ``` lp15@63078 ` 2142` ``` have "c \ S" using \c face_of S\ ``` lp15@63078 ` 2143` ``` by (simp add: face_of_imp_subset) ``` lp15@63078 ` 2144` ``` have "polyhedron S" ``` lp15@63078 ` 2145` ``` apply (simp add: polyhedron_Int_affine) ``` lp15@63078 ` 2146` ``` by (metis \finite F\ faceq seq) ``` lp15@63078 ` 2147` ``` then have "convex S" ``` lp15@63078 ` 2148` ``` by (simp add: polyhedron_imp_convex) ``` lp15@63078 ` 2149` ``` then have *: "(S \ {x. a h \ x = b h}) face_of S" if "h \ F" for h ``` lp15@63078 ` 2150` ``` apply (rule face_of_Int_supporting_hyperplane_le) ``` lp15@63078 ` 2151` ``` using faceq seq that by fastforce ``` lp15@63078 ` 2152` ``` have "rel_interior c \ {}" ``` lp15@63078 ` 2153` ``` using c \c \ {}\ face_of_imp_convex rel_interior_eq_empty by blast ``` lp15@63078 ` 2154` ``` then obtain x where "x \ rel_interior c" by auto ``` lp15@63078 ` 2155` ``` have rels: "rel_interior S = {x \ S. \h\F. a h \ x < b h}" ``` lp15@63078 ` 2156` ``` by (rule rel_interior_polyhedron_explicit [OF \finite F\ seq faceq psub]) ``` lp15@63078 ` 2157` ``` then have xnot: "x \ rel_interior S" ``` lp15@63078 ` 2158` ``` by (metis IntI \x \ rel_interior c\ c \c \ S\ contra_subsetD empty_iff face_of_disjoint_rel_interior rel_interior_subset) ``` lp15@63078 ` 2159` ``` then have "x \ S" ``` lp15@63078 ` 2160` ``` using \c \ S\ \x \ rel_interior c\ rel_interior_subset by auto ``` lp15@63078 ` 2161` ``` then have xint: "x \ \F" ``` lp15@63078 ` 2162` ``` using seq by blast ``` lp15@63078 ` 2163` ``` have "F \ {}" using assms ``` lp15@63078 ` 2164` ``` by (metis affine_Int affine_Inter affine_affine_hull ex_in_conv face_of_affine_trivial) ``` lp15@63078 ` 2165` ``` then obtain i where "i \ F" "~ (a i \ x < b i)" ``` lp15@63078 ` 2166` ``` using \x \ S\ rels xnot by auto ``` lp15@63078 ` 2167` ``` with xint have "a i \ x = b i" ``` lp15@63078 ` 2168` ``` by (metis eq_iff mem_Collect_eq not_le Inter_iff faceq) ```