author  hoelzl 
Mon, 21 Jun 2010 19:33:51 +0200  
changeset 37489  44e42d392c6e 
parent 36844  5f9385ecc1a7 
child 37647  a5400b94d2dd 
permissions  rwrr 
33175  1 
(* Title: HOL/Library/Convex_Euclidean_Space.thy 
2 
Author: Robert Himmelmann, TU Muenchen 

3 
*) 

4 

5 
header {* Convex sets, functions and related things. *} 

6 

7 
theory Convex_Euclidean_Space 

36623  8 
imports Topology_Euclidean_Space Convex 
33175  9 
begin 
10 

11 

12 
(*  *) 

13 
(* To be moved elsewhere *) 

14 
(*  *) 

15 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

16 
lemma basis_0[simp]:"(basis i::'a::euclidean_space) = 0 \<longleftrightarrow> i\<ge>DIM('a)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

17 
using norm_basis[of i, where 'a='a] unfolding norm_eq_zero[where 'a='a,THEN sym] by auto 
33175  18 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

19 
lemma scaleR_2: 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

20 
fixes x :: "'a::real_vector" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

21 
shows "scaleR 2 x = x + x" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

22 
unfolding one_add_one_is_two [symmetric] scaleR_left_distrib by simp 
34964  23 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

24 
declare euclidean_simps[simp] 
33175  25 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

26 
lemma vector_choose_size: "0 <= c ==> \<exists>(x::'a::euclidean_space). norm x = c" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

27 
apply (rule exI[where x="c *\<^sub>R basis 0 ::'a"]) using DIM_positive[where 'a='a] by auto 
33175  28 

29 
lemma setsum_delta_notmem: assumes "x\<notin>s" 

30 
shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s" 

31 
"setsum (\<lambda>y. if (x = y) then P x else Q y) s = setsum Q s" 

32 
"setsum (\<lambda>y. if (y = x) then P y else Q y) s = setsum Q s" 

33 
"setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s" 

34 
apply(rule_tac [!] setsum_cong2) using assms by auto 

35 

36 
lemma setsum_delta'': 

37 
fixes s::"'a::real_vector set" assumes "finite s" 

38 
shows "(\<Sum>x\<in>s. (if y = x then f x else 0) *\<^sub>R x) = (if y\<in>s then (f y) *\<^sub>R y else 0)" 

39 
proof 

40 
have *:"\<And>x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)" by auto 

41 
show ?thesis unfolding * using setsum_delta[OF assms, of y "\<lambda>x. f x *\<^sub>R x"] by auto 

42 
qed 

43 

44 
lemma if_smult:"(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by auto 

45 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

