author  wenzelm 
Fri, 21 Sep 2012 22:45:14 +0200  
changeset 49522  355f3d076924 
parent 44890  22f665a2e91c 
child 49525  e87b42a26991 
permissions  rwrr 
44133  1 
(* Title: HOL/Multivariate_Analysis/Linear_Algebra.thy 
2 
Author: Amine Chaieb, University of Cambridge 

3 
*) 

4 

5 
header {* Elementary linear algebra on Euclidean spaces *} 

6 

7 
theory Linear_Algebra 

8 
imports 

9 
Euclidean_Space 

10 
"~~/src/HOL/Library/Infinite_Set" 

11 
begin 

12 

13 
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" 

14 
by auto 

15 

16 
notation inner (infix "\<bullet>" 70) 

17 

18 
lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)" 

49522  19 
proof  
44133  20 
have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith 
21 
thus ?thesis by (simp add: field_simps power2_eq_square) 

22 
qed 

23 

24 
lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y  x) < d \<longrightarrow> abs(y * y  x * x) < e)" 

49522  25 
using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] 
26 
apply (auto simp add: power2_eq_square) 

44133  27 
apply (rule_tac x="s" in exI) 
28 
apply auto 

29 
apply (erule_tac x=y in allE) 

30 
apply auto 

31 
done 

32 

33 
lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y" 

34 
using real_sqrt_le_iff[of x "y^2"] by simp 

35 

36 
lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y" 

37 
using real_sqrt_le_mono[of "x^2" y] by simp 

38 

39 
lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y" 

40 
using real_sqrt_less_mono[of "x^2" y] by simp 

41 

49522  42 
lemma sqrt_even_pow2: 
43 
assumes n: "even n" 

44133  44 
shows "sqrt(2 ^ n) = 2 ^ (n div 2)" 
49522  45 
proof  
44133  46 
from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex .. 
47 
from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)" 

48 
by (simp only: power_mult[symmetric] mult_commute) 

49 
then show ?thesis using m by simp 

50 
qed 

51 

52 
lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)" 

53 
apply (cases "x = 0", simp_all) 

54 
using sqrt_divide_self_eq[of x] 

55 
apply (simp add: inverse_eq_divide field_simps) 

56 
done 

57 

58 
text{* Hence derive more interesting properties of the norm. *} 

59 

60 
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))" 

44666  61 
by simp (* TODO: delete *) 
44133  62 

49522  63 
lemma norm_cauchy_schwarz: "inner x y <= norm x * norm y" 
44666  64 
(* TODO: move to Inner_Product.thy *) 
44133  65 
using Cauchy_Schwarz_ineq2[of x y] by auto 
66 

67 
lemma norm_triangle_sub: 

68 
fixes x y :: "'a::real_normed_vector" 

69 
shows "norm x \<le> norm y + norm (x  y)" 

70 
using norm_triangle_ineq[of "y" "x  y"] by (simp add: field_simps) 

71 

72 
lemma norm_le: "norm(x) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y" 

73 
by (simp add: norm_eq_sqrt_inner) 

44666  74 

44133  75 
lemma norm_lt: "norm(x) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y" 
76 
by (simp add: norm_eq_sqrt_inner) 

44666  77 

44133  78 
lemma norm_eq: "norm(x) = norm (y) \<longleftrightarrow> x \<bullet> x = y \<bullet> y" 
49522  79 
apply (subst order_eq_iff) 
80 
apply (auto simp: norm_le) 

81 
done 

44666  82 

44133  83 
lemma norm_eq_1: "norm(x) = 1 \<longleftrightarrow> x \<bullet> x = 1" 
44666  84 
by (simp add: norm_eq_sqrt_inner) 
44133  85 

86 
text{* Squaring equations and inequalities involving norms. *} 

87 

88 
lemma dot_square_norm: "x \<bullet> x = norm(x)^2" 

44666  89 
by (simp only: power2_norm_eq_inner) (* TODO: move? *) 
44133  90 

91 
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2" 

92 
by (auto simp add: norm_eq_sqrt_inner) 

93 

94 
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2" 

95 
proof 

96 
assume "\<bar>x\<bar> \<le> \<bar>y\<bar>" 

97 
then have "\<bar>x\<bar>\<twosuperior> \<le> \<bar>y\<bar>\<twosuperior>" by (rule power_mono, simp) 

98 
then show "x\<twosuperior> \<le> y\<twosuperior>" by simp 

99 
next 

100 
assume "x\<twosuperior> \<le> y\<twosuperior>" 

101 
then have "sqrt (x\<twosuperior>) \<le> sqrt (y\<twosuperior>)" by (rule real_sqrt_le_mono) 

102 
then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp 

103 
qed 

104 

105 
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2" 

106 
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) 

107 
using norm_ge_zero[of x] 

108 
apply arith 

109 
done 

110 

111 
lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2" 

112 
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) 

113 
using norm_ge_zero[of x] 

114 
apply arith 

115 
done 

116 

117 
lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a^2" 

118 
by (metis not_le norm_ge_square) 

119 
lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2" 

120 
by (metis norm_le_square not_less) 

121 

122 
text{* Dot product in terms of the norm rather than conversely. *} 

123 

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

124 
lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left 
49522  125 
inner_scaleR_left inner_scaleR_right 
44133  126 

127 
lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2  norm x ^ 2  norm y ^ 2) / 2" 

128 
unfolding power2_norm_eq_inner inner_simps inner_commute by auto 

129 

130 
lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2)  norm(x  y) ^ 2) / 2" 

131 
unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps) 

132 

133 
text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *} 

134 

135 
lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs") 

136 
proof 

137 
assume ?lhs then show ?rhs by simp 

138 
next 

139 
assume ?rhs 

140 
then have "x \<bullet> x  x \<bullet> y = 0 \<and> x \<bullet> y  y \<bullet> y = 0" by simp 

44454  141 
hence "x \<bullet> (x  y) = 0 \<and> y \<bullet> (x  y) = 0" by (simp add: inner_diff inner_commute) 
142 
then have "(x  y) \<bullet> (x  y) = 0" by (simp add: field_simps inner_diff inner_commute) 

44133  143 
then show "x = y" by (simp) 
144 
qed 

145 

146 
lemma norm_triangle_half_r: 

147 
shows "norm (y  x1) < e / 2 \<Longrightarrow> norm (y  x2) < e / 2 \<Longrightarrow> norm (x1  x2) < e" 

148 
using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto 

149 

49522  150 
lemma norm_triangle_half_l: 
151 
assumes "norm (x  y) < e / 2" "norm (x'  (y)) < e / 2" 

44133  152 
shows "norm (x  x') < e" 
153 
using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]] 

154 
unfolding dist_norm[THEN sym] . 

155 

156 
lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e" 

44666  157 
by (rule norm_triangle_ineq [THEN order_trans]) 
44133  158 

159 
lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e" 

44666  160 
by (rule norm_triangle_ineq [THEN le_less_trans]) 
44133  161 

162 
lemma setsum_clauses: 

163 
shows "setsum f {} = 0" 

49522  164 
and "finite S \<Longrightarrow> setsum f (insert x S) = (if x \<in> S then setsum f S else f x + setsum f S)" 
44133  165 
by (auto simp add: insert_absorb) 
166 

167 
lemma setsum_norm_le: 

168 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 

44176
eda112e9cdee
remove redundant lemma setsum_norm in favor of norm_setsum;
huffman
parents:
44170
diff
changeset

169 
assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x" 
44133  170 
shows "norm (setsum f S) \<le> setsum g S" 
49522  171 
by (rule order_trans [OF norm_setsum setsum_mono]) (simp add: fg) 
44133  172 

173 
lemma setsum_norm_bound: 

174 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 

175 
assumes fS: "finite S" 

