Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
authorhoelzl
Thu Dec 02 16:45:28 2010 +0100 (2010-12-02)
changeset 40887ee8d0548c148
parent 40886 3c45d6753fd0
child 40890 29a45797e269
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
src/HOL/Library/Set_Algebras.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Set_Algebras.thy	Thu Dec 02 16:39:15 2010 +0100
     1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Thu Dec 02 16:45:28 2010 +0100
     1.3 @@ -354,4 +354,51 @@
     1.4      - a : (- 1) *o C"
     1.5    by (auto simp add: elt_set_times_def)
     1.6  
     1.7 +lemma set_plus_image:
     1.8 +  fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
     1.9 +  unfolding set_plus_def by (fastsimp simp: image_iff)
    1.10 +
    1.11 +lemma set_setsum_alt:
    1.12 +  assumes fin: "finite I"
    1.13 +  shows "setsum_set S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
    1.14 +    (is "_ = ?setsum I")
    1.15 +using fin proof induct
    1.16 +  case (insert x F)
    1.17 +  have "setsum_set S (insert x F) = S x \<oplus> ?setsum F"
    1.18 +    using insert.hyps by auto
    1.19 +  also have "...= {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
    1.20 +    unfolding set_plus_def
    1.21 +  proof safe
    1.22 +    fix y s assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
    1.23 +    then show "\<exists>s'. y + setsum s F = s' x + setsum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)"
    1.24 +      using insert.hyps
    1.25 +      by (intro exI[of _ "\<lambda>i. if i \<in> F then s i else y"]) (auto simp add: set_plus_def)
    1.26 +  qed auto
    1.27 +  finally show ?case
    1.28 +    using insert.hyps by auto
    1.29 +qed auto
    1.30 +
    1.31 +lemma setsum_set_cond_linear:
    1.32 +  fixes f :: "('a::comm_monoid_add) set \<Rightarrow> ('b::comm_monoid_add) set"
    1.33 +  assumes [intro!]: "\<And>A B. P A  \<Longrightarrow> P B  \<Longrightarrow> P (A \<oplus> B)" "P {0}"
    1.34 +    and f: "\<And>A B. P A  \<Longrightarrow> P B \<Longrightarrow> f (A \<oplus> B) = f A \<oplus> f B" "f {0} = {0}"
    1.35 +  assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)"
    1.36 +  shows "f (setsum_set S I) = setsum_set (f \<circ> S) I"
    1.37 +proof cases
    1.38 +  assume "finite I" from this all show ?thesis
    1.39 +  proof induct
    1.40 +    case (insert x F)
    1.41 +    from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum_set S F)"
    1.42 +      by induct auto
    1.43 +    with insert show ?case
    1.44 +      by (simp, subst f) auto
    1.45 +  qed (auto intro!: f)
    1.46 +qed (auto intro!: f)
    1.47 +
    1.48 +lemma setsum_set_linear:
    1.49 +  fixes f :: "('a::comm_monoid_add) set => ('b::comm_monoid_add) set"
    1.50 +  assumes "\<And>A B. f(A) \<oplus> f(B) = f(A \<oplus> B)" "f {0} = {0}"
    1.51 +  shows "f (setsum_set S I) = setsum_set (f \<circ> S) I"
    1.52 +  using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
    1.53 +
    1.54  end
     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Dec 02 16:39:15 2010 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Dec 02 16:45:28 2010 +0100
     2.3 @@ -1,11 +1,12 @@
     2.4  (*  Title:      HOL/Library/Convex_Euclidean_Space.thy
     2.5      Author:     Robert Himmelmann, TU Muenchen
     2.6 +    Author:     Bogdan Grechuk, University of Edinburgh
     2.7  *)
     2.8  
     2.9  header {* Convex sets, functions and related things. *}
    2.10  
    2.11  theory Convex_Euclidean_Space
    2.12 -imports Topology_Euclidean_Space Convex
    2.13 +imports Topology_Euclidean_Space Convex Set_Algebras
    2.14  begin
    2.15  
    2.16  
    2.17 @@ -5419,4 +5420,225 @@
    2.18  from this show ?thesis using `?lhs<=?rhs` by auto
    2.19  qed
    2.20  
    2.21 +subsection {* Convexity on direct sums *}
    2.22 +
    2.23 +lemma closure_sum:
    2.24 +  fixes S T :: "('n::euclidean_space) set"
    2.25 +  shows "closure S \<oplus> closure T \<subseteq> closure (S \<oplus> T)"
    2.26 +proof-
    2.27 +  have "(closure S) \<oplus> (closure T) = (\<lambda>(x,y). x + y) ` (closure S \<times> closure T)"
    2.28 +    by (simp add: set_plus_image)
    2.29 +  also have "... = (\<lambda>(x,y). x + y) ` closure (S \<times> T)"
    2.30 +    using closure_direct_sum by auto
    2.31 +  also have "... \<subseteq> closure (S \<oplus> T)"
    2.32 +    using fst_snd_linear closure_linear_image[of "(\<lambda>(x,y). x + y)" "S \<times> T"]
    2.33 +    by (auto simp: set_plus_image)
    2.34 +  finally show ?thesis
    2.35 +    by auto
    2.36 +qed
    2.37 +
    2.38 +lemma convex_oplus:
    2.39 +fixes S T :: "('n::euclidean_space) set"
    2.40 +assumes "convex S" "convex T"
    2.41 +shows "convex (S \<oplus> T)"
    2.42 +proof-
    2.43 +have "{x + y |x y. x : S & y : T} = {c. EX a:S. EX b:T. c = a + b}" by auto
    2.44 +thus ?thesis unfolding set_plus_def using convex_sums[of S T] assms by auto
    2.45 +qed
    2.46 +
    2.47 +lemma convex_hull_sum:
    2.48 +fixes S T :: "('n::euclidean_space) set"
    2.49 +shows "convex hull (S \<oplus> T) = (convex hull S) \<oplus> (convex hull T)"
    2.50 +proof-
    2.51 +have "(convex hull S) \<oplus> (convex hull T) =
    2.52 +      (%z. fst z + snd z) ` ((convex hull S) <*> (convex hull T))"
    2.53 +   by (simp add: set_plus_image)
    2.54 +also have "... = (%z. fst z + snd z) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
    2.55 +also have "...= convex hull (S \<oplus> T)" using fst_snd_linear linear_conv_bounded_linear
    2.56 +   convex_hull_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
    2.57 +finally show ?thesis by auto
    2.58 +qed
    2.59 +
    2.60 +lemma rel_interior_sum:
    2.61 +fixes S T :: "('n::euclidean_space) set"
    2.62 +assumes "convex S" "convex T"
    2.63 +shows "rel_interior (S \<oplus> T) = (rel_interior S) \<oplus> (rel_interior T)"
    2.64 +proof-
    2.65 +have "(rel_interior S) \<oplus> (rel_interior T) = (%z. fst z + snd z) ` (rel_interior S <*> rel_interior T)"
    2.66 +   by (simp add: set_plus_image)
    2.67 +also have "... = (%z. fst z + snd z) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
    2.68 +also have "...= rel_interior (S \<oplus> T)" using fst_snd_linear convex_direct_sum assms
    2.69 +   rel_interior_convex_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
    2.70 +finally show ?thesis by auto
    2.71 +qed
    2.72 +
    2.73 +lemma convex_sum_gen:
    2.74 +  fixes S :: "'a \<Rightarrow> 'n::euclidean_space set"
    2.75 +  assumes "\<And>i. i \<in> I \<Longrightarrow> (convex (S i))"
    2.76 +  shows "convex (setsum_set S I)"
    2.77 +proof cases
    2.78 +  assume "finite I" from this assms show ?thesis
    2.79 +    by induct (auto simp: convex_oplus)
    2.80 +qed auto
    2.81 +
    2.82 +lemma convex_hull_sum_gen:
    2.83 +fixes S :: "'a => ('n::euclidean_space) set"
    2.84 +shows "convex hull (setsum_set S I) = setsum_set (%i. (convex hull (S i))) I"
    2.85 +apply (subst setsum_set_linear) using convex_hull_sum convex_hull_singleton by auto
    2.86 +
    2.87 +
    2.88 +lemma rel_interior_sum_gen:
    2.89 +fixes S :: "'a => ('n::euclidean_space) set"
    2.90 +assumes "!i:I. (convex (S i))"
    2.91 +shows "rel_interior (setsum_set S I) = setsum_set (%i. (rel_interior (S i))) I"
    2.92 +apply (subst setsum_set_cond_linear[of convex])
    2.93 +  using rel_interior_sum rel_interior_sing[of "0"] assms by (auto simp add: convex_oplus)
    2.94 +
    2.95 +lemma convex_rel_open_direct_sum:
    2.96 +fixes S T :: "('n::euclidean_space) set"
    2.97 +assumes "convex S" "rel_open S" "convex T" "rel_open T"
    2.98 +shows "convex (S <*> T) & rel_open (S <*> T)"
    2.99 +by (metis assms convex_direct_sum rel_interior_direct_sum rel_open_def)
   2.100 +
   2.101 +lemma convex_rel_open_sum:
   2.102 +fixes S T :: "('n::euclidean_space) set"
   2.103 +assumes "convex S" "rel_open S" "convex T" "rel_open T"
   2.104 +shows "convex (S \<oplus> T) & rel_open (S \<oplus> T)"
   2.105 +by (metis assms convex_oplus rel_interior_sum rel_open_def)
   2.106 +
   2.107 +lemma convex_hull_finite_union_cones:
   2.108 +assumes "finite I" "I ~= {}"
   2.109 +assumes "!i:I. (convex (S i) & cone (S i) & (S i) ~= {})"
   2.110 +shows "convex hull (Union (S ` I)) = setsum_set S I"
   2.111 +  (is "?lhs = ?rhs")
   2.112 +proof-
   2.113 +{ fix x assume "x : ?lhs"
   2.114 +  from this obtain c xs where x_def: "x=setsum (%i. c i *\<^sub>R xs i) I &
   2.115 +     (!i:I. c i >= 0) & (setsum c I = 1) & (!i:I. xs i : S i)"
   2.116 +     using convex_hull_finite_union[of I S] assms by auto
   2.117 +  def s == "(%i. c i *\<^sub>R xs i)"
   2.118 +  { fix i assume "i:I"
   2.119 +    hence "s i : S i" using s_def x_def assms mem_cone[of "S i" "xs i" "c i"] by auto
   2.120 +  } hence "!i:I. s i : S i" by auto
   2.121 +  moreover have "x = setsum s I" using x_def s_def by auto
   2.122 +  ultimately have "x : ?rhs" using set_setsum_alt[of I S] assms by auto
   2.123 +}
   2.124 +moreover
   2.125 +{ fix x assume "x : ?rhs"
   2.126 +  from this obtain s where x_def: "x=setsum s I & (!i:I. s i : S i)"
   2.127 +     using set_setsum_alt[of I S] assms by auto
   2.128 +  def xs == "(%i. of_nat(card I) *\<^sub>R s i)"
   2.129 +  hence "x=setsum (%i. ((1 :: real)/of_nat(card I)) *\<^sub>R xs i) I" using x_def assms by auto
   2.130 +  moreover have "!i:I. xs i : S i" using x_def xs_def assms by (simp add: cone_def)
   2.131 +  moreover have "(!i:I. (1 :: real)/of_nat(card I) >= 0)" by auto
   2.132 +  moreover have "setsum (%i. (1 :: real)/of_nat(card I)) I = 1" using assms by auto
   2.133 +  ultimately have "x : ?lhs" apply (subst convex_hull_finite_union[of I S])
   2.134 +    using assms apply blast
   2.135 +    using assms apply blast
   2.136 +    apply rule apply (rule_tac x="(%i. (1 :: real)/of_nat(card I))" in exI) by auto
   2.137 +} ultimately show ?thesis by auto
   2.138 +qed
   2.139 +
   2.140 +lemma convex_hull_union_cones_two:
   2.141 +fixes S T :: "('m::euclidean_space) set"
   2.142 +assumes "convex S" "cone S" "S ~= {}"
   2.143 +assumes "convex T" "cone T" "T ~= {}"
   2.144 +shows "convex hull (S Un T) = S \<oplus> T"
   2.145 +proof-
   2.146 +def I == "{(1::nat),2}"
   2.147 +def A == "(%i. (if i=(1::nat) then S else T))"
   2.148 +have "Union (A ` I) = S Un T" using A_def I_def by auto
   2.149 +hence "convex hull (Union (A ` I)) = convex hull (S Un T)" by auto
   2.150 +moreover have "convex hull Union (A ` I) = setsum_set A I"
   2.151 +    apply (subst convex_hull_finite_union_cones[of I A]) using assms A_def I_def by auto
   2.152 +moreover have
   2.153 +  "setsum_set A I = S \<oplus> T" using A_def I_def
   2.154 +     unfolding set_plus_def apply auto unfolding set_plus_def by auto
   2.155 +ultimately show ?thesis by auto
   2.156 +qed
   2.157 +
   2.158 +lemma rel_interior_convex_hull_union:
   2.159 +fixes S :: "'a => ('n::euclidean_space) set"
   2.160 +assumes "finite I"
   2.161 +assumes "!i:I. convex (S i) & (S i) ~= {}"
   2.162 +shows "rel_interior (convex hull (Union (S ` I))) =  {setsum (%i. c i *\<^sub>R s i) I
   2.163 +       |c s. (!i:I. c i > 0) & (setsum c I = 1) & (!i:I. s i : rel_interior(S i))}"
   2.164 +(is "?lhs=?rhs")
   2.165 +proof-
   2.166 +{ assume "I={}" hence ?thesis using convex_hull_empty rel_interior_empty by auto }
   2.167 +moreover
   2.168 +{ assume "I ~= {}"
   2.169 +  def C0 == "convex hull (Union (S ` I))"
   2.170 +  have "!i:I. C0 >= S i" unfolding C0_def using hull_subset[of "Union (S ` I)"] by auto
   2.171 +  def K0 == "cone hull ({(1 :: real)} <*> C0)"
   2.172 +  def K == "(%i. cone hull ({(1 :: real)} <*> (S i)))"
   2.173 +  have "!i:I. K i ~= {}" unfolding K_def using assms by (simp add: cone_hull_empty_iff[symmetric])
   2.174 +  { fix i assume "i:I"
   2.175 +    hence "convex (K i)" unfolding K_def apply (subst convex_cone_hull) apply (subst convex_direct_sum)
   2.176 +    using assms by auto
   2.177 +  }
   2.178 +  hence convK: "!i:I. convex (K i)" by auto
   2.179 +  { fix i assume "i:I"
   2.180 +    hence "K0 >= K i" unfolding K0_def K_def apply (subst hull_mono) using `!i:I. C0 >= S i` by auto
   2.181 +  }
   2.182 +  hence "K0 >= Union (K ` I)" by auto
   2.183 +  moreover have "K0 : convex" unfolding mem_def K0_def
   2.184 +     apply (subst convex_cone_hull) apply (subst convex_direct_sum)
   2.185 +     unfolding C0_def using convex_convex_hull by auto
   2.186 +  ultimately have geq: "K0 >= convex hull (Union (K ` I))" using hull_minimal[of _ "K0" "convex"] by blast
   2.187 +  have "!i:I. K i >= {(1 :: real)} <*> (S i)" using K_def by (simp add: hull_subset)
   2.188 +  hence "Union (K ` I) >= {(1 :: real)} <*> Union (S ` I)" by auto
   2.189 +  hence "convex hull Union (K ` I) >= convex hull ({(1 :: real)} <*> Union (S ` I))" by (simp add: hull_mono)
   2.190 +  hence "convex hull Union (K ` I) >= {(1 :: real)} <*> C0" unfolding C0_def
   2.191 +     using convex_hull_direct_sum[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto
   2.192 +  moreover have "convex hull(Union (K ` I)) : cone" unfolding mem_def apply (subst cone_convex_hull)
   2.193 +     using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull by auto
   2.194 +  ultimately have "convex hull (Union (K ` I)) >= K0"
   2.195 +     unfolding K0_def using hull_minimal[of _ "convex hull (Union (K ` I))" "cone"] by blast
   2.196 +  hence "K0 = convex hull (Union (K ` I))" using geq by auto
   2.197 +  also have "...=setsum_set K I"
   2.198 +     apply (subst convex_hull_finite_union_cones[of I K])
   2.199 +     using assms apply blast
   2.200 +     using `I ~= {}` apply blast
   2.201 +     unfolding K_def apply rule
   2.202 +     apply (subst convex_cone_hull) apply (subst convex_direct_sum)
   2.203 +     using assms cone_cone_hull `!i:I. K i ~= {}` K_def by auto
   2.204 +  finally have "K0 = setsum_set K I" by auto
   2.205 +  hence *: "rel_interior K0 = setsum_set (%i. (rel_interior (K i))) I"
   2.206 +     using rel_interior_sum_gen[of I K] convK by auto
   2.207 +  { fix x assume "x : ?lhs"
   2.208 +    hence "((1::real),x) : rel_interior K0" using K0_def C0_def
   2.209 +       rel_interior_convex_cone_aux[of C0 "(1::real)" x] convex_convex_hull by auto
   2.210 +    from this obtain k where k_def: "((1::real),x) = setsum k I & (!i:I. k i : rel_interior (K i))"
   2.211 +      using `finite I` * set_setsum_alt[of I "(%i. rel_interior (K i))"] by auto
   2.212 +    { fix i assume "i:I"
   2.213 +      hence "(convex (S i)) & k i : rel_interior (cone hull {1} <*> S i)" using k_def K_def assms by auto
   2.214 +      hence "EX ci si. k i = (ci, ci *\<^sub>R si) & 0 < ci & si : rel_interior (S i)"
   2.215 +         using rel_interior_convex_cone[of "S i"] by auto
   2.216 +    }
   2.217 +    from this obtain c s where cs_def: "!i:I. (k i = (c i, c i *\<^sub>R s i) & 0 < c i
   2.218 +          & s i : rel_interior (S i))" by metis
   2.219 +    hence "x = (SUM i:I. c i *\<^sub>R s i) & setsum c I = 1" using k_def by (simp add: setsum_prod)
   2.220 +    hence "x : ?rhs" using k_def apply auto
   2.221 +       apply (rule_tac x="c" in exI) apply (rule_tac x="s" in exI) using cs_def by auto
   2.222 +  }
   2.223 +  moreover
   2.224 +  { fix x assume "x : ?rhs"
   2.225 +    from this obtain c s where cs_def: "x=setsum (%i. c i *\<^sub>R s i) I &
   2.226 +       (!i:I. c i > 0) & (setsum c I = 1) & (!i:I. s i : rel_interior(S i))" by auto
   2.227 +    def k == "(%i. (c i, c i *\<^sub>R s i))"
   2.228 +    { fix i assume "i:I"
   2.229 +      hence "k i : rel_interior (K i)"
   2.230 +         using k_def K_def assms cs_def rel_interior_convex_cone[of "S i"] by auto
   2.231 +    }
   2.232 +    hence "((1::real),x) : rel_interior K0"
   2.233 +       using K0_def * set_setsum_alt[of I "(%i. rel_interior (K i))"] assms k_def cs_def
   2.234 +       apply auto apply (rule_tac x="k" in exI) by (simp add: setsum_prod)
   2.235 +    hence "x : ?lhs" using K0_def C0_def
   2.236 +       rel_interior_convex_cone_aux[of C0 "(1::real)" x] by (auto simp add: convex_convex_hull)
   2.237 +  }
   2.238 +  ultimately have ?thesis by blast
   2.239 +} ultimately show ?thesis by blast
   2.240 +qed
   2.241 +
   2.242  end