46 
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space)) ` {a..b} = 
33175  47 
(if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})" 
48 
using image_affinity_interval[of m 0 a b] by auto 

49 

50 
lemma dist_triangle_eq: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

51 
fixes x y z :: "'a::euclidean_space" 
33175  52 
shows "dist x z = dist x y + dist y z \<longleftrightarrow> norm (x  y) *\<^sub>R (y  z) = norm (y  z) *\<^sub>R (x  y)" 
53 
proof have *:"x  y + (y  z) = x  z" by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

54 
show ?thesis unfolding dist_norm norm_triangle_eq[of "x  y" "y  z", unfolded *] 
33175  55 
by(auto simp add:norm_minus_commute) qed 
56 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

57 
lemma norm_minus_eqI:"x =  y \<Longrightarrow> norm x = norm y" by auto 
33175  58 

59 
lemma Min_grI: assumes "finite A" "A \<noteq> {}" "\<forall>a\<in>A. x < a" shows "x < Min A" 

60 
unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto 

61 

62 
lemma dimindex_ge_1:"CARD(_::finite) \<ge> 1" 

63 
using one_le_card_finite by auto 

64 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

65 
lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

66 
unfolding norm_eq_sqrt_inner by simp 
33175  67 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

68 
lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

69 
unfolding norm_eq_sqrt_inner by simp 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

70 

44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

71 

33175  72 

73 
subsection {* Affine set and affine hull.*} 

74 

75 
definition 

76 
affine :: "'a::real_vector set \<Rightarrow> bool" where 

77 
"affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)" 

78 

79 
lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1  u) *\<^sub>R x + u *\<^sub>R y \<in> s)" 

36071  80 
unfolding affine_def by(metis eq_diff_eq') 
33175  81 

82 
lemma affine_empty[intro]: "affine {}" 

83 
unfolding affine_def by auto 

84 

85 
lemma affine_sing[intro]: "affine {x}" 

86 
unfolding affine_alt by (auto simp add: scaleR_left_distrib [symmetric]) 

87 

88 
lemma affine_UNIV[intro]: "affine UNIV" 

89 
unfolding affine_def by auto 

90 

91 
lemma affine_Inter: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter> f)" 

92 
unfolding affine_def by auto 

93 

94 
lemma affine_Int: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)" 

95 
unfolding affine_def by auto 

96 

97 
lemma affine_affine_hull: "affine(affine hull s)" 

98 
unfolding hull_def using affine_Inter[of "{t \<in> affine. s \<subseteq> t}"] 

99 
unfolding mem_def by auto 

100 

101 
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s" 

36071  102 
by (metis affine_affine_hull hull_same mem_def) 
33175  103 

104 
lemma setsum_restrict_set'': assumes "finite A" 

105 
shows "setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x then f x else 0)" 

106 
unfolding mem_def[of _ P, symmetric] unfolding setsum_restrict_set'[OF assms] .. 

107 

108 
subsection {* Some explicit formulations (from Lars Schewe). *} 

109 

110 
lemma affine: fixes V::"'a::real_vector set" 

111 
shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)" 

112 
unfolding affine_def apply rule apply(rule, rule, rule) apply(erule conjE)+ 

113 
defer apply(rule, rule, rule, rule, rule) proof 

114 
fix x y u v assume as:"x \<in> V" "y \<in> V" "u + v = (1::real)" 

115 
"\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" 

116 
thus "u *\<^sub>R x + v *\<^sub>R y \<in> V" apply(cases "x=y") 

117 
using as(4)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>w. if w = x then u else v"]] and as(13) 

118 
by(auto simp add: scaleR_left_distrib[THEN sym]) 

119 
next 

120 
fix s u assume as:"\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V" 

121 
"finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = (1::real)" 

122 
def n \<equiv> "card s" 

123 
have "card s = 0 \<or> card s = 1 \<or> card s = 2 \<or> card s > 2" by auto 

124 
thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" proof(auto simp only: disjE) 

125 
assume "card s = 2" hence "card s = Suc (Suc 0)" by auto 

126 
then obtain a b where "s = {a, b}" unfolding card_Suc_eq by auto 

127 
thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5) 

128 
by(auto simp add: setsum_clauses(2)) 

129 
next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s) 

130 
case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real" 

131 
assume IA:"\<And>u s. \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s; 

34915  132 
s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n = card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and 
133 
as:"Suc n = card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V" 

33175  134 
"finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1" 
135 
have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr) 

136 
assume " \<not> (\<exists>x\<in>s. u x \<noteq> 1)" hence "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto 

137 
thus False using as(7) and `card s > 2` by (metis Numeral1_eq1_nat less_0_number_of less_int_code(15) 

138 
less_nat_number_of not_less_iff_gr_or_eq of_nat_1 of_nat_eq_iff pos2 rel_simps(4)) qed 

139 
then obtain x where x:"x\<in>s" "u x \<noteq> 1" by auto 

140 

141 
have c:"card (s  {x}) = card s  1" apply(rule card_Diff_singleton) using `x\<in>s` as(4) by auto 

142 
have *:"s = insert x (s  {x})" "finite (s  {x})" using `x\<in>s` and as(4) by auto 

143 
have **:"setsum u (s  {x}) = 1  u x" 

144 
using setsum_clauses(2)[OF *(2), of u x, unfolded *(1)[THEN sym] as(7)] by auto 

145 
have ***:"inverse (1  u x) * setsum u (s  {x}) = 1" unfolding ** using `u x \<noteq> 1` by auto 

146 
have "(\<Sum>xa\<in>s  {x}. (inverse (1  u x) * u xa) *\<^sub>R xa) \<in> V" proof(cases "card (s  {x}) > 2") 

147 
case True hence "s  {x} \<noteq> {}" "card (s  {x}) = n" unfolding c and as(1)[symmetric] proof(rule_tac ccontr) 

148 
assume "\<not> s  {x} \<noteq> {}" hence "card (s  {x}) = 0" unfolding card_0_eq[OF *(2)] by simp 

149 
thus False using True by auto qed auto 

150 
thus ?thesis apply(rule_tac IA[of "s  {x}" "\<lambda>y. (inverse (1  u x) * u y)"]) 

151 
unfolding setsum_right_distrib[THEN sym] using as and *** and True by auto 

152 
next case False hence "card (s  {x}) = Suc (Suc 0)" using as(2) and c by auto 

153 
then obtain a b where "(s  {x}) = {a, b}" "a\<noteq>b" unfolding card_Suc_eq by auto 

154 
thus ?thesis using as(3)[THEN bspec[where x=a], THEN bspec[where x=b]] 

155 
using *** *(2) and `s \<subseteq> V` unfolding setsum_right_distrib by(auto simp add: setsum_clauses(2)) qed 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

156 
hence "u x + (1  u x) = 1 \<Longrightarrow> u x *\<^sub>R x + (1  u x) *\<^sub>R ((\<Sum>xa\<in>s  {x}. u xa *\<^sub>R xa) /\<^sub>R (1  u x)) \<in> V" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

157 
applyapply(rule as(3)[rule_format]) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

158 
unfolding RealVector.scaleR_right.setsum using x(1) as(6) by auto 
33175  159 
thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] 
160 
apply(subst *) unfolding setsum_clauses(2)[OF *(2)] 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

161 
using `u x \<noteq> 1` by auto 
33175  162 
qed auto 
163 
next assume "card s = 1" then obtain a where "s={a}" by(auto simp add: card_Suc_eq) 

164 
thus ?thesis using as(4,5) by simp 

165 
qed(insert `s\<noteq>{}` `finite s`, auto) 

166 
qed 

167 

168 
lemma affine_hull_explicit: 

169 
"affine hull p = {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> setsum (\<lambda>v. (u v) *\<^sub>R v) s = y}" 

170 
apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq and mem_def[of _ affine] 

171 
apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof 

172 
fix x assume "x\<in>p" thus "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" 

173 
apply(rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) by auto 

174 
next 

175 
fix t x s u assume as:"p \<subseteq> t" "affine t" "finite s" "s \<noteq> {}" "s \<subseteq> p" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" 

176 
thus "x \<in> t" using as(2)[unfolded affine, THEN spec[where x=s], THEN spec[where x=u]] by auto 

177 
next 

178 
show "affine {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y}" unfolding affine_def 

179 
apply(rule,rule,rule,rule,rule) unfolding mem_Collect_eq proof 

180 
fix u v ::real assume uv:"u + v = 1" 

181 
fix x assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" 

182 
then obtain sx ux where x:"finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "setsum ux sx = 1" "(\<Sum>v\<in>sx. ux v *\<^sub>R v) = x" by auto 

183 
fix y assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y" 

184 
then obtain sy uy where y:"finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "setsum uy sy = 1" "(\<Sum>v\<in>sy. uy v *\<^sub>R v) = y" by auto 

185 
have xy:"finite (sx \<union> sy)" using x(1) y(1) by auto 

186 
have **:"(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy" by auto 

187 
show "\<exists>s ua. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum ua s = 1 \<and> (\<Sum>v\<in>s. ua v *\<^sub>R v) = u *\<^sub>R x + v *\<^sub>R y" 

188 
apply(rule_tac x="sx \<union> sy" in exI) 

189 
apply(rule_tac x="\<lambda>a. (if a\<in>sx then u * ux a else 0) + (if a\<in>sy then v * uy a else 0)" in exI) 

190 
unfolding scaleR_left_distrib setsum_addf if_smult scaleR_zero_left ** setsum_restrict_set[OF xy, THEN sym] 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

191 
unfolding scaleR_scaleR[THEN sym] RealVector.scaleR_right.setsum [symmetric] and setsum_right_distrib[THEN sym] 
33175  192 
unfolding x y using x(13) y(13) uv by simp qed qed 
193 

194 
lemma affine_hull_finite: 

195 
assumes "finite s" 

196 
shows "affine hull s = {y. \<exists>u. setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" 

197 
unfolding affine_hull_explicit and expand_set_eq and mem_Collect_eq apply (rule,rule) 

198 
apply(erule exE)+ apply(erule conjE)+ defer apply(erule exE) apply(erule conjE) proof 

199 
fix x u assume "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" 

200 
thus "\<exists>sa u. finite sa \<and> \<not> (\<forall>x. (x \<in> sa) = (x \<in> {})) \<and> sa \<subseteq> s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = x" 

201 
apply(rule_tac x=s in exI, rule_tac x=u in exI) using assms by auto 

202 
next 

203 
fix x t u assume "t \<subseteq> s" hence *:"s \<inter> t = t" by auto 

204 
assume "finite t" "\<not> (\<forall>x. (x \<in> t) = (x \<in> {}))" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x" 

205 
thus "\<exists>u. setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI) 

206 
unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms, THEN sym] and * by auto qed 

207 

208 
subsection {* Stepping theorems and hence small special cases. *} 

209 

210 
lemma affine_hull_empty[simp]: "affine hull {} = {}" 

211 
apply(rule hull_unique) unfolding mem_def by auto 

212 

213 
lemma affine_hull_finite_step: 

214 
fixes y :: "'a::real_vector" 

215 
shows "(\<exists>u. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1) 

216 
"finite s \<Longrightarrow> (\<exists>u. setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y) \<longleftrightarrow> 

217 
(\<exists>v u. setsum u s = w  v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y  v *\<^sub>R a)" (is "?as \<Longrightarrow> (?lhs = ?rhs)") 

218 
proof 

219 
show ?th1 by simp 

220 
assume ?as 

221 
{ assume ?lhs 

222 
then obtain u where u:"setsum u (insert a s) = w \<and> (\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto 

223 
have ?rhs proof(cases "a\<in>s") 

224 
case True hence *:"insert a s = s" by auto 

225 
show ?thesis using u[unfolded *] apply(rule_tac x=0 in exI) by auto 

226 
next 

227 
case False thus ?thesis apply(rule_tac x="u a" in exI) using u and `?as` by auto 

228 
qed } moreover 

229 
{ assume ?rhs 

230 
then obtain v u where vu:"setsum u s = w  v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y  v *\<^sub>R a" by auto 

231 
have *:"\<And>x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)" by auto 

232 
have ?lhs proof(cases "a\<in>s") 

233 
case True thus ?thesis 

234 
apply(rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI) 

235 
unfolding setsum_clauses(2)[OF `?as`] apply simp 

236 
unfolding scaleR_left_distrib and setsum_addf 

237 
unfolding vu and * and scaleR_zero_left 

238 
by (auto simp add: setsum_delta[OF `?as`]) 

239 
next 

240 
case False 

241 
hence **:"\<And>x. x \<in> s \<Longrightarrow> u x = (if x = a then v else u x)" 

242 
"\<And>x. x \<in> s \<Longrightarrow> u x *\<^sub>R x = (if x = a then v *\<^sub>R x else u x *\<^sub>R x)" by auto 

243 
from False show ?thesis 

244 
apply(rule_tac x="\<lambda>x. if x=a then v else u x" in exI) 

245 
unfolding setsum_clauses(2)[OF `?as`] and * using vu 

246 
using setsum_cong2[of s "\<lambda>x. u x *\<^sub>R x" "\<lambda>x. if x = a then v *\<^sub>R x else u x *\<^sub>R x", OF **(2)] 

247 
using setsum_cong2[of s u "\<lambda>x. if x = a then v else u x", OF **(1)] by auto 

248 
qed } 

249 
ultimately show "?lhs = ?rhs" by blast 

250 
qed 

251 

252 
lemma affine_hull_2: 

253 
fixes a b :: "'a::real_vector" 

254 
shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b u v. (u + v = 1)}" (is "?lhs = ?rhs") 

255 
proof 

256 
have *:"\<And>x y z. z = x  y \<longleftrightarrow> y + z = (x::real)" 

257 
"\<And>x y z. z = x  y \<longleftrightarrow> y + z = (x::'a)" by auto 

258 
have "?lhs = {y. \<exists>u. setsum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}" 

259 
using affine_hull_finite[of "{a,b}"] by auto 

260 
also have "\<dots> = {y. \<exists>v u. u b = 1  v \<and> u b *\<^sub>R b = y  v *\<^sub>R a}" 

261 
by(simp add: affine_hull_finite_step(2)[of "{b}" a]) 

262 
also have "\<dots> = ?rhs" unfolding * by auto 

263 
finally show ?thesis by auto 

264 
qed 

265 

266 
lemma affine_hull_3: 

267 
fixes a b c :: "'a::real_vector" 

268 
shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c u v w. u + v + w = 1}" (is "?lhs = ?rhs") 

269 
proof 

270 
have *:"\<And>x y z. z = x  y \<longleftrightarrow> y + z = (x::real)" 

271 
"\<And>x y z. z = x  y \<longleftrightarrow> y + z = (x::'a)" by auto 

272 
show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step) 

273 
unfolding * apply auto 

274 
apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto 

275 
apply(rule_tac x=u in exI) by(auto intro!: exI) 

276 
qed 

277 

278 
subsection {* Some relations between affine hull and subspaces. *} 

279 

280 
lemma affine_hull_insert_subset_span: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

281 
fixes a :: "'a::euclidean_space" 
33175  282 
shows "affine hull (insert a s) \<subseteq> {a + v v . v \<in> span {x  a  x . x \<in> s}}" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

283 
unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq 
33175  284 
apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof 
285 
fix x t u assume as:"finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x" 

286 
have "(\<lambda>x. x  a) ` (t  {a}) \<subseteq> {x  a x. x \<in> s}" using as(3) by auto 

287 
thus "\<exists>v. x = a + v \<and> (\<exists>S u. finite S \<and> S \<subseteq> {x  a x. x \<in> s} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = v)" 

288 
apply(rule_tac x="x  a" in exI) 

289 
apply (rule conjI, simp) 

290 
apply(rule_tac x="(\<lambda>x. x  a) ` (t  {a})" in exI) 

291 
apply(rule_tac x="\<lambda>x. u (x + a)" in exI) 

292 
apply (rule conjI) using as(1) apply simp 

293 
apply (erule conjI) 

294 
using as(1) 

295 
apply (simp add: setsum_reindex[unfolded inj_on_def] scaleR_right_diff_distrib setsum_subtractf scaleR_left.setsum[THEN sym] setsum_diff1 scaleR_left_diff_distrib) 

296 
unfolding as by simp qed 

297 

298 
lemma affine_hull_insert_span: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

299 
fixes a :: "'a::euclidean_space" 
33175  300 
assumes "a \<notin> s" 
301 
shows "affine hull (insert a s) = 

302 
{a + v  v . v \<in> span {x  a  x. x \<in> s}}" 

303 
apply(rule, rule affine_hull_insert_subset_span) unfolding subset_eq Ball_def 

304 
unfolding affine_hull_explicit and mem_Collect_eq proof(rule,rule,erule exE,erule conjE) 

305 
fix y v assume "y = a + v" "v \<in> span {x  a x. x \<in> s}" 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