49522  176 
and K: "\<forall>x \<in> S. norm (f x) \<le> K" 
44133  177 
shows "norm (setsum f S) \<le> of_nat (card S) * K" 
44176
eda112e9cdee
remove redundant lemma setsum_norm in favor of norm_setsum;
huffman
parents:
44170
diff
changeset

178 
using setsum_norm_le[OF K] setsum_constant[symmetric] 
44133  179 
by simp 
180 

181 
lemma setsum_group: 

182 
assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T" 

183 
shows "setsum (\<lambda>y. setsum g {x. x\<in> S \<and> f x = y}) T = setsum g S" 

184 
apply (subst setsum_image_gen[OF fS, of g f]) 

185 
apply (rule setsum_mono_zero_right[OF fT fST]) 

49522  186 
apply (auto intro: setsum_0') 
187 
done 

44133  188 

189 
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z" 

190 
proof 

191 
assume "\<forall>x. x \<bullet> y = x \<bullet> z" 

49522  192 
then have "\<forall>x. x \<bullet> (y  z) = 0" by (simp add: inner_diff) 
193 
then have "(y  z) \<bullet> (y  z) = 0" .. 

44133  194 
thus "y = z" by simp 
195 
qed simp 

196 

197 
lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y" 

198 
proof 

199 
assume "\<forall>z. x \<bullet> z = y \<bullet> z" 

49522  200 
then have "\<forall>z. (x  y) \<bullet> z = 0" by (simp add: inner_diff) 
201 
then have "(x  y) \<bullet> (x  y) = 0" .. 

44133  202 
thus "x = y" by simp 
203 
qed simp 

204 

49522  205 

206 
subsection {* Orthogonality. *} 

44133  207 

208 
context real_inner 

209 
begin 

210 

211 
definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)" 

212 

213 
lemma orthogonal_clauses: 

214 
"orthogonal a 0" 

215 
"orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)" 

216 
"orthogonal a x \<Longrightarrow> orthogonal a (x)" 

217 
"orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)" 

218 
"orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x  y)" 

219 
"orthogonal 0 a" 

220 
"orthogonal x a \<Longrightarrow> orthogonal (c *\<^sub>R x) a" 

221 
"orthogonal x a \<Longrightarrow> orthogonal (x) a" 

222 
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a" 

223 
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x  y) a" 

44666  224 
unfolding orthogonal_def inner_add inner_diff by auto 
225 

44133  226 
end 
227 

228 
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x" 

229 
by (simp add: orthogonal_def inner_commute) 

230 

49522  231 

232 
subsection {* Linear functions. *} 

233 

234 
definition linear :: "('a::real_vector \<Rightarrow> 'b::real_vector) \<Rightarrow> bool" 

235 
where "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *\<^sub>R x) = c *\<^sub>R f x)" 

236 

237 
lemma linearI: 

238 
assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x" 

239 
shows "linear f" 

240 
using assms unfolding linear_def by auto 

44133  241 

242 
lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. c *\<^sub>R f x)" 

243 
by (simp add: linear_def algebra_simps) 

244 

245 
lemma linear_compose_neg: "linear f ==> linear (\<lambda>x. (f(x)))" 

246 
by (simp add: linear_def) 

247 

248 
lemma linear_compose_add: "linear f \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))" 

249 
by (simp add: linear_def algebra_simps) 

250 

251 
lemma linear_compose_sub: "linear f \<Longrightarrow> linear g ==> linear (\<lambda>x. f x  g x)" 

252 
by (simp add: linear_def algebra_simps) 

253 

254 
lemma linear_compose: "linear f \<Longrightarrow> linear g ==> linear (g o f)" 

255 
by (simp add: linear_def) 

256 

257 
lemma linear_id: "linear id" by (simp add: linear_def id_def) 

258 

259 
lemma linear_zero: "linear (\<lambda>x. 0)" by (simp add: linear_def) 

260 

261 
lemma linear_compose_setsum: 

262 
assumes fS: "finite S" and lS: "\<forall>a \<in> S. linear (f a)" 

263 
shows "linear(\<lambda>x. setsum (\<lambda>a. f a x) S)" 

264 
using lS 

265 
apply (induct rule: finite_induct[OF fS]) 

49522  266 
apply (auto simp add: linear_zero intro: linear_compose_add) 
267 
done 

44133  268 

269 
lemma linear_0: "linear f \<Longrightarrow> f 0 = 0" 

270 
unfolding linear_def 

271 
apply clarsimp 

272 
apply (erule allE[where x="0::'a"]) 

273 
apply simp 

274 
done 

275 

49522  276 
lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" 
277 
by (simp add: linear_def) 

44133  278 

279 
lemma linear_neg: "linear f ==> f (x) =  f x" 

280 
using linear_cmul [where c="1"] by simp 

281 

49522  282 
lemma linear_add: "linear f ==> f(x + y) = f x + f y" 
283 
by (metis linear_def) 

44133  284 

285 
lemma linear_sub: "linear f ==> f(x  y) = f x  f y" 

286 
by (simp add: diff_minus linear_add linear_neg) 

287 

288 
lemma linear_setsum: 

289 
assumes lf: "linear f" and fS: "finite S" 

290 
shows "f (setsum g S) = setsum (f o g) S" 

49522  291 
using fS 
292 
proof (induct rule: finite_induct) 

293 
case empty 

294 
then show ?case by (simp add: linear_0[OF lf]) 

44133  295 
next 
49522  296 
case (insert x F) 
297 
have "f (setsum g (insert x F)) = f (g x + setsum g F)" using insert.hyps 

44133  298 
by simp 
299 
also have "\<dots> = f (g x) + f (setsum g F)" using linear_add[OF lf] by simp 

49522  300 
also have "\<dots> = setsum (f o g) (insert x F)" using insert.hyps by simp 
44133  301 
finally show ?case . 
302 
qed 

303 

304 
lemma linear_setsum_mul: 

305 
assumes lf: "linear f" and fS: "finite S" 

306 
shows "f (setsum (\<lambda>i. c i *\<^sub>R v i) S) = setsum (\<lambda>i. c i *\<^sub>R f (v i)) S" 

49522  307 
using linear_setsum[OF lf fS, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lf] 
308 
by simp 

44133  309 

310 
lemma linear_injective_0: 

311 
assumes lf: "linear f" 

312 
shows "inj f \<longleftrightarrow> (\<forall>x. f x = 0 \<longrightarrow> x = 0)" 

313 
proof 

314 
have "inj f \<longleftrightarrow> (\<forall> x y. f x = f y \<longrightarrow> x = y)" by (simp add: inj_on_def) 

315 
also have "\<dots> \<longleftrightarrow> (\<forall> x y. f x  f y = 0 \<longrightarrow> x  y = 0)" by simp 

316 
also have "\<dots> \<longleftrightarrow> (\<forall> x y. f (x  y) = 0 \<longrightarrow> x  y = 0)" 

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

318 
also have "\<dots> \<longleftrightarrow> (\<forall> x. f x = 0 \<longrightarrow> x = 0)" by auto 

319 
finally show ?thesis . 

320 
qed 

321 

49522  322 

323 
subsection {* Bilinear functions. *} 

44133  324 

325 
definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))" 

326 

327 
lemma bilinear_ladd: "bilinear h ==> h (x + y) z = (h x z) + (h y z)" 

328 
by (simp add: bilinear_def linear_def) 

329 
lemma bilinear_radd: "bilinear h ==> h x (y + z) = (h x y) + (h x z)" 

330 
by (simp add: bilinear_def linear_def) 

331 

332 
lemma bilinear_lmul: "bilinear h ==> h (c *\<^sub>R x) y = c *\<^sub>R (h x y)" 

333 
by (simp add: bilinear_def linear_def) 

334 

335 
lemma bilinear_rmul: "bilinear h ==> h x (c *\<^sub>R y) = c *\<^sub>R (h x y)" 

336 
by (simp add: bilinear_def linear_def) 

337 

338 
lemma bilinear_lneg: "bilinear h ==> h ( x) y = (h x y)" 

