author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47108  2a1953f0d20d 
child 47444  d21c95af2df7 
permissions  rwrr 
41959  1 
(* Title: HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy 
33175  2 
Author: Robert Himmelmann, TU Muenchen 
40887
ee8d0548c148
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
hoelzl
parents:
40719
diff
changeset

3 
Author: Bogdan Grechuk, University of Edinburgh 
33175  4 
*) 
5 

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

7 

8 
theory Convex_Euclidean_Space 

44132  9 
imports 
10 
Topology_Euclidean_Space 

11 
"~~/src/HOL/Library/Convex" 

12 
"~~/src/HOL/Library/Set_Algebras" 

33175  13 
begin 
14 

15 

16 
(*  *) 

17 
(* To be moved elsewhere *) 

18 
(*  *) 

19 

44361
75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

20 
lemma linear_scaleR: "linear (\<lambda>x. scaleR c x)" 
75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

21 
by (simp add: linear_def scaleR_add_right) 
75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

22 

75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

23 
lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>(x::'a::real_vector). scaleR c x)" 
75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

24 
by (simp add: inj_on_def) 
40377  25 

26 
lemma linear_add_cmul: 

27 
assumes "linear f" 

28 
shows "f(a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x + b *\<^sub>R f y" 

29 
using linear_add[of f] linear_cmul[of f] assms by (simp) 

30 

31 
lemma mem_convex_2: 

32 
assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v=1" 

33 
shows "(u *\<^sub>R x + v *\<^sub>R y) : S" 

34 
using assms convex_def[of S] by auto 

35 

36 
lemma mem_convex_alt: 

37 
assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v>0" 

38 
shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) : S" 

39 
apply (subst mem_convex_2) 

40 
using assms apply (auto simp add: algebra_simps zero_le_divide_iff) 

41 
using add_divide_distrib[of u v "u+v"] by auto 

42 

43 
lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)" 

44 
by (blast dest: inj_onD) 

45 

46 
lemma independent_injective_on_span_image: 

44361
75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

47 
assumes iS: "independent S" 
40377  48 
and lf: "linear f" and fi: "inj_on f (span S)" 
49 
shows "independent (f ` S)" 

50 
proof 

51 
{fix a assume a: "a : S" "f a : span (f ` S  {f a})" 

52 
have eq: "f ` S  {f a} = f ` (S  {a})" using fi a span_inc 

53 
by (auto simp add: inj_on_def) 

54 
from a have "f a : f ` span (S {a})" 

55 
unfolding eq span_linear_image[OF lf, of "S  {a}"] by blast 

56 
moreover have "span (S {a}) <= span S" using span_mono[of "S{a}" S] by auto 

57 
ultimately have "a : span (S {a})" using fi a span_inc by (auto simp add: inj_on_def) 

58 
with a(1) iS have False by (simp add: dependent_def) } 

59 
then show ?thesis unfolding dependent_def by blast 

60 
qed 

61 

62 
lemma dim_image_eq: 

63 
fixes f :: "'n::euclidean_space => 'm::euclidean_space" 

64 
assumes lf: "linear f" and fi: "inj_on f (span S)" 

65 
shows "dim (f ` S) = dim (S:: ('n::euclidean_space) set)" 

66 
proof 

67 
obtain B where B_def: "B<=S & independent B & S <= span B & card B = dim S" 

68 
using basis_exists[of S] by auto 

69 
hence "span S = span B" using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto 

70 
hence "independent (f ` B)" using independent_injective_on_span_image[of B f] B_def assms by auto 

71 
moreover have "card (f ` B) = card B" using assms card_image[of f B] subset_inj_on[of f "span S" B] 

72 
B_def span_inc by auto 

73 
moreover have "(f ` B) <= (f ` S)" using B_def by auto 

74 
ultimately have "dim (f ` S) >= dim S" 

75 
using independent_card_le_dim[of "f ` B" "f ` S"] B_def by auto 

76 
from this show ?thesis using dim_image_le[of f S] assms by auto 

77 
qed 

78 

79 
lemma linear_injective_on_subspace_0: 

80 
assumes lf: "linear f" and "subspace S" 

81 
shows "inj_on f S <> (!x : S. f x = 0 > x = 0)" 

82 
proof 

83 
have "inj_on f S <> (!x : S. !y : S. f x = f y > x = y)" by (simp add: inj_on_def) 

84 
also have "... <> (!x : S. !y : S. f x  f y = 0 > x  y = 0)" by simp 

85 
also have "... <> (!x : S. !y : S. f (x  y) = 0 > x  y = 0)" 

86 
by (simp add: linear_sub[OF lf]) 

87 
also have "... <> (! x : S. f x = 0 > x = 0)" 

88 
using `subspace S` subspace_def[of S] subspace_sub[of S] by auto 

89 
finally show ?thesis . 

90 
qed 

91 

92 
lemma subspace_Inter: "(!s : f. subspace s) ==> subspace (Inter f)" 

93 
unfolding subspace_def by auto 

94 

95 
lemma span_eq[simp]: "(span s = s) <> subspace s" 

44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44365
diff
changeset

96 
unfolding span_def by (rule hull_eq, rule subspace_Inter) 
40377  97 

98 
lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d" 

99 
by(auto simp add: inj_on_def euclidean_eq[where 'a='n]) 

100 

101 
lemma finite_substdbasis: "finite {basis i ::'n::euclidean_space i. i : (d:: nat set)}" (is "finite ?S") 

102 
proof 

103 
have eq: "?S = basis ` d" by blast 

104 
show ?thesis unfolding eq apply(rule finite_subset[OF _ range_basis_finite]) by auto 

105 
qed 

106 

107 
lemma card_substdbasis: assumes "d \<subseteq> {..<DIM('n::euclidean_space)}" 

108 
shows "card {basis i ::'n::euclidean_space  i. i : d} = card d" (is "card ?S = _") 

109 
proof 

110 
have eq: "?S = basis ` d" by blast 