306 
then obtain t u where obt:"finite t" "t \<subseteq> {x  a x. x \<in> s}" "a + (\<Sum>v\<in>t. u v *\<^sub>R v) = y" unfolding span_explicit by auto 
33175  307 
def f \<equiv> "(\<lambda>x. x + a) ` t" 
308 
have f:"finite f" "f \<subseteq> s" "(\<Sum>v\<in>f. u (v  a) *\<^sub>R (v  a)) = y  a" unfolding f_def using obt 

309 
by(auto simp add: setsum_reindex[unfolded inj_on_def]) 

310 
have *:"f \<inter> {a} = {}" "f \<inter>  {a} = f" using f(2) assms by auto 

311 
show "\<exists>sa u. finite sa \<and> sa \<noteq> {} \<and> sa \<subseteq> insert a s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y" 

312 
apply(rule_tac x="insert a f" in exI) 

313 
apply(rule_tac x="\<lambda>x. if x=a then 1  setsum (\<lambda>x. u (x  a)) f else u (x  a)" in exI) 

314 
using assms and f unfolding setsum_clauses(2)[OF f(1)] and if_smult 

35577  315 
unfolding setsum_cases[OF f(1), of "\<lambda>x. x = a"] 
316 
by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *) qed 

33175  317 

318 
lemma affine_hull_span: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

319 
fixes a :: "'a::euclidean_space" 
33175  320 
assumes "a \<in> s" 
321 
shows "affine hull s = {a + v  v. v \<in> span {x  a  x. x \<in> s  {a}}}" 

322 
using affine_hull_insert_span[of a "s  {a}", unfolded insert_Diff[OF assms]] by auto 

323 

324 
subsection {* Cones. *} 

325 

326 
definition 

327 
cone :: "'a::real_vector set \<Rightarrow> bool" where 

328 
"cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)" 

329 

330 
lemma cone_empty[intro, simp]: "cone {}" 

331 
unfolding cone_def by auto 

332 

333 
lemma cone_univ[intro, simp]: "cone UNIV" 

334 
unfolding cone_def by auto 

335 

336 
lemma cone_Inter[intro]: "(\<forall>s\<in>f. cone s) \<Longrightarrow> cone(\<Inter> f)" 

337 
unfolding cone_def by auto 

338 

339 
subsection {* Conic hull. *} 

340 

341 
lemma cone_cone_hull: "cone (cone hull s)" 

342 
unfolding hull_def using cone_Inter[of "{t \<in> conic. s \<subseteq> t}"] 

343 
by (auto simp add: mem_def) 

344 

345 
lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s" 

346 
apply(rule hull_eq[unfolded mem_def]) 

347 
using cone_Inter unfolding subset_eq by (auto simp add: mem_def) 

348 

349 
subsection {* Affine dependence and consequential theorems (from Lars Schewe). *} 

350 

351 
definition 

352 
affine_dependent :: "'a::real_vector set \<Rightarrow> bool" where 

353 
"affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> (affine hull (s  {x})))" 

354 

355 
lemma affine_dependent_explicit: 

356 
"affine_dependent p \<longleftrightarrow> 

357 
(\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and> 

358 
(\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)" 

359 
unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq apply(rule) 

360 
apply(erule bexE,erule exE,erule exE) apply(erule conjE)+ defer apply(erule exE,erule exE) apply(erule conjE)+ apply(erule bexE) 

361 
proof 

362 
fix x s u assume as:"x \<in> p" "finite s" "s \<noteq> {}" "s \<subseteq> p  {x}" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" 

363 
have "x\<notin>s" using as(1,4) by auto 

364 
show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0" 

365 
apply(rule_tac x="insert x s" in exI, rule_tac x="\<lambda>v. if v = x then  1 else u v" in exI) 

366 
unfolding if_smult and setsum_clauses(2)[OF as(2)] and setsum_delta_notmem[OF `x\<notin>s`] and as using as by auto 

367 
next 

368 
fix s u v assume as:"finite s" "s \<subseteq> p" "setsum u s = 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" "v \<in> s" "u v \<noteq> 0" 

369 
have "s \<noteq> {v}" using as(3,6) by auto 

370 
thus "\<exists>x\<in>p. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p  {x} \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" 

371 
apply(rule_tac x=v in bexI, rule_tac x="s  {v}" in exI, rule_tac x="\<lambda>x.  (1 / u v) * u x" in exI) 

372 
unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)] using as by auto 

373 
qed 

374 

375 
lemma affine_dependent_explicit_finite: 

376 
fixes s :: "'a::real_vector set" assumes "finite s" 

377 
shows "affine_dependent s \<longleftrightarrow> (\<exists>u. setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)" 

378 
(is "?lhs = ?rhs") 

379 
proof 

380 
have *:"\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))" by auto 

381 
assume ?lhs 

382 
then obtain t u v where "finite t" "t \<subseteq> s" "setsum u t = 0" "v\<in>t" "u v \<noteq> 0" "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0" 

383 
unfolding affine_dependent_explicit by auto 

384 
thus ?rhs apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI) 

385 
apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym] 

386 
unfolding Int_absorb1[OF `t\<subseteq>s`] by auto 

387 
next 

388 
assume ?rhs 

389 
then obtain u v where "setsum u s = 0" "v\<in>s" "u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" by auto 

390 
thus ?lhs unfolding affine_dependent_explicit using assms by auto 

391 
qed 

392 

393 
subsection {* A general lemma. *} 

394 

395 
lemma convex_connected: 

396 
fixes s :: "'a::real_normed_vector set" 

397 
assumes "convex s" shows "connected s" 

398 
proof 

399 
{ fix e1 e2 assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2" 

400 
assume "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}" 

401 
then obtain x1 x2 where x1:"x1\<in>e1" "x1\<in>s" and x2:"x2\<in>e2" "x2\<in>s" by auto 

402 
hence n:"norm (x1  x2) > 0" unfolding zero_less_norm_iff using as(3) by auto 

403 

404 
{ fix x e::real assume as:"0 \<le> x" "x \<le> 1" "0 < e" 

405 
{ 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" 

406 
by (simp add: algebra_simps) 

407 
assume "\<bar>y  x\<bar> < e / norm (x1  x2)" 

408 
hence "norm ((1  x) *\<^sub>R x1 + x *\<^sub>R x2  ((1  y) *\<^sub>R x1 + y *\<^sub>R x2)) < e" 

409 
unfolding * and scaleR_right_diff_distrib[THEN sym] 

410 
unfolding less_divide_eq using n by auto } 

411 
hence "\<exists>d>0. \<forall>y. \<bar>y  x\<bar> < d \<longrightarrow> norm ((1  x) *\<^sub>R x1 + x *\<^sub>R x2  ((1  y) *\<^sub>R x1 + y *\<^sub>R x2)) < e" 

412 
apply(rule_tac x="e / norm (x1  x2)" in exI) using as 

413 
apply auto unfolding zero_less_divide_iff using n by simp } note * = this 

414 

415 
have "\<exists>x\<ge>0. x \<le> 1 \<and> (1  x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1 \<and> (1  x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2" 

416 
apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+ 

417 
using * apply(simp add: dist_norm) 

418 
using as(1,2)[unfolded open_dist] apply simp 

419 
using as(1,2)[unfolded open_dist] apply simp 

420 
using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2 

421 
using as(3) by auto 

422 
then obtain x where "x\<ge>0" "x\<le>1" "(1  x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1" "(1  x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2" by auto 

423 
hence False using as(4) 

424 
using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] 

425 
using x1(2) x2(2) by auto } 

426 
thus ?thesis unfolding connected_def by auto 

427 
qed 

428 

429 
subsection {* One rather trivial consequence. *} 

430 

34964  431 
lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)" 
33175  432 
by(simp add: convex_connected convex_UNIV) 
433 

36623  434 
subsection {* Balls, being convex, are connected. *} 
33175  435 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

436 
lemma convex_box: fixes a::"'a::euclidean_space" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

437 
assumes "\<And>i. i<DIM('a) \<Longrightarrow> convex {x. P i x}" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

438 
shows "convex {x. \<forall>i<DIM('a). P i (x$$i)}" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

439 
using assms unfolding convex_def by(auto simp add:euclidean_simps) 
33175  440 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