339 
by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul) 

340 

341 
lemma bilinear_rneg: "bilinear h ==> h x ( y) =  h x y" 

342 
by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul) 

343 

344 
lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0" 

345 
using add_imp_eq[of x y 0] by auto 

346 

347 
lemma bilinear_lzero: 

348 
assumes bh: "bilinear h" shows "h 0 x = 0" 

49522  349 
using bilinear_ladd[OF bh, of 0 0 x] by (simp add: eq_add_iff field_simps) 
44133  350 

351 
lemma bilinear_rzero: 

352 
assumes bh: "bilinear h" shows "h x 0 = 0" 

49522  353 
using bilinear_radd[OF bh, of x 0 0 ] by (simp add: eq_add_iff field_simps) 
44133  354 

355 
lemma bilinear_lsub: "bilinear h ==> h (x  y) z = h x z  h y z" 

356 
by (simp add: diff_minus bilinear_ladd bilinear_lneg) 

357 

358 
lemma bilinear_rsub: "bilinear h ==> h z (x  y) = h z x  h z y" 

359 
by (simp add: diff_minus bilinear_radd bilinear_rneg) 

360 

361 
lemma bilinear_setsum: 

362 
assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T" 

363 
shows "h (setsum f S) (setsum g T) = setsum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) " 

49522  364 
proof  
44133  365 
have "h (setsum f S) (setsum g T) = setsum (\<lambda>x. h (f x) (setsum g T)) S" 
366 
apply (rule linear_setsum[unfolded o_def]) 

49522  367 
using bh fS apply (auto simp add: bilinear_def) 
368 
done 

44133  369 
also have "\<dots> = setsum (\<lambda>x. setsum (\<lambda>y. h (f x) (g y)) T) S" 
370 
apply (rule setsum_cong, simp) 

371 
apply (rule linear_setsum[unfolded o_def]) 

49522  372 
using bh fT 
373 
apply (auto simp add: bilinear_def) 

374 
done 

44133  375 
finally show ?thesis unfolding setsum_cartesian_product . 
376 
qed 

377 

49522  378 

379 
subsection {* Adjoints. *} 

44133  380 

381 
definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)" 

382 

383 
lemma adjoint_unique: 

384 
assumes "\<forall>x y. inner (f x) y = inner x (g y)" 

385 
shows "adjoint f = g" 

49522  386 
unfolding adjoint_def 
44133  387 
proof (rule some_equality) 
388 
show "\<forall>x y. inner (f x) y = inner x (g y)" using assms . 

389 
next 

390 
fix h assume "\<forall>x y. inner (f x) y = inner x (h y)" 

391 
hence "\<forall>x y. inner x (g y) = inner x (h y)" using assms by simp 

392 
hence "\<forall>x y. inner x (g y  h y) = 0" by (simp add: inner_diff_right) 

393 
hence "\<forall>y. inner (g y  h y) (g y  h y) = 0" by simp 

394 
hence "\<forall>y. h y = g y" by simp 

395 
thus "h = g" by (simp add: ext) 

396 
qed 

397 

398 
lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis 

399 

49522  400 
subsection {* Interlude: Some properties of real sets *} 
44133  401 

402 
lemma seq_mono_lemma: assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n" and "\<forall>n \<ge> m. e n <= e m" 

403 
shows "\<forall>n \<ge> m. d n < e m" 

404 
using assms apply auto 

405 
apply (erule_tac x="n" in allE) 

406 
apply (erule_tac x="n" in allE) 

407 
apply auto 

408 
done 

409 

410 

411 
lemma infinite_enumerate: assumes fS: "infinite S" 

412 
shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)" 

413 
unfolding subseq_def 

414 
using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto 

415 

416 
lemma approachable_lt_le: "(\<exists>(d::real)>0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)" 

49522  417 
apply auto 
418 
apply (rule_tac x="d/2" in exI) 

419 
apply auto 

420 
done 

44133  421 

422 

423 
lemma triangle_lemma: 

424 
assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2" 

425 
shows "x <= y + z" 

49522  426 
proof  
44133  427 
have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg) 
428 
with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps) 

429 
from y z have yz: "y + z \<ge> 0" by arith 

430 
from power2_le_imp_le[OF th yz] show ?thesis . 

431 
qed 

432 

49522  433 

44133  434 
subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *} 
435 

49522  436 
definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) 
437 
where "S hull s = Inter {t. S t \<and> s \<subseteq> t}" 

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

438 

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

439 
lemma hull_same: "S s \<Longrightarrow> S hull s = s" 
44133  440 
unfolding hull_def by auto 
441 

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

442 
lemma hull_in: "(\<And>T. Ball T S ==> S (Inter T)) ==> S (S hull s)" 
49522  443 
unfolding hull_def Ball_def by auto 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

444 

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

445 
lemma hull_eq: "(\<And>T. Ball T S ==> S (Inter T)) ==> (S hull s) = s \<longleftrightarrow> S s" 
49522  446 
using hull_same[of S s] hull_in[of S s] by metis 
44133  447 

448 

449 
lemma hull_hull: "S hull (S hull s) = S hull s" 

450 
unfolding hull_def by blast 

451 

452 
lemma hull_subset[intro]: "s \<subseteq> (S hull s)" 

453 
unfolding hull_def by blast 

454 

455 
lemma hull_mono: " s \<subseteq> t ==> (S hull s) \<subseteq> (S hull t)" 

456 
unfolding hull_def by blast 

457 

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

458 
lemma hull_antimono: "\<forall>x. S x \<longrightarrow> T x ==> (T hull s) \<subseteq> (S hull s)" 
44133  459 
unfolding hull_def by blast 
460 

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

461 
lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> S t ==> (S hull s) \<subseteq> t" 
44133  462 
unfolding hull_def by blast 
463 

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

464 
lemma subset_hull: "S t ==> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t" 
44133  465 
unfolding hull_def by blast 
466 

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

467 
lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' ==> t \<subseteq> t') 
44133  468 
==> (S hull s = t)" 
469 
unfolding hull_def by auto 

470 

471 
lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x" 

472 
using hull_minimal[of S "{x. P x}" Q] 

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

473 
by (auto simp add: subset_eq) 
44133  474 

49522  475 
lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S" 
476 
by (metis hull_subset subset_eq) 

44133  477 

478 
lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))" 

49522  479 
unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2) 
480 

481 
lemma hull_union: 

482 
assumes T: "\<And>T. Ball T S ==> S (Inter T)" 

44133  483 
shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)" 
49522  484 
apply rule 
485 
apply (rule hull_mono) 

486 
unfolding Un_subset_iff 

487 
apply (metis hull_subset Un_upper1 Un_upper2 subset_trans) 

488 
apply (rule hull_minimal) 

489 
apply (metis hull_union_subset) 

490 
apply (metis hull_in T) 

491 
done 

44133  492 

493 
lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> (S hull (insert a s) = S hull s)" 

494 
unfolding hull_def by blast 

495 

496 
lemma hull_redundant: "a \<in> (S hull s) ==> (S hull (insert a s) = S hull s)" 

49522  497 
by (metis hull_redundant_eq) 
498 

44133  499 

44666  500 
subsection {* Archimedean properties and useful consequences *} 
44133  501 

502 
lemma real_arch_simple: "\<exists>n. x <= real (n::nat)" 

44666  503 
unfolding real_of_nat_def by (rule ex_le_of_nat) 
44133  504 

505 
lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)" 

506 
using reals_Archimedean 

507 
apply (auto simp add: field_simps) 

508 
apply (subgoal_tac "inverse (real n) > 0") 

509 
apply arith 

510 
apply simp 

511 
done 

512 

513 
lemma real_pow_lbound: "0 <= x ==> 1 + real n * x <= (1 + x) ^ n" 

49522  514 
proof (induct n) 
515 
case 0 

