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