441 
lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\<forall>i<DIM('a). 0 \<le> x$$i)}" 
36623  442 
by (rule convex_box) (simp add: atLeast_def[symmetric] convex_real_interval) 
33175  443 

444 
lemma convex_local_global_minimum: 

445 
fixes s :: "'a::real_normed_vector set" 

446 
assumes "0<e" "convex_on s f" "ball x e \<subseteq> s" "\<forall>y\<in>ball x e. f x \<le> f y" 

447 
shows "\<forall>y\<in>s. f x \<le> f y" 

448 
proof(rule ccontr) 

449 
have "x\<in>s" using assms(1,3) by auto 

450 
assume "\<not> (\<forall>y\<in>s. f x \<le> f y)" 

451 
then obtain y where "y\<in>s" and y:"f x > f y" by auto 

452 
hence xy:"0 < dist x y" by (auto simp add: dist_nz[THEN sym]) 

453 

454 
then obtain u where "0 < u" "u \<le> 1" and u:"u < e / dist x y" 

455 
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 

456 
hence "f ((1u) *\<^sub>R x + u *\<^sub>R y) \<le> (1u) * f x + u * f y" using `x\<in>s` `y\<in>s` 

457 
using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1u"]] by auto 

458 
moreover 

459 
have *:"x  ((1  u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x  y)" by (simp add: algebra_simps) 

460 
have "(1  u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0<u`] unfolding dist_norm[THEN sym] 

461 
using u unfolding pos_less_divide_eq[OF xy] by auto 

462 
hence "f x \<le> f ((1  u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto 

463 
ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto 

464 
qed 

465 

466 
lemma convex_ball: 

467 
fixes x :: "'a::real_normed_vector" 

468 
shows "convex (ball x e)" 

469 
proof(auto simp add: convex_def) 

470 
fix y z assume yz:"dist x y < e" "dist x z < e" 

471 
fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1" 

472 
have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz 

473 
using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto 

36623  474 
thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using convex_bound_lt[OF yz uv] by auto 
33175  475 
qed 
476 

477 
lemma convex_cball: 

478 
fixes x :: "'a::real_normed_vector" 

479 
shows "convex(cball x e)" 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36341
diff
changeset

480 
proof(auto simp add: convex_def Ball_def) 
33175  481 
fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e" 
482 
fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1" 

483 
have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz 

484 
using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto 

36623  485 
thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using convex_bound_le[OF yz uv] by auto 
33175  486 
qed 
487 

488 
lemma connected_ball: 

489 
fixes x :: "'a::real_normed_vector" 

490 
shows "connected (ball x e)" 

491 
using convex_connected convex_ball by auto 

492 

493 
lemma connected_cball: 

494 
fixes x :: "'a::real_normed_vector" 

495 
shows "connected(cball x e)" 

496 
using convex_connected convex_cball by auto 

497 

498 
subsection {* Convex hull. *} 

499 

500 
lemma convex_convex_hull: "convex(convex hull s)" 

501 
unfolding hull_def using convex_Inter[of "{t\<in>convex. s\<subseteq>t}"] 

502 
unfolding mem_def by auto 

503 

34064
eee04bbbae7e
avoid dependency on implicit dest rule predicate1D in proofs
haftmann
parents:
33758
diff
changeset

504 
lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s" 
36071  505 
by (metis convex_convex_hull hull_same mem_def) 
33175  506 

507 
lemma bounded_convex_hull: 

508 
fixes s :: "'a::real_normed_vector set" 

509 
assumes "bounded s" shows "bounded(convex hull s)" 

510 
proof from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto 

511 
show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B]) 

512 
unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball] 

513 
unfolding subset_eq mem_cball dist_norm using B by auto qed 

514 

515 
lemma finite_imp_bounded_convex_hull: 

516 
fixes s :: "'a::real_normed_vector set" 

517 
shows "finite s \<Longrightarrow> bounded(convex hull s)" 

518 
using bounded_convex_hull finite_imp_bounded by auto 

519 

520 
subsection {* Stepping theorems for convex hulls of finite sets. *} 

521 

522 
lemma convex_hull_empty[simp]: "convex hull {} = {}" 

523 
apply(rule hull_unique) unfolding mem_def by auto 

524 

525 
lemma convex_hull_singleton[simp]: "convex hull {a} = {a}" 

526 
apply(rule hull_unique) unfolding mem_def by auto 

527 

528 
lemma convex_hull_insert: 

529 
fixes s :: "'a::real_vector set" 

530 
assumes "s \<noteq> {}" 

531 
shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and> 

532 
b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull") 

533 
apply(rule,rule hull_minimal,rule) unfolding mem_def[of _ convex] and insert_iff prefer 3 apply rule proof 

534 
fix x assume x:"x = a \<or> x \<in> s" 

535 
thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer 

536 
apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto 

537 
next 

538 
fix x assume "x\<in>?hull" 

539 
then obtain u v b where obt:"u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b" by auto 

540 
have "a\<in>convex hull insert a s" "b\<in>convex hull insert a s" 

541 
using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) by auto 

542 
thus "x\<in> convex hull insert a s" unfolding obt(5) using convex_convex_hull[of "insert a s", unfolded convex_def] 

543 
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 

544 
next 

545 
show "convex ?hull" unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof 

546 
fix x y u v assume as:"(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull" 

547 
from as(4) obtain u1 v1 b1 where obt1:"u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto 

548 
from as(5) obtain u2 v2 b2 where obt2:"u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto 

549 
have *:"\<And>(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) 

550 
have "\<exists>b \<in> 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)" 

551 
proof(cases "u * v1 + v * v2 = 0") 

552 
have *:"\<And>(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) 

36071  553 
case True hence **:"u * v1 = 0" "v * v2 = 0" 
554 
using mult_nonneg_nonneg[OF `u\<ge>0` `v1\<ge>0`] mult_nonneg_nonneg[OF `v\<ge>0` `v2\<ge>0`] by arith+ 

33175  555 
hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto 
556 
thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: ** scaleR_right_distrib) 

557 
next 

558 
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) 

559 
also have "\<dots> = u * (v1 + u1  u1) + v * (v2 + u2  u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) 

560 
also have "\<dots> = u * v1 + v * v2" by simp finally have **:"1  (u * u1 + v * u2) = u * v1 + v * v2" by auto 

561 
case False have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2" apply  

562 
apply(rule add_nonneg_nonneg) prefer 4 apply(rule add_nonneg_nonneg) apply(rule_tac [!] mult_nonneg_nonneg) 

563 
using as(1,2) obt1(1,2) obt2(1,2) by auto 

564 
thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False 

565 
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 

566 
apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4) 

567 
unfolding add_divide_distrib[THEN sym] and real_0_le_divide_iff 

568 
by (auto simp add: scaleR_left_distrib scaleR_right_distrib) 

569 
qed note * = this 

36071  570 
have u1:"u1 \<le> 1" unfolding obt1(3)[THEN sym] and not_le using obt1(2) by auto 
571 
have u2:"u2 \<le> 1" unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto 

33175  572 
have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono) 
573 
apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto 

574 
also have "\<dots> \<le> 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto 

575 
finally 

576 
show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI) 

577 
apply(rule conjI) defer apply(rule_tac x="1  u * u1  v * u2" in exI) unfolding Bex_def 

578 
using as(1,2) obt1(1,2) obt2(1,2) * by(auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps) 

579 
qed 

580 
qed 

581 

582 

583 
subsection {* Explicit expression for convex hull. *} 

584 

585 
lemma convex_hull_indexed: 

586 
fixes s :: "'a::real_vector set" 

587 
shows "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and> 

588 
(setsum u {1..k} = 1) \<and> 

589 
(setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull") 

590 
apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer 

591 
apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule) 

592 
proof 

593 
fix x assume "x\<in>s" 

594 
thus "x \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI) by auto 

595 
next 

596 
fix t assume as:"s \<subseteq> t" "convex t" 

597 
show "?hull \<subseteq> t" apply(rule) unfolding mem_Collect_eq apply(erule exE  erule conjE)+ proof 

598 
fix x k u y assume assm:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> s" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x" 

599 
show "x\<in>t" unfolding assm(3)[THEN sym] apply(rule as(2)[unfolded convex, rule_format]) 

600 
using assm(1,2) as(1) by auto qed 

601 
next 

602 
fix x y u v assume uv:"0\<le>u" "0\<le>v" "u+v=(1::real)" and xy:"x\<in>?hull" "y\<in>?hull" 

603 
from xy obtain k1 u1 x1 where x:"\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto 

604 
from xy obtain k2 u2 x2 where y:"\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto 

605 
have *:"\<And>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)" 

606 
"{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter>  {1..k1} = (\<lambda>i. i + k1) ` {1..k2}" 

607 
prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x  k1" in bexI) by(auto simp add: not_le) 

608 
have inj:"inj_on (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto 

609 
show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" apply(rule) 

610 
apply(rule_tac x="k1 + k2" in exI, rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i  k1)" in exI) 

611 
apply(rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i  k1)" in exI) apply(rule,rule) defer apply(rule) 

35577  612 
unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def Collect_mem_eq 
33175  613 
unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] setsum_right_distrib[THEN sym] proof 
614 
fix i assume i:"i \<in> {1..k1+k2}" 

615 
show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i  k1)) \<and> (if i \<in> {1..k1} then x1 i else x2 (i  k1)) \<in> s" 

616 
proof(cases "i\<in>{1..k1}") 

617 
case True thus ?thesis using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto 

618 
next def j \<equiv> "i  k1" 

619 
case False with i have "j \<in> {1..k2}" unfolding j_def by auto 

620 
thus ?thesis unfolding j_def[symmetric] using False 

621 
using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]] by auto qed 

622 
qed(auto simp add: not_le x(2,3) y(2,3) uv(3)) 

623 
qed 

624 

625 
lemma convex_hull_finite: 

626 
fixes s :: "'a::real_vector set" 

627 
assumes "finite s" 

628 
shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> 

629 
setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set") 

630 
proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set]) 

631 
fix x assume "x\<in>s" thus " \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x" 

632 
apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto 

633 
unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto 

634 
next 

635 
fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1" 

636 
fix ux assume ux:"\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)" 

637 
fix uy assume uy:"\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)" 

638 
{ fix x assume "x\<in>s" 

639 
hence "0 \<le> 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) 

640 
by (auto, metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2)) } 

641 
moreover have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1" 

642 
unfolding setsum_addf and setsum_right_distrib[THEN sym] and ux(2) uy(2) using uv(3) by auto 

643 
moreover have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)" 

644 
unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] by auto 

645 
ultimately show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and> (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)" 

646 
apply(rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI) by auto 

647 
next 

648 
fix t assume t:"s \<subseteq> t" "convex t" 

649 
fix u assume u:"\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)" 

650 
thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]] 

651 
using assms and t(1) by auto 

652 
qed 

653 

654 
subsection {* Another formulation from Lars Schewe. *} 

655 

656 
lemma setsum_constant_scaleR: 

657 
fixes y :: "'a::real_vector" 

658 
shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y" 

659 
apply (cases "finite A") 

660 
apply (induct set: finite) 

661 
apply (simp_all add: algebra_simps) 

662 
done 

663 

664 
lemma convex_hull_explicit: 

665 
fixes p :: "'a::real_vector set" 

666 
shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> 