516 
then show ?case by simp 

44133  517 
next 
518 
case (Suc n) 

49522  519 
then have h: "1 + real n * x \<le> (1 + x) ^ n" by simp 
44133  520 
from h have p: "1 \<le> (1 + x) ^ n" using Suc.prems by simp 
521 
from h have "1 + real n * x + x \<le> (1 + x) ^ n + x" by simp 

522 
also have "\<dots> \<le> (1 + x) ^ Suc n" apply (subst diff_le_0_iff_le[symmetric]) 

523 
apply (simp add: field_simps) 

49522  524 
using mult_left_mono[OF p Suc.prems] apply simp 
525 
done 

44133  526 
finally show ?case by (simp add: real_of_nat_Suc field_simps) 
527 
qed 

528 

529 
lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\<exists>n. y < x^n" 

49522  530 
proof  
44133  531 
from x have x0: "x  1 > 0" by arith 
44666  532 
from reals_Archimedean3[OF x0, rule_format, of y] 
44133  533 
obtain n::nat where n:"y < real n * (x  1)" by metis 
534 
from x0 have x00: "x 1 \<ge> 0" by arith 

535 
from real_pow_lbound[OF x00, of n] n 

536 
have "y < x^n" by auto 

537 
then show ?thesis by metis 

538 
qed 

539 

540 
lemma real_arch_pow2: "\<exists>n. (x::real) < 2^ n" 

541 
using real_arch_pow[of 2 x] by simp 

542 

49522  543 
lemma real_arch_pow_inv: 
544 
assumes y: "(y::real) > 0" and x1: "x < 1" 

44133  545 
shows "\<exists>n. x^n < y" 
49522  546 
proof  
547 
{ assume x0: "x > 0" 

44133  548 
from x0 x1 have ix: "1 < 1/x" by (simp add: field_simps) 
549 
from real_arch_pow[OF ix, of "1/y"] 

550 
obtain n where n: "1/y < (1/x)^n" by blast 

49522  551 
then have ?thesis using y x0 
552 
by (auto simp add: field_simps power_divide) } 

44133  553 
moreover 
49522  554 
{ assume "\<not> x > 0" 
555 
with y x1 have ?thesis apply auto by (rule exI[where x=1], auto) } 

44133  556 
ultimately show ?thesis by metis 
557 
qed 

558 

49522  559 
lemma forall_pos_mono: 
560 
"(\<And>d e::real. d < e \<Longrightarrow> P d ==> P e) \<Longrightarrow> 

561 
(\<And>n::nat. n \<noteq> 0 ==> P(inverse(real n))) \<Longrightarrow> (\<And>e. 0 < e ==> P e)" 

44133  562 
by (metis real_arch_inv) 
563 

49522  564 
lemma forall_pos_mono_1: 
565 
"(\<And>d e::real. d < e \<Longrightarrow> P d ==> P e) \<Longrightarrow> 

566 
(\<And>n. P(inverse(real (Suc n)))) ==> 0 < e ==> P e" 

44133  567 
apply (rule forall_pos_mono) 
568 
apply auto 

569 
apply (atomize) 

570 
apply (erule_tac x="n  1" in allE) 

571 
apply auto 

572 
done 

573 

49522  574 
lemma real_archimedian_rdiv_eq_0: 
575 
assumes x0: "x \<ge> 0" and c: "c \<ge> 0" and xc: "\<forall>(m::nat)>0. real m * x \<le> c" 

44133  576 
shows "x = 0" 
49522  577 
proof  
578 
{ assume "x \<noteq> 0" with x0 have xp: "x > 0" by arith 

44666  579 
from reals_Archimedean3[OF xp, rule_format, of c] 
580 
obtain n::nat where n: "c < real n * x" by blast 

44133  581 
with xc[rule_format, of n] have "n = 0" by arith 
49522  582 
with n c have False by simp } 
44133  583 
then show ?thesis by blast 
584 
qed 

585 

49522  586 

44133  587 
subsection{* A bit of linear algebra. *} 
588 

49522  589 
definition (in real_vector) subspace :: "'a set \<Rightarrow> bool" 
590 
where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x\<in> S. \<forall>y \<in>S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in>S. c *\<^sub>R x \<in>S )" 

44133  591 

592 
definition (in real_vector) "span S = (subspace hull S)" 

593 
definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span(S  {a}))" 

594 
abbreviation (in real_vector) "independent s == ~(dependent s)" 

595 

596 
text {* Closure properties of subspaces. *} 

597 

598 
lemma subspace_UNIV[simp]: "subspace(UNIV)" by (simp add: subspace_def) 

599 

600 
lemma (in real_vector) subspace_0: "subspace S ==> 0 \<in> S" by (metis subspace_def) 

601 

602 
lemma (in real_vector) subspace_add: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S ==> x + y \<in> S" 

603 
by (metis subspace_def) 

604 

605 
lemma (in real_vector) subspace_mul: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> c *\<^sub>R x \<in> S" 

606 
by (metis subspace_def) 

607 

608 
lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow>  x \<in> S" 

609 
by (metis scaleR_minus1_left subspace_mul) 

610 

611 
lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x  y \<in> S" 

612 
by (metis diff_minus subspace_add subspace_neg) 

613 

614 
lemma (in real_vector) subspace_setsum: 

615 
assumes sA: "subspace A" and fB: "finite B" 

49522  616 
and f: "\<forall>x\<in> B. f x \<in> A" 
44133  617 
shows "setsum f B \<in> A" 
618 
using fB f sA 

49522  619 
by (induct rule: finite_induct[OF fB]) 
620 
(simp add: subspace_def sA, auto simp add: sA subspace_add) 

44133  621 

622 
lemma subspace_linear_image: 

623 
assumes lf: "linear f" and sS: "subspace S" 

624 
shows "subspace(f ` S)" 

625 
using lf sS linear_0[OF lf] 

626 
unfolding linear_def subspace_def 

627 
apply (auto simp add: image_iff) 

628 
apply (rule_tac x="x + y" in bexI, auto) 

629 
apply (rule_tac x="c *\<^sub>R x" in bexI, auto) 

630 
done 

631 

