author | huffman |
Tue, 23 Aug 2011 16:17:22 -0700 | |
changeset 44465 | fa56622bb7bc |
parent 44457 | d366fa5551ef |
child 44466 | 0e5c27f07529 |
permissions | -rw-r--r-- |
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 "x-a : S" using assms by auto |
|
188 |
hence "x : {a + v |v. v : S}" apply auto apply (rule exI[of _ "x-a"]) 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(1-3) |
|
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 |
apply-apply(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(1-3) y(1-3) 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 (y-z) : 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 = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto |
|
686 |
moreover have "(1-c) *\<^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 "(1-u) *\<^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 ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * 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="1-u"]] 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 |