667 
(\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs") 

668 
proof 

669 
{ fix x assume "x\<in>?lhs" 

670 
then obtain k u y where obt:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> p" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x" 

671 
unfolding convex_hull_indexed by auto 

672 

673 
have fin:"finite {1..k}" by auto 

674 
have fin':"\<And>v. finite {i \<in> {1..k}. y i = v}" by auto 

675 
{ fix j assume "j\<in>{1..k}" 

676 
hence "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> y i = y j}" 

677 
using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp 

678 
apply(rule setsum_nonneg) using obt(1) by auto } 

679 
moreover 

680 
have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v}) = 1" 

681 
unfolding setsum_image_gen[OF fin, THEN sym] using obt(2) by auto 

682 
moreover have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v} *\<^sub>R v) = x" 

683 
using setsum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, THEN sym] 

684 
unfolding scaleR_left.setsum using obt(3) by auto 

685 
ultimately have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" 

686 
apply(rule_tac x="y ` {1..k}" in exI) 

687 
apply(rule_tac x="\<lambda>v. setsum u {i\<in>{1..k}. y i = v}" in exI) by auto 

688 
hence "x\<in>?rhs" by auto } 

689 
moreover 

690 
{ fix y assume "y\<in>?rhs" 

691 
then obtain s u where obt:"finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto 

692 

693 
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 

694 

695 
{ fix i::nat assume "i\<in>{1..card s}" 

696 
hence "f i \<in> s" apply(subst f(2)[THEN sym]) by auto 

697 
hence "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto } 

698 
moreover have *:"finite {1..card s}" by auto 

699 
{ fix y assume "y\<in>s" 

700 
then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto 

701 
hence "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] apply(erule_tac x=x in ballE) by auto 

702 
hence "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto 

703 
hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y" 

704 
"(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y" 

705 
by (auto simp add: setsum_constant_scaleR) } 

706 

707 
hence "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y" 

708 
unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f] 

709 
unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"] 

710 
using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto 

711 

712 
ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y" 

713 
apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastsimp 

714 
hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto } 

715 
ultimately show ?thesis unfolding expand_set_eq by blast 

716 
qed 

717 

718 
subsection {* A stepping theorem for that expansion. *} 

719 

720 
lemma convex_hull_finite_step: 

721 
fixes s :: "'a::real_vector set" assumes "finite s" 

722 
shows "(\<exists>u. (\<forall>x\<in>insert a s. 0 \<le> u x) \<and> setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y) 

723 
\<longleftrightarrow> (\<exists>v\<ge>0. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = w  v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y  v *\<^sub>R a)" (is "?lhs = ?rhs") 

724 
proof(rule, case_tac[!] "a\<in>s") 

725 
assume "a\<in>s" hence *:"insert a s = s" by auto 

726 
assume ?lhs thus ?rhs unfolding * apply(rule_tac x=0 in exI) by auto 

727 
next 

728 
assume ?lhs then obtain u where u:"\<forall>x\<in>insert a s. 0 \<le> u x" "setsum u (insert a s) = w" "(\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto 

729 
assume "a\<notin>s" thus ?rhs apply(rule_tac x="u a" in exI) using u(1)[THEN bspec[where x=a]] apply simp 

730 
apply(rule_tac x=u in exI) using u[unfolded setsum_clauses(2)[OF assms]] and `a\<notin>s` by auto 

731 
next 

732 
assume "a\<in>s" hence *:"insert a s = s" by auto 

733 
have fin:"finite (insert a s)" using assms by auto 

734 
assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w  v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y  v *\<^sub>R a" by auto 

735 
show ?lhs apply(rule_tac x="\<lambda>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] 

736 
unfolding setsum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and `a\<in>s` by auto 

737 
next 

738 
assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w  v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y  v *\<^sub>R a" by auto 

739 
moreover assume "a\<notin>s" moreover have "(\<Sum>x\<in>s. if a = x then v else u x) = setsum u s" "(\<Sum>x\<in>s. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)" 

740 
apply(rule_tac setsum_cong2) defer apply(rule_tac setsum_cong2) using `a\<notin>s` by auto 

741 
ultimately show ?lhs apply(rule_tac x="\<lambda>x. if a = x then v else u x" in exI) unfolding setsum_clauses(2)[OF assms] by auto 

742 
qed 

743 

744 
subsection {* Hence some special cases. *} 

745 

746 
lemma convex_hull_2: 

747 
"convex hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b  u v. 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1}" 

748 
proof have *:"\<And>u. (\<forall>x\<in>{a, b}. 0 \<le> u x) \<longleftrightarrow> 0 \<le> u a \<and> 0 \<le> u b" by auto have **:"finite {b}" by auto 

749 
show ?thesis apply(simp add: convex_hull_finite) unfolding convex_hull_finite_step[OF **, of a 1, unfolded * conj_assoc] 

750 
apply auto apply(rule_tac x=v in exI) apply(rule_tac x="1  v" in exI) apply simp 

751 
apply(rule_tac x=u in exI) apply simp apply(rule_tac x="\<lambda>x. v" in exI) by simp qed 

752 

753 
lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *\<^sub>R (b  a)  u. 0 \<le> u \<and> u \<le> 1}" 

754 
unfolding convex_hull_2 unfolding Collect_def 

755 
proof(rule ext) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1  y" by auto 

756 
fix x show "(\<exists>v u. x = v *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> v \<and> 0 \<le> u \<and> v + u = 1) = (\<exists>u. x = a + u *\<^sub>R (b  a) \<and> 0 \<le> u \<and> u \<le> 1)" 

757 
unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed 

758 

759 
lemma convex_hull_3: 

760 
"convex hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c  u v w. 0 \<le> u \<and> 0 \<le> v \<and> 0 \<le> w \<and> u + v + w = 1}" 

761 
proof 

762 
have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto 

763 
have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1  y  z" 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

764 
"\<And>x y z ::_::euclidean_space. x + y + z = 1 \<longleftrightarrow> x = 1  y  z" by (auto simp add: field_simps) 
33175  765 
show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and * 
766 
unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto 

767 
apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp 

768 
apply(rule_tac x="1  v  w" in exI) apply simp apply(rule_tac x=v in exI) apply simp apply(rule_tac x="\<lambda>x. w" in exI) by simp qed 

769 

770 
lemma convex_hull_3_alt: 

771 
"convex hull {a,b,c} = {a + u *\<^sub>R (b  a) + v *\<^sub>R (c  a)  u v. 0 \<le> u \<and> 0 \<le> v \<and> u + v \<le> 1}" 

772 
proof have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1  y  z" by auto 

773 
show ?thesis unfolding convex_hull_3 apply (auto simp add: *) apply(rule_tac x=v in exI) apply(rule_tac x=w in exI) apply (simp add: algebra_simps) 

774 
apply(rule_tac x=u in exI) apply(rule_tac x=v in exI) by (simp add: algebra_simps) qed 

775 

776 
subsection {* Relations among closure notions and corresponding hulls. *} 

777 

778 
text {* TODO: Generalize linear algebra concepts defined in @{text 

779 
Euclidean_Space.thy} so that we can generalize these lemmas. *} 

780 

781 
lemma subspace_imp_affine: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

782 
fixes s :: "(_::euclidean_space) set" shows "subspace s \<Longrightarrow> affine s" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

783 
unfolding subspace_def affine_def by auto 
33175  784 

785 
lemma affine_imp_convex: "affine s \<Longrightarrow> convex s" 

786 
unfolding affine_def convex_def by auto 

787 

788 
lemma subspace_imp_convex: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

789 
fixes s :: "(_::euclidean_space) set" shows "subspace s \<Longrightarrow> convex s" 
33175  790 
using subspace_imp_affine affine_imp_convex by auto 
791 

792 
lemma affine_hull_subset_span: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

793 
fixes s :: "(_::euclidean_space) set" shows "(affine hull s) \<subseteq> (span s)" 
36071  794 
by (metis hull_minimal mem_def span_inc subspace_imp_affine subspace_span) 
33175  795 

796 
lemma convex_hull_subset_span: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

797 
fixes s :: "(_::euclidean_space) set" shows "(convex hull s) \<subseteq> (span s)" 
36071  798 
by (metis hull_minimal mem_def span_inc subspace_imp_convex subspace_span) 
33175  799 

800 
lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)" 

36071  801 
by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset mem_def) 
802 

33175  803 

804 
lemma affine_dependent_imp_dependent: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

805 
fixes s :: "(_::euclidean_space) set" shows "affine_dependent s \<Longrightarrow> dependent s" 
33175  806 
unfolding affine_dependent_def dependent_def 
807 
using affine_hull_subset_span by auto 

808 

809 
lemma dependent_imp_affine_dependent: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

810 
fixes s :: "(_::euclidean_space) set" 
33175  811 
assumes "dependent {x  a x . x \<in> s}" "a \<notin> s" 
812 
shows "affine_dependent (insert a s)" 

813 
proof 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

814 
from assms(1)[unfolded dependent_explicit] obtain S u v 
33175  815 
where obt:"finite S" "S \<subseteq> {x  a x. x \<in> s}" "v\<in>S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0" by auto 
816 
def t \<equiv> "(\<lambda>x. x + a) ` S" 

817 

818 
have inj:"inj_on (\<lambda>x. x + a) S" unfolding inj_on_def by auto 

819 
have "0\<notin>S" using obt(2) assms(2) unfolding subset_eq by auto 

820 
have fin:"finite t" and "t\<subseteq>s" unfolding t_def using obt(1,2) by auto 

821 

822 
hence "finite (insert a t)" and "insert a t \<subseteq> insert a s" by auto 

823 
moreover have *:"\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x)) = (\<Sum>x\<in>t. Q x)" 

824 
apply(rule setsum_cong2) using `a\<notin>s` `t\<subseteq>s` by auto 