111 
show ?thesis unfolding eq using card_image[OF basis_inj_on[of d]] assms by auto 

112 
qed 

113 

114 
lemma substdbasis_expansion_unique: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}" 

115 
shows "setsum (%i. f i *\<^sub>R basis i) d = (x::'a::euclidean_space) 

116 
<> (!i<DIM('a). (i:d > f i = x$$i) & (i ~: d > x $$ i = 0))" 

117 
proof have *:"\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44821
diff
changeset

118 
have **:"finite d" apply(rule finite_subset[OF assms]) by fastforce 
40377  119 
have ***:"\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44170
diff
changeset

120 
unfolding euclidean_component_setsum euclidean_component_scaleR basis_component * 
40377  121 
apply(rule setsum_cong2) using assms by auto 
122 
show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto 

123 
qed 

124 

125 
lemma independent_substdbasis: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}" 

126 
shows "independent {basis i ::'a::euclidean_space i. i : (d :: nat set)}" (is "independent ?A") 

127 
proof  

128 
have *: "{basis i i. i < DIM('a)} = basis ` {..<DIM('a)}" by auto 

129 
show ?thesis 

130 
apply(intro independent_mono[of "{basis i ::'a i. i : {..<DIM('a::euclidean_space)}}" "?A"] ) 

131 
using independent_basis[where 'a='a] assms by (auto simp: *) 

132 
qed 

133 

134 
lemma dim_cball: 

135 
assumes "0<e" 

136 
shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)" 

137 
proof 

138 
{ fix x :: "'n::euclidean_space" def y == "(e/norm x) *\<^sub>R x" 

139 
hence "y : cball 0 e" using cball_def dist_norm[of 0 y] assms by auto 

140 
moreover have "x = (norm x/e) *\<^sub>R y" using y_def assms by simp 

141 
moreover hence "x = (norm x/e) *\<^sub>R y" by auto 

142 
ultimately have "x : span (cball 0 e)" 

143 
using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto 

144 
} hence "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto 

145 
from this show ?thesis using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp add: dim_UNIV) 

146 
qed 

147 

148 
lemma indep_card_eq_dim_span: 

149 
fixes B :: "('n::euclidean_space) set" 

150 
assumes "independent B" 

151 
shows "finite B & card B = dim (span B)" 

152 
using assms basis_card_eq_dim[of B "span B"] span_inc by auto 

153 

154 
lemma setsum_not_0: "setsum f A ~= 0 ==> EX a:A. f a ~= 0" 

155 
apply(rule ccontr) by auto 

156 

157 
lemma translate_inj_on: 

44361
75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

158 
fixes A :: "('a::ab_group_add) set" 
40377  159 
shows "inj_on (%x. a+x) A" unfolding inj_on_def by auto 
160 

161 
lemma translation_assoc: 

162 
fixes a b :: "'a::ab_group_add" 

163 
shows "(\<lambda>x. b+x) ` ((\<lambda>x. a+x) ` S) = (\<lambda>x. (a+b)+x) ` S" by auto 

164 

165 
lemma translation_invert: 

166 
fixes a :: "'a::ab_group_add" 

167 
assumes "(\<lambda>x. a+x) ` A = (\<lambda>x. a+x) ` B" 

168 
shows "A=B" 

169 
proof 

170 
have "(%x. a+x) ` ((%x. a+x) ` A) = (%x. a+x) ` ((%x. a+x) ` B)" using assms by auto 

171 
from this show ?thesis using translation_assoc[of "a" a A] translation_assoc[of "a" a B] by auto 

172 
qed 

173 

174 
lemma translation_galois: 

175 
fixes a :: "'a::ab_group_add" 

176 
shows "T=((\<lambda>x. a+x) ` S) <> S=((\<lambda>x. (a)+x) ` T)" 

177 
using translation_assoc[of "a" a S] apply auto 

178 
using translation_assoc[of a "a" T] by auto 

179 

180 
lemma translation_inverse_subset: 

181 
assumes "((%x. a+x) ` V) <= (S :: 'n::ab_group_add set)" 

182 
shows "V <= ((%x. a+x) ` S)" 

183 
proof 

184 
{ fix x assume "x:V" hence "xa : S" using assms by auto 

185 
hence "x : {a + v v. v : S}" apply auto apply (rule exI[of _ "xa"]) apply simp done 

186 
hence "x : ((%x. a+x) ` S)" by auto } 

187 
from this show ?thesis by auto 

188 
qed 

189 

190 
lemma basis_to_basis_subspace_isomorphism: 

191 
assumes s: "subspace (S:: ('n::euclidean_space) set)" 

192 
and t: "subspace (T :: ('m::euclidean_space) set)" 

193 
and d: "dim S = dim T" 

194 
and B: "B <= S" "independent B" "S <= span B" "card B = dim S" 

195 
and C: "C <= T" "independent C" "T <= span C" "card C = dim T" 

196 
shows "EX f. linear f & f ` B = C & f ` S = T & inj_on f S" 

197 
proof 

198 
(* Proof is a modified copy of the proof of similar lemma subspace_isomorphism 

199 
*) 

200 
from B independent_bound have fB: "finite B" by blast 

201 
from C independent_bound have fC: "finite C" by blast 

202 
from B(4) C(4) card_le_inj[of B C] d obtain f where 

203 
f: "f ` B \<subseteq> C" "inj_on f B" using `finite B` `finite C` by auto 

204 
from linear_independent_extend[OF B(2)] obtain g where 

205 
g: "linear g" "\<forall>x\<in> B. g x = f x" by blast 

206 
from inj_on_iff_eq_card[OF fB, of f] f(2) 

207 
have "card (f ` B) = card B" by simp 

208 
with B(4) C(4) have ceq: "card (f ` B) = card C" using d 

209 
by simp 

210 
have "g ` B = f ` B" using g(2) 

211 
by (auto simp add: image_iff) 

212 
also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] . 

