author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44890  22f665a2e91c 
child 49522  355f3d076924 
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)" 

19 
proof 

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

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

26 
apply (rule_tac x="s" in exI) 

27 
apply auto 

28 
apply (erule_tac x=y in allE) 

29 
apply auto 

30 
done 

31 

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

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

34 

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

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

37 

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

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

40 

41 
lemma sqrt_even_pow2: assumes n: "even n" 

42 
shows "sqrt(2 ^ n) = 2 ^ (n div 2)" 

43 
proof 

44 
from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex .. 

45 
from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)" 

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

47 
then show ?thesis using m by simp 

48 
qed 

49 

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

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

52 
using sqrt_divide_self_eq[of x] 

53 
apply (simp add: inverse_eq_divide field_simps) 

54 
done 

55 

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

57 

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

44666  59 
by simp (* TODO: delete *) 
44133  60 

61 
lemma norm_cauchy_schwarz: 

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

65 

66 
lemma norm_triangle_sub: 

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

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

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

70 

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

72 
by (simp add: norm_eq_sqrt_inner) 

44666  73 

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

44666  76 

44133  77 
lemma norm_eq: "norm(x) = norm (y) \<longleftrightarrow> x \<bullet> x = y \<bullet> y" 
78 
apply(subst order_eq_iff) unfolding norm_le by auto 

44666  79 

44133  80 
lemma norm_eq_1: "norm(x) = 1 \<longleftrightarrow> x \<bullet> x = 1" 
44666  81 
by (simp add: norm_eq_sqrt_inner) 
44133  82 

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

84 

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

44666  86 
by (simp only: power2_norm_eq_inner) (* TODO: move? *) 
44133  87 

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

89 
by (auto simp add: norm_eq_sqrt_inner) 

90 

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

92 
proof 

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

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

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

96 
next 

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

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

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

100 
qed 

101 

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

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

104 
using norm_ge_zero[of x] 

105 
apply arith 

106 
done 

107 

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

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

110 
using norm_ge_zero[of x] 

111 
apply arith 

112 
done 

113 

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

115 
by (metis not_le norm_ge_square) 

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

117 
by (metis norm_le_square not_less) 

118 

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

120 

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

121 
lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44176
diff
changeset

122 
inner_scaleR_left inner_scaleR_right 
44133  123 

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

125 
unfolding power2_norm_eq_inner inner_simps inner_commute by auto 

126 

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

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

129 

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

131 

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

133 
proof 

134 
assume ?lhs then show ?rhs by simp 

135 
next 

136 
assume ?rhs 

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

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

44133  140 
then show "x = y" by (simp) 
141 
qed 

142 

143 
lemma norm_triangle_half_r: 

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

145 
using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto 

146 

147 
lemma norm_triangle_half_l: assumes "norm (x  y) < e / 2" "norm (x'  (y)) < e / 2" 

148 
shows "norm (x  x') < e" 

149 
using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]] 

150 
unfolding dist_norm[THEN sym] . 

151 

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

44666  153 
by (rule norm_triangle_ineq [THEN order_trans]) 
44133  154 

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

44666  156 
by (rule norm_triangle_ineq [THEN le_less_trans]) 
44133  157 

158 
lemma setsum_clauses: 

159 
shows "setsum f {} = 0" 

160 
and "finite S \<Longrightarrow> setsum f (insert x S) = 

161 
(if x \<in> S then setsum f S else f x + setsum f S)" 

162 
by (auto simp add: insert_absorb) 

163 

164 
lemma setsum_norm_le: 

165 
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

166 
assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x" 
44133  167 
shows "norm (setsum f S) \<le> setsum g S" 
44176
eda112e9cdee
remove redundant lemma setsum_norm in favor of norm_setsum;
huffman
parents:
44170
diff
changeset

168 
by (rule order_trans [OF norm_setsum setsum_mono], simp add: fg) 
44133  169 

170 
lemma setsum_norm_bound: 

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

172 
assumes fS: "finite S" 

173 
and K: "\<forall>x \<in> S. norm (f x) \<le> K" 

174 
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

175 
using setsum_norm_le[OF K] setsum_constant[symmetric] 
44133  176 
by simp 
177 

178 
lemma setsum_group: 

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

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

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

182 
apply (rule setsum_mono_zero_right[OF fT fST]) 

