|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
World.vdmrt
Sprache: Isabelle
|
|
section \<open>Faces, Extreme Points, Polytopes, Polyhedra etc\<close>
text\<open>Ported from HOL Light by L C Paulson\<close>
theory Polytope
imports Cartesian_Euclidean_Space Path_Connected
begin
subsection \<open>Faces of a (usually convex) set\<close>
definition\<^marker>\<open>tag important\<close> face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
where
"T face_of S \
T \<subseteq> S \<and> convex T \<and>
(\<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)"
lemma face_ofD: "\T face_of S; x \ open_segment a b; a \ S; b \ S; x \ T\ \ a \ T \ b \ T"
unfolding face_of_def by blast
lemma face_of_translation_eq [simp]:
"((+) a ` T face_of (+) a ` S) \ T face_of S"
proof -
have *: "\a T S. T face_of S \ ((+) a ` T face_of (+) a ` S)"
by (simp add: face_of_def)
show ?thesis
by (force simp: image_comp o_def dest: * [where a = "-a"] intro: *)
qed
lemma face_of_linear_image:
assumes "linear f" "inj f"
shows "(f ` c face_of f ` S) \ c face_of S"
by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
lemma face_of_refl: "convex S \ S face_of S"
by (auto simp: face_of_def)
lemma face_of_refl_eq: "S face_of S \ convex S"
by (auto simp: face_of_def)
lemma empty_face_of [iff]: "{} face_of S"
by (simp add: face_of_def)
lemma face_of_empty [simp]: "S face_of {} \ S = {}"
by (meson empty_face_of face_of_def subset_empty)
lemma face_of_trans [trans]: "\S face_of T; T face_of u\ \ S face_of u"
unfolding face_of_def by (safe; blast)
lemma face_of_face: "T face_of S \ (f face_of T \ f face_of S \ f \ T)"
unfolding face_of_def by (safe; blast)
lemma face_of_subset: "\F face_of S; F \ T; T \ S\ \ F face_of T"
unfolding face_of_def by (safe; blast)
lemma face_of_slice: "\F face_of S; convex T\ \ (F \ T) face_of (S \ T)"
unfolding face_of_def by (blast intro: convex_Int)
lemma face_of_Int: "\t1 face_of S; t2 face_of S\ \ (t1 \ t2) face_of S"
unfolding face_of_def by (blast intro: convex_Int)
lemma face_of_Inter: "\A \ {}; \T. T \ A \ T face_of S\ \ (\ A) face_of S"
unfolding face_of_def by (blast intro: convex_Inter)
lemma face_of_Int_Int: "\F face_of T; F' face_of t'\ \ (F \ F') face_of (T \ t')"
unfolding face_of_def by (blast intro: convex_Int)
lemma face_of_imp_subset: "T face_of S \ T \ S"
unfolding face_of_def by blast
proposition face_of_imp_eq_affine_Int:
fixes S :: "'a::euclidean_space set"
assumes S: "convex S" and T: "T face_of S"
shows "T = (affine hull T) \ S"
proof -
have "convex T" using T by (simp add: face_of_def)
have *: False if x: "x \ affine hull T" and "x \ S" "x \ T" and y: "y \ rel_interior T" for x y
proof -
obtain e where "e>0" and e: "cball y e \ affine hull T \ T"
using y by (auto simp: rel_interior_cball)
have "y \ x" "y \ S" "y \ T"
using face_of_imp_subset rel_interior_subset T that by blast+
then have zne: "\u. \u \ {0<..<1}; (1 - u) *\<^sub>R y + u *\<^sub>R x \ T\ \ False"
using \<open>x \<in> S\<close> \<open>x \<notin> T\<close> \<open>T face_of S\<close> unfolding face_of_def
by (meson greaterThanLessThan_iff in_segment(2))
have in01: "min (1/2) (e / norm (x - y)) \ {0<..<1}"
using \<open>y \<noteq> x\<close> \<open>e > 0\<close> by simp
have \<section>: "norm (min (1/2) (e / norm (x - y)) *\<^sub>R y - min (1/2) (e / norm (x - y)) *\<^sub>R x) \<le> e"
using \<open>e > 0\<close>
by (simp add: scaleR_diff_right [symmetric] norm_minus_commute min_mult_distrib_right)
show False
apply (rule zne [OF in01 e [THEN subsetD]])
using \<open>y \<in> T\<close>
apply (simp add: hull_inc mem_affine x)
by (simp add: dist_norm algebra_simps \<section>)
qed
show ?thesis
proof (rule subset_antisym)
show "T \ affine hull T \ S"
using assms by (simp add: hull_subset face_of_imp_subset)
show "affine hull T \ S \ T"
using "*" \<open>convex T\<close> rel_interior_eq_empty by fastforce
qed
qed
lemma face_of_imp_closed:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "closed S" "T face_of S" shows "closed T"
by (metis affine_affine_hull affine_closed closed_Int face_of_imp_eq_affine_Int assms)
lemma face_of_Int_supporting_hyperplane_le_strong:
assumes "convex(S \ {x. a \ x = b})" and aleb: "\x. x \ S \ a \ x \ b"
shows "(S \ {x. a \ x = b}) face_of S"
proof -
have *: "a \ u = a \ x" if "x \ open_segment u v" "u \ S" "v \ S" and b: "b = a \ x"
for u v x
proof (rule antisym)
show "a \ u \ a \ x"
using aleb \<open>u \<in> S\<close> \<open>b = a \<bullet> x\<close> by blast
next
obtain \<xi> where "b = a \<bullet> ((1 - \<xi>) *\<^sub>R u + \<xi> *\<^sub>R v)" "0 < \<xi>" "\<xi> < 1"
using \<open>b = a \<bullet> x\<close> \<open>x \<in> open_segment u v\<close> in_segment
by (auto simp: open_segment_image_interval split: if_split_asm)
then have "b + \ * (a \ u) \ a \ u + \ * b"
using aleb [OF \<open>v \<in> S\<close>] by (simp add: algebra_simps)
then have "(1 - \) * b \ (1 - \) * (a \ u)"
by (simp add: algebra_simps)
then have "b \ a \ u"
using \<open>\<xi> < 1\<close> by auto
with b show "a \ x \ a \ u" by simp
qed
show ?thesis
using "*" open_segment_commute by (fastforce simp add: face_of_def assms)
qed
lemma face_of_Int_supporting_hyperplane_ge_strong:
"\convex(S \ {x. a \ x = b}); \x. x \ S \ a \ x \ b\
\<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
using face_of_Int_supporting_hyperplane_le_strong [of S "-a" "-b"] by simp
lemma face_of_Int_supporting_hyperplane_le:
"\convex S; \x. x \ S \ a \ x \ b\ \ (S \ {x. a \ x = b}) face_of S"
by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_le_strong)
lemma face_of_Int_supporting_hyperplane_ge:
"\convex S; \x. x \ S \ a \ x \ b\ \ (S \ {x. a \ x = b}) face_of S"
by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_ge_strong)
lemma face_of_imp_convex: "T face_of S \ convex T"
using face_of_def by blast
lemma face_of_imp_compact:
fixes S :: "'a::euclidean_space set"
shows "\convex S; compact S; T face_of S\ \ compact T"
by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset)
lemma face_of_Int_subface:
"\A \ B face_of A; A \ B face_of B; C face_of A; D face_of B\
\<Longrightarrow> (C \<inter> D) face_of C \<and> (C \<inter> D) face_of D"
by (meson face_of_Int_Int face_of_face inf_le1 inf_le2)
lemma subset_of_face_of:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "u \ S" "T \ (rel_interior u) \ {}"
shows "u \ T"
proof
fix c
assume "c \ u"
obtain b where "b \ T" "b \ rel_interior u" using assms by auto
then obtain e where "e>0" "b \ u" and e: "cball b e \ affine hull u \ u"
by (auto simp: rel_interior_cball)
show "c \ T"
proof (cases "b=c")
case True with \<open>b \<in> T\<close> show ?thesis by blast
next
case False
define d where "d = b + (e / norm(b - c)) *\<^sub>R (b - c)"
have "d \ cball b e \ affine hull u"
using \<open>e > 0\<close> \<open>b \<in> u\<close> \<open>c \<in> u\<close>
by (simp add: d_def dist_norm hull_inc mem_affine_3_minus False)
with e have "d \ u" by blast
have nbc: "norm (b - c) + e > 0" using \<open>e > 0\<close>
by (metis add.commute le_less_trans less_add_same_cancel2 norm_ge_zero)
then have [simp]: "d \ c" using False scaleR_cancel_left [of "1 + (e / norm (b - c))" b c]
by (simp add: algebra_simps d_def) (simp add: field_split_simps)
have [simp]: "((e - e * e / (e + norm (b - c))) / norm (b - c)) = (e / (e + norm (b - c)))"
using False nbc
by (simp add: divide_simps) (simp add: algebra_simps)
have "b \ open_segment d c"
apply (simp add: open_segment_image_interval)
apply (simp add: d_def algebra_simps image_def)
apply (rule_tac x="e / (e + norm (b - c))" in bexI)
using False nbc \<open>0 < e\<close> by (auto simp: algebra_simps)
then have "d \ T \ c \ T"
by (meson \<open>b \<in> T\<close> \<open>c \<in> u\<close> \<open>d \<in> u\<close> assms face_ofD subset_iff)
then show ?thesis ..
qed
qed
lemma face_of_eq:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "U face_of S" "(rel_interior T) \ (rel_interior U) \ {}"
shows "T = U"
using assms
unfolding disjoint_iff_not_equal
by (metis IntI empty_iff face_of_imp_subset mem_rel_interior_ball subset_antisym subset_of_face_of)
lemma face_of_disjoint_rel_interior:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "T \ S"
shows "T \ rel_interior S = {}"
by (meson assms subset_of_face_of face_of_imp_subset order_refl subset_antisym)
lemma face_of_disjoint_interior:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "T \ S"
shows "T \ interior S = {}"
proof -
have "T \ interior S \ rel_interior S"
by (meson inf_sup_ord(2) interior_subset_rel_interior order.trans)
thus ?thesis
by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty)
qed
lemma face_of_subset_rel_boundary:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "T \ S"
shows "T \ (S - rel_interior S)"
by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI)
lemma face_of_subset_rel_frontier:
fixes S :: "'a::real_normed_vector set"
assumes "T face_of S" "T \ S"
shows "T \ rel_frontier S"
using assms closure_subset face_of_disjoint_rel_interior face_of_imp_subset rel_frontier_def by fastforce
lemma face_of_aff_dim_lt:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "T face_of S" "T \ S"
shows "aff_dim T < aff_dim S"
proof -
have "aff_dim T \ aff_dim S"
by (simp add: face_of_imp_subset aff_dim_subset assms)
moreover have "aff_dim T \ aff_dim S"
proof (cases "T = {}")
case True then show ?thesis
by (metis aff_dim_empty \<open>T \<noteq> S\<close>)
next case False then show ?thesis
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)
qed
ultimately show ?thesis
by simp
qed
lemma subset_of_face_of_affine_hull:
fixes S :: "'a::euclidean_space set"
assumes T: "T face_of S" and "convex S" "U \ S" and dis: "\ disjnt (affine hull T) (rel_interior U)"
shows "U \ T"
proof (rule subset_of_face_of [OF T \<open>U \<subseteq> S\<close>])
show "T \ rel_interior U \ {}"
using face_of_imp_eq_affine_Int [OF \<open>convex S\<close> T] rel_interior_subset [of U] dis \<open>U \<subseteq> S\<close> disjnt_def
by fastforce
qed
lemma affine_hull_face_of_disjoint_rel_interior:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "F face_of S" "F \ S"
shows "affine hull F \ rel_interior S = {}"
by (metis assms disjnt_def face_of_imp_subset order_refl subset_antisym subset_of_face_of_affine_hull)
lemma affine_diff_divide:
assumes "affine S" "k \ 0" "k \ 1" and xy: "x \ S" "y /\<^sub>R (1 - k) \ S"
shows "(x - y) /\<^sub>R k \ S"
proof -
have "inverse(k) *\<^sub>R (x - y) = (1 - inverse k) *\<^sub>R inverse(1 - k) *\<^sub>R y + inverse(k) *\<^sub>R x"
using assms
by (simp add: algebra_simps) (simp add: scaleR_left_distrib [symmetric] field_split_simps)
then show ?thesis
using \<open>affine S\<close> xy by (auto simp: affine_alt)
qed
proposition face_of_convex_hulls:
assumes S: "finite S" "T \ S" and disj: "affine hull T \ convex hull (S - T) = {}"
shows "(convex hull T) face_of (convex hull S)"
proof -
have fin: "finite T" "finite (S - T)" using assms
by (auto simp: finite_subset)
have *: "x \ convex hull T"
if x: "x \ convex hull S" and y: "y \ convex hull S" and w: "w \ convex hull T" "w \ open_segment x y"
for x y w
proof -
have waff: "w \ affine hull T"
using convex_hull_subset_affine_hull w by blast
obtain a b where a: "\i. i \ S \ 0 \ a i" and asum: "sum a S = 1" and aeqx: "(\i\S. a i *\<^sub>R i) = x"
and b: "\i. i \ S \ 0 \ b i" and bsum: "sum b S = 1" and beqy: "(\i\S. b i *\<^sub>R i) = y"
using x y by (auto simp: assms convex_hull_finite)
obtain u where "(1 - u) *\<^sub>R x + u *\<^sub>R y \ convex hull T" "x \ y" and weq: "w = (1 - u) *\<^sub>R x + u *\<^sub>R y"
and u01: "0 < u" "u < 1"
using w by (auto simp: open_segment_image_interval split: if_split_asm)
define c where "c i = (1 - u) * a i + u * b i" for i
have cge0: "\i. i \ S \ 0 \ c i"
using a b u01 by (simp add: c_def)
have sumc1: "sum c S = 1"
by (simp add: c_def sum.distrib sum_distrib_left [symmetric] asum bsum)
have sumci_xy: "(\i\S. c i *\<^sub>R i) = (1 - u) *\<^sub>R x + u *\<^sub>R y"
apply (simp add: c_def sum.distrib scaleR_left_distrib)
by (simp only: scaleR_scaleR [symmetric] Real_Vector_Spaces.scaleR_right.sum [symmetric] aeqx beqy)
show ?thesis
proof (cases "sum c (S - T) = 0")
case True
have ci0: "\i. i \ (S - T) \ c i = 0"
using True cge0 fin(2) sum_nonneg_eq_0_iff by auto
have a0: "a i = 0" if "i \ (S - T)" for i
using ci0 [OF that] u01 a [of i] b [of i] that
by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff)
have [simp]: "sum a T = 1"
using assms by (metis sum.mono_neutral_cong_right a0 asum)
show ?thesis
apply (simp add: convex_hull_finite \<open>finite T\<close>)
apply (rule_tac x=a in exI)
using a0 assms
apply (auto simp: cge0 a aeqx [symmetric] sum.mono_neutral_right)
done
next
case False
define k where "k = sum c (S - T)"
have "k > 0" using False
unfolding k_def by (metis DiffD1 antisym_conv cge0 sum_nonneg not_less)
have weq_sumsum: "w = sum (\x. c x *\<^sub>R x) T + sum (\x. c x *\<^sub>R x) (S - T)"
by (metis (no_types) add.commute S(1) S(2) sum.subset_diff sumci_xy weq)
show ?thesis
proof (cases "k = 1")
case True
then have "sum c T = 0"
by (simp add: S k_def sum_diff sumc1)
then have [simp]: "sum c (S - T) = 1"
by (simp add: S sum_diff sumc1)
have ci0: "\i. i \ T \ c i = 0"
by (meson \<open>finite T\<close> \<open>sum c T = 0\<close> \<open>T \<subseteq> S\<close> cge0 sum_nonneg_eq_0_iff subsetCE)
then have [simp]: "(\i\S-T. c i *\<^sub>R i) = w"
by (simp add: weq_sumsum)
have "w \ convex hull (S - T)"
apply (simp add: convex_hull_finite fin)
apply (rule_tac x=c in exI)
apply (auto simp: cge0 weq True k_def)
done
then show ?thesis
using disj waff by blast
next
case False
then have sumcf: "sum c T = 1 - k"
by (simp add: S k_def sum_diff sumc1)
have ge0: "\x. x \ T \ 0 \ inverse (1 - k) * c x"
by (metis \<open>T \<subseteq> S\<close> cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg subsetD sum_nonneg sumcf)
have eq1: "(\x\T. inverse (1 - k) * c x) = 1"
by (metis False eq_iff_diff_eq_0 mult.commute right_inverse sum_distrib_left sumcf)
have "(\i\T. c i *\<^sub>R i) /\<^sub>R (1 - k) \ convex hull T"
apply (simp add: convex_hull_finite fin)
apply (rule_tac x="\i. inverse (1-k) * c i" in exI)
by (metis (mono_tags, lifting) eq1 ge0 scaleR_scaleR scale_sum_right sum.cong)
with \<open>0 < k\<close> have "inverse(k) *\<^sub>R (w - sum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
moreover have "inverse(k) *\<^sub>R (w - sum (\x. c x *\<^sub>R x) T) \ convex hull (S - T)"
apply (simp add: weq_sumsum convex_hull_finite fin)
apply (rule_tac x="\i. inverse k * c i" in exI)
using \<open>k > 0\<close> cge0
apply (auto simp: scaleR_right.sum sum_distrib_left [symmetric] k_def [symmetric])
done
ultimately show ?thesis
using disj by blast
qed
qed
qed
have [simp]: "convex hull T \ convex hull S"
by (simp add: \<open>T \<subseteq> S\<close> hull_mono)
show ?thesis
using open_segment_commute by (auto simp: face_of_def intro: *)
qed
proposition face_of_convex_hull_insert:
assumes "finite S" "a \ affine hull S" and T: "T face_of convex hull S"
shows "T face_of convex hull insert a S"
proof -
have "convex hull S face_of convex hull insert a S"
by (simp add: assms face_of_convex_hulls insert_Diff_if subset_insertI)
then show ?thesis
using T face_of_trans by blast
qed
proposition face_of_affine_trivial:
assumes "affine S" "T face_of S"
shows "T = {} \ T = S"
proof (rule ccontr, clarsimp)
assume "T \ {}" "T \ S"
then obtain a where "a \ T" by auto
then have "a \ S"
using \<open>T face_of S\<close> face_of_imp_subset by blast
have "S \ T"
proof
fix b assume "b \ S"
show "b \ T"
proof (cases "a = b")
case True with \<open>a \<in> T\<close> show ?thesis by auto
next
case False
then have "a \ 2 *\<^sub>R a - b"
by (simp add: scaleR_2)
with False have "a \ open_segment (2 *\<^sub>R a - b) b"
apply (clarsimp simp: open_segment_def closed_segment_def)
apply (rule_tac x="1/2" in exI)
by (simp add: algebra_simps)
moreover have "2 *\<^sub>R a - b \ S"
by (rule mem_affine [OF \<open>affine S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>, of 2 "-1", simplified])
moreover note \<open>b \<in> S\<close> \<open>a \<in> T\<close>
ultimately show ?thesis
by (rule face_ofD [OF \<open>T face_of S\<close>, THEN conjunct2])
qed
qed
then show False
using \<open>T \<noteq> S\<close> \<open>T face_of S\<close> face_of_imp_subset by blast
qed
lemma face_of_affine_eq:
"affine S \ (T face_of S \ T = {} \ T = S)"
using affine_imp_convex face_of_affine_trivial face_of_refl by auto
proposition Inter_faces_finite_altbound:
fixes T :: "'a::euclidean_space set set"
assumes cfaI: "\c. c \ T \ c face_of S"
shows "\F'. finite F' \ F' \ T \ card F' \ DIM('a) + 2 \ \F' = \T"
proof (cases "\F'. finite F' \ F' \ T \ card F' \ DIM('a) + 2 \ (\c. c \ T \ c \ (\F') \ (\F'))")
case True
then obtain c where c:
"\F'. \finite F'; F' \ T; card F' \ DIM('a) + 2\ \ c F' \ T \ c F' \ (\F') \ (\F')"
by metis
define d where "d = rec_nat {c{}} (\n r. insert (c r) r)"
have [simp]: "d 0 = {c {}}"
by (simp add: d_def)
have dSuc [simp]: "\n. d (Suc n) = insert (c (d n)) (d n)"
by (simp add: d_def)
have dn_notempty: "d n \ {}" for n
by (induction n) auto
have dn_le_Suc: "d n \ T \ finite(d n) \ card(d n) \ Suc n" if "n \ DIM('a) + 2" for n
using that
proof (induction n)
case 0
then show ?case by (simp add: c)
next
case (Suc n)
then show ?case by (auto simp: c card_insert_if)
qed
have aff_dim_le: "aff_dim(\(d n)) \ DIM('a) - int n" if "n \ DIM('a) + 2" for n
using that
proof (induction n)
case 0
then show ?case
by (simp add: aff_dim_le_DIM)
next
case (Suc n)
have fs: "\(d (Suc n)) face_of S"
by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE)
have condn: "convex (\(d n))"
using Suc.prems nat_le_linear not_less_eq_eq
by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc)
have fdn: "\(d (Suc n)) face_of \(d n)"
by (metis (no_types, lifting) Inter_anti_mono Suc.prems dSuc cfaI dn_le_Suc dn_notempty face_of_Inter face_of_imp_subset face_of_subset subset_iff subset_insertI)
have ne: "\(d (Suc n)) \ \(d n)"
by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans)
have *: "\m::int. \d. \d'::int. d < d' \ d' \ m - n \ d \ m - of_nat(n+1)"
by arith
have "aff_dim (\(d (Suc n))) < aff_dim (\(d n))"
by (rule face_of_aff_dim_lt [OF condn fdn ne])
moreover have "aff_dim (\(d n)) \ int (DIM('a)) - int n"
using Suc by auto
ultimately
have "aff_dim (\(d (Suc n))) \ int (DIM('a)) - (n+1)" by arith
then show ?case by linarith
qed
have "aff_dim (\(d (DIM('a) + 2))) \ -2"
using aff_dim_le [OF order_refl] by simp
with aff_dim_geq [of "\(d (DIM('a) + 2))"] show ?thesis
using order.trans by fastforce
next
case False
then show ?thesis
apply simp
apply (erule ex_forward)
by blast
qed
lemma faces_of_translation:
"{F. F face_of image (\x. a + x) S} = image (image (\x. a + x)) {F. F face_of S}"
proof -
have "\F. F face_of (+) a ` S \ \G. G face_of S \ F = (+) a ` G"
by (metis face_of_imp_subset face_of_translation_eq subset_imageE)
then show ?thesis
by (auto simp: image_iff)
qed
proposition face_of_Times:
assumes "F face_of S" and "F' face_of S'"
shows "(F \ F') face_of (S \ S')"
proof -
have "F \ F' \ S \ S'"
using assms [unfolded face_of_def] by blast
moreover
have "convex (F \ F')"
using assms [unfolded face_of_def] by (blast intro: convex_Times)
moreover
have "a \ F \ a' \ F' \ b \ F \ b' \ F'"
if "a \ S" "b \ S" "a' \ S'" "b' \ S'" "x \ F \ F'" "x \ open_segment (a,a') (b,b')"
for a b a' b' x
proof (cases "b=a \ b'=a'")
case True with that show ?thesis
using assms
by (force simp: in_segment dest: face_ofD)
next
case False with assms [unfolded face_of_def] that show ?thesis
by (blast dest!: open_segment_PairD)
qed
ultimately show ?thesis
unfolding face_of_def by blast
qed
corollary face_of_Times_decomp:
fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
shows "C face_of (S \ S') \ (\F F'. F face_of S \ F' face_of S' \ C = F \ F')"
(is "?lhs = ?rhs")
proof
assume C: ?lhs
show ?rhs
proof (cases "C = {}")
case True then show ?thesis by auto
next
case False
have 1: "fst ` C \ S" "snd ` C \ S'"
using C face_of_imp_subset by fastforce+
have "convex C"
using C by (metis face_of_imp_convex)
have conv: "convex (fst ` C)" "convex (snd ` C)"
by (simp_all add: \<open>convex C\<close> convex_linear_image linear_fst linear_snd)
have fstab: "a \ fst ` C \ b \ fst ` C"
if "a \ S" "b \ S" "x \ open_segment a b" "(x,x') \ C" for a b x x'
proof -
have *: "(x,x') \ open_segment (a,x') (b,x')"
using that by (auto simp: in_segment)
show ?thesis
using face_ofD [OF C *] that face_of_imp_subset [OF C] by force
qed
have fst: "fst ` C face_of S"
by (force simp: face_of_def 1 conv fstab)
have sndab: "a' \ snd ` C \ b' \ snd ` C"
if "a' \ S'" "b' \ S'" "x' \ open_segment a' b'" "(x,x') \ C" for a' b' x x'
proof -
have *: "(x,x') \ open_segment (x,a') (x,b')"
using that by (auto simp: in_segment)
show ?thesis
using face_ofD [OF C *] that face_of_imp_subset [OF C] by force
qed
have snd: "snd ` C face_of S'"
by (force simp: face_of_def 1 conv sndab)
have cc: "rel_interior C \ rel_interior (fst ` C) \ rel_interior (snd ` C)"
by (force simp: face_of_Times rel_interior_Times conv fst snd \<open>convex C\<close> linear_fst linear_snd rel_interior_convex_linear_image [symmetric])
have "C = fst ` C \ snd ` C"
proof (rule face_of_eq [OF C])
show "fst ` C \ snd ` C face_of S \ S'"
by (simp add: face_of_Times rel_interior_Times conv fst snd)
show "rel_interior C \ rel_interior (fst ` C \ snd ` C) \ {}"
using False rel_interior_eq_empty \<open>convex C\<close> cc
by (auto simp: face_of_Times rel_interior_Times conv fst)
qed
with fst snd show ?thesis by metis
qed
next
assume ?rhs with face_of_Times show ?lhs by auto
qed
lemma face_of_Times_eq:
fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
shows "(F \ F') face_of (S \ S') \
F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
by (auto simp: face_of_Times_decomp times_eq_iff)
lemma hyperplane_face_of_halfspace_le: "{x. a \ x = b} face_of {x. a \ x \ b}"
proof -
have "{x. a \ x \ b} \ {x. a \ x = b} = {x. a \ x = b}"
by auto
with face_of_Int_supporting_hyperplane_le [OF convex_halfspace_le [of a b], of a b]
show ?thesis by auto
qed
lemma hyperplane_face_of_halfspace_ge: "{x. a \ x = b} face_of {x. a \ x \ b}"
proof -
have "{x. a \ x \ b} \ {x. a \ x = b} = {x. a \ x = b}"
by auto
with face_of_Int_supporting_hyperplane_ge [OF convex_halfspace_ge [of b a], of b a]
show ?thesis by auto
qed
lemma face_of_halfspace_le:
fixes a :: "'n::euclidean_space"
shows "F face_of {x. a \ x \ b} \
F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
(is "?lhs = ?rhs")
proof (cases "a = 0")
case True then show ?thesis
using face_of_affine_eq affine_UNIV by auto
next
case False
then have ine: "interior {x. a \ x \ b} \ {}"
using halfspace_eq_empty_lt interior_halfspace_le by blast
show ?thesis
proof
assume L: ?lhs
have "F face_of {x. a \ x = b}" if "F \ {x. a \ x \ b}"
proof -
have "F face_of rel_frontier {x. a \ x \ b}"
proof (rule face_of_subset [OF L])
show "F \ rel_frontier {x. a \ x \ b}"
by (simp add: L face_of_subset_rel_frontier that)
qed (force simp: rel_frontier_def closed_halfspace_le)
then show ?thesis
using False
by (simp add: frontier_halfspace_le rel_frontier_nonempty_interior [OF ine])
qed
with L show ?rhs
using affine_hyperplane face_of_affine_eq by blast
next
assume ?rhs
then show ?lhs
by (metis convex_halfspace_le empty_face_of face_of_refl hyperplane_face_of_halfspace_le)
qed
qed
lemma face_of_halfspace_ge:
fixes a :: "'n::euclidean_space"
shows "F face_of {x. a \ x \ b} \
F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
using face_of_halfspace_le [of F "-a" "-b"] by simp
subsection\<open>Exposed faces\<close>
text\<open>That is, faces that are intersection with supporting hyperplane\<close>
definition\<^marker>\<open>tag important\<close> exposed_face_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
(infixr "(exposed'_face'_of)" 50)
where "T exposed_face_of S \
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})"
lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
apply (simp add: exposed_face_of_def)
apply (rule_tac x=0 in exI)
apply (rule_tac x=1 in exI, force)
done
lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \ convex S"
proof
assume S: "convex S"
have "S \ {x. 0 \ x \ 0} \ S = S \ {x. 0 \ x = 0}"
by auto
with S show "S exposed_face_of S"
using exposed_face_of_def face_of_refl_eq by blast
qed (simp add: exposed_face_of_def face_of_refl_eq)
lemma exposed_face_of_refl: "convex S \ S exposed_face_of S"
by simp
lemma exposed_face_of:
"T exposed_face_of S \
T face_of S \<and>
(T = {} \<or> T = S \<or>
(\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b}))"
proof (cases "T = {}")
case True then show ?thesis
by simp
next
case False
show ?thesis
proof (cases "T = S")
case True then show ?thesis
by (simp add: face_of_refl_eq)
next
case False
with \<open>T \<noteq> {}\<close> show ?thesis
apply (auto simp: exposed_face_of_def)
apply (metis inner_zero_left)
done
qed
qed
lemma exposed_face_of_Int_supporting_hyperplane_le:
"\convex S; \x. x \ S \ a \ x \ b\ \ (S \ {x. a \ x = b}) exposed_face_of S"
by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
lemma exposed_face_of_Int_supporting_hyperplane_ge:
"\convex S; \x. x \ S \ a \ x \ b\ \ (S \ {x. a \ x = b}) exposed_face_of S"
using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
proposition exposed_face_of_Int:
assumes "T exposed_face_of S"
and "u exposed_face_of S"
shows "(T \ u) exposed_face_of S"
proof -
obtain a b where T: "S \ {x. a \ x = b} face_of S"
and S: "S \ {x. a \ x \ b}"
and teq: "T = S \ {x. a \ x = b}"
using assms by (auto simp: exposed_face_of_def)
obtain a' b' where u: "S \ {x. a' \ x = b'} face_of S"
and s': "S \ {x. a' \ x \ b'}"
and ueq: "u = S \ {x. a' \ x = b'}"
using assms by (auto simp: exposed_face_of_def)
have tu: "T \ u face_of S"
using T teq u ueq by (simp add: face_of_Int)
have ss: "S \ {x. (a + a') \ x \ b + b'}"
using S s' by (force simp: inner_left_distrib)
show ?thesis
apply (simp add: exposed_face_of_def tu)
apply (rule_tac x="a+a'" in exI)
apply (rule_tac x="b+b'" in exI)
using S s'
apply (fastforce simp: ss inner_left_distrib teq ueq)
done
qed
proposition exposed_face_of_Inter:
fixes P :: "'a::euclidean_space set set"
assumes "P \ {}"
and "\T. T \ P \ T exposed_face_of S"
shows "\P exposed_face_of S"
proof -
obtain Q where "finite Q" and QsubP: "Q \ P" "card Q \ DIM('a) + 2" and IntQ: "\Q = \P"
using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of]
by force
show ?thesis
proof (cases "Q = {}")
case True then show ?thesis
by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv)
next
case False
have "Q \ {T. T exposed_face_of S}"
using QsubP assms by blast
moreover have "Q \ {T. T exposed_face_of S} \ \Q exposed_face_of S"
using \<open>finite Q\<close> False
by (induction Q rule: finite_induct; use exposed_face_of_Int in fastforce)
ultimately show ?thesis
by (simp add: IntQ)
qed
qed
proposition exposed_face_of_sums:
assumes "convex S" and "convex T"
and "F exposed_face_of {x + y | x y. x \ S \ y \ T}"
(is "F exposed_face_of ?ST")
obtains k l
where "k exposed_face_of S" "l exposed_face_of T"
"F = {x + y | x y. x \ k \ y \ l}"
proof (cases "F = {}")
case True then show ?thesis
using that by blast
next
case False
show ?thesis
proof (cases "F = ?ST")
case True then show ?thesis
using assms exposed_face_of_refl_eq that by blast
next
case False
obtain p where "p \ F" using \F \ {}\ by blast
moreover
obtain u z where T: "?ST \ {x. u \ x = z} face_of ?ST"
and S: "?ST \ {x. u \ x \ z}"
and feq: "F = ?ST \ {x. u \ x = z}"
using assms by (auto simp: exposed_face_of_def)
ultimately obtain a0 b0
where p: "p = a0 + b0" and "a0 \ S" "b0 \ T" and z: "u \ p = z"
by auto
have lez: "u \ (x + y) \ z" if "x \ S" "y \ T" for x y
using S that by auto
have sef: "S \ {x. u \ x = u \ a0} exposed_face_of S"
proof (rule exposed_face_of_Int_supporting_hyperplane_le [OF \<open>convex S\<close>])
show "\x. x \ S \ u \ x \ u \ a0"
by (metis p z add_le_cancel_right inner_right_distrib lez [OF _ \<open>b0 \<in> T\<close>])
qed
have tef: "T \ {x. u \ x = u \ b0} exposed_face_of T"
proof (rule exposed_face_of_Int_supporting_hyperplane_le [OF \<open>convex T\<close>])
show "\x. x \ T \ u \ x \ u \ b0"
by (metis p z add.commute add_le_cancel_right inner_right_distrib lez [OF \<open>a0 \<in> S\<close>])
qed
have "{x + y |x y. x \ S \ u \ x = u \ a0 \ y \ T \ u \ y = u \ b0} \ F"
by (auto simp: feq) (metis inner_right_distrib p z)
moreover have "F \ {x + y |x y. x \ S \ u \ x = u \ a0 \ y \ T \ u \ y = u \ b0}"
proof -
have "\x y. \z = u \ (x + y); x \ S; y \ T\
\<Longrightarrow> u \<bullet> x = u \<bullet> a0 \<and> u \<bullet> y = u \<bullet> b0"
using z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close>
apply (simp add: inner_right_distrib)
apply (metis add_le_cancel_right antisym lez [unfolded inner_right_distrib] add.commute)
done
then show ?thesis
using feq by blast
qed
ultimately have "F = {x + y |x y. x \ S \ {x. u \ x = u \ a0} \ y \ T \ {x. u \ x = u \ b0}}"
by blast
then show ?thesis
by (rule that [OF sef tef])
qed
qed
proposition exposed_face_of_parallel:
"T exposed_face_of S \
T face_of S \<and>
(\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b} \<and>
(T \<noteq> {} \<longrightarrow> T \<noteq> S \<longrightarrow> a \<noteq> 0) \<and>
(T \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. (w + a) \<in> affine hull S)))"
(is "?lhs = ?rhs")
proof
assume ?lhs then show ?rhs
proof (clarsimp simp: exposed_face_of_def)
fix a b
assume faceS: "S \ {x. a \ x = b} face_of S" and Ssub: "S \ {x. a \ x \ b}"
show "\c d. S \ {x. c \ x \ d} \
S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. c \<bullet> x = d} \<and>
(S \<inter> {x. a \<bullet> x = b} \<noteq> {} \<longrightarrow> S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> c \<noteq> 0) \<and>
(S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. w + c \<in> affine hull S))"
proof (cases "affine hull S \ {x. -a \ x \ -b} = {} \ affine hull S \ {x. - a \ x \ - b}")
case True
then show ?thesis
proof
assume "affine hull S \ {x. - a \ x \ - b} = {}"
then show ?thesis
apply (rule_tac x="0" in exI)
apply (rule_tac x="1" in exI)
using hull_subset by fastforce
next
assume "affine hull S \ {x. - a \ x \ - b}"
then show ?thesis
apply (rule_tac x="0" in exI)
apply (rule_tac x="0" in exI)
using Ssub hull_subset by fastforce
qed
next
case False
then obtain a' b' where "a' \ 0"
and le: "affine hull S \ {x. a' \ x \ b'} = affine hull S \ {x. - a \ x \ - b}"
and eq: "affine hull S \ {x. a' \ x = b'} = affine hull S \ {x. - a \ x = - b}"
and mem: "\w. w \ affine hull S \ w + a' \ affine hull S"
using affine_parallel_slice affine_affine_hull by metis
show ?thesis
proof (intro conjI impI allI ballI exI)
have *: "S \ - (affine hull S \ {x. P x}) \ affine hull S \ {x. Q x} \ S \ {x. \ P x \ Q x}"
for P Q
using hull_subset by fastforce
have "S \ {x. \ (a' \ x \ b') \ a' \ x = b'}"
by (rule *) (use le eq Ssub in auto)
then show "S \ {x. - a' \ x \ - b'}"
by auto
show "S \ {x. a \ x = b} = S \ {x. - a' \ x = - b'}"
using eq hull_subset [of S affine] by force
show "\S \ {x. a \ x = b} \ {}; S \ {x. a \ x = b} \ S\ \ - a' \ 0"
using \<open>a' \<noteq> 0\<close> by auto
show "w + - a' \ affine hull S"
if "S \ {x. a \ x = b} \ S" "w \ affine hull S" for w
proof -
have "w + 1 *\<^sub>R (w - (w + a')) \ affine hull S"
using affine_affine_hull mem mem_affine_3_minus that(2) by blast
then show ?thesis by simp
qed
qed
qed
qed
next
assume ?rhs then show ?lhs
unfolding exposed_face_of_def by blast
qed
subsection\<open>Extreme points of a set: its singleton faces\<close>
definition\<^marker>\<open>tag important\<close> extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
(infixr "(extreme'_point'_of)" 50)
where "x extreme_point_of S \
x \<in> S \<and> (\<forall>a \<in> S. \<forall>b \<in> S. x \<notin> open_segment a b)"
lemma extreme_point_of_stillconvex:
"convex S \ (x extreme_point_of S \ x \ S \ convex(S - {x}))"
by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)
lemma face_of_singleton:
"{x} face_of S \ x extreme_point_of S"
by (fastforce simp add: extreme_point_of_def face_of_def)
lemma extreme_point_not_in_REL_INTERIOR:
fixes S :: "'a::real_normed_vector set"
shows "\x extreme_point_of S; S \ {x}\ \ x \ rel_interior S"
by (metis disjoint_iff face_of_disjoint_rel_interior face_of_singleton insertI1)
lemma extreme_point_not_in_interior:
fixes S :: "'a::{real_normed_vector, perfect_space} set"
assumes "x extreme_point_of S" shows "x \ interior S"
proof (cases "S = {x}")
case False
then show ?thesis
by (meson assms subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior)
qed (simp add: empty_interior_finite)
lemma extreme_point_of_face:
"F face_of S \ v extreme_point_of F \ v extreme_point_of S \ v \ F"
by (meson empty_subsetI face_of_face face_of_singleton insert_subset)
lemma extreme_point_of_convex_hull:
"x extreme_point_of (convex hull S) \ x \ S"
using hull_minimal [of S "(convex hull S) - {x}" convex]
using hull_subset [of S convex]
by (force simp add: extreme_point_of_stillconvex)
proposition extreme_points_of_convex_hull:
"{x. x extreme_point_of (convex hull S)} \ S"
using extreme_point_of_convex_hull by auto
lemma extreme_point_of_empty [simp]: "\ (x extreme_point_of {})"
by (simp add: extreme_point_of_def)
lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} \ x = a"
using extreme_point_of_stillconvex by auto
lemma extreme_point_of_translation_eq:
"(a + x) extreme_point_of (image (\x. a + x) S) \ x extreme_point_of S"
by (auto simp: extreme_point_of_def)
lemma extreme_points_of_translation:
"{x. x extreme_point_of (image (\x. a + x) S)} =
(\<lambda>x. a + x) ` {x. x extreme_point_of S}"
using extreme_point_of_translation_eq
by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
lemma extreme_points_of_translation_subtract:
"{x. x extreme_point_of (image (\x. x - a) S)} =
(\<lambda>x. x - a) ` {x. x extreme_point_of S}"
using extreme_points_of_translation [of "- a" S]
by simp
lemma extreme_point_of_Int:
"\x extreme_point_of S; x extreme_point_of T\ \ x extreme_point_of (S \ T)"
by (simp add: extreme_point_of_def)
lemma extreme_point_of_Int_supporting_hyperplane_le:
"\S \ {x. a \ x = b} = {c}; \x. x \ S \ a \ x \ b\ \ c extreme_point_of S"
by (metis convex_singleton face_of_Int_supporting_hyperplane_le_strong face_of_singleton)
lemma extreme_point_of_Int_supporting_hyperplane_ge:
"\S \ {x. a \ x = b} = {c}; \x. x \ S \ a \ x \ b\ \ c extreme_point_of S"
using extreme_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
by simp
lemma exposed_point_of_Int_supporting_hyperplane_le:
"\S \ {x. a \ x = b} = {c}; \x. x \ S \ a \ x \ b\ \ {c} exposed_face_of S"
unfolding exposed_face_of_def
by (force simp: face_of_singleton extreme_point_of_Int_supporting_hyperplane_le)
lemma exposed_point_of_Int_supporting_hyperplane_ge:
"\S \ {x. a \ x = b} = {c}; \x. x \ S \ a \ x \ b\ \ {c} exposed_face_of S"
using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
by simp
lemma extreme_point_of_convex_hull_insert:
assumes "finite S" "a \ convex hull S"
shows "a extreme_point_of (convex hull (insert a S))"
proof (cases "a \ S")
case False
then show ?thesis
using face_of_convex_hulls [of "insert a S" "{a}"] assms
by (auto simp: face_of_singleton hull_same)
qed (use assms in \<open>simp add: hull_inc\<close>)
subsection\<open>Facets\<close>
definition\<^marker>\<open>tag important\<close> facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
(infixr "(facet'_of)" 50)
where "F facet_of S \ F face_of S \ F \ {} \ aff_dim F = aff_dim S - 1"
lemma facet_of_empty [simp]: "\ S facet_of {}"
by (simp add: facet_of_def)
lemma facet_of_irrefl [simp]: "\ S facet_of S "
by (simp add: facet_of_def)
lemma facet_of_imp_face_of: "F facet_of S \ F face_of S"
by (simp add: facet_of_def)
lemma facet_of_imp_subset: "F facet_of S \ F \ S"
by (simp add: face_of_imp_subset facet_of_def)
lemma hyperplane_facet_of_halfspace_le:
"a \ 0 \ {x. a \ x = b} facet_of {x. a \ x \ b}"
unfolding facet_of_def hyperplane_eq_empty
by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
Suc_leI of_nat_diff aff_dim_halfspace_le)
lemma hyperplane_facet_of_halfspace_ge:
"a \ 0 \ {x. a \ x = b} facet_of {x. a \ x \ b}"
unfolding facet_of_def hyperplane_eq_empty
by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
Suc_leI of_nat_diff aff_dim_halfspace_ge)
lemma facet_of_halfspace_le:
"F facet_of {x. a \ x \ b} \ a \ 0 \ F = {x. a \ x = b}"
(is "?lhs = ?rhs")
proof
assume c: ?lhs
with c facet_of_irrefl show ?rhs
by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm)
next
assume ?rhs then show ?lhs
by (simp add: hyperplane_facet_of_halfspace_le)
qed
lemma facet_of_halfspace_ge:
"F facet_of {x. a \ x \ b} \ a \ 0 \ F = {x. a \ x = b}"
using facet_of_halfspace_le [of F "-a" "-b"] by simp
subsection \<open>Edges: faces of affine dimension 1\<close> (*FIXME too small subsection, rearrange? *)
definition\<^marker>\<open>tag important\<close> edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool" (infixr "(edge'_of)" 50)
where "e edge_of S \ e face_of S \ aff_dim e = 1"
lemma edge_of_imp_subset:
"S edge_of T \ S \ T"
by (simp add: edge_of_def face_of_imp_subset)
subsection\<open>Existence of extreme points\<close>
proposition different_norm_3_collinear_points:
fixes a :: "'a::euclidean_space"
assumes "x \ open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)"
shows False
proof -
obtain u where "norm ((1 - u) *\<^sub>R a + u *\<^sub>R b) = norm b"
and "a \ b"
and u01: "0 < u" "u < 1"
using assms by (auto simp: open_segment_image_interval if_splits)
then have "(1 - u) *\<^sub>R a \ (1 - u) *\<^sub>R a + ((1 - u) * 2) *\<^sub>R a \ u *\<^sub>R b =
(1 - u * u) *\<^sub>R (a \<bullet> a)"
using assms by (simp add: norm_eq algebra_simps inner_commute)
then have "(1 - u) *\<^sub>R ((1 - u) *\<^sub>R a \ a + (2 * u) *\<^sub>R a \ b) =
(1 - u) *\<^sub>R ((1 + u) *\<^sub>R (a \<bullet> a))"
by (simp add: algebra_simps)
then have "(1 - u) *\<^sub>R (a \ a) + (2 * u) *\<^sub>R (a \ b) = (1 + u) *\<^sub>R (a \ a)"
using u01 by auto
then have "a \ b = a \ a"
using u01 by (simp add: algebra_simps)
then have "a = b"
using \<open>norm(a) = norm(b)\<close> norm_eq vector_eq by fastforce
then show ?thesis
using \<open>a \<noteq> b\<close> by force
qed
proposition extreme_point_exists_convex:
fixes S :: "'a::euclidean_space set"
assumes "compact S" "convex S" "S \ {}"
obtains x where "x extreme_point_of S"
proof -
obtain x where "x \ S" and xsup: "\y. y \ S \ norm y \ norm x"
using distance_attains_sup [of S 0] assms by auto
have False if "a \ S" "b \ S" and x: "x \ open_segment a b" for a b
proof -
have noax: "norm a \ norm x" and nobx: "norm b \ norm x" using xsup that by auto
have "a \ b"
using empty_iff open_segment_idem x by auto
show False
by (metis dist_0_norm dist_decreases_open_segment noax nobx not_le x)
qed
then show ?thesis
by (meson \<open>x \<in> S\<close> extreme_point_of_def that)
qed
subsection\<open>Krein-Milman, the weaker form\<close>
proposition Krein_Milman:
fixes S :: "'a::euclidean_space set"
assumes "compact S" "convex S"
shows "S = closure(convex hull {x. x extreme_point_of S})"
proof (cases "S = {}")
case True then show ?thesis by simp
next
case False
have "closed S"
by (simp add: \<open>compact S\<close> compact_imp_closed)
have "closure (convex hull {x. x extreme_point_of S}) \ S"
by (simp add: \<open>closed S\<close> assms closure_minimal extreme_point_of_def hull_minimal)
moreover have "u \ closure (convex hull {x. x extreme_point_of S})"
if "u \ S" for u
proof (rule ccontr)
assume unot: "u \ closure(convex hull {x. x extreme_point_of S})"
then obtain a b where "a \ u < b"
and ab: "\x. x \ closure(convex hull {x. x extreme_point_of S}) \ b < a \ x"
using separating_hyperplane_closed_point [of "closure(convex hull {x. x extreme_point_of S})"]
by blast
have "continuous_on S ((\) a)"
by (rule continuous_intros)+
then obtain m where "m \ S" and m: "\y. y \ S \ a \ m \ a \ y"
using continuous_attains_inf [of S "\x. a \ x"] \compact S\ \u \ S\
by auto
define T where "T = S \ {x. a \ x = a \ m}"
have "m \ T"
by (simp add: T_def \<open>m \<in> S\<close>)
moreover have "compact T"
by (simp add: T_def compact_Int_closed [OF \<open>compact S\<close> closed_hyperplane])
moreover have "convex T"
by (simp add: T_def convex_Int [OF \<open>convex S\<close> convex_hyperplane])
ultimately obtain v where v: "v extreme_point_of T"
using extreme_point_exists_convex [of T] by auto
then have "{v} face_of T"
by (simp add: face_of_singleton)
also have "T face_of S"
by (simp add: T_def m face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
finally have "v extreme_point_of S"
by (simp add: face_of_singleton)
then have "b < a \ v"
using closure_subset by (simp add: closure_hull hull_inc ab)
then show False
using \<open>a \<bullet> u < b\<close> \<open>{v} face_of T\<close> face_of_imp_subset m T_def that by fastforce
qed
ultimately show ?thesis
by blast
qed
text\<open>Now the sharper form.\<close>
lemma Krein_Milman_Minkowski_aux:
fixes S :: "'a::euclidean_space set"
assumes n: "dim S = n" and S: "compact S" "convex S" "0 \ S"
shows "0 \ convex hull {x. x extreme_point_of S}"
using n S
proof (induction n arbitrary: S rule: less_induct)
case (less n S) show ?case
proof (cases "0 \ rel_interior S")
case True with Krein_Milman less.prems
show ?thesis
by (metis subsetD convex_convex_hull convex_rel_interior_closure rel_interior_subset)
next
case False
have "rel_interior S \ {}"
by (simp add: rel_interior_convex_nonempty_aux less)
then obtain c where c: "c \ rel_interior S" by blast
obtain a where "a \ 0"
and le_ay: "\y. y \ S \ a \ 0 \ a \ y"
and less_ay: "\y. y \ rel_interior S \ a \ 0 < a \ y"
by (blast intro: supporting_hyperplane_rel_boundary intro!: less False)
have face: "S \ {x. a \ x = 0} face_of S"
using face_of_Int_supporting_hyperplane_ge le_ay \<open>convex S\<close> by auto
then have co: "compact (S \ {x. a \ x = 0})" "convex (S \ {x. a \ x = 0})"
using less.prems by (blast intro: face_of_imp_compact face_of_imp_convex)+
have "a \ y = 0" if "y \ span (S \ {x. a \ x = 0})" for y
proof -
have "y \ span {x. a \ x = 0}"
by (metis inf.cobounded2 span_mono subsetCE that)
then show ?thesis
by (blast intro: span_induct [OF _ subspace_hyperplane])
qed
then have "dim (S \ {x. a \ x = 0}) < n"
by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_base)
then have "0 \ convex hull {x. x extreme_point_of (S \ {x. a \ x = 0})}"
by (rule less.IH) (auto simp: co less.prems)
then show ?thesis
by (metis (mono_tags, lifting) Collect_mono_iff face extreme_point_of_face hull_mono subset_iff)
qed
qed
theorem Krein_Milman_Minkowski:
fixes S :: "'a::euclidean_space set"
assumes "compact S" "convex S"
shows "S = convex hull {x. x extreme_point_of S}"
proof
show "S \ convex hull {x. x extreme_point_of S}"
proof
fix a assume [simp]: "a \ S"
have 1: "compact ((+) (- a) ` S)"
by (simp add: \<open>compact S\<close> compact_translation_subtract cong: image_cong_simp)
have 2: "convex ((+) (- a) ` S)"
by (simp add: \<open>convex S\<close> compact_translation_subtract)
show a_invex: "a \ convex hull {x. x extreme_point_of S}"
using Krein_Milman_Minkowski_aux [OF refl 1 2]
convex_hull_translation [of "-a"]
by (auto simp: extreme_points_of_translation_subtract translation_assoc cong: image_cong_simp)
qed
next
show "convex hull {x. x extreme_point_of S} \ S"
proof -
have "{a. a extreme_point_of S} \ S"
using extreme_point_of_def by blast
then show ?thesis
by (simp add: \<open>convex S\<close> hull_minimal)
qed
qed
subsection\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
corollary Krein_Milman_polytope:
fixes S :: "'a::euclidean_space set"
shows
"finite S
\<Longrightarrow> convex hull S =
convex hull {x. x extreme_point_of (convex hull S)}"
by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
lemma extreme_points_of_convex_hull_eq:
fixes S :: "'a::euclidean_space set"
shows
"\compact S; \T. T \ S \ convex hull T \ convex hull S\
\<Longrightarrow> {x. x extreme_point_of (convex hull S)} = S"
by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
lemma extreme_point_of_convex_hull_eq:
fixes S :: "'a::euclidean_space set"
shows
"\compact S; \T. T \ S \ convex hull T \ convex hull S\
\<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
using extreme_points_of_convex_hull_eq by auto
lemma extreme_point_of_convex_hull_convex_independent:
fixes S :: "'a::euclidean_space set"
assumes "compact S" and S: "\a. a \ S \ a \ convex hull (S - {a})"
shows "(x extreme_point_of (convex hull S) \ x \ S)"
proof -
have "convex hull T \ convex hull S" if "T \ S" for T
proof -
obtain a where "T \ S" "a \ S" "a \ T" using \T \ S\ by blast
then show ?thesis
by (metis (full_types) Diff_eq_empty_iff Diff_insert0 S hull_mono hull_subset insert_Diff_single subsetCE)
qed
then show ?thesis
by (rule extreme_point_of_convex_hull_eq [OF \<open>compact S\<close>])
qed
lemma extreme_point_of_convex_hull_affine_independent:
fixes S :: "'a::euclidean_space set"
shows
"\ affine_dependent S
\<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc)
text\<open>Elementary proofs exist, not requiring Euclidean spaces and all this development\<close>
lemma extreme_point_of_convex_hull_2:
fixes x :: "'a::euclidean_space"
shows "x extreme_point_of (convex hull {a,b}) \ x = a \ x = b"
proof -
have "x extreme_point_of (convex hull {a,b}) \ x \ {a,b}"
by (intro extreme_point_of_convex_hull_affine_independent affine_independent_2)
then show ?thesis
by simp
qed
lemma extreme_point_of_segment:
fixes x :: "'a::euclidean_space"
shows
"x extreme_point_of closed_segment a b \ x = a \ x = b"
by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
lemma face_of_convex_hull_subset:
fixes S :: "'a::euclidean_space set"
assumes "compact S" and T: "T face_of (convex hull S)"
obtains s' where "s' \<subseteq> S" "T = convex hull s'"
proof
show "{x. x extreme_point_of T} \ S"
using T extreme_point_of_convex_hull extreme_point_of_face by blast
show "T = convex hull {x. x extreme_point_of T}"
proof (rule Krein_Milman_Minkowski)
show "compact T"
using T assms compact_convex_hull face_of_imp_compact by auto
show "convex T"
using T face_of_imp_convex by blast
qed
qed
lemma face_of_convex_hull_aux:
assumes eq: "x *\<^sub>R p = u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c"
and x: "u + v + w = x" "x \ 0" and S: "affine S" "a \ S" "b \ S" "c \ S"
shows "p \ S"
proof -
have "p = (u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x"
by (metis \<open>x \<noteq> 0\<close> eq mult.commute right_inverse scaleR_one scaleR_scaleR)
moreover have "affine hull {a,b,c} \ S"
by (simp add: S hull_minimal)
moreover have "(u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x \ affine hull {a,b,c}"
apply (simp add: affine_hull_3)
apply (rule_tac x="u/x" in exI)
apply (rule_tac x="v/x" in exI)
apply (rule_tac x="w/x" in exI)
using x apply (auto simp: field_split_simps)
done
ultimately show ?thesis by force
qed
proposition face_of_convex_hull_insert_eq:
fixes a :: "'a :: euclidean_space"
assumes "finite S" and a: "a \ affine hull S"
shows "(F face_of (convex hull (insert a S)) \
F face_of (convex hull S) \<or>
(\<exists>F'. F' face_of (convex hull S) \<and> F = convex hull (insert a F')))"
(is "F face_of ?CAS \ _")
proof safe
assume F: "F face_of ?CAS"
and *: "\F'. F' face_of convex hull S \ F = convex hull insert a F'"
obtain T where T: "T \ insert a S" and FeqT: "F = convex hull T"
by (metis F \<open>finite S\<close> compact_insert finite_imp_compact face_of_convex_hull_subset)
show "F face_of convex hull S"
proof (cases "a \ T")
case True
have "F = convex hull insert a (convex hull T \ convex hull S)"
proof
have "T \ insert a (convex hull T \ convex hull S)"
using T hull_subset by fastforce
then show "F \ convex hull insert a (convex hull T \ convex hull S)"
by (simp add: FeqT hull_mono)
show "convex hull insert a (convex hull T \ convex hull S) \ F"
by (simp add: FeqT True hull_inc hull_minimal)
qed
moreover have "convex hull T \ convex hull S face_of convex hull S"
by (metis F FeqT convex_convex_hull face_of_slice hull_mono inf.absorb_iff2 subset_insertI)
ultimately show ?thesis
using * by force
next
case False
then show ?thesis
by (metis FeqT F T face_of_subset hull_mono subset_insert subset_insertI)
qed
next
assume "F face_of convex hull S"
show "F face_of ?CAS"
by (simp add: \<open>F face_of convex hull S\<close> a face_of_convex_hull_insert \<open>finite S\<close>)
next
fix F
assume F: "F face_of convex hull S"
show "convex hull insert a F face_of ?CAS"
proof (cases "S = {}")
case True
then show ?thesis
using F face_of_affine_eq by auto
next
case False
have anotc: "a \ convex hull S"
by (metis (no_types) a affine_hull_convex_hull hull_inc)
show ?thesis
proof (cases "F = {}")
case True show ?thesis
using anotc by (simp add: \<open>F = {}\<close> \<open>finite S\<close> extreme_point_of_convex_hull_insert face_of_singleton)
next
case False
have "convex hull insert a F \ ?CAS"
by (simp add: F a \<open>finite S\<close> convex_hull_subset face_of_convex_hull_insert face_of_imp_subset hull_inc)
moreover
have "(\y v. (1 - ub) *\<^sub>R a + ub *\<^sub>R b = (1 - v) *\<^sub>R a + v *\<^sub>R y \
0 \<le> v \<and> v \<le> 1 \<and> y \<in> F) \<and>
(\<exists>x u. (1 - uc) *\<^sub>R a + uc *\<^sub>R c = (1 - u) *\<^sub>R a + u *\<^sub>R x \<and>
0 \<le> u \<and> u \<le> 1 \<and> x \<in> F)"
if *: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x
\<in> open_segment ((1 - ub) *\<^sub>R a + ub *\<^sub>R b) ((1 - uc) *\<^sub>R a + uc *\<^sub>R c)"
and "0 \ ub" "ub \ 1" "0 \ uc" "uc \ 1" "0 \ ux" "ux \ 1"
and b: "b \ convex hull S" and c: "c \ convex hull S" and "x \ F"
for b c ub uc ux x
proof -
have xah: "x \ affine hull S"
using F convex_hull_subset_affine_hull face_of_imp_subset \<open>x \<in> F\<close> by blast
have ah: "b \ affine hull S" "c \ affine hull S"
using b c convex_hull_subset_affine_hull by blast+
obtain v where ne: "(1 - ub) *\<^sub>R a + ub *\<^sub>R b \ (1 - uc) *\<^sub>R a + uc *\<^sub>R c"
and eq: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x =
(1 - v) *\<^sub>R ((1 - ub) *\<^sub>R a + ub *\<^sub>R b) + v *\<^sub>R ((1 - uc) *\<^sub>R a + uc *\<^sub>R c)"
and "0 < v" "v < 1"
using * by (auto simp: in_segment)
then have 0: "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a +
(ux *\<^sub>R x - (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)) = 0"
by (auto simp: algebra_simps)
then have "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a =
((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c + (-ux) *\<^sub>R x"
by (auto simp: algebra_simps)
then have "a \ affine hull S" if "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) \ 0"
by (rule face_of_convex_hull_aux) (use b c xah ah that in \<open>auto simp: algebra_simps\<close>)
then have "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) = 0"
using a by blast
with 0 have equx: "(1 - v) * ub + v * uc = ux"
and uxx: "ux *\<^sub>R x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)"
by auto (auto simp: algebra_simps)
show ?thesis
proof (cases "uc = 0")
case True
then show ?thesis
using equx \<open>0 \<le> ub\<close> \<open>ub \<le> 1\<close> \<open>v < 1\<close> uxx \<open>x \<in> F\<close> by force
next
case False
show ?thesis
proof (cases "ub = 0")
case True
then show ?thesis
using equx \<open>0 \<le> uc\<close> \<open>uc \<le> 1\<close> \<open>0 < v\<close> uxx \<open>x \<in> F\<close> by force
next
case False
then have "0 < ub" "0 < uc"
using \<open>uc \<noteq> 0\<close> \<open>0 \<le> ub\<close> \<open>0 \<le> uc\<close> by auto
then have "(1 - v) * ub > 0" "v * uc > 0"
by (simp_all add: \<open>0 < uc\<close> \<open>0 < v\<close> \<open>v < 1\<close>)
then have "ux \ 0"
using equx \<open>0 < v\<close> by auto
have "b \ F \ c \ F"
proof (cases "b = c")
case True
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.61 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