213 
finally have gBC: "g ` B = C" . 

214 
have gi: "inj_on g B" using f(2) g(2) 

215 
by (auto simp add: inj_on_def) 

216 
note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi] 

217 
{fix x y assume x: "x \<in> S" and y: "y \<in> S" and gxy:"g x = g y" 

218 
from B(3) x y have x': "x \<in> span B" and y': "y \<in> span B" by blast+ 

219 
from gxy have th0: "g (x  y) = 0" by (simp add: linear_sub[OF g(1)]) 

220 
have th1: "x  y \<in> span B" using x' y' by (metis span_sub) 

221 
have "x=y" using g0[OF th1 th0] by simp } 

222 
then have giS: "inj_on g S" 

223 
unfolding inj_on_def by blast 

224 
from span_subspace[OF B(1,3) s] 

225 
have "g ` S = span (g ` B)" by (simp add: span_linear_image[OF g(1)]) 

226 
also have "\<dots> = span C" unfolding gBC .. 

227 
also have "\<dots> = T" using span_subspace[OF C(1,3) t] . 

228 
finally have gS: "g ` S = T" . 

229 
from g(1) gS giS gBC show ?thesis by blast 

230 
qed 

231 

44524  232 
lemma closure_bounded_linear_image: 
233 
assumes f: "bounded_linear f" 

234 
shows "f ` (closure S) \<subseteq> closure (f ` S)" 

235 
using linear_continuous_on [OF f] closed_closure closure_subset 

236 
by (rule image_closure_subset) 

237 

40377  238 
lemma closure_linear_image: 
44361
75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

239 
fixes f :: "('m::euclidean_space) => ('n::real_normed_vector)" 
40377  240 
assumes "linear f" 
241 
shows "f ` (closure S) <= closure (f ` S)" 

44524  242 
using assms unfolding linear_conv_bounded_linear 
243 
by (rule closure_bounded_linear_image) 

40377  244 

245 
lemma closure_injective_linear_image: 

246 
fixes f :: "('n::euclidean_space) => ('n::euclidean_space)" 

247 
assumes "linear f" "inj f" 

248 
shows "f ` (closure S) = closure (f ` S)" 

249 
proof 

250 
obtain f' where f'_def: "linear f' & f o f' = id & f' o f = id" 

251 
using assms linear_injective_isomorphism[of f] isomorphism_expand by auto 

252 
hence "f' ` closure (f ` S) <= closure (S)" 

253 
using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto 

254 
hence "f ` f' ` closure (f ` S) <= f ` closure (S)" by auto 

255 
hence "closure (f ` S) <= f ` closure (S)" using image_compose[of f f' "closure (f ` S)"] f'_def by auto 

256 
from this show ?thesis using closure_linear_image[of f S] assms by auto 

257 
qed 

258 

259 
lemma closure_direct_sum: 

260 
shows "closure (S <*> T) = closure S <*> closure T" 

44365  261 
by (rule closure_Times) 
40377  262 

44524  263 
lemma closure_scaleR: 
264 
fixes S :: "('a::real_normed_vector) set" 

265 
shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)" 

266 
proof 

267 
show "(op *\<^sub>R c) ` (closure S) \<subseteq> closure ((op *\<^sub>R c) ` S)" 

268 
using bounded_linear_scaleR_right 

269 
by (rule closure_bounded_linear_image) 

270 
show "closure ((op *\<^sub>R c) ` S) \<subseteq> (op *\<^sub>R c) ` (closure S)" 

271 
by (intro closure_minimal image_mono closure_subset 

272 
closed_scaling closed_closure) 

40377  273 
qed 
274 

275 
lemma fst_linear: "linear fst" unfolding linear_def by (simp add: algebra_simps) 

276 

277 
lemma snd_linear: "linear snd" unfolding linear_def by (simp add: algebra_simps) 

278 

40897
1eb1b2f9d062
adapt proofs to changed set_plus_image (cf. ee8d0548c148);
hoelzl
parents:
40887
diff
changeset

279 
lemma fst_snd_linear: "linear (%(x,y). x + y)" unfolding linear_def by (simp add: algebra_simps) 
40377  280 

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

282 
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

283 
shows "scaleR 2 x = x + x" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45498
diff
changeset

284 
unfolding one_add_one [symmetric] scaleR_left_distrib by simp 
34964  285 

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

286 
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

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

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

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

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

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

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

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

295 

296 
lemma setsum_delta'': 

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

298 
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)" 

299 
proof 

300 
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 

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

302 
qed 

303 

304 
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 

