# HG changeset patch # User wenzelm # Date 1357825219 -3600 # Node ID 4156a45aeb638c3a2235c7ba5b4fd1183601f305 # Parent 8a1ea6b00aced0a84e78a07bf5b01041dc6639f8 tuned proofs; diff -r 8a1ea6b00ace -r 4156a45aeb63 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 10 13:15:05 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 10 14:40:19 2013 +0100 @@ -125,8 +125,8 @@ { fix x :: "'n::euclidean_space" def y == "(e/norm x) *\<^sub>R x" then have "y : cball 0 e" using cball_def dist_norm[of 0 y] assms by auto - moreover have "x = (norm x/e) *\<^sub>R y" using y_def assms by simp - moreover hence "x = (norm x/e) *\<^sub>R y" by auto + moreover have *: "x = (norm x/e) *\<^sub>R y" using y_def assms by simp + moreover from * have "x = (norm x/e) *\<^sub>R y" by auto ultimately have "x : span (cball 0 e)" using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto } then have "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto @@ -297,7 +297,7 @@ and "setsum (\y. if (x = y) then P x else Q y) s = setsum Q s" and "setsum (\y. if (y = x) then P y else Q y) s = setsum Q s" and "setsum (\y. if (x = y) then P y else Q y) s = setsum Q s" - apply(rule_tac [!] setsum_cong2) + apply (rule_tac [!] setsum_cong2) using assms apply auto done @@ -659,12 +659,12 @@ qed lemma mem_affine: - assumes "affine S" "x : S" "y : S" "u+v=1" + assumes "affine S" "x : S" "y : S" "u + v = 1" shows "(u *\<^sub>R x + v *\<^sub>R y) : S" using assms affine_def[of S] by auto lemma mem_affine_3: - assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1" + assumes "affine S" "x : S" "y : S" "z : S" "u + v + w = 1" shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S" proof - have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}" @@ -689,7 +689,9 @@ "affine hull (insert a s) \ {a + v| v . v \ span {x - a | x . x \ s}}" unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq - apply (rule, rule) apply (erule exE)+ apply (erule conjE)+ + apply (rule, rule) + apply (erule exE)+ + apply (erule conjE)+ proof - fix x t u assume as: "finite t" "t \ {}" "t \ insert a s" "setsum u t = 1" "(\v\t. u v *\<^sub>R v) = x" @@ -1163,90 +1165,109 @@ shows "\x \ a. x <= b \ f x \ e1 \ f x \ e2" (is "\ x. ?P x") proof - let ?S = "{c. \x \ a. x <= c \ f x \ e1}" - have Se: " \x. x \ ?S" apply (rule exI[where x=a]) by (auto simp add: fa) + have Se: " \x. x \ ?S" + apply (rule exI[where x=a]) + apply (auto simp add: fa) + done have Sub: "\y. isUb UNIV ?S y" apply (rule exI[where x= b]) - using ab fb e12 by (auto simp add: isUb_def setle_def) + using ab fb e12 apply (auto simp add: isUb_def setle_def) + done from reals_complete[OF Se Sub] obtain l where l: "isLub UNIV ?S l"by blast have alb: "a \ l" "l \ b" using l ab fa fb e12 apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) - by (metis linorder_linear) + apply (metis linorder_linear) + done have ale1: "\z \ a. z < l \ f z \ e1" using l apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) - by (metis linorder_linear not_le) - have th1: "\z x e d :: real. z <= x + e \ e < d ==> z < x \ abs(z - x) < d" by arith - have th2: "\e x:: real. 0 < e ==> ~(x + e <= x)" by arith - have "\d::real. 0 < d \ 0 < d/2 \ d/2 < d" by simp - then have th3: "\d::real. d > 0 \ \e > 0. e < d" by blast - {assume le2: "f l \ e2" - from le2 fa fb e12 alb have la: "l \ a" by metis - hence lap: "l - a > 0" using alb by arith - from e2[rule_format, OF le2] obtain e where - e: "e > 0" "\y. dist y (f l) < e \ y \ e2" by metis - from dst[OF alb e(1)] obtain d where - d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis - let ?d' = "min (d/2) ((l - a)/2)" - have "?d' < d \ 0 < ?d' \ ?d' < l - a" using lap d(1) - by (simp add: min_max.less_infI2) - then have "\d'. d' < d \ d' >0 \ l - d' > a" by auto - then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis - from d e have th0: "\y. \y - l\ < d \ f y \ e2" by metis - from th0[rule_format, of "l - d'"] d' have "f (l - d') \ e2" by auto - moreover - have "f (l - d') \ e1" using ale1[rule_format, of "l -d'"] d' by auto - ultimately have False using e12 alb d' by auto} + apply (metis linorder_linear not_le) + done + have th1: "\z x e d :: real. z <= x + e \ e < d ==> z < x \ abs(z - x) < d" by arith + have th2: "\e x:: real. 0 < e ==> ~(x + e <= x)" by arith + have "\d::real. 0 < d \ 0 < d/2 \ d/2 < d" by simp + then have th3: "\d::real. d > 0 \ \e > 0. e < d" by blast + { assume le2: "f l \ e2" + from le2 fa fb e12 alb have la: "l \ a" by metis + then have lap: "l - a > 0" using alb by arith + from e2[rule_format, OF le2] obtain e where + e: "e > 0" "\y. dist y (f l) < e \ y \ e2" by metis + from dst[OF alb e(1)] obtain d where + d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis + let ?d' = "min (d/2) ((l - a)/2)" + have "?d' < d \ 0 < ?d' \ ?d' < l - a" using lap d(1) + by (simp add: min_max.less_infI2) + then have "\d'. d' < d \ d' >0 \ l - d' > a" by auto + then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis + from d e have th0: "\y. \y - l\ < d \ f y \ e2" by metis + from th0[rule_format, of "l - d'"] d' have "f (l - d') \ e2" by auto moreover - {assume le1: "f l \ e1" + have "f (l - d') \ e1" using ale1[rule_format, of "l -d'"] d' by auto + ultimately have False using e12 alb d' by auto } + moreover + { assume le1: "f l \ e1" from le1 fa fb e12 alb have lb: "l \ b" by metis - hence blp: "b - l > 0" using alb by arith - from e1[rule_format, OF le1] obtain e where - e: "e > 0" "\y. dist y (f l) < e \ y \ e1" by metis - from dst[OF alb e(1)] obtain d where - d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis - have "\d::real. 0 < d \ d/2 < d \ 0 < d/2" by simp - then have "\d'. d' < d \ d' >0" using d(1) by blast - then obtain d' where d': "d' > 0" "d' < d" by metis - from d e have th0: "\y. \y - l\ < d \ f y \ e1" by auto - hence "\y. l \ y \ y \ l + d' \ f y \ e1" using d' by auto - with ale1 have "\y. a \ y \ y \ l + d' \ f y \ e1" by auto - with l d' have False - by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } - ultimately show ?thesis using alb by metis + then have blp: "b - l > 0" using alb by arith + from e1[rule_format, OF le1] obtain e where + e: "e > 0" "\y. dist y (f l) < e \ y \ e1" by metis + from dst[OF alb e(1)] obtain d where + d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis + have "\d::real. 0 < d \ d/2 < d \ 0 < d/2" by simp + then have "\d'. d' < d \ d' >0" using d(1) by blast + then obtain d' where d': "d' > 0" "d' < d" by metis + from d e have th0: "\y. \y - l\ < d \ f y \ e1" by auto + then have "\y. l \ y \ y \ l + d' \ f y \ e1" using d' by auto + with ale1 have "\y. a \ y \ y \ l + d' \ f y \ e1" by auto + with l d' have False + by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } + ultimately show ?thesis using alb by metis qed lemma convex_connected: fixes s :: "'a::real_normed_vector set" assumes "convex s" shows "connected s" -proof- - { fix e1 e2 assume as:"open e1" "open e2" "e1 \ e2 \ s = {}" "s \ e1 \ e2" +proof - + { fix e1 e2 + assume as:"open e1" "open e2" "e1 \ e2 \ s = {}" "s \ e1 \ e2" assume "e1 \ s \ {}" "e2 \ s \ {}" then obtain x1 x2 where x1:"x1\e1" "x1\s" and x2:"x2\e2" "x2\s" by auto - hence n:"norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto + then have n: "norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto { fix x e::real assume as:"0 \ x" "x \ 1" "0 < e" - { fix y have *:"(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2" + { fix y + have *: "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2" by (simp add: algebra_simps) assume "\y - x\ < e / norm (x1 - x2)" hence "norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e" unfolding * and scaleR_right_diff_distrib[symmetric] - unfolding less_divide_eq using n by auto } - hence "\d>0. \y. \y - x\ < d \ norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e" - apply(rule_tac x="e / norm (x1 - x2)" in exI) using as - apply auto unfolding zero_less_divide_iff using n by simp } note * = this + unfolding less_divide_eq using n by auto + } + then have "\d>0. \y. \y - x\ < d \ norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e" + apply (rule_tac x="e / norm (x1 - x2)" in exI) + using as + apply auto + unfolding zero_less_divide_iff + using n apply simp + done + } note * = this have "\x\0. x \ 1 \ (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e1 \ (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e2" - apply(rule connected_real_lemma) apply (simp add: `x1\e1` `x2\e2` dist_commute)+ - using * apply(simp add: dist_norm) + apply (rule connected_real_lemma) + apply (simp add: `x1\e1` `x2\e2` dist_commute)+ + using * apply (simp add: dist_norm) using as(1,2)[unfolded open_dist] apply simp using as(1,2)[unfolded open_dist] apply simp using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2 - using as(3) by auto - then obtain x where "x\0" "x\1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e2" by auto - hence False using as(4) + using as(3) apply auto + done + then obtain x where "x\0" "x\1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e2" + by auto + then have False + using as(4) using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] - using x1(2) x2(2) by auto } - thus ?thesis unfolding connected_def by auto + using x1(2) x2(2) by auto + } + then show ?thesis unfolding connected_def by auto qed text {* One rather trivial consequence. *} @@ -1276,37 +1297,53 @@ hence xy:"0 < dist x y" by (auto simp add: dist_nz[symmetric]) then obtain u where "0 < u" "u \ 1" and u:"u < e / dist x y" - using real_lbound_gt_zero[of 1 "e / dist x y"] using xy `e>0` and divide_pos_pos[of e "dist x y"] by auto + using real_lbound_gt_zero[of 1 "e / dist x y"] + using xy `e>0` and divide_pos_pos[of e "dist x y"] by auto hence "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \ (1-u) * f x + u * f y" using `x\s` `y\s` - using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto + using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] + by auto moreover - have *:"x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" by (simp add: algebra_simps) - have "(1 - u) *\<^sub>R x + u *\<^sub>R y \ ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" + by (simp add: algebra_simps) + have "(1 - u) *\<^sub>R x + u *\<^sub>R y \ ball x e" + unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0 f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto - ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto + then have "f x \ f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto + ultimately show False + using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto qed lemma convex_ball: fixes x :: "'a::real_normed_vector" shows "convex (ball x e)" -proof(auto simp add: convex_def) - fix y z assume yz:"dist x y < e" "dist x z < e" - fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" - have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" using uv yz - using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto - thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using convex_bound_lt[OF yz uv] by auto +proof (auto simp add: convex_def) + fix y z + assume yz: "dist x y < e" "dist x z < e" + fix u v :: real + assume uv: "0 \ u" "0 \ v" "u + v = 1" + have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" + using uv yz + using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] + by auto + then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" + using convex_bound_lt[OF yz uv] by auto qed lemma convex_cball: fixes x :: "'a::real_normed_vector" shows "convex(cball x e)" -proof(auto simp add: convex_def Ball_def) - fix y z assume yz:"dist x y \ e" "dist x z \ e" - fix u v ::real assume uv:" 0 \ u" "0 \ v" "u + v = 1" - have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" using uv yz - using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto - thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \ e" using convex_bound_le[OF yz uv] by auto +proof (auto simp add: convex_def Ball_def) + fix y z + assume yz: "dist x y \ e" "dist x z \ e" + fix u v :: real + assume uv: "0 \ u" "0 \ v" "u + v = 1" + have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" + using uv yz + using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] + by auto + then show "dist x (u *\<^sub>R y + v *\<^sub>R z) \ e" + using convex_bound_le[OF yz uv] by auto qed lemma connected_ball: @@ -1319,6 +1356,7 @@ shows "connected(cball x e)" using convex_connected convex_cball by auto + subsection {* Convex hull *} lemma convex_convex_hull: "convex(convex hull s)" @@ -1326,102 +1364,182 @@ by auto lemma convex_hull_eq: "convex hull s = s \ convex s" -by (metis convex_convex_hull hull_same) + by (metis convex_convex_hull hull_same) lemma bounded_convex_hull: fixes s :: "'a::real_normed_vector set" assumes "bounded s" shows "bounded(convex hull s)" -proof- from assms obtain B where B:"\x\s. norm x \ B" unfolding bounded_iff by auto - show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B]) +proof - + from assms obtain B where B: "\x\s. norm x \ B" + unfolding bounded_iff by auto + show ?thesis + apply (rule bounded_subset[OF bounded_cball, of _ 0 B]) unfolding subset_hull[of convex, OF convex_cball] - unfolding subset_eq mem_cball dist_norm using B by auto qed + unfolding subset_eq mem_cball dist_norm using B apply auto + done +qed lemma finite_imp_bounded_convex_hull: fixes s :: "'a::real_normed_vector set" shows "finite s \ bounded(convex hull s)" using bounded_convex_hull finite_imp_bounded by auto + subsubsection {* Convex hull is "preserved" by a linear function *} lemma convex_hull_linear_image: assumes "bounded_linear f" shows "f ` (convex hull s) = convex hull (f ` s)" - apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 - apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption - apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption -proof- + apply rule + unfolding subset_eq ball_simps + apply (rule_tac[!] hull_induct, rule hull_inc) + prefer 3 + apply (erule imageE) + apply (rule_tac x=xa in image_eqI) + apply assumption + apply (rule hull_subset[unfolded subset_eq, rule_format]) + apply assumption +proof - interpret f: bounded_linear f by fact show "convex {x. f x \ convex hull f ` s}" - unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next + unfolding convex_def + by (auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) +next interpret f: bounded_linear f by fact - show "convex {x. x \ f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s] + show "convex {x. x \ f ` (convex hull s)}" + using convex_convex_hull[unfolded convex_def, of s] unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric]) qed auto lemma in_convex_hull_linear_image: assumes "bounded_linear f" "x \ convex hull s" shows "(f x) \ convex hull (f ` s)" -using convex_hull_linear_image[OF assms(1)] assms(2) by auto + using convex_hull_linear_image[OF assms(1)] assms(2) by auto + subsubsection {* Stepping theorems for convex hulls of finite sets *} lemma convex_hull_empty[simp]: "convex hull {} = {}" - apply(rule hull_unique) by auto + by (rule hull_unique) auto lemma convex_hull_singleton[simp]: "convex hull {a} = {a}" - apply(rule hull_unique) by auto + by (rule hull_unique) auto lemma convex_hull_insert: fixes s :: "'a::real_vector set" assumes "s \ {}" - shows "convex hull (insert a s) = {x. \u\0. \v\0. \b. (u + v = 1) \ - b \ (convex hull s) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull") - apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof- - fix x assume x:"x = a \ x \ s" - thus "x\?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer - apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto + shows "convex hull (insert a s) = + {x. \u\0. \v\0. \b. (u + v = 1) \ b \ (convex hull s) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" + (is "?xyz = ?hull") + apply (rule, rule hull_minimal, rule) + unfolding insert_iff + prefer 3 + apply rule +proof - + fix x + assume x: "x = a \ x \ s" + then show "x \ ?hull" + apply rule + unfolding mem_Collect_eq + apply (rule_tac x=1 in exI) + defer + apply (rule_tac x=0 in exI) + using assms hull_subset[of s convex] + apply auto + done next - fix x assume "x\?hull" - then obtain u v b where obt:"u\0" "v\0" "u + v = 1" "b \ convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b" by auto - have "a\convex hull insert a s" "b\convex hull insert a s" - using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) by auto - thus "x\ convex hull insert a s" unfolding obt(5) using convex_convex_hull[of "insert a s", unfolded convex_def] - apply(erule_tac x=a in ballE) apply(erule_tac x=b in ballE) apply(erule_tac x=u in allE) using obt by auto + fix x + assume "x \ ?hull" + then obtain u v b where obt: "u\0" "v\0" "u + v = 1" "b \ convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b" + by auto + have "a \ convex hull insert a s" "b\convex hull insert a s" + using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) + by auto + then show "x \ convex hull insert a s" + unfolding obt(5) + using convex_convex_hull[of "insert a s", unfolded convex_def] + apply (erule_tac x = a in ballE) + apply (erule_tac x = b in ballE) + apply (erule_tac x = u in allE) + using obt apply auto + done next - show "convex ?hull" unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof- - fix x y u v assume as:"(0::real) \ u" "0 \ v" "u + v = 1" "x\?hull" "y\?hull" - from as(4) obtain u1 v1 b1 where obt1:"u1\0" "v1\0" "u1 + v1 = 1" "b1 \ convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto - from as(5) obtain u2 v2 b2 where obt2:"u2\0" "v2\0" "u2 + v2 = 1" "b2 \ convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto - have *:"\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) - have "\b \ convex hull s. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" - proof(cases "u * v1 + v * v2 = 0") - have *:"\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) - case True hence **:"u * v1 = 0" "v * v2 = 0" + show "convex ?hull" + unfolding convex_def + apply (rule, rule, rule, rule, rule, rule, rule) + proof - + fix x y u v + assume as: "(0::real) \ u" "0 \ v" "u + v = 1" "x\?hull" "y\?hull" + from as(4) obtain u1 v1 b1 + where obt1: "u1\0" "v1\0" "u1 + v1 = 1" "b1 \ convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto + from as(5) obtain u2 v2 b2 + where obt2: "u2\0" "v2\0" "u2 + v2 = 1" "b2 \ convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto + have *: "\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" + by (auto simp add: algebra_simps) + have **: "\b \ convex hull s. u *\<^sub>R x + v *\<^sub>R y = + (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" + proof (cases "u * v1 + v * v2 = 0") + case True + have *: "\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" + by (auto simp add: algebra_simps) + from True have ***: "u * v1 = 0" "v * v2 = 0" using mult_nonneg_nonneg[OF `u\0` `v1\0`] mult_nonneg_nonneg[OF `v\0` `v2\0`] by arith+ - hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto - thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: ** scaleR_right_distrib) + then have "u * u1 + v * u2 = 1" + using as(3) obt1(3) obt2(3) by auto + then show ?thesis + unfolding obt1(5) obt2(5) * + using assms hull_subset[of s convex] + by (auto simp add: *** scaleR_right_distrib) next - have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) - also have "\ = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) - also have "\ = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto - case False have "0 \ u * v1 + v * v2" "0 \ u * v1" "0 \ u * v1 + v * v2" "0 \ v * v2" apply - - apply(rule add_nonneg_nonneg) prefer 4 apply(rule add_nonneg_nonneg) apply(rule_tac [!] mult_nonneg_nonneg) - using as(1,2) obt1(1,2) obt2(1,2) by auto - thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False - apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer - apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4) + case False + have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" + using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) + also have "\ = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" + using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) + also have "\ = u * v1 + v * v2" + by simp + finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto + have "0 \ u * v1 + v * v2" "0 \ u * v1" "0 \ u * v1 + v * v2" "0 \ v * v2" + apply (rule add_nonneg_nonneg) + prefer 4 + apply (rule add_nonneg_nonneg) + apply (rule_tac [!] mult_nonneg_nonneg) + using as(1,2) obt1(1,2) obt2(1,2) apply auto + done + then show ?thesis + unfolding obt1(5) obt2(5) + unfolding * and ** + using False + apply (rule_tac x = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) + defer + apply (rule convex_convex_hull[of s, unfolded convex_def, rule_format]) + using obt1(4) obt2(4) unfolding add_divide_distrib[symmetric] and zero_le_divide_iff - by (auto simp add: scaleR_left_distrib scaleR_right_distrib) - qed note * = this - have u1:"u1 \ 1" unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto - have u2:"u2 \ 1" unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto - have "u1 * u + u2 * v \ (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono) - apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto - also have "\ \ 1" unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto - finally - show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI) - apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def - using as(1,2) obt1(1,2) obt2(1,2) * by(auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps) + apply (auto simp add: scaleR_left_distrib scaleR_right_distrib) + done + qed + have u1: "u1 \ 1" + unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto + have u2: "u2 \ 1" + unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto + have "u1 * u + u2 * v \ (max u1 u2) * u + (max u1 u2) * v" + apply (rule add_mono) + apply (rule_tac [!] mult_right_mono) + using as(1,2) obt1(1,2) obt2(1,2) + apply auto + done + also have "\ \ 1" + unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto + finally show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" + unfolding mem_Collect_eq + apply (rule_tac x="u * u1 + v * u2" in exI) + apply (rule conjI) + defer + apply (rule_tac x="1 - u * u1 - v * u2" in exI) + unfolding Bex_def + using as(1,2) obt1(1,2) obt2(1,2) ** + apply (auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps) + done qed qed @@ -1430,162 +1548,307 @@ lemma convex_hull_indexed: fixes s :: "'a::real_vector set" - shows "convex hull s = {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ s) \ - (setsum u {1..k} = 1) \ - (setsum (\i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull") - apply(rule hull_unique) apply(rule) defer - apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule) -proof- - fix x assume "x\s" - thus "x \ ?hull" unfolding mem_Collect_eq apply(rule_tac x=1 in exI, rule_tac x="\x. 1" in exI) by auto + shows "convex hull s = + {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ s) \ + (setsum u {1..k} = 1) \ + (setsum (\i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull") + apply (rule hull_unique) + apply rule + defer + apply (subst convex_def) + apply (rule, rule, rule, rule, rule, rule, rule) +proof - + fix x + assume "x\s" + then show "x \ ?hull" + unfolding mem_Collect_eq + apply (rule_tac x=1 in exI, rule_tac x="\x. 1" in exI) + apply auto + done next - fix t assume as:"s \ t" "convex t" - show "?hull \ t" apply(rule) unfolding mem_Collect_eq apply(erule exE | erule conjE)+ proof- - fix x k u y assume assm:"\i\{1::nat..k}. 0 \ u i \ y i \ s" "setsum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R y i) = x" - show "x\t" unfolding assm(3)[symmetric] apply(rule as(2)[unfolded convex, rule_format]) - using assm(1,2) as(1) by auto qed + fix t + assume as: "s \ t" "convex t" + show "?hull \ t" + apply rule + unfolding mem_Collect_eq + apply (erule exE | erule conjE)+ + proof - + fix x k u y + assume assm: + "\i\{1::nat..k}. 0 \ u i \ y i \ s" + "setsum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R y i) = x" + show "x\t" + unfolding assm(3) [symmetric] + apply (rule as(2)[unfolded convex, rule_format]) + using assm(1,2) as(1) apply auto + done + qed next - fix x y u v assume uv:"0\u" "0\v" "u+v=(1::real)" and xy:"x\?hull" "y\?hull" - from xy obtain k1 u1 x1 where x:"\i\{1::nat..k1}. 0\u1 i \ x1 i \ s" "setsum u1 {Suc 0..k1} = 1" "(\i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto - from xy obtain k2 u2 x2 where y:"\i\{1::nat..k2}. 0\u2 i \ x2 i \ s" "setsum u2 {Suc 0..k2} = 1" "(\i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto - have *:"\P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)" + fix x y u v + assume uv: "0\u" "0\v" "u + v = (1::real)" and xy: "x\?hull" "y\?hull" + from xy obtain k1 u1 x1 where + x: "\i\{1::nat..k1}. 0\u1 i \ x1 i \ s" "setsum u1 {Suc 0..k1} = 1" "(\i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" + by auto + from xy obtain k2 u2 x2 where + y: "\i\{1::nat..k2}. 0\u2 i \ x2 i \ s" "setsum u2 {Suc 0..k2} = 1" "(\i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" + by auto + have *: "\P (x1::'a) x2 s1 s2 i. + (if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)" "{1..k1 + k2} \ {1..k1} = {1..k1}" "{1..k1 + k2} \ - {1..k1} = (\i. i + k1) ` {1..k2}" - prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le) - have inj:"inj_on (\i. i + k1) {1..k2}" unfolding inj_on_def by auto - show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" apply(rule) - apply(rule_tac x="k1 + k2" in exI, rule_tac x="\i. if i \ {1..k1} then u * u1 i else v * u2 (i - k1)" in exI) - apply(rule_tac x="\i. if i \ {1..k1} then x1 i else x2 (i - k1)" in exI) apply(rule,rule) defer apply(rule) - unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def Collect_mem_eq - unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_right_distrib[symmetric] proof- - fix i assume i:"i \ {1..k1+k2}" - show "0 \ (if i \ {1..k1} then u * u1 i else v * u2 (i - k1)) \ (if i \ {1..k1} then x1 i else x2 (i - k1)) \ s" - proof(cases "i\{1..k1}") - case True thus ?thesis using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto - next def j \ "i - k1" - case False with i have "j \ {1..k2}" unfolding j_def by auto - thus ?thesis unfolding j_def[symmetric] using False - using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]] by auto qed - qed(auto simp add: not_le x(2,3) y(2,3) uv(3)) + prefer 3 + apply (rule, rule) + unfolding image_iff + apply (rule_tac x = "x - k1" in bexI) + apply (auto simp add: not_le) + done + have inj: "inj_on (\i. i + k1) {1..k2}" + unfolding inj_on_def by auto + show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" + apply rule + apply (rule_tac x="k1 + k2" in exI) + apply (rule_tac x="\i. if i \ {1..k1} then u * u1 i else v * u2 (i - k1)" in exI) + apply (rule_tac x="\i. if i \ {1..k1} then x1 i else x2 (i - k1)" in exI) + apply (rule, rule) + defer + apply rule + unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and + setsum_reindex[OF inj] and o_def Collect_mem_eq + unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_right_distrib[symmetric] + proof - + fix i + assume i: "i \ {1..k1+k2}" + show "0 \ (if i \ {1..k1} then u * u1 i else v * u2 (i - k1)) \ + (if i \ {1..k1} then x1 i else x2 (i - k1)) \ s" + proof (cases "i\{1..k1}") + case True + then show ?thesis + using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto + next + case False + def j \ "i - k1" + from i False have "j \ {1..k2}" unfolding j_def by auto + then show ?thesis + unfolding j_def[symmetric] + using False + using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]] + apply auto + done + qed + qed (auto simp add: not_le x(2,3) y(2,3) uv(3)) qed lemma convex_hull_finite: fixes s :: "'a::real_vector set" assumes "finite s" shows "convex hull s = {y. \u. (\x\s. 0 \ u x) \ - setsum u s = 1 \ setsum (\x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set") -proof(rule hull_unique, auto simp add: convex_def[of ?set]) - fix x assume "x\s" thus " \u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) = x" - apply(rule_tac x="\y. if x=y then 1 else 0" in exI) apply auto - unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto + setsum u s = 1 \ setsum (\x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set") +proof (rule hull_unique, auto simp add: convex_def[of ?set]) + fix x + assume "x \ s" + then show "\u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) = x" + apply (rule_tac x="\y. if x=y then 1 else 0" in exI) + apply auto + unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] + apply auto + done next - fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" - fix ux assume ux:"\x\s. 0 \ ux x" "setsum ux s = (1::real)" - fix uy assume uy:"\x\s. 0 \ uy x" "setsum uy s = (1::real)" - { fix x assume "x\s" - hence "0 \ u * ux x + v * uy x" using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2) - by (auto, metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2)) } - moreover have "(\x\s. u * ux x + v * uy x) = 1" + fix u v :: real + assume uv: "0 \ u" "0 \ v" "u + v = 1" + fix ux assume ux: "\x\s. 0 \ ux x" "setsum ux s = (1::real)" + fix uy assume uy: "\x\s. 0 \ uy x" "setsum uy s = (1::real)" + { fix x + assume "x\s" + then have "0 \ u * ux x + v * uy x" + using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2) + apply auto + apply (metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2)) + done + } + moreover + have "(\x\s. u * ux x + v * uy x) = 1" unfolding setsum_addf and setsum_right_distrib[symmetric] and ux(2) uy(2) using uv(3) by auto - moreover have "(\x\s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" - unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric] by auto - ultimately show "\uc. (\x\s. 0 \ uc x) \ setsum uc s = 1 \ (\x\s. uc x *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" - apply(rule_tac x="\x. u * ux x + v * uy x" in exI) by auto + moreover + have "(\x\s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" + unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric] + by auto + ultimately + show "\uc. (\x\s. 0 \ uc x) \ setsum uc s = 1 \ + (\x\s. uc x *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" + apply (rule_tac x="\x. u * ux x + v * uy x" in exI) + apply auto + done next - fix t assume t:"s \ t" "convex t" - fix u assume u:"\x\s. 0 \ u x" "setsum u s = (1::real)" - thus "(\x\s. u x *\<^sub>R x) \ t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]] + fix t + assume t: "s \ t" "convex t" + fix u + assume u: "\x\s. 0 \ u x" "setsum u s = (1::real)" + then show "(\x\s. u x *\<^sub>R x) \ t" + using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]] using assms and t(1) by auto qed + subsubsection {* Another formulation from Lars Schewe *} lemma setsum_constant_scaleR: fixes y :: "'a::real_vector" shows "(\x\A. y) = of_nat (card A) *\<^sub>R y" -apply (cases "finite A") -apply (induct set: finite) -apply (simp_all add: algebra_simps) -done + apply (cases "finite A") + apply (induct set: finite) + apply (simp_all add: algebra_simps) + done lemma convex_hull_explicit: fixes p :: "'a::real_vector set" shows "convex hull p = {y. \s u. finite s \ s \ p \ - (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs") -proof- + (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs") +proof - { fix x assume "x\?lhs" - then obtain k u y where obt:"\i\{1::nat..k}. 0 \ u i \ y i \ p" "setsum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R y i) = x" + then obtain k u y where + obt: "\i\{1::nat..k}. 0 \ u i \ y i \ p" "setsum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R y i) = x" unfolding convex_hull_indexed by auto - have fin:"finite {1..k}" by auto - have fin':"\v. finite {i \ {1..k}. y i = v}" by auto - { fix j assume "j\{1..k}" - hence "y j \ p" "0 \ setsum u {i. Suc 0 \ i \ i \ k \ y i = y j}" - using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp - apply(rule setsum_nonneg) using obt(1) by auto } + have fin: "finite {1..k}" by auto + have fin': "\v. finite {i \ {1..k}. y i = v}" by auto + { fix j + assume "j\{1..k}" + then have "y j \ p" "0 \ setsum u {i. Suc 0 \ i \ i \ k \ y i = y j}" + using obt(1)[THEN bspec[where x=j]] and obt(2) + apply simp + apply (rule setsum_nonneg) + using obt(1) + apply auto + done + } moreover have "(\v\y ` {1..k}. setsum u {i \ {1..k}. y i = v}) = 1" unfolding setsum_image_gen[OF fin, symmetric] using obt(2) by auto moreover have "(\v\y ` {1..k}. setsum u {i \ {1..k}. y i = v} *\<^sub>R v) = x" using setsum_image_gen[OF fin, of "\i. u i *\<^sub>R y i" y, symmetric] unfolding scaleR_left.setsum using obt(3) by auto - ultimately have "\s u. finite s \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = x" - apply(rule_tac x="y ` {1..k}" in exI) - apply(rule_tac x="\v. setsum u {i\{1..k}. y i = v}" in exI) by auto - hence "x\?rhs" by auto } + ultimately + have "\s u. finite s \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = x" + apply (rule_tac x="y ` {1..k}" in exI) + apply (rule_tac x="\v. setsum u {i\{1..k}. y i = v}" in exI) + apply auto + done + then have "x\?rhs" by auto + } moreover { fix y assume "y\?rhs" - then obtain s u where obt:"finite s" "s \ p" "\x\s. 0 \ u x" "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = y" by auto - - obtain f where f:"inj_on f {1..card s}" "f ` {1..card s} = s" using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto - - { fix i::nat assume "i\{1..card s}" - hence "f i \ s" apply(subst f(2)[symmetric]) by auto - hence "0 \ u (f i)" "f i \ p" using obt(2,3) by auto } + then obtain s u where + obt: "finite s" "s \ p" "\x\s. 0 \ u x" "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = y" by auto + + obtain f where f: "inj_on f {1..card s}" "f ` {1..card s} = s" + using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto + + { fix i :: nat + assume "i\{1..card s}" + then have "f i \ s" + apply (subst f(2)[symmetric]) + apply auto + done + then have "0 \ u (f i)" "f i \ p" using obt(2,3) by auto + } moreover have *:"finite {1..card s}" by auto - { fix y assume "y\s" - then obtain i where "i\{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto - hence "{x. Suc 0 \ x \ x \ card s \ f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] apply(erule_tac x=x in ballE) by auto - hence "card {x. Suc 0 \ x \ x \ card s \ f x = y} = 1" by auto - hence "(\x\{x \ {1..card s}. f x = y}. u (f x)) = u y" - "(\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y" - by (auto simp add: setsum_constant_scaleR) } - - hence "(\x = 1..card s. u (f x)) = 1" "(\i = 1..card s. u (f i) *\<^sub>R f i) = y" + { fix y + assume "y\s" + then obtain i where "i\{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] + by auto + then have "{x. Suc 0 \ x \ x \ card s \ f x = y} = {i}" + apply auto + using f(1)[unfolded inj_on_def] + apply(erule_tac x=x in ballE) + apply auto + done + then have "card {x. Suc 0 \ x \ x \ card s \ f x = y} = 1" by auto + then have "(\x\{x \ {1..card s}. f x = y}. u (f x)) = u y" + "(\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y" + by (auto simp add: setsum_constant_scaleR) + } + then have "(\x = 1..card s. u (f x)) = 1" "(\i = 1..card s. u (f i) *\<^sub>R f i) = y" unfolding setsum_image_gen[OF *(1), of "\x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\x. u (f x)" f] unfolding f using setsum_cong2[of s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\v. u v *\<^sub>R v"] - using setsum_cong2 [of s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto - - ultimately have "\k u x. (\i\{1..k}. 0 \ u i \ x i \ p) \ setsum u {1..k} = 1 \ (\i::nat = 1..k. u i *\<^sub>R x i) = y" - apply(rule_tac x="card s" in exI) apply(rule_tac x="u \ f" in exI) apply(rule_tac x=f in exI) by fastforce - hence "y \ ?lhs" unfolding convex_hull_indexed by auto } + using setsum_cong2 [of s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x))" u] + unfolding obt(4,5) by auto + ultimately + have "\k u x. (\i\{1..k}. 0 \ u i \ x i \ p) \ setsum u {1..k} = 1 \ + (\i::nat = 1..k. u i *\<^sub>R x i) = y" + apply (rule_tac x="card s" in exI) + apply (rule_tac x="u \ f" in exI) + apply (rule_tac x=f in exI) + apply fastforce + done + then have "y \ ?lhs" unfolding convex_hull_indexed by auto + } ultimately show ?thesis unfolding set_eq_iff by blast qed + subsubsection {* A stepping theorem for that expansion *} lemma convex_hull_finite_step: - fixes s :: "'a::real_vector set" assumes "finite s" + fixes s :: "'a::real_vector set" + assumes "finite s" shows "(\u. (\x\insert a s. 0 \ u x) \ setsum u (insert a s) = w \ setsum (\x. u x *\<^sub>R x) (insert a s) = y) \ (\v\0. \u. (\x\s. 0 \ u x) \ setsum u s = w - v \ setsum (\x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?lhs = ?rhs") -proof(rule, case_tac[!] "a\s") - assume "a\s" hence *:"insert a s = s" by auto - assume ?lhs thus ?rhs unfolding * apply(rule_tac x=0 in exI) by auto +proof (rule, case_tac[!] "a\s") + assume "a\s" + then have *:" insert a s = s" by auto + assume ?lhs + then show ?rhs + unfolding * + apply (rule_tac x=0 in exI) + apply auto + done next - assume ?lhs then obtain u where u:"\x\insert a s. 0 \ u x" "setsum u (insert a s) = w" "(\x\insert a s. u x *\<^sub>R x) = y" by auto - assume "a\s" thus ?rhs apply(rule_tac x="u a" in exI) using u(1)[THEN bspec[where x=a]] apply simp - apply(rule_tac x=u in exI) using u[unfolded setsum_clauses(2)[OF assms]] and `a\s` by auto + assume ?lhs + then obtain u where u: "\x\insert a s. 0 \ u x" "setsum u (insert a s) = w" "(\x\insert a s. u x *\<^sub>R x) = y" + by auto + assume "a \ s" + then show ?rhs + apply (rule_tac x="u a" in exI) + using u(1)[THEN bspec[where x=a]] + apply simp + apply (rule_tac x=u in exI) + using u[unfolded setsum_clauses(2)[OF assms]] and `a\s` + apply auto + done next - assume "a\s" hence *:"insert a s = s" by auto - have fin:"finite (insert a s)" using assms by auto - assume ?rhs then obtain v u where uv:"v\0" "\x\s. 0 \ u x" "setsum u s = w - v" "(\x\s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto - show ?lhs apply(rule_tac x="\x. (if a = x then v else 0) + u x" in exI) unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin] - unfolding setsum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and `a\s` by auto + assume "a \ s" + then have *: "insert a s = s" by auto + have fin: "finite (insert a s)" using assms by auto + assume ?rhs + then obtain v u where uv: "v\0" "\x\s. 0 \ u x" "setsum u s = w - v" "(\x\s. u x *\<^sub>R x) = y - v *\<^sub>R a" + by auto + show ?lhs + apply (rule_tac x = "\x. (if a = x then v else 0) + u x" in exI) + unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin] + unfolding setsum_clauses(2)[OF assms] + using uv and uv(2)[THEN bspec[where x=a]] and `a\s` + apply auto + done next - assume ?rhs then obtain v u where uv:"v\0" "\x\s. 0 \ u x" "setsum u s = w - v" "(\x\s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto - moreover assume "a\s" moreover have "(\x\s. if a = x then v else u x) = setsum u s" "(\x\s. (if a = x then v else u x) *\<^sub>R x) = (\x\s. u x *\<^sub>R x)" - apply(rule_tac setsum_cong2) defer apply(rule_tac setsum_cong2) using `a\s` by auto - ultimately show ?lhs apply(rule_tac x="\x. if a = x then v else u x" in exI) unfolding setsum_clauses(2)[OF assms] by auto -qed + assume ?rhs + then obtain v u where uv: "v\0" "\x\s. 0 \ u x" "setsum u s = w - v" "(\x\s. u x *\<^sub>R x) = y - v *\<^sub>R a" + by auto + moreover + assume "a \ s" + moreover + have "(\x\s. if a = x then v else u x) = setsum u s" "(\x\s. (if a = x then v else u x) *\<^sub>R x) = (\x\s. u x *\<^sub>R x)" + apply (rule_tac setsum_cong2) + defer + apply (rule_tac setsum_cong2) + using `a \ s` + apply auto + done + ultimately show ?lhs + apply (rule_tac x="\x. if a = x then v else u x" in exI) + unfolding setsum_clauses(2)[OF assms] + apply auto + done +qed + subsubsection {* Hence some special cases *}