author  huffman 
Tue, 23 Aug 2011 16:17:22 0700  
changeset 44465  fa56622bb7bc 
parent 44457  d366fa5551ef 
child 44466  0e5c27f07529 
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 card_ge1: assumes "d ~= {}" "finite d" shows "card d >= 1" 

44 
by (metis Suc_eq_plus1 assms(1) assms(2) card_eq_0_iff fact_ge_one_nat fact_num_eq_if_nat one_le_mult_iff plus_nat.add_0) 

45 

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

47 
by (blast dest: inj_onD) 

48 

49 
lemma independent_injective_on_span_image: 

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

50 
assumes iS: "independent S" 
40377  51 
and lf: "linear f" and fi: "inj_on f (span S)" 
52 
shows "independent (f ` S)" 

53 
proof 

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

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

56 
by (auto simp add: inj_on_def) 

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

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

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

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

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

62 
then show ?thesis unfolding dependent_def by blast 

63 
qed 

64 

65 
lemma dim_image_eq: 

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

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

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

69 
proof 

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

71 
using basis_exists[of S] by auto 

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

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

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

75 
B_def span_inc by auto 

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

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

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

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

80 
qed 

81 

82 
lemma linear_injective_on_subspace_0: 

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

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

85 
proof 

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

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

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

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

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

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

92 
finally show ?thesis . 

93 
qed 

94 

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

96 
unfolding subspace_def by auto 

97 

98 
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

99 
unfolding span_def by (rule hull_eq, rule subspace_Inter) 
40377  100 

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

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

103 

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

105 
proof 

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

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

108 
qed 

109 

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

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

112 
proof 

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

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

115 
qed 

116 

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

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

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

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

121 
have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp 

122 
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

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

126 
qed 

127 

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

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

130 
proof  

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

132 
show ?thesis 

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

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

135 
qed 

136 

137 
lemma dim_cball: 

138 
assumes "0<e" 

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

140 
proof 

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

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

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

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

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

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

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

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

149 
qed 

150 

151 
lemma indep_card_eq_dim_span: 

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

153 
assumes "independent B" 

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

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

156 

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

158 
apply(rule ccontr) by auto 

159 

160 
lemma translate_inj_on: 

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

161 
fixes A :: "('a::ab_group_add) set" 
40377  162 
shows "inj_on (%x. a+x) A" unfolding inj_on_def by auto 
163 

164 
lemma translation_assoc: 

165 
fixes a b :: "'a::ab_group_add" 

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

167 

168 
lemma translation_invert: 

169 
fixes a :: "'a::ab_group_add" 

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

171 
shows "A=B" 

172 
proof 

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

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

175 
qed 

176 

177 
lemma translation_galois: 

178 
fixes a :: "'a::ab_group_add" 

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

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

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

182 

183 
lemma translation_inverse_subset: 

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

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

186 
proof 

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

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

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

190 
from this show ?thesis by auto 

191 
qed 

192 

193 
lemma basis_to_basis_subspace_isomorphism: 

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

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

196 
and d: "dim S = dim T" 

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

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

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

200 
proof 

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

202 
*) 

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

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

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

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

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

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

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

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

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

212 
by simp 

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

214 
by (auto simp add: image_iff) 

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

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

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

218 
by (auto simp add: inj_on_def) 

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

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

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

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

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

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

225 
then have giS: "inj_on g S" 

226 
unfolding inj_on_def by blast 

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

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

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

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

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

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

233 
qed 

234 

235 
lemma closure_linear_image: 

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

236 
fixes f :: "('m::euclidean_space) => ('n::real_normed_vector)" 
40377  237 
assumes "linear f" 
238 
shows "f ` (closure S) <= closure (f ` S)" 

239 
using image_closure_subset[of S f "closure (f ` S)"] assms linear_conv_bounded_linear[of f] 

240 
linear_continuous_on[of f "closure S"] closed_closure[of "f ` S"] closure_subset[of "f ` S"] by auto 

241 

242 
lemma closure_injective_linear_image: 

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

244 
assumes "linear f" "inj f" 

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

246 
proof 

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

248 
using assms linear_injective_isomorphism[of f] isomorphism_expand by auto 

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

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

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

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

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

254 
qed 

255 

256 
lemma closure_direct_sum: 

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