305 

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 
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space)) ` {a..b} = 
33175  307 
(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})" 
308 
using image_affinity_interval[of m 0 a b] by auto 

309 

310 
lemma dist_triangle_eq: 

44361
75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

311 
fixes x y z :: "'a::real_inner" 
33175  312 
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)" 
313 
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

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

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

317 
lemma norm_minus_eqI:"x =  y \<Longrightarrow> norm x = norm y" by auto 
33175  318 

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

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

321 

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

322 
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

323 
unfolding norm_eq_sqrt_inner by simp 
33175  324 

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

325 
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

326 
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

327 

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

328 

44467  329 
subsection {* Affine set and affine hull *} 
33175  330 

331 
definition 

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

333 
"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)" 

334 

335 
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  336 
unfolding affine_def by(metis eq_diff_eq') 
33175  337 

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

339 
unfolding affine_def by auto 

340 

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

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

343 

344 
lemma affine_UNIV[intro]: "affine UNIV" 

345 
unfolding affine_def by auto 

346 

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

348 
unfolding affine_def by auto 

349 

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

351 
unfolding affine_def by auto 

352 

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

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

354 
unfolding hull_def using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

355 
by auto 
33175  356 

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

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

358 
by (metis affine_affine_hull hull_same) 
33175  359 

44467  360 
subsubsection {* Some explicit formulations (from Lars Schewe) *} 
33175  361 

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

363 
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)" 

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

365 
defer apply(rule, rule, rule, rule, rule) proof 

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

367 
"\<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" 

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

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

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

371 
next 

372 
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" 

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

374 
def n \<equiv> "card s" 

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

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

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

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

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

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

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

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

383 
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  384 
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 
385 
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  386 
"finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1" 
387 
have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr) 

388 
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 

45498
2dc373f1867a
avoid numeralrepresentationspecific rules in metis proof
huffman
parents:
45051
diff
changeset

389 
thus False using as(7) and `card s > 2` by (metis One_nat_def 
2dc373f1867a
avoid numeralrepresentationspecific rules in metis proof
huffman
parents:
45051
diff
changeset

390 
less_Suc0 Zero_not_Suc of_nat_1 of_nat_eq_iff numeral_2_eq_2) 
2dc373f1867a
avoid numeralrepresentationspecific rules in metis proof
huffman
parents:
45051
diff
changeset

391 
qed 
33175  392 
then obtain x where x:"x\<in>s" "u x \<noteq> 1" by auto 
393 

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

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

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

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

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

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

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

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

402 
thus False using True by auto qed auto 

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

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

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

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

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

408 
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

409 
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

410 
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

411 
unfolding RealVector.scaleR_right.setsum using x(1) as(6) by auto 
33175  412 
thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] 
413 
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

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

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

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

419 
qed 

420 

421 
lemma affine_hull_explicit: 

422 
"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}" 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

423 
apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq 
33175  424 
apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof 
425 
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" 

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

427 
next 

428 
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" 

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

430 
next 

431 
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 

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

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

434 
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" 

435 
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 

436 
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" 

437 
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 

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

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

440 
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" 

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

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

443 
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

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

447 
lemma affine_hull_finite: 

448 
assumes "finite s" 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

450 
unfolding affine_hull_explicit and set_eq_iff and mem_Collect_eq apply (rule,rule) 
33175  451 
apply(erule exE)+ apply(erule conjE)+ defer apply(erule exE) apply(erule conjE) proof 
452 
fix x u assume "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" 

453 
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" 

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

455 
next 

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

457 
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" 

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

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

460 

44467  461 
subsubsection {* Stepping theorems and hence small special cases *} 
33175  462 

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

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

464 
apply(rule hull_unique) by auto 
33175  465 

466 
lemma affine_hull_finite_step: 

467 
fixes y :: "'a::real_vector" 

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

469 
"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> 

470 
(\<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)") 

471 
proof 

472 
show ?th1 by simp 

473 
assume ?as 

474 
{ assume ?lhs 

475 
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 

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

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

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

479 
next 

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

481 
qed } moreover 

482 
{ assume ?rhs 

483 
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 

484 
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 

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

486 
case True thus ?thesis 

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

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

489 
unfolding scaleR_left_distrib and setsum_addf 

490 
unfolding vu and * and scaleR_zero_left 

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

492 
next 

493 
case False 

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

495 
"\<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 

496 
from False show ?thesis 

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

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

499 
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)] 

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

501 
qed } 

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

503 
qed 

504 

505 
lemma affine_hull_2: 

506 
fixes a b :: "'a::real_vector" 

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

508 
proof 

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

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

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

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

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

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

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

516 
finally show ?thesis by auto 

517 
qed 

518 

519 
lemma affine_hull_3: 

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

521 
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") 

522 
proof 

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

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

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

526 
unfolding * apply auto 

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

44629  528 
apply(rule_tac x=u in exI) by force 
33175  529 
qed 
530 

40377  531 
lemma mem_affine: 
532 
assumes "affine S" "x : S" "y : S" "u+v=1" 

533 
shows "(u *\<^sub>R x + v *\<^sub>R y) : S" 

534 
using assms affine_def[of S] by auto 

535 

536 
lemma mem_affine_3: 

537 
assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1" 

538 
shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S" 

539 
proof 

540 
have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}" 

541 
using affine_hull_3[of x y z] assms by auto 

542 
moreover have " affine hull {x, y, z} <= affine hull S" 

543 
using hull_mono[of "{x, y, z}" "S"] assms by auto 

544 
moreover have "affine hull S = S" 

545 
using assms affine_hull_eq[of S] by auto 

546 
ultimately show ?thesis by auto 

547 
qed 

548 

549 
lemma mem_affine_3_minus: 

550 
assumes "affine S" "x : S" "y : S" "z : S" 

551 
shows "x + v *\<^sub>R (yz) : S" 

552 
using mem_affine_3[of S x y z 1 v "v"] assms by (simp add: algebra_simps) 

553 

554 

44467  555 
subsubsection {* Some relations between affine hull and subspaces *} 
33175  556 

557 
lemma affine_hull_insert_subset_span: 

558 
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

559 
unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq 
33175  560 
apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof 
561 
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" 

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

563 
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)" 

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

565 
apply (rule conjI, simp) 

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

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

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

569 
apply (erule conjI) 

570 
using as(1) 

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

572 
unfolding as by simp qed 

573 

574 
lemma affine_hull_insert_span: 

575 
assumes "a \<notin> s" 

576 
shows "affine hull (insert a s) = 

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

578 
apply(rule, rule affine_hull_insert_subset_span) unfolding subset_eq Ball_def 

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

580 
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

581 
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  582 
def f \<equiv> "(\<lambda>x. x + a) ` t" 
583 
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 

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

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

586 
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" 

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

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

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

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

33175  592 

593 
lemma affine_hull_span: 

594 
assumes "a \<in> s" 

595 
shows "affine hull s = {a + v  v. v \<in> span {x  a  x. x \<in> s  {a}}}" 

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

597 

44467  598 
subsubsection {* Parallel affine sets *} 
40377  599 

600 
definition affine_parallel :: "'a::real_vector set => 'a::real_vector set => bool" 

601 
where "affine_parallel S T = (? a. T = ((%x. a + x) ` S))" 

602 

603 
lemma affine_parallel_expl_aux: 

