src/HOL/Analysis/Linear_Algebra.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 months ago) changeset 69981 3dced198b9ec parent 69683 8b3458ca0762 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
 hoelzl@63627 ` 1` ```(* Title: HOL/Analysis/Linear_Algebra.thy ``` huffman@44133 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` huffman@44133 ` 3` ```*) ``` huffman@44133 ` 4` nipkow@69517 ` 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) ``` immler@68072 ` 26` ``` show "f (- a) = - f a" by (rule f.neg) ``` immler@68072 ` 27` ``` show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scale) ``` huffman@44133 ` 28` ```qed ``` huffman@44133 ` 29` lp15@68069 ` 30` ```lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x \ (UNIV::'a::finite set)}" ``` lp15@68069 ` 31` ``` using finite finite_image_set by blast ``` huffman@44133 ` 32` immler@69675 ` 33` ```lemma substdbasis_expansion_unique: ``` immler@69675 ` 34` ``` includes inner_syntax ``` immler@69675 ` 35` ``` assumes d: "d \ Basis" ``` immler@69675 ` 36` ``` shows "(\i\d. f i *\<^sub>R i) = (x::'a::euclidean_space) \ ``` immler@69675 ` 37` ``` (\i\Basis. (i \ d \ f i = x \ i) \ (i \ d \ x \ i = 0))" ``` immler@69675 ` 38` ```proof - ``` immler@69675 ` 39` ``` have *: "\x a b P. x * (if P then a else b) = (if P then x * a else x * b)" ``` immler@69675 ` 40` ``` by auto ``` immler@69675 ` 41` ``` have **: "finite d" ``` immler@69675 ` 42` ``` by (auto intro: finite_subset[OF assms]) ``` immler@69675 ` 43` ``` have ***: "\i. i \ Basis \ (\i\d. f i *\<^sub>R i) \ i = (\x\d. if x = i then f x else 0)" ``` immler@69675 ` 44` ``` using d ``` immler@69675 ` 45` ``` by (auto intro!: sum.cong simp: inner_Basis inner_sum_left) ``` immler@69675 ` 46` ``` show ?thesis ``` immler@69675 ` 47` ``` unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***) ``` immler@69675 ` 48` ```qed ``` immler@69675 ` 49` immler@69675 ` 50` ```lemma independent_substdbasis: "d \ Basis \ independent d" ``` immler@69675 ` 51` ``` by (rule independent_mono[OF independent_Basis]) ``` immler@69675 ` 52` immler@69675 ` 53` ```lemma sum_not_0: "sum f A \ 0 \ \a \ A. f a \ 0" ``` immler@69675 ` 54` ``` by (rule ccontr) auto ``` immler@69675 ` 55` immler@69675 ` 56` ```lemma subset_translation_eq [simp]: ``` immler@69675 ` 57` ``` fixes a :: "'a::real_vector" shows "(+) a ` s \ (+) a ` t \ s \ t" ``` immler@69675 ` 58` ``` by auto ``` immler@69675 ` 59` immler@69675 ` 60` ```lemma translate_inj_on: ``` immler@69675 ` 61` ``` fixes A :: "'a::ab_group_add set" ``` immler@69675 ` 62` ``` shows "inj_on (\x. a + x) A" ``` immler@69675 ` 63` ``` unfolding inj_on_def by auto ``` immler@69675 ` 64` immler@69675 ` 65` ```lemma translation_assoc: ``` immler@69675 ` 66` ``` fixes a b :: "'a::ab_group_add" ``` immler@69675 ` 67` ``` shows "(\x. b + x) ` ((\x. a + x) ` S) = (\x. (a + b) + x) ` S" ``` immler@69675 ` 68` ``` by auto ``` immler@69675 ` 69` immler@69675 ` 70` ```lemma translation_invert: ``` immler@69675 ` 71` ``` fixes a :: "'a::ab_group_add" ``` immler@69675 ` 72` ``` assumes "(\x. a + x) ` A = (\x. a + x) ` B" ``` immler@69675 ` 73` ``` shows "A = B" ``` immler@69675 ` 74` ```proof - ``` immler@69675 ` 75` ``` have "(\x. -a + x) ` ((\x. a + x) ` A) = (\x. - a + x) ` ((\x. a + x) ` B)" ``` immler@69675 ` 76` ``` using assms by auto ``` immler@69675 ` 77` ``` then show ?thesis ``` immler@69675 ` 78` ``` using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto ``` immler@69675 ` 79` ```qed ``` immler@69675 ` 80` immler@69675 ` 81` ```lemma translation_galois: ``` immler@69675 ` 82` ``` fixes a :: "'a::ab_group_add" ``` immler@69675 ` 83` ``` shows "T = ((\x. a + x) ` S) \ S = ((\x. (- a) + x) ` T)" ``` immler@69675 ` 84` ``` using translation_assoc[of "-a" a S] ``` immler@69675 ` 85` ``` apply auto ``` immler@69675 ` 86` ``` using translation_assoc[of a "-a" T] ``` immler@69675 ` 87` ``` apply auto ``` immler@69675 ` 88` ``` done ``` immler@69675 ` 89` immler@69675 ` 90` ```lemma translation_inverse_subset: ``` immler@69675 ` 91` ``` assumes "((\x. - a + x) ` V) \ (S :: 'n::ab_group_add set)" ``` immler@69675 ` 92` ``` shows "V \ ((\x. a + x) ` S)" ``` immler@69675 ` 93` ```proof - ``` immler@69675 ` 94` ``` { ``` immler@69675 ` 95` ``` fix x ``` immler@69675 ` 96` ``` assume "x \ V" ``` immler@69675 ` 97` ``` then have "x-a \ S" using assms by auto ``` immler@69675 ` 98` ``` then have "x \ {a + v |v. v \ S}" ``` immler@69675 ` 99` ``` apply auto ``` immler@69675 ` 100` ``` apply (rule exI[of _ "x-a"], simp) ``` immler@69675 ` 101` ``` done ``` immler@69675 ` 102` ``` then have "x \ ((\x. a+x) ` S)" by auto ``` immler@69675 ` 103` ``` } ``` immler@69675 ` 104` ``` then show ?thesis by auto ``` immler@69675 ` 105` ```qed ``` wenzelm@53406 ` 106` nipkow@68901 ` 107` ```subsection%unimportant \More interesting properties of the norm\ ``` hoelzl@63050 ` 108` immler@69674 ` 109` ```unbundle inner_syntax ``` hoelzl@63050 ` 110` wenzelm@69597 ` 111` ```text\Equality of vectors in terms of \<^term>\(\)\ products.\ ``` hoelzl@63050 ` 112` hoelzl@63050 ` 113` ```lemma linear_componentwise: ``` hoelzl@63050 ` 114` ``` fixes f:: "'a::euclidean_space \ 'b::real_inner" ``` hoelzl@63050 ` 115` ``` assumes lf: "linear f" ``` hoelzl@63050 ` 116` ``` shows "(f x) \ j = (\i\Basis. (x\i) * (f i\j))" (is "?lhs = ?rhs") ``` hoelzl@63050 ` 117` ```proof - ``` immler@68072 ` 118` ``` interpret linear f by fact ``` hoelzl@63050 ` 119` ``` have "?rhs = (\i\Basis. (x\i) *\<^sub>R (f i))\j" ``` nipkow@64267 ` 120` ``` by (simp add: inner_sum_left) ``` hoelzl@63050 ` 121` ``` then show ?thesis ``` immler@68072 ` 122` ``` by (simp add: euclidean_representation sum[symmetric] scale[symmetric]) ``` hoelzl@63050 ` 123` ```qed ``` hoelzl@63050 ` 124` hoelzl@63050 ` 125` ```lemma vector_eq: "x = y \ x \ x = x \ y \ y \ y = x \ x" ``` hoelzl@63050 ` 126` ``` (is "?lhs \ ?rhs") ``` hoelzl@63050 ` 127` ```proof ``` hoelzl@63050 ` 128` ``` assume ?lhs ``` hoelzl@63050 ` 129` ``` then show ?rhs by simp ``` hoelzl@63050 ` 130` ```next ``` hoelzl@63050 ` 131` ``` assume ?rhs ``` hoelzl@63050 ` 132` ``` then have "x \ x - x \ y = 0 \ x \ y - y \ y = 0" ``` hoelzl@63050 ` 133` ``` by simp ``` hoelzl@63050 ` 134` ``` then have "x \ (x - y) = 0 \ y \ (x - y) = 0" ``` hoelzl@63050 ` 135` ``` by (simp add: inner_diff inner_commute) ``` hoelzl@63050 ` 136` ``` then have "(x - y) \ (x - y) = 0" ``` hoelzl@63050 ` 137` ``` by (simp add: field_simps inner_diff inner_commute) ``` hoelzl@63050 ` 138` ``` then show "x = y" by simp ``` hoelzl@63050 ` 139` ```qed ``` hoelzl@63050 ` 140` hoelzl@63050 ` 141` ```lemma norm_triangle_half_r: ``` hoelzl@63050 ` 142` ``` "norm (y - x1) < e / 2 \ norm (y - x2) < e / 2 \ norm (x1 - x2) < e" ``` hoelzl@63050 ` 143` ``` using dist_triangle_half_r unfolding dist_norm[symmetric] by auto ``` hoelzl@63050 ` 144` hoelzl@63050 ` 145` ```lemma norm_triangle_half_l: ``` hoelzl@63050 ` 146` ``` assumes "norm (x - y) < e / 2" ``` hoelzl@63050 ` 147` ``` and "norm (x' - y) < e / 2" ``` hoelzl@63050 ` 148` ``` shows "norm (x - x') < e" ``` hoelzl@63050 ` 149` ``` using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]] ``` hoelzl@63050 ` 150` ``` unfolding dist_norm[symmetric] . ``` hoelzl@63050 ` 151` lp15@66420 ` 152` ```lemma abs_triangle_half_r: ``` lp15@66420 ` 153` ``` fixes y :: "'a::linordered_field" ``` lp15@66420 ` 154` ``` shows "abs (y - x1) < e / 2 \ abs (y - x2) < e / 2 \ abs (x1 - x2) < e" ``` lp15@66420 ` 155` ``` by linarith ``` lp15@66420 ` 156` lp15@66420 ` 157` ```lemma abs_triangle_half_l: ``` lp15@66420 ` 158` ``` fixes y :: "'a::linordered_field" ``` lp15@66420 ` 159` ``` assumes "abs (x - y) < e / 2" ``` lp15@66420 ` 160` ``` and "abs (x' - y) < e / 2" ``` lp15@66420 ` 161` ``` shows "abs (x - x') < e" ``` lp15@66420 ` 162` ``` using assms by linarith ``` lp15@66420 ` 163` nipkow@64267 ` 164` ```lemma sum_clauses: ``` nipkow@64267 ` 165` ``` shows "sum f {} = 0" ``` nipkow@64267 ` 166` ``` and "finite S \ sum f (insert x S) = (if x \ S then sum f S else f x + sum f S)" ``` hoelzl@63050 ` 167` ``` by (auto simp add: insert_absorb) ``` hoelzl@63050 ` 168` hoelzl@63050 ` 169` ```lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" ``` hoelzl@63050 ` 170` ```proof ``` hoelzl@63050 ` 171` ``` assume "\x. x \ y = x \ z" ``` hoelzl@63050 ` 172` ``` then have "\x. x \ (y - z) = 0" ``` hoelzl@63050 ` 173` ``` by (simp add: inner_diff) ``` hoelzl@63050 ` 174` ``` then have "(y - z) \ (y - z) = 0" .. ``` hoelzl@63050 ` 175` ``` then show "y = z" by simp ``` hoelzl@63050 ` 176` ```qed simp ``` hoelzl@63050 ` 177` hoelzl@63050 ` 178` ```lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = y" ``` hoelzl@63050 ` 179` ```proof ``` hoelzl@63050 ` 180` ``` assume "\z. x \ z = y \ z" ``` hoelzl@63050 ` 181` ``` then have "\z. (x - y) \ z = 0" ``` hoelzl@63050 ` 182` ``` by (simp add: inner_diff) ``` hoelzl@63050 ` 183` ``` then have "(x - y) \ (x - y) = 0" .. ``` hoelzl@63050 ` 184` ``` then show "x = y" by simp ``` hoelzl@63050 ` 185` ```qed simp ``` hoelzl@63050 ` 186` immler@69619 ` 187` ```subsection \Substandard Basis\ ``` immler@69619 ` 188` immler@69619 ` 189` ```lemma ex_card: ``` immler@69619 ` 190` ``` assumes "n \ card A" ``` immler@69619 ` 191` ``` shows "\S\A. card S = n" ``` immler@69619 ` 192` ```proof (cases "finite A") ``` immler@69619 ` 193` ``` case True ``` immler@69619 ` 194` ``` from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..n \ card A\ have "{..< n} \ {..< card A}" "inj_on f {..< n}" ``` immler@69619 ` 196` ``` by (auto simp: bij_betw_def intro: subset_inj_on) ``` immler@69619 ` 197` ``` ultimately have "f ` {..< n} \ A" "card (f ` {..< n}) = n" ``` immler@69619 ` 198` ``` by (auto simp: bij_betw_def card_image) ``` immler@69619 ` 199` ``` then show ?thesis by blast ``` immler@69619 ` 200` ```next ``` immler@69619 ` 201` ``` case False ``` immler@69619 ` 202` ``` with \n \ card A\ show ?thesis by force ``` immler@69619 ` 203` ```qed ``` immler@69619 ` 204` immler@69619 ` 205` ```lemma subspace_substandard: "subspace {x::'a::euclidean_space. (\i\Basis. P i \ x\i = 0)}" ``` immler@69619 ` 206` ``` by (auto simp: subspace_def inner_add_left) ``` immler@69619 ` 207` immler@69619 ` 208` ```lemma dim_substandard: ``` immler@69619 ` 209` ``` assumes d: "d \ Basis" ``` immler@69619 ` 210` ``` shows "dim {x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0} = card d" (is "dim ?A = _") ``` immler@69619 ` 211` ```proof (rule dim_unique) ``` immler@69619 ` 212` ``` from d show "d \ ?A" ``` immler@69619 ` 213` ``` by (auto simp: inner_Basis) ``` immler@69619 ` 214` ``` from d show "independent d" ``` immler@69619 ` 215` ``` by (rule independent_mono [OF independent_Basis]) ``` immler@69619 ` 216` ``` have "x \ span d" if "\i\Basis. i \ d \ x \ i = 0" for x ``` immler@69619 ` 217` ``` proof - ``` immler@69619 ` 218` ``` have "finite d" ``` immler@69619 ` 219` ``` by (rule finite_subset [OF d finite_Basis]) ``` immler@69619 ` 220` ``` then have "(\i\d. (x \ i) *\<^sub>R i) \ span d" ``` immler@69619 ` 221` ``` by (simp add: span_sum span_clauses) ``` immler@69619 ` 222` ``` also have "(\i\d. (x \ i) *\<^sub>R i) = (\i\Basis. (x \ i) *\<^sub>R i)" ``` immler@69619 ` 223` ``` by (rule sum.mono_neutral_cong_left [OF finite_Basis d]) (auto simp: that) ``` immler@69619 ` 224` ``` finally show "x \ span d" ``` immler@69619 ` 225` ``` by (simp only: euclidean_representation) ``` immler@69619 ` 226` ``` qed ``` immler@69619 ` 227` ``` then show "?A \ span d" by auto ``` immler@69619 ` 228` ```qed simp ``` immler@69619 ` 229` hoelzl@63050 ` 230` nipkow@68901 ` 231` ```subsection \Orthogonality\ ``` hoelzl@63050 ` 232` immler@67962 ` 233` ```definition%important (in real_inner) "orthogonal x y \ x \ y = 0" ``` immler@67962 ` 234` hoelzl@63050 ` 235` ```context real_inner ``` hoelzl@63050 ` 236` ```begin ``` hoelzl@63050 ` 237` lp15@63072 ` 238` ```lemma orthogonal_self: "orthogonal x x \ x = 0" ``` lp15@63072 ` 239` ``` by (simp add: orthogonal_def) ``` lp15@63072 ` 240` hoelzl@63050 ` 241` ```lemma orthogonal_clauses: ``` hoelzl@63050 ` 242` ``` "orthogonal a 0" ``` hoelzl@63050 ` 243` ``` "orthogonal a x \ orthogonal a (c *\<^sub>R x)" ``` hoelzl@63050 ` 244` ``` "orthogonal a x \ orthogonal a (- x)" ``` hoelzl@63050 ` 245` ``` "orthogonal a x \ orthogonal a y \ orthogonal a (x + y)" ``` hoelzl@63050 ` 246` ``` "orthogonal a x \ orthogonal a y \ orthogonal a (x - y)" ``` hoelzl@63050 ` 247` ``` "orthogonal 0 a" ``` hoelzl@63050 ` 248` ``` "orthogonal x a \ orthogonal (c *\<^sub>R x) a" ``` hoelzl@63050 ` 249` ``` "orthogonal x a \ orthogonal (- x) a" ``` hoelzl@63050 ` 250` ``` "orthogonal x a \ orthogonal y a \ orthogonal (x + y) a" ``` hoelzl@63050 ` 251` ``` "orthogonal x a \ orthogonal y a \ orthogonal (x - y) a" ``` hoelzl@63050 ` 252` ``` unfolding orthogonal_def inner_add inner_diff by auto ``` hoelzl@63050 ` 253` hoelzl@63050 ` 254` ```end ``` hoelzl@63050 ` 255` hoelzl@63050 ` 256` ```lemma orthogonal_commute: "orthogonal x y \ orthogonal y x" ``` hoelzl@63050 ` 257` ``` by (simp add: orthogonal_def inner_commute) ``` hoelzl@63050 ` 258` lp15@63114 ` 259` ```lemma orthogonal_scaleR [simp]: "c \ 0 \ orthogonal (c *\<^sub>R x) = orthogonal x" ``` lp15@63114 ` 260` ``` by (rule ext) (simp add: orthogonal_def) ``` lp15@63114 ` 261` lp15@63114 ` 262` ```lemma pairwise_ortho_scaleR: ``` lp15@63114 ` 263` ``` "pairwise (\i j. orthogonal (f i) (g j)) B ``` lp15@63114 ` 264` ``` \ pairwise (\i j. orthogonal (a i *\<^sub>R f i) (a j *\<^sub>R g j)) B" ``` lp15@63114 ` 265` ``` by (auto simp: pairwise_def orthogonal_clauses) ``` lp15@63114 ` 266` lp15@63114 ` 267` ```lemma orthogonal_rvsum: ``` nipkow@64267 ` 268` ``` "\finite s; \y. y \ s \ orthogonal x (f y)\ \ orthogonal x (sum f s)" ``` lp15@63114 ` 269` ``` by (induction s rule: finite_induct) (auto simp: orthogonal_clauses) ``` lp15@63114 ` 270` lp15@63114 ` 271` ```lemma orthogonal_lvsum: ``` nipkow@64267 ` 272` ``` "\finite s; \x. x \ s \ orthogonal (f x) y\ \ orthogonal (sum f s) y" ``` lp15@63114 ` 273` ``` by (induction s rule: finite_induct) (auto simp: orthogonal_clauses) ``` lp15@63114 ` 274` lp15@63114 ` 275` ```lemma norm_add_Pythagorean: ``` lp15@63114 ` 276` ``` assumes "orthogonal a b" ``` lp15@63114 ` 277` ``` shows "norm(a + b) ^ 2 = norm a ^ 2 + norm b ^ 2" ``` lp15@63114 ` 278` ```proof - ``` lp15@63114 ` 279` ``` from assms have "(a - (0 - b)) \ (a - (0 - b)) = a \ a - (0 - b \ b)" ``` lp15@63114 ` 280` ``` by (simp add: algebra_simps orthogonal_def inner_commute) ``` lp15@63114 ` 281` ``` then show ?thesis ``` lp15@63114 ` 282` ``` by (simp add: power2_norm_eq_inner) ``` lp15@63114 ` 283` ```qed ``` lp15@63114 ` 284` nipkow@64267 ` 285` ```lemma norm_sum_Pythagorean: ``` lp15@63114 ` 286` ``` assumes "finite I" "pairwise (\i j. orthogonal (f i) (f j)) I" ``` nipkow@64267 ` 287` ``` shows "(norm (sum f I))\<^sup>2 = (\i\I. (norm (f i))\<^sup>2)" ``` lp15@63114 ` 288` ```using assms ``` lp15@63114 ` 289` ```proof (induction I rule: finite_induct) ``` lp15@63114 ` 290` ``` case empty then show ?case by simp ``` lp15@63114 ` 291` ```next ``` lp15@63114 ` 292` ``` case (insert x I) ``` nipkow@64267 ` 293` ``` then have "orthogonal (f x) (sum f I)" ``` lp15@63114 ` 294` ``` by (metis pairwise_insert orthogonal_rvsum) ``` lp15@63114 ` 295` ``` with insert show ?case ``` lp15@63114 ` 296` ``` by (simp add: pairwise_insert norm_add_Pythagorean) ``` lp15@63114 ` 297` ```qed ``` lp15@63114 ` 298` hoelzl@63050 ` 299` immler@69683 ` 300` ```subsection \Orthogonality of a transformation\ ``` immler@69675 ` 301` immler@69675 ` 302` ```definition%important "orthogonal_transformation f \ linear f \ (\v w. f v \ f w = v \ w)" ``` immler@69675 ` 303` immler@69675 ` 304` ```lemma%unimportant orthogonal_transformation: ``` immler@69675 ` 305` ``` "orthogonal_transformation f \ linear f \ (\v. norm (f v) = norm v)" ``` immler@69675 ` 306` ``` unfolding orthogonal_transformation_def ``` immler@69675 ` 307` ``` apply auto ``` immler@69675 ` 308` ``` apply (erule_tac x=v in allE)+ ``` immler@69675 ` 309` ``` apply (simp add: norm_eq_sqrt_inner) ``` immler@69675 ` 310` ``` apply (simp add: dot_norm linear_add[symmetric]) ``` immler@69675 ` 311` ``` done ``` immler@69675 ` 312` immler@69675 ` 313` ```lemma%unimportant orthogonal_transformation_id [simp]: "orthogonal_transformation (\x. x)" ``` immler@69675 ` 314` ``` by (simp add: linear_iff orthogonal_transformation_def) ``` immler@69675 ` 315` immler@69675 ` 316` ```lemma%unimportant orthogonal_orthogonal_transformation: ``` immler@69675 ` 317` ``` "orthogonal_transformation f \ orthogonal (f x) (f y) \ orthogonal x y" ``` immler@69675 ` 318` ``` by (simp add: orthogonal_def orthogonal_transformation_def) ``` immler@69675 ` 319` immler@69675 ` 320` ```lemma%unimportant orthogonal_transformation_compose: ``` immler@69675 ` 321` ``` "\orthogonal_transformation f; orthogonal_transformation g\ \ orthogonal_transformation(f \ g)" ``` immler@69675 ` 322` ``` by (auto simp: orthogonal_transformation_def linear_compose) ``` immler@69675 ` 323` immler@69675 ` 324` ```lemma%unimportant orthogonal_transformation_neg: ``` immler@69675 ` 325` ``` "orthogonal_transformation(\x. -(f x)) \ orthogonal_transformation f" ``` immler@69675 ` 326` ``` by (auto simp: orthogonal_transformation_def dest: linear_compose_neg) ``` immler@69675 ` 327` immler@69675 ` 328` ```lemma%unimportant orthogonal_transformation_scaleR: "orthogonal_transformation f \ f (c *\<^sub>R v) = c *\<^sub>R f v" ``` immler@69675 ` 329` ``` by (simp add: linear_iff orthogonal_transformation_def) ``` immler@69675 ` 330` immler@69675 ` 331` ```lemma%unimportant orthogonal_transformation_linear: ``` immler@69675 ` 332` ``` "orthogonal_transformation f \ linear f" ``` immler@69675 ` 333` ``` by (simp add: orthogonal_transformation_def) ``` immler@69675 ` 334` immler@69675 ` 335` ```lemma%unimportant orthogonal_transformation_inj: ``` immler@69675 ` 336` ``` "orthogonal_transformation f \ inj f" ``` immler@69675 ` 337` ``` unfolding orthogonal_transformation_def inj_on_def ``` immler@69675 ` 338` ``` by (metis vector_eq) ``` immler@69675 ` 339` immler@69675 ` 340` ```lemma%unimportant orthogonal_transformation_surj: ``` immler@69675 ` 341` ``` "orthogonal_transformation f \ surj f" ``` immler@69675 ` 342` ``` for f :: "'a::euclidean_space \ 'a::euclidean_space" ``` immler@69675 ` 343` ``` by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear) ``` immler@69675 ` 344` immler@69675 ` 345` ```lemma%unimportant orthogonal_transformation_bij: ``` immler@69675 ` 346` ``` "orthogonal_transformation f \ bij f" ``` immler@69675 ` 347` ``` for f :: "'a::euclidean_space \ 'a::euclidean_space" ``` immler@69675 ` 348` ``` by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj) ``` immler@69675 ` 349` immler@69675 ` 350` ```lemma%unimportant orthogonal_transformation_inv: ``` immler@69675 ` 351` ``` "orthogonal_transformation f \ orthogonal_transformation (inv f)" ``` immler@69675 ` 352` ``` for f :: "'a::euclidean_space \ 'a::euclidean_space" ``` immler@69675 ` 353` ``` by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj) ``` immler@69675 ` 354` immler@69675 ` 355` ```lemma%unimportant orthogonal_transformation_norm: ``` immler@69675 ` 356` ``` "orthogonal_transformation f \ norm (f x) = norm x" ``` immler@69675 ` 357` ``` by (metis orthogonal_transformation) ``` immler@69675 ` 358` immler@69675 ` 359` nipkow@68901 ` 360` ```subsection \Bilinear functions\ ``` hoelzl@63050 ` 361` nipkow@69600 ` 362` ```definition%important ``` nipkow@69600 ` 363` ```bilinear :: "('a::real_vector \ 'b::real_vector \ 'c::real_vector) \ bool" where ``` nipkow@69600 ` 364` ```"bilinear f \ (\x. linear (\y. f x y)) \ (\y. linear (\x. f x y))" ``` hoelzl@63050 ` 365` hoelzl@63050 ` 366` ```lemma bilinear_ladd: "bilinear h \ h (x + y) z = h x z + h y z" ``` hoelzl@63050 ` 367` ``` by (simp add: bilinear_def linear_iff) ``` hoelzl@63050 ` 368` hoelzl@63050 ` 369` ```lemma bilinear_radd: "bilinear h \ h x (y + z) = h x y + h x z" ``` hoelzl@63050 ` 370` ``` by (simp add: bilinear_def linear_iff) ``` hoelzl@63050 ` 371` hoelzl@63050 ` 372` ```lemma bilinear_lmul: "bilinear h \ h (c *\<^sub>R x) y = c *\<^sub>R h x y" ``` hoelzl@63050 ` 373` ``` by (simp add: bilinear_def linear_iff) ``` hoelzl@63050 ` 374` hoelzl@63050 ` 375` ```lemma bilinear_rmul: "bilinear h \ h x (c *\<^sub>R y) = c *\<^sub>R h x y" ``` hoelzl@63050 ` 376` ``` by (simp add: bilinear_def linear_iff) ``` hoelzl@63050 ` 377` hoelzl@63050 ` 378` ```lemma bilinear_lneg: "bilinear h \ h (- x) y = - h x y" ``` hoelzl@63050 ` 379` ``` by (drule bilinear_lmul [of _ "- 1"]) simp ``` hoelzl@63050 ` 380` hoelzl@63050 ` 381` ```lemma bilinear_rneg: "bilinear h \ h x (- y) = - h x y" ``` hoelzl@63050 ` 382` ``` by (drule bilinear_rmul [of _ _ "- 1"]) simp ``` hoelzl@63050 ` 383` hoelzl@63050 ` 384` ```lemma (in ab_group_add) eq_add_iff: "x = x + y \ y = 0" ``` hoelzl@63050 ` 385` ``` using add_left_imp_eq[of x y 0] by auto ``` hoelzl@63050 ` 386` hoelzl@63050 ` 387` ```lemma bilinear_lzero: ``` hoelzl@63050 ` 388` ``` assumes "bilinear h" ``` hoelzl@63050 ` 389` ``` shows "h 0 x = 0" ``` hoelzl@63050 ` 390` ``` using bilinear_ladd [OF assms, of 0 0 x] by (simp add: eq_add_iff field_simps) ``` hoelzl@63050 ` 391` hoelzl@63050 ` 392` ```lemma bilinear_rzero: ``` hoelzl@63050 ` 393` ``` assumes "bilinear h" ``` hoelzl@63050 ` 394` ``` shows "h x 0 = 0" ``` hoelzl@63050 ` 395` ``` using bilinear_radd [OF assms, of x 0 0 ] by (simp add: eq_add_iff field_simps) ``` hoelzl@63050 ` 396` hoelzl@63050 ` 397` ```lemma bilinear_lsub: "bilinear h \ h (x - y) z = h x z - h y z" ``` hoelzl@63050 ` 398` ``` using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg) ``` hoelzl@63050 ` 399` hoelzl@63050 ` 400` ```lemma bilinear_rsub: "bilinear h \ h z (x - y) = h z x - h z y" ``` hoelzl@63050 ` 401` ``` using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg) ``` hoelzl@63050 ` 402` nipkow@64267 ` 403` ```lemma bilinear_sum: ``` immler@68072 ` 404` ``` assumes "bilinear h" ``` nipkow@64267 ` 405` ``` shows "h (sum f S) (sum g T) = sum (\(i,j). h (f i) (g j)) (S \ T) " ``` hoelzl@63050 ` 406` ```proof - ``` immler@68072 ` 407` ``` interpret l: linear "\x. h x y" for y using assms by (simp add: bilinear_def) ``` immler@68072 ` 408` ``` interpret r: linear "\y. h x y" for x using assms by (simp add: bilinear_def) ``` nipkow@64267 ` 409` ``` have "h (sum f S) (sum g T) = sum (\x. h (f x) (sum g T)) S" ``` immler@68072 ` 410` ``` by (simp add: l.sum) ``` nipkow@64267 ` 411` ``` also have "\ = sum (\x. sum (\y. h (f x) (g y)) T) S" ``` immler@68072 ` 412` ``` by (rule sum.cong) (simp_all add: r.sum) ``` hoelzl@63050 ` 413` ``` finally show ?thesis ``` nipkow@64267 ` 414` ``` unfolding sum.cartesian_product . ``` hoelzl@63050 ` 415` ```qed ``` hoelzl@63050 ` 416` hoelzl@63050 ` 417` nipkow@68901 ` 418` ```subsection \Adjoints\ ``` hoelzl@63050 ` 419` nipkow@69600 ` 420` ```definition%important adjoint :: "(('a::real_inner) \ ('b::real_inner)) \ 'b \ 'a" where ``` nipkow@69600 ` 421` ```"adjoint f = (SOME f'. \x y. f x \ y = x \ f' y)" ``` hoelzl@63050 ` 422` hoelzl@63050 ` 423` ```lemma adjoint_unique: ``` hoelzl@63050 ` 424` ``` assumes "\x y. inner (f x) y = inner x (g y)" ``` hoelzl@63050 ` 425` ``` shows "adjoint f = g" ``` hoelzl@63050 ` 426` ``` unfolding adjoint_def ``` hoelzl@63050 ` 427` ```proof (rule some_equality) ``` hoelzl@63050 ` 428` ``` show "\x y. inner (f x) y = inner x (g y)" ``` hoelzl@63050 ` 429` ``` by (rule assms) ``` hoelzl@63050 ` 430` ```next ``` hoelzl@63050 ` 431` ``` fix h ``` hoelzl@63050 ` 432` ``` assume "\x y. inner (f x) y = inner x (h y)" ``` hoelzl@63050 ` 433` ``` then have "\x y. inner x (g y) = inner x (h y)" ``` hoelzl@63050 ` 434` ``` using assms by simp ``` hoelzl@63050 ` 435` ``` then have "\x y. inner x (g y - h y) = 0" ``` hoelzl@63050 ` 436` ``` by (simp add: inner_diff_right) ``` hoelzl@63050 ` 437` ``` then have "\y. inner (g y - h y) (g y - h y) = 0" ``` hoelzl@63050 ` 438` ``` by simp ``` hoelzl@63050 ` 439` ``` then have "\y. h y = g y" ``` hoelzl@63050 ` 440` ``` by simp ``` hoelzl@63050 ` 441` ``` then show "h = g" by (simp add: ext) ``` hoelzl@63050 ` 442` ```qed ``` hoelzl@63050 ` 443` hoelzl@63050 ` 444` ```text \TODO: The following lemmas about adjoints should hold for any ``` wenzelm@63680 ` 445` ``` Hilbert space (i.e. complete inner product space). ``` wenzelm@68224 ` 446` ``` (see \<^url>\https://en.wikipedia.org/wiki/Hermitian_adjoint\) ``` hoelzl@63050 ` 447` ```\ ``` hoelzl@63050 ` 448` hoelzl@63050 ` 449` ```lemma adjoint_works: ``` hoelzl@63050 ` 450` ``` fixes f :: "'n::euclidean_space \ 'm::euclidean_space" ``` hoelzl@63050 ` 451` ``` assumes lf: "linear f" ``` hoelzl@63050 ` 452` ``` shows "x \ adjoint f y = f x \ y" ``` hoelzl@63050 ` 453` ```proof - ``` immler@68072 ` 454` ``` interpret linear f by fact ``` hoelzl@63050 ` 455` ``` have "\y. \w. \x. f x \ y = x \ w" ``` hoelzl@63050 ` 456` ``` proof (intro allI exI) ``` hoelzl@63050 ` 457` ``` fix y :: "'m" and x ``` hoelzl@63050 ` 458` ``` let ?w = "(\i\Basis. (f i \ y) *\<^sub>R i) :: 'n" ``` hoelzl@63050 ` 459` ``` have "f x \ y = f (\i\Basis. (x \ i) *\<^sub>R i) \ y" ``` hoelzl@63050 ` 460` ``` by (simp add: euclidean_representation) ``` hoelzl@63050 ` 461` ``` also have "\ = (\i\Basis. (x \ i) *\<^sub>R f i) \ y" ``` immler@68072 ` 462` ``` by (simp add: sum scale) ``` hoelzl@63050 ` 463` ``` finally show "f x \ y = x \ ?w" ``` nipkow@64267 ` 464` ``` by (simp add: inner_sum_left inner_sum_right mult.commute) ``` hoelzl@63050 ` 465` ``` qed ``` hoelzl@63050 ` 466` ``` then show ?thesis ``` hoelzl@63050 ` 467` ``` unfolding adjoint_def choice_iff ``` hoelzl@63050 ` 468` ``` by (intro someI2_ex[where Q="\f'. x \ f' y = f x \ y"]) auto ``` hoelzl@63050 ` 469` ```qed ``` hoelzl@63050 ` 470` hoelzl@63050 ` 471` ```lemma adjoint_clauses: ``` hoelzl@63050 ` 472` ``` fixes f :: "'n::euclidean_space \ 'm::euclidean_space" ``` hoelzl@63050 ` 473` ``` assumes lf: "linear f" ``` hoelzl@63050 ` 474` ``` shows "x \ adjoint f y = f x \ y" ``` hoelzl@63050 ` 475` ``` and "adjoint f y \ x = y \ f x" ``` hoelzl@63050 ` 476` ``` by (simp_all add: adjoint_works[OF lf] inner_commute) ``` hoelzl@63050 ` 477` hoelzl@63050 ` 478` ```lemma adjoint_linear: ``` hoelzl@63050 ` 479` ``` fixes f :: "'n::euclidean_space \ 'm::euclidean_space" ``` hoelzl@63050 ` 480` ``` assumes lf: "linear f" ``` hoelzl@63050 ` 481` ``` shows "linear (adjoint f)" ``` hoelzl@63050 ` 482` ``` by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m] ``` hoelzl@63050 ` 483` ``` adjoint_clauses[OF lf] inner_distrib) ``` hoelzl@63050 ` 484` hoelzl@63050 ` 485` ```lemma adjoint_adjoint: ``` hoelzl@63050 ` 486` ``` fixes f :: "'n::euclidean_space \ 'm::euclidean_space" ``` hoelzl@63050 ` 487` ``` assumes lf: "linear f" ``` hoelzl@63050 ` 488` ``` shows "adjoint (adjoint f) = f" ``` hoelzl@63050 ` 489` ``` by (rule adjoint_unique, simp add: adjoint_clauses [OF lf]) ``` hoelzl@63050 ` 490` hoelzl@63050 ` 491` hoelzl@63050 ` 492` ```subsection \Archimedean properties and useful consequences\ ``` hoelzl@63050 ` 493` hoelzl@63050 ` 494` ```text\Bernoulli's inequality\ ``` immler@68607 ` 495` ```proposition Bernoulli_inequality: ``` hoelzl@63050 ` 496` ``` fixes x :: real ``` hoelzl@63050 ` 497` ``` assumes "-1 \ x" ``` hoelzl@63050 ` 498` ``` shows "1 + n * x \ (1 + x) ^ n" ``` immler@68607 ` 499` ```proof (induct n) ``` hoelzl@63050 ` 500` ``` case 0 ``` hoelzl@63050 ` 501` ``` then show ?case by simp ``` hoelzl@63050 ` 502` ```next ``` hoelzl@63050 ` 503` ``` case (Suc n) ``` hoelzl@63050 ` 504` ``` have "1 + Suc n * x \ 1 + (Suc n)*x + n * x^2" ``` hoelzl@63050 ` 505` ``` by (simp add: algebra_simps) ``` hoelzl@63050 ` 506` ``` also have "... = (1 + x) * (1 + n*x)" ``` hoelzl@63050 ` 507` ``` by (auto simp: power2_eq_square algebra_simps of_nat_Suc) ``` hoelzl@63050 ` 508` ``` also have "... \ (1 + x) ^ Suc n" ``` hoelzl@63050 ` 509` ``` using Suc.hyps assms mult_left_mono by fastforce ``` hoelzl@63050 ` 510` ``` finally show ?case . ``` hoelzl@63050 ` 511` ```qed ``` hoelzl@63050 ` 512` hoelzl@63050 ` 513` ```corollary Bernoulli_inequality_even: ``` hoelzl@63050 ` 514` ``` fixes x :: real ``` hoelzl@63050 ` 515` ``` assumes "even n" ``` hoelzl@63050 ` 516` ``` shows "1 + n * x \ (1 + x) ^ n" ``` hoelzl@63050 ` 517` ```proof (cases "-1 \ x \ n=0") ``` hoelzl@63050 ` 518` ``` case True ``` hoelzl@63050 ` 519` ``` then show ?thesis ``` hoelzl@63050 ` 520` ``` by (auto simp: Bernoulli_inequality) ``` hoelzl@63050 ` 521` ```next ``` hoelzl@63050 ` 522` ``` case False ``` hoelzl@63050 ` 523` ``` then have "real n \ 1" ``` hoelzl@63050 ` 524` ``` by simp ``` hoelzl@63050 ` 525` ``` with False have "n * x \ -1" ``` hoelzl@63050 ` 526` ``` 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 ` 527` ``` then have "1 + n * x \ 0" ``` hoelzl@63050 ` 528` ``` by auto ``` hoelzl@63050 ` 529` ``` also have "... \ (1 + x) ^ n" ``` hoelzl@63050 ` 530` ``` using assms ``` hoelzl@63050 ` 531` ``` using zero_le_even_power by blast ``` hoelzl@63050 ` 532` ``` finally show ?thesis . ``` hoelzl@63050 ` 533` ```qed ``` hoelzl@63050 ` 534` hoelzl@63050 ` 535` ```corollary real_arch_pow: ``` hoelzl@63050 ` 536` ``` fixes x :: real ``` hoelzl@63050 ` 537` ``` assumes x: "1 < x" ``` hoelzl@63050 ` 538` ``` shows "\n. y < x^n" ``` hoelzl@63050 ` 539` ```proof - ``` hoelzl@63050 ` 540` ``` from x have x0: "x - 1 > 0" ``` hoelzl@63050 ` 541` ``` by arith ``` hoelzl@63050 ` 542` ``` from reals_Archimedean3[OF x0, rule_format, of y] ``` hoelzl@63050 ` 543` ``` obtain n :: nat where n: "y < real n * (x - 1)" by metis ``` hoelzl@63050 ` 544` ``` from x0 have x00: "x- 1 \ -1" by arith ``` hoelzl@63050 ` 545` ``` from Bernoulli_inequality[OF x00, of n] n ``` hoelzl@63050 ` 546` ``` have "y < x^n" by auto ``` hoelzl@63050 ` 547` ``` then show ?thesis by metis ``` hoelzl@63050 ` 548` ```qed ``` hoelzl@63050 ` 549` hoelzl@63050 ` 550` ```corollary real_arch_pow_inv: ``` hoelzl@63050 ` 551` ``` fixes x y :: real ``` hoelzl@63050 ` 552` ``` assumes y: "y > 0" ``` hoelzl@63050 ` 553` ``` and x1: "x < 1" ``` hoelzl@63050 ` 554` ``` shows "\n. x^n < y" ``` hoelzl@63050 ` 555` ```proof (cases "x > 0") ``` hoelzl@63050 ` 556` ``` case True ``` hoelzl@63050 ` 557` ``` with x1 have ix: "1 < 1/x" by (simp add: field_simps) ``` hoelzl@63050 ` 558` ``` from real_arch_pow[OF ix, of "1/y"] ``` hoelzl@63050 ` 559` ``` obtain n where n: "1/y < (1/x)^n" by blast ``` hoelzl@63050 ` 560` ``` then show ?thesis using y \x > 0\ ``` hoelzl@63050 ` 561` ``` by (auto simp add: field_simps) ``` hoelzl@63050 ` 562` ```next ``` hoelzl@63050 ` 563` ``` case False ``` hoelzl@63050 ` 564` ``` with y x1 show ?thesis ``` lp15@68069 ` 565` ``` by (metis less_le_trans not_less power_one_right) ``` hoelzl@63050 ` 566` ```qed ``` hoelzl@63050 ` 567` hoelzl@63050 ` 568` ```lemma forall_pos_mono: ``` hoelzl@63050 ` 569` ``` "(\d e::real. d < e \ P d \ P e) \ ``` hoelzl@63050 ` 570` ``` (\n::nat. n \ 0 \ P (inverse (real n))) \ (\e. 0 < e \ P e)" ``` hoelzl@63050 ` 571` ``` by (metis real_arch_inverse) ``` hoelzl@63050 ` 572` hoelzl@63050 ` 573` ```lemma forall_pos_mono_1: ``` hoelzl@63050 ` 574` ``` "(\d e::real. d < e \ P d \ P e) \ ``` hoelzl@63050 ` 575` ``` (\n. P (inverse (real (Suc n)))) \ 0 < e \ P e" ``` hoelzl@63050 ` 576` ``` apply (rule forall_pos_mono) ``` hoelzl@63050 ` 577` ``` apply auto ``` hoelzl@63050 ` 578` ``` apply (metis Suc_pred of_nat_Suc) ``` hoelzl@63050 ` 579` ``` done ``` hoelzl@63050 ` 580` hoelzl@63050 ` 581` immler@67962 ` 582` ```subsection%unimportant \Euclidean Spaces as Typeclass\ ``` huffman@44133 ` 583` hoelzl@50526 ` 584` ```lemma independent_Basis: "independent Basis" ``` immler@68072 ` 585` ``` by (rule independent_Basis) ``` hoelzl@50526 ` 586` huffman@53939 ` 587` ```lemma span_Basis [simp]: "span Basis = UNIV" ``` immler@68072 ` 588` ``` by (rule span_Basis) ``` huffman@44133 ` 589` hoelzl@50526 ` 590` ```lemma in_span_Basis: "x \ span Basis" ``` hoelzl@50526 ` 591` ``` unfolding span_Basis .. ``` hoelzl@50526 ` 592` wenzelm@53406 ` 593` immler@67962 ` 594` ```subsection%unimportant \Linearity and Bilinearity continued\ ``` huffman@44133 ` 595` huffman@44133 ` 596` ```lemma linear_bounded: ``` wenzelm@56444 ` 597` ``` fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" ``` huffman@44133 ` 598` ``` assumes lf: "linear f" ``` huffman@44133 ` 599` ``` shows "\B. \x. norm (f x) \ B * norm x" ``` huffman@53939 ` 600` ```proof ``` immler@68072 ` 601` ``` interpret linear f by fact ``` hoelzl@50526 ` 602` ``` let ?B = "\b\Basis. norm (f b)" ``` huffman@53939 ` 603` ``` show "\x. norm (f x) \ ?B * norm x" ``` huffman@53939 ` 604` ``` proof ``` wenzelm@53406 ` 605` ``` fix x :: 'a ``` hoelzl@50526 ` 606` ``` let ?g = "\b. (x \ b) *\<^sub>R f b" ``` hoelzl@50526 ` 607` ``` have "norm (f x) = norm (f (\b\Basis. (x \ b) *\<^sub>R b))" ``` hoelzl@50526 ` 608` ``` unfolding euclidean_representation .. ``` nipkow@64267 ` 609` ``` also have "\ = norm (sum ?g Basis)" ``` immler@68072 ` 610` ``` by (simp add: sum scale) ``` nipkow@64267 ` 611` ``` finally have th0: "norm (f x) = norm (sum ?g Basis)" . ``` lp15@64773 ` 612` ``` have th: "norm (?g i) \ norm (f i) * norm x" if "i \ Basis" for i ``` lp15@64773 ` 613` ``` proof - ``` lp15@64773 ` 614` ``` from Basis_le_norm[OF that, of x] ``` huffman@53939 ` 615` ``` show "norm (?g i) \ norm (f i) * norm x" ``` lp15@68069 ` 616` ``` unfolding norm_scaleR by (metis mult.commute mult_left_mono norm_ge_zero) ``` huffman@53939 ` 617` ``` qed ``` nipkow@64267 ` 618` ``` from sum_norm_le[of _ ?g, OF th] ``` huffman@53939 ` 619` ``` show "norm (f x) \ ?B * norm x" ``` nipkow@64267 ` 620` ``` unfolding th0 sum_distrib_right by metis ``` huffman@53939 ` 621` ``` qed ``` huffman@44133 ` 622` ```qed ``` huffman@44133 ` 623` huffman@44133 ` 624` ```lemma linear_conv_bounded_linear: ``` huffman@44133 ` 625` ``` fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" ``` huffman@44133 ` 626` ``` shows "linear f \ bounded_linear f" ``` huffman@44133 ` 627` ```proof ``` huffman@44133 ` 628` ``` assume "linear f" ``` huffman@53939 ` 629` ``` then interpret f: linear f . ``` huffman@44133 ` 630` ``` show "bounded_linear f" ``` huffman@44133 ` 631` ``` proof ``` huffman@44133 ` 632` ``` have "\B. \x. norm (f x) \ B * norm x" ``` wenzelm@60420 ` 633` ``` using \linear f\ by (rule linear_bounded) ``` wenzelm@49522 ` 634` ``` then show "\K. \x. norm (f x) \ norm x * K" ``` haftmann@57512 ` 635` ``` by (simp add: mult.commute) ``` huffman@44133 ` 636` ``` qed ``` huffman@44133 ` 637` ```next ``` huffman@44133 ` 638` ``` assume "bounded_linear f" ``` huffman@44133 ` 639` ``` then interpret f: bounded_linear f . ``` huffman@53939 ` 640` ``` show "linear f" .. ``` huffman@53939 ` 641` ```qed ``` huffman@53939 ` 642` paulson@61518 ` 643` ```lemmas linear_linear = linear_conv_bounded_linear[symmetric] ``` paulson@61518 ` 644` huffman@53939 ` 645` ```lemma linear_bounded_pos: ``` wenzelm@56444 ` 646` ``` fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" ``` huffman@53939 ` 647` ``` assumes lf: "linear f" ``` lp15@67982 ` 648` ``` obtains B where "B > 0" "\x. norm (f x) \ B * norm x" ``` huffman@53939 ` 649` ```proof - ``` huffman@53939 ` 650` ``` have "\B > 0. \x. norm (f x) \ norm x * B" ``` huffman@53939 ` 651` ``` using lf unfolding linear_conv_bounded_linear ``` huffman@53939 ` 652` ``` by (rule bounded_linear.pos_bounded) ``` lp15@67982 ` 653` ``` with that show ?thesis ``` lp15@67982 ` 654` ``` by (auto simp: mult.commute) ``` huffman@44133 ` 655` ```qed ``` huffman@44133 ` 656` lp15@67982 ` 657` ```lemma linear_invertible_bounded_below_pos: ``` lp15@67982 ` 658` ``` fixes f :: "'a::real_normed_vector \ 'b::euclidean_space" ``` lp15@67982 ` 659` ``` assumes "linear f" "linear g" "g \ f = id" ``` lp15@67982 ` 660` ``` obtains B where "B > 0" "\x. B * norm x \ norm(f x)" ``` lp15@67982 ` 661` ```proof - ``` lp15@67982 ` 662` ``` obtain B where "B > 0" and B: "\x. norm (g x) \ B * norm x" ``` lp15@67982 ` 663` ``` using linear_bounded_pos [OF \linear g\] by blast ``` lp15@67982 ` 664` ``` show thesis ``` lp15@67982 ` 665` ``` proof ``` lp15@67982 ` 666` ``` show "0 < 1/B" ``` lp15@67982 ` 667` ``` by (simp add: \B > 0\) ``` lp15@67982 ` 668` ``` show "1/B * norm x \ norm (f x)" for x ``` lp15@67982 ` 669` ``` proof - ``` lp15@67982 ` 670` ``` have "1/B * norm x = 1/B * norm (g (f x))" ``` lp15@67982 ` 671` ``` using assms by (simp add: pointfree_idE) ``` lp15@67982 ` 672` ``` also have "\ \ norm (f x)" ``` lp15@67982 ` 673` ``` using B [of "f x"] by (simp add: \B > 0\ mult.commute pos_divide_le_eq) ``` lp15@67982 ` 674` ``` finally show ?thesis . ``` lp15@67982 ` 675` ``` qed ``` lp15@67982 ` 676` ``` qed ``` lp15@67982 ` 677` ```qed ``` lp15@67982 ` 678` lp15@67982 ` 679` ```lemma linear_inj_bounded_below_pos: ``` lp15@67982 ` 680` ``` fixes f :: "'a::real_normed_vector \ 'b::euclidean_space" ``` lp15@67982 ` 681` ``` assumes "linear f" "inj f" ``` lp15@67982 ` 682` ``` obtains B where "B > 0" "\x. B * norm x \ norm(f x)" ``` immler@68072 ` 683` ``` using linear_injective_left_inverse [OF assms] ``` immler@68072 ` 684` ``` linear_invertible_bounded_below_pos assms by blast ``` lp15@67982 ` 685` wenzelm@49522 ` 686` ```lemma bounded_linearI': ``` wenzelm@56444 ` 687` ``` fixes f ::"'a::euclidean_space \ 'b::real_normed_vector" ``` wenzelm@53406 ` 688` ``` assumes "\x y. f (x + y) = f x + f y" ``` wenzelm@53406 ` 689` ``` and "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" ``` wenzelm@49522 ` 690` ``` shows "bounded_linear f" ``` immler@68072 ` 691` ``` using assms linearI linear_conv_bounded_linear by blast ``` huffman@44133 ` 692` huffman@44133 ` 693` ```lemma bilinear_bounded: ``` wenzelm@56444 ` 694` ``` fixes h :: "'m::euclidean_space \ 'n::euclidean_space \ 'k::real_normed_vector" ``` huffman@44133 ` 695` ``` assumes bh: "bilinear h" ``` huffman@44133 ` 696` ``` shows "\B. \x y. norm (h x y) \ B * norm x * norm y" ``` hoelzl@50526 ` 697` ```proof (clarify intro!: exI[of _ "\i\Basis. \j\Basis. norm (h i j)"]) ``` wenzelm@53406 ` 698` ``` fix x :: 'm ``` wenzelm@53406 ` 699` ``` fix y :: 'n ``` nipkow@64267 ` 700` ``` have "norm (h x y) = norm (h (sum (\i. (x \ i) *\<^sub>R i) Basis) (sum (\i. (y \ i) *\<^sub>R i) Basis))" ``` lp15@68069 ` 701` ``` by (simp add: euclidean_representation) ``` nipkow@64267 ` 702` ``` also have "\ = norm (sum (\ (i,j). h ((x \ i) *\<^sub>R i) ((y \ j) *\<^sub>R j)) (Basis \ Basis))" ``` immler@68072 ` 703` ``` unfolding bilinear_sum[OF bh] .. ``` hoelzl@50526 ` 704` ``` finally have th: "norm (h x y) = \" . ``` lp15@68069 ` 705` ``` have "\i j. \i \ Basis; j \ Basis\ ``` lp15@68069 ` 706` ``` \ \x \ i\ * (\y \ j\ * norm (h i j)) \ norm x * (norm y * norm (h i j))" ``` lp15@68069 ` 707` ``` by (auto simp add: zero_le_mult_iff Basis_le_norm mult_mono) ``` lp15@68069 ` 708` ``` then show "norm (h x y) \ (\i\Basis. \j\Basis. norm (h i j)) * norm x * norm y" ``` lp15@68069 ` 709` ``` unfolding sum_distrib_right th sum.cartesian_product ``` lp15@68069 ` 710` ``` by (clarsimp simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] ``` lp15@68069 ` 711` ``` field_simps simp del: scaleR_scaleR intro!: sum_norm_le) ``` huffman@44133 ` 712` ```qed ``` huffman@44133 ` 713` huffman@44133 ` 714` ```lemma bilinear_conv_bounded_bilinear: ``` huffman@44133 ` 715` ``` fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" ``` huffman@44133 ` 716` ``` shows "bilinear h \ bounded_bilinear h" ``` huffman@44133 ` 717` ```proof ``` huffman@44133 ` 718` ``` assume "bilinear h" ``` huffman@44133 ` 719` ``` show "bounded_bilinear h" ``` huffman@44133 ` 720` ``` proof ``` wenzelm@53406 ` 721` ``` fix x y z ``` wenzelm@53406 ` 722` ``` show "h (x + y) z = h x z + h y z" ``` wenzelm@60420 ` 723` ``` using \bilinear h\ unfolding bilinear_def linear_iff by simp ``` huffman@44133 ` 724` ``` next ``` wenzelm@53406 ` 725` ``` fix x y z ``` wenzelm@53406 ` 726` ``` show "h x (y + z) = h x y + h x z" ``` wenzelm@60420 ` 727` ``` using \bilinear h\ unfolding bilinear_def linear_iff by simp ``` huffman@44133 ` 728` ``` next ``` lp15@68069 ` 729` ``` show "h (scaleR r x) y = scaleR r (h x y)" "h x (scaleR r y) = scaleR r (h x y)" for r x y ``` wenzelm@60420 ` 730` ``` using \bilinear h\ unfolding bilinear_def linear_iff ``` lp15@68069 ` 731` ``` by simp_all ``` huffman@44133 ` 732` ``` next ``` huffman@44133 ` 733` ``` have "\B. \x y. norm (h x y) \ B * norm x * norm y" ``` wenzelm@60420 ` 734` ``` using \bilinear h\ by (rule bilinear_bounded) ``` wenzelm@49522 ` 735` ``` then show "\K. \x y. norm (h x y) \ norm x * norm y * K" ``` haftmann@57514 ` 736` ``` by (simp add: ac_simps) ``` huffman@44133 ` 737` ``` qed ``` huffman@44133 ` 738` ```next ``` huffman@44133 ` 739` ``` assume "bounded_bilinear h" ``` huffman@44133 ` 740` ``` then interpret h: bounded_bilinear h . ``` huffman@44133 ` 741` ``` show "bilinear h" ``` huffman@44133 ` 742` ``` unfolding bilinear_def linear_conv_bounded_linear ``` wenzelm@49522 ` 743` ``` using h.bounded_linear_left h.bounded_linear_right by simp ``` huffman@44133 ` 744` ```qed ``` huffman@44133 ` 745` huffman@53939 ` 746` ```lemma bilinear_bounded_pos: ``` wenzelm@56444 ` 747` ``` fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector" ``` huffman@53939 ` 748` ``` assumes bh: "bilinear h" ``` huffman@53939 ` 749` ``` shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y" ``` huffman@53939 ` 750` ```proof - ``` huffman@53939 ` 751` ``` have "\B > 0. \x y. norm (h x y) \ norm x * norm y * B" ``` huffman@53939 ` 752` ``` using bh [unfolded bilinear_conv_bounded_bilinear] ``` huffman@53939 ` 753` ``` by (rule bounded_bilinear.pos_bounded) ``` huffman@53939 ` 754` ``` then show ?thesis ``` haftmann@57514 ` 755` ``` by (simp only: ac_simps) ``` huffman@53939 ` 756` ```qed ``` huffman@53939 ` 757` immler@68072 ` 758` ```lemma bounded_linear_imp_has_derivative: "bounded_linear f \ (f has_derivative f) net" ``` immler@68072 ` 759` ``` by (auto simp add: has_derivative_def linear_diff linear_linear linear_def ``` immler@68072 ` 760` ``` dest: bounded_linear.linear) ``` lp15@63469 ` 761` lp15@63469 ` 762` ```lemma linear_imp_has_derivative: ``` lp15@63469 ` 763` ``` fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" ``` lp15@63469 ` 764` ``` shows "linear f \ (f has_derivative f) net" ``` immler@68072 ` 765` ``` by (simp add: bounded_linear_imp_has_derivative linear_conv_bounded_linear) ``` lp15@63469 ` 766` lp15@63469 ` 767` ```lemma bounded_linear_imp_differentiable: "bounded_linear f \ f differentiable net" ``` lp15@63469 ` 768` ``` using bounded_linear_imp_has_derivative differentiable_def by blast ``` lp15@63469 ` 769` lp15@63469 ` 770` ```lemma linear_imp_differentiable: ``` lp15@63469 ` 771` ``` fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" ``` lp15@63469 ` 772` ``` shows "linear f \ f differentiable net" ``` immler@68072 ` 773` ``` by (metis linear_imp_has_derivative differentiable_def) ``` lp15@63469 ` 774` wenzelm@49522 ` 775` nipkow@68901 ` 776` ```subsection%unimportant \We continue\ ``` huffman@44133 ` 777` huffman@44133 ` 778` ```lemma independent_bound: ``` wenzelm@53716 ` 779` ``` fixes S :: "'a::euclidean_space set" ``` wenzelm@53716 ` 780` ``` shows "independent S \ finite S \ card S \ DIM('a)" ``` immler@68072 ` 781` ``` by (metis dim_subset_UNIV finiteI_independent dim_span_eq_card_independent) ``` immler@68072 ` 782` immler@68072 ` 783` ```lemmas independent_imp_finite = finiteI_independent ``` huffman@44133 ` 784` lp15@61609 ` 785` ```corollary ``` paulson@60303 ` 786` ``` fixes S :: "'a::euclidean_space set" ``` paulson@60303 ` 787` ``` assumes "independent S" ``` immler@68072 ` 788` ``` shows independent_card_le:"card S \ DIM('a)" ``` immler@68072 ` 789` ``` using assms independent_bound by auto ``` lp15@63075 ` 790` wenzelm@49663 ` 791` ```lemma dependent_biggerset: ``` wenzelm@56444 ` 792` ``` fixes S :: "'a::euclidean_space set" ``` wenzelm@56444 ` 793` ``` shows "(finite S \ card S > DIM('a)) \ dependent S" ``` huffman@44133 ` 794` ``` by (metis independent_bound not_less) ``` huffman@44133 ` 795` wenzelm@60420 ` 796` ```text \Picking an orthogonal replacement for a spanning set.\ ``` huffman@44133 ` 797` wenzelm@53406 ` 798` ```lemma vector_sub_project_orthogonal: ``` wenzelm@53406 ` 799` ``` fixes b x :: "'a::euclidean_space" ``` wenzelm@53406 ` 800` ``` shows "b \ (x - ((b \ x) / (b \ b)) *\<^sub>R b) = 0" ``` huffman@44133 ` 801` ``` unfolding inner_simps by auto ``` huffman@44133 ` 802` huffman@44528 ` 803` ```lemma pairwise_orthogonal_insert: ``` huffman@44528 ` 804` ``` assumes "pairwise orthogonal S" ``` wenzelm@49522 ` 805` ``` and "\y. y \ S \ orthogonal x y" ``` huffman@44528 ` 806` ``` shows "pairwise orthogonal (insert x S)" ``` huffman@44528 ` 807` ``` using assms unfolding pairwise_def ``` huffman@44528 ` 808` ``` by (auto simp add: orthogonal_commute) ``` huffman@44528 ` 809` huffman@44133 ` 810` ```lemma basis_orthogonal: ``` wenzelm@53406 ` 811` ``` fixes B :: "'a::real_inner set" ``` huffman@44133 ` 812` ``` assumes fB: "finite B" ``` huffman@44133 ` 813` ``` shows "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C" ``` huffman@44133 ` 814` ``` (is " \C. ?P B C") ``` wenzelm@49522 ` 815` ``` using fB ``` wenzelm@49522 ` 816` ```proof (induct rule: finite_induct) ``` wenzelm@49522 ` 817` ``` case empty ``` wenzelm@53406 ` 818` ``` then show ?case ``` wenzelm@53406 ` 819` ``` apply (rule exI[where x="{}"]) ``` wenzelm@53406 ` 820` ``` apply (auto simp add: pairwise_def) ``` wenzelm@53406 ` 821` ``` done ``` huffman@44133 ` 822` ```next ``` wenzelm@49522 ` 823` ``` case (insert a B) ``` wenzelm@60420 ` 824` ``` note fB = \finite B\ and aB = \a \ B\ ``` wenzelm@60420 ` 825` ``` from \\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C\ ``` huffman@44133 ` 826` ``` obtain C where C: "finite C" "card C \ card B" ``` huffman@44133 ` 827` ``` "span C = span B" "pairwise orthogonal C" by blast ``` nipkow@64267 ` 828` ``` let ?a = "a - sum (\x. (x \ a / (x \ x)) *\<^sub>R x) C" ``` huffman@44133 ` 829` ``` let ?C = "insert ?a C" ``` wenzelm@53406 ` 830` ``` from C(1) have fC: "finite ?C" ``` wenzelm@53406 ` 831` ``` by simp ``` wenzelm@49522 ` 832` ``` from fB aB C(1,2) have cC: "card ?C \ card (insert a B)" ``` wenzelm@49522 ` 833` ``` by (simp add: card_insert_if) ``` wenzelm@53406 ` 834` ``` { ``` wenzelm@53406 ` 835` ``` fix x k ``` wenzelm@49522 ` 836` ``` have th0: "\(a::'a) b c. a - (b - c) = c + (a - b)" ``` wenzelm@49522 ` 837` ``` by (simp add: field_simps) ``` huffman@44133 ` 838` ``` 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 ` 839` ``` apply (simp only: scaleR_right_diff_distrib th0) ``` huffman@44133 ` 840` ``` apply (rule span_add_eq) ``` immler@68072 ` 841` ``` apply (rule span_scale) ``` nipkow@64267 ` 842` ``` apply (rule span_sum) ``` immler@68072 ` 843` ``` apply (rule span_scale) ``` immler@68072 ` 844` ``` apply (rule span_base) ``` wenzelm@49522 ` 845` ``` apply assumption ``` wenzelm@53406 ` 846` ``` done ``` wenzelm@53406 ` 847` ``` } ``` huffman@44133 ` 848` ``` then have SC: "span ?C = span (insert a B)" ``` huffman@44133 ` 849` ``` unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto ``` wenzelm@53406 ` 850` ``` { ``` wenzelm@53406 ` 851` ``` fix y ``` wenzelm@53406 ` 852` ``` assume yC: "y \ C" ``` wenzelm@53406 ` 853` ``` then have Cy: "C = insert y (C - {y})" ``` wenzelm@53406 ` 854` ``` by blast ``` wenzelm@53406 ` 855` ``` have fth: "finite (C - {y})" ``` wenzelm@53406 ` 856` ``` using C by simp ``` huffman@44528 ` 857` ``` have "orthogonal ?a y" ``` huffman@44528 ` 858` ``` unfolding orthogonal_def ``` nipkow@64267 ` 859` ``` unfolding inner_diff inner_sum_left right_minus_eq ``` nipkow@64267 ` 860` ``` unfolding sum.remove [OF \finite C\ \y \ C\] ``` huffman@44528 ` 861` ``` apply (clarsimp simp add: inner_commute[of y a]) ``` nipkow@64267 ` 862` ``` apply (rule sum.neutral) ``` huffman@44528 ` 863` ``` apply clarsimp ``` huffman@44528 ` 864` ``` apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) ``` wenzelm@60420 ` 865` ``` using \y \ C\ by auto ``` wenzelm@53406 ` 866` ``` } ``` wenzelm@60420 ` 867` ``` with \pairwise orthogonal C\ have CPO: "pairwise orthogonal ?C" ``` huffman@44528 ` 868` ``` by (rule pairwise_orthogonal_insert) ``` wenzelm@53406 ` 869` ``` from fC cC SC CPO have "?P (insert a B) ?C" ``` wenzelm@53406 ` 870` ``` by blast ``` huffman@44133 ` 871` ``` then show ?case by blast ``` huffman@44133 ` 872` ```qed ``` huffman@44133 ` 873` huffman@44133 ` 874` ```lemma orthogonal_basis_exists: ``` huffman@44133 ` 875` ``` fixes V :: "('a::euclidean_space) set" ``` immler@68072 ` 876` ``` shows "\B. independent B \ B \ span V \ V \ span B \ ``` immler@68072 ` 877` ``` (card B = dim V) \ pairwise orthogonal B" ``` wenzelm@49663 ` 878` ```proof - ``` wenzelm@49522 ` 879` ``` from basis_exists[of V] obtain B where ``` wenzelm@53406 ` 880` ``` B: "B \ V" "independent B" "V \ span B" "card B = dim V" ``` immler@68073 ` 881` ``` by force ``` wenzelm@53406 ` 882` ``` from B have fB: "finite B" "card B = dim V" ``` wenzelm@53406 ` 883` ``` using independent_bound by auto ``` huffman@44133 ` 884` ``` from basis_orthogonal[OF fB(1)] obtain C where ``` wenzelm@53406 ` 885` ``` C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C" ``` wenzelm@53406 ` 886` ``` by blast ``` wenzelm@53406 ` 887` ``` from C B have CSV: "C \ span V" ``` immler@68072 ` 888` ``` by (metis span_superset span_mono subset_trans) ``` wenzelm@53406 ` 889` ``` from span_mono[OF B(3)] C have SVC: "span V \ span C" ``` wenzelm@53406 ` 890` ``` by (simp add: span_span) ``` huffman@44133 ` 891` ``` from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB ``` wenzelm@53406 ` 892` ``` have iC: "independent C" ``` huffman@44133 ` 893` ``` by (simp add: dim_span) ``` wenzelm@53406 ` 894` ``` from C fB have "card C \ dim V" ``` wenzelm@53406 ` 895` ``` by simp ``` wenzelm@53406 ` 896` ``` moreover have "dim V \ card C" ``` wenzelm@53406 ` 897` ``` using span_card_ge_dim[OF CSV SVC C(1)] ``` immler@68072 ` 898` ``` by simp ``` wenzelm@53406 ` 899` ``` ultimately have CdV: "card C = dim V" ``` wenzelm@53406 ` 900` ``` using C(1) by simp ``` wenzelm@53406 ` 901` ``` from C B CSV CdV iC show ?thesis ``` wenzelm@53406 ` 902` ``` by auto ``` huffman@44133 ` 903` ```qed ``` huffman@44133 ` 904` wenzelm@60420 ` 905` ```text \Low-dimensional subset is in a hyperplane (weak orthogonal complement).\ ``` huffman@44133 ` 906` wenzelm@49522 ` 907` ```lemma span_not_univ_orthogonal: ``` wenzelm@53406 ` 908` ``` fixes S :: "'a::euclidean_space set" ``` huffman@44133 ` 909` ``` assumes sU: "span S \ UNIV" ``` wenzelm@56444 ` 910` ``` shows "\a::'a. a \ 0 \ (\x \ span S. a \ x = 0)" ``` wenzelm@49522 ` 911` ```proof - ``` wenzelm@53406 ` 912` ``` from sU obtain a where a: "a \ span S" ``` wenzelm@53406 ` 913` ``` by blast ``` huffman@44133 ` 914` ``` from orthogonal_basis_exists obtain B where ``` immler@68072 ` 915` ``` B: "independent B" "B \ span S" "S \ span B" ``` immler@68072 ` 916` ``` "card B = dim S" "pairwise orthogonal B" ``` huffman@44133 ` 917` ``` by blast ``` wenzelm@53406 ` 918` ``` from B have fB: "finite B" "card B = dim S" ``` wenzelm@53406 ` 919` ``` using independent_bound by auto ``` huffman@44133 ` 920` ``` from span_mono[OF B(2)] span_mono[OF B(3)] ``` wenzelm@53406 ` 921` ``` have sSB: "span S = span B" ``` wenzelm@53406 ` 922` ``` by (simp add: span_span) ``` nipkow@64267 ` 923` ``` let ?a = "a - sum (\b. (a \ b / (b \ b)) *\<^sub>R b) B" ``` nipkow@64267 ` 924` ``` have "sum (\b. (a \ b / (b \ b)) *\<^sub>R b) B \ span S" ``` huffman@44133 ` 925` ``` unfolding sSB ``` nipkow@64267 ` 926` ``` apply (rule span_sum) ``` immler@68072 ` 927` ``` apply (rule span_scale) ``` immler@68072 ` 928` ``` apply (rule span_base) ``` wenzelm@49522 ` 929` ``` apply assumption ``` wenzelm@49522 ` 930` ``` done ``` wenzelm@53406 ` 931` ``` with a have a0:"?a \ 0" ``` wenzelm@53406 ` 932` ``` by auto ``` lp15@68058 ` 933` ``` have "?a \ x = 0" if "x\span B" for x ``` lp15@68058 ` 934` ``` proof (rule span_induct [OF that]) ``` wenzelm@49522 ` 935` ``` show "subspace {x. ?a \ x = 0}" ``` wenzelm@49522 ` 936` ``` by (auto simp add: subspace_def inner_add) ``` wenzelm@49522 ` 937` ``` next ``` wenzelm@53406 ` 938` ``` { ``` wenzelm@53406 ` 939` ``` fix x ``` wenzelm@53406 ` 940` ``` assume x: "x \ B" ``` wenzelm@53406 ` 941` ``` from x have B': "B = insert x (B - {x})" ``` wenzelm@53406 ` 942` ``` by blast ``` wenzelm@53406 ` 943` ``` have fth: "finite (B - {x})" ``` wenzelm@53406 ` 944` ``` using fB by simp ``` huffman@44133 ` 945` ``` have "?a \ x = 0" ``` wenzelm@53406 ` 946` ``` apply (subst B') ``` wenzelm@53406 ` 947` ``` using fB fth ``` nipkow@64267 ` 948` ``` unfolding sum_clauses(2)[OF fth] ``` huffman@44133 ` 949` ``` apply simp unfolding inner_simps ``` nipkow@64267 ` 950` ``` apply (clarsimp simp add: inner_add inner_sum_left) ``` nipkow@64267 ` 951` ``` apply (rule sum.neutral, rule ballI) ``` wenzelm@63170 ` 952` ``` apply (simp only: inner_commute) ``` wenzelm@49711 ` 953` ``` apply (auto simp add: x field_simps ``` wenzelm@49711 ` 954` ``` intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format]) ``` wenzelm@53406 ` 955` ``` done ``` wenzelm@53406 ` 956` ``` } ``` lp15@68058 ` 957` ``` then show "?a \ x = 0" if "x \ B" for x ``` lp15@68058 ` 958` ``` using that by blast ``` lp15@68058 ` 959` ``` qed ``` wenzelm@53406 ` 960` ``` with a0 show ?thesis ``` wenzelm@53406 ` 961` ``` unfolding sSB by (auto intro: exI[where x="?a"]) ``` huffman@44133 ` 962` ```qed ``` huffman@44133 ` 963` huffman@44133 ` 964` ```lemma span_not_univ_subset_hyperplane: ``` wenzelm@53406 ` 965` ``` fixes S :: "'a::euclidean_space set" ``` wenzelm@53406 ` 966` ``` assumes SU: "span S \ UNIV" ``` huffman@44133 ` 967` ``` shows "\ a. a \0 \ span S \ {x. a \ x = 0}" ``` huffman@44133 ` 968` ``` using span_not_univ_orthogonal[OF SU] by auto ``` huffman@44133 ` 969` wenzelm@49663 ` 970` ```lemma lowdim_subset_hyperplane: ``` wenzelm@53406 ` 971` ``` fixes S :: "'a::euclidean_space set" ``` huffman@44133 ` 972` ``` assumes d: "dim S < DIM('a)" ``` wenzelm@56444 ` 973` ``` shows "\a::'a. a \ 0 \ span S \ {x. a \ x = 0}" ``` wenzelm@49522 ` 974` ```proof - ``` wenzelm@53406 ` 975` ``` { ``` wenzelm@53406 ` 976` ``` assume "span S = UNIV" ``` wenzelm@53406 ` 977` ``` then have "dim (span S) = dim (UNIV :: ('a) set)" ``` wenzelm@53406 ` 978` ``` by simp ``` wenzelm@53406 ` 979` ``` then have "dim S = DIM('a)" ``` immler@68072 ` 980` ``` by (metis Euclidean_Space.dim_UNIV dim_span) ``` wenzelm@53406 ` 981` ``` with d have False by arith ``` wenzelm@53406 ` 982` ``` } ``` wenzelm@53406 ` 983` ``` then have th: "span S \ UNIV" ``` wenzelm@53406 ` 984` ``` by blast ``` huffman@44133 ` 985` ``` from span_not_univ_subset_hyperplane[OF th] show ?thesis . ``` huffman@44133 ` 986` ```qed ``` huffman@44133 ` 987` huffman@44133 ` 988` ```lemma linear_eq_stdbasis: ``` wenzelm@56444 ` 989` ``` fixes f :: "'a::euclidean_space \ _" ``` wenzelm@56444 ` 990` ``` assumes lf: "linear f" ``` wenzelm@49663 ` 991` ``` and lg: "linear g" ``` lp15@68058 ` 992` ``` and fg: "\b. b \ Basis \ f b = g b" ``` huffman@44133 ` 993` ``` shows "f = g" ``` immler@68072 ` 994` ``` using linear_eq_on_span[OF lf lg, of Basis] fg ``` immler@68072 ` 995` ``` by auto ``` immler@68072 ` 996` huffman@44133 ` 997` wenzelm@60420 ` 998` ```text \Similar results for bilinear functions.\ ``` huffman@44133 ` 999` huffman@44133 ` 1000` ```lemma bilinear_eq: ``` huffman@44133 ` 1001` ``` assumes bf: "bilinear f" ``` wenzelm@49522 ` 1002` ``` and bg: "bilinear g" ``` wenzelm@53406 ` 1003` ``` and SB: "S \ span B" ``` wenzelm@53406 ` 1004` ``` and TC: "T \ span C" ``` lp15@68058 ` 1005` ``` and "x\S" "y\T" ``` lp15@68058 ` 1006` ``` and fg: "\x y. \x \ B; y\ C\ \ f x y = g x y" ``` lp15@68058 ` 1007` ``` shows "f x y = g x y" ``` wenzelm@49663 ` 1008` ```proof - ``` huffman@44170 ` 1009` ``` let ?P = "{x. \y\ span C. f x y = g x y}" ``` huffman@44133 ` 1010` ``` from bf bg have sp: "subspace ?P" ``` huffman@53600 ` 1011` ``` unfolding bilinear_def linear_iff subspace_def bf bg ``` immler@68072 ` 1012` ``` by (auto simp add: span_zero bilinear_lzero[OF bf] bilinear_lzero[OF bg] ``` immler@68072 ` 1013` ``` span_add Ball_def ``` wenzelm@49663 ` 1014` ``` intro: bilinear_ladd[OF bf]) ``` lp15@68058 ` 1015` ``` have sfg: "\x. x \ B \ subspace {a. f x a = g x a}" ``` huffman@44133 ` 1016` ``` apply (auto simp add: subspace_def) ``` huffman@53600 ` 1017` ``` using bf bg unfolding bilinear_def linear_iff ``` immler@68072 ` 1018` ``` apply (auto simp add: span_zero bilinear_rzero[OF bf] bilinear_rzero[OF bg] ``` immler@68072 ` 1019` ``` span_add Ball_def ``` wenzelm@49663 ` 1020` ``` intro: bilinear_ladd[OF bf]) ``` wenzelm@49522 ` 1021` ``` done ``` lp15@68058 ` 1022` ``` have "\y\ span C. f x y = g x y" if "x \ span B" for x ``` lp15@68058 ` 1023` ``` apply (rule span_induct [OF that sp]) ``` lp15@68062 ` 1024` ``` using fg sfg span_induct by blast ``` wenzelm@53406 ` 1025` ``` then show ?thesis ``` lp15@68058 ` 1026` ``` using SB TC assms by auto ``` huffman@44133 ` 1027` ```qed ``` huffman@44133 ` 1028` wenzelm@49522 ` 1029` ```lemma bilinear_eq_stdbasis: ``` wenzelm@53406 ` 1030` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space \ _" ``` huffman@44133 ` 1031` ``` assumes bf: "bilinear f" ``` wenzelm@49522 ` 1032` ``` and bg: "bilinear g" ``` lp15@68058 ` 1033` ``` and fg: "\i j. i \ Basis \ j \ Basis \ f i j = g i j" ``` huffman@44133 ` 1034` ``` shows "f = g" ``` immler@68074 ` 1035` ``` using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast ``` wenzelm@49522 ` 1036` immler@69619 ` 1037` wenzelm@60420 ` 1038` ```subsection \Infinity norm\ ``` huffman@44133 ` 1039` immler@67962 ` 1040` ```definition%important "infnorm (x::'a::euclidean_space) = Sup {\x \ b\ |b. b \ Basis}" ``` huffman@44133 ` 1041` huffman@44133 ` 1042` ```lemma infnorm_set_image: ``` wenzelm@53716 ` 1043` ``` fixes x :: "'a::euclidean_space" ``` wenzelm@56444 ` 1044` ``` shows "{\x \ i\ |i. i \ Basis} = (\i. \x \ i\) ` Basis" ``` hoelzl@50526 ` 1045` ``` by blast ``` huffman@44133 ` 1046` wenzelm@53716 ` 1047` ```lemma infnorm_Max: ``` wenzelm@53716 ` 1048` ``` fixes x :: "'a::euclidean_space" ``` wenzelm@56444 ` 1049` ``` shows "infnorm x = Max ((\i. \x \ i\) ` Basis)" ``` haftmann@62343 ` 1050` ``` by (simp add: infnorm_def infnorm_set_image cSup_eq_Max) ``` hoelzl@51475 ` 1051` huffman@44133 ` 1052` ```lemma infnorm_set_lemma: ``` wenzelm@53716 ` 1053` ``` fixes x :: "'a::euclidean_space" ``` wenzelm@56444 ` 1054` ``` shows "finite {\x \ i\ |i. i \ Basis}" ``` wenzelm@56444 ` 1055` ``` and "{\x \ i\ |i. i \ Basis} \ {}" ``` huffman@44133 ` 1056` ``` unfolding infnorm_set_image ``` huffman@44133 ` 1057` ``` by auto ``` huffman@44133 ` 1058` wenzelm@53406 ` 1059` ```lemma infnorm_pos_le: ``` wenzelm@53406 ` 1060` ``` fixes x :: "'a::euclidean_space" ``` wenzelm@53406 ` 1061` ``` shows "0 \ infnorm x" ``` hoelzl@51475 ` 1062` ``` by (simp add: infnorm_Max Max_ge_iff ex_in_conv) ``` huffman@44133 ` 1063` wenzelm@53406 ` 1064` ```lemma infnorm_triangle: ``` wenzelm@53406 ` 1065` ``` fixes x :: "'a::euclidean_space" ``` wenzelm@53406 ` 1066` ``` shows "infnorm (x + y) \ infnorm x + infnorm y" ``` wenzelm@49522 ` 1067` ```proof - ``` hoelzl@51475 ` 1068` ``` have *: "\a b c d :: real. \a\ \ c \ \b\ \ d \ \a + b\ \ c + d" ``` hoelzl@51475 ` 1069` ``` by simp ``` huffman@44133 ` 1070` ``` show ?thesis ``` hoelzl@51475 ` 1071` ``` by (auto simp: infnorm_Max inner_add_left intro!: *) ``` huffman@44133 ` 1072` ```qed ``` huffman@44133 ` 1073` wenzelm@53406 ` 1074` ```lemma infnorm_eq_0: ``` wenzelm@53406 ` 1075` ``` fixes x :: "'a::euclidean_space" ``` wenzelm@53406 ` 1076` ``` shows "infnorm x = 0 \ x = 0" ``` wenzelm@49522 ` 1077` ```proof - ``` hoelzl@51475 ` 1078` ``` have "infnorm x \ 0 \ x = 0" ``` hoelzl@51475 ` 1079` ``` unfolding infnorm_Max by (simp add: euclidean_all_zero_iff) ``` hoelzl@51475 ` 1080` ``` then show ?thesis ``` hoelzl@51475 ` 1081` ``` using infnorm_pos_le[of x] by simp ``` huffman@44133 ` 1082` ```qed ``` huffman@44133 ` 1083` huffman@44133 ` 1084` ```lemma infnorm_0: "infnorm 0 = 0" ``` huffman@44133 ` 1085` ``` by (simp add: infnorm_eq_0) ``` huffman@44133 ` 1086` huffman@44133 ` 1087` ```lemma infnorm_neg: "infnorm (- x) = infnorm x" ``` lp15@68062 ` 1088` ``` unfolding infnorm_def by simp ``` huffman@44133 ` 1089` huffman@44133 ` 1090` ```lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)" ``` lp15@68062 ` 1091` ``` by (metis infnorm_neg minus_diff_eq) ``` lp15@68062 ` 1092` lp15@68062 ` 1093` ```lemma absdiff_infnorm: "\infnorm x - infnorm y\ \ infnorm (x - y)" ``` wenzelm@49522 ` 1094` ```proof - ``` lp15@68062 ` 1095` ``` have *: "\(nx::real) n ny. nx \ n + ny \ ny \ n + nx \ \nx - ny\ \ n" ``` huffman@44133 ` 1096` ``` by arith ``` lp15@68062 ` 1097` ``` show ?thesis ``` lp15@68062 ` 1098` ``` proof (rule *) ``` lp15@68062 ` 1099` ``` from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"] ``` lp15@68062 ` 1100` ``` show "infnorm x \ infnorm (x - y) + infnorm y" "infnorm y \ infnorm (x - y) + infnorm x" ``` lp15@68062 ` 1101` ``` by (simp_all add: field_simps infnorm_neg) ``` lp15@68062 ` 1102` ``` qed ``` huffman@44133 ` 1103` ```qed ``` huffman@44133 ` 1104` wenzelm@53406 ` 1105` ```lemma real_abs_infnorm: "\infnorm x\ = infnorm x" ``` huffman@44133 ` 1106` ``` using infnorm_pos_le[of x] by arith ``` huffman@44133 ` 1107` hoelzl@50526 ` 1108` ```lemma Basis_le_infnorm: ``` wenzelm@53406 ` 1109` ``` fixes x :: "'a::euclidean_space" ``` wenzelm@53406 ` 1110` ``` shows "b \ Basis \ \x \ b\ \ infnorm x" ``` hoelzl@51475 ` 1111` ``` by (simp add: infnorm_Max) ``` huffman@44133 ` 1112` wenzelm@56444 ` 1113` ```lemma infnorm_mul: "infnorm (a *\<^sub>R x) = \a\ * infnorm x" ``` hoelzl@51475 ` 1114` ``` unfolding infnorm_Max ``` hoelzl@51475 ` 1115` ```proof (safe intro!: Max_eqI) ``` hoelzl@51475 ` 1116` ``` let ?B = "(\i. \x \ i\) ` Basis" ``` lp15@68062 ` 1117` ``` { fix b :: 'a ``` wenzelm@53406 ` 1118` ``` assume "b \ Basis" ``` wenzelm@53406 ` 1119` ``` then show "\a *\<^sub>R x \ b\ \ \a\ * Max ?B" ``` wenzelm@53406 ` 1120` ``` by (simp add: abs_mult mult_left_mono) ``` wenzelm@53406 ` 1121` ``` next ``` wenzelm@53406 ` 1122` ``` from Max_in[of ?B] obtain b where "b \ Basis" "Max ?B = \x \ b\" ``` wenzelm@53406 ` 1123` ``` by (auto simp del: Max_in) ``` wenzelm@53406 ` 1124` ``` then show "\a\ * Max ((\i. \x \ i\) ` Basis) \ (\i. \a *\<^sub>R x \ i\) ` Basis" ``` wenzelm@53406 ` 1125` ``` by (intro image_eqI[where x=b]) (auto simp: abs_mult) ``` wenzelm@53406 ` 1126` ``` } ``` hoelzl@51475 ` 1127` ```qed simp ``` hoelzl@51475 ` 1128` wenzelm@53406 ` 1129` ```lemma infnorm_mul_lemma: "infnorm (a *\<^sub>R x) \ \a\ * infnorm x" ``` hoelzl@51475 ` 1130` ``` unfolding infnorm_mul .. ``` huffman@44133 ` 1131` huffman@44133 ` 1132` ```lemma infnorm_pos_lt: "infnorm x > 0 \ x \ 0" ``` huffman@44133 ` 1133` ``` using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith ``` huffman@44133 ` 1134` wenzelm@60420 ` 1135` ```text \Prove that it differs only up to a bound from Euclidean norm.\ ``` huffman@44133 ` 1136` huffman@44133 ` 1137` ```lemma infnorm_le_norm: "infnorm x \ norm x" ``` hoelzl@51475 ` 1138` ``` by (simp add: Basis_le_norm infnorm_Max) ``` hoelzl@50526 ` 1139` wenzelm@53716 ` 1140` ```lemma norm_le_infnorm: ``` wenzelm@53716 ` 1141` ``` fixes x :: "'a::euclidean_space" ``` wenzelm@53716 ` 1142` ``` shows "norm x \ sqrt DIM('a) * infnorm x" ``` lp15@68062 ` 1143` ``` unfolding norm_eq_sqrt_inner id_def ``` lp15@68062 ` 1144` ```proof (rule real_le_lsqrt[OF inner_ge_zero]) ``` lp15@68062 ` 1145` ``` show "sqrt DIM('a) * infnorm x \ 0" ``` huffman@44133 ` 1146` ``` by (simp add: zero_le_mult_iff infnorm_pos_le) ``` lp15@68062 ` 1147` ``` have "x \ x \ (\b\Basis. x \ b * (x \ b))" ``` lp15@68062 ` 1148` ``` by (metis euclidean_inner order_refl) ``` lp15@68062 ` 1149` ``` also have "... \ DIM('a) * \infnorm x\\<^sup>2" ``` lp15@68062 ` 1150` ``` by (rule sum_bounded_above) (metis Basis_le_infnorm abs_le_square_iff power2_eq_square real_abs_infnorm) ``` lp15@68062 ` 1151` ``` also have "... \ (sqrt DIM('a) * infnorm x)\<^sup>2" ``` lp15@68062 ` 1152` ``` by (simp add: power_mult_distrib) ``` lp15@68062 ` 1153` ``` finally show "x \ x \ (sqrt DIM('a) * infnorm x)\<^sup>2" . ``` huffman@44133 ` 1154` ```qed ``` huffman@44133 ` 1155` huffman@44646 ` 1156` ```lemma tendsto_infnorm [tendsto_intros]: ``` wenzelm@61973 ` 1157` ``` assumes "(f \ a) F" ``` wenzelm@61973 ` 1158` ``` shows "((\x. infnorm (f x)) \ infnorm a) F" ``` huffman@44646 ` 1159` ```proof (rule tendsto_compose [OF LIM_I assms]) ``` wenzelm@53406 ` 1160` ``` fix r :: real ``` wenzelm@53406 ` 1161` ``` assume "r > 0" ``` wenzelm@49522 ` 1162` ``` then show "\s>0. \x. x \ a \ norm (x - a) < s \ norm (infnorm x - infnorm a) < r" ``` lp15@68062 ` 1163` ``` by (metis real_norm_def le_less_trans absdiff_infnorm infnorm_le_norm) ``` huffman@44646 ` 1164` ```qed ``` huffman@44646 ` 1165` wenzelm@60420 ` 1166` ```text \Equality in Cauchy-Schwarz and triangle inequalities.\ ``` huffman@44133 ` 1167` wenzelm@53406 ` 1168` ```lemma norm_cauchy_schwarz_eq: "x \ y = norm x * norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" ``` wenzelm@53406 ` 1169` ``` (is "?lhs \ ?rhs") ``` lp15@68062 ` 1170` ```proof (cases "x=0") ``` lp15@68062 ` 1171` ``` case True ``` lp15@68062 ` 1172` ``` then show ?thesis ``` lp15@68062 ` 1173` ``` by auto ``` lp15@68062 ` 1174` ```next ``` lp15@68062 ` 1175` ``` case False ``` lp15@68062 ` 1176` ``` from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"] ``` lp15@68062 ` 1177` ``` have "?rhs \ ``` wenzelm@49522 ` 1178` ``` (norm y * (norm y * norm x * norm x - norm x * (x \ y)) - ``` wenzelm@49522 ` 1179` ``` norm x * (norm y * (y \ x) - norm x * norm y * norm y) = 0)" ``` lp15@68062 ` 1180` ``` using False unfolding inner_simps ``` lp15@68062 ` 1181` ``` by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) ``` lp15@68062 ` 1182` ``` also have "\ \ (2 * norm x * norm y * (norm x * norm y - x \ y) = 0)" ``` lp15@68062 ` 1183` ``` using False by (simp add: field_simps inner_commute) ``` lp15@68062 ` 1184` ``` also have "\ \ ?lhs" ``` lp15@68062 ` 1185` ``` using False by auto ``` lp15@68062 ` 1186` ``` finally show ?thesis by metis ``` huffman@44133 ` 1187` ```qed ``` huffman@44133 ` 1188` huffman@44133 ` 1189` ```lemma norm_cauchy_schwarz_abs_eq: ``` wenzelm@56444 ` 1190` ``` "\x \ y\ = norm x * norm y \ ``` wenzelm@53716 ` 1191` ``` norm x *\<^sub>R y = norm y *\<^sub>R x \ norm x *\<^sub>R y = - norm y *\<^sub>R x" ``` wenzelm@53406 ` 1192` ``` (is "?lhs \ ?rhs") ``` wenzelm@49522 ` 1193` ```proof - ``` wenzelm@56444 ` 1194` ``` have th: "\(x::real) a. a \ 0 \ \x\ = a \ x = a \ x = - a" ``` wenzelm@53406 ` 1195` ``` by arith ``` huffman@44133 ` 1196` ``` have "?rhs \ norm x *\<^sub>R y = norm y *\<^sub>R x \ norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)" ``` huffman@44133 ` 1197` ``` by simp ``` lp15@68062 ` 1198` ``` also have "\ \ (x \ y = norm x * norm y \ (- x) \ y = norm x * norm y)" ``` huffman@44133 ` 1199` ``` unfolding norm_cauchy_schwarz_eq[symmetric] ``` huffman@44133 ` 1200` ``` unfolding norm_minus_cancel norm_scaleR .. ``` huffman@44133 ` 1201` ``` also have "\ \ ?lhs" ``` wenzelm@53406 ` 1202` ``` unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps ``` wenzelm@53406 ` 1203` ``` by auto ``` huffman@44133 ` 1204` ``` finally show ?thesis .. ``` huffman@44133 ` 1205` ```qed ``` huffman@44133 ` 1206` huffman@44133 ` 1207` ```lemma norm_triangle_eq: ``` huffman@44133 ` 1208` ``` fixes x y :: "'a::real_inner" ``` wenzelm@53406 ` 1209` ``` shows "norm (x + y) = norm x + norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" ``` lp15@68062 ` 1210` ```proof (cases "x = 0 \ y = 0") ``` lp15@68062 ` 1211` ``` case True ``` lp15@68062 ` 1212` ``` then show ?thesis ``` lp15@68062 ` 1213` ``` by force ``` lp15@68062 ` 1214` ```next ``` lp15@68062 ` 1215` ``` case False ``` lp15@68062 ` 1216` ``` then have n: "norm x > 0" "norm y > 0" ``` lp15@68062 ` 1217` ``` by auto ``` lp15@68062 ` 1218` ``` have "norm (x + y) = norm x + norm y \ (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2" ``` lp15@68062 ` 1219` ``` by simp ``` lp15@68062 ` 1220` ``` also have "\ \ norm x *\<^sub>R y = norm y *\<^sub>R x" ``` lp15@68062 ` 1221` ``` unfolding norm_cauchy_schwarz_eq[symmetric] ``` lp15@68062 ` 1222` ``` unfolding power2_norm_eq_inner inner_simps ``` lp15@68062 ` 1223` ``` by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) ``` lp15@68062 ` 1224` ``` finally show ?thesis . ``` huffman@44133 ` 1225` ```qed ``` huffman@44133 ` 1226` wenzelm@49522 ` 1227` wenzelm@60420 ` 1228` ```subsection \Collinearity\ ``` huffman@44133 ` 1229` immler@67962 ` 1230` ```definition%important collinear :: "'a::real_vector set \ bool" ``` wenzelm@49522 ` 1231` ``` where "collinear S \ (\u. \x \ S. \ y \ S. \c. x - y = c *\<^sub>R u)" ``` huffman@44133 ` 1232` lp15@66287 ` 1233` ```lemma collinear_alt: ``` lp15@66287 ` 1234` ``` "collinear S \ (\u v. \x \ S. \c. x = u + c *\<^sub>R v)" (is "?lhs = ?rhs") ``` lp15@66287 ` 1235` ```proof ``` lp15@66287 ` 1236` ``` assume ?lhs ``` lp15@66287 ` 1237` ``` then show ?rhs ``` lp15@66287 ` 1238` ``` unfolding collinear_def by (metis Groups.add_ac(2) diff_add_cancel) ``` lp15@66287 ` 1239` ```next ``` lp15@66287 ` 1240` ``` assume ?rhs ``` lp15@66287 ` 1241` ``` then obtain u v where *: "\x. x \ S \ \c. x = u + c *\<^sub>R v" ``` lp15@66287 ` 1242` ``` by (auto simp: ) ``` lp15@66287 ` 1243` ``` have "\c. x - y = c *\<^sub>R v" if "x \ S" "y \ S" for x y ``` lp15@66287 ` 1244` ``` by (metis *[OF \x \ S\] *[OF \y \ S\] scaleR_left.diff add_diff_cancel_left) ``` lp15@66287 ` 1245` ``` then show ?lhs ``` lp15@66287 ` 1246` ``` using collinear_def by blast ``` lp15@66287 ` 1247` ```qed ``` lp15@66287 ` 1248` lp15@66287 ` 1249` ```lemma collinear: ``` lp15@66287 ` 1250` ``` fixes S :: "'a::{perfect_space,real_vector} set" ``` lp15@66287 ` 1251` ``` shows "collinear S \ (\u. u \ 0 \ (\x \ S. \ y \ S. \c. x - y = c *\<^sub>R u))" ``` lp15@66287 ` 1252` ```proof - ``` lp15@66287 ` 1253` ``` have "\v. v \ 0 \ (\x\S. \y\S. \c. x - y = c *\<^sub>R v)" ``` lp15@66287 ` 1254` ``` if "\x\S. \y\S. \c. x - y = c *\<^sub>R u" "u=0" for u ``` lp15@66287 ` 1255` ``` proof - ``` lp15@66287 ` 1256` ``` have "\x\S. \y\S. x = y" ``` lp15@66287 ` 1257` ``` using that by auto ``` lp15@66287 ` 1258` ``` moreover ``` lp15@66287 ` 1259` ``` obtain v::'a where "v \ 0" ``` lp15@66287 ` 1260` ``` using UNIV_not_singleton [of 0] by auto ``` lp15@66287 ` 1261` ``` ultimately have "\x\S. \y\S. \c. x - y = c *\<^sub>R v" ``` lp15@66287 ` 1262` ``` by auto ``` lp15@66287 ` 1263` ``` then show ?thesis ``` lp15@66287 ` 1264` ``` using \v \ 0\ by blast ``` lp15@66287 ` 1265` ``` qed ``` lp15@66287 ` 1266` ``` then show ?thesis ``` lp15@66287 ` 1267` ``` apply (clarsimp simp: collinear_def) ``` immler@68072 ` 1268` ``` by (metis scaleR_zero_right vector_fraction_eq_iff) ``` lp15@66287 ` 1269` ```qed ``` lp15@66287 ` 1270` lp15@63881 ` 1271` ```lemma collinear_subset: "\collinear T; S \ T\ \ collinear S" ``` lp15@63881 ` 1272` ``` by (meson collinear_def subsetCE) ``` lp15@63881 ` 1273` paulson@60762 ` 1274` ```lemma collinear_empty [iff]: "collinear {}" ``` wenzelm@53406 ` 1275` ``` by (simp add: collinear_def) ``` huffman@44133 ` 1276` paulson@60762 ` 1277` ```lemma collinear_sing [iff]: "collinear {x}" ``` huffman@44133 ` 1278` ``` by (simp add: collinear_def) ``` huffman@44133 ` 1279` paulson@60762 ` 1280` ```lemma collinear_2 [iff]: "collinear {x, y}" ``` huffman@44133 ` 1281` ``` apply (simp add: collinear_def) ``` huffman@44133 ` 1282` ``` apply (rule exI[where x="x - y"]) ``` lp15@68062 ` 1283` ``` by (metis minus_diff_eq scaleR_left.minus scaleR_one) ``` huffman@44133 ` 1284` wenzelm@56444 ` 1285` ```lemma collinear_lemma: "collinear {0, x, y} \ x = 0 \ y = 0 \ (\c. y = c *\<^sub>R x)" ``` wenzelm@53406 ` 1286` ``` (is "?lhs \ ?rhs") ``` lp15@68062 ` 1287` ```proof (cases "x = 0 \ y = 0") ``` lp15@68062 ` 1288` ``` case True ``` lp15@68062 ` 1289` ``` then show ?thesis ``` lp15@68062 ` 1290` ``` by (auto simp: insert_commute) ``` lp15@68062 ` 1291` ```next ``` lp15@68062 ` 1292` ``` case False ``` lp15@68062 ` 1293` ``` show ?thesis ``` lp15@68062 ` 1294` ``` proof ``` lp15@68062 ` 1295` ``` assume h: "?lhs" ``` lp15@68062 ` 1296` ``` then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *\<^sub>R u" ``` lp15@68062 ` 1297` ``` unfolding collinear_def by blast ``` lp15@68062 ` 1298` ``` from u[rule_format, of x 0] u[rule_format, of y 0] ``` lp15@68062 ` 1299` ``` obtain cx and cy where ``` lp15@68062 ` 1300` ``` cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u" ``` lp15@68062 ` 1301` ``` by auto ``` lp15@68062 ` 1302` ``` from cx cy False have cx0: "cx \ 0" and cy0: "cy \ 0" by auto ``` lp15@68062 ` 1303` ``` let ?d = "cy / cx" ``` lp15@68062 ` 1304` ``` from cx cy cx0 have "y = ?d *\<^sub>R x" ``` lp15@68062 ` 1305` ``` by simp ``` lp15@68062 ` 1306` ``` then show ?rhs using False by blast ``` lp15@68062 ` 1307` ``` next ``` lp15@68062 ` 1308` ``` assume h: "?rhs" ``` lp15@68062 ` 1309` ``` then obtain c where c: "y = c *\<^sub>R x" ``` lp15@68062 ` 1310` ``` using False by blast ``` lp15@68062 ` 1311` ``` show ?lhs ``` lp15@68062 ` 1312` ``` unfolding collinear_def c ``` lp15@68062 ` 1313` ``` apply (rule exI[where x=x]) ``` lp15@68062 ` 1314` ``` apply auto ``` lp15@68062 ` 1315` ``` apply (rule exI[where x="- 1"], simp) ``` lp15@68062 ` 1316` ``` apply (rule exI[where x= "-c"], simp) ``` huffman@44133 ` 1317` ``` apply (rule exI[where x=1], simp) ``` lp15@68062 ` 1318` ``` apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib) ``` lp15@68062 ` 1319` ``` apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib) ``` lp15@68062 ` 1320` ``` done ``` lp15@68062 ` 1321` ``` qed ``` huffman@44133 ` 1322` ```qed ``` huffman@44133 ` 1323` wenzelm@56444 ` 1324` ```lemma norm_cauchy_schwarz_equal: "\x \ y\ = norm x * norm y \ collinear {0, x, y}" ``` lp15@68062 ` 1325` ```proof (cases "x=0") ``` lp15@68062 ` 1326` ``` case True ``` lp15@68062 ` 1327` ``` then show ?thesis ``` lp15@68062 ` 1328` ``` by (auto simp: insert_commute) ``` lp15@68062 ` 1329` ```next ``` lp15@68062 ` 1330` ``` case False ``` lp15@68062 ` 1331` ``` then have nnz: "norm x \ 0" ``` lp15@68062 ` 1332` ``` by auto ``` lp15@68062 ` 1333` ``` show ?thesis ``` lp15@68062 ` 1334` ``` proof ``` lp15@68062 ` 1335` ``` assume "\x \ y\ = norm x * norm y" ``` lp15@68062 ` 1336` ``` then show "collinear {0, x, y}" ``` lp15@68062 ` 1337` ``` unfolding norm_cauchy_schwarz_abs_eq collinear_lemma ``` lp15@68062 ` 1338` ``` by (meson eq_vector_fraction_iff nnz) ``` lp15@68062 ` 1339` ``` next ``` lp15@68062 ` 1340` ``` assume "collinear {0, x, y}" ``` lp15@68062 ` 1341` ``` with False show "\x \ y\ = norm x * norm y" ``` lp15@68062 ` 1342` ``` unfolding norm_cauchy_schwarz_abs_eq collinear_lemma by (auto simp: abs_if) ``` lp15@68062 ` 1343` ``` qed ``` lp15@68062 ` 1344` ```qed ``` wenzelm@49522 ` 1345` immler@69675 ` 1346` immler@69675 ` 1347` ```subsection\Properties of special hyperplanes\ ``` immler@69675 ` 1348` immler@69675 ` 1349` ```lemma subspace_hyperplane: "subspace {x. a \ x = 0}" ``` immler@69675 ` 1350` ``` by (simp add: subspace_def inner_right_distrib) ``` immler@69675 ` 1351` immler@69675 ` 1352` ```lemma subspace_hyperplane2: "subspace {x. x \ a = 0}" ``` immler@69675 ` 1353` ``` by (simp add: inner_commute inner_right_distrib subspace_def) ``` immler@69675 ` 1354` immler@69675 ` 1355` ```lemma special_hyperplane_span: ``` immler@69675 ` 1356` ``` fixes S :: "'n::euclidean_space set" ``` immler@69675 ` 1357` ``` assumes "k \ Basis" ``` immler@69675 ` 1358` ``` shows "{x. k \ x = 0} = span (Basis - {k})" ``` immler@69675 ` 1359` ```proof - ``` immler@69675 ` 1360` ``` have *: "x \ span (Basis - {k})" if "k \ x = 0" for x ``` immler@69675 ` 1361` ``` proof - ``` immler@69675 ` 1362` ``` have "x = (\b\Basis. (x \ b) *\<^sub>R b)" ``` immler@69675 ` 1363` ``` by (simp add: euclidean_representation) ``` immler@69675 ` 1364` ``` also have "... = (\b \ Basis - {k}. (x \ b) *\<^sub>R b)" ``` immler@69675 ` 1365` ``` by (auto simp: sum.remove [of _ k] inner_commute assms that) ``` immler@69675 ` 1366` ``` finally have "x = (\b\Basis - {k}. (x \ b) *\<^sub>R b)" . ``` immler@69675 ` 1367` ``` then show ?thesis ``` immler@69675 ` 1368` ``` by (simp add: span_finite) ``` immler@69675 ` 1369` ``` qed ``` immler@69675 ` 1370` ``` show ?thesis ``` immler@69675 ` 1371` ``` apply (rule span_subspace [symmetric]) ``` immler@69675 ` 1372` ``` using assms ``` immler@69675 ` 1373` ``` apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane) ``` immler@69675 ` 1374` ``` done ``` immler@69675 ` 1375` ```qed ``` immler@69675 ` 1376` immler@69675 ` 1377` ```lemma dim_special_hyperplane: ``` immler@69675 ` 1378` ``` fixes k :: "'n::euclidean_space" ``` immler@69675 ` 1379` ``` shows "k \ Basis \ dim {x. k \ x = 0} = DIM('n) - 1" ``` immler@69675 ` 1380` ```apply (simp add: special_hyperplane_span) ``` immler@69675 ` 1381` ```apply (rule dim_unique [OF subset_refl]) ``` immler@69675 ` 1382` ```apply (auto simp: independent_substdbasis) ``` immler@69675 ` 1383` ```apply (metis member_remove remove_def span_base) ``` immler@69675 ` 1384` ```done ``` immler@69675 ` 1385` immler@69675 ` 1386` ```proposition dim_hyperplane: ``` immler@69675 ` 1387` ``` fixes a :: "'a::euclidean_space" ``` immler@69675 ` 1388` ``` assumes "a \ 0" ``` immler@69675 ` 1389` ``` shows "dim {x. a \ x = 0} = DIM('a) - 1" ``` immler@69675 ` 1390` ```proof - ``` immler@69675 ` 1391` ``` have span0: "span {x. a \ x = 0} = {x. a \ x = 0}" ``` immler@69675 ` 1392` ``` by (rule span_unique) (auto simp: subspace_hyperplane) ``` immler@69675 ` 1393` ``` then obtain B where "independent B" ``` immler@69675 ` 1394` ``` and Bsub: "B \ {x. a \ x = 0}" ``` immler@69675 ` 1395` ``` and subspB: "{x. a \ x = 0} \ span B" ``` immler@69675 ` 1396` ``` and card0: "(card B = dim {x. a \ x = 0})" ``` immler@69675 ` 1397` ``` and ortho: "pairwise orthogonal B" ``` immler@69675 ` 1398` ``` using orthogonal_basis_exists by metis ``` immler@69675 ` 1399` ``` with assms have "a \ span B" ``` immler@69675 ` 1400` ``` by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0) ``` immler@69675 ` 1401` ``` then have ind: "independent (insert a B)" ``` immler@69675 ` 1402` ``` by (simp add: \independent B\ independent_insert) ``` immler@69675 ` 1403` ``` have "finite B" ``` immler@69675 ` 1404` ``` using \independent B\ independent_bound by blast ``` immler@69675 ` 1405` ``` have "UNIV \ span (insert a B)" ``` immler@69675 ` 1406` ``` proof fix y::'a ``` immler@69675 ` 1407` ``` obtain r z where z: "y = r *\<^sub>R a + z" "a \ z = 0" ``` immler@69675 ` 1408` ``` apply (rule_tac r="(a \ y) / (a \ a)" and z = "y - ((a \ y) / (a \ a)) *\<^sub>R a" in that) ``` immler@69675 ` 1409` ``` using assms ``` immler@69675 ` 1410` ``` by (auto simp: algebra_simps) ``` immler@69675 ` 1411` ``` show "y \ span (insert a B)" ``` immler@69675 ` 1412` ``` by (metis (mono_tags, lifting) z Bsub span_eq_iff ``` immler@69675 ` 1413` ``` add_diff_cancel_left' mem_Collect_eq span0 span_breakdown_eq span_subspace subspB) ``` immler@69675 ` 1414` ``` qed ``` immler@69675 ` 1415` ``` then have dima: "DIM('a) = dim(insert a B)" ``` immler@69675 ` 1416` ``` by (metis independent_Basis span_Basis dim_eq_card top.extremum_uniqueI) ``` immler@69675 ` 1417` ``` then show ?thesis ``` immler@69675 ` 1418` ``` by (metis (mono_tags, lifting) Bsub Diff_insert_absorb \a \ span B\ ind card0 ``` immler@69675 ` 1419` ``` card_Diff_singleton dim_span indep_card_eq_dim_span insertI1 subsetCE ``` immler@69675 ` 1420` ``` subspB) ``` immler@69675 ` 1421` ```qed ``` immler@69675 ` 1422` immler@69675 ` 1423` ```lemma lowdim_eq_hyperplane: ``` immler@69675 ` 1424` ``` fixes S :: "'a::euclidean_space set" ``` immler@69675 ` 1425` ``` assumes "dim S = DIM('a) - 1" ``` immler@69675 ` 1426` ``` obtains a where "a \ 0" and "span S = {x. a \ x = 0}" ``` immler@69675 ` 1427` ```proof - ``` immler@69675 ` 1428` ``` have dimS: "dim S < DIM('a)" ``` immler@69675 ` 1429` ``` by (simp add: assms) ``` immler@69675 ` 1430` ``` then obtain b where b: "b \ 0" "span S \ {a. b \ a = 0}" ``` immler@69675 ` 1431` ``` using lowdim_subset_hyperplane [of S] by fastforce ``` immler@69675 ` 1432` ``` show ?thesis ``` immler@69675 ` 1433` ``` apply (rule that[OF b(1)]) ``` immler@69675 ` 1434` ``` apply (rule subspace_dim_equal) ``` immler@69675 ` 1435` ``` by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane ``` immler@69675 ` 1436` ``` subspace_span) ``` immler@69675 ` 1437` ```qed ``` immler@69675 ` 1438` immler@69675 ` 1439` ```lemma dim_eq_hyperplane: ``` immler@69675 ` 1440` ``` fixes S :: "'n::euclidean_space set" ``` immler@69675 ` 1441` ``` shows "dim S = DIM('n) - 1 \ (\a. a \ 0 \ span S = {x. a \ x = 0})" ``` immler@69675 ` 1442` ```by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane) ``` immler@69675 ` 1443` immler@69675 ` 1444` immler@69675 ` 1445` ```subsection\ Orthogonal bases, Gram-Schmidt process, and related theorems\ ``` immler@69675 ` 1446` immler@69675 ` 1447` ```lemma pairwise_orthogonal_independent: ``` immler@69675 ` 1448` ``` assumes "pairwise orthogonal S" and "0 \ S" ``` immler@69675 ` 1449` ``` shows "independent S" ``` immler@69675 ` 1450` ```proof - ``` immler@69675 ` 1451` ``` have 0: "\x y. \x \ y; x \ S; y \ S\ \ x \ y = 0" ``` immler@69675 ` 1452` ``` using assms by (simp add: pairwise_def orthogonal_def) ``` immler@69675 ` 1453` ``` have "False" if "a \ S" and a: "a \ span (S - {a})" for a ``` immler@69675 ` 1454` ``` proof - ``` immler@69675 ` 1455` ``` obtain T U where "T \ S - {a}" "a = (\v\T. U v *\<^sub>R v)" ``` immler@69675 ` 1456` ``` using a by (force simp: span_explicit) ``` immler@69675 ` 1457` ``` then have "a \ a = a \ (\v\T. U v *\<^sub>R v)" ``` immler@69675 ` 1458` ``` by simp ``` immler@69675 ` 1459` ``` also have "... = 0" ``` immler@69675 ` 1460` ``` apply (simp add: inner_sum_right) ``` immler@69675 ` 1461` ``` apply (rule comm_monoid_add_class.sum.neutral) ``` immler@69675 ` 1462` ``` by (metis "0" DiffE \T \ S - {a}\ mult_not_zero singletonI subsetCE \a \ S\) ``` immler@69675 ` 1463` ``` finally show ?thesis ``` immler@69675 ` 1464` ``` using \0 \ S\ \a \ S\ by auto ``` immler@69675 ` 1465` ``` qed ``` immler@69675 ` 1466` ``` then show ?thesis ``` immler@69675 ` 1467` ``` by (force simp: dependent_def) ``` immler@69675 ` 1468` ```qed ``` immler@69675 ` 1469` immler@69675 ` 1470` ```lemma pairwise_orthogonal_imp_finite: ``` immler@69675 ` 1471` ``` fixes S :: "'a::euclidean_space set" ``` immler@69675 ` 1472` ``` assumes "pairwise orthogonal S" ``` immler@69675 ` 1473` ``` shows "finite S" ``` immler@69675 ` 1474` ```proof - ``` immler@69675 ` 1475` ``` have "independent (S - {0})" ``` immler@69675 ` 1476` ``` apply (rule pairwise_orthogonal_independent) ``` immler@69675 ` 1477` ``` apply (metis Diff_iff assms pairwise_def) ``` immler@69675 ` 1478` ``` by blast ``` immler@69675 ` 1479` ``` then show ?thesis ``` immler@69675 ` 1480` ``` by (meson independent_imp_finite infinite_remove) ``` immler@69675 ` 1481` ```qed ``` immler@69675 ` 1482` immler@69675 ` 1483` ```lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}" ``` immler@69675 ` 1484` ``` by (simp add: subspace_def orthogonal_clauses) ``` immler@69675 ` 1485` immler@69675 ` 1486` ```lemma subspace_orthogonal_to_vectors: "subspace {y. \x \ S. orthogonal x y}" ``` immler@69675 ` 1487` ``` by (simp add: subspace_def orthogonal_clauses) ``` immler@69675 ` 1488` immler@69675 ` 1489` ```lemma orthogonal_to_span: ``` immler@69675 ` 1490` ``` assumes a: "a \ span S" and x: "\y. y \ S \ orthogonal x y" ``` immler@69675 ` 1491` ``` shows "orthogonal x a" ``` immler@69675 ` 1492` ``` by (metis a orthogonal_clauses(1,2,4) ``` immler@69675 ` 1493` ``` span_induct_alt x) ``` immler@69675 ` 1494` immler@69675 ` 1495` ```proposition Gram_Schmidt_step: ``` immler@69675 ` 1496` ``` fixes S :: "'a::euclidean_space set" ``` immler@69675 ` 1497` ``` assumes S: "pairwise orthogonal S" and x: "x \ span S" ``` immler@69675 ` 1498` ``` shows "orthogonal x (a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b))" ``` immler@69675 ` 1499` ```proof - ``` immler@69675 ` 1500` ``` have "finite S" ``` immler@69675 ` 1501` ``` by (simp add: S pairwise_orthogonal_imp_finite) ``` immler@69675 ` 1502` ``` have "orthogonal (a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b)) x" ``` immler@69675 ` 1503` ``` if "x \ S" for x ``` immler@69675 ` 1504` ``` proof - ``` immler@69675 ` 1505` ``` have "a \ x = (\y\S. if y = x then y \ a else 0)" ``` immler@69675 ` 1506` ``` by (simp add: \finite S\ inner_commute sum.delta that) ``` immler@69675 ` 1507` ``` also have "... = (\b\S. b \ a * (b \ x) / (b \ b))" ``` immler@69675 ` 1508` ``` apply (rule sum.cong [OF refl], simp) ``` immler@69675 ` 1509` ``` by (meson S orthogonal_def pairwise_def that) ``` immler@69675 ` 1510` ``` finally show ?thesis ``` immler@69675 ` 1511` ``` by (simp add: orthogonal_def algebra_simps inner_sum_left) ``` immler@69675 ` 1512` ``` qed ``` immler@69675 ` 1513` ``` then show ?thesis ``` immler@69675 ` 1514` ``` using orthogonal_to_span orthogonal_commute x by blast ``` immler@69675 ` 1515` ```qed ``` immler@69675 ` 1516` immler@69675 ` 1517` immler@69675 ` 1518` ```lemma orthogonal_extension_aux: ``` immler@69675 ` 1519` ``` fixes S :: "'a::euclidean_space set" ``` immler@69675 ` 1520` ``` assumes "finite T" "finite S" "pairwise orthogonal S" ``` immler@69675 ` 1521` ``` shows "\U. pairwise orthogonal (S \ U) \ span (S \ U) = span (S \ T)" ``` immler@69675 ` 1522` ```using assms ``` immler@69675 ` 1523` ```proof (induction arbitrary: S) ``` immler@69675 ` 1524` ``` case empty then show ?case ``` immler@69675 ` 1525` ``` by simp (metis sup_bot_right) ``` immler@69675 ` 1526` ```next ``` immler@69675 ` 1527` ``` case (insert a T) ``` immler@69675 ` 1528` ``` have 0: "\x y. \x \ y; x \ S; y \ S\ \ x \ y = 0" ``` immler@69675 ` 1529` ``` using insert by (simp add: pairwise_def orthogonal_def) ``` immler@69675 ` 1530` ``` define a' where "a' = a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b)" ``` immler@69675 ` 1531` ``` obtain U where orthU: "pairwise orthogonal (S \ insert a' U)" ``` immler@69675 ` 1532` ``` and spanU: "span (insert a' S \ U) = span (insert a' S \ T)" ``` immler@69675 ` 1533` ``` by (rule exE [OF insert.IH [of "insert a' S"]]) ``` immler@69675 ` 1534` ``` (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute ``` immler@69675 ` 1535` ``` pairwise_orthogonal_insert span_clauses) ``` immler@69675 ` 1536` ``` have orthS: "\x. x \ S \ a' \ x = 0" ``` immler@69675 ` 1537` ``` apply (simp add: a'_def) ``` immler@69675 ` 1538` ``` using Gram_Schmidt_step [OF \pairwise orthogonal S\] ``` immler@69675 ` 1539` ``` apply (force simp: orthogonal_def inner_commute span_superset [THEN subsetD]) ``` immler@69675 ` 1540` ``` done ``` immler@69675 ` 1541` ``` have "span (S \ insert a' U) = span (insert a' (S \ T))" ``` immler@69675 ` 1542` ``` using spanU by simp ``` immler@69675 ` 1543` ``` also have "... = span (insert a (S \ T))" ``` immler@69675 ` 1544` ``` apply (rule eq_span_insert_eq) ``` immler@69675 ` 1545` ``` apply (simp add: a'_def span_neg span_sum span_base span_mul) ``` immler@69675 ` 1546` ``` done ``` immler@69675 ` 1547` ``` also have "... = span (S \ insert a T)" ``` immler@69675 ` 1548` ``` by simp ``` immler@69675 ` 1549` ``` finally show ?case ``` immler@69675 ` 1550` ``` by (rule_tac x="insert a' U" in exI) (use orthU in auto) ``` immler@69675 ` 1551` ```qed ``` immler@69675 ` 1552` immler@69675 ` 1553` immler@69675 ` 1554` ```proposition orthogonal_extension: ``` immler@69675 ` 1555` ``` fixes S :: "'a::euclidean_space set" ``` immler@69675 ` 1556` ``` assumes S: "pairwise orthogonal S" ``` immler@69675 ` 1557` ``` obtains U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)" ``` immler@69675 ` 1558` ```proof - ``` immler@69675 ` 1559` ``` obtain B where "finite B" "span B = span T" ``` immler@69675 ` 1560` ``` using basis_subspace_exists [of "span T"] subspace_span by metis ``` immler@69675 ` 1561` ``` with orthogonal_extension_aux [of B S] ``` immler@69675 ` 1562` ``` obtain U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ B)" ``` immler@69675 ` 1563` ``` using assms pairwise_orthogonal_imp_finite by auto ``` immler@69675 ` 1564` ``` with \span B = span T\ show ?thesis ``` immler@69675 ` 1565` ``` by (rule_tac U=U in that) (auto simp: span_Un) ``` immler@69675 ` 1566` ```qed ``` immler@69675 ` 1567` immler@69675 ` 1568` ```corollary%unimportant orthogonal_extension_strong: ``` immler@69675 ` 1569` ``` fixes S :: "'a::euclidean_space set" ``` immler@69675 ` 1570` ``` assumes S: "pairwise orthogonal S" ``` immler@69675 ` 1571` ``` obtains U where "U \ (insert 0 S) = {}" "pairwise orthogonal (S \ U)" ``` immler@69675 ` 1572` ``` "span (S \ U) = span (S \ T)" ``` immler@69675 ` 1573` ```proof - ``` immler@69675 ` 1574` ``` obtain U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)" ``` immler@69675 ` 1575` ``` using orthogonal_extension assms by blast ``` immler@69675 ` 1576` ``` then show ?thesis ``` immler@69675 ` 1577` ``` apply (rule_tac U = "U - (insert 0 S)" in that) ``` immler@69675 ` 1578` ``` apply blast ``` immler@69675 ` 1579` ``` apply (force simp: pairwise_def) ``` immler@69675 ` 1580` ``` apply (metis Un_Diff_cancel Un_insert_left span_redundant span_zero) ``` immler@69675 ` 1581` ``` done ``` immler@69675 ` 1582` ```qed ``` immler@69675 ` 1583` immler@69675 ` 1584` ```subsection\Decomposing a vector into parts in orthogonal subspaces\ ``` immler@69675 ` 1585` immler@69675 ` 1586` ```text\existence of orthonormal basis for a subspace.\ ``` immler@69675 ` 1587` immler@69675 ` 1588` ```lemma orthogonal_spanningset_subspace: ``` immler@69675 ` 1589` ``` fixes S :: "'a :: euclidean_space set" ``` immler@69675 ` 1590` ``` assumes "subspace S" ``` immler@69675 ` 1591` ``` obtains B where "B \ S" "pairwise orthogonal B" "span B = S" ``` immler@69675 ` 1592` ```proof - ``` immler@69675 ` 1593` ``` obtain B where "B \ S" "independent B" "S \ span B" "card B = dim S" ``` immler@69675 ` 1594` ``` using basis_exists by blast ``` immler@69675 ` 1595` ``` with orthogonal_extension [of "{}" B] ``` immler@69675 ` 1596` ``` show ?thesis ``` immler@69675 ` 1597` ``` by (metis Un_empty_left assms pairwise_empty span_superset span_subspace that) ``` immler@69675 ` 1598` ```qed ``` immler@69675 ` 1599` immler@69675 ` 1600` ```lemma orthogonal_basis_subspace: ``` immler@69675 ` 1601` ``` fixes S :: "'a :: euclidean_space set" ``` immler@69675 ` 1602` ``` assumes "subspace S" ``` immler@69675 ` 1603` ``` obtains B where "0 \ B" "B \ S" "pairwise orthogonal B" "independent B" ``` immler@69675 ` 1604` ``` "card B = dim S" "span B = S" ``` immler@69675 ` 1605` ```proof - ``` immler@69675 ` 1606` ``` obtain B where "B \ S" "pairwise orthogonal B" "span B = S" ``` immler@69675 ` 1607` ``` using assms orthogonal_spanningset_subspace by blast ``` immler@69675 ` 1608` ``` then show ?thesis ``` immler@69675 ` 1609` ``` apply (rule_tac B = "B - {0}" in that) ``` immler@69675 ` 1610` ``` apply (auto simp: indep_card_eq_dim_span pairwise_subset pairwise_orthogonal_independent elim: pairwise_subset) ``` immler@69675 ` 1611` ``` done ``` immler@69675 ` 1612` ```qed ``` immler@69675 ` 1613` immler@69675 ` 1614` ```proposition orthonormal_basis_subspace: ``` immler@69675 ` 1615` ``` fixes S :: "'a :: euclidean_space set" ``` immler@69675 ` 1616` ``` assumes "subspace S" ``` immler@69675 ` 1617` ``` obtains B where "B \ S" "pairwise orthogonal B" ``` immler@69675 ` 1618` ``` and "\x. x \ B \ norm x = 1" ``` immler@69675 ` 1619` ``` and "independent B" "card B = dim S" "span B = S" ``` immler@69675 ` 1620` ```proof - ``` immler@69675 ` 1621` ``` obtain B where "0 \ B" "B \ S" ``` immler@69675 ` 1622` ``` and orth: "pairwise orthogonal B" ``` immler@69675 ` 1623` ``` and "independent B" "card B = dim S" "span B = S" ``` immler@69675 ` 1624` ``` by (blast intro: orthogonal_basis_subspace [OF assms]) ``` immler@69675 ` 1625` ``` have 1: "(\x. x /\<^sub>R norm x) ` B \ S" ``` immler@69675 ` 1626` ``` using \span B = S\ span_superset span_mul by fastforce ``` immler@69675 ` 1627` ``` have 2: "pairwise orthogonal ((\x. x /\<^sub>R norm x) ` B)" ``` immler@69675 ` 1628` ``` using orth by (force simp: pairwise_def orthogonal_clauses) ``` immler@69675 ` 1629` ``` have 3: "\x. x \ (\x. x /\<^sub>R norm x) ` B \ norm x = 1" ``` immler@69675 ` 1630` ``` by (metis (no_types, lifting) \0 \ B\ image_iff norm_sgn sgn_div_norm) ``` immler@69675 ` 1631` ``` have 4: "independent ((\x. x /\<^sub>R norm x) ` B)" ``` immler@69675 ` 1632` ``` by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one) ``` immler@69675 ` 1633` ``` have "inj_on (\x. x /\<^sub>R norm x) B" ``` immler@69675 ` 1634` ``` proof ``` immler@69675 ` 1635` ``` fix x y ``` immler@69675 ` 1636` ``` assume "x \ B" "y \ B" "x /\<^sub>R norm x = y /\<^sub>R norm y" ``` immler@69675 ` 1637` ``` moreover have "\i. i \ B \ norm (i /\<^sub>R norm i) = 1" ``` immler@69675 ` 1638` ``` using 3 by blast ``` immler@69675 ` 1639` ``` ultimately show "x = y" ``` immler@69675 ` 1640` ``` by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one) ``` immler@69675 ` 1641` ``` qed ``` immler@69675 ` 1642` ``` then have 5: "card ((\x. x /\<^sub>R norm x) ` B) = dim S" ``` immler@69675 ` 1643` ``` by (metis \card B = dim S\ card_image) ``` immler@69675 ` 1644` ``` have 6: "span ((\x. x /\<^sub>R norm x) ` B) = S" ``` immler@69675 ` 1645` ``` by (metis "1" "4" "5" assms card_eq_dim independent_imp_finite span_subspace) ``` immler@69675 ` 1646` ``` show ?thesis ``` immler@69675 ` 1647` ``` by (rule that [OF 1 2 3 4 5 6]) ``` immler@69675 ` 1648` ```qed ``` immler@69675 ` 1649` immler@69675 ` 1650` immler@69675 ` 1651` ```proposition%unimportant orthogonal_to_subspace_exists_gen: ``` immler@69675 ` 1652` ``` fixes S :: "'a :: euclidean_space set" ``` immler@69675 ` 1653` ``` assumes "span S \ span T" ``` immler@69675 ` 1654` ``` obtains x where "x \ 0" "x \ span T" "\y. y \ span S \ orthogonal x y" ``` immler@69675 ` 1655` ```proof - ``` immler@69675 ` 1656` ``` obtain B where "B \ span S" and orthB: "pairwise orthogonal B" ``` immler@69675 ` 1657` ``` and "\x. x \ B \ norm x = 1" ``` immler@69675 ` 1658` ``` and "independent B" "card B = dim S" "span B = span S" ``` immler@69675 ` 1659` ``` by (rule orthonormal_basis_subspace [of "span S", OF subspace_span]) ``` immler@69675 ` 1660` ``` (auto simp: dim_span) ``` immler@69675 ` 1661` ``` with assms obtain u where spanBT: "span B \ span T" and "u \ span B" "u \ span T" ``` immler@69675 ` 1662` ``` by auto ``` immler@69675 ` 1663` ``` obtain C where orthBC: "pairwise orthogonal (B \ C)" and spanBC: "span (B \ C) = span (B \ {u})" ``` immler@69675 ` 1664` ``` by (blast intro: orthogonal_extension [OF orthB]) ``` immler@69675 ` 1665` ``` show thesis ``` immler@69675 ` 1666` ``` proof (cases "C \ insert 0 B") ``` immler@69675 ` 1667` ``` case True ``` immler@69675 ` 1668` ``` then have "C \ span B" ``` immler@69675 ` 1669` ``` using span_eq ``` immler@69675 ` 1670` ``` by (metis span_insert_0 subset_trans) ``` immler@69675 ` 1671` ``` moreover have "u \ span (B \ C)" ``` immler@69675 ` 1672` ``` using \span (B \ C) = span (B \ {u})\ span_superset by force ``` immler@69675 ` 1673` ``` ultimately show ?thesis ``` immler@69675 ` 1674` ``` using True \u \ span B\ ``` immler@69675 ` 1675` ``` by (metis Un_insert_left span_insert_0 sup.orderE) ``` immler@69675 ` 1676` ``` next ``` immler@69675 ` 1677` ``` case False ``` immler@69675 ` 1678` ``` then obtain x where "x \ C" "x \ 0" "x \ B" ``` immler@69675 ` 1679` ``` by blast ``` immler@69675 ` 1680` ``` then have "x \ span T" ``` immler@69675 ` 1681` ``` by (metis (no_types, lifting) Un_insert_right Un_upper2 \u \ span T\ spanBT spanBC ``` immler@69675 ` 1682` ``` \u \ span T\ insert_subset span_superset span_mono ``` immler@69675 ` 1683` ``` span_span subsetCE subset_trans sup_bot.comm_neutral) ``` immler@69675 ` 1684` ``` moreover have "orthogonal x y" if "y \ span B" for y ``` immler@69675 ` 1685` ``` using that ``` immler@69675 ` 1686` ``` proof (rule span_induct) ``` immler@69675 ` 1687` ``` show "subspace {a. orthogonal x a}" ``` immler@69675 ` 1688` ``` by (simp add: subspace_orthogonal_to_vector) ``` immler@69675 ` 1689` ``` show "\b. b \ B \ orthogonal x b" ``` immler@69675 ` 1690` ``` by (metis Un_iff \x \ C\ \x \ B\ orthBC pairwise_def) ``` immler@69675 ` 1691` ``` qed ``` immler@69675 ` 1692` ``` ultimately show ?thesis ``` immler@69675 ` 1693` ``` using \x \ 0\ that \span B = span S\ by auto ``` immler@69675 ` 1694` ``` qed ``` immler@69675 ` 1695` ```qed ``` immler@69675 ` 1696` immler@69675 ` 1697` ```corollary%unimportant orthogonal_to_subspace_exists: ``` immler@69675 ` 1698` ``` fixes S :: "'a :: euclidean_space set" ``` immler@69675 ` 1699` ``` assumes "dim S < DIM('a)" ``` immler@69675 ` 1700` ``` obtains x where "x \ 0" "\y. y \ span S \ orthogonal x y" ``` immler@69675 ` 1701` ```proof - ``` immler@69675 ` 1702` ```have "span S \ UNIV" ``` immler@69675 ` 1703` ``` by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane ``` immler@69675 ` 1704` ``` mem_Collect_eq top.extremum_strict top.not_eq_extremum) ``` immler@69675 ` 1705` ``` with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis ``` immler@69675 ` 1706` ``` by (auto simp: span_UNIV) ``` immler@69675 ` 1707` ```qed ``` immler@69675 ` 1708` immler@69675 ` 1709` ```corollary%unimportant orthogonal_to_vector_exists: ``` immler@69675 ` 1710` ``` fixes x :: "'a :: euclidean_space" ``` immler@69675 ` 1711` ``` assumes "2 \ DIM('a)" ``` immler@69675 ` 1712` ``` obtains y where "y \ 0" "orthogonal x y" ``` immler@69675 ` 1713` ```proof - ``` immler@69675 ` 1714` ``` have "dim {x} < DIM('a)" ``` immler@69675 ` 1715` ``` using assms by auto ``` immler@69675 ` 1716` ``` then show thesis ``` immler@69675 ` 1717` ``` by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that) ``` immler@69675 ` 1718` ```qed ``` immler@69675 ` 1719` immler@69675 ` 1720` ```proposition%unimportant orthogonal_subspace_decomp_exists: ``` immler@69675 ` 1721` ``` fixes S :: "'a :: euclidean_space set" ``` immler@69675 ` 1722` ``` obtains y z ``` immler@69675 ` 1723` ``` where "y \ span S" ``` immler@69675 ` 1724` ``` and "\w. w \ span S \ orthogonal z w" ``` immler@69675 ` 1725` ``` and "x = y + z" ``` immler@69675 ` 1726` ```proof - ``` immler@69675 ` 1727` ``` obtain T where "0 \ T" "T \ span S" "pairwise orthogonal T" "independent T" ``` immler@69675 ` 1728` ``` "card T = dim (span S)" "span T = span S" ``` immler@69675 ` 1729` ``` using orthogonal_basis_subspace subspace_span by blast ``` immler@69675 ` 1730` ``` let ?a = "\b\T. (b \ x / (b \ b)) *\<^sub>R b" ``` immler@69675 ` 1731` ``` have orth: "orthogonal (x - ?a) w" if "w \ span S" for w ``` immler@69675 ` 1732` ``` by (simp add: Gram_Schmidt_step \pairwise orthogonal T\ \span T = span S\ ``` immler@69675 ` 1733` ``` orthogonal_commute that) ``` immler@69675 ` 1734` ``` show ?thesis ``` immler@69675 ` 1735` ``` apply (rule_tac y = "?a" and z = "x - ?a" in that) ``` immler@69675 ` 1736` ``` apply (meson \T \ span S\ span_scale span_sum subsetCE) ``` immler@69675 ` 1737` ``` apply (fact orth, simp) ``` immler@69675 ` 1738` ``` done ``` immler@69675 ` 1739` ```qed ``` immler@69675 ` 1740` immler@69675 ` 1741` ```lemma orthogonal_subspace_decomp_unique: ``` immler@69675 ` 1742` ``` fixes S :: "'a :: euclidean_space set" ``` immler@69675 ` 1743` ``` assumes "x + y = x' + y'" ``` immler@69675 ` 1744` ``` and ST: "x \ span S" "x' \ span S" "y \ span T" "y' \ span T" ``` immler@69675 ` 1745` ``` and orth: "\a b. \a \ S; b \ T\ \ orthogonal a b" ``` immler@69675 ` 1746` ``` shows "x = x' \ y = y'" ``` immler@69675 ` 1747` ```proof - ``` immler@69675 ` 1748` ``` have "x + y - y' = x'" ``` immler@69675 ` 1749` ``` by (simp add: assms) ``` immler@69675 ` 1750` ``` moreover have "\a b. \a \ span S; b \ span T\ \ orthogonal a b" ``` immler@69675 ` 1751` ``` by (meson orth orthogonal_commute orthogonal_to_span) ``` immler@69675 ` 1752` ``` ultimately have "0 = x' - x" ``` immler@69675 ` 1753` ``` by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self) ``` immler@69675 ` 1754` ``` with assms show ?thesis by auto ``` immler@69675 ` 1755` ```qed ``` immler@69675 ` 1756` immler@69675 ` 1757` ```lemma vector_in_orthogonal_spanningset: ``` immler@69675 ` 1758` ``` fixes a :: "'a::euclidean_space" ``` immler@69675 ` 1759` ``` obtains S where "a \ S" "pairwise orthogonal S" "span S = UNIV" ``` immler@69675 ` 1760` ``` by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def ``` immler@69675 ` 1761` ``` pairwise_orthogonal_insert span_UNIV subsetI subset_antisym) ``` immler@69675 ` 1762` immler@69675 ` 1763` ```lemma vector_in_orthogonal_basis: ``` immler@69675 ` 1764` ``` fixes a :: "'a::euclidean_space" ``` immler@69675 ` 1765` ``` assumes "a \ 0" ``` immler@69675 ` 1766` ``` obtains S where "a \ S" "0 \ S" "pairwise orthogonal S" "independent S" "finite S" ``` immler@69675 ` 1767` ``` "span S = UNIV" "card S = DIM('a)" ``` immler@69675 ` 1768` ```proof - ``` immler@69675 ` 1769` ``` obtain S where S: "a \ S" "pairwise orthogonal S" "span S = UNIV" ``` immler@69675 ` 1770` ``` using vector_in_orthogonal_spanningset . ``` immler@69675 ` 1771` ``` show thesis ``` immler@69675 ` 1772` ``` proof ``` immler@69675 ` 1773` ``` show "pairwise orthogonal (S - {0})" ``` immler@69675 ` 1774` ``` using pairwise_mono S(2) by blast ``` immler@69675 ` 1775` ``` show "independent (S - {0})" ``` immler@69675 ` 1776` ``` by (simp add: \pairwise orthogonal (S - {0})\ pairwise_orthogonal_independent) ``` immler@69675 ` 1777` ``` show "finite (S - {0})" ``` immler@69675 ` 1778` ``` using \independent (S - {0})\ independent_imp_finite by blast ``` immler@69675 ` 1779` ``` show "card (S - {0}) = DIM('a)" ``` immler@69675 ` 1780` ``` using span_delete_0 [of S] S ``` immler@69675 ` 1781` ``` by (simp add: \independent (S - {0})\ indep_card_eq_dim_span dim_UNIV) ``` immler@69675 ` 1782` ``` qed (use S \a \ 0\ in auto) ``` immler@69675 ` 1783` ```qed ``` immler@69675 ` 1784` immler@69675 ` 1785` ```lemma vector_in_orthonormal_basis: ``` immler@69675 ` 1786` ``` fixes a :: "'a::euclidean_space" ``` immler@69675 ` 1787` ``` assumes "norm a = 1" ``` immler@69675 ` 1788` ``` obtains S where "a \ S" "pairwise orthogonal S" "\x. x \ S \ norm x = 1" ``` immler@69675 ` 1789` ``` "independent S" "card S = DIM('a)" "span S = UNIV" ``` immler@69675 ` 1790` ```proof - ``` immler@69675 ` 1791` ``` have "a \ 0" ``` immler@69675 ` 1792` ``` using assms by auto ``` immler@69675 ` 1793` ``` then obtain S where "a \ S" "0 \ S" "finite S" ``` immler@69675 ` 1794` ``` and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)" ``` immler@69675 ` 1795` ``` by (metis vector_in_orthogonal_basis) ``` immler@69675 ` 1796` ``` let ?S = "(\x. x /\<^sub>R norm x) ` S" ``` immler@69675 ` 1797` ``` show thesis ``` immler@69675 ` 1798` ``` proof ``` immler@69675 ` 1799` ``` show "a \ ?S" ``` immler@69675 ` 1800` ``` using \a \ S\ assms image_iff by fastforce ``` immler@69675 ` 1801` ``` next ``` immler@69675 ` 1802` ``` show "pairwise orthogonal ?S" ``` immler@69675 ` 1803` ``` using \pairwise orthogonal S\ by (auto simp: pairwise_def orthogonal_def) ``` immler@69675 ` 1804` ``` show "\x. x \ (\x. x /\<^sub>R norm x) ` S \ norm x = 1" ``` immler@69675 ` 1805` ``` using \0 \ S\ by (auto simp: divide_simps) ``` immler@69675 ` 1806` ``` then show "independent ?S" ``` immler@69675 ` 1807` ``` by (metis \pairwise orthogonal ((\x. x /\<^sub>R norm x) ` S)\ norm_zero pairwise_orthogonal_independent zero_neq_one) ``` immler@69675 ` 1808` ``` have "inj_on (\x. x /\<^sub>R norm x) S" ``` immler@69675 ` 1809` ``` unfolding inj_on_def ``` immler@69675 ` 1810` ``` by (metis (full_types) S(1) \0 \ S\ inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def) ``` immler@69675 ` 1811` ``` then show "card ?S = DIM('a)" ``` immler@69675 ` 1812` ``` by (simp add: card_image S) ``` immler@69675 ` 1813` ``` show "span ?S = UNIV" ``` immler@69675 ` 1814` ``` by (metis (no_types) \0 \ S\ \finite S\ \span S = UNIV\ ``` immler@69675 ` 1815` ``` field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale ``` immler@69675 ` 1816` ``` zero_less_norm_iff) ``` immler@69675 ` 1817` ``` qed ``` immler@69675 ` 1818` ```qed ``` immler@69675 ` 1819` immler@69675 ` 1820` ```proposition dim_orthogonal_sum: ``` immler@69675 ` 1821` ``` fixes A :: "'a::euclidean_space set" ``` immler@69675 ` 1822` ``` assumes "\x y. \x \ A; y \ B\ \ x \ y = 0" ``` immler@69675 ` 1823` ``` shows "dim(A \ B) = dim A + dim B" ``` immler@69675 ` 1824` ```proof - ``` immler@69675 ` 1825` ``` have 1: "\x y. \x \ span A; y \ B\ \ x \ y = 0" ``` immler@69675 ` 1826` ``` by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms) ``` immler@69675 ` 1827` ``` have "\x y. \x \ span A; y \ span B\ \ x \ y = 0" ``` immler@69675 ` 1828` ``` using 1 by (simp add: span_induct [OF _ subspace_hyperplane]) ``` immler@69675 ` 1829` ``` then have 0: "\x y. \x \ span A; y \ span B\ \ x \ y = 0" ``` immler@69675 ` 1830` ``` by simp ``` immler@69675 ` 1831` ``` have "dim(A \ B) = dim (span (A \ B))" ``` immler@69675 ` 1832` ``` by (simp add: dim_span) ``` immler@69675 ` 1833` ``` also have "span (A \ B) = ((\(a, b). a + b) ` (span A \ span B))" ``` immler@69675 ` 1834` ``` by (auto simp add: span_Un image_def) ``` immler@69675 ` 1835` ``` also have "dim \ = dim {x + y |x y. x \ span A \ y \ span B}" ``` immler@69675 ` 1836` ``` by (auto intro!: arg_cong [where f=dim]) ``` immler@69675 ` 1837` ``` also have "... = dim {x + y |x y. x \ span A \ y \ span B} + dim(span A \ span B)" ``` immler@69675 ` 1838` ``` by (auto simp: dest: 0) ``` immler@69675 ` 1839` ``` also have "... = dim (span A) + dim (span B)" ``` immler@69675 ` 1840` ``` by (rule dim_sums_Int) (auto simp: subspace_span) ``` immler@69675 ` 1841` ``` also have "... = dim A + dim B" ``` immler@69675 ` 1842` ``` by (simp add: dim_span) ``` immler@69675 ` 1843` ``` finally show ?thesis . ``` immler@69675 ` 1844` ```qed ``` immler@69675 ` 1845` immler@69675 ` 1846` ```lemma dim_subspace_orthogonal_to_vectors: ``` immler@69675 ` 1847` ``` fixes A :: "'a::euclidean_space set" ``` immler@69675 ` 1848` ``` assumes "subspace A" "subspace B" "A \ B" ``` immler@69675 ` 1849` ``` shows "dim {y \ B. \x \ A. orthogonal x y} + dim A = dim B" ``` immler@69675 ` 1850` ```proof - ``` immler@69675 ` 1851` ``` have "dim (span ({y \ B. \x\A. orthogonal x y} \ A)) = dim (span B)" ``` immler@69675 ` 1852` ``` proof (rule arg_cong [where f=dim, OF subset_antisym]) ``` immler@69675 ` 1853` ``` show "span ({y \ B. \x\A. orthogonal x y} \ A) \ span B" ``` immler@69675 ` 1854` ``` by (simp add: \A \ B\ Collect_restrict span_mono) ``` immler@69675 ` 1855` ``` next ``` immler@69675 ` 1856` ``` have *: "x \ span ({y \ B. \x\A. orthogonal x y} \ A)" ``` immler@69675 ` 1857` ``` if "x \ B" for x ``` immler@69675 ` 1858` ``` proof - ``` immler@69675 ` 1859` ``` obtain y z where "x = y + z" "y \ span A" and orth: "\w. w \ span A \ orthogonal z w" ``` immler@69675 ` 1860` ``` using orthogonal_subspace_decomp_exists [of A x] that by auto ``` immler@69675 ` 1861` ``` have "y \ span B" ``` immler@69675 ` 1862` ``` using \y \ span A\ assms(3) span_mono by blast ``` immler@69675 ` 1863` ``` then have "z \ {a \ B. \x. x \ A \ orthogonal x a}" ``` immler@69675 ` 1864` ``` apply simp ``` immler@69675 ` 1865` ``` using \x = y + z\ assms(1) assms(2) orth orthogonal_commute span_add_eq ``` immler@69675 ` 1866` ``` span_eq_iff that by blast ``` immler@69675 ` 1867` ``` then have z: "z \ span {y \ B. \x\A. orthogonal x y}" ``` immler@69675 ` 1868` ``` by (meson span_superset subset_iff) ``` immler@69675 ` 1869` ``` then show ?thesis ``` immler@69675 ` 1870` ``` apply (auto simp: span_Un image_def \x = y + z\ \y \ span A\) ``` immler@69675 ` 1871` ``` using \y \ span A\ add.commute by blast ``` immler@69675 ` 1872` ``` qed ``` immler@69675 ` 1873` ``` show "span B \ span ({y \ B. \x\A. orthogonal x y} \ A)" ``` immler@69675 ` 1874` ``` by (rule span_minimal) ``` immler@69675 ` 1875` ``` (auto intro: * span_minimal simp: subspace_span) ``` immler@69675 ` 1876` ``` qed ``` immler@69675 ` 1877` ``` then show ?thesis ``` immler@69675 ` 1878` ``` by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq ``` immler@69675 ` 1879` ``` orthogonal_commute orthogonal_def) ``` immler@69675 ` 1880` ```qed ``` immler@69675 ` 1881` immler@54776 ` 1882` ```end ```