825 
have "(\<Sum>x\<in>insert a t. if x = a then  (\<Sum>x\<in>t. u (x  a)) else u (x  a)) = 0" 

826 
unfolding setsum_clauses(2)[OF fin] using `a\<notin>s` `t\<subseteq>s` apply auto unfolding * by auto 

827 
moreover have "\<exists>v\<in>insert a t. (if v = a then  (\<Sum>x\<in>t. u (x  a)) else u (v  a)) \<noteq> 0" 

828 
apply(rule_tac x="v + a" in bexI) using obt(3,4) and `0\<notin>S` unfolding t_def by auto 

829 
moreover have *:"\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x) *\<^sub>R x) = (\<Sum>x\<in>t. Q x *\<^sub>R x)" 

830 
apply(rule setsum_cong2) using `a\<notin>s` `t\<subseteq>s` by auto 

831 
have "(\<Sum>x\<in>t. u (x  a)) *\<^sub>R a = (\<Sum>v\<in>t. u (v  a) *\<^sub>R v)" 

832 
unfolding scaleR_left.setsum unfolding t_def and setsum_reindex[OF inj] and o_def 

833 
using obt(5) by (auto simp add: setsum_addf scaleR_right_distrib) 

834 
hence "(\<Sum>v\<in>insert a t. (if v = a then  (\<Sum>x\<in>t. u (x  a)) else u (v  a)) *\<^sub>R v) = 0" 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

835 
unfolding setsum_clauses(2)[OF fin] using `a\<notin>s` `t\<subseteq>s` by (auto simp add: *) 
33175  836 
ultimately show ?thesis unfolding affine_dependent_explicit 
837 
apply(rule_tac x="insert a t" in exI) by auto 

838 
qed 

839 

840 
lemma convex_cone: 

841 
"convex s \<and> cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. (x + y) \<in> s) \<and> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)" (is "?lhs = ?rhs") 

842 
proof 

843 
{ fix x y assume "x\<in>s" "y\<in>s" and ?lhs 

844 
hence "2 *\<^sub>R x \<in>s" "2 *\<^sub>R y \<in> s" unfolding cone_def by auto 

845 
hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1] 

846 
apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE) 

847 
apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto } 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36341
diff
changeset

848 
thus ?thesis unfolding convex_def cone_def by blast 
33175  849 
qed 
850 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

851 
lemma affine_dependent_biggerset: fixes s::"('a::euclidean_space) set" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

852 
assumes "finite s" "card s \<ge> DIM('a) + 2" 
33175  853 
shows "affine_dependent s" 
854 
proof 

855 
have "s\<noteq>{}" using assms by auto then obtain a where "a\<in>s" by auto 

856 
have *:"{x  a x. x \<in> s  {a}} = (\<lambda>x. x  a) ` (s  {a})" by auto 

857 
have "card {x  a x. x \<in> s  {a}} = card (s  {a})" unfolding * 

858 
apply(rule card_image) unfolding inj_on_def by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

859 
also have "\<dots> > DIM('a)" using assms(2) 
33175  860 
unfolding card_Diff_singleton[OF assms(1) `a\<in>s`] by auto 
861 
finally show ?thesis apply(subst insert_Diff[OF `a\<in>s`, THEN sym]) 

862 
apply(rule dependent_imp_affine_dependent) 

863 
apply(rule dependent_biggerset) by auto qed 

864 

865 
lemma affine_dependent_biggerset_general: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

866 
assumes "finite (s::('a::euclidean_space) set)" "card s \<ge> dim s + 2" 
33175  867 
shows "affine_dependent s" 
868 
proof 

869 
from assms(2) have "s \<noteq> {}" by auto 

870 
then obtain a where "a\<in>s" by auto 

871 
have *:"{x  a x. x \<in> s  {a}} = (\<lambda>x. x  a) ` (s  {a})" by auto 

872 
have **:"card {x  a x. x \<in> s  {a}} = card (s  {a})" unfolding * 

873 
apply(rule card_image) unfolding inj_on_def by auto 

874 
have "dim {x  a x. x \<in> s  {a}} \<le> dim s" 

875 
apply(rule subset_le_dim) unfolding subset_eq 

876 
using `a\<in>s` by (auto simp add:span_superset span_sub) 

877 
also have "\<dots> < dim s + 1" by auto 

878 
also have "\<dots> \<le> card (s  {a})" using assms 

879 
using card_Diff_singleton[OF assms(1) `a\<in>s`] by auto 

880 
finally show ?thesis apply(subst insert_Diff[OF `a\<in>s`, THEN sym]) 

881 
apply(rule dependent_imp_affine_dependent) apply(rule dependent_biggerset_general) unfolding ** by auto qed 

882 

883 
subsection {* Caratheodory's theorem. *} 

884 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

885 
lemma convex_hull_caratheodory: fixes p::"('a::euclidean_space) set" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

886 
shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> 
33175  887 
(\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" 
888 
unfolding convex_hull_explicit expand_set_eq mem_Collect_eq 

889 
proof(rule,rule) 

890 
fix y let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y" 

891 
assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y" 

892 
then obtain N where "?P N" by auto 

893 
hence "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n" apply(rule_tac ex_least_nat_le) by auto 

894 
then obtain n where "?P n" and smallest:"\<forall>k<n. \<not> ?P k" by blast 

895 
then obtain s u where obt:"finite s" "card s = n" "s\<subseteq>p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto 

896 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

897 
have "card s \<le> DIM('a) + 1" proof(rule ccontr, simp only: not_le) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

898 
assume "DIM('a) + 1 < card s" 
33175  899 
hence "affine_dependent s" using affine_dependent_biggerset[OF obt(1)] by auto 
900 
then obtain w v where wv:"setsum w s = 0" "v\<in>s" "w v \<noteq> 0" "(\<Sum>v\<in>s. w v *\<^sub>R v) = 0" 

901 
using affine_dependent_explicit_finite[OF obt(1)] by auto 

902 
def i \<equiv> "(\<lambda>v. (u v) / ( w v)) ` {v\<in>s. w v < 0}" def t \<equiv> "Min i" 

903 
have "\<exists>x\<in>s. w x < 0" proof(rule ccontr, simp add: not_less) 

904 
assume as:"\<forall>x\<in>s. 0 \<le> w x" 

905 
hence "setsum w (s  {v}) \<ge> 0" apply(rule_tac setsum_nonneg) by auto 

906 
hence "setsum w s > 0" unfolding setsum_diff1'[OF obt(1) `v\<in>s`] 

907 
using as[THEN bspec[where x=v]] and `v\<in>s` using `w v \<noteq> 0` by auto 

908 
thus False using wv(1) by auto 

909 
qed hence "i\<noteq>{}" unfolding i_def by auto 

910 

911 
hence "t \<ge> 0" using Min_ge_iff[of i 0 ] and obt(1) unfolding t_def i_def 

912 
using obt(4)[unfolded le_less] apply auto unfolding divide_le_0_iff by auto 

913 
have t:"\<forall>v\<in>s. u v + t * w v \<ge> 0" proof 

914 
fix v assume "v\<in>s" hence v:"0\<le>u v" using obt(4)[THEN bspec[where x=v]] by auto 

915 
show"0 \<le> u v + t * w v" proof(cases "w v < 0") 

916 
case False thus ?thesis apply(rule_tac add_nonneg_nonneg) 

917 
using v apply simp apply(rule mult_nonneg_nonneg) using `t\<ge>0` by auto next 

918 
case True hence "t \<le> u v / ( w v)" using `v\<in>s` 

919 
unfolding t_def i_def apply(rule_tac Min_le) using obt(1) by auto 

920 
thus ?thesis unfolding real_0_le_add_iff 

921 
using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[THEN sym]]] by auto 

922 
qed qed 

923 

924 
obtain a where "a\<in>s" and "t = (\<lambda>v. (u v) / ( w v)) a" and "w a < 0" 

925 
using Min_in[OF _ `i\<noteq>{}`] and obt(1) unfolding i_def t_def by auto 

926 
hence a:"a\<in>s" "u a + t * w a = 0" by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

927 
have *:"\<And>f. setsum f (s  {a}) = setsum f s  ((f a)::'b::ab_group_add)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

928 
unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto 
33175  929 
have "(\<Sum>v\<in>s. u v + t * w v) = 1" 
930 
unfolding setsum_addf wv(1) setsum_right_distrib[THEN sym] obt(5) by auto 

931 
moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v)  (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y" 

932 
unfolding setsum_addf obt(6) scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] wv(4) 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

933 
using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp 
33175  934 
ultimately have "?P (n  1)" apply(rule_tac x="(s  {a})" in exI) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

935 
apply(rule_tac x="\<lambda>v. u v + t * w v" in exI) using obt(13) and t and a 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

936 
by (auto simp add: * scaleR_left_distrib) 
33175  937 
thus False using smallest[THEN spec[where x="n  1"]] by auto qed 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

938 
thus "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 
33175  939 
\<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y" using obt by auto 
940 
qed auto 

941 

942 
lemma caratheodory: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

943 
"convex hull p = {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

944 
card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}" 
33175  945 
unfolding expand_set_eq apply(rule, rule) unfolding mem_Collect_eq proof 
946 
fix x assume "x \<in> convex hull p" 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

947 
then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1" 
33175  948 
"\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"unfolding convex_hull_caratheodory by auto 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

949 
thus "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s" 
33175  950 
apply(rule_tac x=s in exI) using hull_subset[of s convex] 
951 
using convex_convex_hull[unfolded convex_explicit, of s, THEN spec[where x=s], THEN spec[where x=u]] by auto 

952 
next 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

953 
fix x assume "\<exists>s. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

954 
then obtain s where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1" "x \<in> convex hull s" by auto 
33175  955 
thus "x \<in> convex hull p" using hull_mono[OF `s\<subseteq>p`] by auto 
956 
qed 