183 
by (auto intro: setsum_0') 

184 

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

186 
proof 

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

44454  188 
hence "\<forall>x. x \<bullet> (y  z) = 0" by (simp add: inner_diff) 
44133  189 
hence "(y  z) \<bullet> (y  z) = 0" .. 
190 
thus "y = z" by simp 

191 
qed simp 

192 

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

194 
proof 

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

44454  196 
hence "\<forall>z. (x  y) \<bullet> z = 0" by (simp add: inner_diff) 
44133  197 
hence "(x  y) \<bullet> (x  y) = 0" .. 
198 
thus "x = y" by simp 

199 
qed simp 

200 

201 
subsection{* Orthogonality. *} 

202 

203 
context real_inner 

204 
begin 

205 

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

207 

208 
lemma orthogonal_clauses: 

209 
"orthogonal a 0" 

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

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

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

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

214 
"orthogonal 0 a" 

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

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

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

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

44666  219 
unfolding orthogonal_def inner_add inner_diff by auto 
220 

44133  221 
end 
222 

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

224 
by (simp add: orthogonal_def inner_commute) 

225 

226 
subsection{* Linear functions. *} 

227 

228 
definition 

229 
linear :: "('a::real_vector \<Rightarrow> 'b::real_vector) \<Rightarrow> bool" where 

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

231 

232 
lemma linearI: assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x" 

233 
shows "linear f" using assms unfolding linear_def by auto 

234 

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

236 
by (simp add: linear_def algebra_simps) 

237 

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

239 
by (simp add: linear_def) 

240 

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

242 
by (simp add: linear_def algebra_simps) 

243 

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

245 
by (simp add: linear_def algebra_simps) 

246 

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

248 
by (simp add: linear_def) 

249 

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

251 

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

253 

254 
lemma linear_compose_setsum: 

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

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

257 
using lS 

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

259 
by (auto simp add: linear_zero intro: linear_compose_add) 

260 

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

262 
unfolding linear_def 

263 
apply clarsimp 

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

265 
apply simp 

266 
done 

267 

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

269 

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

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

272 

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

274 

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

276 
by (simp add: diff_minus linear_add linear_neg) 

277 

278 
lemma linear_setsum: 

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

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

281 
proof (induct rule: finite_induct[OF fS]) 

282 
case 1 thus ?case by (simp add: linear_0[OF lf]) 

283 
next 

284 
case (2 x F) 

285 
have "f (setsum g (insert x F)) = f (g x + setsum g F)" using "2.hyps" 

286 
by simp 

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

288 
also have "\<dots> = setsum (f o g) (insert x F)" using "2.hyps" by simp 

289 
finally show ?case . 

290 
qed 

291 

292 
lemma linear_setsum_mul: 

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

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

295 
using linear_setsum[OF lf fS, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def] 

296 
linear_cmul[OF lf] by simp 

297 

298 
lemma linear_injective_0: 

299 
assumes lf: "linear f" 

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

301 
proof 

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

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

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

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

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

307 
finally show ?thesis . 

308 
qed 

309 

310 
subsection{* Bilinear functions. *} 

311 

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

313 

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

315 
by (simp add: bilinear_def linear_def) 

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

317 
by (simp add: bilinear_def linear_def) 

318 

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

320 
by (simp add: bilinear_def linear_def) 

321 

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

323 
by (simp add: bilinear_def linear_def) 

324 

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

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

327 

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

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

330 

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

332 
using add_imp_eq[of x y 0] by auto 

333 

334 
lemma bilinear_lzero: 

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

336 
using bilinear_ladd[OF bh, of 0 0 x] 

337 
by (simp add: eq_add_iff field_simps) 

338 

339 
lemma bilinear_rzero: 

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

341 
using bilinear_radd[OF bh, of x 0 0 ] 

342 
by (simp add: eq_add_iff field_simps) 

343 

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

345 
by (simp add: diff_minus bilinear_ladd bilinear_lneg) 

346 

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

348 
by (simp add: diff_minus bilinear_radd bilinear_rneg) 

349 

350 
lemma bilinear_setsum: 

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

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

353 
proof 

354 
have "h (setsum f S) (setsum g T) = setsum (\<lambda>x. h (f x) (setsum g T)) S" 

355 
apply (rule linear_setsum[unfolded o_def]) 

356 
using bh fS by (auto simp add: bilinear_def) 

357 
also have "\<dots> = setsum (\<lambda>x. setsum (\<lambda>y. h (f x) (g y)) T) S" 

358 
apply (rule setsum_cong, simp) 

359 
apply (rule linear_setsum[unfolded o_def]) 

360 
using bh fT by (auto simp add: bilinear_def) 

361 
finally show ?thesis unfolding setsum_cartesian_product . 

362 
qed 

363 

364 
subsection{* Adjoints. *} 

365 

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

367 

368 
lemma adjoint_unique: 

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

370 
shows "adjoint f = g" 

371 
unfolding adjoint_def 

372 
proof (rule some_equality) 

373 
show "\<forall>x y. inner (f x) y = inner x (g y)" using assms . 

374 
next 

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

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

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

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

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

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

381 
qed 

382 

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

384 

385 
subsection{* Interlude: Some properties of real sets *} 

386 

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

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

389 
using assms apply auto 

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

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

392 
apply auto 

393 
done 

394 

395 

396 
lemma infinite_enumerate: assumes fS: "infinite S" 

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

398 
unfolding subseq_def 

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

400 

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

402 
apply auto 

403 
apply (rule_tac x="d/2" in exI) 

404 
apply auto 

405 
done 

406 

407 

408 
lemma triangle_lemma: 

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

410 
shows "x <= y + z" 

411 
proof 

412 
have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg) 

413 
with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps) 

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

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

416 
qed 

417 

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

419 

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

420 
definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

421 
"S hull s = Inter {t. S t \<and> s \<subseteq> t}" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

422 

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

423 
lemma hull_same: "S s \<Longrightarrow> S hull s = s" 
44133  424 
unfolding hull_def by auto 
425 

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

426 
lemma hull_in: "(\<And>T. Ball T S ==> S (Inter T)) ==> S (S hull s)" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