44521  632 
lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f ` S)" 
633 
by (auto simp add: subspace_def linear_def linear_0[of f]) 

634 

44133  635 
lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \<in> S}" 
636 
by (auto simp add: subspace_def linear_def linear_0[of f]) 

637 

638 
lemma subspace_trivial: "subspace {0}" 

639 
by (simp add: subspace_def) 

640 

641 
lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B ==> subspace (A \<inter> B)" 

642 
by (simp add: subspace_def) 

643 

44521  644 
lemma subspace_Times: "\<lbrakk>subspace A; subspace B\<rbrakk> \<Longrightarrow> subspace (A \<times> B)" 
645 
unfolding subspace_def zero_prod_def by simp 

646 

647 
text {* Properties of span. *} 

648 

44133  649 
lemma (in real_vector) span_mono: "A \<subseteq> B ==> span A \<subseteq> span B" 
650 
by (metis span_def hull_mono) 

651 

652 
lemma (in real_vector) subspace_span: "subspace(span S)" 

653 
unfolding span_def 

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

654 
apply (rule hull_in) 
44133  655 
apply (simp only: subspace_def Inter_iff Int_iff subset_eq) 
656 
apply auto 

657 
done 

658 

659 
lemma (in real_vector) span_clauses: 

660 
"a \<in> S ==> a \<in> span S" 

661 
"0 \<in> span S" 

662 
"x\<in> span S \<Longrightarrow> y \<in> span S ==> x + y \<in> span S" 

663 
"x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S" 

664 
by (metis span_def hull_subset subset_eq) 

665 
(metis subspace_span subspace_def)+ 

666 

44521  667 
lemma span_unique: 
49522  668 
"S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> (\<And>T'. S \<subseteq> T' \<Longrightarrow> subspace T' \<Longrightarrow> T \<subseteq> T') \<Longrightarrow> span S = T" 
44521  669 
unfolding span_def by (rule hull_unique) 
670 

671 
lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T" 

672 
unfolding span_def by (rule hull_minimal) 

673 

674 
lemma (in real_vector) span_induct: 

49522  675 
assumes x: "x \<in> span S" 
676 
and P: "subspace P" 

677 
and SP: "\<And>x. x \<in> S ==> x \<in> P" 

44521  678 
shows "x \<in> P" 
49522  679 
proof  
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

680 
from SP have SP': "S \<subseteq> P" by (simp add: subset_eq) 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

681 
from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]] 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

682 
show "x \<in> P" by (metis subset_eq) 
44133  683 
qed 
684 

685 
lemma span_empty[simp]: "span {} = {0}" 

686 
apply (simp add: span_def) 

687 
apply (rule hull_unique) 

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

688 
apply (auto simp add: subspace_def) 
44133  689 
done 
690 

691 
lemma (in real_vector) independent_empty[intro]: "independent {}" 

692 
by (simp add: dependent_def) 

693 

49522  694 
lemma dependent_single[simp]: "dependent {x} \<longleftrightarrow> x = 0" 
44133  695 
unfolding dependent_def by auto 
696 

697 
lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A ==> independent B" 

698 
apply (clarsimp simp add: dependent_def span_mono) 

699 
apply (subgoal_tac "span (B  {a}) \<le> span (A  {a})") 

700 
apply force 

701 
apply (rule span_mono) 

702 
apply auto 

703 
done 

704 

705 
lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow> subspace B \<Longrightarrow> span A = B" 

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

706 
by (metis order_antisym span_def hull_minimal) 
44133  707 

708 
lemma (in real_vector) span_induct': assumes SP: "\<forall>x \<in> S. P x" 

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

709 
and P: "subspace {x. P x}" shows "\<forall>x \<in> span S. P x" 
44133  710 
using span_induct SP P by blast 
711 

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

712 
inductive_set (in real_vector) span_induct_alt_help for S:: "'a set" 
44133  713 
where 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

714 
span_induct_alt_help_0: "0 \<in> span_induct_alt_help S" 
49522  715 
 span_induct_alt_help_S: 
716 
"x \<in> S \<Longrightarrow> z \<in> span_induct_alt_help S \<Longrightarrow> (c *\<^sub>R x + z) \<in> span_induct_alt_help S" 

44133  717 

718 
lemma span_induct_alt': 

49522  719 
assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)" 
720 
shows "\<forall>x \<in> span S. h x" 

721 
proof  

722 
{ fix x:: "'a" assume x: "x \<in> span_induct_alt_help S" 

44133  723 
have "h x" 
724 
apply (rule span_induct_alt_help.induct[OF x]) 

725 
apply (rule h0) 

726 
apply (rule hS, assumption, assumption) 

49522  727 
done } 
44133  728 
note th0 = this 
49522  729 
{ fix x assume x: "x \<in> span S" 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

730 
have "x \<in> span_induct_alt_help S" 
49522  731 
proof (rule span_induct[where x=x and S=S]) 
732 
show "x \<in> span S" using x . 

733 
next 

734 
fix x assume xS : "x \<in> S" 

735 
from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1] 

736 
show "x \<in> span_induct_alt_help S" by simp 

737 
next 

738 
have "0 \<in> span_induct_alt_help S" by (rule span_induct_alt_help_0) 

739 
moreover 

740 
{ fix x y 

741 
assume h: "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S" 

742 
from h have "(x + y) \<in> span_induct_alt_help S" 

743 
apply (induct rule: span_induct_alt_help.induct) 

744 
apply simp 

745 
unfolding add_assoc 

746 
apply (rule span_induct_alt_help_S) 

747 
apply assumption 

748 
apply simp 

749 
done } 

750 
moreover 

751 
{ fix c x 

752 
assume xt: "x \<in> span_induct_alt_help S" 

753 
then have "(c *\<^sub>R x) \<in> span_induct_alt_help S" 

754 
apply (induct rule: span_induct_alt_help.induct) 

755 
apply (simp add: span_induct_alt_help_0) 

756 
apply (simp add: scaleR_right_distrib) 

757 
apply (rule span_induct_alt_help_S) 

758 
apply assumption 

759 
apply simp 

760 
done } 

761 
ultimately 

762 
show "subspace (span_induct_alt_help S)" 

763 
unfolding subspace_def Ball_def by blast 

764 
qed } 

44133  765 
with th0 show ?thesis by blast 
766 
qed 

767 

768 
lemma span_induct_alt: 

769 
assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)" and x: "x \<in> span S" 

770 
shows "h x" 

49522  771 
using span_induct_alt'[of h S] h0 hS x by blast 
44133  772 

773 
text {* Individual closure properties. *} 

774 

775 
lemma span_span: "span (span A) = span A" 

776 
unfolding span_def hull_hull .. 

777 

778 
lemma (in real_vector) span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses(1)) 

779 

780 
lemma (in real_vector) span_0: "0 \<in> span S" by (metis subspace_span subspace_0) 

781 

782 
lemma span_inc: "S \<subseteq> span S" 

783 
by (metis subset_eq span_superset) 

784 

785 
lemma (in real_vector) dependent_0: assumes "0\<in>A" shows "dependent A" 

786 
unfolding dependent_def apply(rule_tac x=0 in bexI) 

787 
using assms span_0 by auto 

788 

789 
lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S ==> x + y \<in> span S" 

790 
by (metis subspace_add subspace_span) 

791 

792 
lemma (in real_vector) span_mul: "x \<in> span S ==> (c *\<^sub>R x) \<in> span S" 

793 
by (metis subspace_span subspace_mul) 

794 

795 
lemma span_neg: "x \<in> span S ==>  x \<in> span S" 

796 
by (metis subspace_neg subspace_span) 

797 

798 
lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S ==> x  y \<in> span S" 

799 
by (metis subspace_span subspace_sub) 

800 

801 
lemma (in real_vector) span_setsum: "finite A \<Longrightarrow> \<forall>x \<in> A. f x \<in> span S ==> setsum f A \<in> span S" 

802 
by (rule subspace_setsum, rule subspace_span) 

803 

804 
lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S" 

805 
apply (auto simp only: span_add span_sub) 

806 
apply (subgoal_tac "(x + y)  x \<in> span S", simp) 

49522  807 
apply (simp only: span_add span_sub) 
808 
done 

44133  809 

810 
text {* Mapping under linear image. *} 

811 

44521  812 
lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f ` B" 
813 
by auto (* TODO: move *) 

814 

815 
lemma span_linear_image: 

816 
assumes lf: "linear f" 

44133  817 
shows "span (f ` S) = f ` (span S)" 
44521  818 
proof (rule span_unique) 
819 
show "f ` S \<subseteq> f ` span S" 

820 
by (intro image_mono span_inc) 

821 
show "subspace (f ` span S)" 

822 
using lf subspace_span by (rule subspace_linear_image) 

823 
next 

49522  824 
fix T assume "f ` S \<subseteq> T" and "subspace T" 
825 
then show "f ` span S \<subseteq> T" 

44521  826 
unfolding image_subset_iff_subset_vimage 
827 
by (intro span_minimal subspace_linear_vimage lf) 

828 
qed 

829 

830 
lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)" 

831 
proof (rule span_unique) 

832 
show "A \<union> B \<subseteq> (\<lambda>(a, b). a + b) ` (span A \<times> span B)" 

833 
by safe (force intro: span_clauses)+ 

834 
next 

835 
have "linear (\<lambda>(a, b). a + b)" 

836 
by (simp add: linear_def scaleR_add_right) 

837 
moreover have "subspace (span A \<times> span B)" 

838 
by (intro subspace_Times subspace_span) 

839 
ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))" 

840 
by (rule subspace_linear_image) 

841 
next 

