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