Quelle Polytope.thy 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 \<open>(face'_of)\<close> 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 faces_of_linear_image:
   "\linear f; inj f\ \ {T. T face_of (f ` S)} = (image f) ` {T. T face_of S}"
  by (smt (verit) Collect_cong face_of_def face_of_linear_image setcompr_eq_image subset_imageE)

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

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

lemma empty_face_of [iff]: "{} face_of S"
  by (simp add: face_of_def)

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

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

lemma face_of_face: "T face_of S \ (f face_of T \ f face_of S \ f \ T)"
  unfolding face_of_def by (safe; blast)

lemma face_of_subset: "\F face_of S; F \ T; T \ S\ \ F face_of T"
  unfolding face_of_def by (safe; blast)

lemma face_of_slice: "\F face_of S; convex T\ \ (F \ T) face_of (S \ T)"
  unfolding face_of_def by (blast intro: convex_Int)

lemma face_of_Int: "\t1 face_of S; t2 face_of S\ \ (t1 \ t2) face_of S"
  unfolding face_of_def by (blast intro: convex_Int)

lemma face_of_Inter: "\A \ {}; \T. T \ A \ T face_of S\ \ (\ A) face_of S"
  unfolding face_of_def by (blast intro: convex_Inter)

lemma face_of_Int_Int: "\F face_of T; F' face_of t'\ \ (F \ F') face_of (T \ t')"
  unfolding face_of_def by (blast intro: convex_Int)

lemma face_of_imp_subset: "T face_of S \ T \ S"
  unfolding face_of_def by blast

proposition face_of_imp_eq_affine_Int:
  fixes S :: "'a::euclidean_space set"
  assumes S: "convex S"  and T: "T face_of S"
  shows "T = (affine hull T) \ S"
proof -
  have "convex T" using T by (simp add: face_of_def)
  have *: False if x: "x \ affine hull T" and "x \ S" "x \ T" and y: "y \ rel_interior T" for x y
  proof -
    obtain e where "e>0" and e: "cball y e \ affine hull T \ T"
      using y by (auto simp: rel_interior_cball)
    have "y \ x" "y \ S" "y \ T"
      using face_of_imp_subset rel_interior_subset T that by blast+
    then have zne: "\u. \u \ {0<..<1}; (1 - u) *\<^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))
    define u where "u \ min (1/2) (e / norm (x - y))"
    have in01: "u \ {0<..<1}"
      using \<open>y \<noteq> x\<close> \<open>e > 0\<close> by (simp add: u_def)
    have "norm (u *\<^sub>R y - u *\<^sub>R x) \ e"
      using \<open>e > 0\<close>
      by (simp add: u_def norm_minus_commute min_mult_distrib_right flip: scaleR_diff_right)
    then have "dist y ((1 - u) *\<^sub>R y + u *\<^sub>R x) \ e"
      by (simp add: dist_norm algebra_simps)
    then show False
      using zne [OF in01 e [THEN subsetD]] by (simp add: \<open>y \<in> T\<close> hull_inc mem_affine x)
  qed
  show ?thesis
  proof (rule subset_antisym)
    show "T \ affine hull T \ S"
      using assms by (simp add: hull_subset face_of_imp_subset)
    show "affine hull T \ S \ T"
      using "*" \<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)
      apply (rule_tac x="e / (e + norm (b - c))" in image_eqI)
      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 = {}"
  using assms face_of_disjoint_rel_interior interior_subset_rel_interior by fastforce

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

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

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

lemma subset_of_face_of_affine_hull:
    fixes S :: "'a::euclidean_space set"
  assumes T: "T face_of S" and "convex S" "U \ S" and dis: "\ disjnt (affine hull T) (rel_interior U)"
  shows "U \ T"