427 
unfolding hull_def Ball_def by auto 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

428 

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

429 
lemma hull_eq: "(\<And>T. Ball T S ==> S (Inter T)) ==> (S hull s) = s \<longleftrightarrow> S s" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

430 
using hull_same[of S s] hull_in[of S s] by metis 
44133  431 

432 

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

434 
unfolding hull_def by blast 

435 

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

437 
unfolding hull_def by blast 

438 

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

440 
unfolding hull_def by blast 

441 

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

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

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

445 
lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> S t ==> (S hull s) \<subseteq> t" 
44133  446 
unfolding hull_def by blast 
447 

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

448 
lemma subset_hull: "S t ==> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t" 
44133  449 
unfolding hull_def by blast 
450 

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

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

454 

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

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

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

457 
by (auto simp add: subset_eq) 
44133  458 

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

460 

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

462 
unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2) 

463 

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

464 
lemma hull_union: assumes T: "\<And>T. Ball T S ==> S (Inter T)" 
44133  465 
shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)" 
466 
apply rule 

467 
apply (rule hull_mono) 

468 
unfolding Un_subset_iff 

469 
apply (metis hull_subset Un_upper1 Un_upper2 subset_trans) 

470 
apply (rule hull_minimal) 

471 
apply (metis hull_union_subset) 

472 
apply (metis hull_in T) 

473 
done 

474 

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

476 
unfolding hull_def by blast 

477 

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

479 
by (metis hull_redundant_eq) 

480 

44666  481 
subsection {* Archimedean properties and useful consequences *} 
44133  482 

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

44666  484 
unfolding real_of_nat_def by (rule ex_le_of_nat) 
44133  485 

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

487 
using reals_Archimedean 

488 
apply (auto simp add: field_simps) 

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

490 
apply arith 

491 
apply simp 

492 
done 

493 

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

495 
proof(induct n) 

496 
case 0 thus ?case by simp 

497 
next 

498 
case (Suc n) 

499 
hence h: "1 + real n * x \<le> (1 + x) ^ n" by simp 

500 
from h have p: "1 \<le> (1 + x) ^ n" using Suc.prems by simp 

501 
from h have "1 + real n * x + x \<le> (1 + x) ^ n + x" by simp 

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

503 
apply (simp add: field_simps) 

504 
using mult_left_mono[OF p Suc.prems] by simp 

505 
finally show ?case by (simp add: real_of_nat_Suc field_simps) 

506 
qed 

507 

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

509 
proof 

510 
from x have x0: "x  1 > 0" by arith 

44666  511 
from reals_Archimedean3[OF x0, rule_format, of y] 
44133  512 
obtain n::nat where n:"y < real n * (x  1)" by metis 
513 
from x0 have x00: "x 1 \<ge> 0" by arith 

514 
from real_pow_lbound[OF x00, of n] n 

515 
have "y < x^n" by auto 

516 
then show ?thesis by metis 

517 
qed 

518 

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

520 
using real_arch_pow[of 2 x] by simp 

521 

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

523 
shows "\<exists>n. x^n < y" 

524 
proof 

525 
{assume x0: "x > 0" 

526 
from x0 x1 have ix: "1 < 1/x" by (simp add: field_simps) 

527 
from real_arch_pow[OF ix, of "1/y"] 

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

529 
then 

530 
have ?thesis using y x0 by (auto simp add: field_simps power_divide) } 

531 
moreover 

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

533 
ultimately show ?thesis by metis 

534 
qed 

535 

536 
lemma forall_pos_mono: "(\<And>d e::real. d < e \<Longrightarrow> P d ==> P e) \<Longrightarrow> (\<And>n::nat. n \<noteq> 0 ==> P(inverse(real n))) \<Longrightarrow> (\<And>e. 0 < e ==> P e)" 

537 
by (metis real_arch_inv) 

538 

539 
lemma forall_pos_mono_1: "(\<And>d e::real. d < e \<Longrightarrow> P d ==> P e) \<Longrightarrow> (\<And>n. P(inverse(real (Suc n)))) ==> 0 < e ==> P e" 

540 
apply (rule forall_pos_mono) 

541 
apply auto 

542 
apply (atomize) 

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

544 
apply auto 

545 
done 

546 

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

548 
shows "x = 0" 

549 
proof 

550 
{assume "x \<noteq> 0" with x0 have xp: "x > 0" by arith 

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

44133  553 
with xc[rule_format, of n] have "n = 0" by arith 
554 
with n c have False by simp} 

555 
then show ?thesis by blast 

556 
qed 

557 

558 
subsection{* A bit of linear algebra. *} 

559 

560 
definition (in real_vector) 

561 
subspace :: "'a set \<Rightarrow> bool" where 

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

563 

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

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

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

567 

568 
text {* Closure properties of subspaces. *} 

569 

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

571 

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

573 

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

575 
by (metis subspace_def) 

576 

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

578 
by (metis subspace_def) 

579 

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

581 
by (metis scaleR_minus1_left subspace_mul) 

582 

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

584 
by (metis diff_minus subspace_add subspace_neg) 

585 

586 
lemma (in real_vector) subspace_setsum: 

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

588 
and f: "\<forall>x\<in> B. f x \<in> A" 