44365  258 
by (rule closure_Times) 
40377  259 

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

260 
lemma closure_scaleR: (* TODO: generalize to real_normed_vector *) 
40377  261 
fixes S :: "('n::euclidean_space) set" 
262 
shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)" 

263 
proof 

264 
{ assume "c ~= 0" hence ?thesis using closure_injective_linear_image[of "(op *\<^sub>R c)" S] 

265 
linear_scaleR injective_scaleR by auto 

266 
} 

267 
moreover 

268 
{ assume zero: "c=0 & S ~= {}" 

269 
hence "closure S ~= {}" using closure_subset by auto 

270 
hence "op *\<^sub>R c ` (closure S) = {0}" using zero by auto 

271 
moreover have "op *\<^sub>R 0 ` S = {0}" using zero by auto 

272 
ultimately have ?thesis using zero by auto 

273 
} 

274 
moreover 

275 
{ assume "S={}" hence ?thesis by auto } 

276 
ultimately show ?thesis by blast 

277 
qed 

278 

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

280 

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

282 

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

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

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

285 
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

286 
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

287 
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

288 
unfolding one_add_one_is_two [symmetric] scaleR_left_distrib by simp 
34964  289 

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

290 
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

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

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

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

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

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

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

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

299 

300 
lemma setsum_delta'': 

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

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

303 
proof 

304 
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 

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

306 
qed 

307 

308 
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 

309 

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

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

313 

314 
lemma dist_triangle_eq: 

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

315 
fixes x y z :: "'a::real_inner" 
33175  316 
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)" 
317 
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

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

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

321 
lemma norm_minus_eqI:"x =  y \<Longrightarrow> norm x = norm y" by auto 
33175  322 

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

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

325 

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

326 
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

327 
unfolding norm_eq_sqrt_inner by simp 
33175  328 

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

329 
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

330 
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

331 

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

332 

33175  333 

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

335 

336 
definition 

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

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

339 

340 
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  341 
unfolding affine_def by(metis eq_diff_eq') 
33175  342 

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

344 
unfolding affine_def by auto 

345 

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

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

348 

349 
lemma affine_UNIV[intro]: "affine UNIV" 

350 
unfolding affine_def by auto 

351 

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

353 
unfolding affine_def by auto 

354 

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

356 
unfolding affine_def by auto 

357 

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

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

359 
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

360 
by auto 
33175  361 

362 
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

363 
by (metis affine_affine_hull hull_same) 
33175  364 

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

366 

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

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

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

370 
defer apply(rule, rule, rule, rule, rule) proof 

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

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

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

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

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

376 
next 

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

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

379 
def n \<equiv> "card s" 

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

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

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

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

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

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

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

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

388 
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  389 
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 
390 
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  391 
"finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1" 
392 
have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr) 

393 
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 

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

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

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

397 

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

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

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

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

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

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

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

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

406 
thus False using True by auto qed auto 

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

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

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

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

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

412 
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

413 
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

414 
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

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

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

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

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

423 
qed 

424 

425 
lemma affine_hull_explicit: 

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

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

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

431 
next 

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

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

434 
next 

435 
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 

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

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

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

439 
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 

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

441 
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 

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

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

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

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

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

447 
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

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

451 
lemma affine_hull_finite: 

452 
assumes "finite s" 

453 
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

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

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

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

459 
next 

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

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

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

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

464 

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

466 

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

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

468 
apply(rule hull_unique) by auto 
33175  469 

470 
lemma affine_hull_finite_step: 

471 
fixes y :: "'a::real_vector" 

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

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

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

475 
proof 

476 
show ?th1 by simp 

477 
assume ?as 

478 
{ assume ?lhs 

479 
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 

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

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

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

483 
next 

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

485 
qed } moreover 

486 
{ assume ?rhs 

487 
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 

488 
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 

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

490 
case True thus ?thesis 

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

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

493 
unfolding scaleR_left_distrib and setsum_addf 

494 
unfolding vu and * and scaleR_zero_left 

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

496 
next 

497 
case False 

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

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

500 
from False show ?thesis 

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

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

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

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

505 
qed } 

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

507 
qed 

508 

509 
lemma affine_hull_2: 

510 
fixes a b :: "'a::real_vector" 

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

512 
proof 

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

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

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

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

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

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

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