957 

958 
subsection {* Openness and compactness are preserved by convex hull operation. *} 

959 

34964  960 
lemma open_convex_hull[intro]: 
33175  961 
fixes s :: "'a::real_normed_vector set" 
962 
assumes "open s" 

963 
shows "open(convex hull s)" 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36341
diff
changeset

964 
unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10) 
33175  965 
proof(rule, rule) fix a 
966 
assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a" 

967 
then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto 

968 

969 
from assms[unfolded open_contains_cball] obtain b where b:"\<forall>x\<in>s. 0 < b x \<and> cball x (b x) \<subseteq> s" 

970 
using bchoice[of s "\<lambda>x e. e>0 \<and> cball x e \<subseteq> s"] by auto 

971 
have "b ` t\<noteq>{}" unfolding i_def using obt by auto def i \<equiv> "b ` t" 

972 

973 
show "\<exists>e>0. cball a e \<subseteq> {y. \<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y}" 

974 
apply(rule_tac x="Min i" in exI) unfolding subset_eq apply rule defer apply rule unfolding mem_Collect_eq 

975 
proof 

976 
show "0 < Min i" unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] `b \` t\<noteq>{}`] 

977 
using b apply simp apply rule apply(erule_tac x=x in ballE) using `t\<subseteq>s` by auto 

978 
next fix y assume "y \<in> cball a (Min i)" 

979 
hence y:"norm (a  y) \<le> Min i" unfolding dist_norm[THEN sym] by auto 

980 
{ fix x assume "x\<in>t" 

981 
hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto 

982 
hence "x + (y  a) \<in> cball x (b x)" using y unfolding mem_cball dist_norm by auto 

983 
moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36341
diff
changeset

984 
ultimately have "x + (y  a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast } 
33175  985 
moreover 
986 
have *:"inj_on (\<lambda>v. v + (y  a)) t" unfolding inj_on_def by auto 

987 
have "(\<Sum>v\<in>(\<lambda>v. v + (y  a)) ` t. u (v  (y  a))) = 1" 

988 
unfolding setsum_reindex[OF *] o_def using obt(4) by auto 

989 
moreover have "(\<Sum>v\<in>(\<lambda>v. v + (y  a)) ` t. u (v  (y  a)) *\<^sub>R v) = y" 

990 
unfolding setsum_reindex[OF *] o_def using obt(4,5) 

991 
by (simp add: setsum_addf setsum_subtractf scaleR_left.setsum[THEN sym] scaleR_right_distrib) 

992 
ultimately show "\<exists>sa u. finite sa \<and> (\<forall>x\<in>sa. x \<in> s) \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y" 

993 
apply(rule_tac x="(\<lambda>v. v + (y  a)) ` t" in exI) apply(rule_tac x="\<lambda>v. u (v  (y  a))" in exI) 

994 
using obt(1, 3) by auto 

995 
qed 

996 
qed 

997 

998 
lemma compact_convex_combinations: 

999 
fixes s t :: "'a::real_normed_vector set" 

1000 
assumes "compact s" "compact t" 

1001 
shows "compact { (1  u) *\<^sub>R x + u *\<^sub>R y  x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t}" 

1002 
proof 

1003 
let ?X = "{0..1} \<times> s \<times> t" 

1004 
let ?h = "(\<lambda>z. (1  fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))" 

1005 
have *:"{ (1  u) *\<^sub>R x + u *\<^sub>R y  x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t} = ?h ` ?X" 

1006 
apply(rule set_ext) unfolding image_iff mem_Collect_eq 

1007 
apply rule apply auto 

1008 
apply (rule_tac x=u in rev_bexI, simp) 

1009 
apply (erule rev_bexI, erule rev_bexI, simp) 

1010 
by auto 

1011 
have "continuous_on ({0..1} \<times> s \<times> t) 

1012 
(\<lambda>z. (1  fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))" 

1013 
unfolding continuous_on by (rule ballI) (intro tendsto_intros) 

1014 
thus ?thesis unfolding * 

1015 
apply (rule compact_continuous_image) 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

1016 
apply (intro compact_Times compact_interval assms) 
33175  1017 
done 
1018 
qed 

1019 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

1020 
lemma compact_convex_hull: fixes s::"('a::euclidean_space) set" 
33175  1021 
assumes "compact s" shows "compact(convex hull s)" 
1022 
proof(cases "s={}") 

1023 
case True thus ?thesis using compact_empty by simp 

1024 
next 

1025 
case False then obtain w where "w\<in>s" by auto 

1026 
show ?thesis unfolding caratheodory[of s] 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

1027 
proof(induct ("DIM('a) + 1")) 
33175  1028 
have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}" 
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36341
diff
changeset

1029 
using compact_empty by auto 
33175  1030 
case 0 thus ?case unfolding * by simp 
1031 
next 

1032 
case (Suc n) 

1033 
show ?case proof(cases "n=0") 

1034 
case True have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} = s" 

1035 
unfolding expand_set_eq and mem_Collect_eq proof(rule, rule) 

1036 
fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t" 

1037 
then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto 

1038 
show "x\<in>s" proof(cases "card t = 0") 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36341
diff
changeset

1039 
case True thus ?thesis using t(4) unfolding card_0_eq[OF t(1)] by simp 
33175  1040 
next 
1041 
case False hence "card t = Suc 0" using t(3) `n=0` by auto 

1042 
then obtain a where "t = {a}" unfolding card_Suc_eq by auto 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36341
diff
changeset

1043 
thus ?thesis using t(2,4) by simp 
33175  1044 
qed 
1045 
next 

1046 
fix x assume "x\<in>s" 

1047 
thus "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t" 

1048 
apply(rule_tac x="{x}" in exI) unfolding convex_hull_singleton by auto 

1049 
qed thus ?thesis using assms by simp 

1050 
next 

1051 
case False have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} = 

1052 
{ (1  u) *\<^sub>R x + u *\<^sub>R y  x y u. 

1053 
0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> {x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> x \<in> convex hull t}}" 

1054 
unfolding expand_set_eq and mem_Collect_eq proof(rule,rule) 

1055 
fix x assume "\<exists>u v c. x = (1  c) *\<^sub>R u + c *\<^sub>R v \<and> 

1056 
0 \<le> c \<and> c \<le> 1 \<and> u \<in> s \<and> (\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> v \<in> convex hull t)" 

1057 
then obtain u v c t where obt:"x = (1  c) *\<^sub>R u + c *\<^sub>R v" 

1058 
"0 \<le> c \<and> c \<le> 1" "u \<in> s" "finite t" "t \<subseteq> s" "card t \<le> n" "v \<in> convex hull t" by auto 

1059 
moreover have "(1  c) *\<^sub>R u + c *\<^sub>R v \<in> convex hull insert u t" 

1060 
apply(rule mem_convex) using obt(2) and convex_convex_hull and hull_subset[of "insert u t" convex] 

1061 
using obt(7) and hull_mono[of t "insert u t"] by auto 

1062 
ultimately show "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t" 

1063 
apply(rule_tac x="insert u t" in exI) by (auto simp add: card_insert_if) 

1064 
next 

1065 
fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t" 

1066 
then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto 

1067 
let ?P = "\<exists>u v c. x = (1  c) *\<^sub>R u + c *\<^sub>R v \<and> 

1068 
0 \<le> c \<and> c \<le> 1 \<and> u \<in> s \<and> (\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> v \<in> convex hull t)" 

1069 
show ?P proof(cases "card t = Suc n") 

1070 
case False hence "card t \<le> n" using t(3) by auto 

1071 
thus ?P apply(rule_tac x=w in exI, rule_tac x=x in exI, rule_tac x=1 in exI) using `w\<in>s` and t 

1072 
by(auto intro!: exI[where x=t]) 

1073 
next 

1074 
case True then obtain a u where au:"t = insert a u" "a\<notin>u" apply(drule_tac card_eq_SucD) by auto 

1075 
show ?P proof(cases "u={}") 

1076 
case True hence "x=a" using t(4)[unfolded au] by auto 

1077 
show ?P unfolding `x=a` apply(rule_tac x=a in exI, rule_tac x=a in exI, rule_tac x=1 in exI) 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36341
diff
changeset

1078 
using t and `n\<noteq>0` unfolding au by(auto intro!: exI[where x="{a}"]) 
33175  1079 
next 
1080 
case False obtain ux vx b where obt:"ux\<ge>0" "vx\<ge>0" "ux + vx = 1" "b \<in> convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b" 

1081 
using t(4)[unfolded au convex_hull_insert[OF False]] by auto 

1082 
have *:"1  vx = ux" using obt(3) by auto 

1083 
show ?P apply(rule_tac x=a in exI, rule_tac x=b in exI, rule_tac x=vx in exI) 

1084 
using obt and t(13) unfolding au and * using card_insert_disjoint[OF _ au(2)] 

1085 
by(auto intro!: exI[where x=u]) 

1086 
qed 

1087 
qed 

1088 
qed 

1089 
thus ?thesis using compact_convex_combinations[OF assms Suc] by simp 

1090 
qed 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36341
diff
changeset

1091 
qed 
33175  1092 
qed 
1093 

1094 
lemma finite_imp_compact_convex_hull: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

1095 
fixes s :: "('a::euclidean_space) set" 
33175  1096 
shows "finite s \<Longrightarrow> compact(convex hull s)" 
36071  1097 
by (metis compact_convex_hull finite_imp_compact) 
33175  1098 

1099 
subsection {* Extremal points of a simplex are some vertices. *} 

1100 

1101 
lemma dist_increases_online: 

1102 
fixes a b d :: "'a::real_inner" 

1103 
assumes "d \<noteq> 0" 

1104 
shows "dist a (b + d) > dist a b \<or> dist a (b  d) > dist a b" 

