author | paulson <lp15@cam.ac.uk> |
Mon, 06 May 2024 14:39:33 +0100 | |
changeset 80175 | 200107cdd3ac |
parent 78516 | 56a408fa2440 |
permissions | -rw-r--r-- |
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)" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
8 |
by simp |
71242 | 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" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
16 |
by (smt (verit, best) assms sum.cong)+ |
71242 | 17 |
|
18 |
lemma span_substd_basis: |
|
19 |
assumes d: "d \<subseteq> Basis" |
|
20 |
shows "span d = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}" |
|
21 |
(is "_ = ?B") |
|
22 |
proof - |
|
23 |
have "d \<subseteq> ?B" |
|
24 |
using d by (auto simp: inner_Basis) |
|
25 |
moreover have s: "subspace ?B" |
|
26 |
using subspace_substandard[of "\<lambda>i. i \<notin> d"] . |
|
27 |
ultimately have "span d \<subseteq> ?B" |
|
28 |
using span_mono[of d "?B"] span_eq_iff[of "?B"] by blast |
|
29 |
moreover have *: "card d \<le> dim (span d)" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
30 |
by (simp add: d dim_eq_card_independent independent_substdbasis) |
71242 | 31 |
moreover from * have "dim ?B \<le> dim (span d)" |
32 |
using dim_substandard[OF assms] by auto |
|
33 |
ultimately show ?thesis |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
34 |
by (simp add: s subspace_dim_equal) |
71242 | 35 |
qed |
36 |
||
37 |
lemma basis_to_substdbasis_subspace_isomorphism: |
|
38 |
fixes B :: "'a::euclidean_space set" |
|
39 |
assumes "independent B" |
|
40 |
shows "\<exists>f d::'a set. card d = card B \<and> linear f \<and> f ` B = d \<and> |
|
41 |
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" |
|
42 |
proof - |
|
43 |
have B: "card B = dim B" |
|
44 |
using dim_unique[of B B "card B"] assms span_superset[of B] by auto |
|
45 |
have "dim B \<le> card (Basis :: 'a set)" |
|
46 |
using dim_subset_UNIV[of B] by simp |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
47 |
from obtain_subset_with_card_n[OF this] |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
48 |
obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B" |
71242 | 49 |
by auto |
50 |
let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}" |
|
51 |
have "\<exists>f. linear f \<and> f ` B = d \<and> f ` span B = ?t \<and> inj_on f (span B)" |
|
52 |
proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_superset) |
|
53 |
show "d \<subseteq> {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}" |
|
54 |
using d inner_not_same_Basis by blast |
|
55 |
qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms) |
|
56 |
with t \<open>card B = dim B\<close> d show ?thesis by auto |
|
57 |
qed |
|
58 |
||
59 |
subsection \<open>Affine set and affine hull\<close> |
|
60 |
||
61 |
definition\<^marker>\<open>tag important\<close> affine :: "'a::real_vector set \<Rightarrow> bool" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
62 |
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)" |
71242 | 63 |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
64 |
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)" |
71242 | 65 |
unfolding affine_def by (metis eq_diff_eq') |
66 |
||
67 |
lemma affine_empty [iff]: "affine {}" |
|
68 |
unfolding affine_def by auto |
|
69 |
||
70 |
lemma affine_sing [iff]: "affine {x}" |
|
71 |
unfolding affine_alt by (auto simp: scaleR_left_distrib [symmetric]) |
|
72 |
||
73 |
lemma affine_UNIV [iff]: "affine UNIV" |
|
74 |
unfolding affine_def by auto |
|
75 |
||
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
76 |
lemma affine_Inter [intro]: "(\<And>S. S\<in>\<F> \<Longrightarrow> affine S) \<Longrightarrow> affine (\<Inter>\<F>)" |
71242 | 77 |
unfolding affine_def by auto |
78 |
||
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
79 |
lemma affine_Int[intro]: "affine S \<Longrightarrow> affine T \<Longrightarrow> affine (S \<inter> T)" |
71242 | 80 |
unfolding affine_def by auto |
81 |
||
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
82 |
lemma affine_scaling: "affine S \<Longrightarrow> affine ((*\<^sub>R) c ` S)" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
83 |
apply (clarsimp simp: affine_def) |
71242 | 84 |
apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI) |
85 |
apply (auto simp: algebra_simps) |
|
86 |
done |
|
87 |
||
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
88 |
lemma affine_affine_hull [simp]: "affine(affine hull S)" |
71242 | 89 |
unfolding hull_def |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
90 |
using affine_Inter[of "{T. affine T \<and> S \<subseteq> T}"] by auto |
71242 | 91 |
|
92 |
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s" |
|
93 |
by (metis affine_affine_hull hull_same) |
|
94 |
||
95 |
lemma affine_hyperplane: "affine {x. a \<bullet> x = b}" |
|
96 |
by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral) |
|
97 |
||
98 |
||
99 |
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Some explicit formulations\<close> |
|
100 |
||
101 |
text "Formalized by Lars Schewe." |
|
102 |
||
103 |
lemma affine: |
|
104 |
fixes V::"'a::real_vector set" |
|
105 |
shows "affine V \<longleftrightarrow> |
|
106 |
(\<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)" |
|
107 |
proof - |
|
108 |
have "u *\<^sub>R x + v *\<^sub>R y \<in> V" if "x \<in> V" "y \<in> V" "u + v = (1::real)" |
|
109 |
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 |
|
110 |
proof (cases "x = y") |
|
111 |
case True |
|
112 |
then show ?thesis |
|
113 |
using that by (metis scaleR_add_left scaleR_one) |
|
114 |
next |
|
115 |
case False |
|
116 |
then show ?thesis |
|
117 |
using that *[of "{x,y}" "\<lambda>w. if w = x then u else v"] by auto |
|
118 |
qed |
|
119 |
moreover have "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V" |
|
120 |
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" |
|
121 |
and "finite S" "S \<noteq> {}" "S \<subseteq> V" "sum u S = 1" for S u |
|
122 |
proof - |
|
123 |
define n where "n = card S" |
|
124 |
consider "card S = 0" | "card S = 1" | "card S = 2" | "card S > 2" by linarith |
|
125 |
then show "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V" |
|
126 |
proof cases |
|
127 |
assume "card S = 1" |
|
128 |
then obtain a where "S={a}" |
|
129 |
by (auto simp: card_Suc_eq) |
|
130 |
then show ?thesis |
|
131 |
using that by simp |
|
132 |
next |
|
133 |
assume "card S = 2" |
|
134 |
then obtain a b where "S = {a, b}" |
|
135 |
by (metis Suc_1 card_1_singletonE card_Suc_eq) |
|
136 |
then show ?thesis |
|
137 |
using *[of a b] that |
|
138 |
by (auto simp: sum_clauses(2)) |
|
139 |
next |
|
140 |
assume "card S > 2" |
|
141 |
then show ?thesis using that n_def |
|
142 |
proof (induct n arbitrary: u S) |
|
143 |
case 0 |
|
144 |
then show ?case by auto |
|
145 |
next |
|
146 |
case (Suc n u S) |
|
147 |
have "sum u S = card S" if "\<not> (\<exists>x\<in>S. u x \<noteq> 1)" |
|
148 |
using that unfolding card_eq_sum by auto |
|
149 |
with Suc.prems obtain x where "x \<in> S" and x: "u x \<noteq> 1" by force |
|
150 |
have c: "card (S - {x}) = card S - 1" |
|
151 |
by (simp add: Suc.prems(3) \<open>x \<in> S\<close>) |
|
152 |
have "sum u (S - {x}) = 1 - u x" |
|
153 |
by (simp add: Suc.prems sum_diff1 \<open>x \<in> S\<close>) |
|
154 |
with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1" |
|
155 |
by auto |
|
156 |
have inV: "(\<Sum>y\<in>S - {x}. (inverse (1 - u x) * u y) *\<^sub>R y) \<in> V" |
|
157 |
proof (cases "card (S - {x}) > 2") |
|
158 |
case True |
|
159 |
then have S: "S - {x} \<noteq> {}" "card (S - {x}) = n" |
|
160 |
using Suc.prems c by force+ |
|
161 |
show ?thesis |
|
162 |
proof (rule Suc.hyps) |
|
163 |
show "(\<Sum>a\<in>S - {x}. inverse (1 - u x) * u a) = 1" |
|
164 |
by (auto simp: eq1 sum_distrib_left[symmetric]) |
|
165 |
qed (use S Suc.prems True in auto) |
|
166 |
next |
|
167 |
case False |
|
168 |
then have "card (S - {x}) = Suc (Suc 0)" |
|
169 |
using Suc.prems c by auto |
|
170 |
then obtain a b where ab: "(S - {x}) = {a, b}" "a\<noteq>b" |
|
171 |
unfolding card_Suc_eq by auto |
|
172 |
then show ?thesis |
|
173 |
using eq1 \<open>S \<subseteq> V\<close> |
|
174 |
by (auto simp: sum_distrib_left distrib_left intro!: Suc.prems(2)[of a b]) |
|
175 |
qed |
|
176 |
have "u x + (1 - u x) = 1 \<Longrightarrow> |
|
177 |
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" |
|
178 |
by (rule Suc.prems) (use \<open>x \<in> S\<close> Suc.prems inV in \<open>auto simp: scaleR_right.sum\<close>) |
|
179 |
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)" |
|
180 |
by (meson Suc.prems(3) sum.remove \<open>x \<in> S\<close>) |
|
181 |
ultimately show "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V" |
|
182 |
by (simp add: x) |
|
183 |
qed |
|
184 |
qed (use \<open>S\<noteq>{}\<close> \<open>finite S\<close> in auto) |
|
185 |
qed |
|
186 |
ultimately show ?thesis |
|
187 |
unfolding affine_def by meson |
|
188 |
qed |
|
189 |
||
190 |
||
191 |
lemma affine_hull_explicit: |
|
192 |
"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}" |
|
193 |
(is "_ = ?rhs") |
|
194 |
proof (rule hull_unique) |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
195 |
have "\<And>x. sum (\<lambda>z. 1) {x} = 1" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
196 |
by auto |
71242 | 197 |
show "p \<subseteq> ?rhs" |
198 |
proof (intro subsetI CollectI exI conjI) |
|
199 |
show "\<And>x. sum (\<lambda>z. 1) {x} = 1" |
|
200 |
by auto |
|
201 |
qed auto |
|
202 |
show "?rhs \<subseteq> T" if "p \<subseteq> T" "affine T" for T |
|
203 |
using that unfolding affine by blast |
|
204 |
show "affine ?rhs" |
|
205 |
unfolding affine_def |
|
206 |
proof clarify |
|
207 |
fix u v :: real and sx ux sy uy |
|
208 |
assume uv: "u + v = 1" |
|
209 |
and x: "finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "sum ux sx = (1::real)" |
|
210 |
and y: "finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "sum uy sy = (1::real)" |
|
211 |
have **: "(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy" |
|
212 |
by auto |
|
213 |
show "\<exists>S w. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p \<and> |
|
214 |
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)" |
|
215 |
proof (intro exI conjI) |
|
216 |
show "finite (sx \<union> sy)" |
|
217 |
using x y by auto |
|
218 |
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" |
|
219 |
using x y uv |
|
220 |
by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] sum_distrib_left [symmetric] **) |
|
221 |
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) |
|
222 |
= (\<Sum>i\<in>sx. (u * ux i) *\<^sub>R i) + (\<Sum>i\<in>sy. (v * uy i) *\<^sub>R i)" |
|
223 |
using x y |
|
224 |
unfolding scaleR_left_distrib scaleR_zero_left if_smult |
|
225 |
by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] **) |
|
226 |
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)" |
|
227 |
unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by blast |
|
228 |
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) |
|
229 |
= u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)" . |
|
230 |
qed (use x y in auto) |
|
231 |
qed |
|
232 |
qed |
|
233 |
||
234 |
lemma affine_hull_finite: |
|
235 |
assumes "finite S" |
|
236 |
shows "affine hull S = {y. \<exists>u. sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}" |
|
237 |
proof - |
|
238 |
have *: "\<exists>h. sum h S = 1 \<and> (\<Sum>v\<in>S. h v *\<^sub>R v) = x" |
|
239 |
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 |
|
240 |
proof - |
|
241 |
have "S \<inter> F = F" |
|
242 |
using that by auto |
|
243 |
show ?thesis |
|
244 |
proof (intro exI conjI) |
|
245 |
show "(\<Sum>x\<in>S. if x \<in> F then u x else 0) = 1" |
|
246 |
by (metis (mono_tags, lifting) \<open>S \<inter> F = F\<close> assms sum.inter_restrict sum) |
|
247 |
show "(\<Sum>v\<in>S. (if v \<in> F then u v else 0) *\<^sub>R v) = x" |
|
248 |
by (simp add: if_smult cong: if_cong) (metis (no_types) \<open>S \<inter> F = F\<close> assms sum.inter_restrict x) |
|
249 |
qed |
|
250 |
qed |
|
251 |
show ?thesis |
|
252 |
unfolding affine_hull_explicit using assms |
|
253 |
by (fastforce dest: *) |
|
254 |
qed |
|
255 |
||
256 |
||
257 |
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Stepping theorems and hence small special cases\<close> |
|
258 |
||
259 |
lemma affine_hull_empty[simp]: "affine hull {} = {}" |
|
260 |
by simp |
|
261 |
||
262 |
lemma affine_hull_finite_step: |
|
263 |
fixes y :: "'a::real_vector" |
|
264 |
shows "finite S \<Longrightarrow> |
|
265 |
(\<exists>u. sum u (insert a S) = w \<and> sum (\<lambda>x. u x *\<^sub>R x) (insert a S) = y) \<longleftrightarrow> |
|
266 |
(\<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") |
|
267 |
proof - |
|
268 |
assume fin: "finite S" |
|
269 |
show "?lhs = ?rhs" |
|
270 |
proof |
|
271 |
assume ?lhs |
|
272 |
then obtain u where u: "sum u (insert a S) = w \<and> (\<Sum>x\<in>insert a S. u x *\<^sub>R x) = y" |
|
273 |
by auto |
|
274 |
show ?rhs |
|
275 |
proof (cases "a \<in> S") |
|
276 |
case True |
|
277 |
then show ?thesis |
|
278 |
using u by (simp add: insert_absorb) (metis diff_zero real_vector.scale_zero_left) |
|
279 |
next |
|
280 |
case False |
|
281 |
show ?thesis |
|
282 |
by (rule exI [where x="u a"]) (use u fin False in auto) |
|
283 |
qed |
|
284 |
next |
|
285 |
assume ?rhs |
|
286 |
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" |
|
287 |
by auto |
|
288 |
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)" |
|
289 |
by auto |
|
290 |
show ?lhs |
|
291 |
proof (cases "a \<in> S") |
|
292 |
case True |
|
293 |
show ?thesis |
|
294 |
by (rule exI [where x="\<lambda>x. (if x=a then v else 0) + u x"]) |
|
295 |
(simp add: True scaleR_left_distrib sum.distrib sum_clauses fin vu * cong: if_cong) |
|
296 |
next |
|
297 |
case False |
|
298 |
then show ?thesis |
|
299 |
apply (rule_tac x="\<lambda>x. if x=a then v else u x" in exI) |
|
300 |
apply (simp add: vu sum_clauses(2)[OF fin] *) |
|
301 |
by (simp add: sum_delta_notmem(3) vu) |
|
302 |
qed |
|
303 |
qed |
|
304 |
qed |
|
305 |
||
306 |
lemma affine_hull_2: |
|
307 |
fixes a b :: "'a::real_vector" |
|
308 |
shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" |
|
309 |
(is "?lhs = ?rhs") |
|
310 |
proof - |
|
311 |
have *: |
|
312 |
"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" |
|
313 |
"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto |
|
314 |
have "?lhs = {y. \<exists>u. sum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}" |
|
315 |
using affine_hull_finite[of "{a,b}"] by auto |
|
316 |
also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}" |
|
317 |
by (simp add: affine_hull_finite_step[of "{b}" a]) |
|
318 |
also have "\<dots> = ?rhs" unfolding * by auto |
|
319 |
finally show ?thesis by auto |
|
320 |
qed |
|
321 |
||
322 |
lemma affine_hull_3: |
|
323 |
fixes a b c :: "'a::real_vector" |
|
324 |
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}" |
|
325 |
proof - |
|
326 |
have *: |
|
327 |
"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" |
|
328 |
"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto |
|
329 |
show ?thesis |
|
330 |
apply (simp add: affine_hull_finite affine_hull_finite_step) |
|
331 |
unfolding * |
|
332 |
apply safe |
|
333 |
apply (metis add.assoc) |
|
334 |
apply (rule_tac x=u in exI, force) |
|
335 |
done |
|
336 |
qed |
|
337 |
||
338 |
lemma mem_affine: |
|
339 |
assumes "affine S" "x \<in> S" "y \<in> S" "u + v = 1" |
|
340 |
shows "u *\<^sub>R x + v *\<^sub>R y \<in> S" |
|
341 |
using assms affine_def[of S] by auto |
|
342 |
||
343 |
lemma mem_affine_3: |
|
344 |
assumes "affine S" "x \<in> S" "y \<in> S" "z \<in> S" "u + v + w = 1" |
|
345 |
shows "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \<in> S" |
|
346 |
proof - |
|
347 |
have "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \<in> affine hull {x, y, z}" |
|
348 |
using affine_hull_3[of x y z] assms by auto |
|
349 |
moreover |
|
350 |
have "affine hull {x, y, z} \<subseteq> affine hull S" |
|
351 |
using hull_mono[of "{x, y, z}" "S"] assms by auto |
|
352 |
moreover |
|
353 |
have "affine hull S = S" |
|
354 |
using assms affine_hull_eq[of S] by auto |
|
355 |
ultimately show ?thesis by auto |
|
356 |
qed |
|
357 |
||
358 |
lemma mem_affine_3_minus: |
|
359 |
assumes "affine S" "x \<in> S" "y \<in> S" "z \<in> S" |
|
360 |
shows "x + v *\<^sub>R (y-z) \<in> S" |
|
361 |
using mem_affine_3[of S x y z 1 v "-v"] assms |
|
362 |
by (simp add: algebra_simps) |
|
363 |
||
364 |
corollary%unimportant mem_affine_3_minus2: |
|
365 |
"\<lbrakk>affine S; x \<in> S; y \<in> S; z \<in> S\<rbrakk> \<Longrightarrow> x - v *\<^sub>R (y-z) \<in> S" |
|
366 |
by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left) |
|
367 |
||
368 |
||
369 |
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Some relations between affine hull and subspaces\<close> |
|
370 |
||
371 |
lemma affine_hull_insert_subset_span: |
|
372 |
"affine hull (insert a S) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> S}}" |
|
373 |
proof - |
|
374 |
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)" |
|
375 |
if "finite F" "F \<noteq> {}" "F \<subseteq> insert a S" "sum u F = 1" "(\<Sum>v\<in>F. u v *\<^sub>R v) = x" |
|
376 |
for x F u |
|
377 |
proof - |
|
378 |
have *: "(\<lambda>x. x - a) ` (F - {a}) \<subseteq> {x - a |x. x \<in> S}" |
|
379 |
using that by auto |
|
380 |
show ?thesis |
|
381 |
proof (intro exI conjI) |
|
382 |
show "finite ((\<lambda>x. x - a) ` (F - {a}))" |
|
383 |
by (simp add: that(1)) |
|
384 |
show "(\<Sum>v\<in>(\<lambda>x. x - a) ` (F - {a}). u(v+a) *\<^sub>R v) = x-a" |
|
385 |
by (simp add: sum.reindex[unfolded inj_on_def] algebra_simps |
|
386 |
sum_subtractf scaleR_left.sum[symmetric] sum_diff1 that) |
|
387 |
qed (use \<open>F \<subseteq> insert a S\<close> in auto) |
|
388 |
qed |
|
389 |
then show ?thesis |
|
71840
8ed78bb0b915
Tuned some proofs in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71243
diff
changeset
|
390 |
unfolding affine_hull_explicit span_explicit by fast |
71242 | 391 |
qed |
392 |
||
393 |
lemma affine_hull_insert_span: |
|
394 |
assumes "a \<notin> S" |
|
395 |
shows "affine hull (insert a S) = {a + v | v . v \<in> span {x - a | x. x \<in> S}}" |
|
396 |
proof - |
|
397 |
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" |
|
398 |
if "v \<in> span {x - a |x. x \<in> S}" "y = a + v" for y v |
|
399 |
proof - |
|
400 |
from that |
|
401 |
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" |
|
402 |
unfolding span_explicit by auto |
|
403 |
define F where "F = (\<lambda>x. x + a) ` T" |
|
404 |
have F: "finite F" "F \<subseteq> S" "(\<Sum>v\<in>F. u (v - a) *\<^sub>R (v - a)) = y - a" |
|
405 |
unfolding F_def using u by (auto simp: sum.reindex[unfolded inj_on_def]) |
|
406 |
have *: "F \<inter> {a} = {}" "F \<inter> - {a} = F" |
|
407 |
using F assms by auto |
|
408 |
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" |
|
409 |
apply (rule_tac x = "insert a F" in exI) |
|
410 |
apply (rule_tac x = "\<lambda>x. if x=a then 1 - sum (\<lambda>x. u (x - a)) F else u (x - a)" in exI) |
|
411 |
using assms F |
|
412 |
apply (auto simp: sum_clauses sum.If_cases if_smult sum_subtractf scaleR_left.sum algebra_simps *) |
|
413 |
done |
|
414 |
qed |
|
415 |
show ?thesis |
|
416 |
by (intro subset_antisym affine_hull_insert_subset_span) (auto simp: affine_hull_explicit dest!: *) |
|
417 |
qed |
|
418 |
||
419 |
lemma affine_hull_span: |
|
420 |
assumes "a \<in> S" |
|
421 |
shows "affine hull S = {a + v | v. v \<in> span {x - a | x. x \<in> S - {a}}}" |
|
422 |
using affine_hull_insert_span[of a "S - {a}", unfolded insert_Diff[OF assms]] by auto |
|
423 |
||
424 |
||
425 |
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Parallel affine sets\<close> |
|
426 |
||
427 |
definition affine_parallel :: "'a::real_vector set \<Rightarrow> 'a::real_vector set \<Rightarrow> bool" |
|
428 |
where "affine_parallel S T \<longleftrightarrow> (\<exists>a. T = (\<lambda>x. a + x) ` S)" |
|
429 |
||
430 |
lemma affine_parallel_expl_aux: |
|
431 |
fixes S T :: "'a::real_vector set" |
|
432 |
assumes "\<And>x. x \<in> S \<longleftrightarrow> a + x \<in> T" |
|
433 |
shows "T = (\<lambda>x. a + x) ` S" |
|
434 |
proof - |
|
435 |
have "x \<in> ((\<lambda>x. a + x) ` S)" if "x \<in> T" for x |
|
436 |
using that |
|
437 |
by (simp add: image_iff) (metis add.commute diff_add_cancel assms) |
|
438 |
moreover have "T \<ge> (\<lambda>x. a + x) ` S" |
|
439 |
using assms by auto |
|
440 |
ultimately show ?thesis by auto |
|
441 |
qed |
|
442 |
||
443 |
lemma affine_parallel_expl: "affine_parallel S T \<longleftrightarrow> (\<exists>a. \<forall>x. x \<in> S \<longleftrightarrow> a + x \<in> T)" |
|
444 |
by (auto simp add: affine_parallel_def) |
|
445 |
(use affine_parallel_expl_aux [of S _ T] in blast) |
|
446 |
||
447 |
lemma affine_parallel_reflex: "affine_parallel S S" |
|
448 |
unfolding affine_parallel_def |
|
449 |
using image_add_0 by blast |
|
450 |
||
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
451 |
lemma affine_parallel_commute: |
71242 | 452 |
assumes "affine_parallel A B" |
453 |
shows "affine_parallel B A" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
454 |
by (metis affine_parallel_def assms translation_galois) |
71242 | 455 |
|
456 |
lemma affine_parallel_assoc: |
|
457 |
assumes "affine_parallel A B" |
|
458 |
and "affine_parallel B C" |
|
459 |
shows "affine_parallel A C" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
460 |
by (metis affine_parallel_def assms translation_assoc) |
71242 | 461 |
|
462 |
lemma affine_translation_aux: |
|
463 |
fixes a :: "'a::real_vector" |
|
464 |
assumes "affine ((\<lambda>x. a + x) ` S)" |
|
465 |
shows "affine S" |
|
466 |
proof - |
|
467 |
{ |
|
468 |
fix x y u v |
|
469 |
assume xy: "x \<in> S" "y \<in> S" "(u :: real) + v = 1" |
|
470 |
then have "(a + x) \<in> ((\<lambda>x. a + x) ` S)" "(a + y) \<in> ((\<lambda>x. a + x) ` S)" |
|
471 |
by auto |
|
472 |
then have h1: "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) \<in> (\<lambda>x. a + x) ` S" |
|
473 |
using xy assms unfolding affine_def by auto |
|
474 |
have "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) = (u + v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)" |
|
475 |
by (simp add: algebra_simps) |
|
476 |
also have "\<dots> = a + (u *\<^sub>R x + v *\<^sub>R y)" |
|
477 |
using \<open>u + v = 1\<close> by auto |
|
478 |
ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) \<in> (\<lambda>x. a + x) ` S" |
|
479 |
using h1 by auto |
|
480 |
then have "u *\<^sub>R x + v *\<^sub>R y \<in> S" by auto |
|
481 |
} |
|
482 |
then show ?thesis unfolding affine_def by auto |
|
483 |
qed |
|
484 |
||
485 |
lemma affine_translation: |
|
486 |
"affine S \<longleftrightarrow> affine ((+) a ` S)" for a :: "'a::real_vector" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
487 |
by (metis affine_translation_aux translation_galois) |
71242 | 488 |
|
489 |
lemma parallel_is_affine: |
|
490 |
fixes S T :: "'a::real_vector set" |
|
491 |
assumes "affine S" "affine_parallel S T" |
|
492 |
shows "affine T" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
493 |
by (metis affine_parallel_def affine_translation assms) |
71242 | 494 |
|
495 |
lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s" |
|
496 |
unfolding subspace_def affine_def by auto |
|
497 |
||
498 |
lemma affine_hull_subset_span: "(affine hull s) \<subseteq> (span s)" |
|
499 |
by (metis hull_minimal span_superset subspace_imp_affine subspace_span) |
|
500 |
||
501 |
||
502 |
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Subspace parallel to an affine set\<close> |
|
503 |
||
504 |
lemma subspace_affine: "subspace S \<longleftrightarrow> affine S \<and> 0 \<in> S" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
505 |
by (metis add_cancel_right_left affine_alt diff_add_cancel mem_affine_3 scaleR_eq_0_iff subspace_def vector_space_assms(4)) |
71242 | 506 |
|
507 |
lemma affine_diffs_subspace: |
|
508 |
assumes "affine S" "a \<in> S" |
|
509 |
shows "subspace ((\<lambda>x. (-a)+x) ` S)" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
510 |
by (metis ab_left_minus affine_translation assms image_eqI subspace_affine) |
71242 | 511 |
|
512 |
lemma affine_diffs_subspace_subtract: |
|
513 |
"subspace ((\<lambda>x. x - a) ` S)" if "affine S" "a \<in> S" |
|
514 |
using that affine_diffs_subspace [of _ a] by simp |
|
515 |
||
516 |
lemma parallel_subspace_explicit: |
|
517 |
assumes "affine S" |
|
518 |
and "a \<in> S" |
|
519 |
assumes "L \<equiv> {y. \<exists>x \<in> S. (-a) + x = y}" |
|
520 |
shows "subspace L \<and> affine_parallel S L" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
521 |
by (smt (verit) Collect_cong ab_left_minus affine_parallel_def assms image_def mem_Collect_eq parallel_is_affine subspace_affine) |
71242 | 522 |
|
523 |
lemma parallel_subspace_aux: |
|
524 |
assumes "subspace A" |
|
525 |
and "subspace B" |
|
526 |
and "affine_parallel A B" |
|
527 |
shows "A \<supseteq> B" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
528 |
by (metis add.right_neutral affine_parallel_expl assms subsetI subspace_def) |
71242 | 529 |
|
530 |
lemma parallel_subspace: |
|
531 |
assumes "subspace A" |
|
532 |
and "subspace B" |
|
533 |
and "affine_parallel A B" |
|
534 |
shows "A = B" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
535 |
by (simp add: affine_parallel_commute assms parallel_subspace_aux subset_antisym) |
71242 | 536 |
|
537 |
lemma affine_parallel_subspace: |
|
538 |
assumes "affine S" "S \<noteq> {}" |
|
539 |
shows "\<exists>!L. subspace L \<and> affine_parallel S L" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
540 |
by (meson affine_parallel_assoc affine_parallel_commute assms equals0I parallel_subspace parallel_subspace_explicit) |
71242 | 541 |
|
542 |
||
543 |
subsection \<open>Affine Dependence\<close> |
|
544 |
||
545 |
text "Formalized by Lars Schewe." |
|
546 |
||
547 |
definition\<^marker>\<open>tag important\<close> affine_dependent :: "'a::real_vector set \<Rightarrow> bool" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
548 |
where "affine_dependent S \<longleftrightarrow> (\<exists>x\<in>S. x \<in> affine hull (S - {x}))" |
71242 | 549 |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
550 |
lemma affine_dependent_imp_dependent: "affine_dependent S \<Longrightarrow> dependent S" |
71242 | 551 |
unfolding affine_dependent_def dependent_def |
552 |
using affine_hull_subset_span by auto |
|
553 |
||
554 |
lemma affine_dependent_subset: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
555 |
"\<lbrakk>affine_dependent S; S \<subseteq> T\<rbrakk> \<Longrightarrow> affine_dependent T" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
556 |
using hull_mono [OF Diff_mono [OF _ subset_refl]] |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
557 |
by (smt (verit) affine_dependent_def subsetD) |
71242 | 558 |
|
559 |
lemma affine_independent_subset: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
560 |
shows "\<lbrakk>\<not> affine_dependent T; S \<subseteq> T\<rbrakk> \<Longrightarrow> \<not> affine_dependent S" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
561 |
by (metis affine_dependent_subset) |
71242 | 562 |
|
563 |
lemma affine_independent_Diff: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
564 |
"\<not> affine_dependent S \<Longrightarrow> \<not> affine_dependent(S - T)" |
71242 | 565 |
by (meson Diff_subset affine_dependent_subset) |
566 |
||
567 |
proposition affine_dependent_explicit: |
|
568 |
"affine_dependent p \<longleftrightarrow> |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
569 |
(\<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)" |
71242 | 570 |
proof - |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
571 |
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" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
572 |
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 |
71242 | 573 |
proof (intro exI conjI) |
574 |
have "x \<notin> S" |
|
575 |
using that by auto |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
576 |
then show "(\<Sum>v \<in> insert x S. if v = x then - 1 else U v) = 0" |
71242 | 577 |
using that by (simp add: sum_delta_notmem) |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
578 |
show "(\<Sum>w \<in> insert x S. (if w = x then - 1 else U w) *\<^sub>R w) = 0" |
71242 | 579 |
using that \<open>x \<notin> S\<close> by (simp add: if_smult sum_delta_notmem cong: if_cong) |
580 |
qed (use that in auto) |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
581 |
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" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
582 |
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 |
71242 | 583 |
proof (intro bexI exI conjI) |
584 |
have "S \<noteq> {v}" |
|
585 |
using that by auto |
|
586 |
then show "S - {v} \<noteq> {}" |
|
587 |
using that by auto |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
588 |
show "(\<Sum>x \<in> S - {v}. - (1 / U v) * U x) = 1" |
71242 | 589 |
unfolding sum_distrib_left[symmetric] sum_diff1[OF \<open>finite S\<close>] by (simp add: that) |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
590 |
show "(\<Sum>x\<in>S - {v}. (- (1 / U v) * U x) *\<^sub>R x) = v" |
71242 | 591 |
unfolding sum_distrib_left [symmetric] scaleR_scaleR[symmetric] |
592 |
scaleR_right.sum [symmetric] sum_diff1[OF \<open>finite S\<close>] |
|
593 |
using that by auto |
|
594 |
show "S - {v} \<subseteq> p - {v}" |
|
595 |
using that by auto |
|
596 |
qed (use that in auto) |
|
597 |
ultimately show ?thesis |
|
598 |
unfolding affine_dependent_def affine_hull_explicit by auto |
|
599 |
qed |
|
600 |
||
601 |
lemma affine_dependent_explicit_finite: |
|
602 |
fixes S :: "'a::real_vector set" |
|
603 |
assumes "finite S" |
|
604 |
shows "affine_dependent S \<longleftrightarrow> |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
605 |
(\<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)" |
71242 | 606 |
(is "?lhs = ?rhs") |
607 |
proof |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
608 |
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)" |
71242 | 609 |
by auto |
610 |
assume ?lhs |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
611 |
then obtain T U v where |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
612 |
"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" |
71242 | 613 |
unfolding affine_dependent_explicit by auto |
614 |
then show ?rhs |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
615 |
apply (rule_tac x="\<lambda>x. if x\<in>T then U x else 0" in exI) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
616 |
apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \<open>T\<subseteq>S\<close>]) |
71242 | 617 |
done |
618 |
next |
|
619 |
assume ?rhs |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
620 |
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" |
71242 | 621 |
by auto |
622 |
then show ?lhs unfolding affine_dependent_explicit |
|
623 |
using assms by auto |
|
624 |
qed |
|
625 |
||
626 |
lemma dependent_imp_affine_dependent: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
627 |
assumes "dependent {x - a| x . x \<in> S}" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
628 |
and "a \<notin> S" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
629 |
shows "affine_dependent (insert a S)" |
71242 | 630 |
proof - |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
631 |
from assms(1)[unfolded dependent_explicit] obtain S' U v |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
632 |
where S: "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" |
71242 | 633 |
by auto |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
634 |
define T where "T = (\<lambda>x. x + a) ` S'" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
635 |
have inj: "inj_on (\<lambda>x. x + a) S'" |
71242 | 636 |
unfolding inj_on_def by auto |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
637 |
have "0 \<notin> S'" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
638 |
using S(2) assms(2) unfolding subset_eq by auto |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
639 |
have fin: "finite T" and "T \<subseteq> S" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
640 |
unfolding T_def using S(1,2) by auto |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
641 |
then have "finite (insert a T)" and "insert a T \<subseteq> insert a S" |
71242 | 642 |
by auto |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
643 |
moreover have *: "\<And>P Q. (\<Sum>x\<in>T. (if x = a then P x else Q x)) = (\<Sum>x\<in>T. Q x)" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
644 |
by (smt (verit, best) \<open>T \<subseteq> S\<close> assms(2) subsetD sum.cong) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
645 |
have "(\<Sum>x\<in>insert a T. if x = a then - (\<Sum>x\<in>T. U (x - a)) else U (x - a)) = 0" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
646 |
by (smt (verit) \<open>T \<subseteq> S\<close> assms(2) fin insert_absorb insert_subset sum.insert sum_mono) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
647 |
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" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
648 |
using S(3,4) \<open>0\<notin>S'\<close> |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
649 |
by (rule_tac x="v + a" in bexI) (auto simp: T_def) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
650 |
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)" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
651 |
using \<open>a\<notin>S\<close> \<open>T\<subseteq>S\<close> by (auto intro!: sum.cong) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
652 |
have "(\<Sum>x\<in>T. U (x - a)) *\<^sub>R a = (\<Sum>v\<in>T. U (v - a) *\<^sub>R v)" |
71242 | 653 |
unfolding scaleR_left.sum |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
654 |
unfolding T_def and sum.reindex[OF inj] and o_def |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
655 |
using S(5) |
71242 | 656 |
by (auto simp: sum.distrib scaleR_right_distrib) |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
657 |
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" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
658 |
unfolding sum_clauses(2)[OF fin] using \<open>a\<notin>S\<close> \<open>T\<subseteq>S\<close> by (auto simp: *) |
71242 | 659 |
ultimately show ?thesis |
660 |
unfolding affine_dependent_explicit |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
661 |
by (force intro!: exI[where x="insert a T"]) |
71242 | 662 |
qed |
663 |
||
664 |
lemma affine_dependent_biggerset: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
665 |
fixes S :: "'a::euclidean_space set" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
666 |
assumes "finite S" "card S \<ge> DIM('a) + 2" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
667 |
shows "affine_dependent S" |
71242 | 668 |
proof - |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
669 |
have "S \<noteq> {}" using assms by auto |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
670 |
then obtain a where "a\<in>S" by auto |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
671 |
have *: "{x - a |x. x \<in> S - {a}} = (\<lambda>x. x - a) ` (S - {a})" |
71242 | 672 |
by auto |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
673 |
have "card {x - a |x. x \<in> S - {a}} = card (S - {a})" |
71242 | 674 |
unfolding * by (simp add: card_image inj_on_def) |
675 |
also have "\<dots> > DIM('a)" using assms(2) |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
676 |
unfolding card_Diff_singleton[OF \<open>a\<in>S\<close>] by auto |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
677 |
finally have "affine_dependent (insert a (S - {a}))" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
678 |
using dependent_biggerset dependent_imp_affine_dependent by blast |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
679 |
then show ?thesis |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
680 |
by (simp add: \<open>a \<in> S\<close> insert_absorb) |
71242 | 681 |
qed |
682 |
||
683 |
lemma affine_dependent_biggerset_general: |
|
684 |
assumes "finite (S :: 'a::euclidean_space set)" |
|
685 |
and "card S \<ge> dim S + 2" |
|
686 |
shows "affine_dependent S" |
|
687 |
proof - |
|
688 |
from assms(2) have "S \<noteq> {}" by auto |
|
689 |
then obtain a where "a\<in>S" by auto |
|
690 |
have *: "{x - a |x. x \<in> S - {a}} = (\<lambda>x. x - a) ` (S - {a})" |
|
691 |
by auto |
|
692 |
have **: "card {x - a |x. x \<in> S - {a}} = card (S - {a})" |
|
693 |
by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def) |
|
694 |
have "dim {x - a |x. x \<in> S - {a}} \<le> dim S" |
|
695 |
using \<open>a\<in>S\<close> by (auto simp: span_base span_diff intro: subset_le_dim) |
|
696 |
also have "\<dots> < dim S + 1" by auto |
|
697 |
also have "\<dots> \<le> card (S - {a})" |
|
74224
e04ec2b9ed97
some fixes connected with card_Diff_singleton
paulson <lp15@cam.ac.uk>
parents:
73372
diff
changeset
|
698 |
using assms card_Diff_singleton[OF \<open>a\<in>S\<close>] by auto |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
699 |
finally have "affine_dependent (insert a (S - {a}))" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
700 |
by (smt (verit) Collect_cong dependent_imp_affine_dependent dependent_biggerset_general ** Diff_iff insertCI) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
701 |
then show ?thesis |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
702 |
by (simp add: \<open>a \<in> S\<close> insert_absorb) |
71242 | 703 |
qed |
704 |
||
705 |
||
706 |
subsection\<^marker>\<open>tag unimportant\<close> \<open>Some Properties of Affine Dependent Sets\<close> |
|
707 |
||
708 |
lemma affine_independent_0 [simp]: "\<not> affine_dependent {}" |
|
709 |
by (simp add: affine_dependent_def) |
|
710 |
||
711 |
lemma affine_independent_1 [simp]: "\<not> affine_dependent {a}" |
|
712 |
by (simp add: affine_dependent_def) |
|
713 |
||
714 |
lemma affine_independent_2 [simp]: "\<not> affine_dependent {a,b}" |
|
715 |
by (simp add: affine_dependent_def insert_Diff_if hull_same) |
|
716 |
||
717 |
lemma affine_hull_translation: "affine hull ((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (affine hull S)" |
|
718 |
proof - |
|
719 |
have "affine ((\<lambda>x. a + x) ` (affine hull S))" |
|
720 |
using affine_translation affine_affine_hull by blast |
|
721 |
moreover have "(\<lambda>x. a + x) ` S \<subseteq> (\<lambda>x. a + x) ` (affine hull S)" |
|
722 |
using hull_subset[of S] by auto |
|
723 |
ultimately have h1: "affine hull ((\<lambda>x. a + x) ` S) \<subseteq> (\<lambda>x. a + x) ` (affine hull S)" |
|
724 |
by (metis hull_minimal) |
|
725 |
have "affine((\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) ` S)))" |
|
726 |
using affine_translation affine_affine_hull by blast |
|
727 |
moreover have "(\<lambda>x. -a + x) ` (\<lambda>x. a + x) ` S \<subseteq> (\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) ` S))" |
|
728 |
using hull_subset[of "(\<lambda>x. a + x) ` S"] by auto |
|
729 |
moreover have "S = (\<lambda>x. -a + x) ` (\<lambda>x. a + x) ` S" |
|
730 |
using translation_assoc[of "-a" a] by auto |
|
731 |
ultimately have "(\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) ` S)) >= (affine hull S)" |
|
732 |
by (metis hull_minimal) |
|
733 |
then have "affine hull ((\<lambda>x. a + x) ` S) >= (\<lambda>x. a + x) ` (affine hull S)" |
|
734 |
by auto |
|
735 |
then show ?thesis using h1 by auto |
|
736 |
qed |
|
737 |
||
738 |
lemma affine_dependent_translation: |
|
739 |
assumes "affine_dependent S" |
|
740 |
shows "affine_dependent ((\<lambda>x. a + x) ` S)" |
|
741 |
proof - |
|
742 |
obtain x where x: "x \<in> S \<and> x \<in> affine hull (S - {x})" |
|
743 |
using assms affine_dependent_def by auto |
|
744 |
have "(+) a ` (S - {x}) = (+) a ` S - {a + x}" |
|
745 |
by auto |
|
746 |
then have "a + x \<in> affine hull ((\<lambda>x. a + x) ` S - {a + x})" |
|
747 |
using affine_hull_translation[of a "S - {x}"] x by auto |
|
748 |
moreover have "a + x \<in> (\<lambda>x. a + x) ` S" |
|
749 |
using x by auto |
|
750 |
ultimately show ?thesis |
|
751 |
unfolding affine_dependent_def by auto |
|
752 |
qed |
|
753 |
||
754 |
lemma affine_dependent_translation_eq: |
|
755 |
"affine_dependent S \<longleftrightarrow> affine_dependent ((\<lambda>x. a + x) ` S)" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
756 |
by (metis affine_dependent_translation translation_galois) |
71242 | 757 |
|
758 |
lemma affine_hull_0_dependent: |
|
759 |
assumes "0 \<in> affine hull S" |
|
760 |
shows "dependent S" |
|
761 |
proof - |
|
762 |
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" |
|
763 |
using assms affine_hull_explicit[of S] by auto |
|
764 |
then have "\<exists>v\<in>s. u v \<noteq> 0" by auto |
|
765 |
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)" |
|
766 |
using s_u by auto |
|
767 |
then show ?thesis |
|
768 |
unfolding dependent_explicit[of S] by auto |
|
769 |
qed |
|
770 |
||
771 |
lemma affine_dependent_imp_dependent2: |
|
772 |
assumes "affine_dependent (insert 0 S)" |
|
773 |
shows "dependent S" |
|
774 |
proof - |
|
775 |
obtain x where x: "x \<in> insert 0 S \<and> x \<in> affine hull (insert 0 S - {x})" |
|
776 |
using affine_dependent_def[of "(insert 0 S)"] assms by blast |
|
777 |
then have "x \<in> span (insert 0 S - {x})" |
|
778 |
using affine_hull_subset_span by auto |
|
779 |
moreover have "span (insert 0 S - {x}) = span (S - {x})" |
|
780 |
using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto |
|
781 |
ultimately have "x \<in> span (S - {x})" by auto |
|
782 |
then have "x \<noteq> 0 \<Longrightarrow> dependent S" |
|
783 |
using x dependent_def by auto |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
784 |
moreover have "dependent S" if "x = 0" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
785 |
by (metis that affine_hull_0_dependent Diff_insert_absorb dependent_zero x) |
71242 | 786 |
ultimately show ?thesis by auto |
787 |
qed |
|
788 |
||
789 |
lemma affine_dependent_iff_dependent: |
|
790 |
assumes "a \<notin> S" |
|
791 |
shows "affine_dependent (insert a S) \<longleftrightarrow> dependent ((\<lambda>x. -a + x) ` S)" |
|
792 |
proof - |
|
793 |
have "((+) (- a) ` S) = {x - a| x . x \<in> S}" by auto |
|
794 |
then show ?thesis |
|
795 |
using affine_dependent_translation_eq[of "(insert a S)" "-a"] |
|
796 |
affine_dependent_imp_dependent2 assms |
|
797 |
dependent_imp_affine_dependent[of a S] |
|
798 |
by (auto simp del: uminus_add_conv_diff) |
|
799 |
qed |
|
800 |
||
801 |
lemma affine_dependent_iff_dependent2: |
|
802 |
assumes "a \<in> S" |
|
803 |
shows "affine_dependent S \<longleftrightarrow> dependent ((\<lambda>x. -a + x) ` (S-{a}))" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
804 |
by (metis Diff_iff affine_dependent_iff_dependent assms insert_Diff singletonI) |
71242 | 805 |
|
806 |
lemma affine_hull_insert_span_gen: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
807 |
"affine hull (insert a S) = (\<lambda>x. a + x) ` span ((\<lambda>x. - a + x) ` S)" |
71242 | 808 |
proof - |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
809 |
have h1: "{x - a |x. x \<in> S} = ((\<lambda>x. -a+x) ` S)" |
71242 | 810 |
by auto |
811 |
{ |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
812 |
assume "a \<notin> S" |
71242 | 813 |
then have ?thesis |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
814 |
using affine_hull_insert_span[of a S] h1 by auto |
71242 | 815 |
} |
816 |
moreover |
|
817 |
{ |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
818 |
assume a1: "a \<in> S" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
819 |
then have "insert 0 ((\<lambda>x. -a+x) ` (S - {a})) = (\<lambda>x. -a+x) ` S" |
71242 | 820 |
by auto |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
821 |
then have "span ((\<lambda>x. -a+x) ` (S - {a})) = span ((\<lambda>x. -a+x) ` S)" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
822 |
using span_insert_0[of "(+) (- a) ` (S - {a})"] |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
823 |
by presburger |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
824 |
moreover have "{x - a |x. x \<in> (S - {a})} = ((\<lambda>x. -a+x) ` (S - {a}))" |
71242 | 825 |
by auto |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
826 |
moreover have "insert a (S - {a}) = insert a S" |
71242 | 827 |
by auto |
828 |
ultimately have ?thesis |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
829 |
using affine_hull_insert_span[of "a" "S-{a}"] by auto |
71242 | 830 |
} |
831 |
ultimately show ?thesis by auto |
|
832 |
qed |
|
833 |
||
834 |
lemma affine_hull_span2: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
835 |
assumes "a \<in> S" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
836 |
shows "affine hull S = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` (S-{a}))" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
837 |
by (metis affine_hull_insert_span_gen assms insert_Diff) |
71242 | 838 |
|
839 |
lemma affine_hull_span_gen: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
840 |
assumes "a \<in> affine hull S" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
841 |
shows "affine hull S = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` S)" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
842 |
by (metis affine_hull_insert_span_gen assms hull_redundant) |
71242 | 843 |
|
844 |
lemma affine_hull_span_0: |
|
845 |
assumes "0 \<in> affine hull S" |
|
846 |
shows "affine hull S = span S" |
|
847 |
using affine_hull_span_gen[of "0" S] assms by auto |
|
848 |
||
849 |
lemma extend_to_affine_basis_nonempty: |
|
72492 | 850 |
fixes S V :: "'n::real_vector set" |
71242 | 851 |
assumes "\<not> affine_dependent S" "S \<subseteq> V" "S \<noteq> {}" |
852 |
shows "\<exists>T. \<not> affine_dependent T \<and> S \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V" |
|
853 |
proof - |
|
854 |
obtain a where a: "a \<in> S" |
|
855 |
using assms by auto |
|
856 |
then have h0: "independent ((\<lambda>x. -a + x) ` (S-{a}))" |
|
857 |
using affine_dependent_iff_dependent2 assms by auto |
|
858 |
obtain B where B: |
|
859 |
"(\<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" |
|
860 |
using assms |
|
861 |
by (blast intro: maximal_independent_subset_extend[OF _ h0, of "(\<lambda>x. -a + x) ` V"]) |
|
862 |
define T where "T = (\<lambda>x. a+x) ` insert 0 B" |
|
863 |
then have "T = insert a ((\<lambda>x. a+x) ` B)" |
|
864 |
by auto |
|
865 |
then have "affine hull T = (\<lambda>x. a+x) ` span B" |
|
866 |
using affine_hull_insert_span_gen[of a "((\<lambda>x. a+x) ` B)"] translation_assoc[of "-a" a B] |
|
867 |
by auto |
|
868 |
then have "V \<subseteq> affine hull T" |
|
869 |
using B assms translation_inverse_subset[of a V "span B"] |
|
870 |
by auto |
|
871 |
moreover have "T \<subseteq> V" |
|
872 |
using T_def B a assms by auto |
|
873 |
ultimately have "affine hull T = affine hull V" |
|
874 |
by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono) |
|
875 |
moreover have "S \<subseteq> T" |
|
876 |
using T_def B translation_inverse_subset[of a "S-{a}" B] |
|
877 |
by auto |
|
878 |
moreover have "\<not> affine_dependent T" |
|
879 |
using T_def affine_dependent_translation_eq[of "insert 0 B"] |
|
880 |
affine_dependent_imp_dependent2 B |
|
881 |
by auto |
|
882 |
ultimately show ?thesis using \<open>T \<subseteq> V\<close> by auto |
|
883 |
qed |
|
884 |
||
885 |
lemma affine_basis_exists: |
|
72492 | 886 |
fixes V :: "'n::real_vector set" |
71242 | 887 |
shows "\<exists>B. B \<subseteq> V \<and> \<not> affine_dependent B \<and> affine hull V = affine hull B" |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
888 |
by (metis affine_dependent_def affine_independent_1 empty_subsetI extend_to_affine_basis_nonempty insert_subset order_refl) |
71242 | 889 |
|
890 |
proposition extend_to_affine_basis: |
|
72492 | 891 |
fixes S V :: "'n::real_vector set" |
71242 | 892 |
assumes "\<not> affine_dependent S" "S \<subseteq> V" |
893 |
obtains T where "\<not> affine_dependent T" "S \<subseteq> T" "T \<subseteq> V" "affine hull T = affine hull V" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
894 |
by (metis affine_basis_exists assms(1) assms(2) bot.extremum extend_to_affine_basis_nonempty) |
71242 | 895 |
|
896 |
||
897 |
subsection \<open>Affine Dimension of a Set\<close> |
|
898 |
||
899 |
definition\<^marker>\<open>tag important\<close> aff_dim :: "('a::euclidean_space) set \<Rightarrow> int" |
|
900 |
where "aff_dim V = |
|
901 |
(SOME d :: int. |
|
902 |
\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)" |
|
903 |
||
904 |
lemma aff_dim_basis_exists: |
|
905 |
fixes V :: "('n::euclidean_space) set" |
|
906 |
shows "\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1" |
|
907 |
proof - |
|
908 |
obtain B where "\<not> affine_dependent B \<and> affine hull B = affine hull V" |
|
909 |
using affine_basis_exists[of V] by auto |
|
910 |
then show ?thesis |
|
911 |
unfolding aff_dim_def |
|
912 |
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"] |
|
913 |
apply auto |
|
914 |
apply (rule exI[of _ "int (card B) - (1 :: int)"]) |
|
915 |
apply (rule exI[of _ "B"], auto) |
|
916 |
done |
|
917 |
qed |
|
918 |
||
919 |
lemma affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}" |
|
920 |
by (metis affine_empty subset_empty subset_hull) |
|
921 |
||
922 |
lemma empty_eq_affine_hull[simp]: "{} = affine hull S \<longleftrightarrow> S = {}" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
923 |
by (metis affine_hull_eq_empty) |
71242 | 924 |
|
925 |
lemma aff_dim_parallel_subspace_aux: |
|
926 |
fixes B :: "'n::euclidean_space set" |
|
927 |
assumes "\<not> affine_dependent B" "a \<in> B" |
|
928 |
shows "finite B \<and> ((card B) - 1 = dim (span ((\<lambda>x. -a+x) ` (B-{a}))))" |
|
929 |
proof - |
|
930 |
have "independent ((\<lambda>x. -a + x) ` (B-{a}))" |
|
931 |
using affine_dependent_iff_dependent2 assms by auto |
|
932 |
then have fin: "dim (span ((\<lambda>x. -a+x) ` (B-{a}))) = card ((\<lambda>x. -a + x) ` (B-{a}))" |
|
933 |
"finite ((\<lambda>x. -a + x) ` (B - {a}))" |
|
934 |
using indep_card_eq_dim_span[of "(\<lambda>x. -a+x) ` (B-{a})"] by auto |
|
935 |
show ?thesis |
|
936 |
proof (cases "(\<lambda>x. -a + x) ` (B - {a}) = {}") |
|
937 |
case True |
|
938 |
have "B = insert a ((\<lambda>x. a + x) ` (\<lambda>x. -a + x) ` (B - {a}))" |
|
939 |
using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto |
|
940 |
then have "B = {a}" using True by auto |
|
941 |
then show ?thesis using assms fin by auto |
|
942 |
next |
|
943 |
case False |
|
944 |
then have "card ((\<lambda>x. -a + x) ` (B - {a})) > 0" |
|
945 |
using fin by auto |
|
946 |
moreover have h1: "card ((\<lambda>x. -a + x) ` (B-{a})) = card (B-{a})" |
|
947 |
by (rule card_image) (use translate_inj_on in blast) |
|
948 |
ultimately have "card (B-{a}) > 0" by auto |
|
949 |
then have *: "finite (B - {a})" |
|
950 |
using card_gt_0_iff[of "(B - {a})"] by auto |
|
951 |
then have "card (B - {a}) = card B - 1" |
|
952 |
using card_Diff_singleton assms by auto |
|
953 |
with * show ?thesis using fin h1 by auto |
|
954 |
qed |
|
955 |
qed |
|
956 |
||
957 |
lemma aff_dim_parallel_subspace: |
|
958 |
fixes V L :: "'n::euclidean_space set" |
|
959 |
assumes "V \<noteq> {}" |
|
960 |
and "subspace L" |
|
961 |
and "affine_parallel (affine hull V) L" |
|
962 |
shows "aff_dim V = int (dim L)" |
|
963 |
proof - |
|
964 |
obtain B where |
|
965 |
B: "affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> int (card B) = aff_dim V + 1" |
|
966 |
using aff_dim_basis_exists by auto |
|
967 |
then have "B \<noteq> {}" |
|
968 |
using assms B |
|
969 |
by auto |
|
970 |
then obtain a where a: "a \<in> B" by auto |
|
971 |
define Lb where "Lb = span ((\<lambda>x. -a+x) ` (B-{a}))" |
|
972 |
moreover have "affine_parallel (affine hull B) Lb" |
|
973 |
using Lb_def B assms affine_hull_span2[of a B] a |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
974 |
affine_parallel_commute[of "Lb" "(affine hull B)"] |
71242 | 975 |
unfolding affine_parallel_def |
976 |
by auto |
|
977 |
moreover have "subspace Lb" |
|
978 |
using Lb_def subspace_span by auto |
|
979 |
moreover have "affine hull B \<noteq> {}" |
|
980 |
using assms B by auto |
|
981 |
ultimately have "L = Lb" |
|
982 |
using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B |
|
983 |
by auto |
|
984 |
then have "dim L = dim Lb" |
|
985 |
by auto |
|
986 |
moreover have "card B - 1 = dim Lb" and "finite B" |
|
987 |
using Lb_def aff_dim_parallel_subspace_aux a B by auto |
|
988 |
ultimately show ?thesis |
|
989 |
using B \<open>B \<noteq> {}\<close> card_gt_0_iff[of B] by auto |
|
990 |
qed |
|
991 |
||
992 |
lemma aff_independent_finite: |
|
993 |
fixes B :: "'n::euclidean_space set" |
|
994 |
assumes "\<not> affine_dependent B" |
|
995 |
shows "finite B" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
996 |
using aff_dim_parallel_subspace_aux assms finite.simps by fastforce |
71242 | 997 |
|
998 |
||
999 |
lemma aff_dim_empty: |
|
1000 |
fixes S :: "'n::euclidean_space set" |
|
1001 |
shows "S = {} \<longleftrightarrow> aff_dim S = -1" |
|
1002 |
proof - |
|
1003 |
obtain B where *: "affine hull B = affine hull S" |
|
1004 |
and "\<not> affine_dependent B" |
|
1005 |
and "int (card B) = aff_dim S + 1" |
|
1006 |
using aff_dim_basis_exists by auto |
|
1007 |
moreover |
|
1008 |
from * have "S = {} \<longleftrightarrow> B = {}" |
|
1009 |
by auto |
|
1010 |
ultimately show ?thesis |
|
1011 |
using aff_independent_finite[of B] card_gt_0_iff[of B] by auto |
|
1012 |
qed |
|
1013 |
||
1014 |
lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1015 |
using aff_dim_empty by blast |
71242 | 1016 |
|
1017 |
lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S" |
|
1018 |
unfolding aff_dim_def using hull_hull[of _ S] by auto |
|
1019 |
||
1020 |
lemma aff_dim_affine_hull2: |
|
1021 |
assumes "affine hull S = affine hull T" |
|
1022 |
shows "aff_dim S = aff_dim T" |
|
1023 |
unfolding aff_dim_def using assms by auto |
|
1024 |
||
1025 |
lemma aff_dim_unique: |
|
1026 |
fixes B V :: "'n::euclidean_space set" |
|
1027 |
assumes "affine hull B = affine hull V \<and> \<not> affine_dependent B" |
|
1028 |
shows "of_nat (card B) = aff_dim V + 1" |
|
1029 |
proof (cases "B = {}") |
|
1030 |
case True |
|
1031 |
then have "V = {}" |
|
1032 |
using assms |
|
1033 |
by auto |
|
1034 |
then have "aff_dim V = (-1::int)" |
|
1035 |
using aff_dim_empty by auto |
|
1036 |
then show ?thesis |
|
1037 |
using \<open>B = {}\<close> by auto |
|
1038 |
next |
|
1039 |
case False |
|
1040 |
then obtain a where a: "a \<in> B" by auto |
|
1041 |
define Lb where "Lb = span ((\<lambda>x. -a+x) ` (B-{a}))" |
|
1042 |
have "affine_parallel (affine hull B) Lb" |
|
1043 |
using Lb_def affine_hull_span2[of a B] a |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1044 |
affine_parallel_commute[of "Lb" "(affine hull B)"] |
71242 | 1045 |
unfolding affine_parallel_def by auto |
1046 |
moreover have "subspace Lb" |
|
1047 |
using Lb_def subspace_span by auto |
|
1048 |
ultimately have "aff_dim B = int(dim Lb)" |
|
1049 |
using aff_dim_parallel_subspace[of B Lb] \<open>B \<noteq> {}\<close> by auto |
|
1050 |
moreover have "(card B) - 1 = dim Lb" "finite B" |
|
1051 |
using Lb_def aff_dim_parallel_subspace_aux a assms by auto |
|
1052 |
ultimately have "of_nat (card B) = aff_dim B + 1" |
|
1053 |
using \<open>B \<noteq> {}\<close> card_gt_0_iff[of B] by auto |
|
1054 |
then show ?thesis |
|
1055 |
using aff_dim_affine_hull2 assms by auto |
|
1056 |
qed |
|
1057 |
||
1058 |
lemma aff_dim_affine_independent: |
|
1059 |
fixes B :: "'n::euclidean_space set" |
|
1060 |
assumes "\<not> affine_dependent B" |
|
1061 |
shows "of_nat (card B) = aff_dim B + 1" |
|
1062 |
using aff_dim_unique[of B B] assms by auto |
|
1063 |
||
1064 |
lemma affine_independent_iff_card: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1065 |
fixes S :: "'a::euclidean_space set" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1066 |
shows "\<not> affine_dependent S \<longleftrightarrow> finite S \<and> aff_dim S = int(card S) - 1" (is "?lhs = ?rhs") |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1067 |
proof |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1068 |
show "?lhs \<Longrightarrow> ?rhs" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1069 |
by (simp add: aff_dim_affine_independent aff_independent_finite) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1070 |
show "?rhs \<Longrightarrow> ?lhs" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1071 |
by (metis of_nat_eq_iff affine_basis_exists aff_dim_unique card_subset_eq diff_add_cancel) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1072 |
qed |
71242 | 1073 |
|
1074 |
lemma aff_dim_sing [simp]: |
|
1075 |
fixes a :: "'n::euclidean_space" |
|
1076 |
shows "aff_dim {a} = 0" |
|
1077 |
using aff_dim_affine_independent[of "{a}"] affine_independent_1 by auto |
|
1078 |
||
72492 | 1079 |
lemma aff_dim_2 [simp]: |
1080 |
fixes a :: "'n::euclidean_space" |
|
1081 |
shows "aff_dim {a,b} = (if a = b then 0 else 1)" |
|
71242 | 1082 |
proof (clarsimp) |
1083 |
assume "a \<noteq> b" |
|
1084 |
then have "aff_dim{a,b} = card{a,b} - 1" |
|
1085 |
using affine_independent_2 [of a b] aff_dim_affine_independent by fastforce |
|
1086 |
also have "\<dots> = 1" |
|
1087 |
using \<open>a \<noteq> b\<close> by simp |
|
1088 |
finally show "aff_dim {a, b} = 1" . |
|
1089 |
qed |
|
1090 |
||
1091 |
lemma aff_dim_inner_basis_exists: |
|
1092 |
fixes V :: "('n::euclidean_space) set" |
|
1093 |
shows "\<exists>B. B \<subseteq> V \<and> affine hull B = affine hull V \<and> |
|
1094 |
\<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1095 |
by (metis aff_dim_unique affine_basis_exists) |
71242 | 1096 |
|
1097 |
lemma aff_dim_le_card: |
|
1098 |
fixes V :: "'n::euclidean_space set" |
|
1099 |
assumes "finite V" |
|
1100 |
shows "aff_dim V \<le> of_nat (card V) - 1" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1101 |
by (metis aff_dim_inner_basis_exists assms card_mono le_diff_eq of_nat_le_iff) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1102 |
|
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1103 |
lemma aff_dim_parallel_le: |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1104 |
fixes S T :: "'n::euclidean_space set" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1105 |
assumes "affine_parallel (affine hull S) (affine hull T)" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1106 |
shows "aff_dim S \<le> aff_dim T" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1107 |
proof (cases "S={} \<or> T={}") |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1108 |
case True |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1109 |
then show ?thesis |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1110 |
by (smt (verit, best) aff_dim_affine_hull2 affine_hull_empty affine_parallel_def assms empty_is_image) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1111 |
next |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1112 |
case False |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1113 |
then obtain L where L: "subspace L" "affine_parallel (affine hull T) L" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1114 |
by (metis affine_affine_hull affine_hull_eq_empty affine_parallel_subspace) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1115 |
with False show ?thesis |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1116 |
by (metis aff_dim_parallel_subspace affine_parallel_assoc assms dual_order.refl) |
71242 | 1117 |
qed |
1118 |
||
1119 |
lemma aff_dim_parallel_eq: |
|
1120 |
fixes S T :: "'n::euclidean_space set" |
|
1121 |
assumes "affine_parallel (affine hull S) (affine hull T)" |
|
1122 |
shows "aff_dim S = aff_dim T" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1123 |
by (smt (verit, del_insts) aff_dim_parallel_le affine_parallel_commute assms) |
71242 | 1124 |
|
1125 |
lemma aff_dim_translation_eq: |
|
1126 |
"aff_dim ((+) a ` S) = aff_dim S" for a :: "'n::euclidean_space" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1127 |
by (metis aff_dim_parallel_eq affine_hull_translation affine_parallel_def) |
71242 | 1128 |
|
1129 |
lemma aff_dim_translation_eq_subtract: |
|
1130 |
"aff_dim ((\<lambda>x. x - a) ` S) = aff_dim S" for a :: "'n::euclidean_space" |
|
1131 |
using aff_dim_translation_eq [of "- a"] by (simp cong: image_cong_simp) |
|
1132 |
||
1133 |
lemma aff_dim_affine: |
|
1134 |
fixes S L :: "'n::euclidean_space set" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1135 |
assumes "affine S" "subspace L" "affine_parallel S L" "S \<noteq> {}" |
71242 | 1136 |
shows "aff_dim S = int (dim L)" |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1137 |
by (simp add: aff_dim_parallel_subspace assms hull_same) |
71242 | 1138 |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1139 |
lemma dim_affine_hull [simp]: |
71242 | 1140 |
fixes S :: "'n::euclidean_space set" |
1141 |
shows "dim (affine hull S) = dim S" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1142 |
by (metis affine_hull_subset_span dim_eq_span dim_mono hull_subset span_eq_dim) |
71242 | 1143 |
|
1144 |
lemma aff_dim_subspace: |
|
1145 |
fixes S :: "'n::euclidean_space set" |
|
1146 |
assumes "subspace S" |
|
1147 |
shows "aff_dim S = int (dim S)" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1148 |
by (metis aff_dim_affine affine_parallel_subspace assms empty_iff parallel_subspace subspace_affine) |
71242 | 1149 |
|
1150 |
lemma aff_dim_zero: |
|
1151 |
fixes S :: "'n::euclidean_space set" |
|
1152 |
assumes "0 \<in> affine hull S" |
|
1153 |
shows "aff_dim S = int (dim S)" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1154 |
by (metis aff_dim_affine_hull aff_dim_subspace affine_hull_span_0 assms dim_span subspace_span) |
71242 | 1155 |
|
1156 |
lemma aff_dim_eq_dim: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1157 |
fixes S :: "'n::euclidean_space set" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1158 |
assumes "a \<in> affine hull S" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1159 |
shows "aff_dim S = int (dim ((+) (- a) ` S))" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1160 |
by (metis ab_left_minus aff_dim_translation_eq aff_dim_zero affine_hull_translation image_eqI assms) |
71242 | 1161 |
|
1162 |
lemma aff_dim_eq_dim_subtract: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1163 |
fixes S :: "'n::euclidean_space set" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1164 |
assumes "a \<in> affine hull S" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1165 |
shows "aff_dim S = int (dim ((\<lambda>x. x - a) ` S))" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1166 |
using aff_dim_eq_dim assms by auto |
71242 | 1167 |
|
1168 |
lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1169 |
by (simp add: aff_dim_subspace) |
71242 | 1170 |
|
1171 |
lemma aff_dim_geq: |
|
1172 |
fixes V :: "'n::euclidean_space set" |
|
1173 |
shows "aff_dim V \<ge> -1" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1174 |
by (metis add_le_cancel_right aff_dim_basis_exists diff_self of_nat_0_le_iff uminus_add_conv_diff) |
71242 | 1175 |
|
1176 |
lemma aff_dim_negative_iff [simp]: |
|
1177 |
fixes S :: "'n::euclidean_space set" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1178 |
shows "aff_dim S < 0 \<longleftrightarrow> S = {}" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1179 |
by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq) |
71242 | 1180 |
|
1181 |
lemma aff_lowdim_subset_hyperplane: |
|
1182 |
fixes S :: "'a::euclidean_space set" |
|
1183 |
assumes "aff_dim S < DIM('a)" |
|
1184 |
obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x = b}" |
|
1185 |
proof (cases "S={}") |
|
1186 |
case True |
|
1187 |
moreover |
|
1188 |
have "(SOME b. b \<in> Basis) \<noteq> 0" |
|
1189 |
by (metis norm_some_Basis norm_zero zero_neq_one) |
|
1190 |
ultimately show ?thesis |
|
1191 |
using that by blast |
|
1192 |
next |
|
1193 |
case False |
|
1194 |
then obtain c S' where "c \<notin> S'" "S = insert c S'" |
|
1195 |
by (meson equals0I mk_disjoint_insert) |
|
1196 |
have "dim ((+) (-c) ` S) < DIM('a)" |
|
1197 |
by (metis \<open>S = insert c S'\<close> aff_dim_eq_dim assms hull_inc insertI1 of_nat_less_imp_less) |
|
1198 |
then obtain a where "a \<noteq> 0" "span ((+) (-c) ` S) \<subseteq> {x. a \<bullet> x = 0}" |
|
1199 |
using lowdim_subset_hyperplane by blast |
|
1200 |
moreover |
|
1201 |
have "a \<bullet> w = a \<bullet> c" if "span ((+) (- c) ` S) \<subseteq> {x. a \<bullet> x = 0}" "w \<in> S" for w |
|
1202 |
proof - |
|
1203 |
have "w-c \<in> span ((+) (- c) ` S)" |
|
1204 |
by (simp add: span_base \<open>w \<in> S\<close>) |
|
1205 |
with that have "w-c \<in> {x. a \<bullet> x = 0}" |
|
1206 |
by blast |
|
1207 |
then show ?thesis |
|
1208 |
by (auto simp: algebra_simps) |
|
1209 |
qed |
|
1210 |
ultimately have "S \<subseteq> {x. a \<bullet> x = a \<bullet> c}" |
|
1211 |
by blast |
|
1212 |
then show ?thesis |
|
1213 |
by (rule that[OF \<open>a \<noteq> 0\<close>]) |
|
1214 |
qed |
|
1215 |
||
1216 |
lemma affine_independent_card_dim_diffs: |
|
1217 |
fixes S :: "'a :: euclidean_space set" |
|
1218 |
assumes "\<not> affine_dependent S" "a \<in> S" |
|
72567 | 1219 |
shows "card S = dim ((\<lambda>x. x - a) ` S) + 1" |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1220 |
using aff_dim_affine_independent aff_dim_eq_dim_subtract assms hull_subset by fastforce |
71242 | 1221 |
|
1222 |
lemma independent_card_le_aff_dim: |
|
1223 |
fixes B :: "'n::euclidean_space set" |
|
1224 |
assumes "B \<subseteq> V" |
|
1225 |
assumes "\<not> affine_dependent B" |
|
1226 |
shows "int (card B) \<le> aff_dim V + 1" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1227 |
by (metis aff_dim_unique aff_independent_finite assms card_mono extend_to_affine_basis of_nat_mono) |
71242 | 1228 |
|
1229 |
lemma aff_dim_subset: |
|
1230 |
fixes S T :: "'n::euclidean_space set" |
|
1231 |
assumes "S \<subseteq> T" |
|
1232 |
shows "aff_dim S \<le> aff_dim T" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1233 |
by (metis add_le_cancel_right aff_dim_inner_basis_exists assms dual_order.trans independent_card_le_aff_dim) |
71242 | 1234 |
|
1235 |
lemma aff_dim_le_DIM: |
|
1236 |
fixes S :: "'n::euclidean_space set" |
|
1237 |
shows "aff_dim S \<le> int (DIM('n))" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1238 |
by (metis aff_dim_UNIV aff_dim_subset top_greatest) |
71242 | 1239 |
|
1240 |
lemma affine_dim_equal: |
|
1241 |
fixes S :: "'n::euclidean_space set" |
|
1242 |
assumes "affine S" "affine T" "S \<noteq> {}" "S \<subseteq> T" "aff_dim S = aff_dim T" |
|
1243 |
shows "S = T" |
|
1244 |
proof - |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1245 |
obtain a where "a \<in> S" "a \<in> T" "T \<noteq> {}" using assms by auto |
71242 | 1246 |
define LS where "LS = {y. \<exists>x \<in> S. (-a) + x = y}" |
1247 |
then have ls: "subspace LS" "affine_parallel S LS" |
|
1248 |
using assms parallel_subspace_explicit[of S a LS] \<open>a \<in> S\<close> by auto |
|
1249 |
then have h1: "int(dim LS) = aff_dim S" |
|
1250 |
using assms aff_dim_affine[of S LS] by auto |
|
1251 |
define LT where "LT = {y. \<exists>x \<in> T. (-a) + x = y}" |
|
1252 |
then have lt: "subspace LT \<and> affine_parallel T LT" |
|
1253 |
using assms parallel_subspace_explicit[of T a LT] \<open>a \<in> T\<close> by auto |
|
1254 |
then have "dim LS = dim LT" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1255 |
using assms aff_dim_affine[of T LT] \<open>T \<noteq> {}\<close> h1 by auto |
71242 | 1256 |
moreover have "LS \<le> LT" |
1257 |
using LS_def LT_def assms by auto |
|
1258 |
ultimately have "LS = LT" |
|
1259 |
using subspace_dim_equal[of LS LT] ls lt by auto |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1260 |
moreover have "S = {x. \<exists>y \<in> LS. a+y=x}" "T = {x. \<exists>y \<in> LT. a+y=x}" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1261 |
using LS_def LT_def by auto |
71242 | 1262 |
ultimately show ?thesis by auto |
1263 |
qed |
|
1264 |
||
1265 |
lemma aff_dim_eq_0: |
|
1266 |
fixes S :: "'a::euclidean_space set" |
|
1267 |
shows "aff_dim S = 0 \<longleftrightarrow> (\<exists>a. S = {a})" |
|
1268 |
proof (cases "S = {}") |
|
1269 |
case False |
|
1270 |
then obtain a where "a \<in> S" by auto |
|
1271 |
show ?thesis |
|
1272 |
proof safe |
|
1273 |
assume 0: "aff_dim S = 0" |
|
1274 |
have "\<not> {a,b} \<subseteq> S" if "b \<noteq> a" for b |
|
1275 |
by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that) |
|
1276 |
then show "\<exists>a. S = {a}" |
|
1277 |
using \<open>a \<in> S\<close> by blast |
|
1278 |
qed auto |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1279 |
qed auto |
71242 | 1280 |
|
1281 |
lemma affine_hull_UNIV: |
|
1282 |
fixes S :: "'n::euclidean_space set" |
|
1283 |
assumes "aff_dim S = int(DIM('n))" |
|
1284 |
shows "affine hull S = (UNIV :: ('n::euclidean_space) set)" |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1285 |
by (simp add: aff_dim_empty affine_dim_equal assms) |
71242 | 1286 |
|
1287 |
lemma disjoint_affine_hull: |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1288 |
fixes S :: "'n::euclidean_space set" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1289 |
assumes "\<not> affine_dependent S" "T \<subseteq> S" "U \<subseteq> S" "T \<inter> U = {}" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1290 |
shows "(affine hull T) \<inter> (affine hull U) = {}" |
71242 | 1291 |
proof - |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1292 |
obtain "finite S" "finite T" "finite U" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1293 |
using assms by (simp add: aff_independent_finite finite_subset) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1294 |
have False if "y \<in> affine hull T" and "y \<in> affine hull U" for y |
73372 | 1295 |
proof - |
1296 |
from that obtain a b |
|
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1297 |
where a1 [simp]: "sum a T = 1" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1298 |
and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) T = y" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1299 |
and [simp]: "sum b U = 1" "sum (\<lambda>v. b v *\<^sub>R v) U = y" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1300 |
by (auto simp: affine_hull_finite \<open>finite T\<close> \<open>finite U\<close>) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1301 |
define c where "c x = (if x \<in> T then a x else if x \<in> U then -(b x) else 0)" for x |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1302 |
have [simp]: "S \<inter> T = T" "S \<inter> - T \<inter> U = U" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1303 |
using assms by auto |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1304 |
have "sum c S = 0" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1305 |
by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite S\<close> sum_negf) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1306 |
moreover have "\<not> (\<forall>v\<in>S. c v = 0)" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1307 |
by (metis (no_types) IntD1 \<open>S \<inter> T = T\<close> a1 c_def sum.neutral zero_neq_one) |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1308 |
moreover have "(\<Sum>v\<in>S. c v *\<^sub>R v) = 0" |
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1309 |
by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases \<open>finite S\<close>) |
73372 | 1310 |
ultimately show ?thesis |
78516
56a408fa2440
substantial tidy-up, shortening many proofs
paulson <lp15@cam.ac.uk>
parents:
76836
diff
changeset
|
1311 |
using assms(1) \<open>finite S\<close> by (auto simp: affine_dependent_explicit) |
73372 | 1312 |
qed |
71242 | 1313 |
then show ?thesis by blast |
1314 |
qed |
|
1315 |
||
1316 |
end |