proof (rule subset_of_face_of [OF T \<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 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 (meson antisym assms disjnt_def equalityD2 face_of_def subset_of_face_of_affine_hull)

lemma affine_diff_divide:
    assumes "affine S" "k \ 0" "k \ 1" and xy: "x \ S" "y /\<^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_conic:
  assumes "conic S" "f face_of S"
  shows "conic f"
  unfolding conic_def
proof (intro strip)
  fix x and c::real
  assume "x \ f" and "0 \ c"
  have f: "\a b x. \a \ S; b \ S; x \ f; x \ open_segment a b\ \ a \ f \ b \ f"
    using \<open>f face_of S\<close> face_ofD by blast
  show "c *\<^sub>R x \ f"
  proof (cases "x=0 \ c=1")
    case True
    then show ?thesis
      using \<open>x \<in> f\<close> by auto
  next
    case False
    with \<open>0 \<le> c\<close> obtain d e where de: "0 \<le> d" "0 \<le> e" "d < 1" "1 < e" "d < e" "(d = c \<or> e = c)"
      apply (simp add: neq_iff)
      by (metis gt_ex less_eq_real_def order_less_le_trans zero_less_one)
    then obtain [simp]: "c *\<^sub>R x \ S" "e *\<^sub>R x \ S" \x \ S\
      using \<open>x \<in> f\<close> assms conic_mul face_of_imp_subset by blast
    have "x \ open_segment (d *\<^sub>R x) (e *\<^sub>R x)" if "c *\<^sub>R x \ f"
      using de False that
      apply (simp add: in_segment)
      apply (rule_tac x="(1 - d) / (e - d)" in exI)
      apply (simp add: field_simps)
      by (smt (verit, del_insts) add_divide_distrib divide_self scaleR_collapse)
    then show ?thesis
      using \<open>conic S\<close> f [of "d *\<^sub>R x" "e *\<^sub>R x" x] de \<open>x \<in> f\<close>
      by (force simp: conic_def in_segment)
  qed
qed

proposition face_of_convex_hulls:
      assumes S: "finite S" "T \ S" and disj: "affine hull T \ convex hull (S - T) = {}"
      shows  "(convex hull T) face_of (convex hull S)"
proof -
  have fin: "finite T" "finite (S - T)" using assms
    by (auto simp: finite_subset)
  have *: "x \ convex hull T"
          if x: "x \ convex hull S" and y: "y \ convex hull S" and w: "w \ convex hull T" "w \ open_segment x y"
          for x y w
  proof -
    have waff: "w \ affine hull T"
      using convex_hull_subset_affine_hull w by blast
    obtain a b where a: "\i. i \ S \ 0 \ a i" and asum: "sum a S = 1" and aeqx: "(\i\S. a i *\<^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  "sum a T = 1"
        using assms by (metis sum.mono_neutral_cong_right a0 asum)
      moreover have "(\x\T. a x *\<^sub>R x) = x"
        using a0 assms by (auto simp: cge0 a aeqx [symmetric] sum.mono_neutral_right)
      ultimately show ?thesis
        using a assms(2) by (auto simp add: convex_hull_finite \<open>finite T\<close> )
    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 "sum c (S - T) = 1"
          by (simp add: S sum_diff sumc1)
        moreover 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 "(\i\S-T. c i *\<^sub>R i) = w"
          by (simp add: weq_sumsum)
        ultimately have "w \ convex hull (S - T)"
          using cge0 by (auto simp add: convex_hull_finite fin)
        then show ?thesis
          using disj waff by blast
      next
        case False
        then have sumcf: "sum c T = 1 - k"
          by (simp add: S k_def sum_diff sumc1)
        have "\x. x \ T \ 0 \ inverse (1 - k) * c x"
          by (metis \<open>T \<subseteq> S\<close> cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg subsetD sum_nonneg sumcf)
        moreover have "(\x\T. inverse (1 - k) * c x) = 1"
          by (metis False eq_iff_diff_eq_0 mult.commute right_inverse sum_distrib_left sumcf)
        ultimately have "(\i\T. c i *\<^sub>R i) /\<^sub>R (1 - k) \ convex hull T"
          apply (simp add: convex_hull_finite fin)
          by (metis (mono_tags, lifting) scaleR_right.sum scaleR_scaleR sum.cong)
        with \<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 simp flip: sum_distrib_left k_def)
          done
        ultimately show ?thesis
          using disj by blast
      qed
    qed
  qed
  have [simp]: "convex hull T \ convex hull S"
    by (simp add: \<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 \ open_segment (2 *\<^sub>R a - b) b"
        by (metis diff_add_cancel inverse_eq_divide midpoint_def midpoint_in_open_segment
            scaleR_2 scaleR_half_double)
      moreover have "2 *\<^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 \ \n. ((\r. insert (c r) r)^^n) {c{}}"
  note d_def [simp]
  have dSuc: "\n. d (Suc n) = insert (c (d n)) (d n)"
    by simp
  have dn_notempty: "d n \ {}" for n
    by (induction n) auto
  have dn_le_Suc: "d n \ T \ finite(d n) \ card(d n) \ Suc n" if "n \ DIM('a) + 2" for n
  using that
  proof (induction n)
    case 0
    then show ?case by (simp add: c)
  next
    case (Suc n)
    then show ?case by (auto simp: c card_insert_if)
  qed
  have aff_dim_le: "aff_dim(\(d n)) \ DIM('a) - int n" if "n \ DIM('a) + 2" for n
  using that
  proof (induction n)
    case 0
    then show ?case
      by (simp add: aff_dim_le_DIM)
  next
    case (Suc n)
    have fs: "\(d (Suc n)) face_of S"
      by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE)
    have condn: "convex (\(d n))"
      using Suc.prems nat_le_linear not_less_eq_eq
      by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc)
    have fdn: "\(d (Suc n)) face_of \(d n)"
      by (metis (no_types, lifting) Inter_anti_mono Suc.prems dSuc cfaI dn_le_Suc dn_notempty face_of_Inter face_of_imp_subset face_of_subset subset_iff subset_insertI)
    have ne: "\(d (Suc n)) \ \(d n)"
      by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans)
    have *: "\m::int. \d. \d'::int. d < d' \ d' \ m - n \ d \ m - of_nat(n+1)"
      by arith
    have "aff_dim (\(d (Suc n))) < aff_dim (\(d n))"
      by (rule face_of_aff_dim_lt [OF condn fdn ne])
    moreover have "aff_dim (\(d n)) \ int (DIM('a)) - int n"
      using Suc by auto
    ultimately
    have "aff_dim (\(d (Suc n))) \ int (DIM('a)) - (n+1)" by arith
    then show ?case by linarith
  qed
  have "aff_dim (\(d (DIM('a) + 2))) \ -2"
      using aff_dim_le [OF order_refl] by simp
  with aff_dim_geq [of "\(d (DIM('a) + 2))"] show ?thesis
    using order.trans by fastforce