842 
fix T assume "A \<union> B \<subseteq> T" and "subspace T" 

49522  843 
then show "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T" 
44521  844 
by (auto intro!: subspace_add elim: span_induct) 
44133  845 
qed 
846 

847 
text {* The key breakdown property. *} 

848 

44521  849 
lemma span_singleton: "span {x} = range (\<lambda>k. k *\<^sub>R x)" 
850 
proof (rule span_unique) 

851 
show "{x} \<subseteq> range (\<lambda>k. k *\<^sub>R x)" 

852 
by (fast intro: scaleR_one [symmetric]) 

853 
show "subspace (range (\<lambda>k. k *\<^sub>R x))" 

854 
unfolding subspace_def 

855 
by (auto intro: scaleR_add_left [symmetric]) 

856 
fix T assume "{x} \<subseteq> T" and "subspace T" thus "range (\<lambda>k. k *\<^sub>R x) \<subseteq> T" 

857 
unfolding subspace_def by auto 

858 
qed 

859 

49522  860 
lemma span_insert: "span (insert a S) = {x. \<exists>k. (x  k *\<^sub>R a) \<in> span S}" 
44521  861 
proof  
862 
have "span ({a} \<union> S) = {x. \<exists>k. (x  k *\<^sub>R a) \<in> span S}" 

863 
unfolding span_union span_singleton 

864 
apply safe 

865 
apply (rule_tac x=k in exI, simp) 

866 
apply (erule rev_image_eqI [OF SigmaI [OF rangeI]]) 

867 
apply simp 

868 
apply (rule right_minus) 

869 
done 

49522  870 
then show ?thesis by simp 
44521  871 
qed 
872 

44133  873 
lemma span_breakdown: 
874 
assumes bS: "b \<in> S" and aS: "a \<in> span S" 

44521  875 
shows "\<exists>k. a  k *\<^sub>R b \<in> span (S  {b})" 
876 
using assms span_insert [of b "S  {b}"] 

877 
by (simp add: insert_absorb) 

44133  878 

49522  879 
lemma span_breakdown_eq: "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x  k *\<^sub>R a) \<in> span S)" 
44521  880 
by (simp add: span_insert) 
44133  881 

882 
text {* Hence some "reversal" results. *} 

883 

884 
lemma in_span_insert: 

885 
assumes a: "a \<in> span (insert b S)" and na: "a \<notin> span S" 

886 
shows "b \<in> span (insert a S)" 

887 
proof 

888 
from span_breakdown[of b "insert b S" a, OF insertI1 a] 

889 
obtain k where k: "a  k*\<^sub>R b \<in> span (S  {b})" by auto 

49522  890 
{ assume k0: "k = 0" 
44133  891 
with k have "a \<in> span S" 
892 
apply (simp) 

893 
apply (rule set_rev_mp) 

894 
apply assumption 

895 
apply (rule span_mono) 

896 
apply blast 

897 
done 

49522  898 
with na have ?thesis by blast } 
44133  899 
moreover 
49522  900 
{ assume k0: "k \<noteq> 0" 
44133  901 
have eq: "b = (1/k) *\<^sub>R a  ((1/k) *\<^sub>R a  b)" by simp 
902 
from k0 have eq': "(1/k) *\<^sub>R (a  k*\<^sub>R b) = (1/k) *\<^sub>R a  b" 

903 
by (simp add: algebra_simps) 

904 
from k have "(1/k) *\<^sub>R (a  k*\<^sub>R b) \<in> span (S  {b})" 

905 
by (rule span_mul) 

906 
hence th: "(1/k) *\<^sub>R a  b \<in> span (S  {b})" 

907 
unfolding eq' . 

908 

909 
from k 

910 
have ?thesis 

911 
apply (subst eq) 

912 
apply (rule span_sub) 

913 
apply (rule span_mul) 

914 
apply (rule span_superset) 

915 
apply blast 

916 
apply (rule set_rev_mp) 

917 
apply (rule th) 

918 
apply (rule span_mono) 

49522  919 
using na by blast } 
44133  920 
ultimately show ?thesis by blast 
921 
qed 

922 

923 
lemma in_span_delete: 

924 
assumes a: "a \<in> span S" 

49522  925 
and na: "a \<notin> span (S{b})" 
44133  926 
shows "b \<in> span (insert a (S  {b}))" 
927 
apply (rule in_span_insert) 

928 
apply (rule set_rev_mp) 

929 
apply (rule a) 

930 
apply (rule span_mono) 

931 
apply blast 

932 
apply (rule na) 

933 
done 

934 

935 
text {* Transitivity property. *} 

936 

44521  937 
lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S" 
938 
unfolding span_def by (rule hull_redundant) 

939 

44133  940 
lemma span_trans: 
941 
assumes x: "x \<in> span S" and y: "y \<in> span (insert x S)" 

942 
shows "y \<in> span S" 

44521  943 
using assms by (simp only: span_redundant) 
44133  944 

945 
lemma span_insert_0[simp]: "span (insert 0 S) = span S" 

44521  946 
by (simp only: span_redundant span_0) 
44133  947 

948 
text {* An explicit expansion is sometimes needed. *} 

949 

950 
lemma span_explicit: 

951 
"span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> setsum (\<lambda>v. u v *\<^sub>R v) S = y}" 

952 
(is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}") 

953 
proof 

49522  954 
{ fix x assume x: "x \<in> ?E" 
44133  955 
then obtain S u where fS: "finite S" and SP: "S\<subseteq>P" and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = x" 
956 
by blast 

957 
have "x \<in> span P" 

958 
unfolding u[symmetric] 

959 
apply (rule span_setsum[OF fS]) 

960 
using span_mono[OF SP] 

49522  961 
apply (auto intro: span_superset span_mul) 
962 
done } 

44133  963 
moreover 
964 
have "\<forall>x \<in> span P. x \<in> ?E" 

49522  965 
proof (rule span_induct_alt') 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

966 
show "0 \<in> Collect ?h" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

967 
unfolding mem_Collect_eq 
49522  968 
apply (rule exI[where x="{}"]) 
969 
apply simp 

970 
done 

44133  971 
next 
972 
fix c x y 

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

973 
assume x: "x \<in> P" and hy: "y \<in> Collect ?h" 
44133  974 
from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P" 
975 
and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y" by blast 

976 
let ?S = "insert x S" 

49522  977 
let ?u = "\<lambda>y. if y = x then (if x \<in> S then u y + c else c) else u y" 
44133  978 
from fS SP x have th0: "finite (insert x S)" "insert x S \<subseteq> P" by blast+ 
49522  979 
{ assume xS: "x \<in> S" 
44133  980 
have S1: "S = (S  {x}) \<union> {x}" 
981 
and Sss:"finite (S  {x})" "finite {x}" "(S {x}) \<inter> {x} = {}" using xS fS by auto 

982 
have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =(\<Sum>v\<in>S  {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x" 

983 
using xS 

984 
by (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]] 

985 
setsum_clauses(2)[OF fS] cong del: if_weak_cong) 

986 
also have "\<dots> = (\<Sum>v\<in>S. u v *\<^sub>R v) + c *\<^sub>R x" 

987 
apply (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]]) 

49522  988 
apply (simp add: algebra_simps) 
989 
done 

44133  990 
also have "\<dots> = c*\<^sub>R x + y" 
991 
by (simp add: add_commute u) 

992 
finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" . 

49522  993 
then have "?Q ?S ?u (c*\<^sub>R x + y)" using th0 by blast } 
994 
moreover 

995 
{ assume xS: "x \<notin> S" 

996 
have th00: "(\<Sum>v\<in>S. (if v = x then c else u v) *\<^sub>R v) = y" 

997 
unfolding u[symmetric] 

998 
apply (rule setsum_cong2) 

999 
using xS apply auto 

1000 
done 

1001 
have "?Q ?S ?u (c*\<^sub>R x + y)" using fS xS th0 

1002 
by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong) } 