520 
finally show ?thesis by auto 

521 
qed 

522 

523 
lemma affine_hull_3: 

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

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

526 
proof 

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

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

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

530 
unfolding * apply auto 

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

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

533 
qed 

534 

40377  535 
lemma mem_affine: 
536 
assumes "affine S" "x : S" "y : S" "u+v=1" 

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

538 
using assms affine_def[of S] by auto 

539 

540 
lemma mem_affine_3: 

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

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

543 
proof 

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

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

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

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

548 
moreover have "affine hull S = S" 

549 
using assms affine_hull_eq[of S] by auto 

550 
ultimately show ?thesis by auto 

551 
qed 

552 

553 
lemma mem_affine_3_minus: 

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

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

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

557 

558 

33175  559 
subsection {* Some relations between affine hull and subspaces. *} 
560 

561 
lemma affine_hull_insert_subset_span: 

562 
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

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

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

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

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

569 
apply (rule conjI, simp) 

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

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

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

573 
apply (erule conjI) 

574 
using as(1) 

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

576 
unfolding as by simp qed 

577 

578 
lemma affine_hull_insert_span: 

579 
assumes "a \<notin> s" 

580 
shows "affine hull (insert a s) = 

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

582 
apply(rule, rule affine_hull_insert_subset_span) unfolding subset_eq Ball_def 

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

584 
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

585 
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  586 
def f \<equiv> "(\<lambda>x. x + a) ` t" 
587 
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 

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

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

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

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

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

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

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

33175  596 

597 
lemma affine_hull_span: 

598 
assumes "a \<in> s" 

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

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

601 

40377  602 
subsection{* Parallel Affine Sets *} 
603 

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

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

606 

607 
lemma affine_parallel_expl_aux: 

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

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

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

611 
proof 

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

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

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

615 
ultimately show ?thesis by auto 

616 
qed 

617 

618 
lemma affine_parallel_expl: 

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

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

621 

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

623 

624 
lemma affine_parallel_commut: 

625 
assumes "affine_parallel A B" shows "affine_parallel B A" 

626 
proof 

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

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

629 
qed 

630 

631 
lemma affine_parallel_assoc: 

632 
assumes "affine_parallel A B" "affine_parallel B C" 

633 
shows "affine_parallel A C" 

634 
proof 

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

636 
moreover 

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

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

639 
qed 

640 

641 
lemma affine_translation_aux: 

642 
fixes a :: "'a::real_vector" 

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

644 
proof 

645 
{ fix x y u v 

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

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

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

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

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

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

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

653 
} from this show ?thesis unfolding affine_def by auto 

654 
qed 

655 

656 
lemma affine_translation: 

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

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

659 
proof 

660 
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 

661 
from this show ?thesis using affine_translation_aux by auto 

662 
qed 

663 

664 
lemma parallel_is_affine: 

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

666 
assumes "affine S" "affine_parallel S T" 

667 
shows "affine T" 

668 
proof 

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

670 
from this show ?thesis using affine_translation assms by auto 

671 
qed 

672 

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

673 
lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s" 
40377  674 
unfolding subspace_def affine_def by auto 
675 

676 
subsection{* Subspace Parallel to an Affine Set *} 

677 

678 
lemma subspace_affine: 

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

680 
proof 

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

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

683 
{ fix c :: real 

684 
fix x assume x_def: "x : S" 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

699 
} from this show ?thesis using h0 by metis 

700 
qed 

701 

702 
lemma affine_diffs_subspace: 

703 
assumes "affine S" "a : S" 

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

705 
proof 

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

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

708 
ultimately show ?thesis using subspace_affine by auto 

709 
qed 

710 

711 
lemma parallel_subspace_explicit: 

712 
assumes "affine S" "a : S" 

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

714 
shows "subspace L & affine_parallel S L" 

715 
proof 

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

717 
hence "affine L" using assms parallel_is_affine by auto 

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

719 
ultimately show ?thesis using subspace_affine par by auto 

720 
qed 

721 

722 
lemma parallel_subspace_aux: 

723 
assumes "subspace A" "subspace B" "affine_parallel A B" 

724 
shows "A>=B" 

725 
proof 

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

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

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

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

730 
qed 

731 

732 
lemma parallel_subspace: 

733 
assumes "subspace A" "subspace B" "affine_parallel A B" 