604 
fixes S T :: "'a::real_vector set" 

605 
assumes "!x. (x : S <> (a+x) : T)" 

606 
shows "T = ((%x. a + x) ` S)" 

607 
proof 

608 
{ fix x assume "x : T" hence "(a)+x : S" using assms by auto 

609 
hence " x : ((%x. a + x) ` S)" using imageI[of "a+x" S "(%x. a+x)"] by auto} 

610 
moreover have "T >= ((%x. a + x) ` S)" using assms by auto 

611 
ultimately show ?thesis by auto 

612 
qed 

613 

614 
lemma affine_parallel_expl: 

615 
"affine_parallel S T = (? a. !x. (x : S <> (a+x) : T))" 

616 
unfolding affine_parallel_def using affine_parallel_expl_aux[of S _ T] by auto 

617 

618 
lemma affine_parallel_reflex: "affine_parallel S S" unfolding affine_parallel_def apply (rule exI[of _ "0"]) by auto 

619 

620 
lemma affine_parallel_commut: 

621 
assumes "affine_parallel A B" shows "affine_parallel B A" 

622 
proof 

623 
from assms obtain a where "B=((%x. a + x) ` A)" unfolding affine_parallel_def by auto 

624 
from this show ?thesis using translation_galois[of B a A] unfolding affine_parallel_def by auto 

625 
qed 

626 

627 
lemma affine_parallel_assoc: 

628 
assumes "affine_parallel A B" "affine_parallel B C" 

629 
shows "affine_parallel A C" 

630 
proof 

631 
from assms obtain ab where "B=((%x. ab + x) ` A)" unfolding affine_parallel_def by auto 

632 
moreover 

633 
from assms obtain bc where "C=((%x. bc + x) ` B)" unfolding affine_parallel_def by auto 

634 
ultimately show ?thesis using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto 

635 
qed 

636 

637 
lemma affine_translation_aux: 

638 
fixes a :: "'a::real_vector" 

639 
assumes "affine ((%x. a + x) ` S)" shows "affine S" 

640 
proof 

641 
{ fix x y u v 

642 
assume xy: "x : S" "y : S" "(u :: real)+v=1" 

643 
hence "(a+x):((%x. a + x) ` S)" "(a+y):((%x. a + x) ` S)" by auto 

644 
hence h1: "u *\<^sub>R (a+x) + v *\<^sub>R (a+y) : ((%x. a + x) ` S)" using xy assms unfolding affine_def by auto 

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

646 
also have "...= a + (u *\<^sub>R x + v *\<^sub>R y)" using `u+v=1` by auto 

647 
ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) : ((%x. a + x) ` S)" using h1 by auto 

648 
hence "u *\<^sub>R x + v *\<^sub>R y : S" by auto 

649 
} from this show ?thesis unfolding affine_def by auto 

650 
qed 

651 

652 
lemma affine_translation: 

653 
fixes a :: "'a::real_vector" 

654 
shows "affine S <> affine ((%x. a + x) ` S)" 

655 
proof 

656 
have "affine S ==> affine ((%x. a + x) ` S)" using affine_translation_aux[of "a" "((%x. a + x) ` S)"] using translation_assoc[of "a" a S] by auto 

657 
from this show ?thesis using affine_translation_aux by auto 

658 
qed 

659 

660 
lemma parallel_is_affine: 

661 
fixes S T :: "'a::real_vector set" 

662 
assumes "affine S" "affine_parallel S T" 

663 
shows "affine T" 

664 
proof 

665 
from assms obtain a where "T=((%x. a + x) ` S)" unfolding affine_parallel_def by auto 

666 
from this show ?thesis using affine_translation assms by auto 

667 
qed 

668 

44361
75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

669 
lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s" 
40377  670 
unfolding subspace_def affine_def by auto 
671 

44467  672 
subsubsection {* Subspace parallel to an affine set *} 
40377  673 

674 
lemma subspace_affine: 

675 
shows "subspace S <> (affine S & 0 : S)" 

676 
proof 

677 
have h0: "subspace S ==> (affine S & 0 : S)" using subspace_imp_affine[of S] subspace_0 by auto 

678 
{ assume assm: "affine S & 0 : S" 

679 
{ fix c :: real 

680 
fix x assume x_def: "x : S" 

681 
have "c *\<^sub>R x = (1c) *\<^sub>R 0 + c *\<^sub>R x" by auto 

682 
moreover have "(1c) *\<^sub>R 0 + c *\<^sub>R x : S" using affine_alt[of S] assm x_def by auto 

683 
ultimately have "c *\<^sub>R x : S" by auto 

684 
} hence h1: "!c. !x : S. c *\<^sub>R x : S" by auto 

685 
{ fix x y assume xy_def: "x : S" "y : S" 

686 
def u == "(1 :: real)/2" 

687 
have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" by auto 

688 
moreover have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1(1/2)) *\<^sub>R y" by (simp add: algebra_simps) 

689 
moreover have "(1u) *\<^sub>R x + u *\<^sub>R y : S" using affine_alt[of S] assm xy_def by auto 

690 
ultimately have "(1/2) *\<^sub>R (x+y) : S" using u_def by auto 

691 
moreover have "(x+y) = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" by auto 

692 
ultimately have "(x+y) : S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto 

693 
} hence "!x : S. !y : S. (x+y) : S" by auto 

694 
hence "subspace S" using h1 assm unfolding subspace_def by auto 

695 
} from this show ?thesis using h0 by metis 

696 
qed 

697 

698 
lemma affine_diffs_subspace: 

699 
assumes "affine S" "a : S" 

700 
shows "subspace ((%x. (a)+x) ` S)" 

701 
proof 

702 
have "affine ((%x. (a)+x) ` S)" using affine_translation assms by auto 

703 
moreover have "0 : ((%x. (a)+x) ` S)" using assms exI[of "(%x. x:S & a+x=0)" a] by auto 

704 
ultimately show ?thesis using subspace_affine by auto 

705 
qed 