1003 
ultimately have "?Q ?S ?u (c*\<^sub>R x + y)" by (cases "x \<in> S") simp_all 

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

1004 
then show "(c*\<^sub>R x + y) \<in> Collect ?h" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

1005 
unfolding mem_Collect_eq 
44133  1006 
apply  
1007 
apply (rule exI[where x="?S"]) 

49522  1008 
apply (rule exI[where x="?u"]) 
1009 
apply metis 

1010 
done 

44133  1011 
qed 
1012 
ultimately show ?thesis by blast 

1013 
qed 

1014 

1015 
lemma dependent_explicit: 

49522  1016 
"dependent P \<longleftrightarrow> (\<exists>S u. finite S \<and> S \<subseteq> P \<and> (\<exists>v\<in>S. u v \<noteq> 0 \<and> setsum (\<lambda>v. u v *\<^sub>R v) S = 0))" 
1017 
(is "?lhs = ?rhs") 

1018 
proof  

1019 
{ assume dP: "dependent P" 

44133  1020 
then obtain a S u where aP: "a \<in> P" and fS: "finite S" 
1021 
and SP: "S \<subseteq> P  {a}" and ua: "setsum (\<lambda>v. u v *\<^sub>R v) S = a" 

1022 
unfolding dependent_def span_explicit by blast 

1023 
let ?S = "insert a S" 

1024 
let ?u = "\<lambda>y. if y = a then  1 else u y" 

1025 
let ?v = a 

1026 
from aP SP have aS: "a \<notin> S" by blast 

1027 
from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0" by auto 

1028 
have s0: "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = 0" 

1029 
using fS aS 

1030 
apply (simp add: setsum_clauses field_simps) 

1031 
apply (subst (2) ua[symmetric]) 

1032 
apply (rule setsum_cong2) 

49522  1033 
apply auto 
1034 
done 

44133  1035 
with th0 have ?rhs 
1036 
apply  

1037 
apply (rule exI[where x= "?S"]) 

1038 
apply (rule exI[where x= "?u"]) 

49522  1039 
apply auto 
1040 
done 

1041 
} 