next
  case False
  then show ?thesis by fastforce
qed

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

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

corollary face_of_Times_decomp:
    fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
    shows "C face_of (S \ S') \ (\F F'. F face_of S \ F' face_of S' \ C = F \ F')"
     (is "?lhs = ?rhs")
proof
  assume C: ?lhs
  show ?rhs
  proof (cases "C = {}")
    case True then show ?thesis by auto
  next
    case False
    have 1: "fst ` C \ S" "snd ` C \ S'"
      using C face_of_imp_subset by fastforce+
    have "convex C"
      using C by (metis face_of_imp_convex)
    have conv: "convex (fst ` C)" "convex (snd ` C)"
      by (simp_all add: \<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
qed (use face_of_Times in auto)

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

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

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

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

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

subsection\<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 \<open>(exposed'_face'_of)\<close> 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"
proof -
  have "S \ {x. 0 \ x \ 1} \ {} = S \ {x. 0 \ x = 1}"
    by force
  then show ?thesis
    using exposed_face_of_def by blast
qed

lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \ convex S"
proof
  assume S: "convex S"
  have "S \ {x. 0 \ x \ 0} \ S = S \ {x. 0 \ x = 0}"
    by auto
  with S show "S exposed_face_of S"
    using exposed_face_of_def face_of_refl_eq by blast
qed (simp add: exposed_face_of_def face_of_refl_eq)

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

lemma exposed_face_of:
    "T exposed_face_of S \
     T face_of S \<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}))"
     (is "?lhs = ?rhs")
proof
  show "?lhs \ ?rhs"
    by (smt (verit) Collect_cong exposed_face_of_def hyperplane_eq_empty inf.absorb_iff1
                    inf_bot_right inner_zero_left)
  show "?rhs \ ?lhs"
    using exposed_face_of_def face_of_imp_convex by fastforce
qed

lemma exposed_face_of_Int_supporting_hyperplane_le:
  "\convex S; \x. x \ S \ a \ x \ b\ \ (S \ {x. a \ x = b}) exposed_face_of S"
  by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)

