author hoelzl Thu Dec 02 16:45:28 2010 +0100 (2010-12-02) changeset 40887 ee8d0548c148 parent 40886 3c45d6753fd0 child 40890 29a45797e269
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
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.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.9  header {* Convex sets, functions and related things. *}
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.17 @@ -5419,4 +5420,225 @@
2.18  from this show ?thesis using `?lhs<=?rhs` by auto
2.19  qed
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.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.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.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.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.242  end