734 
shows "A=B" 

735 
proof 

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

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

738 
ultimately show ?thesis by auto 

739 
qed 

740 

741 
lemma affine_parallel_subspace: 

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

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

744 
proof 

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

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

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

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

749 
} from this show ?thesis using ex by auto 

750 
qed 

751 

33175  752 
subsection {* Cones. *} 
753 

754 
definition 

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

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

757 

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

759 
unfolding cone_def by auto 

760 

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

762 
unfolding cone_def by auto 

763 

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

765 
unfolding cone_def by auto 

766 

767 
subsection {* Conic hull. *} 

768 

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

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

770 
unfolding hull_def by auto 
33175  771 

772 
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

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

774 
using cone_Inter unfolding subset_eq by auto 
33175  775 

40377  776 
lemma mem_cone: 
777 
assumes "cone S" "x : S" "c>=0" 

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

779 
using assms cone_def[of S] by auto 

780 

781 
lemma cone_contains_0: 

782 
assumes "cone S" 

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

784 
proof 

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

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

787 
} from this show ?thesis by auto 

788 
qed 

789 

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

790 
lemma cone_0: "cone {0}" 
40377  791 
unfolding cone_def by auto 
792 

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

794 
unfolding cone_def by blast 

795 

796 
lemma cone_iff: 

797 
assumes "S ~= {}" 

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

799 
proof 

800 
{ assume "cone S" 

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

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

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

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

805 
} 

806 
moreover 

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

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

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

810 
} 

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

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

813 
} 

814 
moreover 

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

816 
{ fix x assume "x:S" 

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

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

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

820 
} 

821 
hence "cone S" unfolding cone_def by auto 

822 
} ultimately show ?thesis by blast 

823 
qed 

824 

825 
lemma cone_hull_empty: 

826 
"cone hull {} = {}" 

827 
by (metis cone_empty cone_hull_eq) 

828 

829 
lemma cone_hull_empty_iff: 

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

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

832 

833 
lemma cone_hull_contains_0: 

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

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

836 

837 
lemma mem_cone_hull: 

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

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

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

840 
by (metis assms cone_cone_hull hull_inc mem_cone) 
40377  841 

842 
lemma cone_hull_expl: 

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

844 
proof 

845 
{ fix x assume "x : ?rhs" 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

862 
} ultimately show ?thesis by auto 

863 
qed 

864 

865 
lemma cone_closure: 

866 
fixes S :: "('m::euclidean_space) set" 

867 
assumes "cone S" 

868 
shows "cone (closure S)" 

869 
proof 

870 
{ assume "S = {}" hence ?thesis by auto } 

871 
moreover 

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

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

874 
using closure_subset by (auto simp add: closure_scaleR) 

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

876 
} 

877 
ultimately show ?thesis by blast 

878 
qed 

879 

33175  880 
subsection {* Affine dependence and consequential theorems (from Lars Schewe). *} 
881 

882 
definition 

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

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

885 

886 
lemma affine_dependent_explicit: 

887 
"affine_dependent p \<longleftrightarrow> 

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

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

890 
unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq apply(rule) 

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

892 
proof 

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

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

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

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

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

898 
next 

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

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

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

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

903 
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 

904 
qed 

905 

906 
lemma affine_dependent_explicit_finite: 

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

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

909 
(is "?lhs = ?rhs") 

910 
proof 

911 
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 

912 
assume ?lhs 

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

914 
unfolding affine_dependent_explicit by auto 

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

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

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

918 
next 

919 
assume ?rhs 

920 
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 

921 
thus ?lhs unfolding affine_dependent_explicit using assms by auto 

922 
qed 

923 

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

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

925 

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

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

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

928 
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

929 
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

930 
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

931 
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

932 
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

933 
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

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

935 
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

936 
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

937 
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

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

939 
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

940 
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

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

942 
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

943 
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

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

945 
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

946 
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

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

948 
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

949 
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

950 
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

951 
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

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

953 
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

954 
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

955 
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

956 
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

957 
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

958 
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

959 
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

960 
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

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

962 
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

963 
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

964 
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

965 
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

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

967 
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

968 
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

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

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

971 
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

972 
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

973 
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

974 
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

975 
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

976 
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

977 
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

978 
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

979 
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

980 
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