1105 
proof(cases "inner a d  inner b d > 0") 

1106 
case True hence "0 < inner d d + (inner a d * 2  inner b d * 2)" 

1107 
apply(rule_tac add_pos_pos) using assms by auto 

1108 
thus ?thesis apply(rule_tac disjI2) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff 

1109 
by (simp add: algebra_simps inner_commute) 

1110 
next 

1111 
case False hence "0 < inner d d + (inner b d * 2  inner a d * 2)" 

1112 
apply(rule_tac add_pos_nonneg) using assms by auto 

1113 
thus ?thesis apply(rule_tac disjI1) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff 

1114 
by (simp add: algebra_simps inner_commute) 

1115 
qed 

1116 

1117 
lemma norm_increases_online: 

1118 
fixes d :: "'a::real_inner" 

1119 
shows "d \<noteq> 0 \<Longrightarrow> norm(a + d) > norm a \<or> norm(a  d) > norm a" 

1120 
using dist_increases_online[of d a 0] unfolding dist_norm by auto 

1121 

1122 
lemma simplex_furthest_lt: 

1123 
fixes s::"'a::real_inner set" assumes "finite s" 

1124 
shows "\<forall>x \<in> (convex hull s). x \<notin> s \<longrightarrow> (\<exists>y\<in>(convex hull s). norm(x  a) < norm(y  a))" 

1125 
proof(induct_tac rule: finite_induct[of s]) 

1126 
fix x s assume as:"finite s" "x\<notin>s" "\<forall>x\<in>convex hull s. x \<notin> s \<longrightarrow> (\<exists>y\<in>convex hull s. norm (x  a) < norm (y  a))" 

1127 
show "\<forall>xa\<in>convex hull insert x s. xa \<notin> insert x s \<longrightarrow> (\<exists>y\<in>convex hull insert x s. norm (xa  a) < norm (y  a))" 

1128 
proof(rule,rule,cases "s = {}") 

1129 
case False fix y assume y:"y \<in> convex hull insert x s" "y \<notin> insert x s" 

1130 
obtain u v b where obt:"u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "y = u *\<^sub>R x + v *\<^sub>R b" 

1131 
using y(1)[unfolded convex_hull_insert[OF False]] by auto 

1132 
show "\<exists>z\<in>convex hull insert x s. norm (y  a) < norm (z  a)" 

1133 
proof(cases "y\<in>convex hull s") 

1134 
case True then obtain z where "z\<in>convex hull s" "norm (y  a) < norm (z  a)" 

1135 
using as(3)[THEN bspec[where x=y]] and y(2) by auto 

1136 
thus ?thesis apply(rule_tac x=z in bexI) unfolding convex_hull_insert[OF False] by auto 

1137 
next 

1138 
case False show ?thesis using obt(3) proof(cases "u=0", case_tac[!] "v=0") 

1139 
assume "u=0" "v\<noteq>0" hence "y = b" using obt by auto 

1140 
thus ?thesis using False and obt(4) by auto 

1141 
next 

1142 
assume "u\<noteq>0" "v=0" hence "y = x" using obt by auto 

1143 
thus ?thesis using y(2) by auto 

1144 
next 

1145 
assume "u\<noteq>0" "v\<noteq>0" 

1146 
then obtain w where w:"w>0" "w<u" "w<v" using real_lbound_gt_zero[of u v] and obt(1,2) by auto 

1147 
have "x\<noteq>b" proof(rule ccontr) 

1148 
assume "\<not> x\<noteq>b" hence "y=b" unfolding obt(5) 

1149 
using obt(3) by(auto simp add: scaleR_left_distrib[THEN sym]) 

1150 
thus False using obt(4) and False by simp qed 

1151 
hence *:"w *\<^sub>R (x  b) \<noteq> 0" using w(1) by auto 

1152 
show ?thesis using dist_increases_online[OF *, of a y] 

1153 
proof(erule_tac disjE) 

1154 
assume "dist a y < dist a (y + w *\<^sub>R (x  b))" 

1155 
hence "norm (y  a) < norm ((u + w) *\<^sub>R x + (v  w) *\<^sub>R b  a)" 

1156 
unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps) 

1157 
moreover have "(u + w) *\<^sub>R x + (v  w) *\<^sub>R b \<in> convex hull insert x s" 

1158 
unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq 

1159 
apply(rule_tac x="u + w" in exI) apply rule defer 

1160 
apply(rule_tac x="v  w" in exI) using `u\<ge>0` and w and obt(3,4) by auto 

1161 
ultimately show ?thesis by auto 

1162 
next 

1163 
assume "dist a y < dist a (y  w *\<^sub>R (x  b))" 

1164 
hence "norm (y  a) < norm ((u  w) *\<^sub>R x + (v + w) *\<^sub>R b  a)" 

1165 
unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps) 

1166 
moreover have "(u  w) *\<^sub>R x + (v + w) *\<^sub>R b \<in> convex hull insert x s" 

1167 
unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq 

1168 
apply(rule_tac x="u  w" in exI) apply rule defer 

1169 
apply(rule_tac x="v + w" in exI) using `u\<ge>0` and w and obt(3,4) by auto 

1170 
ultimately show ?thesis by auto 

1171 
qed 

1172 
qed auto 

1173 
qed 

1174 
qed auto 

1175 
qed (auto simp add: assms) 

1176 

1177 
lemma simplex_furthest_le: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

1178 
fixes s :: "('a::euclidean_space) set" 
33175  1179 
assumes "finite s" "s \<noteq> {}" 
1180 
shows "\<exists>y\<in>s. \<forall>x\<in>(convex hull s). norm(x  a) \<le> norm(y  a)" 

1181 
proof 

1182 
have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto 

1183 
then obtain x where x:"x\<in>convex hull s" "\<forall>y\<in>convex hull s. norm (y  a) \<le> norm (x  a)" 

1184 
using distance_attains_sup[OF finite_imp_compact_convex_hull[OF assms(1)], of a] 

1185 
unfolding dist_commute[of a] unfolding dist_norm by auto 

1186 
thus ?thesis proof(cases "x\<in>s") 

1187 
case False then obtain y where "y\<in>convex hull s" "norm (x  a) < norm (y  a)" 

1188 
using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1) by auto 

1189 
thus ?thesis using x(2)[THEN bspec[where x=y]] by auto 

1190 
qed auto 

1191 
qed 

1192 

1193 
lemma simplex_furthest_le_exists: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

1194 
fixes s :: "('a::euclidean_space) set" 
33175  1195 
shows "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x  a) \<le> norm(y  a))" 
1196 
using simplex_furthest_le[of s] by (cases "s={}")auto 

1197 

1198 
lemma simplex_extremal_le: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

1199 
fixes s :: "('a::euclidean_space) set" 
33175  1200 
assumes "finite s" "s \<noteq> {}" 
1201 
shows "\<exists>u\<in>s. \<exists>v\<in>s. \<forall>x\<in>convex hull s. \<forall>y \<in> convex hull s. norm(x  y) \<le> norm(u  v)" 

1202 
proof 

1203 
have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto 

1204 
then obtain u v where obt:"u\<in>convex hull s" "v\<in>convex hull s" 

1205 
"\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull s. norm (x  y) \<le> norm (u  v)" 

1206 
using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]] by auto 

1207 
thus ?thesis proof(cases "u\<notin>s \<or> v\<notin>s", erule_tac disjE) 

1208 
assume "u\<notin>s" then obtain y where "y\<in>convex hull s" "norm (u  v) < norm (y  v)" 

1209 
using simplex_furthest_lt[OF assms(1), THEN bspec[where x=u]] and obt(1) by auto 

1210 
thus ?thesis using obt(3)[THEN bspec[where x=y], THEN bspec[where x=v]] and obt(2) by auto 

1211 
next 

1212 
assume "v\<notin>s" then obtain y where "y\<in>convex hull s" "norm (v  u) < norm (y  u)" 

1213 
using simplex_furthest_lt[OF assms(1), THEN bspec[where x=v]] and obt(2) by auto 

1214 
thus ?thesis using obt(3)[THEN bspec[where x=u], THEN bspec[where x=y]] and obt(1) 

1215 
by (auto simp add: norm_minus_commute) 

1216 
qed auto 

1217 
qed 

1218 

1219 
lemma simplex_extremal_le_exists: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36844
diff
changeset

1220 
fixes s :: "('a::euclidean_space) set" 
33175  1221 
shows "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s 
1222 
\<Longrightarrow> (\<exists>u\<in>s. \<exists>v\<in>s. norm(x  y) \<le> norm(u  v))" 

1223 
using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto 

1224 

1225 
subsection {* Closest point of a convex set is unique, with a continuous projection. *} 

1226 

1227 
definition 

36337  1228 
closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a" where 
33175  1229 
"closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))" 
1230 

1231 
lemma closest_point_exists: 

1232 
assumes "closed s" "s \<noteq> {}" 

1233 
shows "closest_point s a \<in> s" "\<forall>y\<in>s. dist a (closest_point s a) \<le> dist a y" 

1234 
unfolding closest_point_def apply(rule_tac[!] someI2_ex) 

1235 
using distance_attains_inf[OF assms(1,2), of a] by auto 

1236 

1237 
lemma closest_point_in_set: 

1238 
"closed s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> (closest_point s a) \<in> s" 

1239 
by(meson closest_point_exists) 

1240 

1241 
lemma closest_point_le: 

1242 
"closed s \<Longrightarrow> x \<in> s \<Longrightarrow> dist a (closest_point s a) \<le> dist a x" 

1243 
using closest_point_exists[of s] by auto 

1244 

1245 
lemma closest_point_self: 

1246 
assumes "x \<in> s" shows "closest_point s x = x" 

1247 
unfolding closest_point_def apply(rule some1_equality, rule ex1I[of _ x]) 