lemma exposed_face_of_Int_supporting_hyperplane_ge:
  "\convex S; \x. x \ S \ a \ x \ b\ \ (S \ {x. a \ x = b}) exposed_face_of S"
  using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp

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

proposition exposed_face_of_Inter:
    fixes P :: "'a::euclidean_space set set"
  assumes "P \ {}"
      and "\T. T \ P \ T exposed_face_of S"
    shows "\P exposed_face_of S"
proof -
  obtain Q where "finite Q" and QsubP: "Q \ P" "card Q \ DIM('a) + 2" and IntQ: "\Q = \P"
    using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of]
    by force
  show ?thesis
  proof (cases "Q = {}")
    case True then show ?thesis
      by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv)
  next
    case False
    have "Q \ {T. T exposed_face_of S}"
      using QsubP assms by blast
    moreover have "Q \ {T. T exposed_face_of S} \ \Q exposed_face_of S"
      using \<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"
        by (smt (verit, best) z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close> inner_right_distrib lez)
      then show ?thesis
        using feq by blast
    qed
    ultimately have "F = {x + y |x y. x \ S \ {x. u \ x = u \ a0} \ y \ T \ {x. u \ x = u \ b0}}"
      by blast
    then show ?thesis
      by (rule that [OF sef tef])
  qed
qed

proposition exposed_face_of_parallel:
   "T exposed_face_of S \
         T face_of S \<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 \<open>(extreme'_point'_of)\<close> 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"
  using assms extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior by fastforce

lemma extreme_point_of_face:
     "F face_of S \ v extreme_point_of F \ v extreme_point_of S \ v \ F"
  by (meson empty_subsetI face_of_face face_of_singleton insert_subset)

lemma extreme_point_of_convex_hull:
  "x extreme_point_of (convex hull S) \ x \ S"
  using hull_minimal [of S "(convex hull S) - {x}" convex]
  using hull_subset [of S convex]
  by (force simp add: extreme_point_of_stillconvex)

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

lemma extreme_point_of_empty [simp]: "\ (x extreme_point_of {})"
  by (simp add: extreme_point_of_def)

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

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

lemma extreme_points_of_translation:
   "{x. x extreme_point_of (image (\x. a + x) S)} =
    (\<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>)

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

subsection\<open>Facets\<close>

definition\<^marker>\<open>tag important\<close> facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
                    (infixr \<open>(facet'_of)\<close> 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 \<open>(edge'_of)\<close> 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"
    using \<open>convex S\<close> extreme_point_of_stillconvex subset_hull by fastforce
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"
  by (simp add: extreme_point_of_convex_hull_affine_independent)

lemma extreme_point_of_segment:
  fixes x :: "'a::euclidean_space"
  shows "x extreme_point_of closed_segment a b \ x = a \ x = b"
  by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)

lemma face_of_convex_hull_subset:
  fixes S :: "'a::euclidean_space set"
  assumes "compact S" and T: "T face_of (convex hull S)"
  obtains S' where "S' \<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}"
    by (metis Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull
        face_of_imp_compact face_of_imp_convex)
qed

lemma face_of_convex_hull_aux:
  assumes eq: "x *\<^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
--> --------------------

--> maximum size reached

--> --------------------

quality97%

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.