589 
shows "setsum f B \<in> A" 

590 
using fB f sA 

591 
apply(induct rule: finite_induct[OF fB]) 

592 
by (simp add: subspace_def sA, auto simp add: sA subspace_add) 

593 

594 
lemma subspace_linear_image: 

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

596 
shows "subspace(f ` S)" 

597 
using lf sS linear_0[OF lf] 

598 
unfolding linear_def subspace_def 

599 
apply (auto simp add: image_iff) 

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

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

602 
done 

603 

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

606 

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

609 

610 
lemma subspace_trivial: "subspace {0}" 

611 
by (simp add: subspace_def) 

612 

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

614 
by (simp add: subspace_def) 

615 

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

618 

619 
text {* Properties of span. *} 

620 

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

623 

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

625 
unfolding span_def 

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

626 
apply (rule hull_in) 
44133  627 
apply (simp only: subspace_def Inter_iff Int_iff subset_eq) 
628 
apply auto 

629 
done 

630 

631 
lemma (in real_vector) span_clauses: 

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

633 
"0 \<in> span S" 

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

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

636 
by (metis span_def hull_subset subset_eq) 

637 
(metis subspace_span subspace_def)+ 

638 

44521  639 
lemma span_unique: 
640 
"\<lbrakk>S \<subseteq> T; subspace T; \<And>T'. \<lbrakk>S \<subseteq> T'; subspace T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk> \<Longrightarrow> span S = T" 

641 
unfolding span_def by (rule hull_unique) 

642 

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

644 
unfolding span_def by (rule hull_minimal) 

645 

646 
lemma (in real_vector) span_induct: 

647 
assumes x: "x \<in> span S" and P: "subspace P" and SP: "\<And>x. x \<in> S ==> x \<in> P" 

648 
shows "x \<in> P" 

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

650 
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

651 
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

652 
show "x \<in> P" by (metis subset_eq) 
44133  653 
qed 
654 

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

656 
apply (simp add: span_def) 

657 
apply (rule hull_unique) 

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

658 
apply (auto simp add: subspace_def) 
44133  659 
done 
660 

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

662 
by (simp add: dependent_def) 

663 

664 
lemma dependent_single[simp]: 

665 
"dependent {x} \<longleftrightarrow> x = 0" 

666 
unfolding dependent_def by auto 

667 

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

669 
apply (clarsimp simp add: dependent_def span_mono) 

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

671 
apply force 

672 
apply (rule span_mono) 

673 
apply auto 

674 
done 

675 

676 
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

677 
by (metis order_antisym span_def hull_minimal) 
44133  678 

679 
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

680 
and P: "subspace {x. P x}" shows "\<forall>x \<in> span S. P x" 
44133  681 
using span_induct SP P by blast 
682 

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

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

685 
span_induct_alt_help_0: "0 \<in> span_induct_alt_help S" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

686 
 span_induct_alt_help_S: "x \<in> S \<Longrightarrow> z \<in> span_induct_alt_help S \<Longrightarrow> (c *\<^sub>R x + z) \<in> span_induct_alt_help S" 
44133  687 

688 
lemma span_induct_alt': 

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

690 
proof 

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

691 
{fix x:: "'a" assume x: "x \<in> span_induct_alt_help S" 
44133  692 
have "h x" 
693 
apply (rule span_induct_alt_help.induct[OF x]) 

694 
apply (rule h0) 

695 
apply (rule hS, assumption, assumption) 

696 
done} 

697 
note th0 = this 

698 
{fix x assume x: "x \<in> span S" 

699 

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

700 
have "x \<in> span_induct_alt_help S" 
44133  701 
proof(rule span_induct[where x=x and S=S]) 
702 
show "x \<in> span S" using x . 

703 
next 

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

705 
from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1] 

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

706 
show "x \<in> span_induct_alt_help S" by simp 
44133  707 
next 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

708 
have "0 \<in> span_induct_alt_help S" by (rule span_induct_alt_help_0) 
44133  709 
moreover 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

710 
{fix x y assume h: "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S" 
44133  711 
from h 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

712 
have "(x + y) \<in> span_induct_alt_help S" 
44133  713 
apply (induct rule: span_induct_alt_help.induct) 
714 
apply simp 

715 
unfolding add_assoc 

716 
apply (rule span_induct_alt_help_S) 

717 
apply assumption 

718 
apply simp 

719 
done} 

720 
moreover 

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

721 
{fix c x assume xt: "x \<in> span_induct_alt_help S" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44166
diff
changeset

722 
then have "(c *\<^sub>R x) \<in> span_induct_alt_help S" 
44133  723 
apply (induct rule: span_induct_alt_help.induct) 
724 
apply (simp add: span_induct_alt_help_0) 

725 
apply (simp add: scaleR_right_distrib) 

726 
apply (rule span_induct_alt_help_S) 

727 
apply assumption 

728 
apply simp 

729 
done 

730 
} 

731 
ultimately show "subspace (span_induct_alt_help S)" 

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

732 
unfolding subspace_def Ball_def by blast 
44133  733 
qed} 
734 
with th0 show ?thesis by blast 

735 
qed 

736 

737 
lemma span_induct_alt: 

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

739 
shows "h x" 

740 
using span_induct_alt'[of h S] h0 hS x by blast 

