src/HOL/Multivariate_Analysis/Linear_Algebra.thy
 author huffman Thu Aug 25 11:57:42 2011 -0700 (2011-08-25) changeset 44521 083eedb37a37 parent 44517 68e8eb0ce8aa child 44527 bf8014b4f933 permissions -rw-r--r--
simplify many proofs about subspace and span;
reorder premises in rule span_induct;
 huffman@44133 ` 1` ```(* Title: HOL/Multivariate_Analysis/Linear_Algebra.thy ``` huffman@44133 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` huffman@44133 ` 3` ```*) ``` huffman@44133 ` 4` huffman@44133 ` 5` ```header {* Elementary linear algebra on Euclidean spaces *} ``` huffman@44133 ` 6` huffman@44133 ` 7` ```theory Linear_Algebra ``` huffman@44133 ` 8` ```imports ``` huffman@44133 ` 9` ``` Euclidean_Space ``` huffman@44133 ` 10` ``` "~~/src/HOL/Library/Infinite_Set" ``` huffman@44133 ` 11` ```begin ``` huffman@44133 ` 12` huffman@44133 ` 13` ```lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" ``` huffman@44133 ` 14` ``` by auto ``` huffman@44133 ` 15` huffman@44133 ` 16` ```notation inner (infix "\" 70) ``` huffman@44133 ` 17` huffman@44133 ` 18` ```lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)" ``` huffman@44133 ` 19` ```proof- ``` huffman@44133 ` 20` ``` have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith ``` huffman@44133 ` 21` ``` thus ?thesis by (simp add: field_simps power2_eq_square) ``` huffman@44133 ` 22` ```qed ``` huffman@44133 ` 23` huffman@44133 ` 24` ```lemma square_continuous: "0 < (e::real) ==> \d. 0 < d \ (\y. abs(y - x) < d \ abs(y * y - x * x) < e)" ``` huffman@44133 ` 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) ``` huffman@44133 ` 26` ``` apply (rule_tac x="s" in exI) ``` huffman@44133 ` 27` ``` apply auto ``` huffman@44133 ` 28` ``` apply (erule_tac x=y in allE) ``` huffman@44133 ` 29` ``` apply auto ``` huffman@44133 ` 30` ``` done ``` huffman@44133 ` 31` huffman@44133 ` 32` ```lemma real_le_lsqrt: "0 <= x \ 0 <= y \ x <= y^2 ==> sqrt x <= y" ``` huffman@44133 ` 33` ``` using real_sqrt_le_iff[of x "y^2"] by simp ``` huffman@44133 ` 34` huffman@44133 ` 35` ```lemma real_le_rsqrt: "x^2 \ y \ x \ sqrt y" ``` huffman@44133 ` 36` ``` using real_sqrt_le_mono[of "x^2" y] by simp ``` huffman@44133 ` 37` huffman@44133 ` 38` ```lemma real_less_rsqrt: "x^2 < y \ x < sqrt y" ``` huffman@44133 ` 39` ``` using real_sqrt_less_mono[of "x^2" y] by simp ``` huffman@44133 ` 40` huffman@44133 ` 41` ```lemma sqrt_even_pow2: assumes n: "even n" ``` huffman@44133 ` 42` ``` shows "sqrt(2 ^ n) = 2 ^ (n div 2)" ``` huffman@44133 ` 43` ```proof- ``` huffman@44133 ` 44` ``` from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex .. ``` huffman@44133 ` 45` ``` from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)" ``` huffman@44133 ` 46` ``` by (simp only: power_mult[symmetric] mult_commute) ``` huffman@44133 ` 47` ``` then show ?thesis using m by simp ``` huffman@44133 ` 48` ```qed ``` huffman@44133 ` 49` huffman@44133 ` 50` ```lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)" ``` huffman@44133 ` 51` ``` apply (cases "x = 0", simp_all) ``` huffman@44133 ` 52` ``` using sqrt_divide_self_eq[of x] ``` huffman@44133 ` 53` ``` apply (simp add: inverse_eq_divide field_simps) ``` huffman@44133 ` 54` ``` done ``` huffman@44133 ` 55` huffman@44133 ` 56` ```text{* Hence derive more interesting properties of the norm. *} ``` huffman@44133 ` 57` huffman@44133 ` 58` ```(* FIXME: same as norm_scaleR ``` huffman@44133 ` 59` ```lemma norm_mul[simp]: "norm(a *\<^sub>R x) = abs(a) * norm x" ``` huffman@44133 ` 60` ``` by (simp add: norm_vector_def setL2_right_distrib abs_mult) ``` huffman@44133 ` 61` ```*) ``` huffman@44133 ` 62` huffman@44133 ` 63` ```lemma norm_eq_0_dot: "(norm x = 0) \ (inner x x = (0::real))" ``` huffman@44517 ` 64` ``` by (simp add: power2_eq_square) ``` huffman@44133 ` 65` huffman@44133 ` 66` ```lemma norm_cauchy_schwarz: ``` huffman@44133 ` 67` ``` shows "inner x y <= norm x * norm y" ``` huffman@44133 ` 68` ``` using Cauchy_Schwarz_ineq2[of x y] by auto ``` huffman@44133 ` 69` huffman@44133 ` 70` ```lemma norm_cauchy_schwarz_abs: ``` huffman@44133 ` 71` ``` shows "\inner x y\ \ norm x * norm y" ``` huffman@44133 ` 72` ``` by (rule Cauchy_Schwarz_ineq2) ``` huffman@44133 ` 73` huffman@44133 ` 74` ```lemma norm_triangle_sub: ``` huffman@44133 ` 75` ``` fixes x y :: "'a::real_normed_vector" ``` huffman@44133 ` 76` ``` shows "norm x \ norm y + norm (x - y)" ``` huffman@44133 ` 77` ``` using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps) ``` huffman@44133 ` 78` huffman@44133 ` 79` ```lemma real_abs_norm: "\norm x\ = norm x" ``` huffman@44133 ` 80` ``` by (rule abs_norm_cancel) ``` huffman@44133 ` 81` ```lemma real_abs_sub_norm: "\norm x - norm y\ <= norm(x - y)" ``` huffman@44133 ` 82` ``` by (rule norm_triangle_ineq3) ``` huffman@44133 ` 83` ```lemma norm_le: "norm(x) <= norm(y) \ x \ x <= y \ y" ``` huffman@44133 ` 84` ``` by (simp add: norm_eq_sqrt_inner) ``` huffman@44133 ` 85` ```lemma norm_lt: "norm(x) < norm(y) \ x \ x < y \ y" ``` huffman@44133 ` 86` ``` by (simp add: norm_eq_sqrt_inner) ``` huffman@44133 ` 87` ```lemma norm_eq: "norm(x) = norm (y) \ x \ x = y \ y" ``` huffman@44133 ` 88` ``` apply(subst order_eq_iff) unfolding norm_le by auto ``` huffman@44133 ` 89` ```lemma norm_eq_1: "norm(x) = 1 \ x \ x = 1" ``` huffman@44133 ` 90` ``` unfolding norm_eq_sqrt_inner by auto ``` huffman@44133 ` 91` huffman@44133 ` 92` ```text{* Squaring equations and inequalities involving norms. *} ``` huffman@44133 ` 93` huffman@44133 ` 94` ```lemma dot_square_norm: "x \ x = norm(x)^2" ``` huffman@44133 ` 95` ``` by (simp add: norm_eq_sqrt_inner) ``` huffman@44133 ` 96` huffman@44133 ` 97` ```lemma norm_eq_square: "norm(x) = a \ 0 <= a \ x \ x = a^2" ``` huffman@44133 ` 98` ``` by (auto simp add: norm_eq_sqrt_inner) ``` huffman@44133 ` 99` huffman@44133 ` 100` ```lemma real_abs_le_square_iff: "\x\ \ \y\ \ (x::real)^2 \ y^2" ``` huffman@44133 ` 101` ```proof ``` huffman@44133 ` 102` ``` assume "\x\ \ \y\" ``` huffman@44133 ` 103` ``` then have "\x\\ \ \y\\" by (rule power_mono, simp) ``` huffman@44133 ` 104` ``` then show "x\ \ y\" by simp ``` huffman@44133 ` 105` ```next ``` huffman@44133 ` 106` ``` assume "x\ \ y\" ``` huffman@44133 ` 107` ``` then have "sqrt (x\) \ sqrt (y\)" by (rule real_sqrt_le_mono) ``` huffman@44133 ` 108` ``` then show "\x\ \ \y\" by simp ``` huffman@44133 ` 109` ```qed ``` huffman@44133 ` 110` huffman@44133 ` 111` ```lemma norm_le_square: "norm(x) <= a \ 0 <= a \ x \ x <= a^2" ``` huffman@44133 ` 112` ``` apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) ``` huffman@44133 ` 113` ``` using norm_ge_zero[of x] ``` huffman@44133 ` 114` ``` apply arith ``` huffman@44133 ` 115` ``` done ``` huffman@44133 ` 116` huffman@44133 ` 117` ```lemma norm_ge_square: "norm(x) >= a \ a <= 0 \ x \ x >= a ^ 2" ``` huffman@44133 ` 118` ``` apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) ``` huffman@44133 ` 119` ``` using norm_ge_zero[of x] ``` huffman@44133 ` 120` ``` apply arith ``` huffman@44133 ` 121` ``` done ``` huffman@44133 ` 122` huffman@44133 ` 123` ```lemma norm_lt_square: "norm(x) < a \ 0 < a \ x \ x < a^2" ``` huffman@44133 ` 124` ``` by (metis not_le norm_ge_square) ``` huffman@44133 ` 125` ```lemma norm_gt_square: "norm(x) > a \ a < 0 \ x \ x > a^2" ``` huffman@44133 ` 126` ``` by (metis norm_le_square not_less) ``` huffman@44133 ` 127` huffman@44133 ` 128` ```text{* Dot product in terms of the norm rather than conversely. *} ``` huffman@44133 ` 129` huffman@44282 ` 130` ```lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left ``` huffman@44282 ` 131` ```inner_scaleR_left inner_scaleR_right ``` huffman@44133 ` 132` huffman@44133 ` 133` ```lemma dot_norm: "x \ y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2" ``` huffman@44133 ` 134` ``` unfolding power2_norm_eq_inner inner_simps inner_commute by auto ``` huffman@44133 ` 135` huffman@44133 ` 136` ```lemma dot_norm_neg: "x \ y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2" ``` huffman@44133 ` 137` ``` unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps) ``` huffman@44133 ` 138` huffman@44133 ` 139` ```text{* Equality of vectors in terms of @{term "op \"} products. *} ``` huffman@44133 ` 140` huffman@44133 ` 141` ```lemma vector_eq: "x = y \ x \ x = x \ y \ y \ y = x \ x" (is "?lhs \ ?rhs") ``` huffman@44133 ` 142` ```proof ``` huffman@44133 ` 143` ``` assume ?lhs then show ?rhs by simp ``` huffman@44133 ` 144` ```next ``` huffman@44133 ` 145` ``` assume ?rhs ``` huffman@44133 ` 146` ``` then have "x \ x - x \ y = 0 \ x \ y - y \ y = 0" by simp ``` huffman@44454 ` 147` ``` hence "x \ (x - y) = 0 \ y \ (x - y) = 0" by (simp add: inner_diff inner_commute) ``` huffman@44454 ` 148` ``` then have "(x - y) \ (x - y) = 0" by (simp add: field_simps inner_diff inner_commute) ``` huffman@44133 ` 149` ``` then show "x = y" by (simp) ``` huffman@44133 ` 150` ```qed ``` huffman@44133 ` 151` huffman@44133 ` 152` ```lemma norm_triangle_half_r: ``` huffman@44133 ` 153` ``` shows "norm (y - x1) < e / 2 \ norm (y - x2) < e / 2 \ norm (x1 - x2) < e" ``` huffman@44133 ` 154` ``` using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto ``` huffman@44133 ` 155` huffman@44133 ` 156` ```lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2" ``` huffman@44133 ` 157` ``` shows "norm (x - x') < e" ``` huffman@44133 ` 158` ``` using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]] ``` huffman@44133 ` 159` ``` unfolding dist_norm[THEN sym] . ``` huffman@44133 ` 160` huffman@44133 ` 161` ```lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e" ``` huffman@44133 ` 162` ``` by (metis order_trans norm_triangle_ineq) ``` huffman@44133 ` 163` huffman@44133 ` 164` ```lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e" ``` huffman@44133 ` 165` ``` by (metis basic_trans_rules(21) norm_triangle_ineq) ``` huffman@44133 ` 166` huffman@44133 ` 167` ```lemma setsum_clauses: ``` huffman@44133 ` 168` ``` shows "setsum f {} = 0" ``` huffman@44133 ` 169` ``` and "finite S \ setsum f (insert x S) = ``` huffman@44133 ` 170` ``` (if x \ S then setsum f S else f x + setsum f S)" ``` huffman@44133 ` 171` ``` by (auto simp add: insert_absorb) ``` huffman@44133 ` 172` huffman@44133 ` 173` ```lemma setsum_norm_le: ``` huffman@44133 ` 174` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` huffman@44176 ` 175` ``` assumes fg: "\x \ S. norm (f x) \ g x" ``` huffman@44133 ` 176` ``` shows "norm (setsum f S) \ setsum g S" ``` huffman@44176 ` 177` ``` by (rule order_trans [OF norm_setsum setsum_mono], simp add: fg) ``` huffman@44133 ` 178` huffman@44133 ` 179` ```lemma setsum_norm_bound: ``` huffman@44133 ` 180` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` huffman@44133 ` 181` ``` assumes fS: "finite S" ``` huffman@44133 ` 182` ``` and K: "\x \ S. norm (f x) \ K" ``` huffman@44133 ` 183` ``` shows "norm (setsum f S) \ of_nat (card S) * K" ``` huffman@44176 ` 184` ``` using setsum_norm_le[OF K] setsum_constant[symmetric] ``` huffman@44133 ` 185` ``` by simp ``` huffman@44133 ` 186` huffman@44133 ` 187` ```lemma setsum_group: ``` huffman@44133 ` 188` ``` assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \ T" ``` huffman@44133 ` 189` ``` shows "setsum (\y. setsum g {x. x\ S \ f x = y}) T = setsum g S" ``` huffman@44133 ` 190` ``` apply (subst setsum_image_gen[OF fS, of g f]) ``` huffman@44133 ` 191` ``` apply (rule setsum_mono_zero_right[OF fT fST]) ``` huffman@44133 ` 192` ``` by (auto intro: setsum_0') ``` huffman@44133 ` 193` huffman@44133 ` 194` ```lemma dot_lsum: "finite S \ setsum f S \ y = setsum (\x. f x \ y) S " ``` huffman@44454 ` 195` ``` apply(induct rule: finite_induct) by(auto simp add: inner_add) ``` huffman@44133 ` 196` huffman@44133 ` 197` ```lemma dot_rsum: "finite S \ y \ setsum f S = setsum (\x. y \ f x) S " ``` huffman@44454 ` 198` ``` apply(induct rule: finite_induct) by(auto simp add: inner_add) ``` huffman@44133 ` 199` huffman@44133 ` 200` ```lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" ``` huffman@44133 ` 201` ```proof ``` huffman@44133 ` 202` ``` assume "\x. x \ y = x \ z" ``` huffman@44454 ` 203` ``` hence "\x. x \ (y - z) = 0" by (simp add: inner_diff) ``` huffman@44133 ` 204` ``` hence "(y - z) \ (y - z) = 0" .. ``` huffman@44133 ` 205` ``` thus "y = z" by simp ``` huffman@44133 ` 206` ```qed simp ``` huffman@44133 ` 207` huffman@44133 ` 208` ```lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = y" ``` huffman@44133 ` 209` ```proof ``` huffman@44133 ` 210` ``` assume "\z. x \ z = y \ z" ``` huffman@44454 ` 211` ``` hence "\z. (x - y) \ z = 0" by (simp add: inner_diff) ``` huffman@44133 ` 212` ``` hence "(x - y) \ (x - y) = 0" .. ``` huffman@44133 ` 213` ``` thus "x = y" by simp ``` huffman@44133 ` 214` ```qed simp ``` huffman@44133 ` 215` huffman@44133 ` 216` ```subsection{* Orthogonality. *} ``` huffman@44133 ` 217` huffman@44133 ` 218` ```context real_inner ``` huffman@44133 ` 219` ```begin ``` huffman@44133 ` 220` huffman@44133 ` 221` ```definition "orthogonal x y \ (x \ y = 0)" ``` huffman@44133 ` 222` huffman@44133 ` 223` ```lemma orthogonal_clauses: ``` huffman@44133 ` 224` ``` "orthogonal a 0" ``` huffman@44133 ` 225` ``` "orthogonal a x \ orthogonal a (c *\<^sub>R x)" ``` huffman@44133 ` 226` ``` "orthogonal a x \ orthogonal a (-x)" ``` huffman@44133 ` 227` ``` "orthogonal a x \ orthogonal a y \ orthogonal a (x + y)" ``` huffman@44133 ` 228` ``` "orthogonal a x \ orthogonal a y \ orthogonal a (x - y)" ``` huffman@44133 ` 229` ``` "orthogonal 0 a" ``` huffman@44133 ` 230` ``` "orthogonal x a \ orthogonal (c *\<^sub>R x) a" ``` huffman@44133 ` 231` ``` "orthogonal x a \ orthogonal (-x) a" ``` huffman@44133 ` 232` ``` "orthogonal x a \ orthogonal y a \ orthogonal (x + y) a" ``` huffman@44133 ` 233` ``` "orthogonal x a \ orthogonal y a \ orthogonal (x - y) a" ``` huffman@44133 ` 234` ``` unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto ``` huffman@44133 ` 235` ``` ``` huffman@44133 ` 236` ```end ``` huffman@44133 ` 237` huffman@44133 ` 238` ```lemma orthogonal_commute: "orthogonal x y \ orthogonal y x" ``` huffman@44133 ` 239` ``` by (simp add: orthogonal_def inner_commute) ``` huffman@44133 ` 240` huffman@44133 ` 241` ```subsection{* Linear functions. *} ``` huffman@44133 ` 242` huffman@44133 ` 243` ```definition ``` huffman@44133 ` 244` ``` linear :: "('a::real_vector \ 'b::real_vector) \ bool" where ``` huffman@44133 ` 245` ``` "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *\<^sub>R x) = c *\<^sub>R f x)" ``` huffman@44133 ` 246` huffman@44133 ` 247` ```lemma linearI: assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" ``` huffman@44133 ` 248` ``` shows "linear f" using assms unfolding linear_def by auto ``` huffman@44133 ` 249` huffman@44133 ` 250` ```lemma linear_compose_cmul: "linear f ==> linear (\x. c *\<^sub>R f x)" ``` huffman@44133 ` 251` ``` by (simp add: linear_def algebra_simps) ``` huffman@44133 ` 252` huffman@44133 ` 253` ```lemma linear_compose_neg: "linear f ==> linear (\x. -(f(x)))" ``` huffman@44133 ` 254` ``` by (simp add: linear_def) ``` huffman@44133 ` 255` huffman@44133 ` 256` ```lemma linear_compose_add: "linear f \ linear g ==> linear (\x. f(x) + g(x))" ``` huffman@44133 ` 257` ``` by (simp add: linear_def algebra_simps) ``` huffman@44133 ` 258` huffman@44133 ` 259` ```lemma linear_compose_sub: "linear f \ linear g ==> linear (\x. f x - g x)" ``` huffman@44133 ` 260` ``` by (simp add: linear_def algebra_simps) ``` huffman@44133 ` 261` huffman@44133 ` 262` ```lemma linear_compose: "linear f \ linear g ==> linear (g o f)" ``` huffman@44133 ` 263` ``` by (simp add: linear_def) ``` huffman@44133 ` 264` huffman@44133 ` 265` ```lemma linear_id: "linear id" by (simp add: linear_def id_def) ``` huffman@44133 ` 266` huffman@44133 ` 267` ```lemma linear_zero: "linear (\x. 0)" by (simp add: linear_def) ``` huffman@44133 ` 268` huffman@44133 ` 269` ```lemma linear_compose_setsum: ``` huffman@44133 ` 270` ``` assumes fS: "finite S" and lS: "\a \ S. linear (f a)" ``` huffman@44133 ` 271` ``` shows "linear(\x. setsum (\a. f a x) S)" ``` huffman@44133 ` 272` ``` using lS ``` huffman@44133 ` 273` ``` apply (induct rule: finite_induct[OF fS]) ``` huffman@44133 ` 274` ``` by (auto simp add: linear_zero intro: linear_compose_add) ``` huffman@44133 ` 275` huffman@44133 ` 276` ```lemma linear_0: "linear f \ f 0 = 0" ``` huffman@44133 ` 277` ``` unfolding linear_def ``` huffman@44133 ` 278` ``` apply clarsimp ``` huffman@44133 ` 279` ``` apply (erule allE[where x="0::'a"]) ``` huffman@44133 ` 280` ``` apply simp ``` huffman@44133 ` 281` ``` done ``` huffman@44133 ` 282` huffman@44133 ` 283` ```lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" by (simp add: linear_def) ``` huffman@44133 ` 284` huffman@44133 ` 285` ```lemma linear_neg: "linear f ==> f (-x) = - f x" ``` huffman@44133 ` 286` ``` using linear_cmul [where c="-1"] by simp ``` huffman@44133 ` 287` huffman@44133 ` 288` ```lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def) ``` huffman@44133 ` 289` huffman@44133 ` 290` ```lemma linear_sub: "linear f ==> f(x - y) = f x - f y" ``` huffman@44133 ` 291` ``` by (simp add: diff_minus linear_add linear_neg) ``` huffman@44133 ` 292` huffman@44133 ` 293` ```lemma linear_setsum: ``` huffman@44133 ` 294` ``` assumes lf: "linear f" and fS: "finite S" ``` huffman@44133 ` 295` ``` shows "f (setsum g S) = setsum (f o g) S" ``` huffman@44133 ` 296` ```proof (induct rule: finite_induct[OF fS]) ``` huffman@44133 ` 297` ``` case 1 thus ?case by (simp add: linear_0[OF lf]) ``` huffman@44133 ` 298` ```next ``` huffman@44133 ` 299` ``` case (2 x F) ``` huffman@44133 ` 300` ``` have "f (setsum g (insert x F)) = f (g x + setsum g F)" using "2.hyps" ``` huffman@44133 ` 301` ``` by simp ``` huffman@44133 ` 302` ``` also have "\ = f (g x) + f (setsum g F)" using linear_add[OF lf] by simp ``` huffman@44133 ` 303` ``` also have "\ = setsum (f o g) (insert x F)" using "2.hyps" by simp ``` huffman@44133 ` 304` ``` finally show ?case . ``` huffman@44133 ` 305` ```qed ``` huffman@44133 ` 306` huffman@44133 ` 307` ```lemma linear_setsum_mul: ``` huffman@44133 ` 308` ``` assumes lf: "linear f" and fS: "finite S" ``` huffman@44133 ` 309` ``` shows "f (setsum (\i. c i *\<^sub>R v i) S) = setsum (\i. c i *\<^sub>R f (v i)) S" ``` huffman@44133 ` 310` ``` using linear_setsum[OF lf fS, of "\i. c i *\<^sub>R v i" , unfolded o_def] ``` huffman@44133 ` 311` ``` linear_cmul[OF lf] by simp ``` huffman@44133 ` 312` huffman@44133 ` 313` ```lemma linear_injective_0: ``` huffman@44133 ` 314` ``` assumes lf: "linear f" ``` huffman@44133 ` 315` ``` shows "inj f \ (\x. f x = 0 \ x = 0)" ``` huffman@44133 ` 316` ```proof- ``` huffman@44133 ` 317` ``` have "inj f \ (\ x y. f x = f y \ x = y)" by (simp add: inj_on_def) ``` huffman@44133 ` 318` ``` also have "\ \ (\ x y. f x - f y = 0 \ x - y = 0)" by simp ``` huffman@44133 ` 319` ``` also have "\ \ (\ x y. f (x - y) = 0 \ x - y = 0)" ``` huffman@44133 ` 320` ``` by (simp add: linear_sub[OF lf]) ``` huffman@44133 ` 321` ``` also have "\ \ (\ x. f x = 0 \ x = 0)" by auto ``` huffman@44133 ` 322` ``` finally show ?thesis . ``` huffman@44133 ` 323` ```qed ``` huffman@44133 ` 324` huffman@44133 ` 325` ```subsection{* Bilinear functions. *} ``` huffman@44133 ` 326` huffman@44133 ` 327` ```definition "bilinear f \ (\x. linear(\y. f x y)) \ (\y. linear(\x. f x y))" ``` huffman@44133 ` 328` huffman@44133 ` 329` ```lemma bilinear_ladd: "bilinear h ==> h (x + y) z = (h x z) + (h y z)" ``` huffman@44133 ` 330` ``` by (simp add: bilinear_def linear_def) ``` huffman@44133 ` 331` ```lemma bilinear_radd: "bilinear h ==> h x (y + z) = (h x y) + (h x z)" ``` huffman@44133 ` 332` ``` by (simp add: bilinear_def linear_def) ``` huffman@44133 ` 333` huffman@44133 ` 334` ```lemma bilinear_lmul: "bilinear h ==> h (c *\<^sub>R x) y = c *\<^sub>R (h x y)" ``` huffman@44133 ` 335` ``` by (simp add: bilinear_def linear_def) ``` huffman@44133 ` 336` huffman@44133 ` 337` ```lemma bilinear_rmul: "bilinear h ==> h x (c *\<^sub>R y) = c *\<^sub>R (h x y)" ``` huffman@44133 ` 338` ``` by (simp add: bilinear_def linear_def) ``` huffman@44133 ` 339` huffman@44133 ` 340` ```lemma bilinear_lneg: "bilinear h ==> h (- x) y = -(h x y)" ``` huffman@44133 ` 341` ``` by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul) ``` huffman@44133 ` 342` huffman@44133 ` 343` ```lemma bilinear_rneg: "bilinear h ==> h x (- y) = - h x y" ``` huffman@44133 ` 344` ``` by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul) ``` huffman@44133 ` 345` huffman@44133 ` 346` ```lemma (in ab_group_add) eq_add_iff: "x = x + y \ y = 0" ``` huffman@44133 ` 347` ``` using add_imp_eq[of x y 0] by auto ``` huffman@44133 ` 348` huffman@44133 ` 349` ```lemma bilinear_lzero: ``` huffman@44133 ` 350` ``` assumes bh: "bilinear h" shows "h 0 x = 0" ``` huffman@44133 ` 351` ``` using bilinear_ladd[OF bh, of 0 0 x] ``` huffman@44133 ` 352` ``` by (simp add: eq_add_iff field_simps) ``` huffman@44133 ` 353` huffman@44133 ` 354` ```lemma bilinear_rzero: ``` huffman@44133 ` 355` ``` assumes bh: "bilinear h" shows "h x 0 = 0" ``` huffman@44133 ` 356` ``` using bilinear_radd[OF bh, of x 0 0 ] ``` huffman@44133 ` 357` ``` by (simp add: eq_add_iff field_simps) ``` huffman@44133 ` 358` huffman@44133 ` 359` ```lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z" ``` huffman@44133 ` 360` ``` by (simp add: diff_minus bilinear_ladd bilinear_lneg) ``` huffman@44133 ` 361` huffman@44133 ` 362` ```lemma bilinear_rsub: "bilinear h ==> h z (x - y) = h z x - h z y" ``` huffman@44133 ` 363` ``` by (simp add: diff_minus bilinear_radd bilinear_rneg) ``` huffman@44133 ` 364` huffman@44133 ` 365` ```lemma bilinear_setsum: ``` huffman@44133 ` 366` ``` assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T" ``` huffman@44133 ` 367` ``` shows "h (setsum f S) (setsum g T) = setsum (\(i,j). h (f i) (g j)) (S \ T) " ``` huffman@44133 ` 368` ```proof- ``` huffman@44133 ` 369` ``` have "h (setsum f S) (setsum g T) = setsum (\x. h (f x) (setsum g T)) S" ``` huffman@44133 ` 370` ``` apply (rule linear_setsum[unfolded o_def]) ``` huffman@44133 ` 371` ``` using bh fS by (auto simp add: bilinear_def) ``` huffman@44133 ` 372` ``` also have "\ = setsum (\x. setsum (\y. h (f x) (g y)) T) S" ``` huffman@44133 ` 373` ``` apply (rule setsum_cong, simp) ``` huffman@44133 ` 374` ``` apply (rule linear_setsum[unfolded o_def]) ``` huffman@44133 ` 375` ``` using bh fT by (auto simp add: bilinear_def) ``` huffman@44133 ` 376` ``` finally show ?thesis unfolding setsum_cartesian_product . ``` huffman@44133 ` 377` ```qed ``` huffman@44133 ` 378` huffman@44133 ` 379` ```subsection{* Adjoints. *} ``` huffman@44133 ` 380` huffman@44133 ` 381` ```definition "adjoint f = (SOME f'. \x y. f x \ y = x \ f' y)" ``` huffman@44133 ` 382` huffman@44133 ` 383` ```lemma adjoint_unique: ``` huffman@44133 ` 384` ``` assumes "\x y. inner (f x) y = inner x (g y)" ``` huffman@44133 ` 385` ``` shows "adjoint f = g" ``` huffman@44133 ` 386` ```unfolding adjoint_def ``` huffman@44133 ` 387` ```proof (rule some_equality) ``` huffman@44133 ` 388` ``` show "\x y. inner (f x) y = inner x (g y)" using assms . ``` huffman@44133 ` 389` ```next ``` huffman@44133 ` 390` ``` fix h assume "\x y. inner (f x) y = inner x (h y)" ``` huffman@44133 ` 391` ``` hence "\x y. inner x (g y) = inner x (h y)" using assms by simp ``` huffman@44133 ` 392` ``` hence "\x y. inner x (g y - h y) = 0" by (simp add: inner_diff_right) ``` huffman@44133 ` 393` ``` hence "\y. inner (g y - h y) (g y - h y) = 0" by simp ``` huffman@44133 ` 394` ``` hence "\y. h y = g y" by simp ``` huffman@44133 ` 395` ``` thus "h = g" by (simp add: ext) ``` huffman@44133 ` 396` ```qed ``` huffman@44133 ` 397` huffman@44133 ` 398` ```lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis ``` huffman@44133 ` 399` huffman@44133 ` 400` ```subsection{* Interlude: Some properties of real sets *} ``` huffman@44133 ` 401` huffman@44133 ` 402` ```lemma seq_mono_lemma: assumes "\(n::nat) \ m. (d n :: real) < e n" and "\n \ m. e n <= e m" ``` huffman@44133 ` 403` ``` shows "\n \ m. d n < e m" ``` huffman@44133 ` 404` ``` using assms apply auto ``` huffman@44133 ` 405` ``` apply (erule_tac x="n" in allE) ``` huffman@44133 ` 406` ``` apply (erule_tac x="n" in allE) ``` huffman@44133 ` 407` ``` apply auto ``` huffman@44133 ` 408` ``` done ``` huffman@44133 ` 409` huffman@44133 ` 410` huffman@44133 ` 411` ```lemma infinite_enumerate: assumes fS: "infinite S" ``` huffman@44133 ` 412` ``` shows "\r. subseq r \ (\n. r n \ S)" ``` huffman@44133 ` 413` ```unfolding subseq_def ``` huffman@44133 ` 414` ```using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto ``` huffman@44133 ` 415` huffman@44133 ` 416` ```lemma approachable_lt_le: "(\(d::real)>0. \x. f x < d \ P x) \ (\d>0. \x. f x \ d \ P x)" ``` huffman@44133 ` 417` ```apply auto ``` huffman@44133 ` 418` ```apply (rule_tac x="d/2" in exI) ``` huffman@44133 ` 419` ```apply auto ``` huffman@44133 ` 420` ```done ``` huffman@44133 ` 421` huffman@44133 ` 422` huffman@44133 ` 423` ```lemma triangle_lemma: ``` huffman@44133 ` 424` ``` assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2" ``` huffman@44133 ` 425` ``` shows "x <= y + z" ``` huffman@44133 ` 426` ```proof- ``` huffman@44133 ` 427` ``` have "y^2 + z^2 \ y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg) ``` huffman@44133 ` 428` ``` with xy have th: "x ^2 \ (y+z)^2" by (simp add: power2_eq_square field_simps) ``` huffman@44133 ` 429` ``` from y z have yz: "y + z \ 0" by arith ``` huffman@44133 ` 430` ``` from power2_le_imp_le[OF th yz] show ?thesis . ``` huffman@44133 ` 431` ```qed ``` huffman@44133 ` 432` huffman@44133 ` 433` ```text {* TODO: move to NthRoot *} ``` huffman@44133 ` 434` ```lemma sqrt_add_le_add_sqrt: ``` huffman@44133 ` 435` ``` assumes x: "0 \ x" and y: "0 \ y" ``` huffman@44133 ` 436` ``` shows "sqrt (x + y) \ sqrt x + sqrt y" ``` huffman@44133 ` 437` ```apply (rule power2_le_imp_le) ``` huffman@44142 ` 438` ```apply (simp add: real_sum_squared_expand x y) ``` huffman@44133 ` 439` ```apply (simp add: mult_nonneg_nonneg x y) ``` huffman@44142 ` 440` ```apply (simp add: x y) ``` huffman@44133 ` 441` ```done ``` huffman@44133 ` 442` huffman@44133 ` 443` ```subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *} ``` huffman@44133 ` 444` huffman@44170 ` 445` ```definition hull :: "('a set \ bool) \ 'a set \ 'a set" (infixl "hull" 75) where ``` huffman@44170 ` 446` ``` "S hull s = Inter {t. S t \ s \ t}" ``` huffman@44170 ` 447` huffman@44170 ` 448` ```lemma hull_same: "S s \ S hull s = s" ``` huffman@44133 ` 449` ``` unfolding hull_def by auto ``` huffman@44133 ` 450` huffman@44170 ` 451` ```lemma hull_in: "(\T. Ball T S ==> S (Inter T)) ==> S (S hull s)" ``` huffman@44170 ` 452` ```unfolding hull_def Ball_def by auto ``` huffman@44170 ` 453` huffman@44170 ` 454` ```lemma hull_eq: "(\T. Ball T S ==> S (Inter T)) ==> (S hull s) = s \ S s" ``` huffman@44170 ` 455` ```using hull_same[of S s] hull_in[of S s] by metis ``` huffman@44133 ` 456` huffman@44133 ` 457` huffman@44133 ` 458` ```lemma hull_hull: "S hull (S hull s) = S hull s" ``` huffman@44133 ` 459` ``` unfolding hull_def by blast ``` huffman@44133 ` 460` huffman@44133 ` 461` ```lemma hull_subset[intro]: "s \ (S hull s)" ``` huffman@44133 ` 462` ``` unfolding hull_def by blast ``` huffman@44133 ` 463` huffman@44133 ` 464` ```lemma hull_mono: " s \ t ==> (S hull s) \ (S hull t)" ``` huffman@44133 ` 465` ``` unfolding hull_def by blast ``` huffman@44133 ` 466` huffman@44170 ` 467` ```lemma hull_antimono: "\x. S x \ T x ==> (T hull s) \ (S hull s)" ``` huffman@44133 ` 468` ``` unfolding hull_def by blast ``` huffman@44133 ` 469` huffman@44170 ` 470` ```lemma hull_minimal: "s \ t \ S t ==> (S hull s) \ t" ``` huffman@44133 ` 471` ``` unfolding hull_def by blast ``` huffman@44133 ` 472` huffman@44170 ` 473` ```lemma subset_hull: "S t ==> S hull s \ t \ s \ t" ``` huffman@44133 ` 474` ``` unfolding hull_def by blast ``` huffman@44133 ` 475` huffman@44170 ` 476` ```lemma hull_unique: "s \ t \ S t \ (\t'. s \ t' \ S t' ==> t \ t') ``` huffman@44133 ` 477` ``` ==> (S hull s = t)" ``` huffman@44133 ` 478` ```unfolding hull_def by auto ``` huffman@44133 ` 479` huffman@44133 ` 480` ```lemma hull_induct: "(\x. x\ S \ P x) \ Q {x. P x} \ \x\ Q hull S. P x" ``` huffman@44133 ` 481` ``` using hull_minimal[of S "{x. P x}" Q] ``` huffman@44170 ` 482` ``` by (auto simp add: subset_eq) ``` huffman@44133 ` 483` huffman@44133 ` 484` ```lemma hull_inc: "x \ S \ x \ P hull S" by (metis hull_subset subset_eq) ``` huffman@44133 ` 485` huffman@44133 ` 486` ```lemma hull_union_subset: "(S hull s) \ (S hull t) \ (S hull (s \ t))" ``` huffman@44133 ` 487` ```unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2) ``` huffman@44133 ` 488` huffman@44170 ` 489` ```lemma hull_union: assumes T: "\T. Ball T S ==> S (Inter T)" ``` huffman@44133 ` 490` ``` shows "S hull (s \ t) = S hull (S hull s \ S hull t)" ``` huffman@44133 ` 491` ```apply rule ``` huffman@44133 ` 492` ```apply (rule hull_mono) ``` huffman@44133 ` 493` ```unfolding Un_subset_iff ``` huffman@44133 ` 494` ```apply (metis hull_subset Un_upper1 Un_upper2 subset_trans) ``` huffman@44133 ` 495` ```apply (rule hull_minimal) ``` huffman@44133 ` 496` ```apply (metis hull_union_subset) ``` huffman@44133 ` 497` ```apply (metis hull_in T) ``` huffman@44133 ` 498` ```done ``` huffman@44133 ` 499` huffman@44133 ` 500` ```lemma hull_redundant_eq: "a \ (S hull s) \ (S hull (insert a s) = S hull s)" ``` huffman@44133 ` 501` ``` unfolding hull_def by blast ``` huffman@44133 ` 502` huffman@44133 ` 503` ```lemma hull_redundant: "a \ (S hull s) ==> (S hull (insert a s) = S hull s)" ``` huffman@44133 ` 504` ```by (metis hull_redundant_eq) ``` huffman@44133 ` 505` huffman@44133 ` 506` ```text{* Archimedian properties and useful consequences. *} ``` huffman@44133 ` 507` huffman@44133 ` 508` ```lemma real_arch_simple: "\n. x <= real (n::nat)" ``` huffman@44133 ` 509` ``` using reals_Archimedean2[of x] apply auto by (rule_tac x="Suc n" in exI, auto) ``` huffman@44133 ` 510` ```lemmas real_arch_lt = reals_Archimedean2 ``` huffman@44133 ` 511` huffman@44133 ` 512` ```lemmas real_arch = reals_Archimedean3 ``` huffman@44133 ` 513` huffman@44133 ` 514` ```lemma real_arch_inv: "0 < e \ (\n::nat. n \ 0 \ 0 < inverse (real n) \ inverse (real n) < e)" ``` huffman@44133 ` 515` ``` using reals_Archimedean ``` huffman@44133 ` 516` ``` apply (auto simp add: field_simps) ``` huffman@44133 ` 517` ``` apply (subgoal_tac "inverse (real n) > 0") ``` huffman@44133 ` 518` ``` apply arith ``` huffman@44133 ` 519` ``` apply simp ``` huffman@44133 ` 520` ``` done ``` huffman@44133 ` 521` huffman@44133 ` 522` ```lemma real_pow_lbound: "0 <= x ==> 1 + real n * x <= (1 + x) ^ n" ``` huffman@44133 ` 523` ```proof(induct n) ``` huffman@44133 ` 524` ``` case 0 thus ?case by simp ``` huffman@44133 ` 525` ```next ``` huffman@44133 ` 526` ``` case (Suc n) ``` huffman@44133 ` 527` ``` hence h: "1 + real n * x \ (1 + x) ^ n" by simp ``` huffman@44133 ` 528` ``` from h have p: "1 \ (1 + x) ^ n" using Suc.prems by simp ``` huffman@44133 ` 529` ``` from h have "1 + real n * x + x \ (1 + x) ^ n + x" by simp ``` huffman@44133 ` 530` ``` also have "\ \ (1 + x) ^ Suc n" apply (subst diff_le_0_iff_le[symmetric]) ``` huffman@44133 ` 531` ``` apply (simp add: field_simps) ``` huffman@44133 ` 532` ``` using mult_left_mono[OF p Suc.prems] by simp ``` huffman@44133 ` 533` ``` finally show ?case by (simp add: real_of_nat_Suc field_simps) ``` huffman@44133 ` 534` ```qed ``` huffman@44133 ` 535` huffman@44133 ` 536` ```lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\n. y < x^n" ``` huffman@44133 ` 537` ```proof- ``` huffman@44133 ` 538` ``` from x have x0: "x - 1 > 0" by arith ``` huffman@44133 ` 539` ``` from real_arch[OF x0, rule_format, of y] ``` huffman@44133 ` 540` ``` obtain n::nat where n:"y < real n * (x - 1)" by metis ``` huffman@44133 ` 541` ``` from x0 have x00: "x- 1 \ 0" by arith ``` huffman@44133 ` 542` ``` from real_pow_lbound[OF x00, of n] n ``` huffman@44133 ` 543` ``` have "y < x^n" by auto ``` huffman@44133 ` 544` ``` then show ?thesis by metis ``` huffman@44133 ` 545` ```qed ``` huffman@44133 ` 546` huffman@44133 ` 547` ```lemma real_arch_pow2: "\n. (x::real) < 2^ n" ``` huffman@44133 ` 548` ``` using real_arch_pow[of 2 x] by simp ``` huffman@44133 ` 549` huffman@44133 ` 550` ```lemma real_arch_pow_inv: assumes y: "(y::real) > 0" and x1: "x < 1" ``` huffman@44133 ` 551` ``` shows "\n. x^n < y" ``` huffman@44133 ` 552` ```proof- ``` huffman@44133 ` 553` ``` {assume x0: "x > 0" ``` huffman@44133 ` 554` ``` from x0 x1 have ix: "1 < 1/x" by (simp add: field_simps) ``` huffman@44133 ` 555` ``` from real_arch_pow[OF ix, of "1/y"] ``` huffman@44133 ` 556` ``` obtain n where n: "1/y < (1/x)^n" by blast ``` huffman@44133 ` 557` ``` then ``` huffman@44133 ` 558` ``` have ?thesis using y x0 by (auto simp add: field_simps power_divide) } ``` huffman@44133 ` 559` ``` moreover ``` huffman@44133 ` 560` ``` {assume "\ x > 0" with y x1 have ?thesis apply auto by (rule exI[where x=1], auto)} ``` huffman@44133 ` 561` ``` ultimately show ?thesis by metis ``` huffman@44133 ` 562` ```qed ``` huffman@44133 ` 563` huffman@44133 ` 564` ```lemma forall_pos_mono: "(\d e::real. d < e \ P d ==> P e) \ (\n::nat. n \ 0 ==> P(inverse(real n))) \ (\e. 0 < e ==> P e)" ``` huffman@44133 ` 565` ``` by (metis real_arch_inv) ``` huffman@44133 ` 566` huffman@44133 ` 567` ```lemma forall_pos_mono_1: "(\d e::real. d < e \ P d ==> P e) \ (\n. P(inverse(real (Suc n)))) ==> 0 < e ==> P e" ``` huffman@44133 ` 568` ``` apply (rule forall_pos_mono) ``` huffman@44133 ` 569` ``` apply auto ``` huffman@44133 ` 570` ``` apply (atomize) ``` huffman@44133 ` 571` ``` apply (erule_tac x="n - 1" in allE) ``` huffman@44133 ` 572` ``` apply auto ``` huffman@44133 ` 573` ``` done ``` huffman@44133 ` 574` huffman@44133 ` 575` ```lemma real_archimedian_rdiv_eq_0: assumes x0: "x \ 0" and c: "c \ 0" and xc: "\(m::nat)>0. real m * x \ c" ``` huffman@44133 ` 576` ``` shows "x = 0" ``` huffman@44133 ` 577` ```proof- ``` huffman@44133 ` 578` ``` {assume "x \ 0" with x0 have xp: "x > 0" by arith ``` huffman@44133 ` 579` ``` from real_arch[OF xp, rule_format, of c] obtain n::nat where n: "c < real n * x" by blast ``` huffman@44133 ` 580` ``` with xc[rule_format, of n] have "n = 0" by arith ``` huffman@44133 ` 581` ``` with n c have False by simp} ``` huffman@44133 ` 582` ``` then show ?thesis by blast ``` huffman@44133 ` 583` ```qed ``` huffman@44133 ` 584` huffman@44133 ` 585` ```subsection{* A bit of linear algebra. *} ``` huffman@44133 ` 586` huffman@44133 ` 587` ```definition (in real_vector) ``` huffman@44133 ` 588` ``` subspace :: "'a set \ bool" where ``` huffman@44133 ` 589` ``` "subspace S \ 0 \ S \ (\x\ S. \y \S. x + y \ S) \ (\c. \x \S. c *\<^sub>R x \S )" ``` huffman@44133 ` 590` huffman@44133 ` 591` ```definition (in real_vector) "span S = (subspace hull S)" ``` huffman@44133 ` 592` ```definition (in real_vector) "dependent S \ (\a \ S. a \ span(S - {a}))" ``` huffman@44133 ` 593` ```abbreviation (in real_vector) "independent s == ~(dependent s)" ``` huffman@44133 ` 594` huffman@44133 ` 595` ```text {* Closure properties of subspaces. *} ``` huffman@44133 ` 596` huffman@44133 ` 597` ```lemma subspace_UNIV[simp]: "subspace(UNIV)" by (simp add: subspace_def) ``` huffman@44133 ` 598` huffman@44133 ` 599` ```lemma (in real_vector) subspace_0: "subspace S ==> 0 \ S" by (metis subspace_def) ``` huffman@44133 ` 600` huffman@44133 ` 601` ```lemma (in real_vector) subspace_add: "subspace S \ x \ S \ y \ S ==> x + y \ S" ``` huffman@44133 ` 602` ``` by (metis subspace_def) ``` huffman@44133 ` 603` huffman@44133 ` 604` ```lemma (in real_vector) subspace_mul: "subspace S \ x \ S \ c *\<^sub>R x \ S" ``` huffman@44133 ` 605` ``` by (metis subspace_def) ``` huffman@44133 ` 606` huffman@44133 ` 607` ```lemma subspace_neg: "subspace S \ x \ S \ - x \ S" ``` huffman@44133 ` 608` ``` by (metis scaleR_minus1_left subspace_mul) ``` huffman@44133 ` 609` huffman@44133 ` 610` ```lemma subspace_sub: "subspace S \ x \ S \ y \ S \ x - y \ S" ``` huffman@44133 ` 611` ``` by (metis diff_minus subspace_add subspace_neg) ``` huffman@44133 ` 612` huffman@44133 ` 613` ```lemma (in real_vector) subspace_setsum: ``` huffman@44133 ` 614` ``` assumes sA: "subspace A" and fB: "finite B" ``` huffman@44133 ` 615` ``` and f: "\x\ B. f x \ A" ``` huffman@44133 ` 616` ``` shows "setsum f B \ A" ``` huffman@44133 ` 617` ``` using fB f sA ``` huffman@44133 ` 618` ``` apply(induct rule: finite_induct[OF fB]) ``` huffman@44133 ` 619` ``` by (simp add: subspace_def sA, auto simp add: sA subspace_add) ``` huffman@44133 ` 620` huffman@44133 ` 621` ```lemma subspace_linear_image: ``` huffman@44133 ` 622` ``` assumes lf: "linear f" and sS: "subspace S" ``` huffman@44133 ` 623` ``` shows "subspace(f ` S)" ``` huffman@44133 ` 624` ``` using lf sS linear_0[OF lf] ``` huffman@44133 ` 625` ``` unfolding linear_def subspace_def ``` huffman@44133 ` 626` ``` apply (auto simp add: image_iff) ``` huffman@44133 ` 627` ``` apply (rule_tac x="x + y" in bexI, auto) ``` huffman@44133 ` 628` ``` apply (rule_tac x="c *\<^sub>R x" in bexI, auto) ``` huffman@44133 ` 629` ``` done ``` huffman@44133 ` 630` huffman@44521 ` 631` ```lemma subspace_linear_vimage: "linear f \ subspace S \ subspace (f -` S)" ``` huffman@44521 ` 632` ``` by (auto simp add: subspace_def linear_def linear_0[of f]) ``` huffman@44521 ` 633` huffman@44133 ` 634` ```lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \ S}" ``` huffman@44133 ` 635` ``` by (auto simp add: subspace_def linear_def linear_0[of f]) ``` huffman@44133 ` 636` huffman@44133 ` 637` ```lemma subspace_trivial: "subspace {0}" ``` huffman@44133 ` 638` ``` by (simp add: subspace_def) ``` huffman@44133 ` 639` huffman@44133 ` 640` ```lemma (in real_vector) subspace_inter: "subspace A \ subspace B ==> subspace (A \ B)" ``` huffman@44133 ` 641` ``` by (simp add: subspace_def) ``` huffman@44133 ` 642` huffman@44521 ` 643` ```lemma subspace_Times: "\subspace A; subspace B\ \ subspace (A \ B)" ``` huffman@44521 ` 644` ``` unfolding subspace_def zero_prod_def by simp ``` huffman@44521 ` 645` huffman@44521 ` 646` ```text {* Properties of span. *} ``` huffman@44521 ` 647` huffman@44133 ` 648` ```lemma (in real_vector) span_mono: "A \ B ==> span A \ span B" ``` huffman@44133 ` 649` ``` by (metis span_def hull_mono) ``` huffman@44133 ` 650` huffman@44133 ` 651` ```lemma (in real_vector) subspace_span: "subspace(span S)" ``` huffman@44133 ` 652` ``` unfolding span_def ``` huffman@44170 ` 653` ``` apply (rule hull_in) ``` huffman@44133 ` 654` ``` apply (simp only: subspace_def Inter_iff Int_iff subset_eq) ``` huffman@44133 ` 655` ``` apply auto ``` huffman@44133 ` 656` ``` done ``` huffman@44133 ` 657` huffman@44133 ` 658` ```lemma (in real_vector) span_clauses: ``` huffman@44133 ` 659` ``` "a \ S ==> a \ span S" ``` huffman@44133 ` 660` ``` "0 \ span S" ``` huffman@44133 ` 661` ``` "x\ span S \ y \ span S ==> x + y \ span S" ``` huffman@44133 ` 662` ``` "x \ span S \ c *\<^sub>R x \ span S" ``` huffman@44133 ` 663` ``` by (metis span_def hull_subset subset_eq) ``` huffman@44133 ` 664` ``` (metis subspace_span subspace_def)+ ``` huffman@44133 ` 665` huffman@44521 ` 666` ```lemma span_unique: ``` huffman@44521 ` 667` ``` "\S \ T; subspace T; \T'. \S \ T'; subspace T'\ \ T \ T'\ \ span S = T" ``` huffman@44521 ` 668` ``` unfolding span_def by (rule hull_unique) ``` huffman@44521 ` 669` huffman@44521 ` 670` ```lemma span_minimal: "S \ T \ subspace T \ span S \ T" ``` huffman@44521 ` 671` ``` unfolding span_def by (rule hull_minimal) ``` huffman@44521 ` 672` huffman@44521 ` 673` ```lemma (in real_vector) span_induct: ``` huffman@44521 ` 674` ``` assumes x: "x \ span S" and P: "subspace P" and SP: "\x. x \ S ==> x \ P" ``` huffman@44521 ` 675` ``` shows "x \ P" ``` huffman@44133 ` 676` ```proof- ``` huffman@44170 ` 677` ``` from SP have SP': "S \ P" by (simp add: subset_eq) ``` huffman@44170 ` 678` ``` from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]] ``` huffman@44170 ` 679` ``` show "x \ P" by (metis subset_eq) ``` huffman@44133 ` 680` ```qed ``` huffman@44133 ` 681` huffman@44133 ` 682` ```lemma span_empty[simp]: "span {} = {0}" ``` huffman@44133 ` 683` ``` apply (simp add: span_def) ``` huffman@44133 ` 684` ``` apply (rule hull_unique) ``` huffman@44170 ` 685` ``` apply (auto simp add: subspace_def) ``` huffman@44133 ` 686` ``` done ``` huffman@44133 ` 687` huffman@44133 ` 688` ```lemma (in real_vector) independent_empty[intro]: "independent {}" ``` huffman@44133 ` 689` ``` by (simp add: dependent_def) ``` huffman@44133 ` 690` huffman@44133 ` 691` ```lemma dependent_single[simp]: ``` huffman@44133 ` 692` ``` "dependent {x} \ x = 0" ``` huffman@44133 ` 693` ``` unfolding dependent_def by auto ``` huffman@44133 ` 694` huffman@44133 ` 695` ```lemma (in real_vector) independent_mono: "independent A \ B \ A ==> independent B" ``` huffman@44133 ` 696` ``` apply (clarsimp simp add: dependent_def span_mono) ``` huffman@44133 ` 697` ``` apply (subgoal_tac "span (B - {a}) \ span (A - {a})") ``` huffman@44133 ` 698` ``` apply force ``` huffman@44133 ` 699` ``` apply (rule span_mono) ``` huffman@44133 ` 700` ``` apply auto ``` huffman@44133 ` 701` ``` done ``` huffman@44133 ` 702` huffman@44133 ` 703` ```lemma (in real_vector) span_subspace: "A \ B \ B \ span A \ subspace B \ span A = B" ``` huffman@44170 ` 704` ``` by (metis order_antisym span_def hull_minimal) ``` huffman@44133 ` 705` huffman@44133 ` 706` ```lemma (in real_vector) span_induct': assumes SP: "\x \ S. P x" ``` huffman@44170 ` 707` ``` and P: "subspace {x. P x}" shows "\x \ span S. P x" ``` huffman@44133 ` 708` ``` using span_induct SP P by blast ``` huffman@44133 ` 709` huffman@44170 ` 710` ```inductive_set (in real_vector) span_induct_alt_help for S:: "'a set" ``` huffman@44133 ` 711` ``` where ``` huffman@44170 ` 712` ``` span_induct_alt_help_0: "0 \ span_induct_alt_help S" ``` huffman@44170 ` 713` ``` | span_induct_alt_help_S: "x \ S \ z \ span_induct_alt_help S \ (c *\<^sub>R x + z) \ span_induct_alt_help S" ``` huffman@44133 ` 714` huffman@44133 ` 715` ```lemma span_induct_alt': ``` huffman@44133 ` 716` ``` assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" shows "\x \ span S. h x" ``` huffman@44133 ` 717` ```proof- ``` huffman@44170 ` 718` ``` {fix x:: "'a" assume x: "x \ span_induct_alt_help S" ``` huffman@44133 ` 719` ``` have "h x" ``` huffman@44133 ` 720` ``` apply (rule span_induct_alt_help.induct[OF x]) ``` huffman@44133 ` 721` ``` apply (rule h0) ``` huffman@44133 ` 722` ``` apply (rule hS, assumption, assumption) ``` huffman@44133 ` 723` ``` done} ``` huffman@44133 ` 724` ``` note th0 = this ``` huffman@44133 ` 725` ``` {fix x assume x: "x \ span S" ``` huffman@44133 ` 726` huffman@44170 ` 727` ``` have "x \ span_induct_alt_help S" ``` huffman@44133 ` 728` ``` proof(rule span_induct[where x=x and S=S]) ``` huffman@44133 ` 729` ``` show "x \ span S" using x . ``` huffman@44133 ` 730` ``` next ``` huffman@44133 ` 731` ``` fix x assume xS : "x \ S" ``` huffman@44133 ` 732` ``` from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1] ``` huffman@44170 ` 733` ``` show "x \ span_induct_alt_help S" by simp ``` huffman@44133 ` 734` ``` next ``` huffman@44170 ` 735` ``` have "0 \ span_induct_alt_help S" by (rule span_induct_alt_help_0) ``` huffman@44133 ` 736` ``` moreover ``` huffman@44170 ` 737` ``` {fix x y assume h: "x \ span_induct_alt_help S" "y \ span_induct_alt_help S" ``` huffman@44133 ` 738` ``` from h ``` huffman@44170 ` 739` ``` have "(x + y) \ span_induct_alt_help S" ``` huffman@44133 ` 740` ``` apply (induct rule: span_induct_alt_help.induct) ``` huffman@44133 ` 741` ``` apply simp ``` huffman@44133 ` 742` ``` unfolding add_assoc ``` huffman@44133 ` 743` ``` apply (rule span_induct_alt_help_S) ``` huffman@44133 ` 744` ``` apply assumption ``` huffman@44133 ` 745` ``` apply simp ``` huffman@44133 ` 746` ``` done} ``` huffman@44133 ` 747` ``` moreover ``` huffman@44170 ` 748` ``` {fix c x assume xt: "x \ span_induct_alt_help S" ``` huffman@44170 ` 749` ``` then have "(c *\<^sub>R x) \ span_induct_alt_help S" ``` huffman@44133 ` 750` ``` apply (induct rule: span_induct_alt_help.induct) ``` huffman@44133 ` 751` ``` apply (simp add: span_induct_alt_help_0) ``` huffman@44133 ` 752` ``` apply (simp add: scaleR_right_distrib) ``` huffman@44133 ` 753` ``` apply (rule span_induct_alt_help_S) ``` huffman@44133 ` 754` ``` apply assumption ``` huffman@44133 ` 755` ``` apply simp ``` huffman@44133 ` 756` ``` done ``` huffman@44133 ` 757` ``` } ``` huffman@44133 ` 758` ``` ultimately show "subspace (span_induct_alt_help S)" ``` huffman@44170 ` 759` ``` unfolding subspace_def Ball_def by blast ``` huffman@44133 ` 760` ``` qed} ``` huffman@44133 ` 761` ``` with th0 show ?thesis by blast ``` huffman@44133 ` 762` ```qed ``` huffman@44133 ` 763` huffman@44133 ` 764` ```lemma span_induct_alt: ``` huffman@44133 ` 765` ``` assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" and x: "x \ span S" ``` huffman@44133 ` 766` ``` shows "h x" ``` huffman@44133 ` 767` ```using span_induct_alt'[of h S] h0 hS x by blast ``` huffman@44133 ` 768` huffman@44133 ` 769` ```text {* Individual closure properties. *} ``` huffman@44133 ` 770` huffman@44133 ` 771` ```lemma span_span: "span (span A) = span A" ``` huffman@44133 ` 772` ``` unfolding span_def hull_hull .. ``` huffman@44133 ` 773` huffman@44133 ` 774` ```lemma (in real_vector) span_superset: "x \ S ==> x \ span S" by (metis span_clauses(1)) ``` huffman@44133 ` 775` huffman@44133 ` 776` ```lemma (in real_vector) span_0: "0 \ span S" by (metis subspace_span subspace_0) ``` huffman@44133 ` 777` huffman@44133 ` 778` ```lemma span_inc: "S \ span S" ``` huffman@44133 ` 779` ``` by (metis subset_eq span_superset) ``` huffman@44133 ` 780` huffman@44133 ` 781` ```lemma (in real_vector) dependent_0: assumes "0\A" shows "dependent A" ``` huffman@44133 ` 782` ``` unfolding dependent_def apply(rule_tac x=0 in bexI) ``` huffman@44133 ` 783` ``` using assms span_0 by auto ``` huffman@44133 ` 784` huffman@44133 ` 785` ```lemma (in real_vector) span_add: "x \ span S \ y \ span S ==> x + y \ span S" ``` huffman@44133 ` 786` ``` by (metis subspace_add subspace_span) ``` huffman@44133 ` 787` huffman@44133 ` 788` ```lemma (in real_vector) span_mul: "x \ span S ==> (c *\<^sub>R x) \ span S" ``` huffman@44133 ` 789` ``` by (metis subspace_span subspace_mul) ``` huffman@44133 ` 790` huffman@44133 ` 791` ```lemma span_neg: "x \ span S ==> - x \ span S" ``` huffman@44133 ` 792` ``` by (metis subspace_neg subspace_span) ``` huffman@44133 ` 793` huffman@44133 ` 794` ```lemma span_sub: "x \ span S \ y \ span S ==> x - y \ span S" ``` huffman@44133 ` 795` ``` by (metis subspace_span subspace_sub) ``` huffman@44133 ` 796` huffman@44133 ` 797` ```lemma (in real_vector) span_setsum: "finite A \ \x \ A. f x \ span S ==> setsum f A \ span S" ``` huffman@44133 ` 798` ``` by (rule subspace_setsum, rule subspace_span) ``` huffman@44133 ` 799` huffman@44133 ` 800` ```lemma span_add_eq: "x \ span S \ x + y \ span S \ y \ span S" ``` huffman@44133 ` 801` ``` apply (auto simp only: span_add span_sub) ``` huffman@44133 ` 802` ``` apply (subgoal_tac "(x + y) - x \ span S", simp) ``` huffman@44133 ` 803` ``` by (simp only: span_add span_sub) ``` huffman@44133 ` 804` huffman@44133 ` 805` ```text {* Mapping under linear image. *} ``` huffman@44133 ` 806` huffman@44521 ` 807` ```lemma image_subset_iff_subset_vimage: "f ` A \ B \ A \ f -` B" ``` huffman@44521 ` 808` ``` by auto (* TODO: move *) ``` huffman@44521 ` 809` huffman@44521 ` 810` ```lemma span_linear_image: ``` huffman@44521 ` 811` ``` assumes lf: "linear f" ``` huffman@44133 ` 812` ``` shows "span (f ` S) = f ` (span S)" ``` huffman@44521 ` 813` ```proof (rule span_unique) ``` huffman@44521 ` 814` ``` show "f ` S \ f ` span S" ``` huffman@44521 ` 815` ``` by (intro image_mono span_inc) ``` huffman@44521 ` 816` ``` show "subspace (f ` span S)" ``` huffman@44521 ` 817` ``` using lf subspace_span by (rule subspace_linear_image) ``` huffman@44521 ` 818` ```next ``` huffman@44521 ` 819` ``` fix T assume "f ` S \ T" and "subspace T" thus "f ` span S \ T" ``` huffman@44521 ` 820` ``` unfolding image_subset_iff_subset_vimage ``` huffman@44521 ` 821` ``` by (intro span_minimal subspace_linear_vimage lf) ``` huffman@44521 ` 822` ```qed ``` huffman@44521 ` 823` huffman@44521 ` 824` ```lemma span_union: "span (A \ B) = (\(a, b). a + b) ` (span A \ span B)" ``` huffman@44521 ` 825` ```proof (rule span_unique) ``` huffman@44521 ` 826` ``` show "A \ B \ (\(a, b). a + b) ` (span A \ span B)" ``` huffman@44521 ` 827` ``` by safe (force intro: span_clauses)+ ``` huffman@44521 ` 828` ```next ``` huffman@44521 ` 829` ``` have "linear (\(a, b). a + b)" ``` huffman@44521 ` 830` ``` by (simp add: linear_def scaleR_add_right) ``` huffman@44521 ` 831` ``` moreover have "subspace (span A \ span B)" ``` huffman@44521 ` 832` ``` by (intro subspace_Times subspace_span) ``` huffman@44521 ` 833` ``` ultimately show "subspace ((\(a, b). a + b) ` (span A \ span B))" ``` huffman@44521 ` 834` ``` by (rule subspace_linear_image) ``` huffman@44521 ` 835` ```next ``` huffman@44521 ` 836` ``` fix T assume "A \ B \ T" and "subspace T" ``` huffman@44521 ` 837` ``` thus "(\(a, b). a + b) ` (span A \ span B) \ T" ``` huffman@44521 ` 838` ``` by (auto intro!: subspace_add elim: span_induct) ``` huffman@44133 ` 839` ```qed ``` huffman@44133 ` 840` huffman@44133 ` 841` ```text {* The key breakdown property. *} ``` huffman@44133 ` 842` huffman@44521 ` 843` ```lemma span_singleton: "span {x} = range (\k. k *\<^sub>R x)" ``` huffman@44521 ` 844` ```proof (rule span_unique) ``` huffman@44521 ` 845` ``` show "{x} \ range (\k. k *\<^sub>R x)" ``` huffman@44521 ` 846` ``` by (fast intro: scaleR_one [symmetric]) ``` huffman@44521 ` 847` ``` show "subspace (range (\k. k *\<^sub>R x))" ``` huffman@44521 ` 848` ``` unfolding subspace_def ``` huffman@44521 ` 849` ``` by (auto intro: scaleR_add_left [symmetric]) ``` huffman@44521 ` 850` ``` fix T assume "{x} \ T" and "subspace T" thus "range (\k. k *\<^sub>R x) \ T" ``` huffman@44521 ` 851` ``` unfolding subspace_def by auto ``` huffman@44521 ` 852` ```qed ``` huffman@44521 ` 853` huffman@44521 ` 854` ```lemma span_insert: ``` huffman@44521 ` 855` ``` "span (insert a S) = {x. \k. (x - k *\<^sub>R a) \ span S}" ``` huffman@44521 ` 856` ```proof - ``` huffman@44521 ` 857` ``` have "span ({a} \ S) = {x. \k. (x - k *\<^sub>R a) \ span S}" ``` huffman@44521 ` 858` ``` unfolding span_union span_singleton ``` huffman@44521 ` 859` ``` apply safe ``` huffman@44521 ` 860` ``` apply (rule_tac x=k in exI, simp) ``` huffman@44521 ` 861` ``` apply (erule rev_image_eqI [OF SigmaI [OF rangeI]]) ``` huffman@44521 ` 862` ``` apply simp ``` huffman@44521 ` 863` ``` apply (rule right_minus) ``` huffman@44521 ` 864` ``` done ``` huffman@44521 ` 865` ``` thus ?thesis by simp ``` huffman@44521 ` 866` ```qed ``` huffman@44521 ` 867` huffman@44133 ` 868` ```lemma span_breakdown: ``` huffman@44133 ` 869` ``` assumes bS: "b \ S" and aS: "a \ span S" ``` huffman@44521 ` 870` ``` shows "\k. a - k *\<^sub>R b \ span (S - {b})" ``` huffman@44521 ` 871` ``` using assms span_insert [of b "S - {b}"] ``` huffman@44521 ` 872` ``` by (simp add: insert_absorb) ``` huffman@44133 ` 873` huffman@44133 ` 874` ```lemma span_breakdown_eq: ``` huffman@44521 ` 875` ``` "x \ span (insert a S) \ (\k. (x - k *\<^sub>R a) \ span S)" ``` huffman@44521 ` 876` ``` by (simp add: span_insert) ``` huffman@44133 ` 877` huffman@44133 ` 878` ```text {* Hence some "reversal" results. *} ``` huffman@44133 ` 879` huffman@44133 ` 880` ```lemma in_span_insert: ``` huffman@44133 ` 881` ``` assumes a: "a \ span (insert b S)" and na: "a \ span S" ``` huffman@44133 ` 882` ``` shows "b \ span (insert a S)" ``` huffman@44133 ` 883` ```proof- ``` huffman@44133 ` 884` ``` from span_breakdown[of b "insert b S" a, OF insertI1 a] ``` huffman@44133 ` 885` ``` obtain k where k: "a - k*\<^sub>R b \ span (S - {b})" by auto ``` huffman@44133 ` 886` ``` {assume k0: "k = 0" ``` huffman@44133 ` 887` ``` with k have "a \ span S" ``` huffman@44133 ` 888` ``` apply (simp) ``` huffman@44133 ` 889` ``` apply (rule set_rev_mp) ``` huffman@44133 ` 890` ``` apply assumption ``` huffman@44133 ` 891` ``` apply (rule span_mono) ``` huffman@44133 ` 892` ``` apply blast ``` huffman@44133 ` 893` ``` done ``` huffman@44133 ` 894` ``` with na have ?thesis by blast} ``` huffman@44133 ` 895` ``` moreover ``` huffman@44133 ` 896` ``` {assume k0: "k \ 0" ``` huffman@44133 ` 897` ``` have eq: "b = (1/k) *\<^sub>R a - ((1/k) *\<^sub>R a - b)" by simp ``` huffman@44133 ` 898` ``` from k0 have eq': "(1/k) *\<^sub>R (a - k*\<^sub>R b) = (1/k) *\<^sub>R a - b" ``` huffman@44133 ` 899` ``` by (simp add: algebra_simps) ``` huffman@44133 ` 900` ``` from k have "(1/k) *\<^sub>R (a - k*\<^sub>R b) \ span (S - {b})" ``` huffman@44133 ` 901` ``` by (rule span_mul) ``` huffman@44133 ` 902` ``` hence th: "(1/k) *\<^sub>R a - b \ span (S - {b})" ``` huffman@44133 ` 903` ``` unfolding eq' . ``` huffman@44133 ` 904` huffman@44133 ` 905` ``` from k ``` huffman@44133 ` 906` ``` have ?thesis ``` huffman@44133 ` 907` ``` apply (subst eq) ``` huffman@44133 ` 908` ``` apply (rule span_sub) ``` huffman@44133 ` 909` ``` apply (rule span_mul) ``` huffman@44133 ` 910` ``` apply (rule span_superset) ``` huffman@44133 ` 911` ``` apply blast ``` huffman@44133 ` 912` ``` apply (rule set_rev_mp) ``` huffman@44133 ` 913` ``` apply (rule th) ``` huffman@44133 ` 914` ``` apply (rule span_mono) ``` huffman@44133 ` 915` ``` using na by blast} ``` huffman@44133 ` 916` ``` ultimately show ?thesis by blast ``` huffman@44133 ` 917` ```qed ``` huffman@44133 ` 918` huffman@44133 ` 919` ```lemma in_span_delete: ``` huffman@44133 ` 920` ``` assumes a: "a \ span S" ``` huffman@44133 ` 921` ``` and na: "a \ span (S-{b})" ``` huffman@44133 ` 922` ``` shows "b \ span (insert a (S - {b}))" ``` huffman@44133 ` 923` ``` apply (rule in_span_insert) ``` huffman@44133 ` 924` ``` apply (rule set_rev_mp) ``` huffman@44133 ` 925` ``` apply (rule a) ``` huffman@44133 ` 926` ``` apply (rule span_mono) ``` huffman@44133 ` 927` ``` apply blast ``` huffman@44133 ` 928` ``` apply (rule na) ``` huffman@44133 ` 929` ``` done ``` huffman@44133 ` 930` huffman@44133 ` 931` ```text {* Transitivity property. *} ``` huffman@44133 ` 932` huffman@44521 ` 933` ```lemma span_redundant: "x \ span S \ span (insert x S) = span S" ``` huffman@44521 ` 934` ``` unfolding span_def by (rule hull_redundant) ``` huffman@44521 ` 935` huffman@44133 ` 936` ```lemma span_trans: ``` huffman@44133 ` 937` ``` assumes x: "x \ span S" and y: "y \ span (insert x S)" ``` huffman@44133 ` 938` ``` shows "y \ span S" ``` huffman@44521 ` 939` ``` using assms by (simp only: span_redundant) ``` huffman@44133 ` 940` huffman@44133 ` 941` ```lemma span_insert_0[simp]: "span (insert 0 S) = span S" ``` huffman@44521 ` 942` ``` by (simp only: span_redundant span_0) ``` huffman@44133 ` 943` huffman@44133 ` 944` ```text {* An explicit expansion is sometimes needed. *} ``` huffman@44133 ` 945` huffman@44133 ` 946` ```lemma span_explicit: ``` huffman@44133 ` 947` ``` "span P = {y. \S u. finite S \ S \ P \ setsum (\v. u v *\<^sub>R v) S = y}" ``` huffman@44133 ` 948` ``` (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \S u. ?Q S u y}") ``` huffman@44133 ` 949` ```proof- ``` huffman@44133 ` 950` ``` {fix x assume x: "x \ ?E" ``` huffman@44133 ` 951` ``` then obtain S u where fS: "finite S" and SP: "S\P" and u: "setsum (\v. u v *\<^sub>R v) S = x" ``` huffman@44133 ` 952` ``` by blast ``` huffman@44133 ` 953` ``` have "x \ span P" ``` huffman@44133 ` 954` ``` unfolding u[symmetric] ``` huffman@44133 ` 955` ``` apply (rule span_setsum[OF fS]) ``` huffman@44133 ` 956` ``` using span_mono[OF SP] ``` huffman@44133 ` 957` ``` by (auto intro: span_superset span_mul)} ``` huffman@44133 ` 958` ``` moreover ``` huffman@44133 ` 959` ``` have "\x \ span P. x \ ?E" ``` huffman@44133 ` 960` ``` proof(rule span_induct_alt') ``` huffman@44170 ` 961` ``` show "0 \ Collect ?h" ``` huffman@44170 ` 962` ``` unfolding mem_Collect_eq ``` huffman@44133 ` 963` ``` apply (rule exI[where x="{}"]) by simp ``` huffman@44133 ` 964` ``` next ``` huffman@44133 ` 965` ``` fix c x y ``` huffman@44170 ` 966` ``` assume x: "x \ P" and hy: "y \ Collect ?h" ``` huffman@44133 ` 967` ``` from hy obtain S u where fS: "finite S" and SP: "S\P" ``` huffman@44133 ` 968` ``` and u: "setsum (\v. u v *\<^sub>R v) S = y" by blast ``` huffman@44133 ` 969` ``` let ?S = "insert x S" ``` huffman@44133 ` 970` ``` let ?u = "\y. if y = x then (if x \ S then u y + c else c) ``` huffman@44133 ` 971` ``` else u y" ``` huffman@44133 ` 972` ``` from fS SP x have th0: "finite (insert x S)" "insert x S \ P" by blast+ ``` huffman@44133 ` 973` ``` {assume xS: "x \ S" ``` huffman@44133 ` 974` ``` have S1: "S = (S - {x}) \ {x}" ``` huffman@44133 ` 975` ``` and Sss:"finite (S - {x})" "finite {x}" "(S -{x}) \ {x} = {}" using xS fS by auto ``` huffman@44133 ` 976` ``` have "setsum (\v. ?u v *\<^sub>R v) ?S =(\v\S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x" ``` huffman@44133 ` 977` ``` using xS ``` huffman@44133 ` 978` ``` by (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]] ``` huffman@44133 ` 979` ``` setsum_clauses(2)[OF fS] cong del: if_weak_cong) ``` huffman@44133 ` 980` ``` also have "\ = (\v\S. u v *\<^sub>R v) + c *\<^sub>R x" ``` huffman@44133 ` 981` ``` apply (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]]) ``` huffman@44133 ` 982` ``` by (simp add: algebra_simps) ``` huffman@44133 ` 983` ``` also have "\ = c*\<^sub>R x + y" ``` huffman@44133 ` 984` ``` by (simp add: add_commute u) ``` huffman@44133 ` 985` ``` finally have "setsum (\v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" . ``` huffman@44133 ` 986` ``` then have "?Q ?S ?u (c*\<^sub>R x + y)" using th0 by blast} ``` huffman@44133 ` 987` ``` moreover ``` huffman@44133 ` 988` ``` {assume xS: "x \ S" ``` huffman@44133 ` 989` ``` have th00: "(\v\S. (if v = x then c else u v) *\<^sub>R v) = y" ``` huffman@44133 ` 990` ``` unfolding u[symmetric] ``` huffman@44133 ` 991` ``` apply (rule setsum_cong2) ``` huffman@44133 ` 992` ``` using xS by auto ``` huffman@44133 ` 993` ``` have "?Q ?S ?u (c*\<^sub>R x + y)" using fS xS th0 ``` huffman@44133 ` 994` ``` by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong)} ``` huffman@44133 ` 995` ``` ultimately have "?Q ?S ?u (c*\<^sub>R x + y)" ``` huffman@44133 ` 996` ``` by (cases "x \ S", simp, simp) ``` huffman@44170 ` 997` ``` then show "(c*\<^sub>R x + y) \ Collect ?h" ``` huffman@44170 ` 998` ``` unfolding mem_Collect_eq ``` huffman@44133 ` 999` ``` apply - ``` huffman@44133 ` 1000` ``` apply (rule exI[where x="?S"]) ``` huffman@44133 ` 1001` ``` apply (rule exI[where x="?u"]) by metis ``` huffman@44133 ` 1002` ``` qed ``` huffman@44133 ` 1003` ``` ultimately show ?thesis by blast ``` huffman@44133 ` 1004` ```qed ``` huffman@44133 ` 1005` huffman@44133 ` 1006` ```lemma dependent_explicit: ``` huffman@44133 ` 1007` ``` "dependent P \ (\S u. finite S \ S \ P \ (\v\S. u v \ 0 \ setsum (\v. u v *\<^sub>R v) S = 0))" (is "?lhs = ?rhs") ``` huffman@44133 ` 1008` ```proof- ``` huffman@44133 ` 1009` ``` {assume dP: "dependent P" ``` huffman@44133 ` 1010` ``` then obtain a S u where aP: "a \ P" and fS: "finite S" ``` huffman@44133 ` 1011` ``` and SP: "S \ P - {a}" and ua: "setsum (\v. u v *\<^sub>R v) S = a" ``` huffman@44133 ` 1012` ``` unfolding dependent_def span_explicit by blast ``` huffman@44133 ` 1013` ``` let ?S = "insert a S" ``` huffman@44133 ` 1014` ``` let ?u = "\y. if y = a then - 1 else u y" ``` huffman@44133 ` 1015` ``` let ?v = a ``` huffman@44133 ` 1016` ``` from aP SP have aS: "a \ S" by blast ``` huffman@44133 ` 1017` ``` from fS SP aP have th0: "finite ?S" "?S \ P" "?v \ ?S" "?u ?v \ 0" by auto ``` huffman@44133 ` 1018` ``` have s0: "setsum (\v. ?u v *\<^sub>R v) ?S = 0" ``` huffman@44133 ` 1019` ``` using fS aS ``` huffman@44133 ` 1020` ``` apply (simp add: setsum_clauses field_simps) ``` huffman@44133 ` 1021` ``` apply (subst (2) ua[symmetric]) ``` huffman@44133 ` 1022` ``` apply (rule setsum_cong2) ``` huffman@44133 ` 1023` ``` by auto ``` huffman@44133 ` 1024` ``` with th0 have ?rhs ``` huffman@44133 ` 1025` ``` apply - ``` huffman@44133 ` 1026` ``` apply (rule exI[where x= "?S"]) ``` huffman@44133 ` 1027` ``` apply (rule exI[where x= "?u"]) ``` huffman@44133 ` 1028` ``` by clarsimp} ``` huffman@44133 ` 1029` ``` moreover ``` huffman@44133 ` 1030` ``` {fix S u v assume fS: "finite S" ``` huffman@44133 ` 1031` ``` and SP: "S \ P" and vS: "v \ S" and uv: "u v \ 0" ``` huffman@44133 ` 1032` ``` and u: "setsum (\v. u v *\<^sub>R v) S = 0" ``` huffman@44133 ` 1033` ``` let ?a = v ``` huffman@44133 ` 1034` ``` let ?S = "S - {v}" ``` huffman@44133 ` 1035` ``` let ?u = "\i. (- u i) / u v" ``` huffman@44133 ` 1036` ``` have th0: "?a \ P" "finite ?S" "?S \ P" using fS SP vS by auto ``` huffman@44133 ` 1037` ``` have "setsum (\v. ?u v *\<^sub>R v) ?S = setsum (\v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v" ``` huffman@44133 ` 1038` ``` using fS vS uv ``` huffman@44133 ` 1039` ``` by (simp add: setsum_diff1 divide_inverse field_simps) ``` huffman@44133 ` 1040` ``` also have "\ = ?a" ``` huffman@44133 ` 1041` ``` unfolding scaleR_right.setsum [symmetric] u ``` huffman@44133 ` 1042` ``` using uv by simp ``` huffman@44133 ` 1043` ``` finally have "setsum (\v. ?u v *\<^sub>R v) ?S = ?a" . ``` huffman@44133 ` 1044` ``` with th0 have ?lhs ``` huffman@44133 ` 1045` ``` unfolding dependent_def span_explicit ``` huffman@44133 ` 1046` ``` apply - ``` huffman@44133 ` 1047` ``` apply (rule bexI[where x= "?a"]) ``` huffman@44133 ` 1048` ``` apply (simp_all del: scaleR_minus_left) ``` huffman@44133 ` 1049` ``` apply (rule exI[where x= "?S"]) ``` huffman@44133 ` 1050` ``` by (auto simp del: scaleR_minus_left)} ``` huffman@44133 ` 1051` ``` ultimately show ?thesis by blast ``` huffman@44133 ` 1052` ```qed ``` huffman@44133 ` 1053` huffman@44133 ` 1054` huffman@44133 ` 1055` ```lemma span_finite: ``` huffman@44133 ` 1056` ``` assumes fS: "finite S" ``` huffman@44133 ` 1057` ``` shows "span S = {y. \u. setsum (\v. u v *\<^sub>R v) S = y}" ``` huffman@44133 ` 1058` ``` (is "_ = ?rhs") ``` huffman@44133 ` 1059` ```proof- ``` huffman@44133 ` 1060` ``` {fix y assume y: "y \ span S" ``` huffman@44133 ` 1061` ``` from y obtain S' u where fS': "finite S'" and SS': "S' \ S" and ``` huffman@44133 ` 1062` ``` u: "setsum (\v. u v *\<^sub>R v) S' = y" unfolding span_explicit by blast ``` huffman@44133 ` 1063` ``` let ?u = "\x. if x \ S' then u x else 0" ``` huffman@44133 ` 1064` ``` have "setsum (\v. ?u v *\<^sub>R v) S = setsum (\v. u v *\<^sub>R v) S'" ``` huffman@44133 ` 1065` ``` using SS' fS by (auto intro!: setsum_mono_zero_cong_right) ``` huffman@44133 ` 1066` ``` hence "setsum (\v. ?u v *\<^sub>R v) S = y" by (metis u) ``` huffman@44133 ` 1067` ``` hence "y \ ?rhs" by auto} ``` huffman@44133 ` 1068` ``` moreover ``` huffman@44133 ` 1069` ``` {fix y u assume u: "setsum (\v. u v *\<^sub>R v) S = y" ``` huffman@44133 ` 1070` ``` then have "y \ span S" using fS unfolding span_explicit by auto} ``` huffman@44133 ` 1071` ``` ultimately show ?thesis by blast ``` huffman@44133 ` 1072` ```qed ``` huffman@44133 ` 1073` huffman@44133 ` 1074` ```text {* This is useful for building a basis step-by-step. *} ``` huffman@44133 ` 1075` huffman@44133 ` 1076` ```lemma independent_insert: ``` huffman@44133 ` 1077` ``` "independent(insert a S) \ ``` huffman@44133 ` 1078` ``` (if a \ S then independent S ``` huffman@44133 ` 1079` ``` else independent S \ a \ span S)" (is "?lhs \ ?rhs") ``` huffman@44133 ` 1080` ```proof- ``` huffman@44133 ` 1081` ``` {assume aS: "a \ S" ``` huffman@44133 ` 1082` ``` hence ?thesis using insert_absorb[OF aS] by simp} ``` huffman@44133 ` 1083` ``` moreover ``` huffman@44133 ` 1084` ``` {assume aS: "a \ S" ``` huffman@44133 ` 1085` ``` {assume i: ?lhs ``` huffman@44133 ` 1086` ``` then have ?rhs using aS ``` huffman@44133 ` 1087` ``` apply simp ``` huffman@44133 ` 1088` ``` apply (rule conjI) ``` huffman@44133 ` 1089` ``` apply (rule independent_mono) ``` huffman@44133 ` 1090` ``` apply assumption ``` huffman@44133 ` 1091` ``` apply blast ``` huffman@44133 ` 1092` ``` by (simp add: dependent_def)} ``` huffman@44133 ` 1093` ``` moreover ``` huffman@44133 ` 1094` ``` {assume i: ?rhs ``` huffman@44133 ` 1095` ``` have ?lhs using i aS ``` huffman@44133 ` 1096` ``` apply simp ``` huffman@44133 ` 1097` ``` apply (auto simp add: dependent_def) ``` huffman@44133 ` 1098` ``` apply (case_tac "aa = a", auto) ``` huffman@44133 ` 1099` ``` apply (subgoal_tac "insert a S - {aa} = insert a (S - {aa})") ``` huffman@44133 ` 1100` ``` apply simp ``` huffman@44133 ` 1101` ``` apply (subgoal_tac "a \ span (insert aa (S - {aa}))") ``` huffman@44133 ` 1102` ``` apply (subgoal_tac "insert aa (S - {aa}) = S") ``` huffman@44133 ` 1103` ``` apply simp ``` huffman@44133 ` 1104` ``` apply blast ``` huffman@44133 ` 1105` ``` apply (rule in_span_insert) ``` huffman@44133 ` 1106` ``` apply assumption ``` huffman@44133 ` 1107` ``` apply blast ``` huffman@44133 ` 1108` ``` apply blast ``` huffman@44133 ` 1109` ``` done} ``` huffman@44133 ` 1110` ``` ultimately have ?thesis by blast} ``` huffman@44133 ` 1111` ``` ultimately show ?thesis by blast ``` huffman@44133 ` 1112` ```qed ``` huffman@44133 ` 1113` huffman@44133 ` 1114` ```text {* The degenerate case of the Exchange Lemma. *} ``` huffman@44133 ` 1115` huffman@44133 ` 1116` ```lemma mem_delete: "x \ (A - {a}) \ x \ a \ x \ A" ``` huffman@44133 ` 1117` ``` by blast ``` huffman@44133 ` 1118` huffman@44133 ` 1119` ```lemma spanning_subset_independent: ``` huffman@44133 ` 1120` ``` assumes BA: "B \ A" and iA: "independent A" ``` huffman@44133 ` 1121` ``` and AsB: "A \ span B" ``` huffman@44133 ` 1122` ``` shows "A = B" ``` huffman@44133 ` 1123` ```proof ``` huffman@44133 ` 1124` ``` from BA show "B \ A" . ``` huffman@44133 ` 1125` ```next ``` huffman@44133 ` 1126` ``` from span_mono[OF BA] span_mono[OF AsB] ``` huffman@44133 ` 1127` ``` have sAB: "span A = span B" unfolding span_span by blast ``` huffman@44133 ` 1128` huffman@44133 ` 1129` ``` {fix x assume x: "x \ A" ``` huffman@44133 ` 1130` ``` from iA have th0: "x \ span (A - {x})" ``` huffman@44133 ` 1131` ``` unfolding dependent_def using x by blast ``` huffman@44133 ` 1132` ``` from x have xsA: "x \ span A" by (blast intro: span_superset) ``` huffman@44133 ` 1133` ``` have "A - {x} \ A" by blast ``` huffman@44133 ` 1134` ``` hence th1:"span (A - {x}) \ span A" by (metis span_mono) ``` huffman@44133 ` 1135` ``` {assume xB: "x \ B" ``` huffman@44133 ` 1136` ``` from xB BA have "B \ A -{x}" by blast ``` huffman@44133 ` 1137` ``` hence "span B \ span (A - {x})" by (metis span_mono) ``` huffman@44133 ` 1138` ``` with th1 th0 sAB have "x \ span A" by blast ``` huffman@44133 ` 1139` ``` with x have False by (metis span_superset)} ``` huffman@44133 ` 1140` ``` then have "x \ B" by blast} ``` huffman@44133 ` 1141` ``` then show "A \ B" by blast ``` huffman@44133 ` 1142` ```qed ``` huffman@44133 ` 1143` huffman@44133 ` 1144` ```text {* The general case of the Exchange Lemma, the key to what follows. *} ``` huffman@44133 ` 1145` huffman@44133 ` 1146` ```lemma exchange_lemma: ``` huffman@44133 ` 1147` ``` assumes f:"finite t" and i: "independent s" ``` huffman@44133 ` 1148` ``` and sp:"s \ span t" ``` huffman@44133 ` 1149` ``` shows "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" ``` huffman@44133 ` 1150` ```using f i sp ``` huffman@44133 ` 1151` ```proof(induct "card (t - s)" arbitrary: s t rule: less_induct) ``` huffman@44133 ` 1152` ``` case less ``` huffman@44133 ` 1153` ``` note ft = `finite t` and s = `independent s` and sp = `s \ span t` ``` huffman@44133 ` 1154` ``` let ?P = "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" ``` huffman@44133 ` 1155` ``` let ?ths = "\t'. ?P t'" ``` huffman@44133 ` 1156` ``` {assume st: "s \ t" ``` huffman@44133 ` 1157` ``` from st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t]) ``` huffman@44133 ` 1158` ``` by (auto intro: span_superset)} ``` huffman@44133 ` 1159` ``` moreover ``` huffman@44133 ` 1160` ``` {assume st: "t \ s" ``` huffman@44133 ` 1161` huffman@44133 ` 1162` ``` from spanning_subset_independent[OF st s sp] ``` huffman@44133 ` 1163` ``` st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t]) ``` huffman@44133 ` 1164` ``` by (auto intro: span_superset)} ``` huffman@44133 ` 1165` ``` moreover ``` huffman@44133 ` 1166` ``` {assume st: "\ s \ t" "\ t \ s" ``` huffman@44133 ` 1167` ``` from st(2) obtain b where b: "b \ t" "b \ s" by blast ``` huffman@44133 ` 1168` ``` from b have "t - {b} - s \ t - s" by blast ``` huffman@44133 ` 1169` ``` then have cardlt: "card (t - {b} - s) < card (t - s)" using ft ``` huffman@44133 ` 1170` ``` by (auto intro: psubset_card_mono) ``` huffman@44133 ` 1171` ``` from b ft have ct0: "card t \ 0" by auto ``` huffman@44133 ` 1172` ``` {assume stb: "s \ span(t -{b})" ``` huffman@44133 ` 1173` ``` from ft have ftb: "finite (t -{b})" by auto ``` huffman@44133 ` 1174` ``` from less(1)[OF cardlt ftb s stb] ``` huffman@44133 ` 1175` ``` obtain u where u: "card u = card (t-{b})" "s \ u" "u \ s \ (t - {b})" "s \ span u" and fu: "finite u" by blast ``` huffman@44133 ` 1176` ``` let ?w = "insert b u" ``` huffman@44133 ` 1177` ``` have th0: "s \ insert b u" using u by blast ``` huffman@44133 ` 1178` ``` from u(3) b have "u \ s \ t" by blast ``` huffman@44133 ` 1179` ``` then have th1: "insert b u \ s \ t" using u b by blast ``` huffman@44133 ` 1180` ``` have bu: "b \ u" using b u by blast ``` huffman@44133 ` 1181` ``` from u(1) ft b have "card u = (card t - 1)" by auto ``` huffman@44133 ` 1182` ``` then ``` huffman@44133 ` 1183` ``` have th2: "card (insert b u) = card t" ``` huffman@44133 ` 1184` ``` using card_insert_disjoint[OF fu bu] ct0 by auto ``` huffman@44133 ` 1185` ``` from u(4) have "s \ span u" . ``` huffman@44133 ` 1186` ``` also have "\ \ span (insert b u)" apply (rule span_mono) by blast ``` huffman@44133 ` 1187` ``` finally have th3: "s \ span (insert b u)" . ``` huffman@44133 ` 1188` ``` from th0 th1 th2 th3 fu have th: "?P ?w" by blast ``` huffman@44133 ` 1189` ``` from th have ?ths by blast} ``` huffman@44133 ` 1190` ``` moreover ``` huffman@44133 ` 1191` ``` {assume stb: "\ s \ span(t -{b})" ``` huffman@44133 ` 1192` ``` from stb obtain a where a: "a \ s" "a \ span (t - {b})" by blast ``` huffman@44133 ` 1193` ``` have ab: "a \ b" using a b by blast ``` huffman@44133 ` 1194` ``` have at: "a \ t" using a ab span_superset[of a "t- {b}"] by auto ``` huffman@44133 ` 1195` ``` have mlt: "card ((insert a (t - {b})) - s) < card (t - s)" ``` huffman@44133 ` 1196` ``` using cardlt ft a b by auto ``` huffman@44133 ` 1197` ``` have ft': "finite (insert a (t - {b}))" using ft by auto ``` huffman@44133 ` 1198` ``` {fix x assume xs: "x \ s" ``` huffman@44133 ` 1199` ``` have t: "t \ (insert b (insert a (t -{b})))" using b by auto ``` huffman@44133 ` 1200` ``` from b(1) have "b \ span t" by (simp add: span_superset) ``` huffman@44133 ` 1201` ``` have bs: "b \ span (insert a (t - {b}))" apply(rule in_span_delete) ``` huffman@44133 ` 1202` ``` using a sp unfolding subset_eq by auto ``` huffman@44133 ` 1203` ``` from xs sp have "x \ span t" by blast ``` huffman@44133 ` 1204` ``` with span_mono[OF t] ``` huffman@44133 ` 1205` ``` have x: "x \ span (insert b (insert a (t - {b})))" .. ``` huffman@44133 ` 1206` ``` from span_trans[OF bs x] have "x \ span (insert a (t - {b}))" .} ``` huffman@44133 ` 1207` ``` then have sp': "s \ span (insert a (t - {b}))" by blast ``` huffman@44133 ` 1208` huffman@44133 ` 1209` ``` from less(1)[OF mlt ft' s sp'] obtain u where ``` huffman@44133 ` 1210` ``` u: "card u = card (insert a (t -{b}))" "finite u" "s \ u" "u \ s \ insert a (t -{b})" ``` huffman@44133 ` 1211` ``` "s \ span u" by blast ``` huffman@44133 ` 1212` ``` from u a b ft at ct0 have "?P u" by auto ``` huffman@44133 ` 1213` ``` then have ?ths by blast } ``` huffman@44133 ` 1214` ``` ultimately have ?ths by blast ``` huffman@44133 ` 1215` ``` } ``` huffman@44133 ` 1216` ``` ultimately ``` huffman@44133 ` 1217` ``` show ?ths by blast ``` huffman@44133 ` 1218` ```qed ``` huffman@44133 ` 1219` huffman@44133 ` 1220` ```text {* This implies corresponding size bounds. *} ``` huffman@44133 ` 1221` huffman@44133 ` 1222` ```lemma independent_span_bound: ``` huffman@44133 ` 1223` ``` assumes f: "finite t" and i: "independent s" and sp:"s \ span t" ``` huffman@44133 ` 1224` ``` shows "finite s \ card s \ card t" ``` huffman@44133 ` 1225` ``` by (metis exchange_lemma[OF f i sp] finite_subset card_mono) ``` huffman@44133 ` 1226` huffman@44133 ` 1227` huffman@44133 ` 1228` ```lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\ (UNIV::'a::finite set)}" ``` huffman@44133 ` 1229` ```proof- ``` huffman@44133 ` 1230` ``` have eq: "{f x |x. x\ UNIV} = f ` UNIV" by auto ``` huffman@44133 ` 1231` ``` show ?thesis unfolding eq ``` huffman@44133 ` 1232` ``` apply (rule finite_imageI) ``` huffman@44133 ` 1233` ``` apply (rule finite) ``` huffman@44133 ` 1234` ``` done ``` huffman@44133 ` 1235` ```qed ``` huffman@44133 ` 1236` huffman@44133 ` 1237` ```subsection{* Euclidean Spaces as Typeclass*} ``` huffman@44133 ` 1238` huffman@44133 ` 1239` ```lemma independent_eq_inj_on: ``` huffman@44133 ` 1240` ``` fixes D :: nat and f :: "nat \ 'c::real_vector" assumes *: "inj_on f {.. (\a u. a < D \ (\i\{..R f i) \ f a)" ``` huffman@44133 ` 1242` ```proof - ``` huffman@44133 ` 1243` ``` from * have eq: "\i. i < D \ f ` {..i. inj_on f ({..i. finite (f ` {.. {DIM('a)..}" by auto ``` huffman@44133 ` 1263` ``` show ?thesis unfolding * image_Un basis_finite by auto ``` huffman@44133 ` 1264` ```qed ``` huffman@44133 ` 1265` huffman@44133 ` 1266` ```lemma (in euclidean_space) range_basis_finite[intro]: ``` huffman@44133 ` 1267` ``` "finite (range basis)" ``` huffman@44133 ` 1268` ``` unfolding range_basis by auto ``` huffman@44133 ` 1269` huffman@44133 ` 1270` ```lemma span_basis: "span (range basis) = (UNIV :: 'a::euclidean_space set)" ``` huffman@44133 ` 1271` ```proof - ``` huffman@44133 ` 1272` ``` { fix x :: 'a ``` huffman@44133 ` 1273` ``` have "(\iR basis i) \ span (range basis :: 'a set)" ``` huffman@44133 ` 1274` ``` by (simp add: span_setsum span_mul span_superset) ``` huffman@44133 ` 1275` ``` hence "x \ span (range basis)" ``` huffman@44133 ` 1276` ``` by (simp only: euclidean_representation [symmetric]) ``` huffman@44133 ` 1277` ``` } thus ?thesis by auto ``` huffman@44133 ` 1278` ```qed ``` huffman@44133 ` 1279` huffman@44133 ` 1280` ```lemma basis_representation: ``` huffman@44133 ` 1281` ``` "\u. x = (\v\basis ` {..R (v\'a\euclidean_space))" ``` huffman@44133 ` 1282` ```proof - ``` huffman@44133 ` 1283` ``` have "x\UNIV" by auto from this[unfolded span_basis[THEN sym]] ``` huffman@44133 ` 1284` ``` have "\u. (\v\basis ` {..R v) = x" ``` huffman@44133 ` 1285` ``` unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto ``` huffman@44133 ` 1286` ``` thus ?thesis by fastsimp ``` huffman@44133 ` 1287` ```qed ``` huffman@44133 ` 1288` huffman@44133 ` 1289` ```lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..'a) ` {.. span (basis ` {.. e \ \x\$\$i\ <= e" ``` huffman@44133 ` 1299` ``` by (metis component_le_norm order_trans) ``` huffman@44133 ` 1300` huffman@44133 ` 1301` ```lemma norm_bound_component_lt: "norm (x::'a::euclidean_space) < e \ \x\$\$i\ < e" ``` huffman@44133 ` 1302` ``` by (metis component_le_norm basic_trans_rules(21)) ``` huffman@44133 ` 1303` huffman@44133 ` 1304` ```lemma norm_le_l1: "norm (x::'a::euclidean_space) \ (\ix \$\$ i\)" ``` huffman@44133 ` 1305` ``` apply (subst euclidean_representation[of x]) ``` huffman@44176 ` 1306` ``` apply (rule order_trans[OF norm_setsum]) ``` huffman@44133 ` 1307` ``` by (auto intro!: setsum_mono) ``` huffman@44133 ` 1308` huffman@44133 ` 1309` ```lemma setsum_norm_allsubsets_bound: ``` huffman@44133 ` 1310` ``` fixes f:: "'a \ 'n::euclidean_space" ``` huffman@44133 ` 1311` ``` assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" ``` huffman@44133 ` 1312` ``` shows "setsum (\x. norm (f x)) P \ 2 * real DIM('n) * e" ``` huffman@44133 ` 1313` ```proof- ``` huffman@44133 ` 1314` ``` let ?d = "real DIM('n)" ``` huffman@44133 ` 1315` ``` let ?nf = "\x. norm (f x)" ``` huffman@44133 ` 1316` ``` let ?U = "{..x. setsum (\i. \f x \$\$ i\) ?U) P = setsum (\i. setsum (\x. \f x \$\$ i\) P) ?U" ``` huffman@44133 ` 1318` ``` by (rule setsum_commute) ``` huffman@44133 ` 1319` ``` have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def) ``` huffman@44133 ` 1320` ``` have "setsum ?nf P \ setsum (\x. setsum (\i. \f x \$\$ i\) ?U) P" ``` huffman@44133 ` 1321` ``` apply (rule setsum_mono) by (rule norm_le_l1) ``` huffman@44133 ` 1322` ``` also have "\ \ 2 * ?d * e" ``` huffman@44133 ` 1323` ``` unfolding th0 th1 ``` huffman@44133 ` 1324` ``` proof(rule setsum_bounded) ``` huffman@44133 ` 1325` ``` fix i assume i: "i \ ?U" ``` huffman@44133 ` 1326` ``` let ?Pp = "{x. x\ P \ f x \$\$ i \ 0}" ``` huffman@44133 ` 1327` ``` let ?Pn = "{x. x \ P \ f x \$\$ i < 0}" ``` huffman@44133 ` 1328` ``` have thp: "P = ?Pp \ ?Pn" by auto ``` huffman@44133 ` 1329` ``` have thp0: "?Pp \ ?Pn ={}" by auto ``` huffman@44133 ` 1330` ``` have PpP: "?Pp \ P" and PnP: "?Pn \ P" by blast+ ``` huffman@44133 ` 1331` ``` have Ppe:"setsum (\x. \f x \$\$ i\) ?Pp \ e" ``` huffman@44133 ` 1332` ``` using component_le_norm[of "setsum (\x. f x) ?Pp" i] fPs[OF PpP] ``` huffman@44457 ` 1333` ``` by(auto intro: abs_le_D1) ``` huffman@44133 ` 1334` ``` have Pne: "setsum (\x. \f x \$\$ i\) ?Pn \ e" ``` huffman@44133 ` 1335` ``` using component_le_norm[of "setsum (\x. - f x) ?Pn" i] fPs[OF PnP] ``` huffman@44133 ` 1336` ``` by(auto simp add: setsum_negf intro: abs_le_D1) ``` huffman@44133 ` 1337` ``` have "setsum (\x. \f x \$\$ i\) P = setsum (\x. \f x \$\$ i\) ?Pp + setsum (\x. \f x \$\$ i\) ?Pn" ``` huffman@44133 ` 1338` ``` apply (subst thp) ``` huffman@44133 ` 1339` ``` apply (rule setsum_Un_zero) ``` huffman@44133 ` 1340` ``` using fP thp0 by auto ``` huffman@44133 ` 1341` ``` also have "\ \ 2*e" using Pne Ppe by arith ``` huffman@44133 ` 1342` ``` finally show "setsum (\x. \f x \$\$ i\) P \ 2*e" . ``` huffman@44133 ` 1343` ``` qed ``` huffman@44133 ` 1344` ``` finally show ?thesis . ``` huffman@44133 ` 1345` ```qed ``` huffman@44133 ` 1346` huffman@44133 ` 1347` ```lemma choice_iff': "(\xy. P x y) \ (\f. \xix. P i x) \ ``` huffman@44133 ` 1350` ``` (\x::'a. \i ?rhs") ``` huffman@44133 ` 1351` ```proof- ``` huffman@44133 ` 1352` ``` let ?S = "{..ii y \ (\i < DIM('a). x \$\$ i \ y \$\$ i)" ``` huffman@44133 ` 1372` ``` and eucl_less: "x < y \ (\i < DIM('a). x \$\$ i < y \$\$ i)" ``` huffman@44133 ` 1373` huffman@44133 ` 1374` ```lemma eucl_less_not_refl[simp, intro!]: "\ x < (x::'a::ordered_euclidean_space)" ``` huffman@44133 ` 1375` ``` unfolding eucl_less[where 'a='a] by auto ``` huffman@44133 ` 1376` huffman@44133 ` 1377` ```lemma euclidean_trans[trans]: ``` huffman@44133 ` 1378` ``` fixes x y z :: "'a::ordered_euclidean_space" ``` huffman@44133 ` 1379` ``` shows "x < y \ y < z \ x < z" ``` huffman@44133 ` 1380` ``` and "x \ y \ y < z \ x < z" ``` huffman@44133 ` 1381` ``` and "x \ y \ y \ z \ x \ z" ``` huffman@44133 ` 1382` ``` by (force simp: eucl_less[where 'a='a] eucl_le[where 'a='a])+ ``` huffman@44133 ` 1383` huffman@44133 ` 1384` ```subsection {* Linearity and Bilinearity continued *} ``` huffman@44133 ` 1385` huffman@44133 ` 1386` ```lemma linear_bounded: ``` huffman@44133 ` 1387` ``` fixes f:: "'a::euclidean_space \ 'b::real_normed_vector" ``` huffman@44133 ` 1388` ``` assumes lf: "linear f" ``` huffman@44133 ` 1389` ``` shows "\B. \x. norm (f x) \ B * norm x" ``` huffman@44133 ` 1390` ```proof- ``` huffman@44133 ` 1391` ``` let ?S = "{..i. (x\$\$i) *\<^sub>R (basis i)) ?S))" ``` huffman@44133 ` 1397` ``` apply(subst euclidean_representation[of x]) .. ``` huffman@44133 ` 1398` ``` also have "\ = norm (setsum (\ i. (x\$\$i) *\<^sub>R f (basis i)) ?S)" ``` huffman@44133 ` 1399` ``` using linear_setsum[OF lf fS, of ?g, unfolded o_def] linear_cmul[OF lf] by auto ``` huffman@44133 ` 1400` ``` finally have th0: "norm (f x) = norm (setsum (\i. (x\$\$i) *\<^sub>R f (basis i))?S)" . ``` huffman@44133 ` 1401` ``` {fix i assume i: "i \ ?S" ``` huffman@44133 ` 1402` ``` from component_le_norm[of x i] ``` huffman@44133 ` 1403` ``` have "norm ((x\$\$i) *\<^sub>R f (basis i :: 'a)) \ norm (f (basis i)) * norm x" ``` huffman@44133 ` 1404` ``` unfolding norm_scaleR ``` huffman@44133 ` 1405` ``` apply (simp only: mult_commute) ``` huffman@44133 ` 1406` ``` apply (rule mult_mono) ``` huffman@44133 ` 1407` ``` by (auto simp add: field_simps) } ``` huffman@44133 ` 1408` ``` then have th: "\i\ ?S. norm ((x\$\$i) *\<^sub>R f (basis i :: 'a)) \ norm (f (basis i)) * norm x" by metis ``` huffman@44176 ` 1409` ``` from setsum_norm_le[of _ "\i. (x\$\$i) *\<^sub>R (f (basis i))", OF th] ``` huffman@44133 ` 1410` ``` have "norm (f x) \ ?B * norm x" unfolding th0 setsum_left_distrib by metis} ``` huffman@44133 ` 1411` ``` then show ?thesis by blast ``` huffman@44133 ` 1412` ```qed ``` huffman@44133 ` 1413` huffman@44133 ` 1414` ```lemma linear_bounded_pos: ``` huffman@44133 ` 1415` ``` fixes f:: "'a::euclidean_space \ 'b::real_normed_vector" ``` huffman@44133 ` 1416` ``` assumes lf: "linear f" ``` huffman@44133 ` 1417` ``` shows "\B > 0. \x. norm (f x) \ B * norm x" ``` huffman@44133 ` 1418` ```proof- ``` huffman@44133 ` 1419` ``` from linear_bounded[OF lf] obtain B where ``` huffman@44133 ` 1420` ``` B: "\x. norm (f x) \ B * norm x" by blast ``` huffman@44133 ` 1421` ``` let ?K = "\B\ + 1" ``` huffman@44133 ` 1422` ``` have Kp: "?K > 0" by arith ``` huffman@44133 ` 1423` ``` { assume C: "B < 0" ``` huffman@44133 ` 1424` ``` have "((\\ i. 1)::'a) \ 0" unfolding euclidean_eq[where 'a='a] ``` huffman@44286 ` 1425` ``` by(auto intro!:exI[where x=0]) ``` huffman@44133 ` 1426` ``` hence "norm ((\\ i. 1)::'a) > 0" by auto ``` huffman@44133 ` 1427` ``` with C have "B * norm ((\\ i. 1)::'a) < 0" ``` huffman@44133 ` 1428` ``` by (simp add: mult_less_0_iff) ``` huffman@44133 ` 1429` ``` with B[rule_format, of "(\\ i. 1)::'a"] norm_ge_zero[of "f ((\\ i. 1)::'a)"] have False by simp ``` huffman@44133 ` 1430` ``` } ``` huffman@44133 ` 1431` ``` then have Bp: "B \ 0" by (metis not_leE) ``` huffman@44133 ` 1432` ``` {fix x::"'a" ``` huffman@44133 ` 1433` ``` have "norm (f x) \ ?K * norm x" ``` huffman@44133 ` 1434` ``` using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp ``` huffman@44133 ` 1435` ``` apply (auto simp add: field_simps split add: abs_split) ``` huffman@44133 ` 1436` ``` apply (erule order_trans, simp) ``` huffman@44133 ` 1437` ``` done ``` huffman@44133 ` 1438` ``` } ``` huffman@44133 ` 1439` ``` then show ?thesis using Kp by blast ``` huffman@44133 ` 1440` ```qed ``` huffman@44133 ` 1441` huffman@44133 ` 1442` ```lemma linear_conv_bounded_linear: ``` huffman@44133 ` 1443` ``` fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" ``` huffman@44133 ` 1444` ``` shows "linear f \ bounded_linear f" ``` huffman@44133 ` 1445` ```proof ``` huffman@44133 ` 1446` ``` assume "linear f" ``` huffman@44133 ` 1447` ``` show "bounded_linear f" ``` huffman@44133 ` 1448` ``` proof ``` huffman@44133 ` 1449` ``` fix x y show "f (x + y) = f x + f y" ``` huffman@44133 ` 1450` ``` using `linear f` unfolding linear_def by simp ``` huffman@44133 ` 1451` ``` next ``` huffman@44133 ` 1452` ``` fix r x show "f (scaleR r x) = scaleR r (f x)" ``` huffman@44133 ` 1453` ``` using `linear f` unfolding linear_def by simp ``` huffman@44133 ` 1454` ``` next ``` huffman@44133 ` 1455` ``` have "\B. \x. norm (f x) \ B * norm x" ``` huffman@44133 ` 1456` ``` using `linear f` by (rule linear_bounded) ``` huffman@44133 ` 1457` ``` thus "\K. \x. norm (f x) \ norm x * K" ``` huffman@44133 ` 1458` ``` by (simp add: mult_commute) ``` huffman@44133 ` 1459` ``` qed ``` huffman@44133 ` 1460` ```next ``` huffman@44133 ` 1461` ``` assume "bounded_linear f" ``` huffman@44133 ` 1462` ``` then interpret f: bounded_linear f . ``` huffman@44133 ` 1463` ``` show "linear f" ``` huffman@44133 ` 1464` ``` by (simp add: f.add f.scaleR linear_def) ``` huffman@44133 ` 1465` ```qed ``` huffman@44133 ` 1466` huffman@44133 ` 1467` ```lemma bounded_linearI': fixes f::"'a::euclidean_space \ 'b::real_normed_vector" ``` huffman@44133 ` 1468` ``` assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" ``` huffman@44133 ` 1469` ``` shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym] ``` huffman@44133 ` 1470` ``` by(rule linearI[OF assms]) ``` huffman@44133 ` 1471` huffman@44133 ` 1472` huffman@44133 ` 1473` ```lemma bilinear_bounded: ``` huffman@44133 ` 1474` ``` fixes h:: "'m::euclidean_space \ 'n::euclidean_space \ 'k::real_normed_vector" ``` huffman@44133 ` 1475` ``` assumes bh: "bilinear h" ``` huffman@44133 ` 1476` ``` shows "\B. \x y. norm (h x y) \ B * norm x * norm y" ``` huffman@44133 ` 1477` ```proof- ``` huffman@44133 ` 1478` ``` let ?M = "{..i. (x\$\$i) *\<^sub>R basis i) ?M) (setsum (\i. (y\$\$i) *\<^sub>R basis i) ?N))" ``` huffman@44133 ` 1484` ``` apply(subst euclidean_representation[where 'a='m]) ``` huffman@44133 ` 1485` ``` apply(subst euclidean_representation[where 'a='n]) .. ``` huffman@44133 ` 1486` ``` also have "\ = norm (setsum (\ (i,j). h ((x\$\$i) *\<^sub>R basis i) ((y\$\$j) *\<^sub>R basis j)) (?M \ ?N))" ``` huffman@44133 ` 1487` ``` unfolding bilinear_setsum[OF bh fM fN] .. ``` huffman@44133 ` 1488` ``` finally have th: "norm (h x y) = \" . ``` huffman@44133 ` 1489` ``` have "norm (h x y) \ ?B * norm x * norm y" ``` huffman@44133 ` 1490` ``` apply (simp add: setsum_left_distrib th) ``` huffman@44133 ` 1491` ``` apply (rule setsum_norm_le) ``` huffman@44133 ` 1492` ``` using fN fM ``` huffman@44133 ` 1493` ``` apply simp ``` huffman@44133 ` 1494` ``` apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps simp del: scaleR_scaleR) ``` huffman@44133 ` 1495` ``` apply (rule mult_mono) ``` huffman@44133 ` 1496` ``` apply (auto simp add: zero_le_mult_iff component_le_norm) ``` huffman@44133 ` 1497` ``` apply (rule mult_mono) ``` huffman@44133 ` 1498` ``` apply (auto simp add: zero_le_mult_iff component_le_norm) ``` huffman@44133 ` 1499` ``` done} ``` huffman@44133 ` 1500` ``` then show ?thesis by metis ``` huffman@44133 ` 1501` ```qed ``` huffman@44133 ` 1502` huffman@44133 ` 1503` ```lemma bilinear_bounded_pos: ``` huffman@44133 ` 1504` ``` fixes h:: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" ``` huffman@44133 ` 1505` ``` assumes bh: "bilinear h" ``` huffman@44133 ` 1506` ``` shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y" ``` huffman@44133 ` 1507` ```proof- ``` huffman@44133 ` 1508` ``` from bilinear_bounded[OF bh] obtain B where ``` huffman@44133 ` 1509` ``` B: "\x y. norm (h x y) \ B * norm x * norm y" by blast ``` huffman@44133 ` 1510` ``` let ?K = "\B\ + 1" ``` huffman@44133 ` 1511` ``` have Kp: "?K > 0" by arith ``` huffman@44133 ` 1512` ``` have KB: "B < ?K" by arith ``` huffman@44133 ` 1513` ``` {fix x::'a and y::'b ``` huffman@44133 ` 1514` ``` from KB Kp ``` huffman@44133 ` 1515` ``` have "B * norm x * norm y \ ?K * norm x * norm y" ``` huffman@44133 ` 1516` ``` apply - ``` huffman@44133 ` 1517` ``` apply (rule mult_right_mono, rule mult_right_mono) ``` huffman@44133 ` 1518` ``` by auto ``` huffman@44133 ` 1519` ``` then have "norm (h x y) \ ?K * norm x * norm y" ``` huffman@44133 ` 1520` ``` using B[rule_format, of x y] by simp} ``` huffman@44133 ` 1521` ``` with Kp show ?thesis by blast ``` huffman@44133 ` 1522` ```qed ``` huffman@44133 ` 1523` huffman@44133 ` 1524` ```lemma bilinear_conv_bounded_bilinear: ``` huffman@44133 ` 1525` ``` fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" ``` huffman@44133 ` 1526` ``` shows "bilinear h \ bounded_bilinear h" ``` huffman@44133 ` 1527` ```proof ``` huffman@44133 ` 1528` ``` assume "bilinear h" ``` huffman@44133 ` 1529` ``` show "bounded_bilinear h" ``` huffman@44133 ` 1530` ``` proof ``` huffman@44133 ` 1531` ``` fix x y z show "h (x + y) z = h x z + h y z" ``` huffman@44133 ` 1532` ``` using `bilinear h` unfolding bilinear_def linear_def by simp ``` huffman@44133 ` 1533` ``` next ``` huffman@44133 ` 1534` ``` fix x y z show "h x (y + z) = h x y + h x z" ``` huffman@44133 ` 1535` ``` using `bilinear h` unfolding bilinear_def linear_def by simp ``` huffman@44133 ` 1536` ``` next ``` huffman@44133 ` 1537` ``` fix r x y show "h (scaleR r x) y = scaleR r (h x y)" ``` huffman@44133 ` 1538` ``` using `bilinear h` unfolding bilinear_def linear_def ``` huffman@44133 ` 1539` ``` by simp ``` huffman@44133 ` 1540` ``` next ``` huffman@44133 ` 1541` ``` fix r x y show "h x (scaleR r y) = scaleR r (h x y)" ``` huffman@44133 ` 1542` ``` using `bilinear h` unfolding bilinear_def linear_def ``` huffman@44133 ` 1543` ``` by simp ``` huffman@44133 ` 1544` ``` next ``` huffman@44133 ` 1545` ``` have "\B. \x y. norm (h x y) \ B * norm x * norm y" ``` huffman@44133 ` 1546` ``` using `bilinear h` by (rule bilinear_bounded) ``` huffman@44133 ` 1547` ``` thus "\K. \x y. norm (h x y) \ norm x * norm y * K" ``` huffman@44133 ` 1548` ``` by (simp add: mult_ac) ``` huffman@44133 ` 1549` ``` qed ``` huffman@44133 ` 1550` ```next ``` huffman@44133 ` 1551` ``` assume "bounded_bilinear h" ``` huffman@44133 ` 1552` ``` then interpret h: bounded_bilinear h . ``` huffman@44133 ` 1553` ``` show "bilinear h" ``` huffman@44133 ` 1554` ``` unfolding bilinear_def linear_conv_bounded_linear ``` huffman@44133 ` 1555` ``` using h.bounded_linear_left h.bounded_linear_right ``` huffman@44133 ` 1556` ``` by simp ``` huffman@44133 ` 1557` ```qed ``` huffman@44133 ` 1558` huffman@44133 ` 1559` ```subsection {* We continue. *} ``` huffman@44133 ` 1560` huffman@44133 ` 1561` ```lemma independent_bound: ``` huffman@44133 ` 1562` ``` fixes S:: "('a::euclidean_space) set" ``` huffman@44133 ` 1563` ``` shows "independent S \ finite S \ card S <= DIM('a::euclidean_space)" ``` huffman@44133 ` 1564` ``` using independent_span_bound[of "(basis::nat=>'a) ` {.. card S > DIM('a)) ==> dependent S" ``` huffman@44133 ` 1567` ``` by (metis independent_bound not_less) ``` huffman@44133 ` 1568` huffman@44133 ` 1569` ```text {* Hence we can create a maximal independent subset. *} ``` huffman@44133 ` 1570` huffman@44133 ` 1571` ```lemma maximal_independent_subset_extend: ``` huffman@44133 ` 1572` ``` assumes sv: "(S::('a::euclidean_space) set) \ V" and iS: "independent S" ``` huffman@44133 ` 1573` ``` shows "\B. S \ B \ B \ V \ independent B \ V \ span B" ``` huffman@44133 ` 1574` ``` using sv iS ``` huffman@44133 ` 1575` ```proof(induct "DIM('a) - card S" arbitrary: S rule: less_induct) ``` huffman@44133 ` 1576` ``` case less ``` huffman@44133 ` 1577` ``` note sv = `S \ V` and i = `independent S` ``` huffman@44133 ` 1578` ``` let ?P = "\B. S \ B \ B \ V \ independent B \ V \ span B" ``` huffman@44133 ` 1579` ``` let ?ths = "\x. ?P x" ``` huffman@44133 ` 1580` ``` let ?d = "DIM('a)" ``` huffman@44133 ` 1581` ``` {assume "V \ span S" ``` huffman@44133 ` 1582` ``` then have ?ths using sv i by blast } ``` huffman@44133 ` 1583` ``` moreover ``` huffman@44133 ` 1584` ``` {assume VS: "\ V \ span S" ``` huffman@44133 ` 1585` ``` from VS obtain a where a: "a \ V" "a \ span S" by blast ``` huffman@44133 ` 1586` ``` from a have aS: "a \ S" by (auto simp add: span_superset) ``` huffman@44133 ` 1587` ``` have th0: "insert a S \ V" using a sv by blast ``` huffman@44133 ` 1588` ``` from independent_insert[of a S] i a ``` huffman@44133 ` 1589` ``` have th1: "independent (insert a S)" by auto ``` huffman@44133 ` 1590` ``` have mlt: "?d - card (insert a S) < ?d - card S" ``` huffman@44133 ` 1591` ``` using aS a independent_bound[OF th1] ``` huffman@44133 ` 1592` ``` by auto ``` huffman@44133 ` 1593` huffman@44133 ` 1594` ``` from less(1)[OF mlt th0 th1] ``` huffman@44133 ` 1595` ``` obtain B where B: "insert a S \ B" "B \ V" "independent B" " V \ span B" ``` huffman@44133 ` 1596` ``` by blast ``` huffman@44133 ` 1597` ``` from B have "?P B" by auto ``` huffman@44133 ` 1598` ``` then have ?ths by blast} ``` huffman@44133 ` 1599` ``` ultimately show ?ths by blast ``` huffman@44133 ` 1600` ```qed ``` huffman@44133 ` 1601` huffman@44133 ` 1602` ```lemma maximal_independent_subset: ``` huffman@44133 ` 1603` ``` "\(B:: ('a::euclidean_space) set). B\ V \ independent B \ V \ span B" ``` huffman@44133 ` 1604` ``` by (metis maximal_independent_subset_extend[of "{}:: ('a::euclidean_space) set"] empty_subsetI independent_empty) ``` huffman@44133 ` 1605` huffman@44133 ` 1606` huffman@44133 ` 1607` ```text {* Notion of dimension. *} ``` huffman@44133 ` 1608` huffman@44133 ` 1609` ```definition "dim V = (SOME n. \B. B \ V \ independent B \ V \ span B \ (card B = n))" ``` huffman@44133 ` 1610` huffman@44133 ` 1611` ```lemma basis_exists: "\B. (B :: ('a::euclidean_space) set) \ V \ independent B \ V \ span B \ (card B = dim V)" ``` huffman@44133 ` 1612` ```unfolding dim_def some_eq_ex[of "\n. \B. B \ V \ independent B \ V \ span B \ (card B = n)"] ``` huffman@44133 ` 1613` ```using maximal_independent_subset[of V] independent_bound ``` huffman@44133 ` 1614` ```by auto ``` huffman@44133 ` 1615` huffman@44133 ` 1616` ```text {* Consequences of independence or spanning for cardinality. *} ``` huffman@44133 ` 1617` huffman@44133 ` 1618` ```lemma independent_card_le_dim: ``` huffman@44133 ` 1619` ``` assumes "(B::('a::euclidean_space) set) \ V" and "independent B" shows "card B \ dim V" ``` huffman@44133 ` 1620` ```proof - ``` huffman@44133 ` 1621` ``` from basis_exists[of V] `B \ V` ``` huffman@44133 ` 1622` ``` obtain B' where "independent B'" and "B \ span B'" and "card B' = dim V" by blast ``` huffman@44133 ` 1623` ``` with independent_span_bound[OF _ `independent B` `B \ span B'`] independent_bound[of B'] ``` huffman@44133 ` 1624` ``` show ?thesis by auto ``` huffman@44133 ` 1625` ```qed ``` huffman@44133 ` 1626` huffman@44133 ` 1627` ```lemma span_card_ge_dim: "(B::('a::euclidean_space) set) \ V \ V \ span B \ finite B \ dim V \ card B" ``` huffman@44133 ` 1628` ``` by (metis basis_exists[of V] independent_span_bound subset_trans) ``` huffman@44133 ` 1629` huffman@44133 ` 1630` ```lemma basis_card_eq_dim: ``` huffman@44133 ` 1631` ``` "B \ (V:: ('a::euclidean_space) set) \ V \ span B \ independent B \ finite B \ card B = dim V" ``` huffman@44133 ` 1632` ``` by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_bound) ``` huffman@44133 ` 1633` huffman@44133 ` 1634` ```lemma dim_unique: "(B::('a::euclidean_space) set) \ V \ V \ span B \ independent B \ card B = n \ dim V = n" ``` huffman@44133 ` 1635` ``` by (metis basis_card_eq_dim) ``` huffman@44133 ` 1636` huffman@44133 ` 1637` ```text {* More lemmas about dimension. *} ``` huffman@44133 ` 1638` huffman@44133 ` 1639` ```lemma dim_UNIV: "dim (UNIV :: ('a::euclidean_space) set) = DIM('a)" ``` huffman@44133 ` 1640` ``` apply (rule dim_unique[of "(basis::nat=>'a) ` {.. T \ dim S \ dim T" ``` huffman@44133 ` 1645` ``` using basis_exists[of T] basis_exists[of S] ``` huffman@44133 ` 1646` ``` by (metis independent_card_le_dim subset_trans) ``` huffman@44133 ` 1647` huffman@44133 ` 1648` ```lemma dim_subset_UNIV: "dim (S:: ('a::euclidean_space) set) \ DIM('a)" ``` huffman@44133 ` 1649` ``` by (metis dim_subset subset_UNIV dim_UNIV) ``` huffman@44133 ` 1650` huffman@44133 ` 1651` ```text {* Converses to those. *} ``` huffman@44133 ` 1652` huffman@44133 ` 1653` ```lemma card_ge_dim_independent: ``` huffman@44133 ` 1654` ``` assumes BV:"(B::('a::euclidean_space) set) \ V" and iB:"independent B" and dVB:"dim V \ card B" ``` huffman@44133 ` 1655` ``` shows "V \ span B" ``` huffman@44133 ` 1656` ```proof- ``` huffman@44133 ` 1657` ``` {fix a assume aV: "a \ V" ``` huffman@44133 ` 1658` ``` {assume aB: "a \ span B" ``` huffman@44133 ` 1659` ``` then have iaB: "independent (insert a B)" using iB aV BV by (simp add: independent_insert) ``` huffman@44133 ` 1660` ``` from aV BV have th0: "insert a B \ V" by blast ``` huffman@44133 ` 1661` ``` from aB have "a \B" by (auto simp add: span_superset) ``` huffman@44133 ` 1662` ``` with independent_card_le_dim[OF th0 iaB] dVB independent_bound[OF iB] have False by auto } ``` huffman@44133 ` 1663` ``` then have "a \ span B" by blast} ``` huffman@44133 ` 1664` ``` then show ?thesis by blast ``` huffman@44133 ` 1665` ```qed ``` huffman@44133 ` 1666` huffman@44133 ` 1667` ```lemma card_le_dim_spanning: ``` huffman@44133 ` 1668` ``` assumes BV: "(B:: ('a::euclidean_space) set) \ V" and VB: "V \ span B" ``` huffman@44133 ` 1669` ``` and fB: "finite B" and dVB: "dim V \ card B" ``` huffman@44133 ` 1670` ``` shows "independent B" ``` huffman@44133 ` 1671` ```proof- ``` huffman@44133 ` 1672` ``` {fix a assume a: "a \ B" "a \ span (B -{a})" ``` huffman@44133 ` 1673` ``` from a fB have c0: "card B \ 0" by auto ``` huffman@44133 ` 1674` ``` from a fB have cb: "card (B -{a}) = card B - 1" by auto ``` huffman@44133 ` 1675` ``` from BV a have th0: "B -{a} \ V" by blast ``` huffman@44133 ` 1676` ``` {fix x assume x: "x \ V" ``` huffman@44133 ` 1677` ``` from a have eq: "insert a (B -{a}) = B" by blast ``` huffman@44133 ` 1678` ``` from x VB have x': "x \ span B" by blast ``` huffman@44133 ` 1679` ``` from span_trans[OF a(2), unfolded eq, OF x'] ``` huffman@44133 ` 1680` ``` have "x \ span (B -{a})" . } ``` huffman@44133 ` 1681` ``` then have th1: "V \ span (B -{a})" by blast ``` huffman@44133 ` 1682` ``` have th2: "finite (B -{a})" using fB by auto ``` huffman@44133 ` 1683` ``` from span_card_ge_dim[OF th0 th1 th2] ``` huffman@44133 ` 1684` ``` have c: "dim V \ card (B -{a})" . ``` huffman@44133 ` 1685` ``` from c c0 dVB cb have False by simp} ``` huffman@44133 ` 1686` ``` then show ?thesis unfolding dependent_def by blast ``` huffman@44133 ` 1687` ```qed ``` huffman@44133 ` 1688` huffman@44133 ` 1689` ```lemma card_eq_dim: "(B:: ('a::euclidean_space) set) \ V \ card B = dim V \ finite B \ independent B \ V \ span B" ``` huffman@44133 ` 1690` ``` by (metis order_eq_iff card_le_dim_spanning ``` huffman@44133 ` 1691` ``` card_ge_dim_independent) ``` huffman@44133 ` 1692` huffman@44133 ` 1693` ```text {* More general size bound lemmas. *} ``` huffman@44133 ` 1694` huffman@44133 ` 1695` ```lemma independent_bound_general: ``` huffman@44133 ` 1696` ``` "independent (S:: ('a::euclidean_space) set) \ finite S \ card S \ dim S" ``` huffman@44133 ` 1697` ``` by (metis independent_card_le_dim independent_bound subset_refl) ``` huffman@44133 ` 1698` huffman@44133 ` 1699` ```lemma dependent_biggerset_general: "(finite (S:: ('a::euclidean_space) set) \ card S > dim S) \ dependent S" ``` huffman@44133 ` 1700` ``` using independent_bound_general[of S] by (metis linorder_not_le) ``` huffman@44133 ` 1701` huffman@44133 ` 1702` ```lemma dim_span: "dim (span (S:: ('a::euclidean_space) set)) = dim S" ``` huffman@44133 ` 1703` ```proof- ``` huffman@44133 ` 1704` ``` have th0: "dim S \ dim (span S)" ``` huffman@44133 ` 1705` ``` by (auto simp add: subset_eq intro: dim_subset span_superset) ``` huffman@44133 ` 1706` ``` from basis_exists[of S] ``` huffman@44133 ` 1707` ``` obtain B where B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast ``` huffman@44133 ` 1708` ``` from B have fB: "finite B" "card B = dim S" using independent_bound by blast+ ``` huffman@44133 ` 1709` ``` have bSS: "B \ span S" using B(1) by (metis subset_eq span_inc) ``` huffman@44133 ` 1710` ``` have sssB: "span S \ span B" using span_mono[OF B(3)] by (simp add: span_span) ``` huffman@44133 ` 1711` ``` from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis ``` huffman@44133 ` 1712` ``` using fB(2) by arith ``` huffman@44133 ` 1713` ```qed ``` huffman@44133 ` 1714` huffman@44133 ` 1715` ```lemma subset_le_dim: "(S:: ('a::euclidean_space) set) \ span T \ dim S \ dim T" ``` huffman@44133 ` 1716` ``` by (metis dim_span dim_subset) ``` huffman@44133 ` 1717` huffman@44133 ` 1718` ```lemma span_eq_dim: "span (S:: ('a::euclidean_space) set) = span T ==> dim S = dim T" ``` huffman@44133 ` 1719` ``` by (metis dim_span) ``` huffman@44133 ` 1720` huffman@44133 ` 1721` ```lemma spans_image: ``` huffman@44133 ` 1722` ``` assumes lf: "linear f" and VB: "V \ span B" ``` huffman@44133 ` 1723` ``` shows "f ` V \ span (f ` B)" ``` huffman@44133 ` 1724` ``` unfolding span_linear_image[OF lf] ``` huffman@44133 ` 1725` ``` by (metis VB image_mono) ``` huffman@44133 ` 1726` huffman@44133 ` 1727` ```lemma dim_image_le: ``` huffman@44133 ` 1728` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` huffman@44133 ` 1729` ``` assumes lf: "linear f" shows "dim (f ` S) \ dim (S)" ``` huffman@44133 ` 1730` ```proof- ``` huffman@44133 ` 1731` ``` from basis_exists[of S] obtain B where ``` huffman@44133 ` 1732` ``` B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast ``` huffman@44133 ` 1733` ``` from B have fB: "finite B" "card B = dim S" using independent_bound by blast+ ``` huffman@44133 ` 1734` ``` have "dim (f ` S) \ card (f ` B)" ``` huffman@44133 ` 1735` ``` apply (rule span_card_ge_dim) ``` huffman@44133 ` 1736` ``` using lf B fB by (auto simp add: span_linear_image spans_image subset_image_iff) ``` huffman@44133 ` 1737` ``` also have "\ \ dim S" using card_image_le[OF fB(1)] fB by simp ``` huffman@44133 ` 1738` ``` finally show ?thesis . ``` huffman@44133 ` 1739` ```qed ``` huffman@44133 ` 1740` huffman@44133 ` 1741` ```text {* Relation between bases and injectivity/surjectivity of map. *} ``` huffman@44133 ` 1742` huffman@44133 ` 1743` ```lemma spanning_surjective_image: ``` huffman@44133 ` 1744` ``` assumes us: "UNIV \ span S" ``` huffman@44133 ` 1745` ``` and lf: "linear f" and sf: "surj f" ``` huffman@44133 ` 1746` ``` shows "UNIV \ span (f ` S)" ``` huffman@44133 ` 1747` ```proof- ``` huffman@44133 ` 1748` ``` have "UNIV \ f ` UNIV" using sf by (auto simp add: surj_def) ``` huffman@44133 ` 1749` ``` also have " \ \ span (f ` S)" using spans_image[OF lf us] . ``` huffman@44133 ` 1750` ```finally show ?thesis . ``` huffman@44133 ` 1751` ```qed ``` huffman@44133 ` 1752` huffman@44133 ` 1753` ```lemma independent_injective_image: ``` huffman@44133 ` 1754` ``` assumes iS: "independent S" and lf: "linear f" and fi: "inj f" ``` huffman@44133 ` 1755` ``` shows "independent (f ` S)" ``` huffman@44133 ` 1756` ```proof- ``` huffman@44133 ` 1757` ``` {fix a assume a: "a \ S" "f a \ span (f ` S - {f a})" ``` huffman@44133 ` 1758` ``` have eq: "f ` S - {f a} = f ` (S - {a})" using fi ``` huffman@44133 ` 1759` ``` by (auto simp add: inj_on_def) ``` huffman@44133 ` 1760` ``` from a have "f a \ f ` span (S -{a})" ``` huffman@44133 ` 1761` ``` unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast ``` huffman@44133 ` 1762` ``` hence "a \ span (S -{a})" using fi by (auto simp add: inj_on_def) ``` huffman@44133 ` 1763` ``` with a(1) iS have False by (simp add: dependent_def) } ``` huffman@44133 ` 1764` ``` then show ?thesis unfolding dependent_def by blast ``` huffman@44133 ` 1765` ```qed ``` huffman@44133 ` 1766` huffman@44133 ` 1767` ```text {* Picking an orthogonal replacement for a spanning set. *} ``` huffman@44133 ` 1768` huffman@44133 ` 1769` ``` (* FIXME : Move to some general theory ?*) ``` huffman@44133 ` 1770` ```definition "pairwise R S \ (\x \ S. \y\ S. x\y \ R x y)" ``` huffman@44133 ` 1771` huffman@44133 ` 1772` ```lemma vector_sub_project_orthogonal: "(b::'a::euclidean_space) \ (x - ((b \ x) / (b \ b)) *\<^sub>R b) = 0" ``` huffman@44133 ` 1773` ``` unfolding inner_simps by auto ``` huffman@44133 ` 1774` huffman@44133 ` 1775` ```lemma basis_orthogonal: ``` huffman@44133 ` 1776` ``` fixes B :: "('a::euclidean_space) set" ``` huffman@44133 ` 1777` ``` assumes fB: "finite B" ``` huffman@44133 ` 1778` ``` shows "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C" ``` huffman@44133 ` 1779` ``` (is " \C. ?P B C") ``` huffman@44133 ` 1780` ```proof(induct rule: finite_induct[OF fB]) ``` huffman@44133 ` 1781` ``` case 1 thus ?case apply (rule exI[where x="{}"]) by (auto simp add: pairwise_def) ``` huffman@44133 ` 1782` ```next ``` huffman@44133 ` 1783` ``` case (2 a B) ``` huffman@44133 ` 1784` ``` note fB = `finite B` and aB = `a \ B` ``` huffman@44133 ` 1785` ``` from `\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C` ``` huffman@44133 ` 1786` ``` obtain C where C: "finite C" "card C \ card B" ``` huffman@44133 ` 1787` ``` "span C = span B" "pairwise orthogonal C" by blast ``` huffman@44133 ` 1788` ``` let ?a = "a - setsum (\x. (x \ a / (x \ x)) *\<^sub>R x) C" ``` huffman@44133 ` 1789` ``` let ?C = "insert ?a C" ``` huffman@44133 ` 1790` ``` from C(1) have fC: "finite ?C" by simp ``` huffman@44133 ` 1791` ``` from fB aB C(1,2) have cC: "card ?C \ card (insert a B)" by (simp add: card_insert_if) ``` huffman@44133 ` 1792` ``` {fix x k ``` huffman@44133 ` 1793` ``` have th0: "\(a::'a) b c. a - (b - c) = c + (a - b)" by (simp add: field_simps) ``` huffman@44133 ` 1794` ``` have "x - k *\<^sub>R (a - (\x\C. (x \ a / (x \ x)) *\<^sub>R x)) \ span C \ x - k *\<^sub>R a \ span C" ``` huffman@44133 ` 1795` ``` apply (simp only: scaleR_right_diff_distrib th0) ``` huffman@44133 ` 1796` ``` apply (rule span_add_eq) ``` huffman@44133 ` 1797` ``` apply (rule span_mul) ``` huffman@44133 ` 1798` ``` apply (rule span_setsum[OF C(1)]) ``` huffman@44133 ` 1799` ``` apply clarify ``` huffman@44133 ` 1800` ``` apply (rule span_mul) ``` huffman@44133 ` 1801` ``` by (rule span_superset)} ``` huffman@44133 ` 1802` ``` then have SC: "span ?C = span (insert a B)" ``` huffman@44133 ` 1803` ``` unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto ``` huffman@44133 ` 1804` ``` thm pairwise_def ``` huffman@44133 ` 1805` ``` {fix x y assume xC: "x \ ?C" and yC: "y \ ?C" and xy: "x \ y" ``` huffman@44133 ` 1806` ``` {assume xa: "x = ?a" and ya: "y = ?a" ``` huffman@44133 ` 1807` ``` have "orthogonal x y" using xa ya xy by blast} ``` huffman@44133 ` 1808` ``` moreover ``` huffman@44133 ` 1809` ``` {assume xa: "x = ?a" and ya: "y \ ?a" "y \ C" ``` huffman@44133 ` 1810` ``` from ya have Cy: "C = insert y (C - {y})" by blast ``` huffman@44133 ` 1811` ``` have fth: "finite (C - {y})" using C by simp ``` huffman@44133 ` 1812` ``` have "orthogonal x y" ``` huffman@44133 ` 1813` ``` using xa ya ``` huffman@44133 ` 1814` ``` unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq ``` huffman@44133 ` 1815` ``` apply simp ``` huffman@44133 ` 1816` ``` apply (subst Cy) ``` huffman@44133 ` 1817` ``` using C(1) fth ``` huffman@44133 ` 1818` ``` apply (simp only: setsum_clauses) ``` huffman@44454 ` 1819` ``` apply (auto simp add: inner_add inner_commute[of y a] dot_lsum[OF fth]) ``` huffman@44133 ` 1820` ``` apply (rule setsum_0') ``` huffman@44133 ` 1821` ``` apply clarsimp ``` huffman@44133 ` 1822` ``` apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) ``` huffman@44133 ` 1823` ``` by auto} ``` huffman@44133 ` 1824` ``` moreover ``` huffman@44133 ` 1825` ``` {assume xa: "x \ ?a" "x \ C" and ya: "y = ?a" ``` huffman@44133 ` 1826` ``` from xa have Cx: "C = insert x (C - {x})" by blast ``` huffman@44133 ` 1827` ``` have fth: "finite (C - {x})" using C by simp ``` huffman@44133 ` 1828` ``` have "orthogonal x y" ``` huffman@44133 ` 1829` ``` using xa ya ``` huffman@44133 ` 1830` ``` unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq ``` huffman@44133 ` 1831` ``` apply simp ``` huffman@44133 ` 1832` ``` apply (subst Cx) ``` huffman@44133 ` 1833` ``` using C(1) fth ``` huffman@44133 ` 1834` ``` apply (simp only: setsum_clauses) ``` huffman@44133 ` 1835` ``` apply (subst inner_commute[of x]) ``` huffman@44454 ` 1836` ``` apply (auto simp add: inner_add inner_commute[of x a] dot_rsum[OF fth]) ``` huffman@44133 ` 1837` ``` apply (rule setsum_0') ``` huffman@44133 ` 1838` ``` apply clarsimp ``` huffman@44133 ` 1839` ``` apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) ``` huffman@44133 ` 1840` ``` by auto} ``` huffman@44133 ` 1841` ``` moreover ``` huffman@44133 ` 1842` ``` {assume xa: "x \ C" and ya: "y \ C" ``` huffman@44133 ` 1843` ``` have "orthogonal x y" using xa ya xy C(4) unfolding pairwise_def by blast} ``` huffman@44133 ` 1844` ``` ultimately have "orthogonal x y" using xC yC by blast} ``` huffman@44133 ` 1845` ``` then have CPO: "pairwise orthogonal ?C" unfolding pairwise_def by blast ``` huffman@44133 ` 1846` ``` from fC cC SC CPO have "?P (insert a B) ?C" by blast ``` huffman@44133 ` 1847` ``` then show ?case by blast ``` huffman@44133 ` 1848` ```qed ``` huffman@44133 ` 1849` huffman@44133 ` 1850` ```lemma orthogonal_basis_exists: ``` huffman@44133 ` 1851` ``` fixes V :: "('a::euclidean_space) set" ``` huffman@44133 ` 1852` ``` shows "\B. independent B \ B \ span V \ V \ span B \ (card B = dim V) \ pairwise orthogonal B" ``` huffman@44133 ` 1853` ```proof- ``` huffman@44133 ` 1854` ``` from basis_exists[of V] obtain B where B: "B \ V" "independent B" "V \ span B" "card B = dim V" by blast ``` huffman@44133 ` 1855` ``` from B have fB: "finite B" "card B = dim V" using independent_bound by auto ``` huffman@44133 ` 1856` ``` from basis_orthogonal[OF fB(1)] obtain C where ``` huffman@44133 ` 1857` ``` C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C" by blast ``` huffman@44133 ` 1858` ``` from C B ``` huffman@44133 ` 1859` ``` have CSV: "C \ span V" by (metis span_inc span_mono subset_trans) ``` huffman@44133 ` 1860` ``` from span_mono[OF B(3)] C have SVC: "span V \ span C" by (simp add: span_span) ``` huffman@44133 ` 1861` ``` from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB ``` huffman@44133 ` 1862` ``` have iC: "independent C" by (simp add: dim_span) ``` huffman@44133 ` 1863` ``` from C fB have "card C \ dim V" by simp ``` huffman@44133 ` 1864` ``` moreover have "dim V \ card C" using span_card_ge_dim[OF CSV SVC C(1)] ``` huffman@44133 ` 1865` ``` by (simp add: dim_span) ``` huffman@44133 ` 1866` ``` ultimately have CdV: "card C = dim V" using C(1) by simp ``` huffman@44133 ` 1867` ``` from C B CSV CdV iC show ?thesis by auto ``` huffman@44133 ` 1868` ```qed ``` huffman@44133 ` 1869` huffman@44133 ` 1870` ```lemma span_eq: "span S = span T \ S \ span T \ T \ span S" ``` huffman@44133 ` 1871` ``` using span_inc[unfolded subset_eq] using span_mono[of T "span S"] span_mono[of S "span T"] ``` huffman@44133 ` 1872` ``` by(auto simp add: span_span) ``` huffman@44133 ` 1873` huffman@44133 ` 1874` ```text {* Low-dimensional subset is in a hyperplane (weak orthogonal complement). *} ``` huffman@44133 ` 1875` huffman@44133 ` 1876` ```lemma span_not_univ_orthogonal: fixes S::"('a::euclidean_space) set" ``` huffman@44133 ` 1877` ``` assumes sU: "span S \ UNIV" ``` huffman@44133 ` 1878` ``` shows "\(a::'a). a \0 \ (\x \ span S. a \ x = 0)" ``` huffman@44133 ` 1879` ```proof- ``` huffman@44133 ` 1880` ``` from sU obtain a where a: "a \ span S" by blast ``` huffman@44133 ` 1881` ``` from orthogonal_basis_exists obtain B where ``` huffman@44133 ` 1882` ``` B: "independent B" "B \ span S" "S \ span B" "card B = dim S" "pairwise orthogonal B" ``` huffman@44133 ` 1883` ``` by blast ``` huffman@44133 ` 1884` ``` from B have fB: "finite B" "card B = dim S" using independent_bound by auto ``` huffman@44133 ` 1885` ``` from span_mono[OF B(2)] span_mono[OF B(3)] ``` huffman@44133 ` 1886` ``` have sSB: "span S = span B" by (simp add: span_span) ``` huffman@44133 ` 1887` ``` let ?a = "a - setsum (\b. (a \ b / (b \ b)) *\<^sub>R b) B" ``` huffman@44133 ` 1888` ``` have "setsum (\b. (a \ b / (b \ b)) *\<^sub>R b) B \ span S" ``` huffman@44133 ` 1889` ``` unfolding sSB ``` huffman@44133 ` 1890` ``` apply (rule span_setsum[OF fB(1)]) ``` huffman@44133 ` 1891` ``` apply clarsimp ``` huffman@44133 ` 1892` ``` apply (rule span_mul) ``` huffman@44133 ` 1893` ``` by (rule span_superset) ``` huffman@44133 ` 1894` ``` with a have a0:"?a \ 0" by auto ``` huffman@44133 ` 1895` ``` have "\x\span B. ?a \ x = 0" ``` huffman@44133 ` 1896` ``` proof(rule span_induct') ``` huffman@44454 ` 1897` ``` show "subspace {x. ?a \ x = 0}" by (auto simp add: subspace_def inner_add) ``` huffman@44133 ` 1898` ```next ``` huffman@44133 ` 1899` ``` {fix x assume x: "x \ B" ``` huffman@44133 ` 1900` ``` from x have B': "B = insert x (B - {x})" by blast ``` huffman@44133 ` 1901` ``` have fth: "finite (B - {x})" using fB by simp ``` huffman@44133 ` 1902` ``` have "?a \ x = 0" ``` huffman@44133 ` 1903` ``` apply (subst B') using fB fth ``` huffman@44133 ` 1904` ``` unfolding setsum_clauses(2)[OF fth] ``` huffman@44133 ` 1905` ``` apply simp unfolding inner_simps ``` huffman@44454 ` 1906` ``` apply (clarsimp simp add: inner_add dot_lsum) ``` huffman@44133 ` 1907` ``` apply (rule setsum_0', rule ballI) ``` huffman@44133 ` 1908` ``` unfolding inner_commute ``` huffman@44133 ` 1909` ``` by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])} ``` huffman@44133 ` 1910` ``` then show "\x \ B. ?a \ x = 0" by blast ``` huffman@44133 ` 1911` ``` qed ``` huffman@44133 ` 1912` ``` with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"]) ``` huffman@44133 ` 1913` ```qed ``` huffman@44133 ` 1914` huffman@44133 ` 1915` ```lemma span_not_univ_subset_hyperplane: ``` huffman@44133 ` 1916` ``` assumes SU: "span S \ (UNIV ::('a::euclidean_space) set)" ``` huffman@44133 ` 1917` ``` shows "\ a. a \0 \ span S \ {x. a \ x = 0}" ``` huffman@44133 ` 1918` ``` using span_not_univ_orthogonal[OF SU] by auto ``` huffman@44133 ` 1919` huffman@44133 ` 1920` ```lemma lowdim_subset_hyperplane: fixes S::"('a::euclidean_space) set" ``` huffman@44133 ` 1921` ``` assumes d: "dim S < DIM('a)" ``` huffman@44133 ` 1922` ``` shows "\(a::'a). a \ 0 \ span S \ {x. a \ x = 0}" ``` huffman@44133 ` 1923` ```proof- ``` huffman@44133 ` 1924` ``` {assume "span S = UNIV" ``` huffman@44133 ` 1925` ``` hence "dim (span S) = dim (UNIV :: ('a) set)" by simp ``` huffman@44133 ` 1926` ``` hence "dim S = DIM('a)" by (simp add: dim_span dim_UNIV) ``` huffman@44133 ` 1927` ``` with d have False by arith} ``` huffman@44133 ` 1928` ``` hence th: "span S \ UNIV" by blast ``` huffman@44133 ` 1929` ``` from span_not_univ_subset_hyperplane[OF th] show ?thesis . ``` huffman@44133 ` 1930` ```qed ``` huffman@44133 ` 1931` huffman@44133 ` 1932` ```text {* We can extend a linear basis-basis injection to the whole set. *} ``` huffman@44133 ` 1933` huffman@44133 ` 1934` ```lemma linear_indep_image_lemma: ``` huffman@44133 ` 1935` ``` assumes lf: "linear f" and fB: "finite B" ``` huffman@44133 ` 1936` ``` and ifB: "independent (f ` B)" ``` huffman@44133 ` 1937` ``` and fi: "inj_on f B" and xsB: "x \ span B" ``` huffman@44133 ` 1938` ``` and fx: "f x = 0" ``` huffman@44133 ` 1939` ``` shows "x = 0" ``` huffman@44133 ` 1940` ``` using fB ifB fi xsB fx ``` huffman@44133 ` 1941` ```proof(induct arbitrary: x rule: finite_induct[OF fB]) ``` huffman@44142 ` 1942` ``` case 1 thus ?case by auto ``` huffman@44133 ` 1943` ```next ``` huffman@44133 ` 1944` ``` case (2 a b x) ``` huffman@44133 ` 1945` ``` have fb: "finite b" using "2.prems" by simp ``` huffman@44133 ` 1946` ``` have th0: "f ` b \ f ` (insert a b)" ``` huffman@44133 ` 1947` ``` apply (rule image_mono) by blast ``` huffman@44133 ` 1948` ``` from independent_mono[ OF "2.prems"(2) th0] ``` huffman@44133 ` 1949` ``` have ifb: "independent (f ` b)" . ``` huffman@44133 ` 1950` ``` have fib: "inj_on f b" ``` huffman@44133 ` 1951` ``` apply (rule subset_inj_on [OF "2.prems"(3)]) ``` huffman@44133 ` 1952` ``` by blast ``` huffman@44133 ` 1953` ``` from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)] ``` huffman@44133 ` 1954` ``` obtain k where k: "x - k*\<^sub>R a \ span (b -{a})" by blast ``` huffman@44133 ` 1955` ``` have "f (x - k*\<^sub>R a) \ span (f ` b)" ``` huffman@44133 ` 1956` ``` unfolding span_linear_image[OF lf] ``` huffman@44133 ` 1957` ``` apply (rule imageI) ``` huffman@44133 ` 1958` ``` using k span_mono[of "b-{a}" b] by blast ``` huffman@44133 ` 1959` ``` hence "f x - k*\<^sub>R f a \ span (f ` b)" ``` huffman@44133 ` 1960` ``` by (simp add: linear_sub[OF lf] linear_cmul[OF lf]) ``` huffman@44133 ` 1961` ``` hence th: "-k *\<^sub>R f a \ span (f ` b)" ``` huffman@44133 ` 1962` ``` using "2.prems"(5) by simp ``` huffman@44133 ` 1963` ``` {assume k0: "k = 0" ``` huffman@44133 ` 1964` ``` from k0 k have "x \ span (b -{a})" by simp ``` huffman@44133 ` 1965` ``` then have "x \ span b" using span_mono[of "b-{a}" b] ``` huffman@44133 ` 1966` ``` by blast} ``` huffman@44133 ` 1967` ``` moreover ``` huffman@44133 ` 1968` ``` {assume k0: "k \ 0" ``` huffman@44133 ` 1969` ``` from span_mul[OF th, of "- 1/ k"] k0 ``` huffman@44133 ` 1970` ``` have th1: "f a \ span (f ` b)" ``` huffman@44133 ` 1971` ``` by auto ``` huffman@44133 ` 1972` ``` from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric] ``` huffman@44133 ` 1973` ``` have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast ``` huffman@44133 ` 1974` ``` from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"] ``` huffman@44133 ` 1975` ``` have "f a \ span (f ` b)" using tha ``` huffman@44133 ` 1976` ``` using "2.hyps"(2) ``` huffman@44133 ` 1977` ``` "2.prems"(3) by auto ``` huffman@44133 ` 1978` ``` with th1 have False by blast ``` huffman@44133 ` 1979` ``` then have "x \ span b" by blast} ``` huffman@44133 ` 1980` ``` ultimately have xsb: "x \ span b" by blast ``` huffman@44133 ` 1981` ``` from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] ``` huffman@44133 ` 1982` ``` show "x = 0" . ``` huffman@44133 ` 1983` ```qed ``` huffman@44133 ` 1984` huffman@44133 ` 1985` ```text {* We can extend a linear mapping from basis. *} ``` huffman@44133 ` 1986` huffman@44133 ` 1987` ```lemma linear_independent_extend_lemma: ``` huffman@44133 ` 1988` ``` fixes f :: "'a::real_vector \ 'b::real_vector" ``` huffman@44133 ` 1989` ``` assumes fi: "finite B" and ib: "independent B" ``` huffman@44133 ` 1990` ``` shows "\g. (\x\ span B. \y\ span B. g (x + y) = g x + g y) ``` huffman@44133 ` 1991` ``` \ (\x\ span B. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) ``` huffman@44133 ` 1992` ``` \ (\x\ B. g x = f x)" ``` huffman@44133 ` 1993` ```using ib fi ``` huffman@44133 ` 1994` ```proof(induct rule: finite_induct[OF fi]) ``` huffman@44142 ` 1995` ``` case 1 thus ?case by auto ``` huffman@44133 ` 1996` ```next ``` huffman@44133 ` 1997` ``` case (2 a b) ``` huffman@44133 ` 1998` ``` from "2.prems" "2.hyps" have ibf: "independent b" "finite b" ``` huffman@44133 ` 1999` ``` by (simp_all add: independent_insert) ``` huffman@44133 ` 2000` ``` from "2.hyps"(3)[OF ibf] obtain g where ``` huffman@44133 ` 2001` ``` g: "\x\span b. \y\span b. g (x + y) = g x + g y" ``` huffman@44133 ` 2002` ``` "\x\span b. \c. g (c *\<^sub>R x) = c *\<^sub>R g x" "\x\b. g x = f x" by blast ``` huffman@44133 ` 2003` ``` let ?h = "\z. SOME k. (z - k *\<^sub>R a) \ span b" ``` huffman@44133 ` 2004` ``` {fix z assume z: "z \ span (insert a b)" ``` huffman@44133 ` 2005` ``` have th0: "z - ?h z *\<^sub>R a \ span b" ``` huffman@44133 ` 2006` ``` apply (rule someI_ex) ``` huffman@44133 ` 2007` ``` unfolding span_breakdown_eq[symmetric] ``` huffman@44133 ` 2008` ``` using z . ``` huffman@44133 ` 2009` ``` {fix k assume k: "z - k *\<^sub>R a \ span b" ``` huffman@44133 ` 2010` ``` have eq: "z - ?h z *\<^sub>R a - (z - k*\<^sub>R a) = (k - ?h z) *\<^sub>R a" ``` huffman@44133 ` 2011` ``` by (simp add: field_simps scaleR_left_distrib [symmetric]) ``` huffman@44133 ` 2012` ``` from span_sub[OF th0 k] ``` huffman@44133 ` 2013` ``` have khz: "(k - ?h z) *\<^sub>R a \ span b" by (simp add: eq) ``` huffman@44133 ` 2014` ``` {assume "k \ ?h z" hence k0: "k - ?h z \ 0" by simp ``` huffman@44133 ` 2015` ``` from k0 span_mul[OF khz, of "1 /(k - ?h z)"] ``` huffman@44133 ` 2016` ``` have "a \ span b" by simp ``` huffman@44133 ` 2017` ``` with "2.prems"(1) "2.hyps"(2) have False ``` huffman@44133 ` 2018` ``` by (auto simp add: dependent_def)} ``` huffman@44133 ` 2019` ``` then have "k = ?h z" by blast} ``` huffman@44133 ` 2020` ``` with th0 have "z - ?h z *\<^sub>R a \ span b \ (\k. z - k *\<^sub>R a \ span b \ k = ?h z)" by blast} ``` huffman@44133 ` 2021` ``` note h = this ``` huffman@44133 ` 2022` ``` let ?g = "\z. ?h z *\<^sub>R f a + g (z - ?h z *\<^sub>R a)" ``` huffman@44133 ` 2023` ``` {fix x y assume x: "x \ span (insert a b)" and y: "y \ span (insert a b)" ``` huffman@44133 ` 2024` ``` have tha: "\(x::'a) y a k l. (x + y) - (k + l) *\<^sub>R a = (x - k *\<^sub>R a) + (y - l *\<^sub>R a)" ``` huffman@44133 ` 2025` ``` by (simp add: algebra_simps) ``` huffman@44133 ` 2026` ``` have addh: "?h (x + y) = ?h x + ?h y" ``` huffman@44133 ` 2027` ``` apply (rule conjunct2[OF h, rule_format, symmetric]) ``` huffman@44133 ` 2028` ``` apply (rule span_add[OF x y]) ``` huffman@44133 ` 2029` ``` unfolding tha ``` huffman@44133 ` 2030` ``` by (metis span_add x y conjunct1[OF h, rule_format]) ``` huffman@44133 ` 2031` ``` have "?g (x + y) = ?g x + ?g y" ``` huffman@44133 ` 2032` ``` unfolding addh tha ``` huffman@44133 ` 2033` ``` g(1)[rule_format,OF conjunct1[OF h, OF x] conjunct1[OF h, OF y]] ``` huffman@44133 ` 2034` ``` by (simp add: scaleR_left_distrib)} ``` huffman@44133 ` 2035` ``` moreover ``` huffman@44133 ` 2036` ``` {fix x:: "'a" and c:: real assume x: "x \ span (insert a b)" ``` huffman@44133 ` 2037` ``` have tha: "\(x::'a) c k a. c *\<^sub>R x - (c * k) *\<^sub>R a = c *\<^sub>R (x - k *\<^sub>R a)" ``` huffman@44133 ` 2038` ``` by (simp add: algebra_simps) ``` huffman@44133 ` 2039` ``` have hc: "?h (c *\<^sub>R x) = c * ?h x" ``` huffman@44133 ` 2040` ``` apply (rule conjunct2[OF h, rule_format, symmetric]) ``` huffman@44133 ` 2041` ``` apply (metis span_mul x) ``` huffman@44133 ` 2042` ``` by (metis tha span_mul x conjunct1[OF h]) ``` huffman@44133 ` 2043` ``` have "?g (c *\<^sub>R x) = c*\<^sub>R ?g x" ``` huffman@44133 ` 2044` ``` unfolding hc tha g(2)[rule_format, OF conjunct1[OF h, OF x]] ``` huffman@44133 ` 2045` ``` by (simp add: algebra_simps)} ``` huffman@44133 ` 2046` ``` moreover ``` huffman@44133 ` 2047` ``` {fix x assume x: "x \ (insert a b)" ``` huffman@44133 ` 2048` ``` {assume xa: "x = a" ``` huffman@44133 ` 2049` ``` have ha1: "1 = ?h a" ``` huffman@44133 ` 2050` ``` apply (rule conjunct2[OF h, rule_format]) ``` huffman@44133 ` 2051` ``` apply (metis span_superset insertI1) ``` huffman@44133 ` 2052` ``` using conjunct1[OF h, OF span_superset, OF insertI1] ``` huffman@44133 ` 2053` ``` by (auto simp add: span_0) ``` huffman@44133 ` 2054` huffman@44133 ` 2055` ``` from xa ha1[symmetric] have "?g x = f x" ``` huffman@44133 ` 2056` ``` apply simp ``` huffman@44133 ` 2057` ``` using g(2)[rule_format, OF span_0, of 0] ``` huffman@44133 ` 2058` ``` by simp} ``` huffman@44133 ` 2059` ``` moreover ``` huffman@44133 ` 2060` ``` {assume xb: "x \ b" ``` huffman@44133 ` 2061` ``` have h0: "0 = ?h x" ``` huffman@44133 ` 2062` ``` apply (rule conjunct2[OF h, rule_format]) ``` huffman@44133 ` 2063` ``` apply (metis span_superset x) ``` huffman@44133 ` 2064` ``` apply simp ``` huffman@44133 ` 2065` ``` apply (metis span_superset xb) ``` huffman@44133 ` 2066` ``` done ``` huffman@44133 ` 2067` ``` have "?g x = f x" ``` huffman@44133 ` 2068` ``` by (simp add: h0[symmetric] g(3)[rule_format, OF xb])} ``` huffman@44133 ` 2069` ``` ultimately have "?g x = f x" using x by blast } ``` huffman@44133 ` 2070` ``` ultimately show ?case apply - apply (rule exI[where x="?g"]) by blast ``` huffman@44133 ` 2071` ```qed ``` huffman@44133 ` 2072` huffman@44133 ` 2073` ```lemma linear_independent_extend: ``` huffman@44133 ` 2074` ``` assumes iB: "independent (B:: ('a::euclidean_space) set)" ``` huffman@44133 ` 2075` ``` shows "\g. linear g \ (\x\B. g x = f x)" ``` huffman@44133 ` 2076` ```proof- ``` huffman@44133 ` 2077` ``` from maximal_independent_subset_extend[of B UNIV] iB ``` huffman@44133 ` 2078` ``` obtain C where C: "B \ C" "independent C" "\x. x \ span C" by auto ``` huffman@44133 ` 2079` huffman@44133 ` 2080` ``` from C(2) independent_bound[of C] linear_independent_extend_lemma[of C f] ``` huffman@44133 ` 2081` ``` obtain g where g: "(\x\ span C. \y\ span C. g (x + y) = g x + g y) ``` huffman@44133 ` 2082` ``` \ (\x\ span C. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) ``` huffman@44133 ` 2083` ``` \ (\x\ C. g x = f x)" by blast ``` huffman@44133 ` 2084` ``` from g show ?thesis unfolding linear_def using C ``` huffman@44133 ` 2085` ``` apply clarsimp by blast ``` huffman@44133 ` 2086` ```qed ``` huffman@44133 ` 2087` huffman@44133 ` 2088` ```text {* Can construct an isomorphism between spaces of same dimension. *} ``` huffman@44133 ` 2089` huffman@44133 ` 2090` ```lemma card_le_inj: assumes fA: "finite A" and fB: "finite B" ``` huffman@44133 ` 2091` ``` and c: "card A \ card B" shows "(\f. f ` A \ B \ inj_on f A)" ``` huffman@44133 ` 2092` ```using fB c ``` huffman@44133 ` 2093` ```proof(induct arbitrary: B rule: finite_induct[OF fA]) ``` huffman@44133 ` 2094` ``` case 1 thus ?case by simp ``` huffman@44133 ` 2095` ```next ``` huffman@44133 ` 2096` ``` case (2 x s t) ``` huffman@44133 ` 2097` ``` thus ?case ``` huffman@44133 ` 2098` ``` proof(induct rule: finite_induct[OF "2.prems"(1)]) ``` huffman@44133 ` 2099` ``` case 1 then show ?case by simp ``` huffman@44133 ` 2100` ``` next ``` huffman@44133 ` 2101` ``` case (2 y t) ``` huffman@44133 ` 2102` ``` from "2.prems"(1,2,5) "2.hyps"(1,2) have cst:"card s \ card t" by simp ``` huffman@44133 ` 2103` ``` from "2.prems"(3) [OF "2.hyps"(1) cst] obtain f where ``` huffman@44133 ` 2104` ``` f: "f ` s \ t \ inj_on f s" by blast ``` huffman@44133 ` 2105` ``` from f "2.prems"(2) "2.hyps"(2) show ?case ``` huffman@44133 ` 2106` ``` apply - ``` huffman@44133 ` 2107` ``` apply (rule exI[where x = "\z. if z = x then y else f z"]) ``` huffman@44133 ` 2108` ``` by (auto simp add: inj_on_def) ``` huffman@44133 ` 2109` ``` qed ``` huffman@44133 ` 2110` ```qed ``` huffman@44133 ` 2111` huffman@44133 ` 2112` ```lemma card_subset_eq: assumes fB: "finite B" and AB: "A \ B" and ``` huffman@44133 ` 2113` ``` c: "card A = card B" ``` huffman@44133 ` 2114` ``` shows "A = B" ``` huffman@44133 ` 2115` ```proof- ``` huffman@44133 ` 2116` ``` from fB AB have fA: "finite A" by (auto intro: finite_subset) ``` huffman@44133 ` 2117` ``` from fA fB have fBA: "finite (B - A)" by auto ``` huffman@44133 ` 2118` ``` have e: "A \ (B - A) = {}" by blast ``` huffman@44133 ` 2119` ``` have eq: "A \ (B - A) = B" using AB by blast ``` huffman@44133 ` 2120` ``` from card_Un_disjoint[OF fA fBA e, unfolded eq c] ``` huffman@44133 ` 2121` ``` have "card (B - A) = 0" by arith ``` huffman@44133 ` 2122` ``` hence "B - A = {}" unfolding card_eq_0_iff using fA fB by simp ``` huffman@44133 ` 2123` ``` with AB show "A = B" by blast ``` huffman@44133 ` 2124` ```qed ``` huffman@44133 ` 2125` huffman@44133 ` 2126` ```lemma subspace_isomorphism: ``` huffman@44133 ` 2127` ``` assumes s: "subspace (S:: ('a::euclidean_space) set)" ``` huffman@44133 ` 2128` ``` and t: "subspace (T :: ('b::euclidean_space) set)" ``` huffman@44133 ` 2129` ``` and d: "dim S = dim T" ``` huffman@44133 ` 2130` ``` shows "\f. linear f \ f ` S = T \ inj_on f S" ``` huffman@44133 ` 2131` ```proof- ``` huffman@44133 ` 2132` ``` from basis_exists[of S] independent_bound obtain B where ``` huffman@44133 ` 2133` ``` B: "B \ S" "independent B" "S \ span B" "card B = dim S" and fB: "finite B" by blast ``` huffman@44133 ` 2134` ``` from basis_exists[of T] independent_bound obtain C where ``` huffman@44133 ` 2135` ``` C: "C \ T" "independent C" "T \ span C" "card C = dim T" and fC: "finite C" by blast ``` huffman@44133 ` 2136` ``` from B(4) C(4) card_le_inj[of B C] d obtain f where ``` huffman@44133 ` 2137` ``` f: "f ` B \ C" "inj_on f B" using `finite B` `finite C` by auto ``` huffman@44133 ` 2138` ``` from linear_independent_extend[OF B(2)] obtain g where ``` huffman@44133 ` 2139` ``` g: "linear g" "\x\ B. g x = f x" by blast ``` huffman@44133 ` 2140` ``` from inj_on_iff_eq_card[OF fB, of f] f(2) ``` huffman@44133 ` 2141` ``` have "card (f ` B) = card B" by simp ``` huffman@44133 ` 2142` ``` with B(4) C(4) have ceq: "card (f ` B) = card C" using d ``` huffman@44133 ` 2143` ``` by simp ``` huffman@44133 ` 2144` ``` have "g ` B = f ` B" using g(2) ``` huffman@44133 ` 2145` ``` by (auto simp add: image_iff) ``` huffman@44133 ` 2146` ``` also have "\ = C" using card_subset_eq[OF fC f(1) ceq] . ``` huffman@44133 ` 2147` ``` finally have gBC: "g ` B = C" . ``` huffman@44133 ` 2148` ``` have gi: "inj_on g B" using f(2) g(2) ``` huffman@44133 ` 2149` ``` by (auto simp add: inj_on_def) ``` huffman@44133 ` 2150` ``` note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi] ``` huffman@44133 ` 2151` ``` {fix x y assume x: "x \ S" and y: "y \ S" and gxy:"g x = g y" ``` huffman@44133 ` 2152` ``` from B(3) x y have x': "x \ span B" and y': "y \ span B" by blast+ ``` huffman@44133 ` 2153` ``` from gxy have th0: "g (x - y) = 0" by (simp add: linear_sub[OF g(1)]) ``` huffman@44133 ` 2154` ``` have th1: "x - y \ span B" using x' y' by (metis span_sub) ``` huffman@44133 ` 2155` ``` have "x=y" using g0[OF th1 th0] by simp } ``` huffman@44133 ` 2156` ``` then have giS: "inj_on g S" ``` huffman@44133 ` 2157` ``` unfolding inj_on_def by blast ``` huffman@44133 ` 2158` ``` from span_subspace[OF B(1,3) s] ``` huffman@44133 ` 2159` ``` have "g ` S = span (g ` B)" by (simp add: span_linear_image[OF g(1)]) ``` huffman@44133 ` 2160` ``` also have "\ = span C" unfolding gBC .. ``` huffman@44133 ` 2161` ``` also have "\ = T" using span_subspace[OF C(1,3) t] . ``` huffman@44133 ` 2162` ``` finally have gS: "g ` S = T" . ``` huffman@44133 ` 2163` ``` from g(1) gS giS show ?thesis by blast ``` huffman@44133 ` 2164` ```qed ``` huffman@44133 ` 2165` huffman@44133 ` 2166` ```text {* Linear functions are equal on a subspace if they are on a spanning set. *} ``` huffman@44133 ` 2167` huffman@44133 ` 2168` ```lemma subspace_kernel: ``` huffman@44133 ` 2169` ``` assumes lf: "linear f" ``` huffman@44133 ` 2170` ``` shows "subspace {x. f x = 0}" ``` huffman@44133 ` 2171` ```apply (simp add: subspace_def) ``` huffman@44133 ` 2172` ```by (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf]) ``` huffman@44133 ` 2173` huffman@44133 ` 2174` ```lemma linear_eq_0_span: ``` huffman@44133 ` 2175` ``` assumes lf: "linear f" and f0: "\x\B. f x = 0" ``` huffman@44133 ` 2176` ``` shows "\x \ span B. f x = 0" ``` huffman@44170 ` 2177` ``` using f0 subspace_kernel[OF lf] ``` huffman@44170 ` 2178` ``` by (rule span_induct') ``` huffman@44133 ` 2179` huffman@44133 ` 2180` ```lemma linear_eq_0: ``` huffman@44133 ` 2181` ``` assumes lf: "linear f" and SB: "S \ span B" and f0: "\x\B. f x = 0" ``` huffman@44133 ` 2182` ``` shows "\x \ S. f x = 0" ``` huffman@44133 ` 2183` ``` by (metis linear_eq_0_span[OF lf] subset_eq SB f0) ``` huffman@44133 ` 2184` huffman@44133 ` 2185` ```lemma linear_eq: ``` huffman@44133 ` 2186` ``` assumes lf: "linear f" and lg: "linear g" and S: "S \ span B" ``` huffman@44133 ` 2187` ``` and fg: "\ x\ B. f x = g x" ``` huffman@44133 ` 2188` ``` shows "\x\ S. f x = g x" ``` huffman@44133 ` 2189` ```proof- ``` huffman@44133 ` 2190` ``` let ?h = "\x. f x - g x" ``` huffman@44133 ` 2191` ``` from fg have fg': "\x\ B. ?h x = 0" by simp ``` huffman@44133 ` 2192` ``` from linear_eq_0[OF linear_compose_sub[OF lf lg] S fg'] ``` huffman@44133 ` 2193` ``` show ?thesis by simp ``` huffman@44133 ` 2194` ```qed ``` huffman@44133 ` 2195` huffman@44133 ` 2196` ```lemma linear_eq_stdbasis: ``` huffman@44133 ` 2197` ``` assumes lf: "linear (f::'a::euclidean_space \ _)" and lg: "linear g" ``` huffman@44133 ` 2198` ``` and fg: "\i (UNIV :: 'a set)" ``` huffman@44133 ` 2204` ``` from equalityD2[OF span_basis'[where 'a='a]] ``` huffman@44133 ` 2205` ``` have IU: " (UNIV :: 'a set) \ span ?I" by blast ``` huffman@44133 ` 2206` ``` have "f x = g x" apply(rule linear_eq[OF lf lg IU,rule_format]) using fg x by auto } ``` huffman@44454 ` 2207` ``` then show ?thesis by auto ``` huffman@44133 ` 2208` ```qed ``` huffman@44133 ` 2209` huffman@44133 ` 2210` ```text {* Similar results for bilinear functions. *} ``` huffman@44133 ` 2211` huffman@44133 ` 2212` ```lemma bilinear_eq: ``` huffman@44133 ` 2213` ``` assumes bf: "bilinear f" ``` huffman@44133 ` 2214` ``` and bg: "bilinear g" ``` huffman@44133 ` 2215` ``` and SB: "S \ span B" and TC: "T \ span C" ``` huffman@44133 ` 2216` ``` and fg: "\x\ B. \y\ C. f x y = g x y" ``` huffman@44133 ` 2217` ``` shows "\x\S. \y\T. f x y = g x y " ``` huffman@44133 ` 2218` ```proof- ``` huffman@44170 ` 2219` ``` let ?P = "{x. \y\ span C. f x y = g x y}" ``` huffman@44133 ` 2220` ``` from bf bg have sp: "subspace ?P" ``` huffman@44133 ` 2221` ``` unfolding bilinear_def linear_def subspace_def bf bg ``` huffman@44170 ` 2222` ``` by(auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) ``` huffman@44133 ` 2223` huffman@44133 ` 2224` ``` have "\x \ span B. \y\ span C. f x y = g x y" ``` huffman@44170 ` 2225` ``` apply (rule span_induct' [OF _ sp]) ``` huffman@44133 ` 2226` ``` apply (rule ballI) ``` huffman@44170 ` 2227` ``` apply (rule span_induct') ``` huffman@44170 ` 2228` ``` apply (simp add: fg) ``` huffman@44133 ` 2229` ``` apply (auto simp add: subspace_def) ``` huffman@44133 ` 2230` ``` using bf bg unfolding bilinear_def linear_def ``` huffman@44170 ` 2231` ``` by(auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf]) ``` huffman@44454 ` 2232` ``` then show ?thesis using SB TC by auto ``` huffman@44133 ` 2233` ```qed ``` huffman@44133 ` 2234` huffman@44133 ` 2235` ```lemma bilinear_eq_stdbasis: fixes f::"'a::euclidean_space \ 'b::euclidean_space \ _" ``` huffman@44133 ` 2236` ``` assumes bf: "bilinear f" ``` huffman@44133 ` 2237` ``` and bg: "bilinear g" ``` huffman@44133 ` 2238` ``` and fg: "\ijx \ (basis ` {..y\ (basis ` {.. 'b::euclidean_space" ``` huffman@44133 ` 2249` ``` assumes lf: "linear f" and fi: "inj f" ``` huffman@44133 ` 2250` ``` shows "\g. linear g \ g o f = id" ``` huffman@44133 ` 2251` ```proof- ``` huffman@44133 ` 2252` ``` from linear_independent_extend[OF independent_injective_image, OF independent_basis, OF lf fi] ``` huffman@44133 ` 2253` ``` obtain h:: "'b => 'a" where h: "linear h" ``` huffman@44133 ` 2254` ``` " \x \ f ` basis ` {..i f) (basis i) = id (basis i)" ``` huffman@44133 ` 2257` ``` using inv_o_cancel[OF fi, unfolded fun_eq_iff id_def o_def] ``` huffman@44133 ` 2258` ``` by auto ``` huffman@44133 ` 2259` huffman@44133 ` 2260` ``` from linear_eq_stdbasis[OF linear_compose[OF lf h(1)] linear_id th] ``` huffman@44133 ` 2261` ``` have "h o f = id" . ``` huffman@44133 ` 2262` ``` then show ?thesis using h(1) by blast ``` huffman@44133 ` 2263` ```qed ``` huffman@44133 ` 2264` huffman@44133 ` 2265` ```lemma linear_surjective_right_inverse: fixes f::"'a::euclidean_space => 'b::euclidean_space" ``` huffman@44133 ` 2266` ``` assumes lf: "linear f" and sf: "surj f" ``` huffman@44133 ` 2267` ``` shows "\g. linear g \ f o g = id" ``` huffman@44133 ` 2268` ```proof- ``` huffman@44133 ` 2269` ``` from linear_independent_extend[OF independent_basis[where 'a='b],of "inv f"] ``` huffman@44133 ` 2270` ``` obtain h:: "'b \ 'a" where ``` huffman@44133 ` 2271` ``` h: "linear h" "\ x\ basis ` {..i 'b::euclidean_space"} is also surjective. *} ``` huffman@44133 ` 2281` huffman@44133 ` 2282` ```lemma linear_injective_imp_surjective: fixes f::"'a::euclidean_space => 'a::euclidean_space" ``` huffman@44133 ` 2283` ``` assumes lf: "linear f" and fi: "inj f" ``` huffman@44133 ` 2284` ``` shows "surj f" ``` huffman@44133 ` 2285` ```proof- ``` huffman@44133 ` 2286` ``` let ?U = "UNIV :: 'a set" ``` huffman@44133 ` 2287` ``` from basis_exists[of ?U] obtain B ``` huffman@44133 ` 2288` ``` where B: "B \ ?U" "independent B" "?U \ span B" "card B = dim ?U" ``` huffman@44133 ` 2289` ``` by blast ``` huffman@44133 ` 2290` ``` from B(4) have d: "dim ?U = card B" by simp ``` huffman@44133 ` 2291` ``` have th: "?U \ span (f ` B)" ``` huffman@44133 ` 2292` ``` apply (rule card_ge_dim_independent) ``` huffman@44133 ` 2293` ``` apply blast ``` huffman@44133 ` 2294` ``` apply (rule independent_injective_image[OF B(2) lf fi]) ``` huffman@44133 ` 2295` ``` apply (rule order_eq_refl) ``` huffman@44133 ` 2296` ``` apply (rule sym) ``` huffman@44133 ` 2297` ``` unfolding d ``` huffman@44133 ` 2298` ``` apply (rule card_image) ``` huffman@44133 ` 2299` ``` apply (rule subset_inj_on[OF fi]) ``` huffman@44133 ` 2300` ``` by blast ``` huffman@44133 ` 2301` ``` from th show ?thesis ``` huffman@44133 ` 2302` ``` unfolding span_linear_image[OF lf] surj_def ``` huffman@44133 ` 2303` ``` using B(3) by blast ``` huffman@44133 ` 2304` ```qed ``` huffman@44133 ` 2305` huffman@44133 ` 2306` ```text {* And vice versa. *} ``` huffman@44133 ` 2307` huffman@44133 ` 2308` ```lemma surjective_iff_injective_gen: ``` huffman@44133 ` 2309` ``` assumes fS: "finite S" and fT: "finite T" and c: "card S = card T" ``` huffman@44133 ` 2310` ``` and ST: "f ` S \ T" ``` huffman@44133 ` 2311` ``` shows "(\y \ T. \x \ S. f x = y) \ inj_on f S" (is "?lhs \ ?rhs") ``` huffman@44133 ` 2312` ```proof- ``` huffman@44133 ` 2313` ``` {assume h: "?lhs" ``` huffman@44133 ` 2314` ``` {fix x y assume x: "x \ S" and y: "y \ S" and f: "f x = f y" ``` huffman@44133 ` 2315` ``` from x fS have S0: "card S \ 0" by auto ``` huffman@44133 ` 2316` ``` {assume xy: "x \ y" ``` huffman@44133 ` 2317` ``` have th: "card S \ card (f ` (S - {y}))" ``` huffman@44133 ` 2318` ``` unfolding c ``` huffman@44133 ` 2319` ``` apply (rule card_mono) ``` huffman@44133 ` 2320` ``` apply (rule finite_imageI) ``` huffman@44133 ` 2321` ``` using fS apply simp ``` huffman@44133 ` 2322` ``` using h xy x y f unfolding subset_eq image_iff ``` huffman@44133 ` 2323` ``` apply auto ``` huffman@44133 ` 2324` ``` apply (case_tac "xa = f x") ``` huffman@44133 ` 2325` ``` apply (rule bexI[where x=x]) ``` huffman@44133 ` 2326` ``` apply auto ``` huffman@44133 ` 2327` ``` done ``` huffman@44133 ` 2328` ``` also have " \ \ card (S -{y})" ``` huffman@44133 ` 2329` ``` apply (rule card_image_le) ``` huffman@44133 ` 2330` ``` using fS by simp ``` huffman@44133 ` 2331` ``` also have "\ \ card S - 1" using y fS by simp ``` huffman@44133 ` 2332` ``` finally have False using S0 by arith } ```