706 

707 
lemma parallel_subspace_explicit: 

708 
assumes "affine S" "a : S" 

709 
assumes "L == {y. ? x : S. (a)+x=y}" 

710 
shows "subspace L & affine_parallel S L" 

711 
proof 

712 
have par: "affine_parallel S L" unfolding affine_parallel_def using assms by auto 

713 
hence "affine L" using assms parallel_is_affine by auto 

714 
moreover have "0 : L" using assms apply auto using exI[of "(%x. x:S & a+x=0)" a] by auto 

715 
ultimately show ?thesis using subspace_affine par by auto 

716 
qed 

717 

718 
lemma parallel_subspace_aux: 

719 
assumes "subspace A" "subspace B" "affine_parallel A B" 

720 
shows "A>=B" 

721 
proof 

722 
from assms obtain a where a_def: "!x. (x : A <> (a+x) : B)" using affine_parallel_expl[of A B] by auto 

723 
hence "a : A" using assms subspace_0[of B] by auto 

724 
hence "a : A" using assms subspace_neg[of A "a"] by auto 

725 
from this show ?thesis using assms a_def unfolding subspace_def by auto 

726 
qed 

727 

728 
lemma parallel_subspace: 

729 
assumes "subspace A" "subspace B" "affine_parallel A B" 

730 
shows "A=B" 

731 
proof 

732 
have "A>=B" using assms parallel_subspace_aux by auto 

733 
moreover have "A<=B" using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto 

734 
ultimately show ?thesis by auto 

735 
qed 

736 

737 
lemma affine_parallel_subspace: 

738 
assumes "affine S" "S ~= {}" 

739 
shows "?!L. subspace L & affine_parallel S L" 

740 
proof 

741 
have ex: "? L. subspace L & affine_parallel S L" using assms parallel_subspace_explicit by auto 

742 
{ fix L1 L2 assume ass: "subspace L1 & affine_parallel S L1" "subspace L2 & affine_parallel S L2" 

743 
hence "affine_parallel L1 L2" using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto 

744 
hence "L1=L2" using ass parallel_subspace by auto 

745 
} from this show ?thesis using ex by auto 

746 
qed 

747 

44467  748 
subsection {* Cones *} 
33175  749 

750 
definition 

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

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

753 

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

755 
unfolding cone_def by auto 

756 

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

758 
unfolding cone_def by auto 

759 

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

761 
unfolding cone_def by auto 

762 

44467  763 
subsubsection {* Conic hull *} 
33175  764 

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

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

766 
unfolding hull_def by auto 
33175  767 

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

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

769 
apply(rule hull_eq) 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

770 
using cone_Inter unfolding subset_eq by auto 
33175  771 

40377  772 
lemma mem_cone: 
773 
assumes "cone S" "x : S" "c>=0" 

774 
shows "c *\<^sub>R x : S" 

775 
using assms cone_def[of S] by auto 

776 

777 
lemma cone_contains_0: 

778 
assumes "cone S" 

779 
shows "(S ~= {}) <> (0 : S)" 

780 
proof 

781 
{ assume "S ~= {}" from this obtain a where "a:S" by auto 

782 
hence "0 : S" using assms mem_cone[of S a 0] by auto 

783 
} from this show ?thesis by auto 

784 
qed 

785 

44361
75ec83d45303
remove unnecessary euclidean_space class constraints
huffman
parents:
44349
diff
changeset

786 
lemma cone_0: "cone {0}" 
40377  787 
unfolding cone_def by auto 
788 

789 
lemma cone_Union[intro]: "(!s:f. cone s) > (cone (Union f))" 

790 
unfolding cone_def by blast 

791 

792 
lemma cone_iff: 

793 
assumes "S ~= {}" 

794 
shows "cone S <> 0:S & (!c. c>0 > ((op *\<^sub>R c) ` S) = S)" 

795 
proof 

796 
{ assume "cone S" 

797 
{ fix c assume "(c :: real)>0" 

798 
{ fix x assume "x : S" hence "x : (op *\<^sub>R c) ` S" unfolding image_def 

799 
using `cone S` `c>0` mem_cone[of S x "1/c"] 

800 
exI[of "(%t. t:S & x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] by auto 

801 
} 

802 
moreover 

803 
{ fix x assume "x : (op *\<^sub>R c) ` S" 

804 
(*from this obtain t where "t:S & x = c *\<^sub>R t" by auto*) 

805 
hence "x:S" using `cone S` `c>0` unfolding cone_def image_def `c>0` by auto 

806 
} 

807 
ultimately have "((op *\<^sub>R c) ` S) = S" by auto 

808 
} hence "0:S & (!c. c>0 > ((op *\<^sub>R c) ` S) = S)" using `cone S` cone_contains_0[of S] assms by auto 

809 
} 

810 
moreover 

811 
{ assume a: "0:S & (!c. c>0 > ((op *\<^sub>R c) ` S) = S)" 

812 
{ fix x assume "x:S" 

813 
fix c1 assume "(c1 :: real)>=0" 

814 
hence "(c1=0)  (c1>0)" by auto 

815 
hence "c1 *\<^sub>R x : S" using a `x:S` by auto 

816 
} 

817 
hence "cone S" unfolding cone_def by auto 

818 
} ultimately show ?thesis by blast 

819 
qed 

820 

821 
lemma cone_hull_empty: 

822 
"cone hull {} = {}" 

823 
by (metis cone_empty cone_hull_eq) 

824 

825 
lemma cone_hull_empty_iff: 

826 
shows "(S = {}) <> (cone hull S = {})" 

827 
by (metis bot_least cone_hull_empty hull_subset xtrans(5)) 

828 

829 
lemma cone_hull_contains_0: 

830 
shows "(S ~= {}) <> (0 : cone hull S)" 

831 
using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S] by auto 

832 

833 
lemma mem_cone_hull: 

834 
assumes "x : S" "c>=0" 

835 
shows "c *\<^sub>R x : cone hull S" 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