741 

742 
text {* Individual closure properties. *} 

743 

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

745 
unfolding span_def hull_hull .. 

746 

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

748 

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

750 

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

752 
by (metis subset_eq span_superset) 

753 

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

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

756 
using assms span_0 by auto 

757 

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

759 
by (metis subspace_add subspace_span) 

760 

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

762 
by (metis subspace_span subspace_mul) 

763 

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

765 
by (metis subspace_neg subspace_span) 

766 

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

768 
by (metis subspace_span subspace_sub) 

769 

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

771 
by (rule subspace_setsum, rule subspace_span) 

772 

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

774 
apply (auto simp only: span_add span_sub) 

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

776 
by (simp only: span_add span_sub) 

777 

778 
text {* Mapping under linear image. *} 

779 

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

782 

783 
lemma span_linear_image: 

784 
assumes lf: "linear f" 

44133  785 
shows "span (f ` S) = f ` (span S)" 
44521  786 
proof (rule span_unique) 
787 
show "f ` S \<subseteq> f ` span S" 

788 
by (intro image_mono span_inc) 

789 
show "subspace (f ` span S)" 

790 
using lf subspace_span by (rule subspace_linear_image) 

791 
next 

792 
fix T assume "f ` S \<subseteq> T" and "subspace T" thus "f ` span S \<subseteq> T" 

793 
unfolding image_subset_iff_subset_vimage 

794 
by (intro span_minimal subspace_linear_vimage lf) 

795 
qed 

796 

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

798 
proof (rule span_unique) 

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

800 
by safe (force intro: span_clauses)+ 

801 
next 

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

803 
by (simp add: linear_def scaleR_add_right) 

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

805 
by (intro subspace_Times subspace_span) 

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

807 
by (rule subspace_linear_image) 

808 
next 

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

810 
thus "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T" 

811 
by (auto intro!: subspace_add elim: span_induct) 

44133  812 
qed 
813 

814 
text {* The key breakdown property. *} 

815 

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

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

819 
by (fast intro: scaleR_one [symmetric]) 

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

821 
unfolding subspace_def 

822 
by (auto intro: scaleR_add_left [symmetric]) 

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

824 
unfolding subspace_def by auto 

825 
qed 

826 

827 
lemma span_insert: 

828 
"span (insert a S) = {x. \<exists>k. (x  k *\<^sub>R a) \<in> span S}" 

829 
proof  

830 
have "span ({a} \<union> S) = {x. \<exists>k. (x  k *\<^sub>R a) \<in> span S}" 

831 
unfolding span_union span_singleton 

832 
apply safe 

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

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

835 
apply simp 

836 
apply (rule right_minus) 

837 
done 

838 
thus ?thesis by simp 

839 
qed 

840 

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

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

845 
by (simp add: insert_absorb) 

44133  846 

847 
lemma span_breakdown_eq: 

44521  848 
"x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x  k *\<^sub>R a) \<in> span S)" 
849 
by (simp add: span_insert) 

44133  850 

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

852 

853 
lemma in_span_insert: 

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

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

856 
proof 

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

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

859 
{assume k0: "k = 0" 

860 
with k have "a \<in> span S" 

861 
apply (simp) 

862 
apply (rule set_rev_mp) 

863 
apply assumption 

864 
apply (rule span_mono) 

865 
apply blast 

866 
done 

867 
with na have ?thesis by blast} 

868 
moreover 

869 
{assume k0: "k \<noteq> 0" 

870 
have eq: "b = (1/k) *\<^sub>R a  ((1/k) *\<^sub>R a  b)" by simp 

871 
from k0 have eq': "(1/k) *\<^sub>R (a  k*\<^sub>R b) = (1/k) *\<^sub>R a  b" 

872 
by (simp add: algebra_simps) 

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

874 
by (rule span_mul) 

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

876 
unfolding eq' . 

877 

878 
from k 

879 
have ?thesis 

880 
apply (subst eq) 

881 
apply (rule span_sub) 

882 
apply (rule span_mul) 

883 
apply (rule span_superset) 

884 
apply blast 

885 
apply (rule set_rev_mp) 

886 
apply (rule th) 

887 
apply (rule span_mono) 

888 
using na by blast} 

889 
ultimately show ?thesis by blast 

890 
qed 

891 

892 
lemma in_span_delete: 

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

894 
and na: "a \<notin> span (S{b})" 

895 
shows "b \<in> span (insert a (S  {b}))" 

896 
apply (rule in_span_insert) 

897 
apply (rule set_rev_mp) 

898 
apply (rule a) 

899 
apply (rule span_mono) 

900 
apply blast 

901 
apply (rule na) 

902 
done 

903 

904 
text {* Transitivity property. *} 

905 

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

908 

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

911 
shows "y \<in> span S" 

44521  912 
using assms by (simp only: span_redundant) 
44133  913 

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

44521  915 
by (simp only: span_redundant span_0) 
44133  916 

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

918 

919 
lemma span_explicit: 

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

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

922 
proof 

923 
{fix x assume x: "x \<in> ?E" 

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

925 
by blast 

926 
have "x \<in> span P" 

927 
unfolding u[symmetric] 

928 
apply (rule span_setsum[OF fS]) 

929 
using span_mono[OF SP] 

930 
by (auto intro: span_superset span_mul)} 

