1.1 --- a/src/HOL/Library/Convex.thy Fri Sep 13 16:50:35 2013 +0200
1.2 +++ b/src/HOL/Library/Convex.thy Fri Sep 13 11:16:13 2013 -0700
1.3 @@ -244,7 +244,7 @@
1.4 lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
1.5 unfolding convex_on_def by auto
1.6
1.7 -lemma convex_add[intro]:
1.8 +lemma convex_on_add [intro]:
1.9 assumes "convex_on s f" "convex_on s g"
1.10 shows "convex_on s (\<lambda>x. f x + g x)"
1.11 proof -
1.12 @@ -262,7 +262,7 @@
1.13 then show ?thesis unfolding convex_on_def by auto
1.14 qed
1.15
1.16 -lemma convex_cmul[intro]:
1.17 +lemma convex_on_cmul [intro]:
1.18 assumes "0 \<le> (c::real)" "convex_on s f"
1.19 shows "convex_on s (\<lambda>x. c * f x)"
1.20 proof-
1.21 @@ -284,7 +284,7 @@
1.22 using assms unfolding convex_on_def by fastforce
1.23 qed
1.24
1.25 -lemma convex_distance[intro]:
1.26 +lemma convex_on_dist [intro]:
1.27 fixes s :: "'a::real_normed_vector set"
1.28 shows "convex_on s (\<lambda>x. dist a x)"
1.29 proof (auto simp add: convex_on_def dist_norm)
1.30 @@ -304,42 +304,47 @@
1.31
1.32 subsection {* Arithmetic operations on sets preserve convexity. *}
1.33
1.34 -lemma convex_scaling:
1.35 - assumes "convex s"
1.36 - shows"convex ((\<lambda>x. c *\<^sub>R x) ` s)"
1.37 - using assms unfolding convex_def image_iff
1.38 -proof safe
1.39 - fix x xa y xb :: "'a::real_vector"
1.40 - fix u v :: real
1.41 - assume asm: "\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s"
1.42 - "xa \<in> s" "xb \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1"
1.43 - show "\<exists>x\<in>s. u *\<^sub>R c *\<^sub>R xa + v *\<^sub>R c *\<^sub>R xb = c *\<^sub>R x"
1.44 - using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by (auto simp add: algebra_simps)
1.45 +lemma convex_linear_image:
1.46 + assumes "linear f" and "convex s" shows "convex (f ` s)"
1.47 +proof -
1.48 + interpret f: linear f by fact
1.49 + from `convex s` show "convex (f ` s)"
1.50 + by (simp add: convex_def f.scaleR [symmetric] f.add [symmetric])
1.51 qed
1.52
1.53 -lemma convex_negations: "convex s \<Longrightarrow> convex ((\<lambda>x. -x)` s)"
1.54 - using assms unfolding convex_def image_iff
1.55 -proof safe
1.56 - fix x xa y xb :: "'a::real_vector"
1.57 - fix u v :: real
1.58 - assume asm: "\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s"
1.59 - "xa \<in> s" "xb \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1"
1.60 - show "\<exists>x\<in>s. u *\<^sub>R - xa + v *\<^sub>R - xb = - x"
1.61 - using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by auto
1.62 +lemma convex_linear_vimage:
1.63 + assumes "linear f" and "convex s" shows "convex (f -` s)"
1.64 +proof -
1.65 + interpret f: linear f by fact
1.66 + from `convex s` show "convex (f -` s)"
1.67 + by (simp add: convex_def f.add f.scaleR)
1.68 +qed
1.69 +
1.70 +lemma convex_scaling:
1.71 + assumes "convex s" shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)"
1.72 +proof -
1.73 + have "linear (\<lambda>x. c *\<^sub>R x)" by (simp add: linearI scaleR_add_right)
1.74 + then show ?thesis using `convex s` by (rule convex_linear_image)
1.75 +qed
1.76 +
1.77 +lemma convex_negations:
1.78 + assumes "convex s" shows "convex ((\<lambda>x. - x) ` s)"
1.79 +proof -
1.80 + have "linear (\<lambda>x. - x)" by (simp add: linearI)
1.81 + then show ?thesis using `convex s` by (rule convex_linear_image)
1.82 qed
1.83
1.84 lemma convex_sums:
1.85 - assumes "convex s" "convex t"
1.86 + assumes "convex s" and "convex t"
1.87 shows "convex {x + y| x y. x \<in> s \<and> y \<in> t}"
1.88 - using assms unfolding convex_def image_iff
1.89 -proof safe
1.90 - fix xa xb ya yb
1.91 - assume xy:"xa\<in>s" "xb\<in>s" "ya\<in>t" "yb\<in>t"
1.92 - fix u v :: real
1.93 - assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
1.94 - show "\<exists>x y. u *\<^sub>R (xa + ya) + v *\<^sub>R (xb + yb) = x + y \<and> x \<in> s \<and> y \<in> t"
1.95 - using exI[of _ "u *\<^sub>R xa + v *\<^sub>R xb"] exI[of _ "u *\<^sub>R ya + v *\<^sub>R yb"]
1.96 - assms[unfolded convex_def] uv xy by (auto simp add:scaleR_right_distrib)
1.97 +proof -
1.98 + have "linear (\<lambda>(x, y). x + y)"
1.99 + by (auto intro: linearI simp add: scaleR_add_right)
1.100 + with assms have "convex ((\<lambda>(x, y). x + y) ` (s \<times> t))"
1.101 + by (intro convex_linear_image convex_Times)
1.102 + also have "((\<lambda>(x, y). x + y) ` (s \<times> t)) = {x + y| x y. x \<in> s \<and> y \<in> t}"
1.103 + by auto
1.104 + finally show ?thesis .
1.105 qed
1.106
1.107 lemma convex_differences:
1.108 @@ -347,17 +352,7 @@
1.109 shows "convex {x - y| x y. x \<in> s \<and> y \<in> t}"
1.110 proof -
1.111 have "{x - y| x y. x \<in> s \<and> y \<in> t} = {x + y |x y. x \<in> s \<and> y \<in> uminus ` t}"
1.112 - proof safe
1.113 - fix x x' y
1.114 - assume "x' \<in> s" "y \<in> t"
1.115 - then show "\<exists>x y'. x' - y = x + y' \<and> x \<in> s \<and> y' \<in> uminus ` t"
1.116 - using exI[of _ x'] exI[of _ "-y"] by auto
1.117 - next
1.118 - fix x x' y y'
1.119 - assume "x' \<in> s" "y' \<in> t"
1.120 - then show "\<exists>x y. x' + - y' = x - y \<and> x \<in> s \<and> y \<in> t"
1.121 - using exI[of _ x'] exI[of _ y'] by auto
1.122 - qed
1.123 + unfolding diff_def by auto
1.124 then show ?thesis
1.125 using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto
1.126 qed
1.127 @@ -380,21 +375,6 @@
1.128 using convex_translation[OF convex_scaling[OF assms], of a c] by auto
1.129 qed
1.130
1.131 -lemma convex_linear_image:
1.132 - assumes c:"convex s" and l:"bounded_linear f"
1.133 - shows "convex(f ` s)"
1.134 -proof (auto simp add: convex_def)
1.135 - interpret f: bounded_linear f by fact
1.136 - fix x y
1.137 - assume xy: "x \<in> s" "y \<in> s"
1.138 - fix u v :: real
1.139 - assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
1.140 - show "u *\<^sub>R f x + v *\<^sub>R f y \<in> f ` s" unfolding image_iff
1.141 - using bexI[of _ "u *\<^sub>R x + v *\<^sub>R y"] f.add f.scaleR
1.142 - c[unfolded convex_def] xy uv by auto
1.143 -qed
1.144 -
1.145 -
1.146 lemma pos_is_convex: "convex {0 :: real <..}"
1.147 unfolding convex_alt
1.148 proof safe
2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Sep 13 16:50:35 2013 +0200
2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Sep 13 11:16:13 2013 -0700
2.3 @@ -20,6 +20,9 @@
2.4 lemma linear_scaleR: "linear (\<lambda>x. scaleR c x)"
2.5 by (simp add: linear_iff scaleR_add_right)
2.6
2.7 +lemma linear_scaleR_left: "linear (\<lambda>r. scaleR r x)"
2.8 + by (simp add: linear_iff scaleR_add_left)
2.9 +
2.10 lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
2.11 by (simp add: inj_on_def)
2.12
2.13 @@ -1405,7 +1408,7 @@
2.14 assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
2.15 have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
2.16 using uv yz
2.17 - using convex_distance[of "ball x e" x, unfolded convex_on_def,
2.18 + using convex_on_dist [of "ball x e" x, unfolded convex_on_def,
2.19 THEN bspec[where x=y], THEN bspec[where x=z]]
2.20 by auto
2.21 then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e"
2.22 @@ -1423,7 +1426,7 @@
2.23 assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
2.24 have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
2.25 using uv yz
2.26 - using convex_distance[of "cball x e" x, unfolded convex_on_def,
2.27 + using convex_on_dist [of "cball x e" x, unfolded convex_on_def,
2.28 THEN bspec[where x=y], THEN bspec[where x=z]]
2.29 by auto
2.30 then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e"
2.31 @@ -1478,33 +1481,60 @@
2.32 subsubsection {* Convex hull is "preserved" by a linear function *}
2.33
2.34 lemma convex_hull_linear_image:
2.35 - assumes "bounded_linear f"
2.36 + assumes f: "linear f"
2.37 shows "f ` (convex hull s) = convex hull (f ` s)"
2.38 - apply rule
2.39 - unfolding subset_eq ball_simps
2.40 - apply (rule_tac[!] hull_induct, rule hull_inc)
2.41 - prefer 3
2.42 - apply (erule imageE)
2.43 - apply (rule_tac x=xa in image_eqI)
2.44 - apply assumption
2.45 - apply (rule hull_subset[unfolded subset_eq, rule_format])
2.46 - apply assumption
2.47 -proof -
2.48 - interpret f: bounded_linear f by fact
2.49 - show "convex {x. f x \<in> convex hull f ` s}"
2.50 - unfolding convex_def
2.51 - by (auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format])
2.52 - show "convex {x. x \<in> f ` (convex hull s)}"
2.53 - using convex_convex_hull[unfolded convex_def, of s]
2.54 - unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
2.55 -qed auto
2.56 +proof
2.57 + show "convex hull (f ` s) \<subseteq> f ` (convex hull s)"
2.58 + by (intro hull_minimal image_mono hull_subset convex_linear_image assms convex_convex_hull)
2.59 + show "f ` (convex hull s) \<subseteq> convex hull (f ` s)"
2.60 + proof (unfold image_subset_iff_subset_vimage, rule hull_minimal)
2.61 + show "s \<subseteq> f -` (convex hull (f ` s))"
2.62 + by (fast intro: hull_inc)
2.63 + show "convex (f -` (convex hull (f ` s)))"
2.64 + by (intro convex_linear_vimage [OF f] convex_convex_hull)
2.65 + qed
2.66 +qed
2.67
2.68 lemma in_convex_hull_linear_image:
2.69 - assumes "bounded_linear f"
2.70 + assumes "linear f"
2.71 and "x \<in> convex hull s"
2.72 shows "f x \<in> convex hull (f ` s)"
2.73 using convex_hull_linear_image[OF assms(1)] assms(2) by auto
2.74
2.75 +lemma convex_hull_Times:
2.76 + "convex hull (s \<times> t) = (convex hull s) \<times> (convex hull t)"
2.77 +proof
2.78 + show "convex hull (s \<times> t) \<subseteq> (convex hull s) \<times> (convex hull t)"
2.79 + by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull)
2.80 + have "\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)"
2.81 + proof (intro hull_induct)
2.82 + fix x y assume "x \<in> s" and "y \<in> t"
2.83 + then show "(x, y) \<in> convex hull (s \<times> t)"
2.84 + by (simp add: hull_inc)
2.85 + next
2.86 + fix x let ?S = "((\<lambda>y. (0, y)) -` (\<lambda>p. (- x, 0) + p) ` (convex hull s \<times> t))"
2.87 + have "convex ?S"
2.88 + by (intro convex_linear_vimage convex_translation convex_convex_hull,
2.89 + simp add: linear_iff)
2.90 + also have "?S = {y. (x, y) \<in> convex hull (s \<times> t)}"
2.91 + by (auto simp add: uminus_add_conv_diff image_def Bex_def)
2.92 + finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
2.93 + next
2.94 + show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
2.95 + proof (unfold Collect_ball_eq, rule convex_INT [rule_format])
2.96 + fix y let ?S = "((\<lambda>x. (x, 0)) -` (\<lambda>p. (0, - y) + p) ` (convex hull s \<times> t))"
2.97 + have "convex ?S"
2.98 + by (intro convex_linear_vimage convex_translation convex_convex_hull,
2.99 + simp add: linear_iff)
2.100 + also have "?S = {x. (x, y) \<in> convex hull (s \<times> t)}"
2.101 + by (auto simp add: uminus_add_conv_diff image_def Bex_def)
2.102 + finally show "convex {x. (x, y) \<in> convex hull (s \<times> t)}" .
2.103 + qed
2.104 + qed
2.105 + then show "(convex hull s) \<times> (convex hull t) \<subseteq> convex hull (s \<times> t)"
2.106 + unfolding subset_eq split_paired_Ball_Sigma .
2.107 +qed
2.108 +
2.109
2.110 subsubsection {* Stepping theorems for convex hulls of finite sets *}
2.111
2.112 @@ -5693,36 +5723,34 @@
2.113 apply auto
2.114 done
2.115
2.116 -(* FIXME: rewrite these lemmas without using vec1
2.117 -subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
2.118 +subsection {* On @{text "real"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
2.119
2.120 lemma is_interval_1:
2.121 - "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b \<longrightarrow> x \<in> s)"
2.122 - unfolding is_interval_def forall_1 by auto
2.123 -
2.124 -lemma is_interval_connected_1: "is_interval s \<longleftrightarrow> connected (s::(real^1) set)"
2.125 + "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
2.126 + unfolding is_interval_def by auto
2.127 +
2.128 +lemma is_interval_connected_1: "is_interval s \<longleftrightarrow> connected (s::real set)"
2.129 apply(rule, rule is_interval_connected, assumption) unfolding is_interval_1
2.130 apply(rule,rule,rule,rule,erule conjE,rule ccontr) proof-
2.131 - fix a b x assume as:"connected s" "a \<in> s" "b \<in> s" "dest_vec1 a \<le> dest_vec1 x" "dest_vec1 x \<le> dest_vec1 b" "x\<notin>s"
2.132 - hence *:"dest_vec1 a < dest_vec1 x" "dest_vec1 x < dest_vec1 b" apply(rule_tac [!] ccontr) unfolding not_less by auto
2.133 - let ?halfl = "{z. inner (basis 1) z < dest_vec1 x} " and ?halfr = "{z. inner (basis 1) z > dest_vec1 x} "
2.134 - { fix y assume "y \<in> s" have "y \<in> ?halfr \<union> ?halfl" apply(rule ccontr)
2.135 - using as(6) `y\<in>s` by (auto simp add: inner_vector_def) }
2.136 - moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: inner_vector_def)
2.137 + fix a b x assume as:"connected s" "a \<in> s" "b \<in> s" "a \<le> x" "x \<le> b" "x\<notin>s"
2.138 + hence *:"a < x" "x < b" unfolding not_le [symmetric] by auto
2.139 + let ?halfl = "{..<x} " and ?halfr = "{x<..} "
2.140 + { fix y assume "y \<in> s" with `x \<notin> s` have "x \<noteq> y" by auto
2.141 + then have "y \<in> ?halfr \<union> ?halfl" by auto }
2.142 + moreover have "a\<in>?halfl" "b\<in>?halfr" using * by auto
2.143 hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}" using as(2-3) by auto
2.144 ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]])
2.145 apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI)
2.146 - apply(rule, rule open_halfspace_lt, rule, rule open_halfspace_gt)
2.147 - by(auto simp add: field_simps) qed
2.148 + apply(rule, rule open_lessThan, rule, rule open_greaterThan)
2.149 + by auto qed
2.150
2.151 lemma is_interval_convex_1:
2.152 - "is_interval s \<longleftrightarrow> convex (s::(real^1) set)"
2.153 + "is_interval s \<longleftrightarrow> convex (s::real set)"
2.154 by(metis is_interval_convex convex_connected is_interval_connected_1)
2.155
2.156 lemma convex_connected_1:
2.157 - "connected s \<longleftrightarrow> convex (s::(real^1) set)"
2.158 + "connected s \<longleftrightarrow> convex (s::real set)"
2.159 by(metis is_interval_convex convex_connected is_interval_connected_1)
2.160 -*)
2.161
2.162
2.163 subsection {* Another intermediate value theorem formulation *}
2.164 @@ -5800,7 +5828,93 @@
2.165 qed
2.166
2.167 lemma inner_setsum_Basis[simp]: "i \<in> Basis \<Longrightarrow> (\<Sum>Basis) \<bullet> i = 1"
2.168 - by (simp add: One_def inner_setsum_left setsum_cases inner_Basis)
2.169 + by (simp add: inner_setsum_left setsum_cases inner_Basis)
2.170 +
2.171 +lemma convex_set_plus:
2.172 + assumes "convex s" and "convex t" shows "convex (s + t)"
2.173 +proof -
2.174 + have "convex {x + y |x y. x \<in> s \<and> y \<in> t}"
2.175 + using assms by (rule convex_sums)
2.176 + moreover have "{x + y |x y. x \<in> s \<and> y \<in> t} = s + t"
2.177 + unfolding set_plus_def by auto
2.178 + finally show "convex (s + t)" .
2.179 +qed
2.180 +
2.181 +lemma finite_set_setsum:
2.182 + assumes "finite A" and "\<forall>i\<in>A. finite (B i)" shows "finite (\<Sum>i\<in>A. B i)"
2.183 + using assms by (induct set: finite, simp, simp add: finite_set_plus)
2.184 +
2.185 +lemma set_setsum_eq:
2.186 + "finite A \<Longrightarrow> (\<Sum>i\<in>A. B i) = {\<Sum>i\<in>A. f i |f. \<forall>i\<in>A. f i \<in> B i}"
2.187 + apply (induct set: finite)
2.188 + apply simp
2.189 + apply simp
2.190 + apply (safe elim!: set_plus_elim)
2.191 + apply (rule_tac x="fun_upd f x a" in exI)
2.192 + apply simp
2.193 + apply (rule_tac f="\<lambda>x. a + x" in arg_cong)
2.194 + apply (rule setsum_cong [OF refl])
2.195 + apply clarsimp
2.196 + apply (fast intro: set_plus_intro)
2.197 + done
2.198 +
2.199 +lemma box_eq_set_setsum_Basis:
2.200 + shows "{x. \<forall>i\<in>Basis. x\<bullet>i \<in> B i} = (\<Sum>i\<in>Basis. image (\<lambda>x. x *\<^sub>R i) (B i))"
2.201 + apply (subst set_setsum_eq [OF finite_Basis])
2.202 + apply safe
2.203 + apply (fast intro: euclidean_representation [symmetric])
2.204 + apply (subst inner_setsum_left)
2.205 + apply (subgoal_tac "(\<Sum>x\<in>Basis. f x \<bullet> i) = f i \<bullet> i")
2.206 + apply (drule (1) bspec)
2.207 + apply clarsimp
2.208 + apply (frule setsum_diff1' [OF finite_Basis])
2.209 + apply (erule trans)
2.210 + apply simp
2.211 + apply (rule setsum_0')
2.212 + apply clarsimp
2.213 + apply (frule_tac x=i in bspec, assumption)
2.214 + apply (drule_tac x=x in bspec, assumption)
2.215 + apply clarsimp
2.216 + apply (cut_tac u=x and v=i in inner_Basis, assumption+)
2.217 + apply (rule ccontr)
2.218 + apply simp
2.219 + done
2.220 +
2.221 +lemma convex_hull_set_plus:
2.222 + "convex hull (s + t) = convex hull s + convex hull t"
2.223 + unfolding set_plus_image
2.224 + apply (subst convex_hull_linear_image [symmetric])
2.225 + apply (simp add: linear_iff scaleR_right_distrib)
2.226 + apply (simp add: convex_hull_Times)
2.227 + done
2.228 +
2.229 +lemma convex_hull_set_setsum:
2.230 + "convex hull (\<Sum>i\<in>A. B i) = (\<Sum>i\<in>A. convex hull (B i))"
2.231 +proof (cases "finite A")
2.232 + assume "finite A" then show ?thesis
2.233 + by (induct set: finite, simp, simp add: convex_hull_set_plus)
2.234 +qed simp
2.235 +
2.236 +lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
2.237 +proof -
2.238 + assume "bounded_linear f"
2.239 + then interpret f: bounded_linear f .
2.240 + show "linear f"
2.241 + by (simp add: f.add f.scaleR linear_iff)
2.242 +qed
2.243 +
2.244 +lemma convex_hull_eq_real_interval:
2.245 + fixes x y :: real assumes "x \<le> y"
2.246 + shows "convex hull {x, y} = {x..y}"
2.247 +proof (rule hull_unique)
2.248 + show "{x, y} \<subseteq> {x..y}" using `x \<le> y` by auto
2.249 + show "convex {x..y}" by (rule convex_interval)
2.250 +next
2.251 + fix s assume "{x, y} \<subseteq> s" and "convex s"
2.252 + then show "{x..y} \<subseteq> s"
2.253 + unfolding is_interval_convex_1 [symmetric] is_interval_def Basis_real_def
2.254 + by - (clarify, simp (no_asm_use), fast)
2.255 +qed
2.256
2.257 lemma unit_interval_convex_hull:
2.258 defines "One \<equiv> \<Sum>Basis"
2.259 @@ -5809,145 +5923,21 @@
2.260 proof -
2.261 have One[simp]: "\<And>i. i \<in> Basis \<Longrightarrow> One \<bullet> i = 1"
2.262 by (simp add: One_def inner_setsum_left setsum_cases inner_Basis)
2.263 - have 01: "{0,One} \<subseteq> convex hull ?points"
2.264 - apply rule
2.265 - apply (rule_tac hull_subset[unfolded subset_eq, rule_format])
2.266 - apply auto
2.267 - done
2.268 - {
2.269 - fix n x
2.270 - assume "x \<in> {0::'a::ordered_euclidean_space .. One}"
2.271 - "n \<le> DIM('a)" "card {i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0} \<le> n"
2.272 - then have "x \<in> convex hull ?points"
2.273 - proof (induct n arbitrary: x)
2.274 - case 0
2.275 - then have "x = 0"
2.276 - apply (subst euclidean_eq_iff)
2.277 - apply rule
2.278 - apply auto
2.279 - done
2.280 - then show "x\<in>convex hull ?points" using 01 by auto
2.281 - next
2.282 - case (Suc n)
2.283 - show "x\<in>convex hull ?points"
2.284 - proof (cases "{i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0} = {}")
2.285 - case True
2.286 - then have "x = 0"
2.287 - apply (subst euclidean_eq_iff)
2.288 - apply auto
2.289 - done
2.290 - then show "x\<in>convex hull ?points"
2.291 - using 01 by auto
2.292 - next
2.293 - case False
2.294 - def xi \<equiv> "Min ((\<lambda>i. x\<bullet>i) ` {i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0})"
2.295 - have "xi \<in> (\<lambda>i. x\<bullet>i) ` {i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0}"
2.296 - unfolding xi_def
2.297 - apply (rule Min_in)
2.298 - using False
2.299 - apply auto
2.300 - done
2.301 - then obtain i where i': "x\<bullet>i = xi" "x\<bullet>i \<noteq> 0" "i\<in>Basis"
2.302 - by auto
2.303 - have i: "\<And>j. j\<in>Basis \<Longrightarrow> x\<bullet>j > 0 \<Longrightarrow> x\<bullet>i \<le> x\<bullet>j"
2.304 - unfolding i'(1) xi_def
2.305 - apply (rule_tac Min_le)
2.306 - unfolding image_iff
2.307 - defer
2.308 - apply (rule_tac x=j in bexI)
2.309 - using i'
2.310 - apply auto
2.311 - done
2.312 - have i01: "x\<bullet>i \<le> 1" "x\<bullet>i > 0"
2.313 - using Suc(2)[unfolded mem_interval,rule_format,of i]
2.314 - using i'(2-) `x\<bullet>i \<noteq> 0`
2.315 - by auto
2.316 - show ?thesis
2.317 - proof (cases "x\<bullet>i = 1")
2.318 - case True
2.319 - have "\<forall>j\<in>{i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0}. x\<bullet>j = 1"
2.320 - apply rule
2.321 - apply (rule ccontr)
2.322 - unfolding mem_Collect_eq
2.323 - proof (erule conjE)
2.324 - fix j
2.325 - assume as: "x \<bullet> j \<noteq> 0" "x \<bullet> j \<noteq> 1" "j \<in> Basis"
2.326 - then have j: "x\<bullet>j \<in> {0<..<1}" using Suc(2)
2.327 - by (auto simp add: eucl_le[where 'a='a] elim!:allE[where x=j])
2.328 - then have "x\<bullet>j \<in> op \<bullet> x ` {i. i\<in>Basis \<and> x \<bullet> i \<noteq> 0}"
2.329 - using as(3) by auto
2.330 - then have "x\<bullet>j \<ge> x\<bullet>i"
2.331 - unfolding i'(1) xi_def
2.332 - apply (rule_tac Min_le)
2.333 - apply auto
2.334 - done
2.335 - then show False
2.336 - using True Suc(2) j
2.337 - by (auto simp add: elim!:ballE[where x=j])
2.338 - qed
2.339 - then show "x \<in> convex hull ?points"
2.340 - apply (rule_tac hull_subset[unfolded subset_eq, rule_format])
2.341 - apply auto
2.342 - done
2.343 - next
2.344 - let ?y = "\<Sum>j\<in>Basis. (if x\<bullet>j = 0 then 0 else (x\<bullet>j - x\<bullet>i) / (1 - x\<bullet>i)) *\<^sub>R j"
2.345 - case False
2.346 - then have *: "x = (x\<bullet>i) *\<^sub>R (\<Sum>j\<in>Basis. (if x\<bullet>j = 0 then 0 else 1) *\<^sub>R j) + (1 - x\<bullet>i) *\<^sub>R ?y"
2.347 - by (subst euclidean_eq_iff) (simp add: inner_simps)
2.348 - {
2.349 - fix j :: 'a
2.350 - assume j: "j \<in> Basis"
2.351 - have "x\<bullet>j \<noteq> 0 \<Longrightarrow> 0 \<le> (x \<bullet> j - x \<bullet> i) / (1 - x \<bullet> i)" "(x \<bullet> j - x \<bullet> i) / (1 - x \<bullet> i) \<le> 1"
2.352 - apply (rule_tac divide_nonneg_pos)
2.353 - using i(1)[of j]
2.354 - using False i01
2.355 - using Suc(2)[unfolded mem_interval, rule_format, of j]
2.356 - using j
2.357 - by (auto simp add: field_simps)
2.358 - with j have "0 \<le> ?y \<bullet> j \<and> ?y \<bullet> j \<le> 1"
2.359 - by (auto simp: inner_simps)
2.360 - }
2.361 - moreover have "i\<in>{j. j\<in>Basis \<and> x\<bullet>j \<noteq> 0} - {j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0}"
2.362 - using i01 using i'(3) by auto
2.363 - then have "{j. j\<in>Basis \<and> x\<bullet>j \<noteq> 0} \<noteq> {j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0}"
2.364 - using i'(3) by blast
2.365 - then have **: "{j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0} \<subset> {j. j\<in>Basis \<and> x\<bullet>j \<noteq> 0}"
2.366 - by auto
2.367 - have "card {j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0} \<le> n"
2.368 - using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto
2.369 - ultimately show ?thesis
2.370 - apply (subst *)
2.371 - apply (rule convex_convex_hull[unfolded convex_def, rule_format])
2.372 - apply (rule_tac hull_subset[unfolded subset_eq, rule_format])
2.373 - defer
2.374 - apply (rule Suc(1))
2.375 - unfolding mem_interval
2.376 - using i01 Suc(3)
2.377 - by auto
2.378 - qed
2.379 - qed
2.380 - qed
2.381 - } note * = this
2.382 - show ?thesis
2.383 - apply rule
2.384 - defer
2.385 - apply (rule hull_minimal)
2.386 - unfolding subset_eq
2.387 - prefer 3
2.388 - apply rule
2.389 - apply (rule_tac n2="DIM('a)" in *)
2.390 - prefer 3
2.391 - apply (rule card_mono)
2.392 - using 01 and convex_interval(1)
2.393 - prefer 5
2.394 - apply -
2.395 - apply rule
2.396 - unfolding mem_interval
2.397 - apply rule
2.398 - unfolding mem_Collect_eq
2.399 - apply (erule_tac x=i in ballE)
2.400 - apply auto
2.401 - done
2.402 + have "?int = {x. \<forall>i\<in>Basis. x \<bullet> i \<in> {0..1}}"
2.403 + by (auto simp add: eucl_le [where 'a='a])
2.404 + also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` {0..1})"
2.405 + by (simp only: box_eq_set_setsum_Basis)
2.406 + also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` (convex hull {0, 1}))"
2.407 + by (simp only: convex_hull_eq_real_interval zero_le_one)
2.408 + also have "\<dots> = (\<Sum>i\<in>Basis. convex hull ((\<lambda>x. x *\<^sub>R i) ` {0, 1}))"
2.409 + by (simp only: convex_hull_linear_image linear_scaleR_left)
2.410 + also have "\<dots> = convex hull (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` {0, 1})"
2.411 + by (simp only: convex_hull_set_setsum)
2.412 + also have "\<dots> = convex hull {x. \<forall>i\<in>Basis. x\<bullet>i \<in> {0, 1}}"
2.413 + by (simp only: box_eq_set_setsum_Basis)
2.414 + also have "convex hull {x. \<forall>i\<in>Basis. x\<bullet>i \<in> {0, 1}} = convex hull ?points"
2.415 + by simp
2.416 + finally show ?thesis .
2.417 qed
2.418
2.419 text {* And this is a finite set of vertices. *}
2.420 @@ -6201,8 +6191,7 @@
2.421 by auto
2.422
2.423 lemma convex_on_continuous:
2.424 - assumes "open (s::('a::ordered_euclidean_space) set)" "convex_on s f"
2.425 - (* FIXME: generalize to euclidean_space *)
2.426 + assumes "open (s::('a::euclidean_space) set)" "convex_on s f"
2.427 shows "continuous_on s f"
2.428 unfolding continuous_on_eq_continuous_at[OF assms(1)]
2.429 proof
2.430 @@ -6218,34 +6207,54 @@
2.431 apply auto
2.432 done
2.433 let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
2.434 - obtain c where c: "finite c" "{x - ?d..x + ?d} = convex hull c"
2.435 - using cube_convex_hull[OF `d>0`, of x] by auto
2.436 - have "x \<in> {x - ?d..x + ?d}"
2.437 - using `d > 0` unfolding mem_interval by (auto simp: inner_setsum_left_Basis inner_simps)
2.438 - then have "c \<noteq> {}" using c by auto
2.439 + obtain c
2.440 + where c: "finite c"
2.441 + and c1: "convex hull c \<subseteq> cball x e"
2.442 + and c2: "cball x d \<subseteq> convex hull c"
2.443 + proof
2.444 + def c \<equiv> "\<Sum>i\<in>Basis. (\<lambda>a. a *\<^sub>R i) ` {x\<bullet>i - d, x\<bullet>i + d}"
2.445 + show "finite c"
2.446 + unfolding c_def by (simp add: finite_set_setsum)
2.447 + have 1: "convex hull c = {a. \<forall>i\<in>Basis. a \<bullet> i \<in> {x \<bullet> i - d..x \<bullet> i + d}}"
2.448 + unfolding box_eq_set_setsum_Basis
2.449 + unfolding c_def convex_hull_set_setsum
2.450 + apply (subst convex_hull_linear_image [symmetric])
2.451 + apply (simp add: linear_iff scaleR_add_left)
2.452 + apply (rule setsum_cong [OF refl])
2.453 + apply (rule image_cong [OF _ refl])
2.454 + apply (rule convex_hull_eq_real_interval)
2.455 + apply (cut_tac `0 < d`, simp)
2.456 + done
2.457 + then have 2: "convex hull c = {a. \<forall>i\<in>Basis. a \<bullet> i \<in> cball (x \<bullet> i) d}"
2.458 + by (simp add: dist_norm abs_le_iff algebra_simps)
2.459 + show "cball x d \<subseteq> convex hull c"
2.460 + unfolding 2
2.461 + apply clarsimp
2.462 + apply (simp only: dist_norm)
2.463 + apply (subst inner_diff_left [symmetric])
2.464 + apply simp
2.465 + apply (erule (1) order_trans [OF Basis_le_norm])
2.466 + done
2.467 + have e': "e = (\<Sum>(i::'a)\<in>Basis. d)"
2.468 + by (simp add: d_def real_of_nat_def DIM_positive)
2.469 + show "convex hull c \<subseteq> cball x e"
2.470 + unfolding 2
2.471 + apply clarsimp
2.472 + apply (subst euclidean_dist_l2)
2.473 + apply (rule order_trans [OF setL2_le_setsum])
2.474 + apply (rule zero_le_dist)
2.475 + unfolding e'
2.476 + apply (rule setsum_mono)
2.477 + apply simp
2.478 + done
2.479 + qed
2.480 def k \<equiv> "Max (f ` c)"
2.481 - have "convex_on {x - ?d..x + ?d} f"
2.482 + have "convex_on (convex hull c) f"
2.483 apply(rule convex_on_subset[OF assms(2)])
2.484 apply(rule subset_trans[OF _ e(1)])
2.485 - unfolding subset_eq mem_cball
2.486 - proof
2.487 - fix z
2.488 - assume z: "z \<in> {x - ?d..x + ?d}"
2.489 - have e: "e = setsum (\<lambda>i::'a. d) Basis"
2.490 - unfolding setsum_constant d_def
2.491 - using dimge1
2.492 - unfolding real_eq_of_nat
2.493 - by auto
2.494 - show "dist x z \<le> e"
2.495 - unfolding dist_norm e
2.496 - apply (rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
2.497 - using z[unfolded mem_interval]
2.498 - apply (erule_tac x=b in ballE)
2.499 - apply (auto simp: inner_simps)
2.500 - done
2.501 - qed
2.502 - then have k: "\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k"
2.503 - unfolding c(2)
2.504 + apply(rule c1)
2.505 + done
2.506 + then have k: "\<forall>y\<in>convex hull c. f y \<le> k"
2.507 apply (rule_tac convex_on_convex_hull_bound)
2.508 apply assumption
2.509 unfolding k_def
2.510 @@ -6261,33 +6270,20 @@
2.511 apply (auto simp: real_of_nat_ge_one_iff Suc_le_eq DIM_positive)
2.512 done
2.513 then have dsube: "cball x d \<subseteq> cball x e"
2.514 - unfolding subset_eq Ball_def mem_cball by auto
2.515 + by (rule subset_cball)
2.516 have conv: "convex_on (cball x d) f"
2.517 apply (rule convex_on_subset)
2.518 apply (rule convex_on_subset[OF assms(2)])
2.519 apply (rule e(1))
2.520 - using dsube
2.521 - apply auto
2.522 + apply (rule dsube)
2.523 done
2.524 then have "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)"
2.525 - apply (rule_tac convex_bounds_lemma)
2.526 - apply assumption
2.527 - proof
2.528 - fix y
2.529 - assume y: "y \<in> cball x d"
2.530 - {
2.531 - fix i :: 'a
2.532 - assume "i \<in> Basis"
2.533 - then have "x \<bullet> i - d \<le> y \<bullet> i" "y \<bullet> i \<le> x \<bullet> i + d"
2.534 - using order_trans[OF Basis_le_norm y[unfolded mem_cball dist_norm], of i]
2.535 - by (auto simp: inner_diff_left)
2.536 - }
2.537 - then show "f y \<le> k"
2.538 - apply (rule_tac k[rule_format])
2.539 - unfolding mem_cball mem_interval dist_norm
2.540 - apply (auto simp: inner_simps)
2.541 - done
2.542 - qed
2.543 + apply (rule convex_bounds_lemma)
2.544 + apply (rule ballI)
2.545 + apply (rule k [rule_format])
2.546 + apply (erule rev_subsetD)
2.547 + apply (rule c2)
2.548 + done
2.549 then have "continuous_on (ball x d) f"
2.550 apply (rule_tac convex_on_bounded_continuous)
2.551 apply (rule open_ball, rule convex_on_subset[OF conv])
2.552 @@ -7147,7 +7143,7 @@
2.553 using fd linear_0 by auto
2.554 then have "(convex hull (insert 0 d)) = f ` (convex hull (insert 0 B))"
2.555 using convex_hull_linear_image[of f "(insert 0 d)"]
2.556 - convex_hull_linear_image[of f "(insert 0 B)"] `bounded_linear f`
2.557 + convex_hull_linear_image[of f "(insert 0 B)"] `linear f`
2.558 by auto
2.559 moreover have "rel_interior (f ` (convex hull insert 0 B)) =
2.560 f ` rel_interior (convex hull insert 0 B)"
2.561 @@ -8019,8 +8015,8 @@
2.562 by auto
2.563 then have "rel_interior (f ` S) = rel_interior (f ` rel_interior S)"
2.564 using assms convex_rel_interior
2.565 - linear_conv_bounded_linear[of f] convex_linear_image[of S]
2.566 - convex_linear_image[of "rel_interior S"]
2.567 + linear_conv_bounded_linear[of f] convex_linear_image[of _ S]
2.568 + convex_linear_image[of _ "rel_interior S"]
2.569 closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"]
2.570 by auto
2.571 then have "rel_interior (f ` S) \<subseteq> f ` rel_interior S"
2.572 @@ -8045,30 +8041,12 @@
2.573 }
2.574 then have "z \<in> rel_interior (f ` S)"
2.575 using convex_rel_interior_iff[of "f ` S" z] `convex S`
2.576 - `linear f` `S ~= {}` convex_linear_image[of S f] linear_conv_bounded_linear[of f]
2.577 + `linear f` `S ~= {}` convex_linear_image[of f S] linear_conv_bounded_linear[of f]
2.578 by auto
2.579 }
2.580 ultimately show ?thesis by auto
2.581 qed
2.582
2.583 -
2.584 -lemma convex_linear_preimage:
2.585 - assumes c: "convex S"
2.586 - and l: "bounded_linear f"
2.587 - shows "convex (f -` S)"
2.588 -proof (auto simp add: convex_def)
2.589 - interpret f: bounded_linear f by fact
2.590 - fix x y
2.591 - assume xy: "f x \<in> S" "f y \<in> S"
2.592 - fix u v :: real
2.593 - assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
2.594 - show "f (u *\<^sub>R x + v *\<^sub>R y) \<in> S"
2.595 - unfolding image_iff
2.596 - using bexI[of _ "u *\<^sub>R x + v *\<^sub>R y"] f.add f.scaleR c[unfolded convex_def] xy uv
2.597 - by auto
2.598 -qed
2.599 -
2.600 -
2.601 lemma rel_interior_convex_linear_preimage:
2.602 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
2.603 assumes "linear f"
2.604 @@ -8083,7 +8061,7 @@
2.605 then have "S \<inter> (range f) \<noteq> {}"
2.606 by auto
2.607 have conv: "convex (f -` S)"
2.608 - using convex_linear_preimage assms linear_conv_bounded_linear by auto
2.609 + using convex_linear_vimage assms by auto
2.610 then have "convex (S \<inter> range f)"
2.611 by (metis assms(1) assms(2) convex_Int subspace_UNIV subspace_imp_convex subspace_linear_image)
2.612 {
2.613 @@ -8134,112 +8112,6 @@
2.614 ultimately show ?thesis by auto
2.615 qed
2.616
2.617 -
2.618 -lemma convex_direct_sum:
2.619 - fixes S :: "'n::euclidean_space set"
2.620 - and T :: "'m::euclidean_space set"
2.621 - assumes "convex S"
2.622 - and "convex T"
2.623 - shows "convex (S \<times> T)"
2.624 -proof -
2.625 - {
2.626 - fix x
2.627 - assume "x \<in> S \<times> T"
2.628 - then obtain xs xt where xst: "xs \<in> S" "xt \<in> T" "(xs, xt) = x"
2.629 - by auto
2.630 - fix y assume "y \<in> S \<times> T"
2.631 - then obtain ys yt where yst: "ys \<in> S" "yt \<in> T" "(ys, yt) = y"
2.632 - by auto
2.633 - fix u v :: real assume uv: "u \<ge> 0 \<and> v \<ge> 0 \<and> u + v = 1"
2.634 - have "u *\<^sub>R x + v *\<^sub>R y = (u *\<^sub>R xs + v *\<^sub>R ys, u *\<^sub>R xt + v *\<^sub>R yt)"
2.635 - using xst yst by auto
2.636 - moreover have "u *\<^sub>R xs + v *\<^sub>R ys \<in> S"
2.637 - using uv xst yst convex_def[of S] assms by auto
2.638 - moreover have "u *\<^sub>R xt + v *\<^sub>R yt \<in> T"
2.639 - using uv xst yst convex_def[of T] assms by auto
2.640 - ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> S \<times> T" by auto
2.641 - }
2.642 - then show ?thesis
2.643 - unfolding convex_def by auto
2.644 -qed
2.645 -
2.646 -lemma convex_hull_direct_sum:
2.647 - fixes S :: "'n::euclidean_space set"
2.648 - and T :: "'m::euclidean_space set"
2.649 - shows "convex hull (S \<times> T) = (convex hull S) \<times> (convex hull T)"
2.650 -proof -
2.651 - {
2.652 - fix x
2.653 - assume "x \<in> (convex hull S) \<times> (convex hull T)"
2.654 - then obtain xs xt where xst: "xs \<in> convex hull S" "xt \<in> convex hull T" "(xs, xt) = x"
2.655 - by auto
2.656 - from xst obtain sI su where s: "finite sI" "sI \<subseteq> S" "\<forall>x\<in>sI. 0 \<le> su x"
2.657 - "setsum su sI = 1" "(\<Sum>v\<in>sI. su v *\<^sub>R v) = xs"
2.658 - using convex_hull_explicit[of S] by auto
2.659 - from xst obtain tI tu where t: "finite tI" "tI \<le> T" "\<forall>x\<in>tI. 0 \<le> tu x"
2.660 - "setsum tu tI = 1" "(\<Sum>v\<in>tI. tu v *\<^sub>R v) = xt"
2.661 - using convex_hull_explicit[of T] by auto
2.662 - def I \<equiv> "sI \<times> tI"
2.663 - def u \<equiv> "\<lambda>i. su (fst i) * tu (snd i)"
2.664 - have "fst (\<Sum>v\<in>sI \<times> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) =
2.665 - (\<Sum>vs\<in>sI. \<Sum>vt\<in>tI. (su vs * tu vt) *\<^sub>R vs)"
2.666 - using fst_setsum[of "(\<lambda>v. (su (fst v) * tu (snd v)) *\<^sub>R v)" "sI \<times> tI"]
2.667 - by (simp add: split_def scaleR_prod_def setsum_cartesian_product)
2.668 - also have "\<dots> = (\<Sum>vt\<in>tI. tu vt *\<^sub>R (\<Sum>vs\<in>sI. su vs *\<^sub>R vs))"
2.669 - using setsum_commute[of "(\<lambda>vt vs. (su vs * tu vt) *\<^sub>R vs)" sI tI]
2.670 - by (simp add: mult_commute scaleR_right.setsum)
2.671 - also have "\<dots> = (\<Sum>vt\<in>tI. tu vt *\<^sub>R xs)"
2.672 - using s by auto
2.673 - also have "\<dots> = (\<Sum>vt\<in>tI. tu vt) *\<^sub>R xs"
2.674 - by (simp add: scaleR_left.setsum)
2.675 - also have "\<dots> = xs"
2.676 - using t by auto
2.677 - finally have h1: "fst (\<Sum>v\<in>sI \<times> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)=xs"
2.678 - by auto
2.679 - have "snd (\<Sum>v\<in>sI \<times> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) =
2.680 - (\<Sum>vs\<in>sI. \<Sum>vt\<in>tI. (su vs * tu vt) *\<^sub>R vt)"
2.681 - using snd_setsum[of "(\<lambda>v. (su (fst v) * tu (snd v)) *\<^sub>R v)" "sI \<times> tI"]
2.682 - by (simp add: split_def scaleR_prod_def setsum_cartesian_product)
2.683 - also have "\<dots> = (\<Sum>vs\<in>sI. su vs *\<^sub>R (\<Sum>vt\<in>tI. tu vt *\<^sub>R vt))"
2.684 - by (simp add: mult_commute scaleR_right.setsum)
2.685 - also have "\<dots> = (\<Sum>vs\<in>sI. su vs *\<^sub>R xt)"
2.686 - using t by auto
2.687 - also have "\<dots> = (\<Sum>vs\<in>sI. su vs) *\<^sub>R xt"
2.688 - by (simp add: scaleR_left.setsum)
2.689 - also have "\<dots> = xt"
2.690 - using s by auto
2.691 - finally have h2: "snd (\<Sum>v\<in>sI \<times> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) = xt"
2.692 - by auto
2.693 - from h1 h2 have "(\<Sum>v\<in>sI \<times> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) = x"
2.694 - using xst by auto
2.695 -
2.696 - moreover have "finite I" "I \<subseteq> S \<times> T"
2.697 - using s t I_def by auto
2.698 - moreover have "\<forall>i\<in>I. 0 \<le> u i"
2.699 - using s t I_def u_def by (simp add: mult_nonneg_nonneg)
2.700 - moreover have "setsum u I = 1"
2.701 - using u_def I_def setsum_cartesian_product[of "\<lambda>x y. su x * tu y"]
2.702 - s t setsum_product[of su sI tu tI]
2.703 - by (auto simp add: split_def)
2.704 - ultimately have "x \<in> convex hull (S \<times> T)"
2.705 - apply (subst convex_hull_explicit[of "S \<times> T"])
2.706 - apply rule
2.707 - apply (rule_tac x="I" in exI)
2.708 - apply (rule_tac x="u" in exI)
2.709 - using I_def u_def
2.710 - apply auto
2.711 - done
2.712 - }
2.713 - then have "convex hull (S \<times> T) \<supseteq> (convex hull S) \<times> (convex hull T)"
2.714 - by auto
2.715 - moreover have "convex ((convex hull S) \<times> (convex hull T))"
2.716 - by (simp add: convex_direct_sum convex_convex_hull)
2.717 - ultimately show ?thesis
2.718 - using hull_minimal[of "S \<times> T" "(convex hull S) \<times> (convex hull T)" "convex"]
2.719 - hull_subset[of S convex] hull_subset[of T convex]
2.720 - by auto
2.721 -qed
2.722 -
2.723 lemma rel_interior_direct_sum:
2.724 fixes S :: "'n::euclidean_space set"
2.725 and T :: "'m::euclidean_space set"
2.726 @@ -8289,7 +8161,7 @@
2.727 by auto
2.728 also have "\<dots> = rel_interior (S \<times> (UNIV :: 'm set)) \<inter> rel_interior ((UNIV :: 'n set) \<times> T)"
2.729 apply (subst convex_rel_interior_inter_two[of "S \<times> (UNIV :: 'm set)" "(UNIV :: 'n set) <*> T"])
2.730 - using * ri assms convex_direct_sum
2.731 + using * ri assms convex_Times
2.732 apply auto
2.733 done
2.734 finally have ?thesis using * by auto
2.735 @@ -8366,7 +8238,7 @@
2.736 using rel_interior_convex_linear_preimage[of f S]
2.737 by auto
2.738 then show ?thesis
2.739 - using convex_linear_preimage assms linear_conv_bounded_linear
2.740 + using convex_linear_vimage assms
2.741 by auto
2.742 qed
2.743
2.744 @@ -8495,7 +8367,7 @@
2.745 { assume "S={}" hence ?thesis by (simp add: rel_interior_empty cone_hull_empty) }
2.746 moreover
2.747 { assume "S ~= {}" from this obtain s where "s : S" by auto
2.748 -have conv: "convex ({(1 :: real)} <*> S)" using convex_direct_sum[of "{(1 :: real)}" S]
2.749 +have conv: "convex ({(1 :: real)} <*> S)" using convex_Times[of "{(1 :: real)}" S]
2.750 assms convex_singleton[of "1 :: real"] by auto
2.751 def f == "(%y. {z. (y,z) : cone hull ({(1 :: real)} <*> S)})"
2.752 hence *: "(c, x) : rel_interior (cone hull ({(1 :: real)} <*> S)) =
2.753 @@ -8687,7 +8559,7 @@
2.754 have "(convex hull S) + (convex hull T) =
2.755 (%(x,y). x + y) ` ((convex hull S) <*> (convex hull T))"
2.756 by (simp add: set_plus_image)
2.757 -also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
2.758 +also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_Times by auto
2.759 also have "...= convex hull (S + T)" using fst_snd_linear linear_conv_bounded_linear
2.760 convex_hull_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
2.761 finally show ?thesis by auto
2.762 @@ -8701,7 +8573,7 @@
2.763 have "(rel_interior S) + (rel_interior T) = (%(x,y). x + y) ` (rel_interior S <*> rel_interior T)"
2.764 by (simp add: set_plus_image)
2.765 also have "... = (%(x,y). x + y) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
2.766 -also have "...= rel_interior (S + T)" using fst_snd_linear convex_direct_sum assms
2.767 +also have "...= rel_interior (S + T)" using fst_snd_linear convex_Times assms
2.768 rel_interior_convex_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
2.769 finally show ?thesis by auto
2.770 qed
2.771 @@ -8732,7 +8604,7 @@
2.772 fixes S T :: "('n::euclidean_space) set"
2.773 assumes "convex S" "rel_open S" "convex T" "rel_open T"
2.774 shows "convex (S <*> T) & rel_open (S <*> T)"
2.775 -by (metis assms convex_direct_sum rel_interior_direct_sum rel_open_def)
2.776 +by (metis assms convex_Times rel_interior_direct_sum rel_open_def)
2.777
2.778 lemma convex_rel_open_sum:
2.779 fixes S T :: "('n::euclidean_space) set"
2.780 @@ -8808,7 +8680,7 @@
2.781 def K == "(%i. cone hull ({(1 :: real)} <*> (S i)))"
2.782 have "!i:I. K i ~= {}" unfolding K_def using assms by (simp add: cone_hull_empty_iff[symmetric])
2.783 { fix i assume "i:I"
2.784 - hence "convex (K i)" unfolding K_def apply (subst convex_cone_hull) apply (subst convex_direct_sum)
2.785 + hence "convex (K i)" unfolding K_def apply (subst convex_cone_hull) apply (subst convex_Times)
2.786 using assms by auto
2.787 }
2.788 hence convK: "!i:I. convex (K i)" by auto
2.789 @@ -8817,14 +8689,14 @@
2.790 }
2.791 hence "K0 >= Union (K ` I)" by auto
2.792 moreover have "convex K0" unfolding K0_def
2.793 - apply (subst convex_cone_hull) apply (subst convex_direct_sum)
2.794 + apply (subst convex_cone_hull) apply (subst convex_Times)
2.795 unfolding C0_def using convex_convex_hull by auto
2.796 ultimately have geq: "K0 >= convex hull (Union (K ` I))" using hull_minimal[of _ "K0" "convex"] by blast
2.797 have "!i:I. K i >= {(1 :: real)} <*> (S i)" using K_def by (simp add: hull_subset)
2.798 hence "Union (K ` I) >= {(1 :: real)} <*> Union (S ` I)" by auto
2.799 hence "convex hull Union (K ` I) >= convex hull ({(1 :: real)} <*> Union (S ` I))" by (simp add: hull_mono)
2.800 hence "convex hull Union (K ` I) >= {(1 :: real)} <*> C0" unfolding C0_def
2.801 - using convex_hull_direct_sum[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto
2.802 + using convex_hull_Times[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto
2.803 moreover have "cone (convex hull(Union (K ` I)))" apply (subst cone_convex_hull)
2.804 using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull by auto
2.805 ultimately have "convex hull (Union (K ` I)) >= K0"
2.806 @@ -8835,7 +8707,7 @@
2.807 using assms apply blast
2.808 using `I ~= {}` apply blast
2.809 unfolding K_def apply rule
2.810 - apply (subst convex_cone_hull) apply (subst convex_direct_sum)
2.811 + apply (subst convex_cone_hull) apply (subst convex_Times)
2.812 using assms cone_cone_hull `!i:I. K i ~= {}` K_def by auto
2.813 finally have "K0 = setsum K I" by auto
2.814 hence *: "rel_interior K0 = setsum (%i. (rel_interior (K i))) I"