71243
|
1 |
section "Affine Sets"
|
|
2 |
|
71242
|
3 |
theory Affine
|
|
4 |
imports Linear_Algebra
|
|
5 |
begin
|
|
6 |
|
|
7 |
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)"
|
|
8 |
by (fact if_distrib)
|
|
9 |
|
|
10 |
lemma sum_delta_notmem:
|
|
11 |
assumes "x \<notin> s"
|
|
12 |
shows "sum (\<lambda>y. if (y = x) then P x else Q y) s = sum Q s"
|
|
13 |
and "sum (\<lambda>y. if (x = y) then P x else Q y) s = sum Q s"
|
|
14 |
and "sum (\<lambda>y. if (y = x) then P y else Q y) s = sum Q s"
|
|
15 |
and "sum (\<lambda>y. if (x = y) then P y else Q y) s = sum Q s"
|
|
16 |
apply (rule_tac [!] sum.cong)
|
|
17 |
using assms
|
|
18 |
apply auto
|
|
19 |
done
|
|
20 |
|
|
21 |
lemmas independent_finite = independent_imp_finite
|
|
22 |
|
|
23 |
lemma span_substd_basis:
|
|
24 |
assumes d: "d \<subseteq> Basis"
|
|
25 |
shows "span d = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
|
|
26 |
(is "_ = ?B")
|
|
27 |
proof -
|
|
28 |
have "d \<subseteq> ?B"
|
|
29 |
using d by (auto simp: inner_Basis)
|
|
30 |
moreover have s: "subspace ?B"
|
|
31 |
using subspace_substandard[of "\<lambda>i. i \<notin> d"] .
|
|
32 |
ultimately have "span d \<subseteq> ?B"
|
|
33 |
using span_mono[of d "?B"] span_eq_iff[of "?B"] by blast
|
|
34 |
moreover have *: "card d \<le> dim (span d)"
|
|
35 |
using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms]
|
|
36 |
span_superset[of d]
|
|
37 |
by auto
|
|
38 |
moreover from * have "dim ?B \<le> dim (span d)"
|
|
39 |
using dim_substandard[OF assms] by auto
|
|
40 |
ultimately show ?thesis
|
|
41 |
using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto
|
|
42 |
qed
|
|
43 |
|
|
44 |
lemma basis_to_substdbasis_subspace_isomorphism:
|
|
45 |
fixes B :: "'a::euclidean_space set"
|
|
46 |
assumes "independent B"
|
|
47 |
shows "\<exists>f d::'a set. card d = card B \<and> linear f \<and> f ` B = d \<and>
|
|
48 |
f ` span B = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} \<and> inj_on f (span B) \<and> d \<subseteq> Basis"
|
|
49 |
proof -
|
|
50 |
have B: "card B = dim B"
|
|
51 |
using dim_unique[of B B "card B"] assms span_superset[of B] by auto
|
|
52 |
have "dim B \<le> card (Basis :: 'a set)"
|
|
53 |
using dim_subset_UNIV[of B] by simp
|
|
54 |
from ex_card[OF this] obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B"
|
|
55 |
by auto
|
|
56 |
let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
|
|
57 |
have "\<exists>f. linear f \<and> f ` B = d \<and> f ` span B = ?t \<and> inj_on f (span B)"
|
|
58 |
proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_superset)
|
|
59 |
show "d \<subseteq> {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
|
|
60 |
using d inner_not_same_Basis by blast
|
|
61 |
qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms)
|
|
62 |
with t \<open>card B = dim B\<close> d show ?thesis by auto
|
|
63 |
qed
|
|
64 |
|
|
65 |
subsection \<open>Affine set and affine hull\<close>
|
|
66 |
|
|
67 |
definition\<^marker>\<open>tag important\<close> affine :: "'a::real_vector set \<Rightarrow> bool"
|
|
68 |
where "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)"
|
|
69 |
|
|
70 |
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)"
|
|
71 |
unfolding affine_def by (metis eq_diff_eq')
|
|
72 |
|
|
73 |
lemma affine_empty [iff]: "affine {}"
|
|
74 |
unfolding affine_def by auto
|
|
75 |
|
|
76 |
lemma affine_sing [iff]: "affine {x}"
|
|
77 |
unfolding affine_alt by (auto simp: scaleR_left_distrib [symmetric])
|
|
78 |
|
|
79 |
lemma affine_UNIV [iff]: "affine UNIV"
|
|
80 |
unfolding affine_def by auto
|
|
81 |
|
|
82 |
lemma affine_Inter [intro]: "(\<And>s. s\<in>f \<Longrightarrow> affine s) \<Longrightarrow> affine (\<Inter>f)"
|
|
83 |
unfolding affine_def by auto
|
|
84 |
|
|
85 |
lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
|
|
86 |
unfolding affine_def by auto
|
|
87 |
|
|
88 |
lemma affine_scaling: "affine s \<Longrightarrow> affine (image (\<lambda>x. c *\<^sub>R x) s)"
|
|
89 |
apply (clarsimp simp add: affine_def)
|
|
90 |
apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI)
|
|
91 |
apply (auto simp: algebra_simps)
|
|
92 |
done
|
|
93 |
|
|
94 |
lemma affine_affine_hull [simp]: "affine(affine hull s)"
|
|
95 |
unfolding hull_def
|
|
96 |
using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] by auto
|
|
97 |
|
|
98 |
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
|
|
99 |
by (metis affine_affine_hull hull_same)
|
|
100 |
|
|
101 |
lemma affine_hyperplane: "affine {x. a \<bullet> x = b}"
|
|
102 |
by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)
|
|
103 |
|
|
104 |
|
|
105 |
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Some explicit formulations\<close>
|
|
106 |
|
|
107 |
text "Formalized by Lars Schewe."
|
|
108 |
|
|
109 |
lemma affine:
|
|
110 |
fixes V::"'a::real_vector set"
|
|
111 |
shows "affine V \<longleftrightarrow>
|
|
112 |
(\<forall>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> V \<and> sum u S = 1 \<longrightarrow> (\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V)"
|
|
113 |
proof -
|
|
114 |
have "u *\<^sub>R x + v *\<^sub>R y \<in> V" if "x \<in> V" "y \<in> V" "u + v = (1::real)"
|
|
115 |
and *: "\<And>S u. \<lbrakk>finite S; S \<noteq> {}; S \<subseteq> V; sum u S = 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V" for x y u v
|
|
116 |
proof (cases "x = y")
|
|
117 |
case True
|
|
118 |
then show ?thesis
|
|
119 |
using that by (metis scaleR_add_left scaleR_one)
|
|
120 |
next
|
|
121 |
case False
|
|
122 |
then show ?thesis
|
|
123 |
using that *[of "{x,y}" "\<lambda>w. if w = x then u else v"] by auto
|
|
124 |
qed
|
|
125 |
moreover have "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V"
|
|
126 |
if *: "\<And>x y u v. \<lbrakk>x\<in>V; y\<in>V; u + v = 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
|
|
127 |
and "finite S" "S \<noteq> {}" "S \<subseteq> V" "sum u S = 1" for S u
|
|
128 |
proof -
|
|
129 |
define n where "n = card S"
|
|
130 |
consider "card S = 0" | "card S = 1" | "card S = 2" | "card S > 2" by linarith
|
|
131 |
then show "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V"
|
|
132 |
proof cases
|
|
133 |
assume "card S = 1"
|
|
134 |
then obtain a where "S={a}"
|
|
135 |
by (auto simp: card_Suc_eq)
|
|
136 |
then show ?thesis
|
|
137 |
using that by simp
|
|
138 |
next
|
|
139 |
assume "card S = 2"
|
|
140 |
then obtain a b where "S = {a, b}"
|
|
141 |
by (metis Suc_1 card_1_singletonE card_Suc_eq)
|
|
142 |
then show ?thesis
|
|
143 |
using *[of a b] that
|
|
144 |
by (auto simp: sum_clauses(2))
|
|
145 |
next
|
|
146 |
assume "card S > 2"
|
|
147 |
then show ?thesis using that n_def
|
|
148 |
proof (induct n arbitrary: u S)
|
|
149 |
case 0
|
|
150 |
then show ?case by auto
|
|
151 |
next
|
|
152 |
case (Suc n u S)
|
|
153 |
have "sum u S = card S" if "\<not> (\<exists>x\<in>S. u x \<noteq> 1)"
|
|
154 |
using that unfolding card_eq_sum by auto
|
|
155 |
with Suc.prems obtain x where "x \<in> S" and x: "u x \<noteq> 1" by force
|
|
156 |
have c: "card (S - {x}) = card S - 1"
|
|
157 |
by (simp add: Suc.prems(3) \<open>x \<in> S\<close>)
|
|
158 |
have "sum u (S - {x}) = 1 - u x"
|
|
159 |
by (simp add: Suc.prems sum_diff1 \<open>x \<in> S\<close>)
|
|
160 |
with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1"
|
|
161 |
by auto
|
|
162 |
have inV: "(\<Sum>y\<in>S - {x}. (inverse (1 - u x) * u y) *\<^sub>R y) \<in> V"
|
|
163 |
proof (cases "card (S - {x}) > 2")
|
|
164 |
case True
|
|
165 |
then have S: "S - {x} \<noteq> {}" "card (S - {x}) = n"
|
|
166 |
using Suc.prems c by force+
|
|
167 |
show ?thesis
|
|
168 |
proof (rule Suc.hyps)
|
|
169 |
show "(\<Sum>a\<in>S - {x}. inverse (1 - u x) * u a) = 1"
|
|
170 |
by (auto simp: eq1 sum_distrib_left[symmetric])
|
|
171 |
qed (use S Suc.prems True in auto)
|
|
172 |
next
|
|
173 |
case False
|
|
174 |
then have "card (S - {x}) = Suc (Suc 0)"
|
|
175 |
using Suc.prems c by auto
|
|
176 |
then obtain a b where ab: "(S - {x}) = {a, b}" "a\<noteq>b"
|
|
177 |
unfolding card_Suc_eq by auto
|
|
178 |
then show ?thesis
|
|
179 |
using eq1 \<open>S \<subseteq> V\<close>
|
|
180 |
by (auto simp: sum_distrib_left distrib_left intro!: Suc.prems(2)[of a b])
|
|
181 |
qed
|
|
182 |
have "u x + (1 - u x) = 1 \<Longrightarrow>
|
|
183 |
u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\<Sum>y\<in>S - {x}. u y *\<^sub>R y) /\<^sub>R (1 - u x)) \<in> V"
|
|
184 |
by (rule Suc.prems) (use \<open>x \<in> S\<close> Suc.prems inV in \<open>auto simp: scaleR_right.sum\<close>)
|
|
185 |
moreover have "(\<Sum>a\<in>S. u a *\<^sub>R a) = u x *\<^sub>R x + (\<Sum>a\<in>S - {x}. u a *\<^sub>R a)"
|
|
186 |
by (meson Suc.prems(3) sum.remove \<open>x \<in> S\<close>)
|
|
187 |
ultimately show "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V"
|
|
188 |
by (simp add: x)
|
|
189 |
qed
|
|
190 |
qed (use \<open>S\<noteq>{}\<close> \<open>finite S\<close> in auto)
|
|
191 |
qed
|
|
192 |
ultimately show ?thesis
|
|
193 |
unfolding affine_def by meson
|
|
194 |
qed
|
|
195 |
|
|
196 |
|
|
197 |
lemma affine_hull_explicit:
|
|
198 |
"affine hull p = {y. \<exists>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p \<and> sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
|
|
199 |
(is "_ = ?rhs")
|
|
200 |
proof (rule hull_unique)
|
|
201 |
show "p \<subseteq> ?rhs"
|
|
202 |
proof (intro subsetI CollectI exI conjI)
|
|
203 |
show "\<And>x. sum (\<lambda>z. 1) {x} = 1"
|
|
204 |
by auto
|
|
205 |
qed auto
|
|
206 |
show "?rhs \<subseteq> T" if "p \<subseteq> T" "affine T" for T
|
|
207 |
using that unfolding affine by blast
|
|
208 |
show "affine ?rhs"
|
|
209 |
unfolding affine_def
|
|
210 |
proof clarify
|
|
211 |
fix u v :: real and sx ux sy uy
|
|
212 |
assume uv: "u + v = 1"
|
|
213 |
and x: "finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "sum ux sx = (1::real)"
|
|
214 |
and y: "finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "sum uy sy = (1::real)"
|
|
215 |
have **: "(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy"
|
|
216 |
by auto
|
|
217 |
show "\<exists>S w. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p \<and>
|
|
218 |
sum w S = 1 \<and> (\<Sum>v\<in>S. w v *\<^sub>R v) = u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)"
|
|
219 |
proof (intro exI conjI)
|
|
220 |
show "finite (sx \<union> sy)"
|
|
221 |
using x y by auto
|
|
222 |
show "sum (\<lambda>i. (if i\<in>sx then u * ux i else 0) + (if i\<in>sy then v * uy i else 0)) (sx \<union> sy) = 1"
|
|
223 |
using x y uv
|
|
224 |
by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] sum_distrib_left [symmetric] **)
|
|
225 |
have "(\<Sum>i\<in>sx \<union> sy. ((if i \<in> sx then u * ux i else 0) + (if i \<in> sy then v * uy i else 0)) *\<^sub>R i)
|
|
226 |
= (\<Sum>i\<in>sx. (u * ux i) *\<^sub>R i) + (\<Sum>i\<in>sy. (v * uy i) *\<^sub>R i)"
|
|
227 |
using x y
|
|
228 |
unfolding scaleR_left_distrib scaleR_zero_left if_smult
|
|
229 |
by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] **)
|
|
230 |
also have "\<dots> = u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)"
|
|
231 |
unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by blast
|
|
232 |
finally show "(\<Sum>i\<in>sx \<union> sy. ((if i \<in> sx then u * ux i else 0) + (if i \<in> sy then v * uy i else 0)) *\<^sub>R i)
|
|
233 |
= u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)" .
|
|
234 |
qed (use x y in auto)
|
|
235 |
qed
|
|
236 |
qed
|
|
237 |
|
|
238 |
lemma affine_hull_finite:
|
|
239 |
assumes "finite S"
|
|
240 |
shows "affine hull S = {y. \<exists>u. sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
|
|
241 |
proof -
|
|
242 |
have *: "\<exists>h. sum h S = 1 \<and> (\<Sum>v\<in>S. h v *\<^sub>R v) = x"
|
|
243 |
if "F \<subseteq> S" "finite F" "F \<noteq> {}" and sum: "sum u F = 1" and x: "(\<Sum>v\<in>F. u v *\<^sub>R v) = x" for x F u
|
|
244 |
proof -
|
|
245 |
have "S \<inter> F = F"
|
|
246 |
using that by auto
|
|
247 |
show ?thesis
|
|
248 |
proof (intro exI conjI)
|
|
249 |
show "(\<Sum>x\<in>S. if x \<in> F then u x else 0) = 1"
|
|
250 |
by (metis (mono_tags, lifting) \<open>S \<inter> F = F\<close> assms sum.inter_restrict sum)
|
|
251 |
show "(\<Sum>v\<in>S. (if v \<in> F then u v else 0) *\<^sub>R v) = x"
|
|
252 |
by (simp add: if_smult cong: if_cong) (metis (no_types) \<open>S \<inter> F = F\<close> assms sum.inter_restrict x)
|
|
253 |
qed
|
|
254 |
qed
|
|
255 |
show ?thesis
|
|
256 |
unfolding affine_hull_explicit using assms
|
|
257 |
by (fastforce dest: *)
|
|
258 |
qed
|
|
259 |
|
|
260 |
|
|
261 |
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Stepping theorems and hence small special cases\<close>
|
|
262 |
|
|
263 |
lemma affine_hull_empty[simp]: "affine hull {} = {}"
|
|
264 |
by simp
|
|
265 |
|
|
266 |
lemma affine_hull_finite_step:
|
|
267 |
fixes y :: "'a::real_vector"
|
|
268 |
shows "finite S \<Longrightarrow>
|
|
269 |
(\<exists>u. sum u (insert a S) = w \<and> sum (\<lambda>x. u x *\<^sub>R x) (insert a S) = y) \<longleftrightarrow>
|
|
270 |
(\<exists>v u. sum u S = w - v \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y - v *\<^sub>R a)" (is "_ \<Longrightarrow> ?lhs = ?rhs")
|
|
271 |
proof -
|
|
272 |
assume fin: "finite S"
|
|
273 |
show "?lhs = ?rhs"
|
|
274 |
proof
|
|
275 |
assume ?lhs
|
|
276 |
then obtain u where u: "sum u (insert a S) = w \<and> (\<Sum>x\<in>insert a S. u x *\<^sub>R x) = y"
|
|
277 |
by auto
|
|
278 |
show ?rhs
|
|
279 |
proof (cases "a \<in> S")
|
|
280 |
case True
|
|
281 |
then show ?thesis
|
|
282 |
using u by (simp add: insert_absorb) (metis diff_zero real_vector.scale_zero_left)
|
|
283 |
next
|
|
284 |
case False
|
|
285 |
show ?thesis
|
|
286 |
by (rule exI [where x="u a"]) (use u fin False in auto)
|
|
287 |
qed
|
|
288 |
next
|
|
289 |
assume ?rhs
|
|
290 |
then obtain v u where vu: "sum u S = w - v" "(\<Sum>x\<in>S. u x *\<^sub>R x) = y - v *\<^sub>R a"
|
|
291 |
by auto
|
|
292 |
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)"
|
|
293 |
by auto
|
|
294 |
show ?lhs
|
|
295 |
proof (cases "a \<in> S")
|
|
296 |
case True
|
|
297 |
show ?thesis
|
|
298 |
by (rule exI [where x="\<lambda>x. (if x=a then v else 0) + u x"])
|
|
299 |
(simp add: True scaleR_left_distrib sum.distrib sum_clauses fin vu * cong: if_cong)
|
|
300 |
next
|
|
301 |
case False
|
|
302 |
then show ?thesis
|
|
303 |
apply (rule_tac x="\<lambda>x. if x=a then v else u x" in exI)
|
|
304 |
apply (simp add: vu sum_clauses(2)[OF fin] *)
|
|
305 |
by (simp add: sum_delta_notmem(3) vu)
|
|
306 |
qed
|
|
307 |
qed
|
|
308 |
qed
|
|
309 |
|
|
310 |
lemma affine_hull_2:
|
|
311 |
fixes a b :: "'a::real_vector"
|
|
312 |
shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}"
|
|
313 |
(is "?lhs = ?rhs")
|
|
314 |
proof -
|
|
315 |
have *:
|
|
316 |
"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
|
|
317 |
"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
|
|
318 |
have "?lhs = {y. \<exists>u. sum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}"
|
|
319 |
using affine_hull_finite[of "{a,b}"] by auto
|
|
320 |
also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}"
|
|
321 |
by (simp add: affine_hull_finite_step[of "{b}" a])
|
|
322 |
also have "\<dots> = ?rhs" unfolding * by auto
|
|
323 |
finally show ?thesis by auto
|
|
324 |
qed
|
|
325 |
|
|
326 |
lemma affine_hull_3:
|
|
327 |
fixes a b c :: "'a::real_vector"
|
|
328 |
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}"
|
|
329 |
proof -
|
|
330 |
have *:
|
|
331 |
"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
|
|
332 |
"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
|
|
333 |
show ?thesis
|
|
334 |
apply (simp add: affine_hull_finite affine_hull_finite_step)
|
|
335 |
unfolding *
|
|
336 |
apply safe
|
|
337 |
apply (metis add.assoc)
|
|
338 |
apply (rule_tac x=u in exI, force)
|
|
339 |
done
|
|
340 |
qed
|
|
341 |
|
|
342 |
lemma mem_affine:
|
|
343 |
assumes "affine S" "x \<in> S" "y \<in> S" "u + v = 1"
|
|
344 |
shows "u *\<^sub>R x + v *\<^sub>R y \<in> S"
|
|
345 |
using assms affine_def[of S] by auto
|
|
346 |
|
|
347 |
lemma mem_affine_3:
|
|
348 |
assumes "affine S" "x \<in> S" "y \<in> S" "z \<in> S" "u + v + w = 1"
|
|
349 |
shows "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \<in> S"
|
|
350 |
proof -
|
|
351 |
have "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \<in> affine hull {x, y, z}"
|
|
352 |
using affine_hull_3[of x y z] assms by auto
|
|
353 |
moreover
|
|
354 |
have "affine hull {x, y, z} \<subseteq> affine hull S"
|
|
355 |
using hull_mono[of "{x, y, z}" "S"] assms by auto
|
|
356 |
moreover
|
|
357 |
have "affine hull S = S"
|
|
358 |
using assms affine_hull_eq[of S] by auto
|
|
359 |
ultimately show ?thesis by auto
|
|
360 |
qed
|
|
361 |
|
|
362 |
lemma mem_affine_3_minus:
|
|
363 |
assumes "affine S" "x \<in> S" "y \<in> S" "z \<in> S"
|
|
364 |
shows "x + v *\<^sub>R (y-z) \<in> S"
|
|
365 |
using mem_affine_3[of S x y z 1 v "-v"] assms
|
|
366 |
by (simp add: algebra_simps)
|
|
367 |
|
|
368 |
corollary%unimportant mem_affine_3_minus2:
|
|
369 |
"\<lbrakk>affine S; x \<in> S; y \<in> S; z \<in> S\<rbrakk> \<Longrightarrow> x - v *\<^sub>R (y-z) \<in> S"
|
|
370 |
by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left)
|
|
371 |
|
|
372 |
|
|
373 |
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Some relations between affine hull and subspaces\<close>
|
|
374 |
|
|
375 |
lemma affine_hull_insert_subset_span:
|
|
376 |
"affine hull (insert a S) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> S}}"
|
|
377 |
proof -
|
|
378 |
have "\<exists>v T u. x = a + v \<and> (finite T \<and> T \<subseteq> {x - a |x. x \<in> S} \<and> (\<Sum>v\<in>T. u v *\<^sub>R v) = v)"
|
|
379 |
if "finite F" "F \<noteq> {}" "F \<subseteq> insert a S" "sum u F = 1" "(\<Sum>v\<in>F. u v *\<^sub>R v) = x"
|
|
380 |
for x F u
|
|
381 |
proof -
|
|
382 |
have *: "(\<lambda>x. x - a) ` (F - {a}) \<subseteq> {x - a |x. x \<in> S}"
|
|
383 |
using that by auto
|
|
384 |
show ?thesis
|
|
385 |
proof (intro exI conjI)
|
|
386 |
show "finite ((\<lambda>x. x - a) ` (F - {a}))"
|
|
387 |
by (simp add: that(1))
|
|
388 |
show "(\<Sum>v\<in>(\<lambda>x. x - a) ` (F - {a}). u(v+a) *\<^sub>R v) = x-a"
|
|
389 |
by (simp add: sum.reindex[unfolded inj_on_def] algebra_simps
|
|
390 |
sum_subtractf scaleR_left.sum[symmetric] sum_diff1 that)
|
|
391 |
qed (use \<open>F \<subseteq> insert a S\<close> in auto)
|
|
392 |
qed
|
|
393 |
then show ?thesis
|
|
394 |
unfolding affine_hull_explicit span_explicit by blast
|
|
395 |
qed
|
|
396 |
|
|
397 |
lemma affine_hull_insert_span:
|
|
398 |
assumes "a \<notin> S"
|
|
399 |
shows "affine hull (insert a S) = {a + v | v . v \<in> span {x - a | x. x \<in> S}}"
|
|
400 |
proof -
|
|
401 |
have *: "\<exists>G u. finite G \<and> G \<noteq> {} \<and> G \<subseteq> insert a S \<and> sum u G = 1 \<and> (\<Sum>v\<in>G. u v *\<^sub>R v) = y"
|
|
402 |
if "v \<in> span {x - a |x. x \<in> S}" "y = a + v" for y v
|
|
403 |
proof -
|
|
404 |
from that
|
|
405 |
obtain T u where u: "finite T" "T \<subseteq> {x - a |x. x \<in> S}" "a + (\<Sum>v\<in>T. u v *\<^sub>R v) = y"
|
|
406 |
unfolding span_explicit by auto
|
|
407 |
define F where "F = (\<lambda>x. x + a) ` T"
|
|
408 |
have F: "finite F" "F \<subseteq> S" "(\<Sum>v\<in>F. u (v - a) *\<^sub>R (v - a)) = y - a"
|
|
409 |
unfolding F_def using u by (auto simp: sum.reindex[unfolded inj_on_def])
|
|
410 |
have *: "F \<inter> {a} = {}" "F \<inter> - {a} = F"
|
|
411 |
using F assms by auto
|
|
412 |
show "\<exists>G u. finite G \<and> G \<noteq> {} \<and> G \<subseteq> insert a S \<and> sum u G = 1 \<and> (\<Sum>v\<in>G. u v *\<^sub>R v) = y"
|
|
413 |
apply (rule_tac x = "insert a F" in exI)
|
|
414 |
apply (rule_tac x = "\<lambda>x. if x=a then 1 - sum (\<lambda>x. u (x - a)) F else u (x - a)" in exI)
|
|
415 |
using assms F
|
|
416 |
apply (auto simp: sum_clauses sum.If_cases if_smult sum_subtractf scaleR_left.sum algebra_simps *)
|
|
417 |
done
|
|
418 |
qed
|
|
419 |
show ?thesis
|
|
420 |
by (intro subset_antisym affine_hull_insert_subset_span) (auto simp: affine_hull_explicit dest!: *)
|
|
421 |
qed
|
|
422 |
|
|
423 |
lemma affine_hull_span:
|
|
424 |
assumes "a \<in> S"
|
|
425 |
shows "affine hull S = {a + v | v. v \<in> span {x - a | x. x \<in> S - {a}}}"
|
|
426 |
using affine_hull_insert_span[of a "S - {a}", unfolded insert_Diff[OF assms]] by auto
|
|
427 |
|
|
428 |
|
|
429 |
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Parallel affine sets\<close>
|
|
430 |
|
|
431 |
definition affine_parallel :: "'a::real_vector set \<Rightarrow> 'a::real_vector set \<Rightarrow> bool"
|
|
432 |
where "affine_parallel S T \<longleftrightarrow> (\<exists>a. T = (\<lambda>x. a + x) ` S)"
|
|
433 |
|
|
434 |
lemma affine_parallel_expl_aux:
|
|
435 |
fixes S T :: "'a::real_vector set"
|
|
436 |
assumes "\<And>x. x \<in> S \<longleftrightarrow> a + x \<in> T"
|
|
437 |
shows "T = (\<lambda>x. a + x) ` S"
|
|
438 |
proof -
|
|
439 |
have "x \<in> ((\<lambda>x. a + x) ` S)" if "x \<in> T" for x
|
|
440 |
using that
|
|
441 |
by (simp add: image_iff) (metis add.commute diff_add_cancel assms)
|
|
442 |
moreover have "T \<ge> (\<lambda>x. a + x) ` S"
|
|
443 |
using assms by auto
|
|
444 |
ultimately show ?thesis by auto
|
|
445 |
qed
|
|
446 |
|
|
447 |
lemma affine_parallel_expl: "affine_parallel S T \<longleftrightarrow> (\<exists>a. \<forall>x. x \<in> S \<longleftrightarrow> a + x \<in> T)"
|
|
448 |
by (auto simp add: affine_parallel_def)
|
|
449 |
(use affine_parallel_expl_aux [of S _ T] in blast)
|
|
450 |
|
|
451 |
lemma affine_parallel_reflex: "affine_parallel S S"
|
|
452 |
unfolding affine_parallel_def
|
|
453 |
using image_add_0 by blast
|
|
454 |
|
|
455 |
lemma affine_parallel_commut:
|
|
456 |
assumes "affine_parallel A B"
|
|
457 |
shows "affine_parallel B A"
|
|
458 |
proof -
|
|
459 |
from assms obtain a where B: "B = (\<lambda>x. a + x) ` A"
|
|
460 |
unfolding affine_parallel_def by auto
|
|
461 |
have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
|
|
462 |
from B show ?thesis
|
|
463 |
using translation_galois [of B a A]
|
|
464 |
unfolding affine_parallel_def by blast
|
|
465 |
qed
|
|
466 |
|
|
467 |
lemma affine_parallel_assoc:
|
|
468 |
assumes "affine_parallel A B"
|
|
469 |
and "affine_parallel B C"
|
|
470 |
shows "affine_parallel A C"
|
|
471 |
proof -
|
|
472 |
from assms obtain ab where "B = (\<lambda>x. ab + x) ` A"
|
|
473 |
unfolding affine_parallel_def by auto
|
|
474 |
moreover
|
|
475 |
from assms obtain bc where "C = (\<lambda>x. bc + x) ` B"
|
|
476 |
unfolding affine_parallel_def by auto
|
|
477 |
ultimately show ?thesis
|
|
478 |
using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto
|
|
479 |
qed
|
|
480 |
|
|
481 |
lemma affine_translation_aux:
|
|
482 |
fixes a :: "'a::real_vector"
|
|
483 |
assumes "affine ((\<lambda>x. a + x) ` S)"
|
|
484 |
shows "affine S"
|
|
485 |
proof -
|
|
486 |
{
|
|
487 |
fix x y u v
|
|
488 |
assume xy: "x \<in> S" "y \<in> S" "(u :: real) + v = 1"
|
|
489 |
then have "(a + x) \<in> ((\<lambda>x. a + x) ` S)" "(a + y) \<in> ((\<lambda>x. a + x) ` S)"
|
|
490 |
by auto
|
|
491 |
then have h1: "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) \<in> (\<lambda>x. a + x) ` S"
|
|
492 |
using xy assms unfolding affine_def by auto
|
|
493 |
have "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) = (u + v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)"
|
|
494 |
by (simp add: algebra_simps)
|
|
495 |
also have "\<dots> = a + (u *\<^sub>R x + v *\<^sub>R y)"
|
|
496 |
using \<open>u + v = 1\<close> by auto
|
|
497 |
ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) \<in> (\<lambda>x. a + x) ` S"
|
|
498 |
using h1 by auto
|
|
499 |
then have "u *\<^sub>R x + v *\<^sub>R y \<in> S" by auto
|
|
500 |
}
|
|
501 |
then show ?thesis unfolding affine_def by auto
|
|
502 |
qed
|
|
503 |
|
|
504 |
lemma affine_translation:
|
|
505 |
"affine S \<longleftrightarrow> affine ((+) a ` S)" for a :: "'a::real_vector"
|
|
506 |
proof
|
|
507 |
show "affine ((+) a ` S)" if "affine S"
|
|
508 |
using that translation_assoc [of "- a" a S]
|
|
509 |
by (auto intro: affine_translation_aux [of "- a" "((+) a ` S)"])
|
|
510 |
show "affine S" if "affine ((+) a ` S)"
|
|
511 |
using that by (rule affine_translation_aux)
|
|
512 |
qed
|
|
513 |
|
|
514 |
lemma parallel_is_affine:
|
|
515 |
fixes S T :: "'a::real_vector set"
|
|
516 |
assumes "affine S" "affine_parallel S T"
|
|
517 |
shows "affine T"
|
|
518 |
proof -
|
|
519 |
from assms obtain a where "T = (\<lambda>x. a + x) ` S"
|
|
520 |
unfolding affine_parallel_def by auto
|
|
521 |
then show ?thesis
|
|
522 |
using affine_translation assms by auto
|
|
523 |
qed
|
|
524 |
|
|
525 |
lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
|
|
526 |
unfolding subspace_def affine_def by auto
|
|
527 |
|
|
528 |
lemma affine_hull_subset_span: "(affine hull s) \<subseteq> (span s)"
|
|
529 |
by (metis hull_minimal span_superset subspace_imp_affine subspace_span)
|
|
530 |
|
|
531 |
|
|
532 |
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Subspace parallel to an affine set\<close>
|
|
533 |
|
|
534 |
lemma subspace_affine: "subspace S \<longleftrightarrow> affine S \<and> 0 \<in> S"
|
|
535 |
proof -
|
|
536 |
have h0: "subspace S \<Longrightarrow> affine S \<and> 0 \<in> S"
|
|
537 |
using subspace_imp_affine[of S] subspace_0 by auto
|
|
538 |
{
|
|
539 |
assume assm: "affine S \<and> 0 \<in> S"
|
|
540 |
{
|
|
541 |
fix c :: real
|
|
542 |
fix x
|
|
543 |
assume x: "x \<in> S"
|
|
544 |
have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto
|
|
545 |
moreover
|
|
546 |
have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \<in> S"
|
|
547 |
using affine_alt[of S] assm x by auto
|
|
548 |
ultimately have "c *\<^sub>R x \<in> S" by auto
|
|
549 |
}
|
|
550 |
then have h1: "\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S" by auto
|
|
551 |
|
|
552 |
{
|
|
553 |
fix x y
|
|
554 |
assume xy: "x \<in> S" "y \<in> S"
|
|
555 |
define u where "u = (1 :: real)/2"
|
|
556 |
have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)"
|
|
557 |
by auto
|
|
558 |
moreover
|
|
559 |
have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y"
|
|
560 |
by (simp add: algebra_simps)
|
|
561 |
moreover
|
|
562 |
have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> S"
|
|
563 |
using affine_alt[of S] assm xy by auto
|
|
564 |
ultimately
|
|
565 |
have "(1/2) *\<^sub>R (x+y) \<in> S"
|
|
566 |
using u_def by auto
|
|
567 |
moreover
|
|
568 |
have "x + y = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))"
|
|
569 |
by auto
|
|
570 |
ultimately
|
|
571 |
have "x + y \<in> S"
|
|
572 |
using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
|
|
573 |
}
|
|
574 |
then have "\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S"
|
|
575 |
by auto
|
|
576 |
then have "subspace S"
|
|
577 |
using h1 assm unfolding subspace_def by auto
|
|
578 |
}
|
|
579 |
then show ?thesis using h0 by metis
|
|
580 |
qed
|
|
581 |
|
|
582 |
lemma affine_diffs_subspace:
|
|
583 |
assumes "affine S" "a \<in> S"
|
|
584 |
shows "subspace ((\<lambda>x. (-a)+x) ` S)"
|
|
585 |
proof -
|
|
586 |
have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
|
|
587 |
have "affine ((\<lambda>x. (-a)+x) ` S)"
|
|
588 |
using affine_translation assms by blast
|
|
589 |
moreover have "0 \<in> ((\<lambda>x. (-a)+x) ` S)"
|
|
590 |
using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto
|
|
591 |
ultimately show ?thesis using subspace_affine by auto
|
|
592 |
qed
|
|
593 |
|
|
594 |
lemma affine_diffs_subspace_subtract:
|
|
595 |
"subspace ((\<lambda>x. x - a) ` S)" if "affine S" "a \<in> S"
|
|
596 |
using that affine_diffs_subspace [of _ a] by simp
|
|
597 |
|
|
598 |
lemma parallel_subspace_explicit:
|
|
599 |
assumes "affine S"
|
|
600 |
and "a \<in> S"
|
|
601 |
assumes "L \<equiv> {y. \<exists>x \<in> S. (-a) + x = y}"
|
|
602 |
shows "subspace L \<and> affine_parallel S L"
|
|
603 |
proof -
|
|
604 |
from assms have "L = plus (- a) ` S" by auto
|
|
605 |
then have par: "affine_parallel S L"
|
|
606 |
unfolding affine_parallel_def ..
|
|
607 |
then have "affine L" using assms parallel_is_affine by auto
|
|
608 |
moreover have "0 \<in> L"
|
|
609 |
using assms by auto
|
|
610 |
ultimately show ?thesis
|
|
611 |
using subspace_affine par by auto
|
|
612 |
qed
|
|
613 |
|
|
614 |
lemma parallel_subspace_aux:
|
|
615 |
assumes "subspace A"
|
|
616 |
and "subspace B"
|
|
617 |
and "affine_parallel A B"
|
|
618 |
shows "A \<supseteq> B"
|
|
619 |
proof -
|
|
620 |
from assms obtain a where a: "\<forall>x. x \<in> A \<longleftrightarrow> a + x \<in> B"
|
|
621 |
using affine_parallel_expl[of A B] by auto
|
|
622 |
then have "-a \<in> A"
|
|
623 |
using assms subspace_0[of B] by auto
|
|
624 |
then have "a \<in> A"
|
|
625 |
using assms subspace_neg[of A "-a"] by auto
|
|
626 |
then show ?thesis
|
|
627 |
using assms a unfolding subspace_def by auto
|
|
628 |
qed
|
|
629 |
|
|
630 |
lemma parallel_subspace:
|
|
631 |
assumes "subspace A"
|
|
632 |
and "subspace B"
|
|
633 |
and "affine_parallel A B"
|
|
634 |
shows "A = B"
|
|
635 |
proof
|
|
636 |
show "A \<supseteq> B"
|
|
637 |
using assms parallel_subspace_aux by auto
|
|
638 |
show "A \<subseteq> B"
|
|
639 |
using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto
|
|
640 |
qed
|
|
641 |
|
|
642 |
lemma affine_parallel_subspace:
|
|
643 |
assumes "affine S" "S \<noteq> {}"
|
|
644 |
shows "\<exists>!L. subspace L \<and> affine_parallel S L"
|
|
645 |
proof -
|
|
646 |
have ex: "\<exists>L. subspace L \<and> affine_parallel S L"
|
|
647 |
using assms parallel_subspace_explicit by auto
|
|
648 |
{
|
|
649 |
fix L1 L2
|
|
650 |
assume ass: "subspace L1 \<and> affine_parallel S L1" "subspace L2 \<and> affine_parallel S L2"
|
|
651 |
then have "affine_parallel L1 L2"
|
|
652 |
using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto
|
|
653 |
then have "L1 = L2"
|
|
654 |
using ass parallel_subspace by auto
|
|
655 |
}
|
|
656 |
then show ?thesis using ex by auto
|
|
657 |
qed
|
|
658 |
|
|
659 |
|
|
660 |
subsection \<open>Affine Dependence\<close>
|
|
661 |
|
|
662 |
text "Formalized by Lars Schewe."
|
|
663 |
|
|
664 |
definition\<^marker>\<open>tag important\<close> affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
|
|
665 |
where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
|
|
666 |
|
|
667 |
lemma affine_dependent_imp_dependent: "affine_dependent s \<Longrightarrow> dependent s"
|
|
668 |
unfolding affine_dependent_def dependent_def
|
|
669 |
using affine_hull_subset_span by auto
|
|
670 |
|
|
671 |
lemma affine_dependent_subset:
|
|
672 |
"\<lbrakk>affine_dependent s; s \<subseteq> t\<rbrakk> \<Longrightarrow> affine_dependent t"
|
|
673 |
apply (simp add: affine_dependent_def Bex_def)
|
|
674 |
apply (blast dest: hull_mono [OF Diff_mono [OF _ subset_refl]])
|
|
675 |
done
|
|
676 |
|
|
677 |
lemma affine_independent_subset:
|
|
678 |
shows "\<lbrakk>\<not> affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> \<not> affine_dependent s"
|
|
679 |
by (metis affine_dependent_subset)
|
|
680 |
|
|
681 |
lemma affine_independent_Diff:
|
|
682 |
"\<not> affine_dependent s \<Longrightarrow> \<not> affine_dependent(s - t)"
|
|
683 |
by (meson Diff_subset affine_dependent_subset)
|
|
684 |
|
|
685 |
proposition affine_dependent_explicit:
|
|
686 |
"affine_dependent p \<longleftrightarrow>
|
|
687 |
(\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
|
|
688 |
proof -
|
|
689 |
have "\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> (\<Sum>w\<in>S. u w *\<^sub>R w) = 0"
|
|
690 |
if "(\<Sum>w\<in>S. u w *\<^sub>R w) = x" "x \<in> p" "finite S" "S \<noteq> {}" "S \<subseteq> p - {x}" "sum u S = 1" for x S u
|
|
691 |
proof (intro exI conjI)
|
|
692 |
have "x \<notin> S"
|
|
693 |
using that by auto
|
|
694 |
then show "(\<Sum>v \<in> insert x S. if v = x then - 1 else u v) = 0"
|
|
695 |
using that by (simp add: sum_delta_notmem)
|
|
696 |
show "(\<Sum>w \<in> insert x S. (if w = x then - 1 else u w) *\<^sub>R w) = 0"
|
|
697 |
using that \<open>x \<notin> S\<close> by (simp add: if_smult sum_delta_notmem cong: if_cong)
|
|
698 |
qed (use that in auto)
|
|
699 |
moreover have "\<exists>x\<in>p. \<exists>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p - {x} \<and> sum u S = 1 \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = x"
|
|
700 |
if "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0" "finite S" "S \<subseteq> p" "sum u S = 0" "v \<in> S" "u v \<noteq> 0" for S u v
|
|
701 |
proof (intro bexI exI conjI)
|
|
702 |
have "S \<noteq> {v}"
|
|
703 |
using that by auto
|
|
704 |
then show "S - {v} \<noteq> {}"
|
|
705 |
using that by auto
|
|
706 |
show "(\<Sum>x \<in> S - {v}. - (1 / u v) * u x) = 1"
|
|
707 |
unfolding sum_distrib_left[symmetric] sum_diff1[OF \<open>finite S\<close>] by (simp add: that)
|
|
708 |
show "(\<Sum>x\<in>S - {v}. (- (1 / u v) * u x) *\<^sub>R x) = v"
|
|
709 |
unfolding sum_distrib_left [symmetric] scaleR_scaleR[symmetric]
|
|
710 |
scaleR_right.sum [symmetric] sum_diff1[OF \<open>finite S\<close>]
|
|
711 |
using that by auto
|
|
712 |
show "S - {v} \<subseteq> p - {v}"
|
|
713 |
using that by auto
|
|
714 |
qed (use that in auto)
|
|
715 |
ultimately show ?thesis
|
|
716 |
unfolding affine_dependent_def affine_hull_explicit by auto
|
|
717 |
qed
|
|
718 |
|
|
719 |
lemma affine_dependent_explicit_finite:
|
|
720 |
fixes S :: "'a::real_vector set"
|
|
721 |
assumes "finite S"
|
|
722 |
shows "affine_dependent S \<longleftrightarrow>
|
|
723 |
(\<exists>u. sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
|
|
724 |
(is "?lhs = ?rhs")
|
|
725 |
proof
|
|
726 |
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)"
|
|
727 |
by auto
|
|
728 |
assume ?lhs
|
|
729 |
then obtain t u v where
|
|
730 |
"finite t" "t \<subseteq> S" "sum u t = 0" "v\<in>t" "u v \<noteq> 0" "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0"
|
|
731 |
unfolding affine_dependent_explicit by auto
|
|
732 |
then show ?rhs
|
|
733 |
apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
|
|
734 |
apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \<open>t\<subseteq>S\<close>])
|
|
735 |
done
|
|
736 |
next
|
|
737 |
assume ?rhs
|
|
738 |
then obtain u v where "sum u S = 0" "v\<in>S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0"
|
|
739 |
by auto
|
|
740 |
then show ?lhs unfolding affine_dependent_explicit
|
|
741 |
using assms by auto
|
|
742 |
qed
|
|
743 |
|
|
744 |
lemma dependent_imp_affine_dependent:
|
|
745 |
assumes "dependent {x - a| x . x \<in> s}"
|
|
746 |
and "a \<notin> s"
|
|
747 |
shows "affine_dependent (insert a s)"
|
|
748 |
proof -
|
|
749 |
from assms(1)[unfolded dependent_explicit] obtain S u v
|
|
750 |
where obt: "finite S" "S \<subseteq> {x - a |x. x \<in> s}" "v\<in>S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0"
|
|
751 |
by auto
|
|
752 |
define t where "t = (\<lambda>x. x + a) ` S"
|
|
753 |
|
|
754 |
have inj: "inj_on (\<lambda>x. x + a) S"
|
|
755 |
unfolding inj_on_def by auto
|
|
756 |
have "0 \<notin> S"
|
|
757 |
using obt(2) assms(2) unfolding subset_eq by auto
|
|
758 |
have fin: "finite t" and "t \<subseteq> s"
|
|
759 |
unfolding t_def using obt(1,2) by auto
|
|
760 |
then have "finite (insert a t)" and "insert a t \<subseteq> insert a s"
|
|
761 |
by auto
|
|
762 |
moreover have *: "\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x)) = (\<Sum>x\<in>t. Q x)"
|
|
763 |
apply (rule sum.cong)
|
|
764 |
using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close>
|
|
765 |
apply auto
|
|
766 |
done
|
|
767 |
have "(\<Sum>x\<in>insert a t. if x = a then - (\<Sum>x\<in>t. u (x - a)) else u (x - a)) = 0"
|
|
768 |
unfolding sum_clauses(2)[OF fin] * using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close> by auto
|
|
769 |
moreover have "\<exists>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) \<noteq> 0"
|
|
770 |
using obt(3,4) \<open>0\<notin>S\<close>
|
|
771 |
by (rule_tac x="v + a" in bexI) (auto simp: t_def)
|
|
772 |
moreover have *: "\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x) *\<^sub>R x) = (\<Sum>x\<in>t. Q x *\<^sub>R x)"
|
|
773 |
using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close> by (auto intro!: sum.cong)
|
|
774 |
have "(\<Sum>x\<in>t. u (x - a)) *\<^sub>R a = (\<Sum>v\<in>t. u (v - a) *\<^sub>R v)"
|
|
775 |
unfolding scaleR_left.sum
|
|
776 |
unfolding t_def and sum.reindex[OF inj] and o_def
|
|
777 |
using obt(5)
|
|
778 |
by (auto simp: sum.distrib scaleR_right_distrib)
|
|
779 |
then have "(\<Sum>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0"
|
|
780 |
unfolding sum_clauses(2)[OF fin]
|
|
781 |
using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close>
|
|
782 |
by (auto simp: *)
|
|
783 |
ultimately show ?thesis
|
|
784 |
unfolding affine_dependent_explicit
|
|
785 |
apply (rule_tac x="insert a t" in exI, auto)
|
|
786 |
done
|
|
787 |
qed
|
|
788 |
|
|
789 |
lemma affine_dependent_biggerset:
|
|
790 |
fixes s :: "'a::euclidean_space set"
|
|
791 |
assumes "finite s" "card s \<ge> DIM('a) + 2"
|
|
792 |
shows "affine_dependent s"
|
|
793 |
proof -
|
|
794 |
have "s \<noteq> {}" using assms by auto
|
|
795 |
then obtain a where "a\<in>s" by auto
|
|
796 |
have *: "{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})"
|
|
797 |
by auto
|
|
798 |
have "card {x - a |x. x \<in> s - {a}} = card (s - {a})"
|
|
799 |
unfolding * by (simp add: card_image inj_on_def)
|
|
800 |
also have "\<dots> > DIM('a)" using assms(2)
|
|
801 |
unfolding card_Diff_singleton[OF assms(1) \<open>a\<in>s\<close>] by auto
|
|
802 |
finally show ?thesis
|
|
803 |
apply (subst insert_Diff[OF \<open>a\<in>s\<close>, symmetric])
|
|
804 |
apply (rule dependent_imp_affine_dependent)
|
|
805 |
apply (rule dependent_biggerset, auto)
|
|
806 |
done
|
|
807 |
qed
|
|
808 |
|
|
809 |
lemma affine_dependent_biggerset_general:
|
|
810 |
assumes "finite (S :: 'a::euclidean_space set)"
|
|
811 |
and "card S \<ge> dim S + 2"
|
|
812 |
shows "affine_dependent S"
|
|
813 |
proof -
|
|
814 |
from assms(2) have "S \<noteq> {}" by auto
|
|
815 |
then obtain a where "a\<in>S" by auto
|
|
816 |
have *: "{x - a |x. x \<in> S - {a}} = (\<lambda>x. x - a) ` (S - {a})"
|
|
817 |
by auto
|
|
818 |
have **: "card {x - a |x. x \<in> S - {a}} = card (S - {a})"
|
|
819 |
by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def)
|
|
820 |
have "dim {x - a |x. x \<in> S - {a}} \<le> dim S"
|
|
821 |
using \<open>a\<in>S\<close> by (auto simp: span_base span_diff intro: subset_le_dim)
|
|
822 |
also have "\<dots> < dim S + 1" by auto
|
|
823 |
also have "\<dots> \<le> card (S - {a})"
|
|
824 |
using assms
|
|
825 |
using card_Diff_singleton[OF assms(1) \<open>a\<in>S\<close>]
|
|
826 |
by auto
|
|
827 |
finally show ?thesis
|
|
828 |
apply (subst insert_Diff[OF \<open>a\<in>S\<close>, symmetric])
|
|
829 |
apply (rule dependent_imp_affine_dependent)
|
|
830 |
apply (rule dependent_biggerset_general)
|
|
831 |
unfolding **
|
|
832 |
apply auto
|
|
833 |
done
|
|
834 |
qed
|
|
835 |
|
|
836 |
|
|
837 |
subsection\<^marker>\<open>tag unimportant\<close> \<open>Some Properties of Affine Dependent Sets\<close>
|
|
838 |
|
|
839 |
lemma affine_independent_0 [simp]: "\<not> affine_dependent {}"
|
|
840 |
by (simp add: affine_dependent_def)
|
|
841 |
|
|
842 |
lemma affine_independent_1 [simp]: "\<not> affine_dependent {a}"
|
|
843 |
by (simp add: affine_dependent_def)
|
|
844 |
|
|
845 |
lemma affine_independent_2 [simp]: "\<not> affine_dependent {a,b}"
|
|
846 |
by (simp add: affine_dependent_def insert_Diff_if hull_same)
|
|
847 |
|
|
848 |
lemma affine_hull_translation: "affine hull ((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (affine hull S)"
|
|
849 |
proof -
|
|
850 |
have "affine ((\<lambda>x. a + x) ` (affine hull S))"
|
|
851 |
using affine_translation affine_affine_hull by blast
|
|
852 |
moreover have "(\<lambda>x. a + x) ` S \<subseteq> (\<lambda>x. a + x) ` (affine hull S)"
|
|
853 |
using hull_subset[of S] by auto
|
|
854 |
ultimately have h1: "affine hull ((\<lambda>x. a + x) ` S) \<subseteq> (\<lambda>x. a + x) ` (affine hull S)"
|
|
855 |
by (metis hull_minimal)
|
|
856 |
have "affine((\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) ` S)))"
|
|
857 |
using affine_translation affine_affine_hull by blast
|
|
858 |
moreover have "(\<lambda>x. -a + x) ` (\<lambda>x. a + x) ` S \<subseteq> (\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) ` S))"
|
|
859 |
using hull_subset[of "(\<lambda>x. a + x) ` S"] by auto
|
|
860 |
moreover have "S = (\<lambda>x. -a + x) ` (\<lambda>x. a + x) ` S"
|
|
861 |
using translation_assoc[of "-a" a] by auto
|
|
862 |
ultimately have "(\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) ` S)) >= (affine hull S)"
|
|
863 |
by (metis hull_minimal)
|
|
864 |
then have "affine hull ((\<lambda>x. a + x) ` S) >= (\<lambda>x. a + x) ` (affine hull S)"
|
|
865 |
by auto
|
|
866 |
then show ?thesis using h1 by auto
|
|
867 |
qed
|
|
868 |
|
|
869 |
lemma affine_dependent_translation:
|
|
870 |
assumes "affine_dependent S"
|
|
871 |
shows "affine_dependent ((\<lambda>x. a + x) ` S)"
|
|
872 |
proof -
|
|
873 |
obtain x where x: "x \<in> S \<and> x \<in> affine hull (S - {x})"
|
|
874 |
using assms affine_dependent_def by auto
|
|
875 |
have "(+) a ` (S - {x}) = (+) a ` S - {a + x}"
|
|
876 |
by auto
|
|
877 |
then have "a + x \<in> affine hull ((\<lambda>x. a + x) ` S - {a + x})"
|
|
878 |
using affine_hull_translation[of a "S - {x}"] x by auto
|
|
879 |
moreover have "a + x \<in> (\<lambda>x. a + x) ` S"
|
|
880 |
using x by auto
|
|
881 |
ultimately show ?thesis
|
|
882 |
unfolding affine_dependent_def by auto
|
|
883 |
qed
|
|
884 |
|
|
885 |
lemma affine_dependent_translation_eq:
|
|
886 |
"affine_dependent S \<longleftrightarrow> affine_dependent ((\<lambda>x. a + x) ` S)"
|
|
887 |
proof -
|
|
888 |
{
|
|
889 |
assume "affine_dependent ((\<lambda>x. a + x) ` S)"
|
|
890 |
then have "affine_dependent S"
|
|
891 |
using affine_dependent_translation[of "((\<lambda>x. a + x) ` S)" "-a"] translation_assoc[of "-a" a]
|
|
892 |
by auto
|
|
893 |
}
|
|
894 |
then show ?thesis
|
|
895 |
using affine_dependent_translation by auto
|
|
896 |
qed
|
|
897 |
|
|
898 |
lemma affine_hull_0_dependent:
|
|
899 |
assumes "0 \<in> affine hull S"
|
|
900 |
shows "dependent S"
|
|
901 |
proof -
|
|
902 |
obtain s u where s_u: "finite s \<and> s \<noteq> {} \<and> s \<subseteq> S \<and> sum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
|
|
903 |
using assms affine_hull_explicit[of S] by auto
|
|
904 |
then have "\<exists>v\<in>s. u v \<noteq> 0" by auto
|
|
905 |
then have "finite s \<and> s \<subseteq> S \<and> (\<exists>v\<in>s. u v \<noteq> 0 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0)"
|
|
906 |
using s_u by auto
|
|
907 |
then show ?thesis
|
|
908 |
unfolding dependent_explicit[of S] by auto
|
|
909 |
qed
|
|
910 |
|
|
911 |
lemma affine_dependent_imp_dependent2:
|
|
912 |
assumes "affine_dependent (insert 0 S)"
|
|
913 |
shows "dependent S"
|
|
914 |
proof -
|
|
915 |
obtain x where x: "x \<in> insert 0 S \<and> x \<in> affine hull (insert 0 S - {x})"
|
|
916 |
using affine_dependent_def[of "(insert 0 S)"] assms by blast
|
|
917 |
then have "x \<in> span (insert 0 S - {x})"
|
|
918 |
using affine_hull_subset_span by auto
|
|
919 |
moreover have "span (insert 0 S - {x}) = span (S - {x})"
|
|
920 |
using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto
|
|
921 |
ultimately have "x \<in> span (S - {x})" by auto
|
|
922 |
then have "x \<noteq> 0 \<Longrightarrow> dependent S"
|
|
923 |
using x dependent_def by auto
|
|
924 |
moreover
|
|
925 |
{
|
|
926 |
assume "x = 0"
|
|
927 |
then have "0 \<in> affine hull S"
|
|
928 |
using x hull_mono[of "S - {0}" S] by auto
|
|
929 |
then have "dependent S"
|
|
930 |
using affine_hull_0_dependent by auto
|
|
931 |
}
|
|
932 |
ultimately show ?thesis by auto
|
|
933 |
qed
|
|
934 |
|
|
935 |
lemma affine_dependent_iff_dependent:
|
|
936 |
assumes "a \<notin> S"
|
|
937 |
shows "affine_dependent (insert a S) \<longleftrightarrow> dependent ((\<lambda>x. -a + x) ` S)"
|
|
938 |
proof -
|
|
939 |
have "((+) (- a) ` S) = {x - a| x . x \<in> S}" by auto
|
|
940 |
then show ?thesis
|
|
941 |
using affine_dependent_translation_eq[of "(insert a S)" "-a"]
|
|
942 |
affine_dependent_imp_dependent2 assms
|
|
943 |
dependent_imp_affine_dependent[of a S]
|
|
944 |
by (auto simp del: uminus_add_conv_diff)
|
|
945 |
qed
|
|
946 |
|
|
947 |
lemma affine_dependent_iff_dependent2:
|
|
948 |
assumes "a \<in> S"
|
|
949 |
shows "affine_dependent S \<longleftrightarrow> dependent ((\<lambda>x. -a + x) ` (S-{a}))"
|
|
950 |
proof -
|
|
951 |
have "insert a (S - {a}) = S"
|
|
952 |
using assms by auto
|
|
953 |
then show ?thesis
|
|
954 |
using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto
|
|
955 |
qed
|
|
956 |
|
|
957 |
lemma affine_hull_insert_span_gen:
|
|
958 |
"affine hull (insert a s) = (\<lambda>x. a + x) ` span ((\<lambda>x. - a + x) ` s)"
|
|
959 |
proof -
|
|
960 |
have h1: "{x - a |x. x \<in> s} = ((\<lambda>x. -a+x) ` s)"
|
|
961 |
by auto
|
|
962 |
{
|
|
963 |
assume "a \<notin> s"
|
|
964 |
then have ?thesis
|
|
965 |
using affine_hull_insert_span[of a s] h1 by auto
|
|
966 |
}
|
|
967 |
moreover
|
|
968 |
{
|
|
969 |
assume a1: "a \<in> s"
|
|
970 |
have "\<exists>x. x \<in> s \<and> -a+x=0"
|
|
971 |
apply (rule exI[of _ a])
|
|
972 |
using a1
|
|
973 |
apply auto
|
|
974 |
done
|
|
975 |
then have "insert 0 ((\<lambda>x. -a+x) ` (s - {a})) = (\<lambda>x. -a+x) ` s"
|
|
976 |
by auto
|
|
977 |
then have "span ((\<lambda>x. -a+x) ` (s - {a}))=span ((\<lambda>x. -a+x) ` s)"
|
|
978 |
using span_insert_0[of "(+) (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff)
|
|
979 |
moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
|
|
980 |
by auto
|
|
981 |
moreover have "insert a (s - {a}) = insert a s"
|
|
982 |
by auto
|
|
983 |
ultimately have ?thesis
|
|
984 |
using affine_hull_insert_span[of "a" "s-{a}"] by auto
|
|
985 |
}
|
|
986 |
ultimately show ?thesis by auto
|
|
987 |
qed
|
|
988 |
|
|
989 |
lemma affine_hull_span2:
|
|
990 |
assumes "a \<in> s"
|
|
991 |
shows "affine hull s = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` (s-{a}))"
|
|
992 |
using affine_hull_insert_span_gen[of a "s - {a}", unfolded insert_Diff[OF assms]]
|
|
993 |
by auto
|
|
994 |
|
|
995 |
lemma affine_hull_span_gen:
|
|
996 |
assumes "a \<in> affine hull s"
|
|
997 |
shows "affine hull s = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` s)"
|
|
998 |
proof -
|
|
999 |
have "affine hull (insert a s) = affine hull s"
|
|
1000 |
using hull_redundant[of a affine s] assms by auto
|
|
1001 |
then show ?thesis
|
|
1002 |
using affine_hull_insert_span_gen[of a "s"] by auto
|
|
1003 |
qed
|
|
1004 |
|
|
1005 |
lemma affine_hull_span_0:
|
|
1006 |
assumes "0 \<in> affine hull S"
|
|
1007 |
shows "affine hull S = span S"
|
|
1008 |
using affine_hull_span_gen[of "0" S] assms by auto
|
|
1009 |
|
|
1010 |
lemma extend_to_affine_basis_nonempty:
|
|
1011 |
fixes S V :: "'n::euclidean_space set"
|
|
1012 |
assumes "\<not> affine_dependent S" "S \<subseteq> V" "S \<noteq> {}"
|
|
1013 |
shows "\<exists>T. \<not> affine_dependent T \<and> S \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
|
|
1014 |
proof -
|
|
1015 |
obtain a where a: "a \<in> S"
|
|
1016 |
using assms by auto
|
|
1017 |
then have h0: "independent ((\<lambda>x. -a + x) ` (S-{a}))"
|
|
1018 |
using affine_dependent_iff_dependent2 assms by auto
|
|
1019 |
obtain B where B:
|
|
1020 |
"(\<lambda>x. -a+x) ` (S - {a}) \<subseteq> B \<and> B \<subseteq> (\<lambda>x. -a+x) ` V \<and> independent B \<and> (\<lambda>x. -a+x) ` V \<subseteq> span B"
|
|
1021 |
using assms
|
|
1022 |
by (blast intro: maximal_independent_subset_extend[OF _ h0, of "(\<lambda>x. -a + x) ` V"])
|
|
1023 |
define T where "T = (\<lambda>x. a+x) ` insert 0 B"
|
|
1024 |
then have "T = insert a ((\<lambda>x. a+x) ` B)"
|
|
1025 |
by auto
|
|
1026 |
then have "affine hull T = (\<lambda>x. a+x) ` span B"
|
|
1027 |
using affine_hull_insert_span_gen[of a "((\<lambda>x. a+x) ` B)"] translation_assoc[of "-a" a B]
|
|
1028 |
by auto
|
|
1029 |
then have "V \<subseteq> affine hull T"
|
|
1030 |
using B assms translation_inverse_subset[of a V "span B"]
|
|
1031 |
by auto
|
|
1032 |
moreover have "T \<subseteq> V"
|
|
1033 |
using T_def B a assms by auto
|
|
1034 |
ultimately have "affine hull T = affine hull V"
|
|
1035 |
by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono)
|
|
1036 |
moreover have "S \<subseteq> T"
|
|
1037 |
using T_def B translation_inverse_subset[of a "S-{a}" B]
|
|
1038 |
by auto
|
|
1039 |
moreover have "\<not> affine_dependent T"
|
|
1040 |
using T_def affine_dependent_translation_eq[of "insert 0 B"]
|
|
1041 |
affine_dependent_imp_dependent2 B
|
|
1042 |
by auto
|
|
1043 |
ultimately show ?thesis using \<open>T \<subseteq> V\<close> by auto
|
|
1044 |
qed
|
|
1045 |
|
|
1046 |
lemma affine_basis_exists:
|
|
1047 |
fixes V :: "'n::euclidean_space set"
|
|
1048 |
shows "\<exists>B. B \<subseteq> V \<and> \<not> affine_dependent B \<and> affine hull V = affine hull B"
|
|
1049 |
proof (cases "V = {}")
|
|
1050 |
case True
|
|
1051 |
then show ?thesis
|
|
1052 |
using affine_independent_0 by auto
|
|
1053 |
next
|
|
1054 |
case False
|
|
1055 |
then obtain x where "x \<in> V" by auto
|
|
1056 |
then show ?thesis
|
|
1057 |
using affine_dependent_def[of "{x}"] extend_to_affine_basis_nonempty[of "{x}" V]
|
|
1058 |
by auto
|
|
1059 |
qed
|
|
1060 |
|
|
1061 |
proposition extend_to_affine_basis:
|
|
1062 |
fixes S V :: "'n::euclidean_space set"
|
|
1063 |
assumes "\<not> affine_dependent S" "S \<subseteq> V"
|
|
1064 |
obtains T where "\<not> affine_dependent T" "S \<subseteq> T" "T \<subseteq> V" "affine hull T = affine hull V"
|
|
1065 |
proof (cases "S = {}")
|
|
1066 |
case True then show ?thesis
|
|
1067 |
using affine_basis_exists by (metis empty_subsetI that)
|
|
1068 |
next
|
|
1069 |
case False
|
|
1070 |
then show ?thesis by (metis assms extend_to_affine_basis_nonempty that)
|
|
1071 |
qed
|
|
1072 |
|
|
1073 |
|
|
1074 |
subsection \<open>Affine Dimension of a Set\<close>
|
|
1075 |
|
|
1076 |
definition\<^marker>\<open>tag important\<close> aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
|
|
1077 |
where "aff_dim V =
|
|
1078 |
(SOME d :: int.
|
|
1079 |
\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"
|
|
1080 |
|
|
1081 |
lemma aff_dim_basis_exists:
|
|
1082 |
fixes V :: "('n::euclidean_space) set"
|
|
1083 |
shows "\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1"
|
|
1084 |
proof -
|
|
1085 |
obtain B where "\<not> affine_dependent B \<and> affine hull B = affine hull V"
|
|
1086 |
using affine_basis_exists[of V] by auto
|
|
1087 |
then show ?thesis
|
|
1088 |
unfolding aff_dim_def
|
|
1089 |
some_eq_ex[of "\<lambda>d. \<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1"]
|
|
1090 |
apply auto
|
|
1091 |
apply (rule exI[of _ "int (card B) - (1 :: int)"])
|
|
1092 |
apply (rule exI[of _ "B"], auto)
|
|
1093 |
done
|
|
1094 |
qed
|
|
1095 |
|
|
1096 |
lemma affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
|
|
1097 |
by (metis affine_empty subset_empty subset_hull)
|
|
1098 |
|
|
1099 |
lemma empty_eq_affine_hull[simp]: "{} = affine hull S \<longleftrightarrow> S = {}"
|
|
1100 |
by (metis affine_hull_eq_empty)
|
|
1101 |
|
|
1102 |
lemma aff_dim_parallel_subspace_aux:
|
|
1103 |
fixes B :: "'n::euclidean_space set"
|
|
1104 |
assumes "\<not> affine_dependent B" "a \<in> B"
|
|
1105 |
shows "finite B \<and> ((card B) - 1 = dim (span ((\<lambda>x. -a+x) ` (B-{a}))))"
|
|
1106 |
proof -
|
|
1107 |
have "independent ((\<lambda>x. -a + x) ` (B-{a}))"
|
|
1108 |
using affine_dependent_iff_dependent2 assms by auto
|
|
1109 |
then have fin: "dim (span ((\<lambda>x. -a+x) ` (B-{a}))) = card ((\<lambda>x. -a + x) ` (B-{a}))"
|
|
1110 |
"finite ((\<lambda>x. -a + x) ` (B - {a}))"
|
|
1111 |
using indep_card_eq_dim_span[of "(\<lambda>x. -a+x) ` (B-{a})"] by auto
|
|
1112 |
show ?thesis
|
|
1113 |
proof (cases "(\<lambda>x. -a + x) ` (B - {a}) = {}")
|
|
1114 |
case True
|
|
1115 |
have "B = insert a ((\<lambda>x. a + x) ` (\<lambda>x. -a + x) ` (B - {a}))"
|
|
1116 |
using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto
|
|
1117 |
then have "B = {a}" using True by auto
|
|
1118 |
then show ?thesis using assms fin by auto
|
|
1119 |
next
|
|
1120 |
case False
|
|
1121 |
then have "card ((\<lambda>x. -a + x) ` (B - {a})) > 0"
|
|
1122 |
using fin by auto
|
|
1123 |
moreover have h1: "card ((\<lambda>x. -a + x) ` (B-{a})) = card (B-{a})"
|
|
1124 |
by (rule card_image) (use translate_inj_on in blast)
|
|
1125 |
ultimately have "card (B-{a}) > 0" by auto
|
|
1126 |
then have *: "finite (B - {a})"
|
|
1127 |
using card_gt_0_iff[of "(B - {a})"] by auto
|
|
1128 |
then have "card (B - {a}) = card B - 1"
|
|
1129 |
using card_Diff_singleton assms by auto
|
|
1130 |
with * show ?thesis using fin h1 by auto
|
|
1131 |
qed
|
|
1132 |
qed
|
|
1133 |
|
|
1134 |
lemma aff_dim_parallel_subspace:
|
|
1135 |
fixes V L :: "'n::euclidean_space set"
|
|
1136 |
assumes "V \<noteq> {}"
|
|
1137 |
and "subspace L"
|
|
1138 |
and "affine_parallel (affine hull V) L"
|
|
1139 |
shows "aff_dim V = int (dim L)"
|
|
1140 |
proof -
|
|
1141 |
obtain B where
|
|
1142 |
B: "affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> int (card B) = aff_dim V + 1"
|
|
1143 |
using aff_dim_basis_exists by auto
|
|
1144 |
then have "B \<noteq> {}"
|
|
1145 |
using assms B
|
|
1146 |
by auto
|
|
1147 |
then obtain a where a: "a \<in> B" by auto
|
|
1148 |
define Lb where "Lb = span ((\<lambda>x. -a+x) ` (B-{a}))"
|
|
1149 |
moreover have "affine_parallel (affine hull B) Lb"
|
|
1150 |
using Lb_def B assms affine_hull_span2[of a B] a
|
|
1151 |
affine_parallel_commut[of "Lb" "(affine hull B)"]
|
|
1152 |
unfolding affine_parallel_def
|
|
1153 |
by auto
|
|
1154 |
moreover have "subspace Lb"
|
|
1155 |
using Lb_def subspace_span by auto
|
|
1156 |
moreover have "affine hull B \<noteq> {}"
|
|
1157 |
using assms B by auto
|
|
1158 |
ultimately have "L = Lb"
|
|
1159 |
using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B
|
|
1160 |
by auto
|
|
1161 |
then have "dim L = dim Lb"
|
|
1162 |
by auto
|
|
1163 |
moreover have "card B - 1 = dim Lb" and "finite B"
|
|
1164 |
using Lb_def aff_dim_parallel_subspace_aux a B by auto
|
|
1165 |
ultimately show ?thesis
|
|
1166 |
using B \<open>B \<noteq> {}\<close> card_gt_0_iff[of B] by auto
|
|
1167 |
qed
|
|
1168 |
|
|
1169 |
lemma aff_independent_finite:
|
|
1170 |
fixes B :: "'n::euclidean_space set"
|
|
1171 |
assumes "\<not> affine_dependent B"
|
|
1172 |
shows "finite B"
|
|
1173 |
proof -
|
|
1174 |
{
|
|
1175 |
assume "B \<noteq> {}"
|
|
1176 |
then obtain a where "a \<in> B" by auto
|
|
1177 |
then have ?thesis
|
|
1178 |
using aff_dim_parallel_subspace_aux assms by auto
|
|
1179 |
}
|
|
1180 |
then show ?thesis by auto
|
|
1181 |
qed
|
|
1182 |
|
|
1183 |
|
|
1184 |
lemma aff_dim_empty:
|
|
1185 |
fixes S :: "'n::euclidean_space set"
|
|
1186 |
shows "S = {} \<longleftrightarrow> aff_dim S = -1"
|
|
1187 |
proof -
|
|
1188 |
obtain B where *: "affine hull B = affine hull S"
|
|
1189 |
and "\<not> affine_dependent B"
|
|
1190 |
and "int (card B) = aff_dim S + 1"
|
|
1191 |
using aff_dim_basis_exists by auto
|
|
1192 |
moreover
|
|
1193 |
from * have "S = {} \<longleftrightarrow> B = {}"
|
|
1194 |
by auto
|
|
1195 |
ultimately show ?thesis
|
|
1196 |
using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
|
|
1197 |
qed
|
|
1198 |
|
|
1199 |
lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"
|
|
1200 |
by (simp add: aff_dim_empty [symmetric])
|
|
1201 |
|
|
1202 |
lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S"
|
|
1203 |
unfolding aff_dim_def using hull_hull[of _ S] by auto
|
|
1204 |
|
|
1205 |
lemma aff_dim_affine_hull2:
|
|
1206 |
assumes "affine hull S = affine hull T"
|
|
1207 |
shows "aff_dim S = aff_dim T"
|
|
1208 |
unfolding aff_dim_def using assms by auto
|
|
1209 |
|
|
1210 |
lemma aff_dim_unique:
|
|
1211 |
fixes B V :: "'n::euclidean_space set"
|
|
1212 |
assumes "affine hull B = affine hull V \<and> \<not> affine_dependent B"
|
|
1213 |
shows "of_nat (card B) = aff_dim V + 1"
|
|
1214 |
proof (cases "B = {}")
|
|
1215 |
case True
|
|
1216 |
then have "V = {}"
|
|
1217 |
using assms
|
|
1218 |
by auto
|
|
1219 |
then have "aff_dim V = (-1::int)"
|
|
1220 |
using aff_dim_empty by auto
|
|
1221 |
then show ?thesis
|
|
1222 |
using \<open>B = {}\<close> by auto
|
|
1223 |
next
|
|
1224 |
case False
|
|
1225 |
then obtain a where a: "a \<in> B" by auto
|
|
1226 |
define Lb where "Lb = span ((\<lambda>x. -a+x) ` (B-{a}))"
|
|
1227 |
have "affine_parallel (affine hull B) Lb"
|
|
1228 |
using Lb_def affine_hull_span2[of a B] a
|
|
1229 |
affine_parallel_commut[of "Lb" "(affine hull B)"]
|
|
1230 |
unfolding affine_parallel_def by auto
|
|
1231 |
moreover have "subspace Lb"
|
|
1232 |
using Lb_def subspace_span by auto
|
|
1233 |
ultimately have "aff_dim B = int(dim Lb)"
|
|
1234 |
using aff_dim_parallel_subspace[of B Lb] \<open>B \<noteq> {}\<close> by auto
|
|
1235 |
moreover have "(card B) - 1 = dim Lb" "finite B"
|
|
1236 |
using Lb_def aff_dim_parallel_subspace_aux a assms by auto
|
|
1237 |
ultimately have "of_nat (card B) = aff_dim B + 1"
|
|
1238 |
using \<open>B \<noteq> {}\<close> card_gt_0_iff[of B] by auto
|
|
1239 |
then show ?thesis
|
|
1240 |
using aff_dim_affine_hull2 assms by auto
|
|
1241 |
qed
|
|
1242 |
|
|
1243 |
lemma aff_dim_affine_independent:
|
|
1244 |
fixes B :: "'n::euclidean_space set"
|
|
1245 |
assumes "\<not> affine_dependent B"
|
|
1246 |
shows "of_nat (card B) = aff_dim B + 1"
|
|
1247 |
using aff_dim_unique[of B B] assms by auto
|
|
1248 |
|
|
1249 |
lemma affine_independent_iff_card:
|
|
1250 |
fixes s :: "'a::euclidean_space set"
|
|
1251 |
shows "\<not> affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
|
|
1252 |
apply (rule iffI)
|
|
1253 |
apply (simp add: aff_dim_affine_independent aff_independent_finite)
|
|
1254 |
by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff)
|
|
1255 |
|
|
1256 |
lemma aff_dim_sing [simp]:
|
|
1257 |
fixes a :: "'n::euclidean_space"
|
|
1258 |
shows "aff_dim {a} = 0"
|
|
1259 |
using aff_dim_affine_independent[of "{a}"] affine_independent_1 by auto
|
|
1260 |
|
|
1261 |
lemma aff_dim_2 [simp]: "aff_dim {a,b} = (if a = b then 0 else 1)"
|
|
1262 |
proof (clarsimp)
|
|
1263 |
assume "a \<noteq> b"
|
|
1264 |
then have "aff_dim{a,b} = card{a,b} - 1"
|
|
1265 |
using affine_independent_2 [of a b] aff_dim_affine_independent by fastforce
|
|
1266 |
also have "\<dots> = 1"
|
|
1267 |
using \<open>a \<noteq> b\<close> by simp
|
|
1268 |
finally show "aff_dim {a, b} = 1" .
|
|
1269 |
qed
|
|
1270 |
|
|
1271 |
lemma aff_dim_inner_basis_exists:
|
|
1272 |
fixes V :: "('n::euclidean_space) set"
|
|
1273 |
shows "\<exists>B. B \<subseteq> V \<and> affine hull B = affine hull V \<and>
|
|
1274 |
\<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1"
|
|
1275 |
proof -
|
|
1276 |
obtain B where B: "\<not> affine_dependent B" "B \<subseteq> V" "affine hull B = affine hull V"
|
|
1277 |
using affine_basis_exists[of V] by auto
|
|
1278 |
then have "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto
|
|
1279 |
with B show ?thesis by auto
|
|
1280 |
qed
|
|
1281 |
|
|
1282 |
lemma aff_dim_le_card:
|
|
1283 |
fixes V :: "'n::euclidean_space set"
|
|
1284 |
assumes "finite V"
|
|
1285 |
shows "aff_dim V \<le> of_nat (card V) - 1"
|
|
1286 |
proof -
|
|
1287 |
obtain B where B: "B \<subseteq> V" "of_nat (card B) = aff_dim V + 1"
|
|
1288 |
using aff_dim_inner_basis_exists[of V] by auto
|
|
1289 |
then have "card B \<le> card V"
|
|
1290 |
using assms card_mono by auto
|
|
1291 |
with B show ?thesis by auto
|
|
1292 |
qed
|
|
1293 |
|
|
1294 |
lemma aff_dim_parallel_eq:
|
|
1295 |
fixes S T :: "'n::euclidean_space set"
|
|
1296 |
assumes "affine_parallel (affine hull S) (affine hull T)"
|
|
1297 |
shows "aff_dim S = aff_dim T"
|
|
1298 |
proof -
|
|
1299 |
{
|
|
1300 |
assume "T \<noteq> {}" "S \<noteq> {}"
|
|
1301 |
then obtain L where L: "subspace L \<and> affine_parallel (affine hull T) L"
|
|
1302 |
using affine_parallel_subspace[of "affine hull T"]
|
|
1303 |
affine_affine_hull[of T]
|
|
1304 |
by auto
|
|
1305 |
then have "aff_dim T = int (dim L)"
|
|
1306 |
using aff_dim_parallel_subspace \<open>T \<noteq> {}\<close> by auto
|
|
1307 |
moreover have *: "subspace L \<and> affine_parallel (affine hull S) L"
|
|
1308 |
using L affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto
|
|
1309 |
moreover from * have "aff_dim S = int (dim L)"
|
|
1310 |
using aff_dim_parallel_subspace \<open>S \<noteq> {}\<close> by auto
|
|
1311 |
ultimately have ?thesis by auto
|
|
1312 |
}
|
|
1313 |
moreover
|
|
1314 |
{
|
|
1315 |
assume "S = {}"
|
|
1316 |
then have "S = {}" and "T = {}"
|
|
1317 |
using assms
|
|
1318 |
unfolding affine_parallel_def
|
|
1319 |
by auto
|
|
1320 |
then have ?thesis using aff_dim_empty by auto
|
|
1321 |
}
|
|
1322 |
moreover
|
|
1323 |
{
|
|
1324 |
assume "T = {}"
|
|
1325 |
then have "S = {}" and "T = {}"
|
|
1326 |
using assms
|
|
1327 |
unfolding affine_parallel_def
|
|
1328 |
by auto
|
|
1329 |
then have ?thesis
|
|
1330 |
using aff_dim_empty by auto
|
|
1331 |
}
|
|
1332 |
ultimately show ?thesis by blast
|
|
1333 |
qed
|
|
1334 |
|
|
1335 |
lemma aff_dim_translation_eq:
|
|
1336 |
"aff_dim ((+) a ` S) = aff_dim S" for a :: "'n::euclidean_space"
|
|
1337 |
proof -
|
|
1338 |
have "affine_parallel (affine hull S) (affine hull ((\<lambda>x. a + x) ` S))"
|
|
1339 |
unfolding affine_parallel_def
|
|
1340 |
apply (rule exI[of _ "a"])
|
|
1341 |
using affine_hull_translation[of a S]
|
|
1342 |
apply auto
|
|
1343 |
done
|
|
1344 |
then show ?thesis
|
|
1345 |
using aff_dim_parallel_eq[of S "(\<lambda>x. a + x) ` S"] by auto
|
|
1346 |
qed
|
|
1347 |
|
|
1348 |
lemma aff_dim_translation_eq_subtract:
|
|
1349 |
"aff_dim ((\<lambda>x. x - a) ` S) = aff_dim S" for a :: "'n::euclidean_space"
|
|
1350 |
using aff_dim_translation_eq [of "- a"] by (simp cong: image_cong_simp)
|
|
1351 |
|
|
1352 |
lemma aff_dim_affine:
|
|
1353 |
fixes S L :: "'n::euclidean_space set"
|
|
1354 |
assumes "S \<noteq> {}"
|
|
1355 |
and "affine S"
|
|
1356 |
and "subspace L"
|
|
1357 |
and "affine_parallel S L"
|
|
1358 |
shows "aff_dim S = int (dim L)"
|
|
1359 |
proof -
|
|
1360 |
have *: "affine hull S = S"
|
|
1361 |
using assms affine_hull_eq[of S] by auto
|
|
1362 |
then have "affine_parallel (affine hull S) L"
|
|
1363 |
using assms by (simp add: *)
|
|
1364 |
then show ?thesis
|
|
1365 |
using assms aff_dim_parallel_subspace[of S L] by blast
|
|
1366 |
qed
|
|
1367 |
|
|
1368 |
lemma dim_affine_hull:
|
|
1369 |
fixes S :: "'n::euclidean_space set"
|
|
1370 |
shows "dim (affine hull S) = dim S"
|
|
1371 |
proof -
|
|
1372 |
have "dim (affine hull S) \<ge> dim S"
|
|
1373 |
using dim_subset by auto
|
|
1374 |
moreover have "dim (span S) \<ge> dim (affine hull S)"
|
|
1375 |
using dim_subset affine_hull_subset_span by blast
|
|
1376 |
moreover have "dim (span S) = dim S"
|
|
1377 |
using dim_span by auto
|
|
1378 |
ultimately show ?thesis by auto
|
|
1379 |
qed
|
|
1380 |
|
|
1381 |
lemma aff_dim_subspace:
|
|
1382 |
fixes S :: "'n::euclidean_space set"
|
|
1383 |
assumes "subspace S"
|
|
1384 |
shows "aff_dim S = int (dim S)"
|
|
1385 |
proof (cases "S={}")
|
|
1386 |
case True with assms show ?thesis
|
|
1387 |
by (simp add: subspace_affine)
|
|
1388 |
next
|
|
1389 |
case False
|
|
1390 |
with aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] subspace_affine
|
|
1391 |
show ?thesis by auto
|
|
1392 |
qed
|
|
1393 |
|
|
1394 |
lemma aff_dim_zero:
|
|
1395 |
fixes S :: "'n::euclidean_space set"
|
|
1396 |
assumes "0 \<in> affine hull S"
|
|
1397 |
shows "aff_dim S = int (dim S)"
|
|
1398 |
proof -
|
|
1399 |
have "subspace (affine hull S)"
|
|
1400 |
using subspace_affine[of "affine hull S"] affine_affine_hull assms
|
|
1401 |
by auto
|
|
1402 |
then have "aff_dim (affine hull S) = int (dim (affine hull S))"
|
|
1403 |
using assms aff_dim_subspace[of "affine hull S"] by auto
|
|
1404 |
then show ?thesis
|
|
1405 |
using aff_dim_affine_hull[of S] dim_affine_hull[of S]
|
|
1406 |
by auto
|
|
1407 |
qed
|
|
1408 |
|
|
1409 |
lemma aff_dim_eq_dim:
|
|
1410 |
"aff_dim S = int (dim ((+) (- a) ` S))" if "a \<in> affine hull S"
|
|
1411 |
for S :: "'n::euclidean_space set"
|
|
1412 |
proof -
|
|
1413 |
have "0 \<in> affine hull (+) (- a) ` S"
|
|
1414 |
unfolding affine_hull_translation
|
|
1415 |
using that by (simp add: ac_simps)
|
|
1416 |
with aff_dim_zero show ?thesis
|
|
1417 |
by (metis aff_dim_translation_eq)
|
|
1418 |
qed
|
|
1419 |
|
|
1420 |
lemma aff_dim_eq_dim_subtract:
|
|
1421 |
"aff_dim S = int (dim ((\<lambda>x. x - a) ` S))" if "a \<in> affine hull S"
|
|
1422 |
for S :: "'n::euclidean_space set"
|
|
1423 |
using aff_dim_eq_dim [of a] that by (simp cong: image_cong_simp)
|
|
1424 |
|
|
1425 |
lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
|
|
1426 |
using aff_dim_subspace[of "(UNIV :: 'n::euclidean_space set)"]
|
|
1427 |
dim_UNIV[where 'a="'n::euclidean_space"]
|
|
1428 |
by auto
|
|
1429 |
|
|
1430 |
lemma aff_dim_geq:
|
|
1431 |
fixes V :: "'n::euclidean_space set"
|
|
1432 |
shows "aff_dim V \<ge> -1"
|
|
1433 |
proof -
|
|
1434 |
obtain B where "affine hull B = affine hull V"
|
|
1435 |
and "\<not> affine_dependent B"
|
|
1436 |
and "int (card B) = aff_dim V + 1"
|
|
1437 |
using aff_dim_basis_exists by auto
|
|
1438 |
then show ?thesis by auto
|
|
1439 |
qed
|
|
1440 |
|
|
1441 |
lemma aff_dim_negative_iff [simp]:
|
|
1442 |
fixes S :: "'n::euclidean_space set"
|
|
1443 |
shows "aff_dim S < 0 \<longleftrightarrow>S = {}"
|
|
1444 |
by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq)
|
|
1445 |
|
|
1446 |
lemma aff_lowdim_subset_hyperplane:
|
|
1447 |
fixes S :: "'a::euclidean_space set"
|
|
1448 |
assumes "aff_dim S < DIM('a)"
|
|
1449 |
obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x = b}"
|
|
1450 |
proof (cases "S={}")
|
|
1451 |
case True
|
|
1452 |
moreover
|
|
1453 |
have "(SOME b. b \<in> Basis) \<noteq> 0"
|
|
1454 |
by (metis norm_some_Basis norm_zero zero_neq_one)
|
|
1455 |
ultimately show ?thesis
|
|
1456 |
using that by blast
|
|
1457 |
next
|
|
1458 |
case False
|
|
1459 |
then obtain c S' where "c \<notin> S'" "S = insert c S'"
|
|
1460 |
by (meson equals0I mk_disjoint_insert)
|
|
1461 |
have "dim ((+) (-c) ` S) < DIM('a)"
|
|
1462 |
by (metis \<open>S = insert c S'\<close> aff_dim_eq_dim assms hull_inc insertI1 of_nat_less_imp_less)
|
|
1463 |
then obtain a where "a \<noteq> 0" "span ((+) (-c) ` S) \<subseteq> {x. a \<bullet> x = 0}"
|
|
1464 |
using lowdim_subset_hyperplane by blast
|
|
1465 |
moreover
|
|
1466 |
have "a \<bullet> w = a \<bullet> c" if "span ((+) (- c) ` S) \<subseteq> {x. a \<bullet> x = 0}" "w \<in> S" for w
|
|
1467 |
proof -
|
|
1468 |
have "w-c \<in> span ((+) (- c) ` S)"
|
|
1469 |
by (simp add: span_base \<open>w \<in> S\<close>)
|
|
1470 |
with that have "w-c \<in> {x. a \<bullet> x = 0}"
|
|
1471 |
by blast
|
|
1472 |
then show ?thesis
|
|
1473 |
by (auto simp: algebra_simps)
|
|
1474 |
qed
|
|
1475 |
ultimately have "S \<subseteq> {x. a \<bullet> x = a \<bullet> c}"
|
|
1476 |
by blast
|
|
1477 |
then show ?thesis
|
|
1478 |
by (rule that[OF \<open>a \<noteq> 0\<close>])
|
|
1479 |
qed
|
|
1480 |
|
|
1481 |
lemma affine_independent_card_dim_diffs:
|
|
1482 |
fixes S :: "'a :: euclidean_space set"
|
|
1483 |
assumes "\<not> affine_dependent S" "a \<in> S"
|
|
1484 |
shows "card S = dim {x - a|x. x \<in> S} + 1"
|
|
1485 |
proof -
|
|
1486 |
have 1: "{b - a|b. b \<in> (S - {a})} \<subseteq> {x - a|x. x \<in> S}" by auto
|
|
1487 |
have 2: "x - a \<in> span {b - a |b. b \<in> S - {a}}" if "x \<in> S" for x
|
|
1488 |
proof (cases "x = a")
|
|
1489 |
case True then show ?thesis by (simp add: span_clauses)
|
|
1490 |
next
|
|
1491 |
case False then show ?thesis
|
|
1492 |
using assms by (blast intro: span_base that)
|
|
1493 |
qed
|
|
1494 |
have "\<not> affine_dependent (insert a S)"
|
|
1495 |
by (simp add: assms insert_absorb)
|
|
1496 |
then have 3: "independent {b - a |b. b \<in> S - {a}}"
|
|
1497 |
using dependent_imp_affine_dependent by fastforce
|
|
1498 |
have "{b - a |b. b \<in> S - {a}} = (\<lambda>b. b-a) ` (S - {a})"
|
|
1499 |
by blast
|
|
1500 |
then have "card {b - a |b. b \<in> S - {a}} = card ((\<lambda>b. b-a) ` (S - {a}))"
|
|
1501 |
by simp
|
|
1502 |
also have "\<dots> = card (S - {a})"
|
|
1503 |
by (metis (no_types, lifting) card_image diff_add_cancel inj_onI)
|
|
1504 |
also have "\<dots> = card S - 1"
|
|
1505 |
by (simp add: aff_independent_finite assms)
|
|
1506 |
finally have 4: "card {b - a |b. b \<in> S - {a}} = card S - 1" .
|
|
1507 |
have "finite S"
|
|
1508 |
by (meson assms aff_independent_finite)
|
|
1509 |
with \<open>a \<in> S\<close> have "card S \<noteq> 0" by auto
|
|
1510 |
moreover have "dim {x - a |x. x \<in> S} = card S - 1"
|
|
1511 |
using 2 by (blast intro: dim_unique [OF 1 _ 3 4])
|
|
1512 |
ultimately show ?thesis
|
|
1513 |
by auto
|
|
1514 |
qed
|
|
1515 |
|
|
1516 |
lemma independent_card_le_aff_dim:
|
|
1517 |
fixes B :: "'n::euclidean_space set"
|
|
1518 |
assumes "B \<subseteq> V"
|
|
1519 |
assumes "\<not> affine_dependent B"
|
|
1520 |
shows "int (card B) \<le> aff_dim V + 1"
|
|
1521 |
proof -
|
|
1522 |
obtain T where T: "\<not> affine_dependent T \<and> B \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
|
|
1523 |
by (metis assms extend_to_affine_basis[of B V])
|
|
1524 |
then have "of_nat (card T) = aff_dim V + 1"
|
|
1525 |
using aff_dim_unique by auto
|
|
1526 |
then show ?thesis
|
|
1527 |
using T card_mono[of T B] aff_independent_finite[of T] by auto
|
|
1528 |
qed
|
|
1529 |
|
|
1530 |
lemma aff_dim_subset:
|
|
1531 |
fixes S T :: "'n::euclidean_space set"
|
|
1532 |
assumes "S \<subseteq> T"
|
|
1533 |
shows "aff_dim S \<le> aff_dim T"
|
|
1534 |
proof -
|
|
1535 |
obtain B where B: "\<not> affine_dependent B" "B \<subseteq> S" "affine hull B = affine hull S"
|
|
1536 |
"of_nat (card B) = aff_dim S + 1"
|
|
1537 |
using aff_dim_inner_basis_exists[of S] by auto
|
|
1538 |
then have "int (card B) \<le> aff_dim T + 1"
|
|
1539 |
using assms independent_card_le_aff_dim[of B T] by auto
|
|
1540 |
with B show ?thesis by auto
|
|
1541 |
qed
|
|
1542 |
|
|
1543 |
lemma aff_dim_le_DIM:
|
|
1544 |
fixes S :: "'n::euclidean_space set"
|
|
1545 |
shows "aff_dim S \<le> int (DIM('n))"
|
|
1546 |
proof -
|
|
1547 |
have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
|
|
1548 |
using aff_dim_UNIV by auto
|
|
1549 |
then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
|
|
1550 |
using aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
|
|
1551 |
qed
|
|
1552 |
|
|
1553 |
lemma affine_dim_equal:
|
|
1554 |
fixes S :: "'n::euclidean_space set"
|
|
1555 |
assumes "affine S" "affine T" "S \<noteq> {}" "S \<subseteq> T" "aff_dim S = aff_dim T"
|
|
1556 |
shows "S = T"
|
|
1557 |
proof -
|
|
1558 |
obtain a where "a \<in> S" using assms by auto
|
|
1559 |
then have "a \<in> T" using assms by auto
|
|
1560 |
define LS where "LS = {y. \<exists>x \<in> S. (-a) + x = y}"
|
|
1561 |
then have ls: "subspace LS" "affine_parallel S LS"
|
|
1562 |
using assms parallel_subspace_explicit[of S a LS] \<open>a \<in> S\<close> by auto
|
|
1563 |
then have h1: "int(dim LS) = aff_dim S"
|
|
1564 |
using assms aff_dim_affine[of S LS] by auto
|
|
1565 |
have "T \<noteq> {}" using assms by auto
|
|
1566 |
define LT where "LT = {y. \<exists>x \<in> T. (-a) + x = y}"
|
|
1567 |
then have lt: "subspace LT \<and> affine_parallel T LT"
|
|
1568 |
using assms parallel_subspace_explicit[of T a LT] \<open>a \<in> T\<close> by auto
|
|
1569 |
then have "int(dim LT) = aff_dim T"
|
|
1570 |
using assms aff_dim_affine[of T LT] \<open>T \<noteq> {}\<close> by auto
|
|
1571 |
then have "dim LS = dim LT"
|
|
1572 |
using h1 assms by auto
|
|
1573 |
moreover have "LS \<le> LT"
|
|
1574 |
using LS_def LT_def assms by auto
|
|
1575 |
ultimately have "LS = LT"
|
|
1576 |
using subspace_dim_equal[of LS LT] ls lt by auto
|
|
1577 |
moreover have "S = {x. \<exists>y \<in> LS. a+y=x}"
|
|
1578 |
using LS_def by auto
|
|
1579 |
moreover have "T = {x. \<exists>y \<in> LT. a+y=x}"
|
|
1580 |
using LT_def by auto
|
|
1581 |
ultimately show ?thesis by auto
|
|
1582 |
qed
|
|
1583 |
|
|
1584 |
lemma aff_dim_eq_0:
|
|
1585 |
fixes S :: "'a::euclidean_space set"
|
|
1586 |
shows "aff_dim S = 0 \<longleftrightarrow> (\<exists>a. S = {a})"
|
|
1587 |
proof (cases "S = {}")
|
|
1588 |
case True
|
|
1589 |
then show ?thesis
|
|
1590 |
by auto
|
|
1591 |
next
|
|
1592 |
case False
|
|
1593 |
then obtain a where "a \<in> S" by auto
|
|
1594 |
show ?thesis
|
|
1595 |
proof safe
|
|
1596 |
assume 0: "aff_dim S = 0"
|
|
1597 |
have "\<not> {a,b} \<subseteq> S" if "b \<noteq> a" for b
|
|
1598 |
by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that)
|
|
1599 |
then show "\<exists>a. S = {a}"
|
|
1600 |
using \<open>a \<in> S\<close> by blast
|
|
1601 |
qed auto
|
|
1602 |
qed
|
|
1603 |
|
|
1604 |
lemma affine_hull_UNIV:
|
|
1605 |
fixes S :: "'n::euclidean_space set"
|
|
1606 |
assumes "aff_dim S = int(DIM('n))"
|
|
1607 |
shows "affine hull S = (UNIV :: ('n::euclidean_space) set)"
|
|
1608 |
proof -
|
|
1609 |
have "S \<noteq> {}"
|
|
1610 |
using assms aff_dim_empty[of S] by auto
|
|
1611 |
have h0: "S \<subseteq> affine hull S"
|
|
1612 |
using hull_subset[of S _] by auto
|
|
1613 |
have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S"
|
|
1614 |
using aff_dim_UNIV assms by auto
|
|
1615 |
then have h2: "aff_dim (affine hull S) \<le> aff_dim (UNIV :: ('n::euclidean_space) set)"
|
|
1616 |
using aff_dim_le_DIM[of "affine hull S"] assms h0 by auto
|
|
1617 |
have h3: "aff_dim S \<le> aff_dim (affine hull S)"
|
|
1618 |
using h0 aff_dim_subset[of S "affine hull S"] assms by auto
|
|
1619 |
then have h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)"
|
|
1620 |
using h0 h1 h2 by auto
|
|
1621 |
then show ?thesis
|
|
1622 |
using affine_dim_equal[of "affine hull S" "(UNIV :: ('n::euclidean_space) set)"]
|
|
1623 |
affine_affine_hull[of S] affine_UNIV assms h4 h0 \<open>S \<noteq> {}\<close>
|
|
1624 |
by auto
|
|
1625 |
qed
|
|
1626 |
|
|
1627 |
lemma disjoint_affine_hull:
|
|
1628 |
fixes s :: "'n::euclidean_space set"
|
|
1629 |
assumes "\<not> affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
|
|
1630 |
shows "(affine hull t) \<inter> (affine hull u) = {}"
|
|
1631 |
proof -
|
|
1632 |
have "finite s" using assms by (simp add: aff_independent_finite)
|
|
1633 |
then have "finite t" "finite u" using assms finite_subset by blast+
|
|
1634 |
{ fix y
|
|
1635 |
assume yt: "y \<in> affine hull t" and yu: "y \<in> affine hull u"
|
|
1636 |
then obtain a b
|
|
1637 |
where a1 [simp]: "sum a t = 1" and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) t = y"
|
|
1638 |
and [simp]: "sum b u = 1" "sum (\<lambda>v. b v *\<^sub>R v) u = y"
|
|
1639 |
by (auto simp: affine_hull_finite \<open>finite t\<close> \<open>finite u\<close>)
|
|
1640 |
define c where "c x = (if x \<in> t then a x else if x \<in> u then -(b x) else 0)" for x
|
|
1641 |
have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u" using assms by auto
|
|
1642 |
have "sum c s = 0"
|
|
1643 |
by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite s\<close> sum_negf)
|
|
1644 |
moreover have "\<not> (\<forall>v\<in>s. c v = 0)"
|
|
1645 |
by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum.neutral zero_neq_one)
|
|
1646 |
moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
|
|
1647 |
by (simp add: c_def if_smult sum_negf
|
|
1648 |
comm_monoid_add_class.sum.If_cases \<open>finite s\<close>)
|
|
1649 |
ultimately have False
|
|
1650 |
using assms \<open>finite s\<close> by (auto simp: affine_dependent_explicit)
|
|
1651 |
}
|
|
1652 |
then show ?thesis by blast
|
|
1653 |
qed
|
|
1654 |
|
|
1655 |
end |