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