836 
by (metis assms cone_cone_hull hull_inc mem_cone) 
40377  837 

838 
lemma cone_hull_expl: 

839 
shows "cone hull S = {c *\<^sub>R x  c x. c>=0 & x : S}" (is "?lhs = ?rhs") 

840 
proof 

841 
{ fix x assume "x : ?rhs" 

842 
from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto 

843 
fix c assume c_def: "(c :: real)>=0" 

844 
hence "c *\<^sub>R x = (c*cx) *\<^sub>R xx" using x_def by (simp add: algebra_simps) 

845 
moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto 

846 
ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto 

847 
} hence "cone ?rhs" unfolding cone_def by auto 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

848 
hence "?rhs : Collect cone" unfolding mem_Collect_eq by auto 
40377  849 
{ fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto 
850 
hence "x : ?rhs" by auto 

851 
} hence "S <= ?rhs" by auto 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

852 
hence "?lhs <= ?rhs" using `?rhs : Collect cone` hull_minimal[of S "?rhs" "cone"] by auto 
40377  853 
moreover 
854 
{ fix x assume "x : ?rhs" 

855 
from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto 

856 
hence "xx : cone hull S" using hull_subset[of S] by auto 

857 
hence "x : ?lhs" using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto 

858 
} ultimately show ?thesis by auto 

859 
qed 

860 

861 
lemma cone_closure: 

44524  862 
fixes S :: "('a::real_normed_vector) set" 
863 
assumes "cone S" shows "cone (closure S)" 

40377  864 
proof 
865 
{ assume "S = {}" hence ?thesis by auto } 

866 
moreover 

867 
{ assume "S ~= {}" hence "0:S & (!c. c>0 > op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto 

868 
hence "0:(closure S) & (!c. c>0 > op *\<^sub>R c ` (closure S) = (closure S))" 

869 
using closure_subset by (auto simp add: closure_scaleR) 

870 
hence ?thesis using cone_iff[of "closure S"] by auto 

871 
} 

872 
ultimately show ?thesis by blast 

873 
qed 

874 

44467  875 
subsection {* Affine dependence and consequential theorems (from Lars Schewe) *} 
33175  876 

877 
definition 

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

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

880 

881 
lemma affine_dependent_explicit: 

882 
"affine_dependent p \<longleftrightarrow> 

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

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

885 
unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq apply(rule) 

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

887 
proof 

888 
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" 

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

890 
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" 

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

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

893 
next 

894 
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" 

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

896 
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" 

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

898 
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 

899 
qed 

900 

901 
lemma affine_dependent_explicit_finite: 

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

903 
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)" 

904 
(is "?lhs = ?rhs") 

905 
proof 

906 
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 

907 
assume ?lhs 

908 
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" 

909 
unfolding affine_dependent_explicit by auto 

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

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

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

913 
next 

914 
assume ?rhs 

915 
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 

916 
thus ?lhs unfolding affine_dependent_explicit using assms by auto 

917 
qed 

918 

44465
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

919 
subsection {* Connectedness of convex sets *} 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

920 

fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

921 
lemma connected_real_lemma: 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

922 
fixes f :: "real \<Rightarrow> 'a::metric_space" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

923 
assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

924 
and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y  x) < d \<longrightarrow> dist(f y) (f x) < e" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

925 
and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

926 
and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

927 
and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

928 
shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x") 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

929 
proof 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

930 
let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

931 
have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa) 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

932 
have Sub: "\<exists>y. isUb UNIV ?S y" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

933 
apply (rule exI[where x= b]) 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

934 
using ab fb e12 by (auto simp add: isUb_def setle_def) 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

935 
from reals_complete[OF Se Sub] obtain l where 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

936 
l: "isLub UNIV ?S l"by blast 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

937 
have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

938 
apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

939 
by (metis linorder_linear) 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

940 
have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

941 
apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

942 
by (metis linorder_linear not_le) 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

943 
have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z  x) < d" by arith 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

944 
have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

945 
have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

946 
then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

947 
{assume le2: "f l \<in> e2" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

948 
from le2 fa fb e12 alb have la: "l \<noteq> a" by metis 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

949 
hence lap: "l  a > 0" using alb by arith 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

950 
from e2[rule_format, OF le2] obtain e where 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

951 
e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

952 
from dst[OF alb e(1)] obtain d where 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

953 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

954 
let ?d' = "min (d/2) ((l  a)/2)" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

955 
have "?d' < d \<and> 0 < ?d' \<and> ?d' < l  a" using lap d(1) 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

956 
by (simp add: min_max.less_infI2) 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

957 
then have "\<exists>d'. d' < d \<and> d' >0 \<and> l  d' > a" by auto 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

958 
then obtain d' where d': "d' > 0" "d' < d" "l  d' > a" by metis 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

959 
from d e have th0: "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> f y \<in> e2" by metis 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

960 
from th0[rule_format, of "l  d'"] d' have "f (l  d') \<in> e2" by auto 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

961 
moreover 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

962 
have "f (l  d') \<in> e1" using ale1[rule_format, of "l d'"] d' by auto 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

963 
ultimately have False using e12 alb d' by auto} 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

964 
moreover 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

965 
{assume le1: "f l \<in> e1" 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

966 
from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

967 
hence blp: "b  l > 0" using alb by arith 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

968 
from e1[rule_format, OF le1] obtain e where 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

969 
e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

970 
from dst[OF alb e(1)] obtain d where 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

971 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

972 
have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

973 
then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

974 
then obtain d' where d': "d' > 0" "d' < d" by metis 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

975 
from d e have th0: "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> f y \<in> e1" by auto 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

976 
hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

977 
with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

978 
with l d' have False 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

979 
by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

980 
ultimately show ?thesis using alb by metis 
fa56622bb7bc
move connected_real_lemma to the one place it is used
huffman
parents:
44457
diff
changeset

981 
qed 
33175  982 

983 
lemma convex_connected: 

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

985 
assumes "convex s" shows "connected s" 

986 
proof 

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

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

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

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

991 

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

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

994 
by (simp add: algebra_simps) 

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

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

997 
unfolding * and scaleR_right_diff_distrib[THEN sym] 

998 
unfolding less_divide_eq using n by auto } 