931 
moreover 

932 
have "\<forall>x \<in> span P. x \<in> ?E" 

933 
proof(rule span_induct_alt') 

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

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

935 
unfolding mem_Collect_eq 
44133  936 
apply (rule exI[where x="{}"]) by simp 
937 
next 

938 
fix c x y 

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

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

942 
let ?S = "insert x S" 

943 
let ?u = "\<lambda>y. if y = x then (if x \<in> S then u y + c else c) 

944 
else u y" 

945 
from fS SP x have th0: "finite (insert x S)" "insert x S \<subseteq> P" by blast+ 

946 
{assume xS: "x \<in> S" 

947 
have S1: "S = (S  {x}) \<union> {x}" 

948 
and Sss:"finite (S  {x})" "finite {x}" "(S {x}) \<inter> {x} = {}" using xS fS by auto 

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

950 
using xS 

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

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

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

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

955 
by (simp add: algebra_simps) 

956 
also have "\<dots> = c*\<^sub>R x + y" 

957 
by (simp add: add_commute u) 

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

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

960 
moreover 

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

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

963 
unfolding u[symmetric] 

964 
apply (rule setsum_cong2) 

965 
using xS by auto 

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

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

968 
ultimately have "?Q ?S ?u (c*\<^sub>R x + y)" 

969 
by (cases "x \<in> S", simp, simp) 

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

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

971 
unfolding mem_Collect_eq 
44133  972 
apply  
973 
apply (rule exI[where x="?S"]) 

974 
apply (rule exI[where x="?u"]) by metis 

975 
qed 

976 
ultimately show ?thesis by blast 

977 
qed 

978 

979 
lemma dependent_explicit: 

980 
"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))" (is "?lhs = ?rhs") 

981 
proof 

982 
{assume dP: "dependent P" 

983 
then obtain a S u where aP: "a \<in> P" and fS: "finite S" 

984 
and SP: "S \<subseteq> P  {a}" and ua: "setsum (\<lambda>v. u v *\<^sub>R v) S = a" 

985 
unfolding dependent_def span_explicit by blast 

986 
let ?S = "insert a S" 

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

988 
let ?v = a 

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

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

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

992 
using fS aS 

993 
apply (simp add: setsum_clauses field_simps) 

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

995 
apply (rule setsum_cong2) 

996 
by auto 

997 
with th0 have ?rhs 

998 
apply  

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

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

1001 
by clarsimp} 

1002 
moreover 

1003 
{fix S u v assume fS: "finite S" 

1004 
and SP: "S \<subseteq> P" and vS: "v \<in> S" and uv: "u v \<noteq> 0" 

1005 
and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = 0" 

1006 
let ?a = v 

1007 
let ?S = "S  {v}" 

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

1009 
have th0: "?a \<in> P" "finite ?S" "?S \<subseteq> P" using fS SP vS by auto 

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

1011 
using fS vS uv 

1012 
by (simp add: setsum_diff1 divide_inverse field_simps) 

1013 
also have "\<dots> = ?a" 

1014 
unfolding scaleR_right.setsum [symmetric] u 

1015 
using uv by simp 

1016 
finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" . 

1017 
with th0 have ?lhs 

1018 
unfolding dependent_def span_explicit 

1019 
apply  

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

1021 
apply (simp_all del: scaleR_minus_left) 

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

1023 
by (auto simp del: scaleR_minus_left)} 

1024 
ultimately show ?thesis by blast 

1025 
qed 

1026 

1027 

1028 
lemma span_finite: 

1029 
assumes fS: "finite S" 

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

1031 
(is "_ = ?rhs") 

1032 
proof 

1033 
{fix y assume y: "y \<in> span S" 

1034 
from y obtain S' u where fS': "finite S'" and SS': "S' \<subseteq> S" and 

1035 
u: "setsum (\<lambda>v. u v *\<^sub>R v) S' = y" unfolding span_explicit by blast 

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

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

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

1039 
hence "setsum (\<lambda>v. ?u v *\<^sub>R v) S = y" by (metis u) 

1040 
hence "y \<in> ?rhs" by auto} 

1041 
moreover 

1042 
{fix y u assume u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y" 

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

1044 
ultimately show ?thesis by blast 

1045 
qed 

1046 

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

1048 

1049 
lemma independent_insert: 

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

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

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

1053 
proof 

1054 
{assume aS: "a \<in> S" 

1055 
hence ?thesis using insert_absorb[OF aS] by simp} 

1056 
moreover 

1057 
{assume aS: "a \<notin> S" 

1058 
{assume i: ?lhs 

1059 
then have ?rhs using aS 

1060 
apply simp 

1061 
apply (rule conjI) 

1062 
apply (rule independent_mono) 

1063 
apply assumption 

1064 
apply blast 

1065 
by (simp add: dependent_def)} 

1066 
moreover 

1067 
{assume i: ?rhs 

1068 
have ?lhs using i aS 

1069 
apply simp 

1070 
apply (auto simp add: dependent_def) 

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

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

1073 
apply simp 

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

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

1076 
apply simp 

1077 
apply blast 

1078 
apply (rule in_span_insert) 

1079 
apply assumption 

1080 
apply blast 

1081 
apply blast 

1082 
done} 

1083 
ultimately have ?thesis by blast} 

1084 
ultimately show ?thesis by blast 

1085 
qed 

1086 

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

1088 

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

1090 
by blast 

1091 

1092 
lemma spanning_subset_independent: 

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

1094 
and AsB: "A \<subseteq> span B" 

1095 
shows "A = B" 

1096 
proof 

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

1098 
next 

1099 
from span_mono[OF BA] span_mono[OF AsB] 

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

1101 

1102 
{fix x assume x: "x \<in> A" 

1103 
from iA have th0: "x \<notin> span (A  {x})" 

1104 
unfolding dependent_def using x by blast 

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

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

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

1108 
{assume xB: "x \<notin> B" 

1109 
from xB BA have "B \<subseteq> A {x}" by blast 

1110 
hence "span B \<subseteq> span (A  {x})" by (metis span_mono) 

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

1112 
with x have False by (metis span_superset)} 

1113 
then have "x \<in> B" by blast} 

1114 
then show "A \<subseteq> B" by blast 

1115 
qed 

1116 

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

1118 

1119 
lemma exchange_lemma: 

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

1121 
and sp:"s \<subseteq> span t" 

1122 
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'" 

1123 
using f i sp 

1124 
proof(induct "card (t  s)" arbitrary: s t rule: less_induct) 

1125 
case less 

1126 
note ft = `finite t` and s = `independent s` and sp = `s \<subseteq> span t` 

1127 
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'" 

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

1129 
{assume st: "s \<subseteq> t" 

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

1131 
by (auto intro: span_superset)} 

1132 
moreover 

1133 
{assume st: "t \<subseteq> s" 

1134 

1135 
from spanning_subset_independent[OF st s sp] 

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

1137 
by (auto intro: span_superset)} 

1138 
moreover 

1139 
{assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s" 

1140 
from st(2) obtain b where b: "b \<in> t" "b \<notin> s" by blast 

1141 
from b have "t  {b}  s \<subset> t  s" by blast 

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

1143 
by (auto intro: psubset_card_mono) 

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

1145 
{assume stb: "s \<subseteq> span(t {b})" 

1146 
from ft have ftb: "finite (t {b})" by auto 

1147 
from less(1)[OF cardlt ftb s stb] 

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

1149 
let ?w = "insert b u" 

1150 
have th0: "s \<subseteq> insert b u" using u by blast 

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

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

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

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

1155 
then 

1156 
have th2: "card (insert b u) = card t" 

1157 
using card_insert_disjoint[OF fu bu] ct0 by auto 

1158 
from u(4) have "s \<subseteq> span u" . 

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

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

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

1162 
from th have ?ths by blast} 

1163 
moreover 

1164 
{assume stb: "\<not> s \<subseteq> span(t {b})" 

1165 
from stb obtain a where a: "a \<in> s" "a \<notin> span (t  {b})" by blast 

1166 
have ab: "a \<noteq> b" using a b by blast 

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

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

1169 
using cardlt ft a b by auto 

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

1171 
{fix x assume xs: "x \<in> s" 

1172 
have t: "t \<subseteq> (insert b (insert a (t {b})))" using b by auto 

1173 
from b(1) have "b \<in> span t" by (simp add: span_superset) 

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

1175 
using a sp unfolding subset_eq by auto 

1176 
from xs sp have "x \<in> span t" by blast 

1177 
with span_mono[OF t] 

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

1179 
from span_trans[OF bs x] have "x \<in> span (insert a (t  {b}))" .} 

1180 
then have sp': "s \<subseteq> span (insert a (t  {b}))" by blast 

1181 

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

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

1184 
"s \<subseteq> span u" by blast 

1185 
from u a b ft at ct0 have "?P u" by auto 

1186 
then have ?ths by blast } 

1187 
ultimately have ?ths by blast 

1188 
} 

1189 
ultimately 

1190 
show ?ths by blast 

1191 
qed 

1192 

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

1194 

1195 
lemma independent_span_bound: 

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

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

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

1199 

1200 

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

1202 
proof 

1203 
have eq: "{f x x. x\<in> UNIV} = f ` UNIV" by auto 

1204 
show ?thesis unfolding eq 

1205 
apply (rule finite_imageI) 

1206 
apply (rule finite) 

1207 
done 

1208 
qed 

1209 

1210 
subsection{* Euclidean Spaces as Typeclass*} 

1211 

1212 
lemma independent_eq_inj_on: 

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

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

1215 
proof  

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

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

1218 
by (auto simp: inj_on_def) 

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

1220 
show ?thesis unfolding dependent_def span_finite[OF *] 

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

1222 
qed 

1223 

1224 
lemma independent_basis: 

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

1226 
unfolding independent_eq_inj_on [OF basis_inj] 

1227 
apply clarify 

1228 
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

1229 
apply (simp add: inner_setsum_right dot_basis) 
44133  1230 
done 
1231 

1232 
lemma (in euclidean_space) range_basis: 

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

1234 
proof  

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

1236 
show ?thesis unfolding * image_Un basis_finite by auto 

1237 
qed 

1238 

1239 
lemma (in euclidean_space) range_basis_finite[intro]: 

1240 
"finite (range basis)" 

1241 
unfolding range_basis by auto 

1242 

1243 
lemma span_basis: "span (range basis) = (UNIV :: 'a::euclidean_space set)" 

1244 
proof  

1245 
{ fix x :: 'a 

1246 
have "(\<Sum>i<DIM('a). (x $$ i) *\<^sub>R basis i) \<in> span (range basis :: 'a set)" 

1247 
by (simp add: span_setsum span_mul span_superset) 

1248 
hence "x \<in> span (range basis)" 

1249 
by (simp only: euclidean_representation [symmetric]) 

1250 
} thus ?thesis by auto 

1251 
qed 

1252 

1253 
lemma basis_representation: 

1254 
"\<exists>u. x = (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R (v\<Colon>'a\<Colon>euclidean_space))" 

1255 
proof  

1256 
have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]] 

1257 
have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x" 

1258 
unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44750
diff
changeset

1259 
thus ?thesis by fastforce 
44133  1260 
qed 
1261 

1262 
lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = UNIV" 

1263 
apply(subst span_basis[symmetric]) unfolding range_basis by auto 

1264 

1265 
lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = DIM('a)" 

1266 
apply(subst card_image) using basis_inj by auto 

1267 

1268 
lemma in_span_basis: "(x::'a::euclidean_space) \<in> span (basis ` {..<DIM('a)})" 

1269 
unfolding span_basis' .. 

1270 

1271 
lemma norm_bound_component_le: "norm (x::'a::euclidean_space) \<le> e \<Longrightarrow> \<bar>x$$i\<bar> <= e" 

1272 
by (metis component_le_norm order_trans) 

1273 

1274 
lemma norm_bound_component_lt: "norm (x::'a::euclidean_space) < e \<Longrightarrow> \<bar>x$$i\<bar> < e" 

1275 
by (metis component_le_norm basic_trans_rules(21)) 

1276 

1277 
lemma norm_le_l1: "norm (x::'a::euclidean_space) \<le> (\<Sum>i<DIM('a). \<bar>x $$ i\<bar>)" 

1278 
apply (subst euclidean_representation[of x]) 

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

1279 
apply (rule order_trans[OF norm_setsum]) 
44133  1280 
by (auto intro!: setsum_mono) 
1281 

1282 
lemma setsum_norm_allsubsets_bound: 

1283 
fixes f:: "'a \<Rightarrow> 'n::euclidean_space" 

1284 
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e" 

1285 
shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real DIM('n) * e" 

1286 
proof 

1287 
let ?d = "real DIM('n)" 

1288 
let ?nf = "\<lambda>x. norm (f x)" 

1289 
let ?U = "{..<DIM('n)}" 

1290 
have th0: "setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $$ i\<bar>) ?U) P = setsum (\<lambda>i. setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P) ?U" 

1291 
by (rule setsum_commute) 

1292 
have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def) 

1293 
have "setsum ?nf P \<le> setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $$ i\<bar>) ?U) P" 

1294 
apply (rule setsum_mono) by (rule norm_le_l1) 

1295 
also have "\<dots> \<le> 2 * ?d * e" 

1296 
unfolding th0 th1 

1297 
proof(rule setsum_bounded) 

1298 
fix i assume i: "i \<in> ?U" 

1299 
let ?Pp = "{x. x\<in> P \<and> f x $$ i \<ge> 0}" 

1300 
let ?Pn = "{x. x \<in> P \<and> f x $$ i < 0}" 

1301 
have thp: "P = ?Pp \<union> ?Pn" by auto 

1302 
have thp0: "?Pp \<inter> ?Pn ={}" by auto 

1303 
have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+ 

1304 
have Ppe:"setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp \<le> e" 

1305 
using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i] fPs[OF PpP] 

44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44454
diff
changeset

1306 
by(auto intro: abs_le_D1) 
44133  1307 
have Pne: "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn \<le> e" 
1308 
using component_le_norm[of "setsum (\<lambda>x.  f x) ?Pn" i] fPs[OF PnP] 

1309 
by(auto simp add: setsum_negf intro: abs_le_D1) 

1310 
have "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn" 

1311 
apply (subst thp) 

1312 
apply (rule setsum_Un_zero) 

1313 
using fP thp0 by auto 

1314 
also have "\<dots> \<le> 2*e" using Pne Ppe by arith 

1315 
finally show "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P \<le> 2*e" . 

1316 
qed 

1317 
finally show ?thesis . 

1318 
qed 

1319 

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

1321 

1322 
lemma lambda_skolem': "(\<forall>i<DIM('a::euclidean_space). \<exists>x. P i x) \<longleftrightarrow> 

1323 
(\<exists>x::'a. \<forall>i<DIM('a). P i (x$$i))" (is "?lhs \<longleftrightarrow> ?rhs") 

1324 
proof 

1325 
let ?S = "{..<DIM('a)}" 

1326 
{assume H: "?rhs" 

1327 
then have ?lhs by auto} 

1328 
moreover 

1329 
{assume H: "?lhs" 

1330 
then obtain f where f:"\<forall>i<DIM('a). P i (f i)" unfolding choice_iff' by metis 

1331 
let ?x = "(\<chi>\<chi> i. (f i)) :: 'a" 

< 