981 
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

982 
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

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

984 
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

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

986 
qed 
33175  987 

988 
lemma convex_connected: 

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

990 
assumes "convex s" shows "connected s" 

991 
proof 

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

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

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

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

996 

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

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

999 
by (simp add: algebra_simps) 

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

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

1002 
unfolding * and scaleR_right_diff_distrib[THEN sym] 

1003 
unfolding less_divide_eq using n by auto } 

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

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

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

1007 

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

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

1010 
using * apply(simp add: dist_norm) 

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

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

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

1014 
using as(3) by auto 

1015 
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 

1016 
hence False using as(4) 

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

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

1019 
thus ?thesis unfolding connected_def by auto 

1020 
qed 

1021 

1022 
subsection {* One rather trivial consequence. *} 

1023 

34964  1024 
lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)" 
33175  1025 
by(simp add: convex_connected convex_UNIV) 
1026 

36623  1027 
subsection {* Balls, being convex, are connected. *} 
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_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

1030 
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

1031 
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

1032 
using assms unfolding convex_def by auto 
33175  1033 

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

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

1037 
lemma convex_local_global_minimum: 

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

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

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

1041 
proof(rule ccontr) 

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

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

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

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

1046 

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

1048 
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 

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

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

1051 
moreover 

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

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

1054 
using u unfolding pos_less_divide_eq[OF xy] by auto 

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

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

1057 
qed 

1058 

1059 
lemma convex_ball: 

1060 
fixes x :: "'a::real_normed_vector" 

1061 
shows "convex (ball x e)" 

1062 
proof(auto simp add: convex_def) 

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

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

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

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

1070 
lemma convex_cball: 

1071 
fixes x :: "'a::real_normed_vector" 

1072 
shows "convex(cball x e)" 

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

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

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

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

1081 
lemma connected_ball: 

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

1083 
shows "connected (ball x e)" 

1084 
using convex_connected convex_ball by auto 

1085 

1086 
lemma connected_cball: 

1087 
fixes x :: "'a::real_normed_vector" 

1088 
shows "connected(cball x e)" 

1089 
using convex_connected convex_cball by auto 

1090 

1091 
subsection {* Convex hull. *} 

1092 

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

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

1094 
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

1095 
by auto 
33175  1096 

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

1097 
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

1098 
by (metis convex_convex_hull hull_same) 
33175  1099 

1100 
lemma bounded_convex_hull: 

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

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

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

1104 
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

1105 
unfolding subset_hull[of convex, OF convex_cball] 
33175  1106 
unfolding subset_eq mem_cball dist_norm using B by auto qed 
1107 

1108 
lemma finite_imp_bounded_convex_hull: 

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

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

1111 
using bounded_convex_hull finite_imp_bounded by auto 

1112 

40377  1113 
subsection {* Convex hull is "preserved" by a linear function. *} 
1114 

1115 
lemma convex_hull_linear_image: 

1116 
assumes "bounded_linear f" 

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

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

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

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

1121 
proof 

1122 
interpret f: bounded_linear f by fact 

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

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

1125 
interpret f: bounded_linear f by fact 

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

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

1128 
qed auto 

1129 

1130 
lemma in_convex_hull_linear_image: 

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

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

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

1134 

33175  1135 
subsection {* Stepping theorems for convex hulls of finite sets. *} 
1136 

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

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

1138 
apply(rule hull_unique) by auto 
33175  1139 

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

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

1141 
apply(rule hull_unique) by auto 
33175  1142 

1143 
lemma convex_hull_insert: 

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

1145 
assumes "s \<noteq> {}" 

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

1147 
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

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

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

1152 
next 

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

1154 
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 

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

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

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

1158 
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 

1159 
next 

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

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

1162 
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 

1163 
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 

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

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

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

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

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

1172 
next 

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

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

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

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

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

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

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

1180 
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 

1181 
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

1182 
unfolding add_divide_distrib[THEN sym] and zero_le_divide_iff 
33175  1183 
by (auto simp add: scaleR_left_distrib scaleR_right_distrib) 
1184 
qed note * = this 

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

33175  1187 
have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono) 
1188 
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

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

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

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

1194 
qed 

1195 
qed 

1196 

1197 

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

1199 

1200 
lemma convex_hull_indexed: 

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

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

1203 