44133  1042 
moreover 
49522  1043 
{ fix S u v 
1044 
assume fS: "finite S" 

44133  1045 
and SP: "S \<subseteq> P" and vS: "v \<in> S" and uv: "u v \<noteq> 0" 
49522  1046 
and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = 0" 
44133  1047 
let ?a = v 
1048 
let ?S = "S  {v}" 

1049 
let ?u = "\<lambda>i. ( u i) / u v" 

49522  1050 
have th0: "?a \<in> P" "finite ?S" "?S \<subseteq> P" using fS SP vS by auto 
44133  1051 
have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = setsum (\<lambda>v. ( (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S  ?u v *\<^sub>R v" 
49522  1052 
using fS vS uv by (simp add: setsum_diff1 divide_inverse field_simps) 
1053 
also have "\<dots> = ?a" unfolding scaleR_right.setsum [symmetric] u using uv by simp 

44133  1054 
finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" . 
1055 
with th0 have ?lhs 

1056 
unfolding dependent_def span_explicit 

1057 
apply  

1058 
apply (rule bexI[where x= "?a"]) 

1059 
apply (simp_all del: scaleR_minus_left) 

1060 
apply (rule exI[where x= "?S"]) 

49522  1061 
apply (auto simp del: scaleR_minus_left) 
1062 
done 

1063 
} 

44133  1064 
ultimately show ?thesis by blast 
1065 
qed 

1066 

1067 

1068 
lemma span_finite: 

1069 
assumes fS: "finite S" 

1070 
shows "span S = {y. \<exists>u. setsum (\<lambda>v. u v *\<^sub>R v) S = y}" 

1071 
(is "_ = ?rhs") 

49522  1072 
proof  
1073 
{ fix y assume y: "y \<in> span S" 

44133  1074 
from y obtain S' u where fS': "finite S'" and SS': "S' \<subseteq> S" and 
1075 
u: "setsum (\<lambda>v. u v *\<^sub>R v) S' = y" unfolding span_explicit by blast 

1076 
let ?u = "\<lambda>x. if x \<in> S' then u x else 0" 

1077 
have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = setsum (\<lambda>v. u v *\<^sub>R v) S'" 

1078 
using SS' fS by (auto intro!: setsum_mono_zero_cong_right) 

49522  1079 
then have "setsum (\<lambda>v. ?u v *\<^sub>R v) S = y" by (metis u) 
1080 
then have "y \<in> ?rhs" by auto } 

44133  1081 
moreover 
49522  1082 
{ fix y u 
1083 
assume u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y" 

1084 
then have "y \<in> span S" using fS unfolding span_explicit by auto } 

44133  1085 
ultimately show ?thesis by blast 
1086 
qed 

1087 

1088 
text {* This is useful for building a basis stepbystep. *} 

1089 

1090 
lemma independent_insert: 

1091 
"independent(insert a S) \<longleftrightarrow> 

1092 
(if a \<in> S then independent S 

1093 
else independent S \<and> a \<notin> span S)" (is "?lhs \<longleftrightarrow> ?rhs") 

49522  1094 
proof  
1095 
{ assume aS: "a \<in> S" 

1096 
then have ?thesis using insert_absorb[OF aS] by simp } 

44133  1097 
moreover 
49522  1098 
{ assume aS: "a \<notin> S" 
1099 
{ assume i: ?lhs 

44133  1100 
then have ?rhs using aS 
1101 
apply simp 

1102 
apply (rule conjI) 

1103 
apply (rule independent_mono) 

1104 
apply assumption 

1105 
apply blast 

49522  1106 
apply (simp add: dependent_def) 
1107 
done } 

44133  1108 
moreover 
49522  1109 
{ assume i: ?rhs 
44133  1110 
have ?lhs using i aS 
1111 
apply simp 

1112 
apply (auto simp add: dependent_def) 

1113 
apply (case_tac "aa = a", auto) 

1114 
apply (subgoal_tac "insert a S  {aa} = insert a (S  {aa})") 

1115 
apply simp 

1116 
apply (subgoal_tac "a \<in> span (insert aa (S  {aa}))") 

1117 
apply (subgoal_tac "insert aa (S  {aa}) = S") 

1118 
apply simp 

1119 
apply blast 

1120 
apply (rule in_span_insert) 

1121 
apply assumption 

1122 
apply blast 

1123 
apply blast 

49522  1124 
done } 
1125 
ultimately have ?thesis by blast } 

44133  1126 
ultimately show ?thesis by blast 
1127 
qed 

1128 

1129 
text {* The degenerate case of the Exchange Lemma. *} 

1130 

1131 
lemma mem_delete: "x \<in> (A  {a}) \<longleftrightarrow> x \<noteq> a \<and> x \<in> A" 

1132 
by blast 

1133 

1134 
lemma spanning_subset_independent: 

1135 
assumes BA: "B \<subseteq> A" and iA: "independent A" 

49522  1136 
and AsB: "A \<subseteq> span B" 
44133  1137 
shows "A = B" 
1138 
proof 

1139 
from BA show "B \<subseteq> A" . 

1140 
next 

1141 
from span_mono[OF BA] span_mono[OF AsB] 

1142 
have sAB: "span A = span B" unfolding span_span by blast 

1143 

49522  1144 
{ fix x assume x: "x \<in> A" 
44133  1145 
from iA have th0: "x \<notin> span (A  {x})" 
1146 
unfolding dependent_def using x by blast 

1147 
from x have xsA: "x \<in> span A" by (blast intro: span_superset) 

1148 
have "A  {x} \<subseteq> A" by blast 

1149 
hence th1:"span (A  {x}) \<subseteq> span A" by (metis span_mono) 

49522  1150 
{ assume xB: "x \<notin> B" 
44133  1151 
from xB BA have "B \<subseteq> A {x}" by blast 
1152 
hence "span B \<subseteq> span (A  {x})" by (metis span_mono) 

1153 
with th1 th0 sAB have "x \<notin> span A" by blast 

49522  1154 
with x have False by (metis span_superset) } 
1155 
then have "x \<in> B" by blast } 

44133  1156 
then show "A \<subseteq> B" by blast 
1157 
qed 

1158 

1159 
text {* The general case of the Exchange Lemma, the key to what follows. *} 

1160 

1161 
lemma exchange_lemma: 

1162 
assumes f:"finite t" and i: "independent s" 

49522  1163 
and sp:"s \<subseteq> span t" 
44133  1164 
shows "\<exists>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'" 
1165 
using f i sp 

49522  1166 
proof (induct "card (t  s)" arbitrary: s t rule: less_induct) 
44133  1167 
case less 
1168 
note ft = `finite t` and s = `independent s` and sp = `s \<subseteq> span t` 

1169 
let ?P = "\<lambda>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'" 

1170 
let ?ths = "\<exists>t'. ?P t'" 

49522  1171 
{ assume st: "s \<subseteq> t" 
44133  1172 
from st ft span_mono[OF st] have ?ths apply  apply (rule exI[where x=t]) 
49522  1173 
apply (auto intro: span_superset) 
1174 
done } 

44133  1175 
moreover 
49522  1176 
{ assume st: "t \<subseteq> s" 
44133  1177 

1178 
from spanning_subset_independent[OF st s sp] 

1179 
st ft span_mono[OF st] have ?ths apply  apply (rule exI[where x=t]) 

49522  1180 
apply (auto intro: span_superset) 
1181 
done } 

44133  1182 
moreover 
49522  1183 
{ assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s" 
44133  1184 
from st(2) obtain b where b: "b \<in> t" "b \<notin> s" by blast 
1185 
from b have "t  {b}  s \<subset> t  s" by blast 

1186 
then have cardlt: "card (t  {b}  s) < card (t  s)" using ft 

1187 
by (auto intro: psubset_card_mono) 

1188 
from b ft have ct0: "card t \<noteq> 0" by auto 

49522  1189 
{ assume stb: "s \<subseteq> span(t {b})" 
44133  1190 
from ft have ftb: "finite (t {b})" by auto 
1191 
from less(1)[OF cardlt ftb s stb] 

49522  1192 
obtain u where u: "card u = card (t{b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t  {b})" "s \<subseteq> span u" 
1193 
and fu: "finite u" by blast 

44133  1194 
let ?w = "insert b u" 
1195 
have th0: "s \<subseteq> insert b u" using u by blast 

1196 
from u(3) b have "u \<subseteq> s \<union> t" by blast 

1197 
then have th1: "insert b u \<subseteq> s \<union> t" using u b by blast 

1198 
have bu: "b \<notin> u" using b u by blast 

1199 
from u(1) ft b have "card u = (card t  1)" by auto 

49522  1200 
then have th2: "card (insert b u) = card t" 
44133  1201 
using card_insert_disjoint[OF fu bu] ct0 by auto 
1202 
from u(4) have "s \<subseteq> span u" . 

1203 
also have "\<dots> \<subseteq> span (insert b u)" apply (rule span_mono) by blast 

1204 
finally have th3: "s \<subseteq> span (insert b u)" . 

1205 
from th0 th1 th2 th3 fu have th: "?P ?w" by blast 

49522  1206 
from th have ?ths by blast } 
44133  1207 
moreover 
49522  1208 
{ assume stb: "\<not> s \<subseteq> span(t {b})" 
44133  1209 
from stb obtain a where a: "a \<in> s" "a \<notin> span (t  {b})" by blast 
1210 
have ab: "a \<noteq> b" using a b by blast 

1211 
have at: "a \<notin> t" using a ab span_superset[of a "t {b}"] by auto 

1212 
have mlt: "card ((insert a (t  {b}))  s) < card (t  s)" 

1213 
using cardlt ft a b by auto 

1214 
have ft': "finite (insert a (t  {b}))" using ft by auto 

49522  1215 
{ fix x assume xs: "x \<in> s" 
44133  1216 
have t: "t \<subseteq> (insert b (insert a (t {b})))" using b by auto 
1217 
from b(1) have "b \<in> span t" by (simp add: span_superset) 

1218 
have bs: "b \<in> span (insert a (t  {b}))" apply(rule in_span_delete) 

49522  1219 
using a sp unfolding subset_eq apply auto done 
44133  1220 
from xs sp have "x \<in> span t" by blast 
1221 
with span_mono[OF t] 

1222 
have x: "x \<in> span (insert b (insert a (t  {b})))" .. 

49522  1223 
from span_trans[OF bs x] have "x \<in> span (insert a (t  {b}))" . } 
44133  1224 
then have sp': "s \<subseteq> span (insert a (t  {b}))" by blast 
1225 

1226 
from less(1)[OF mlt ft' s sp'] obtain u where 

1227 
u: "card u = card (insert a (t {b}))" "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t {b})" 

49522  1228 
"s \<subseteq> span u" by blast 
44133  1229 
from u a b ft at ct0 have "?P u" by auto 
1230 
then have ?ths by blast } 

1231 
ultimately have ?ths by blast 

1232 
} 

49522  1233 
ultimately show ?ths by blast 
44133  1234 
qed 
1235 

1236 
text {* This implies corresponding size bounds. *} 

1237 

1238 
lemma independent_span_bound: 

1239 
assumes f: "finite t" and i: "independent s" and sp:"s \<subseteq> span t" 

1240 
shows "finite s \<and> card s \<le> card t" 

1241 
by (metis exchange_lemma[OF f i sp] finite_subset card_mono) 

1242 

1243 

1244 
lemma finite_Atleast_Atmost_nat[simp]: "finite {f x x. x\<in> (UNIV::'a::finite set)}" 

49522  1245 
proof  
44133  1246 
have eq: "{f x x. x\<in> UNIV} = f ` UNIV" by auto 
1247 
show ?thesis unfolding eq 

1248 
apply (rule finite_imageI) 

1249 
apply (rule finite) 

1250 
done 

1251 
qed 

1252 

1253 
subsection{* Euclidean Spaces as Typeclass*} 

1254 

1255 
lemma independent_eq_inj_on: 

49522  1256 
fixes D :: nat and f :: "nat \<Rightarrow> 'c::real_vector" 
1257 
assumes *: "inj_on f {..<D}" 

44133  1258 
shows "independent (f ` {..<D}) \<longleftrightarrow> (\<forall>a u. a < D \<longrightarrow> (\<Sum>i\<in>{..<D}{a}. u (f i) *\<^sub>R f i) \<noteq> f a)" 
1259 
proof  

1260 
from * have eq: "\<And>i. i < D \<Longrightarrow> f ` {..<D}  {f i} = f`({..<D}  {i})" 

1261 
and inj: "\<And>i. inj_on f ({..<D}  {i})" 

1262 
by (auto simp: inj_on_def) 

1263 
have *: "\<And>i. finite (f ` {..<D}  {i})" by simp 

1264 
show ?thesis unfolding dependent_def span_finite[OF *] 

1265 
by (auto simp: eq setsum_reindex[OF inj]) 

1266 
qed 

1267 

1268 
lemma independent_basis: 

1269 
"independent (basis ` {..<DIM('a)} :: 'a::euclidean_space set)" 

1270 
unfolding independent_eq_inj_on [OF basis_inj] 

1271 
apply clarify 

1272 
apply (drule_tac f="inner (basis a)" in arg_cong) 

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

1273 
apply (simp add: inner_setsum_right dot_basis) 
44133  1274 
done 
1275 

1276 
lemma (in euclidean_space) range_basis: 

1277 
"range basis = insert 0 (basis ` {..<DIM('a)})" 

1278 
proof  

1279 
have *: "UNIV = {..<DIM('a)} \<union> {DIM('a)..}" by auto 