999 
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" 

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

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

1002 

1003 
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" 

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

1005 
using * apply(simp add: dist_norm) 

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

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

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

1009 
using as(3) by auto 

1010 
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 

1011 
hence False using as(4) 

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

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

1014 
thus ?thesis unfolding connected_def by auto 

1015 
qed 

1016 

44467  1017 
text {* One rather trivial consequence. *} 
33175  1018 

34964  1019 
lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)" 
33175  1020 
by(simp add: convex_connected convex_UNIV) 
1021 

44467  1022 
text {* Balls, being convex, are connected. *} 
33175  1023 

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

1024 
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

1025 
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

1026 
shows "convex {x. \<forall>i<DIM('a). P i (x$$i)}" 
44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44365
diff
changeset

1027 
using assms unfolding convex_def by auto 
33175  1028 

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

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

1032 
lemma convex_local_global_minimum: 

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

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

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

1036 
proof(rule ccontr) 

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

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

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

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

1041 

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

1043 
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 

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

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

1046 
moreover 

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

1048 
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] 

1049 
using u unfolding pos_less_divide_eq[OF xy] by auto 

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

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

1052 
qed 

1053 

1054 
lemma convex_ball: 

1055 
fixes x :: "'a::real_normed_vector" 

1056 
shows "convex (ball x e)" 

1057 
proof(auto simp add: convex_def) 

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

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

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

1061 
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  1062 
thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using convex_bound_lt[OF yz uv] by auto 
33175  1063 
qed 
1064 

1065 
lemma convex_cball: 

1066 
fixes x :: "'a::real_normed_vector" 

1067 
shows "convex(cball x e)" 

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

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

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

1072 
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  1073 
thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using convex_bound_le[OF yz uv] by auto 
33175  1074 
qed 
1075 

1076 
lemma connected_ball: 

1077 
fixes x :: "'a::real_normed_vector" 

1078 
shows "connected (ball x e)" 

1079 
using convex_connected convex_ball by auto 

1080 

1081 
lemma connected_cball: 

1082 
fixes x :: "'a::real_normed_vector" 

1083 
shows "connected(cball x e)" 

1084 
using convex_connected convex_cball by auto 

1085 

44467  1086 
subsection {* Convex hull *} 
33175  1087 

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

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

1089 
unfolding hull_def using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"] 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

1090 
by auto 
33175  1091 

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

1092 
lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s" 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

1093 
by (metis convex_convex_hull hull_same) 
33175  1094 

1095 
lemma bounded_convex_hull: 

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

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

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

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

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

1100 
unfolding subset_hull[of convex, OF convex_cball] 
33175  1101 
unfolding subset_eq mem_cball dist_norm using B by auto qed 
1102 

1103 
lemma finite_imp_bounded_convex_hull: 

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

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

1106 
using bounded_convex_hull finite_imp_bounded by auto 

1107 

44467  1108 
subsubsection {* Convex hull is "preserved" by a linear function *} 
40377  1109 

1110 
lemma convex_hull_linear_image: 

1111 
assumes "bounded_linear f" 

1112 
shows "f ` (convex hull s) = convex hull (f ` s)" 

1113 
apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 

1114 
apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption 

1115 
apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption 

1116 
proof 

1117 
interpret f: bounded_linear f by fact 

1118 
show "convex {x. f x \<in> convex hull f ` s}" 

1119 
unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next 

1120 
interpret f: bounded_linear f by fact 

1121 
show "convex {x. x \<in> f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s] 

1122 
unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric]) 

1123 
qed auto 

1124 

1125 
lemma in_convex_hull_linear_image: 

1126 
assumes "bounded_linear f" "x \<in> convex hull s" 

1127 
shows "(f x) \<in> convex hull (f ` s)" 

1128 
using convex_hull_linear_image[OF assms(1)] assms(2) by auto 

1129 

44467  1130 
subsubsection {* Stepping theorems for convex hulls of finite sets *} 
33175  1131 

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

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

1133 
apply(rule hull_unique) by auto 
33175  1134 

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

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

1136 
apply(rule hull_unique) by auto 
33175  1137 

1138 
lemma convex_hull_insert: 

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

1140 
assumes "s \<noteq> {}" 

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

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

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44142
diff
changeset

1143 
apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof 
33175  1144 
fix x assume x:"x = a \<or> x \<in> s" 
1145 
thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer 

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

1147 
next 

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

1149 
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 

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

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

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

1153 
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 

1154 
next 

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

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

1157 
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 

1158 
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 

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

1160 
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)" 

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

1162 
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  1163 
case True hence **:"u * v1 = 0" "v * v2 = 0" 
1164 
using mult_nonneg_nonneg[OF `u\<ge>0` `v1\<ge>0`] mult_nonneg_nonneg[OF `v\<ge>0` `v2\<ge>0`] by arith+ 

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

1167 
next 

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

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

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

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

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

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

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

1175 
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 

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

44349
f057535311c5
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
huffman
parents:
44282
diff
changeset

1177 
unfolding add_divide_distrib[THEN sym] and zero_le_divide_iff 
33175  1178 
by (auto simp add: scaleR_left_distrib scaleR_right_distrib) 
1179 
qed note * = this 

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

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

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44170
diff
changeset

1184 
also have "\<dots> \<le> 1" unfolding right_distrib[THEN sym] and as(3) using u1 u2 by auto 
33175  1185 
finally 
1186 
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) 

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

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

1189 
qed 

1190 
qed 

1191 

1192 

44467  1193 
subsubsection {* Explicit expression for convex hull *} 
33175  1194 

1195 
lemma convex_hull_indexed: 

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

1197 
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> 

