src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
 author hoelzl Fri Dec 14 15:46:01 2012 +0100 (2012-12-14) changeset 50526 899c9c4e4a4c parent 49962 a8cc904a6820 child 50998 501200635659 permissions -rw-r--r--
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
 hoelzl@37489 ` 1` hoelzl@37489 ` 2` ```header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*} ``` hoelzl@37489 ` 3` hoelzl@37489 ` 4` ```theory Cartesian_Euclidean_Space ``` hoelzl@37489 ` 5` ```imports Finite_Cartesian_Product Integration ``` hoelzl@37489 ` 6` ```begin ``` hoelzl@37489 ` 7` hoelzl@37489 ` 8` ```lemma delta_mult_idempotent: ``` wenzelm@49644 ` 9` ``` "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" ``` wenzelm@49644 ` 10` ``` by (cases "k=a") auto ``` hoelzl@37489 ` 11` hoelzl@37489 ` 12` ```lemma setsum_Plus: ``` hoelzl@37489 ` 13` ``` "\finite A; finite B\ \ ``` hoelzl@37489 ` 14` ``` (\x\A <+> B. g x) = (\x\A. g (Inl x)) + (\x\B. g (Inr x))" ``` hoelzl@37489 ` 15` ``` unfolding Plus_def ``` hoelzl@37489 ` 16` ``` by (subst setsum_Un_disjoint, auto simp add: setsum_reindex) ``` hoelzl@37489 ` 17` hoelzl@37489 ` 18` ```lemma setsum_UNIV_sum: ``` hoelzl@37489 ` 19` ``` fixes g :: "'a::finite + 'b::finite \ _" ``` hoelzl@37489 ` 20` ``` shows "(\x\UNIV. g x) = (\x\UNIV. g (Inl x)) + (\x\UNIV. g (Inr x))" ``` hoelzl@37489 ` 21` ``` apply (subst UNIV_Plus_UNIV [symmetric]) ``` hoelzl@37489 ` 22` ``` apply (rule setsum_Plus [OF finite finite]) ``` hoelzl@37489 ` 23` ``` done ``` hoelzl@37489 ` 24` hoelzl@37489 ` 25` ```lemma setsum_mult_product: ``` hoelzl@37489 ` 26` ``` "setsum h {..i\{..j\{..j. j + i * B) {..j. j + i * B) ` {.. {i * B.. (\j. j + i * B) ` {.. (\ x y. (\ i. (x\$i) * (y\$i)))" ``` wenzelm@49644 ` 46` ```instance .. ``` wenzelm@49644 ` 47` hoelzl@37489 ` 48` ```end ``` hoelzl@37489 ` 49` huffman@44136 ` 50` ```instantiation vec :: (one, finite) one ``` hoelzl@37489 ` 51` ```begin ``` wenzelm@49644 ` 52` wenzelm@49644 ` 53` ```definition "1 \ (\ i. 1)" ``` wenzelm@49644 ` 54` ```instance .. ``` wenzelm@49644 ` 55` hoelzl@37489 ` 56` ```end ``` hoelzl@37489 ` 57` huffman@44136 ` 58` ```instantiation vec :: (ord, finite) ord ``` hoelzl@37489 ` 59` ```begin ``` wenzelm@49644 ` 60` wenzelm@49644 ` 61` ```definition "x \ y \ (\i. x\$i \ y\$i)" ``` wenzelm@49644 ` 62` ```definition "x < y \ (\i. x\$i < y\$i)" ``` wenzelm@49644 ` 63` ```instance .. ``` wenzelm@49644 ` 64` hoelzl@37489 ` 65` ```end ``` hoelzl@37489 ` 66` hoelzl@37489 ` 67` ```text{* The ordering on one-dimensional vectors is linear. *} ``` hoelzl@37489 ` 68` wenzelm@49197 ` 69` ```class cart_one = ``` wenzelm@49197 ` 70` ``` assumes UNIV_one: "card (UNIV \ 'a set) = Suc 0" ``` hoelzl@37489 ` 71` ```begin ``` wenzelm@49197 ` 72` wenzelm@49197 ` 73` ```subclass finite ``` wenzelm@49197 ` 74` ```proof ``` wenzelm@49197 ` 75` ``` from UNIV_one show "finite (UNIV :: 'a set)" ``` wenzelm@49197 ` 76` ``` by (auto intro!: card_ge_0_finite) ``` wenzelm@49197 ` 77` ```qed ``` wenzelm@49197 ` 78` hoelzl@37489 ` 79` ```end ``` hoelzl@37489 ` 80` wenzelm@49197 ` 81` ```instantiation vec :: (linorder, cart_one) linorder ``` wenzelm@49197 ` 82` ```begin ``` wenzelm@49197 ` 83` wenzelm@49197 ` 84` ```instance ``` wenzelm@49197 ` 85` ```proof ``` wenzelm@49197 ` 86` ``` obtain a :: 'b where all: "\P. (\i. P i) \ P a" ``` wenzelm@49197 ` 87` ``` proof - ``` wenzelm@49197 ` 88` ``` have "card (UNIV :: 'b set) = Suc 0" by (rule UNIV_one) ``` wenzelm@49197 ` 89` ``` then obtain b :: 'b where "UNIV = {b}" by (auto iff: card_Suc_eq) ``` wenzelm@49197 ` 90` ``` then have "\P. (\i\UNIV. P i) \ P b" by auto ``` wenzelm@49197 ` 91` ``` then show thesis by (auto intro: that) ``` wenzelm@49197 ` 92` ``` qed ``` wenzelm@49197 ` 93` wenzelm@49197 ` 94` ``` note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps ``` wenzelm@49197 ` 95` ``` fix x y z :: "'a^'b::cart_one" ``` wenzelm@49197 ` 96` ``` show "x \ x" "(x < y) = (x \ y \ \ y \ x)" "x \ y \ y \ x" by auto ``` wenzelm@49197 ` 97` ``` { assume "x\y" "y\z" then show "x\z" by auto } ``` wenzelm@49197 ` 98` ``` { assume "x\y" "y\x" then show "x=y" by auto } ``` wenzelm@49197 ` 99` ```qed ``` wenzelm@49197 ` 100` wenzelm@49197 ` 101` ```end ``` hoelzl@37489 ` 102` hoelzl@37489 ` 103` ```text{* Constant Vectors *} ``` hoelzl@37489 ` 104` hoelzl@37489 ` 105` ```definition "vec x = (\ i. x)" ``` hoelzl@37489 ` 106` hoelzl@37489 ` 107` ```text{* Also the scalar-vector multiplication. *} ``` hoelzl@37489 ` 108` hoelzl@37489 ` 109` ```definition vector_scalar_mult:: "'a::times \ 'a ^ 'n \ 'a ^ 'n" (infixl "*s" 70) ``` hoelzl@37489 ` 110` ``` where "c *s x = (\ i. c * (x\$i))" ``` hoelzl@37489 ` 111` wenzelm@49644 ` 112` hoelzl@37489 ` 113` ```subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} ``` hoelzl@37489 ` 114` hoelzl@37489 ` 115` ```method_setup vector = {* ``` hoelzl@37489 ` 116` ```let ``` hoelzl@37489 ` 117` ``` val ss1 = HOL_basic_ss addsimps [@{thm setsum_addf} RS sym, ``` wenzelm@49644 ` 118` ``` @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, ``` wenzelm@49644 ` 119` ``` @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym] ``` hoelzl@37489 ` 120` ``` val ss2 = @{simpset} addsimps ``` huffman@44136 ` 121` ``` [@{thm plus_vec_def}, @{thm times_vec_def}, ``` huffman@44136 ` 122` ``` @{thm minus_vec_def}, @{thm uminus_vec_def}, ``` huffman@44136 ` 123` ``` @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def}, ``` huffman@44136 ` 124` ``` @{thm scaleR_vec_def}, ``` huffman@44136 ` 125` ``` @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}] ``` wenzelm@49644 ` 126` ``` fun vector_arith_tac ths = ``` wenzelm@49644 ` 127` ``` simp_tac ss1 ``` wenzelm@49644 ` 128` ``` THEN' (fn i => rtac @{thm setsum_cong2} i ``` hoelzl@37489 ` 129` ``` ORELSE rtac @{thm setsum_0'} i ``` huffman@44136 ` 130` ``` ORELSE simp_tac (HOL_basic_ss addsimps [@{thm vec_eq_iff}]) i) ``` wenzelm@49644 ` 131` ``` (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) ``` wenzelm@49644 ` 132` ``` THEN' asm_full_simp_tac (ss2 addsimps ths) ``` wenzelm@49644 ` 133` ```in ``` hoelzl@37489 ` 134` ``` Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths))) ``` wenzelm@49644 ` 135` ```end ``` wenzelm@42814 ` 136` ```*} "lift trivial vector statements to real arith statements" ``` hoelzl@37489 ` 137` huffman@44136 ` 138` ```lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def) ``` huffman@44136 ` 139` ```lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def) ``` hoelzl@37489 ` 140` hoelzl@37489 ` 141` ```lemma vec_inj[simp]: "vec x = vec y \ x = y" by vector ``` hoelzl@37489 ` 142` hoelzl@37489 ` 143` ```lemma vec_in_image_vec: "vec x \ (vec ` S) \ x \ S" by auto ``` hoelzl@37489 ` 144` hoelzl@37489 ` 145` ```lemma vec_add: "vec(x + y) = vec x + vec y" by (vector vec_def) ``` hoelzl@37489 ` 146` ```lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def) ``` hoelzl@37489 ` 147` ```lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def) ``` hoelzl@37489 ` 148` ```lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def) ``` hoelzl@37489 ` 149` wenzelm@49644 ` 150` ```lemma vec_setsum: ``` wenzelm@49644 ` 151` ``` assumes "finite S" ``` hoelzl@37489 ` 152` ``` shows "vec(setsum f S) = setsum (vec o f) S" ``` wenzelm@49644 ` 153` ``` using assms ``` wenzelm@49644 ` 154` ```proof induct ``` wenzelm@49644 ` 155` ``` case empty ``` wenzelm@49644 ` 156` ``` then show ?case by simp ``` wenzelm@49644 ` 157` ```next ``` wenzelm@49644 ` 158` ``` case insert ``` wenzelm@49644 ` 159` ``` then show ?case by (auto simp add: vec_add) ``` wenzelm@49644 ` 160` ```qed ``` hoelzl@37489 ` 161` hoelzl@37489 ` 162` ```text{* Obvious "component-pushing". *} ``` hoelzl@37489 ` 163` hoelzl@37489 ` 164` ```lemma vec_component [simp]: "vec x \$ i = x" ``` hoelzl@37489 ` 165` ``` by (vector vec_def) ``` hoelzl@37489 ` 166` hoelzl@37489 ` 167` ```lemma vector_mult_component [simp]: "(x * y)\$i = x\$i * y\$i" ``` hoelzl@37489 ` 168` ``` by vector ``` hoelzl@37489 ` 169` hoelzl@37489 ` 170` ```lemma vector_smult_component [simp]: "(c *s y)\$i = c * (y\$i)" ``` hoelzl@37489 ` 171` ``` by vector ``` hoelzl@37489 ` 172` hoelzl@37489 ` 173` ```lemma cond_component: "(if b then x else y)\$i = (if b then x\$i else y\$i)" by vector ``` hoelzl@37489 ` 174` hoelzl@37489 ` 175` ```lemmas vector_component = ``` hoelzl@37489 ` 176` ``` vec_component vector_add_component vector_mult_component ``` hoelzl@37489 ` 177` ``` vector_smult_component vector_minus_component vector_uminus_component ``` hoelzl@37489 ` 178` ``` vector_scaleR_component cond_component ``` hoelzl@37489 ` 179` wenzelm@49644 ` 180` hoelzl@37489 ` 181` ```subsection {* Some frequently useful arithmetic lemmas over vectors. *} ``` hoelzl@37489 ` 182` huffman@44136 ` 183` ```instance vec :: (semigroup_mult, finite) semigroup_mult ``` huffman@44136 ` 184` ``` by default (vector mult_assoc) ``` hoelzl@37489 ` 185` huffman@44136 ` 186` ```instance vec :: (monoid_mult, finite) monoid_mult ``` huffman@44136 ` 187` ``` by default vector+ ``` hoelzl@37489 ` 188` huffman@44136 ` 189` ```instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult ``` huffman@44136 ` 190` ``` by default (vector mult_commute) ``` hoelzl@37489 ` 191` huffman@44136 ` 192` ```instance vec :: (ab_semigroup_idem_mult, finite) ab_semigroup_idem_mult ``` huffman@44136 ` 193` ``` by default (vector mult_idem) ``` hoelzl@37489 ` 194` huffman@44136 ` 195` ```instance vec :: (comm_monoid_mult, finite) comm_monoid_mult ``` huffman@44136 ` 196` ``` by default vector ``` hoelzl@37489 ` 197` huffman@44136 ` 198` ```instance vec :: (semiring, finite) semiring ``` huffman@44136 ` 199` ``` by default (vector field_simps)+ ``` hoelzl@37489 ` 200` huffman@44136 ` 201` ```instance vec :: (semiring_0, finite) semiring_0 ``` huffman@44136 ` 202` ``` by default (vector field_simps)+ ``` huffman@44136 ` 203` ```instance vec :: (semiring_1, finite) semiring_1 ``` huffman@44136 ` 204` ``` by default vector ``` huffman@44136 ` 205` ```instance vec :: (comm_semiring, finite) comm_semiring ``` huffman@44136 ` 206` ``` by default (vector field_simps)+ ``` hoelzl@37489 ` 207` huffman@44136 ` 208` ```instance vec :: (comm_semiring_0, finite) comm_semiring_0 .. ``` huffman@44136 ` 209` ```instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. ``` huffman@44136 ` 210` ```instance vec :: (semiring_0_cancel, finite) semiring_0_cancel .. ``` huffman@44136 ` 211` ```instance vec :: (comm_semiring_0_cancel, finite) comm_semiring_0_cancel .. ``` huffman@44136 ` 212` ```instance vec :: (ring, finite) ring .. ``` huffman@44136 ` 213` ```instance vec :: (semiring_1_cancel, finite) semiring_1_cancel .. ``` huffman@44136 ` 214` ```instance vec :: (comm_semiring_1, finite) comm_semiring_1 .. ``` hoelzl@37489 ` 215` huffman@44136 ` 216` ```instance vec :: (ring_1, finite) ring_1 .. ``` hoelzl@37489 ` 217` huffman@44136 ` 218` ```instance vec :: (real_algebra, finite) real_algebra ``` wenzelm@49644 ` 219` ``` by default (simp_all add: vec_eq_iff) ``` hoelzl@37489 ` 220` huffman@44136 ` 221` ```instance vec :: (real_algebra_1, finite) real_algebra_1 .. ``` hoelzl@37489 ` 222` wenzelm@49644 ` 223` ```lemma of_nat_index: "(of_nat n :: 'a::semiring_1 ^'n)\$i = of_nat n" ``` wenzelm@49644 ` 224` ```proof (induct n) ``` wenzelm@49644 ` 225` ``` case 0 ``` wenzelm@49644 ` 226` ``` then show ?case by vector ``` wenzelm@49644 ` 227` ```next ``` wenzelm@49644 ` 228` ``` case Suc ``` wenzelm@49644 ` 229` ``` then show ?case by vector ``` wenzelm@49644 ` 230` ```qed ``` hoelzl@37489 ` 231` wenzelm@49644 ` 232` ```lemma one_index[simp]: "(1 :: 'a::one ^'n)\$i = 1" ``` wenzelm@49644 ` 233` ``` by vector ``` hoelzl@37489 ` 234` huffman@44136 ` 235` ```instance vec :: (semiring_char_0, finite) semiring_char_0 ``` haftmann@38621 ` 236` ```proof ``` haftmann@38621 ` 237` ``` fix m n :: nat ``` haftmann@38621 ` 238` ``` show "inj (of_nat :: nat \ 'a ^ 'b)" ``` huffman@44136 ` 239` ``` by (auto intro!: injI simp add: vec_eq_iff of_nat_index) ``` hoelzl@37489 ` 240` ```qed ``` hoelzl@37489 ` 241` huffman@47108 ` 242` ```instance vec :: (numeral, finite) numeral .. ``` huffman@47108 ` 243` ```instance vec :: (semiring_numeral, finite) semiring_numeral .. ``` huffman@47108 ` 244` huffman@47108 ` 245` ```lemma numeral_index [simp]: "numeral w \$ i = numeral w" ``` wenzelm@49644 ` 246` ``` by (induct w) (simp_all only: numeral.simps vector_add_component one_index) ``` huffman@47108 ` 247` huffman@47108 ` 248` ```lemma neg_numeral_index [simp]: "neg_numeral w \$ i = neg_numeral w" ``` huffman@47108 ` 249` ``` by (simp only: neg_numeral_def vector_uminus_component numeral_index) ``` huffman@47108 ` 250` huffman@44136 ` 251` ```instance vec :: (comm_ring_1, finite) comm_ring_1 .. ``` huffman@44136 ` 252` ```instance vec :: (ring_char_0, finite) ring_char_0 .. ``` hoelzl@37489 ` 253` hoelzl@37489 ` 254` ```lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" ``` hoelzl@37489 ` 255` ``` by (vector mult_assoc) ``` hoelzl@37489 ` 256` ```lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x" ``` hoelzl@37489 ` 257` ``` by (vector field_simps) ``` hoelzl@37489 ` 258` ```lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y" ``` hoelzl@37489 ` 259` ``` by (vector field_simps) ``` hoelzl@37489 ` 260` ```lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector ``` hoelzl@37489 ` 261` ```lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector ``` hoelzl@37489 ` 262` ```lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y" ``` hoelzl@37489 ` 263` ``` by (vector field_simps) ``` hoelzl@37489 ` 264` ```lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector ``` hoelzl@37489 ` 265` ```lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector ``` huffman@47108 ` 266` ```lemma vector_sneg_minus1: "-x = (-1::'a::ring_1) *s x" by vector ``` hoelzl@37489 ` 267` ```lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector ``` hoelzl@37489 ` 268` ```lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x" ``` hoelzl@37489 ` 269` ``` by (vector field_simps) ``` hoelzl@37489 ` 270` hoelzl@37489 ` 271` ```lemma vec_eq[simp]: "(vec m = vec n) \ (m = n)" ``` huffman@44136 ` 272` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 273` hoelzl@37489 ` 274` ```lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) ``` hoelzl@37489 ` 275` ```lemma vector_mul_eq_0[simp]: "(a *s x = 0) \ a = (0::'a::idom) \ x = 0" ``` hoelzl@37489 ` 276` ``` by vector ``` hoelzl@37489 ` 277` ```lemma vector_mul_lcancel[simp]: "a *s x = a *s y \ a = (0::real) \ x = y" ``` hoelzl@37489 ` 278` ``` by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) ``` hoelzl@37489 ` 279` ```lemma vector_mul_rcancel[simp]: "a *s x = b *s x \ (a::real) = b \ x = 0" ``` hoelzl@37489 ` 280` ``` by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) ``` hoelzl@37489 ` 281` ```lemma vector_mul_lcancel_imp: "a \ (0::real) ==> a *s x = a *s y ==> (x = y)" ``` hoelzl@37489 ` 282` ``` by (metis vector_mul_lcancel) ``` hoelzl@37489 ` 283` ```lemma vector_mul_rcancel_imp: "x \ 0 \ (a::real) *s x = b *s x ==> a = b" ``` hoelzl@37489 ` 284` ``` by (metis vector_mul_rcancel) ``` hoelzl@37489 ` 285` hoelzl@37489 ` 286` ```lemma component_le_norm_cart: "\x\$i\ <= norm x" ``` huffman@44136 ` 287` ``` apply (simp add: norm_vec_def) ``` hoelzl@37489 ` 288` ``` apply (rule member_le_setL2, simp_all) ``` hoelzl@37489 ` 289` ``` done ``` hoelzl@37489 ` 290` hoelzl@37489 ` 291` ```lemma norm_bound_component_le_cart: "norm x <= e ==> \x\$i\ <= e" ``` hoelzl@37489 ` 292` ``` by (metis component_le_norm_cart order_trans) ``` hoelzl@37489 ` 293` hoelzl@37489 ` 294` ```lemma norm_bound_component_lt_cart: "norm x < e ==> \x\$i\ < e" ``` hoelzl@37489 ` 295` ``` by (metis component_le_norm_cart basic_trans_rules(21)) ``` hoelzl@37489 ` 296` hoelzl@37489 ` 297` ```lemma norm_le_l1_cart: "norm x <= setsum(\i. \x\$i\) UNIV" ``` huffman@44136 ` 298` ``` by (simp add: norm_vec_def setL2_le_setsum) ``` hoelzl@37489 ` 299` hoelzl@37489 ` 300` ```lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x" ``` huffman@44136 ` 301` ``` unfolding scaleR_vec_def vector_scalar_mult_def by simp ``` hoelzl@37489 ` 302` hoelzl@37489 ` 303` ```lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \c\ * dist x y" ``` hoelzl@37489 ` 304` ``` unfolding dist_norm scalar_mult_eq_scaleR ``` hoelzl@37489 ` 305` ``` unfolding scaleR_right_diff_distrib[symmetric] by simp ``` hoelzl@37489 ` 306` hoelzl@37489 ` 307` ```lemma setsum_component [simp]: ``` hoelzl@37489 ` 308` ``` fixes f:: " 'a \ ('b::comm_monoid_add) ^'n" ``` hoelzl@37489 ` 309` ``` shows "(setsum f S)\$i = setsum (\x. (f x)\$i) S" ``` wenzelm@49644 ` 310` ```proof (cases "finite S") ``` wenzelm@49644 ` 311` ``` case True ``` wenzelm@49644 ` 312` ``` then show ?thesis by induct simp_all ``` wenzelm@49644 ` 313` ```next ``` wenzelm@49644 ` 314` ``` case False ``` wenzelm@49644 ` 315` ``` then show ?thesis by simp ``` wenzelm@49644 ` 316` ```qed ``` hoelzl@37489 ` 317` hoelzl@37489 ` 318` ```lemma setsum_eq: "setsum f S = (\ i. setsum (\x. (f x)\$i ) S)" ``` huffman@44136 ` 319` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 320` hoelzl@37489 ` 321` ```lemma setsum_cmul: ``` hoelzl@37489 ` 322` ``` fixes f:: "'c \ ('a::semiring_1)^'n" ``` hoelzl@37489 ` 323` ``` shows "setsum (\x. c *s f x) S = c *s setsum f S" ``` huffman@44136 ` 324` ``` by (simp add: vec_eq_iff setsum_right_distrib) ``` hoelzl@37489 ` 325` hoelzl@37489 ` 326` ```(* TODO: use setsum_norm_allsubsets_bound *) ``` hoelzl@37489 ` 327` ```lemma setsum_norm_allsubsets_bound_cart: ``` hoelzl@37489 ` 328` ``` fixes f:: "'a \ real ^'n" ``` hoelzl@37489 ` 329` ``` assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" ``` hoelzl@37489 ` 330` ``` shows "setsum (\x. norm (f x)) P \ 2 * real CARD('n) * e" ``` hoelzl@50526 ` 331` ``` using setsum_norm_allsubsets_bound[OF assms] ``` hoelzl@50526 ` 332` ``` by (simp add: DIM_cart Basis_real_def) ``` hoelzl@37489 ` 333` huffman@44136 ` 334` ```instance vec :: (ordered_euclidean_space, finite) ordered_euclidean_space ``` hoelzl@37489 ` 335` ```proof ``` hoelzl@37489 ` 336` ``` fix x y::"'a^'b" ``` hoelzl@50526 ` 337` ``` show "(x \ y) = (\i\Basis. x \ i \ y \ i)" ``` hoelzl@50526 ` 338` ``` unfolding less_eq_vec_def apply(subst eucl_le) by (simp add: Basis_vec_def inner_axis) ``` hoelzl@50526 ` 339` ``` show"(x < y) = (\i\Basis. x \ i < y \ i)" ``` hoelzl@50526 ` 340` ``` unfolding less_vec_def apply(subst eucl_less) by (simp add: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 341` ```qed ``` hoelzl@37489 ` 342` hoelzl@37489 ` 343` ```subsection {* Matrix operations *} ``` hoelzl@37489 ` 344` hoelzl@37489 ` 345` ```text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *} ``` hoelzl@37489 ` 346` wenzelm@49644 ` 347` ```definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \ 'a ^'p^'n \ 'a ^ 'p ^'m" ``` wenzelm@49644 ` 348` ``` (infixl "**" 70) ``` hoelzl@37489 ` 349` ``` where "m ** m' == (\ i j. setsum (\k. ((m\$i)\$k) * ((m'\$k)\$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m" ``` hoelzl@37489 ` 350` wenzelm@49644 ` 351` ```definition matrix_vector_mult :: "('a::semiring_1) ^'n^'m \ 'a ^'n \ 'a ^ 'm" ``` wenzelm@49644 ` 352` ``` (infixl "*v" 70) ``` hoelzl@37489 ` 353` ``` where "m *v x \ (\ i. setsum (\j. ((m\$i)\$j) * (x\$j)) (UNIV ::'n set)) :: 'a^'m" ``` hoelzl@37489 ` 354` wenzelm@49644 ` 355` ```definition vector_matrix_mult :: "'a ^ 'm \ ('a::semiring_1) ^'n^'m \ 'a ^'n " ``` wenzelm@49644 ` 356` ``` (infixl "v*" 70) ``` hoelzl@37489 ` 357` ``` where "v v* m == (\ j. setsum (\i. ((m\$i)\$j) * (v\$i)) (UNIV :: 'm set)) :: 'a^'n" ``` hoelzl@37489 ` 358` hoelzl@37489 ` 359` ```definition "(mat::'a::zero => 'a ^'n^'n) k = (\ i j. if i = j then k else 0)" ``` hoelzl@37489 ` 360` ```definition transpose where ``` hoelzl@37489 ` 361` ``` "(transpose::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A\$j)\$i))" ``` hoelzl@37489 ` 362` ```definition "(row::'m => 'a ^'n^'m \ 'a ^'n) i A = (\ j. ((A\$i)\$j))" ``` hoelzl@37489 ` 363` ```definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\ i. ((A\$i)\$j))" ``` hoelzl@37489 ` 364` ```definition "rows(A::'a^'n^'m) = { row i A | i. i \ (UNIV :: 'm set)}" ``` hoelzl@37489 ` 365` ```definition "columns(A::'a^'n^'m) = { column i A | i. i \ (UNIV :: 'n set)}" ``` hoelzl@37489 ` 366` hoelzl@37489 ` 367` ```lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) ``` hoelzl@37489 ` 368` ```lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" ``` hoelzl@37489 ` 369` ``` by (vector matrix_matrix_mult_def setsum_addf[symmetric] field_simps) ``` hoelzl@37489 ` 370` hoelzl@37489 ` 371` ```lemma matrix_mul_lid: ``` hoelzl@37489 ` 372` ``` fixes A :: "'a::semiring_1 ^ 'm ^ 'n" ``` hoelzl@37489 ` 373` ``` shows "mat 1 ** A = A" ``` hoelzl@37489 ` 374` ``` apply (simp add: matrix_matrix_mult_def mat_def) ``` hoelzl@37489 ` 375` ``` apply vector ``` wenzelm@49644 ` 376` ``` apply (auto simp only: if_distrib cond_application_beta setsum_delta'[OF finite] ``` wenzelm@49644 ` 377` ``` mult_1_left mult_zero_left if_True UNIV_I) ``` wenzelm@49644 ` 378` ``` done ``` hoelzl@37489 ` 379` hoelzl@37489 ` 380` hoelzl@37489 ` 381` ```lemma matrix_mul_rid: ``` hoelzl@37489 ` 382` ``` fixes A :: "'a::semiring_1 ^ 'm ^ 'n" ``` hoelzl@37489 ` 383` ``` shows "A ** mat 1 = A" ``` hoelzl@37489 ` 384` ``` apply (simp add: matrix_matrix_mult_def mat_def) ``` hoelzl@37489 ` 385` ``` apply vector ``` wenzelm@49644 ` 386` ``` apply (auto simp only: if_distrib cond_application_beta setsum_delta[OF finite] ``` wenzelm@49644 ` 387` ``` mult_1_right mult_zero_right if_True UNIV_I cong: if_cong) ``` wenzelm@49644 ` 388` ``` done ``` hoelzl@37489 ` 389` hoelzl@37489 ` 390` ```lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" ``` hoelzl@37489 ` 391` ``` apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc) ``` hoelzl@37489 ` 392` ``` apply (subst setsum_commute) ``` hoelzl@37489 ` 393` ``` apply simp ``` hoelzl@37489 ` 394` ``` done ``` hoelzl@37489 ` 395` hoelzl@37489 ` 396` ```lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" ``` wenzelm@49644 ` 397` ``` apply (vector matrix_matrix_mult_def matrix_vector_mult_def ``` wenzelm@49644 ` 398` ``` setsum_right_distrib setsum_left_distrib mult_assoc) ``` hoelzl@37489 ` 399` ``` apply (subst setsum_commute) ``` hoelzl@37489 ` 400` ``` apply simp ``` hoelzl@37489 ` 401` ``` done ``` hoelzl@37489 ` 402` hoelzl@37489 ` 403` ```lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" ``` hoelzl@37489 ` 404` ``` apply (vector matrix_vector_mult_def mat_def) ``` wenzelm@49644 ` 405` ``` apply (simp add: if_distrib cond_application_beta setsum_delta' cong del: if_weak_cong) ``` wenzelm@49644 ` 406` ``` done ``` hoelzl@37489 ` 407` wenzelm@49644 ` 408` ```lemma matrix_transpose_mul: ``` wenzelm@49644 ` 409` ``` "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)" ``` huffman@44136 ` 410` ``` by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult_commute) ``` hoelzl@37489 ` 411` hoelzl@37489 ` 412` ```lemma matrix_eq: ``` hoelzl@37489 ` 413` ``` fixes A B :: "'a::semiring_1 ^ 'n ^ 'm" ``` hoelzl@37489 ` 414` ``` shows "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") ``` hoelzl@37489 ` 415` ``` apply auto ``` huffman@44136 ` 416` ``` apply (subst vec_eq_iff) ``` hoelzl@37489 ` 417` ``` apply clarify ``` hoelzl@50526 ` 418` ``` apply (clarsimp simp add: matrix_vector_mult_def if_distrib cond_application_beta vec_eq_iff cong del: if_weak_cong) ``` hoelzl@50526 ` 419` ``` apply (erule_tac x="axis ia 1" in allE) ``` hoelzl@37489 ` 420` ``` apply (erule_tac x="i" in allE) ``` hoelzl@50526 ` 421` ``` apply (auto simp add: if_distrib cond_application_beta axis_def ``` wenzelm@49644 ` 422` ``` setsum_delta[OF finite] cong del: if_weak_cong) ``` wenzelm@49644 ` 423` ``` done ``` hoelzl@37489 ` 424` wenzelm@49644 ` 425` ```lemma matrix_vector_mul_component: "((A::real^_^_) *v x)\$k = (A\$k) \ x" ``` huffman@44136 ` 426` ``` by (simp add: matrix_vector_mult_def inner_vec_def) ``` hoelzl@37489 ` 427` hoelzl@37489 ` 428` ```lemma dot_lmul_matrix: "((x::real ^_) v* A) \ y = x \ (A *v y)" ``` huffman@44136 ` 429` ``` apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac) ``` hoelzl@37489 ` 430` ``` apply (subst setsum_commute) ``` wenzelm@49644 ` 431` ``` apply simp ``` wenzelm@49644 ` 432` ``` done ``` hoelzl@37489 ` 433` hoelzl@37489 ` 434` ```lemma transpose_mat: "transpose (mat n) = mat n" ``` hoelzl@37489 ` 435` ``` by (vector transpose_def mat_def) ``` hoelzl@37489 ` 436` hoelzl@37489 ` 437` ```lemma transpose_transpose: "transpose(transpose A) = A" ``` hoelzl@37489 ` 438` ``` by (vector transpose_def) ``` hoelzl@37489 ` 439` hoelzl@37489 ` 440` ```lemma row_transpose: ``` hoelzl@37489 ` 441` ``` fixes A:: "'a::semiring_1^_^_" ``` hoelzl@37489 ` 442` ``` shows "row i (transpose A) = column i A" ``` huffman@44136 ` 443` ``` by (simp add: row_def column_def transpose_def vec_eq_iff) ``` hoelzl@37489 ` 444` hoelzl@37489 ` 445` ```lemma column_transpose: ``` hoelzl@37489 ` 446` ``` fixes A:: "'a::semiring_1^_^_" ``` hoelzl@37489 ` 447` ``` shows "column i (transpose A) = row i A" ``` huffman@44136 ` 448` ``` by (simp add: row_def column_def transpose_def vec_eq_iff) ``` hoelzl@37489 ` 449` hoelzl@37489 ` 450` ```lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A" ``` wenzelm@49644 ` 451` ``` by (auto simp add: rows_def columns_def row_transpose intro: set_eqI) ``` hoelzl@37489 ` 452` wenzelm@49644 ` 453` ```lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" ``` wenzelm@49644 ` 454` ``` by (metis transpose_transpose rows_transpose) ``` hoelzl@37489 ` 455` hoelzl@37489 ` 456` ```text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *} ``` hoelzl@37489 ` 457` hoelzl@37489 ` 458` ```lemma matrix_mult_dot: "A *v x = (\ i. A\$i \ x)" ``` huffman@44136 ` 459` ``` by (simp add: matrix_vector_mult_def inner_vec_def) ``` hoelzl@37489 ` 460` wenzelm@49644 ` 461` ```lemma matrix_mult_vsum: ``` wenzelm@49644 ` 462` ``` "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\i. (x\$i) *s column i A) (UNIV:: 'n set)" ``` huffman@44136 ` 463` ``` by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult_commute) ``` hoelzl@37489 ` 464` hoelzl@37489 ` 465` ```lemma vector_componentwise: ``` hoelzl@50526 ` 466` ``` "(x::'a::ring_1^'n) = (\ j. \i\UNIV. (x\$i) * (axis i 1 :: 'a^'n) \$ j)" ``` hoelzl@50526 ` 467` ``` by (simp add: axis_def if_distrib setsum_cases vec_eq_iff) ``` hoelzl@50526 ` 468` hoelzl@50526 ` 469` ```lemma basis_expansion: "setsum (\i. (x\$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" ``` hoelzl@50526 ` 470` ``` by (auto simp add: axis_def vec_eq_iff if_distrib setsum_cases cong del: if_weak_cong) ``` hoelzl@37489 ` 471` hoelzl@37489 ` 472` ```lemma linear_componentwise: ``` hoelzl@37489 ` 473` ``` fixes f:: "real ^'m \ real ^ _" ``` hoelzl@37489 ` 474` ``` assumes lf: "linear f" ``` hoelzl@50526 ` 475` ``` shows "(f x)\$j = setsum (\i. (x\$i) * (f (axis i 1)\$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") ``` wenzelm@49644 ` 476` ```proof - ``` hoelzl@37489 ` 477` ``` let ?M = "(UNIV :: 'm set)" ``` hoelzl@37489 ` 478` ``` let ?N = "(UNIV :: 'n set)" ``` hoelzl@37489 ` 479` ``` have fM: "finite ?M" by simp ``` hoelzl@50526 ` 480` ``` have "?rhs = (setsum (\i.(x\$i) *\<^sub>R f (axis i 1) ) ?M)\$j" ``` hoelzl@50526 ` 481` ``` unfolding setsum_component by simp ``` wenzelm@49644 ` 482` ``` then show ?thesis ``` hoelzl@50526 ` 483` ``` unfolding linear_setsum_mul[OF lf fM, symmetric] ``` hoelzl@50526 ` 484` ``` unfolding scalar_mult_eq_scaleR[symmetric] ``` hoelzl@50526 ` 485` ``` unfolding basis_expansion ``` hoelzl@50526 ` 486` ``` by simp ``` hoelzl@37489 ` 487` ```qed ``` hoelzl@37489 ` 488` hoelzl@37489 ` 489` ```text{* Inverse matrices (not necessarily square) *} ``` hoelzl@37489 ` 490` wenzelm@49644 ` 491` ```definition ``` wenzelm@49644 ` 492` ``` "invertible(A::'a::semiring_1^'n^'m) \ (\A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" ``` hoelzl@37489 ` 493` wenzelm@49644 ` 494` ```definition ``` wenzelm@49644 ` 495` ``` "matrix_inv(A:: 'a::semiring_1^'n^'m) = ``` wenzelm@49644 ` 496` ``` (SOME A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" ``` hoelzl@37489 ` 497` hoelzl@37489 ` 498` ```text{* Correspondence between matrices and linear operators. *} ``` hoelzl@37489 ` 499` wenzelm@49644 ` 500` ```definition matrix :: "('a::{plus,times, one, zero}^'m \ 'a ^ 'n) \ 'a^'m^'n" ``` hoelzl@50526 ` 501` ``` where "matrix f = (\ i j. (f(axis j 1))\$i)" ``` hoelzl@37489 ` 502` hoelzl@37489 ` 503` ```lemma matrix_vector_mul_linear: "linear(\x. A *v (x::real ^ _))" ``` wenzelm@49644 ` 504` ``` by (simp add: linear_def matrix_vector_mult_def vec_eq_iff ``` wenzelm@49644 ` 505` ``` field_simps setsum_right_distrib setsum_addf) ``` hoelzl@37489 ` 506` wenzelm@49644 ` 507` ```lemma matrix_works: ``` wenzelm@49644 ` 508` ``` assumes lf: "linear f" ``` wenzelm@49644 ` 509` ``` shows "matrix f *v x = f (x::real ^ 'n)" ``` wenzelm@49644 ` 510` ``` apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult_commute) ``` wenzelm@49644 ` 511` ``` apply clarify ``` wenzelm@49644 ` 512` ``` apply (rule linear_componentwise[OF lf, symmetric]) ``` wenzelm@49644 ` 513` ``` done ``` hoelzl@37489 ` 514` wenzelm@49644 ` 515` ```lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::real ^ 'n))" ``` wenzelm@49644 ` 516` ``` by (simp add: ext matrix_works) ``` hoelzl@37489 ` 517` hoelzl@37489 ` 518` ```lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: real ^ 'n)) = A" ``` hoelzl@37489 ` 519` ``` by (simp add: matrix_eq matrix_vector_mul_linear matrix_works) ``` hoelzl@37489 ` 520` hoelzl@37489 ` 521` ```lemma matrix_compose: ``` hoelzl@37489 ` 522` ``` assumes lf: "linear (f::real^'n \ real^'m)" ``` wenzelm@49644 ` 523` ``` and lg: "linear (g::real^'m \ real^_)" ``` hoelzl@37489 ` 524` ``` shows "matrix (g o f) = matrix g ** matrix f" ``` hoelzl@37489 ` 525` ``` using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]] ``` wenzelm@49644 ` 526` ``` by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) ``` hoelzl@37489 ` 527` wenzelm@49644 ` 528` ```lemma matrix_vector_column: ``` wenzelm@49644 ` 529` ``` "(A::'a::comm_semiring_1^'n^_) *v x = setsum (\i. (x\$i) *s ((transpose A)\$i)) (UNIV:: 'n set)" ``` huffman@44136 ` 530` ``` by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult_commute) ``` hoelzl@37489 ` 531` hoelzl@37489 ` 532` ```lemma adjoint_matrix: "adjoint(\x. (A::real^'n^'m) *v x) = (\x. transpose A *v x)" ``` hoelzl@37489 ` 533` ``` apply (rule adjoint_unique) ``` wenzelm@49644 ` 534` ``` apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def ``` wenzelm@49644 ` 535` ``` setsum_left_distrib setsum_right_distrib) ``` hoelzl@37489 ` 536` ``` apply (subst setsum_commute) ``` hoelzl@37489 ` 537` ``` apply (auto simp add: mult_ac) ``` hoelzl@37489 ` 538` ``` done ``` hoelzl@37489 ` 539` hoelzl@37489 ` 540` ```lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \ real ^'m)" ``` hoelzl@37489 ` 541` ``` shows "matrix(adjoint f) = transpose(matrix f)" ``` hoelzl@37489 ` 542` ``` apply (subst matrix_vector_mul[OF lf]) ``` wenzelm@49644 ` 543` ``` unfolding adjoint_matrix matrix_of_matrix_vector_mul ``` wenzelm@49644 ` 544` ``` apply rule ``` wenzelm@49644 ` 545` ``` done ``` wenzelm@49644 ` 546` hoelzl@37489 ` 547` huffman@44360 ` 548` ```subsection {* lambda skolemization on cartesian products *} ``` hoelzl@37489 ` 549` hoelzl@37489 ` 550` ```(* FIXME: rename do choice_cart *) ``` hoelzl@37489 ` 551` hoelzl@37489 ` 552` ```lemma lambda_skolem: "(\i. \x. P i x) \ ``` hoelzl@37494 ` 553` ``` (\x::'a ^ 'n. \i. P i (x \$ i))" (is "?lhs \ ?rhs") ``` wenzelm@49644 ` 554` ```proof - ``` hoelzl@37489 ` 555` ``` let ?S = "(UNIV :: 'n set)" ``` wenzelm@49644 ` 556` ``` { assume H: "?rhs" ``` wenzelm@49644 ` 557` ``` then have ?lhs by auto } ``` hoelzl@37489 ` 558` ``` moreover ``` wenzelm@49644 ` 559` ``` { assume H: "?lhs" ``` hoelzl@37489 ` 560` ``` then obtain f where f:"\i. P i (f i)" unfolding choice_iff by metis ``` hoelzl@37489 ` 561` ``` let ?x = "(\ i. (f i)) :: 'a ^ 'n" ``` wenzelm@49644 ` 562` ``` { fix i ``` hoelzl@37489 ` 563` ``` from f have "P i (f i)" by metis ``` hoelzl@37494 ` 564` ``` then have "P i (?x \$ i)" by auto ``` hoelzl@37489 ` 565` ``` } ``` hoelzl@37489 ` 566` ``` hence "\i. P i (?x\$i)" by metis ``` hoelzl@37489 ` 567` ``` hence ?rhs by metis } ``` hoelzl@37489 ` 568` ``` ultimately show ?thesis by metis ``` hoelzl@37489 ` 569` ```qed ``` hoelzl@37489 ` 570` hoelzl@37489 ` 571` ```lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \ (x - ((b \ x) / (b \ b)) *s b) = 0" ``` hoelzl@50526 ` 572` ``` unfolding inner_simps scalar_mult_eq_scaleR by auto ``` hoelzl@37489 ` 573` hoelzl@37489 ` 574` ```lemma left_invertible_transpose: ``` hoelzl@37489 ` 575` ``` "(\(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" ``` hoelzl@37489 ` 576` ``` by (metis matrix_transpose_mul transpose_mat transpose_transpose) ``` hoelzl@37489 ` 577` hoelzl@37489 ` 578` ```lemma right_invertible_transpose: ``` hoelzl@37489 ` 579` ``` "(\(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(B). B ** A = mat 1)" ``` hoelzl@37489 ` 580` ``` by (metis matrix_transpose_mul transpose_mat transpose_transpose) ``` hoelzl@37489 ` 581` hoelzl@37489 ` 582` ```lemma matrix_left_invertible_injective: ``` wenzelm@49644 ` 583` ``` "(\B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x y. A *v x = A *v y \ x = y)" ``` wenzelm@49644 ` 584` ```proof - ``` wenzelm@49644 ` 585` ``` { fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y" ``` hoelzl@37489 ` 586` ``` from xy have "B*v (A *v x) = B *v (A*v y)" by simp ``` hoelzl@37489 ` 587` ``` hence "x = y" ``` wenzelm@49644 ` 588` ``` unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid . } ``` hoelzl@37489 ` 589` ``` moreover ``` wenzelm@49644 ` 590` ``` { assume A: "\x y. A *v x = A *v y \ x = y" ``` hoelzl@37489 ` 591` ``` hence i: "inj (op *v A)" unfolding inj_on_def by auto ``` hoelzl@37489 ` 592` ``` from linear_injective_left_inverse[OF matrix_vector_mul_linear i] ``` hoelzl@37489 ` 593` ``` obtain g where g: "linear g" "g o op *v A = id" by blast ``` hoelzl@37489 ` 594` ``` have "matrix g ** A = mat 1" ``` hoelzl@37489 ` 595` ``` unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] ``` huffman@44165 ` 596` ``` using g(2) by (simp add: fun_eq_iff) ``` wenzelm@49644 ` 597` ``` then have "\B. (B::real ^'m^'n) ** A = mat 1" by blast } ``` hoelzl@37489 ` 598` ``` ultimately show ?thesis by blast ``` hoelzl@37489 ` 599` ```qed ``` hoelzl@37489 ` 600` hoelzl@37489 ` 601` ```lemma matrix_left_invertible_ker: ``` hoelzl@37489 ` 602` ``` "(\B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x. A *v x = 0 \ x = 0)" ``` hoelzl@37489 ` 603` ``` unfolding matrix_left_invertible_injective ``` hoelzl@37489 ` 604` ``` using linear_injective_0[OF matrix_vector_mul_linear, of A] ``` hoelzl@37489 ` 605` ``` by (simp add: inj_on_def) ``` hoelzl@37489 ` 606` hoelzl@37489 ` 607` ```lemma matrix_right_invertible_surjective: ``` wenzelm@49644 ` 608` ``` "(\B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \ surj (\x. A *v x)" ``` wenzelm@49644 ` 609` ```proof - ``` wenzelm@49644 ` 610` ``` { fix B :: "real ^'m^'n" ``` wenzelm@49644 ` 611` ``` assume AB: "A ** B = mat 1" ``` wenzelm@49644 ` 612` ``` { fix x :: "real ^ 'm" ``` hoelzl@37489 ` 613` ``` have "A *v (B *v x) = x" ``` wenzelm@49644 ` 614` ``` by (simp add: matrix_vector_mul_lid matrix_vector_mul_assoc AB) } ``` hoelzl@37489 ` 615` ``` hence "surj (op *v A)" unfolding surj_def by metis } ``` hoelzl@37489 ` 616` ``` moreover ``` wenzelm@49644 ` 617` ``` { assume sf: "surj (op *v A)" ``` hoelzl@37489 ` 618` ``` from linear_surjective_right_inverse[OF matrix_vector_mul_linear sf] ``` hoelzl@37489 ` 619` ``` obtain g:: "real ^'m \ real ^'n" where g: "linear g" "op *v A o g = id" ``` hoelzl@37489 ` 620` ``` by blast ``` hoelzl@37489 ` 621` hoelzl@37489 ` 622` ``` have "A ** (matrix g) = mat 1" ``` hoelzl@37489 ` 623` ``` unfolding matrix_eq matrix_vector_mul_lid ``` hoelzl@37489 ` 624` ``` matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] ``` huffman@44165 ` 625` ``` using g(2) unfolding o_def fun_eq_iff id_def ``` hoelzl@37489 ` 626` ``` . ``` hoelzl@37489 ` 627` ``` hence "\B. A ** (B::real^'m^'n) = mat 1" by blast ``` hoelzl@37489 ` 628` ``` } ``` hoelzl@37489 ` 629` ``` ultimately show ?thesis unfolding surj_def by blast ``` hoelzl@37489 ` 630` ```qed ``` hoelzl@37489 ` 631` hoelzl@37489 ` 632` ```lemma matrix_left_invertible_independent_columns: ``` hoelzl@37489 ` 633` ``` fixes A :: "real^'n^'m" ``` wenzelm@49644 ` 634` ``` shows "(\(B::real ^'m^'n). B ** A = mat 1) \ ``` wenzelm@49644 ` 635` ``` (\c. setsum (\i. c i *s column i A) (UNIV :: 'n set) = 0 \ (\i. c i = 0))" ``` wenzelm@49644 ` 636` ``` (is "?lhs \ ?rhs") ``` wenzelm@49644 ` 637` ```proof - ``` hoelzl@37489 ` 638` ``` let ?U = "UNIV :: 'n set" ``` wenzelm@49644 ` 639` ``` { assume k: "\x. A *v x = 0 \ x = 0" ``` wenzelm@49644 ` 640` ``` { fix c i ``` wenzelm@49644 ` 641` ``` assume c: "setsum (\i. c i *s column i A) ?U = 0" and i: "i \ ?U" ``` hoelzl@37489 ` 642` ``` let ?x = "\ i. c i" ``` hoelzl@37489 ` 643` ``` have th0:"A *v ?x = 0" ``` hoelzl@37489 ` 644` ``` using c ``` huffman@44136 ` 645` ``` unfolding matrix_mult_vsum vec_eq_iff ``` hoelzl@37489 ` 646` ``` by auto ``` hoelzl@37489 ` 647` ``` from k[rule_format, OF th0] i ``` huffman@44136 ` 648` ``` have "c i = 0" by (vector vec_eq_iff)} ``` wenzelm@49644 ` 649` ``` hence ?rhs by blast } ``` hoelzl@37489 ` 650` ``` moreover ``` wenzelm@49644 ` 651` ``` { assume H: ?rhs ``` wenzelm@49644 ` 652` ``` { fix x assume x: "A *v x = 0" ``` hoelzl@37489 ` 653` ``` let ?c = "\i. ((x\$i ):: real)" ``` hoelzl@37489 ` 654` ``` from H[rule_format, of ?c, unfolded matrix_mult_vsum[symmetric], OF x] ``` wenzelm@49644 ` 655` ``` have "x = 0" by vector } ``` wenzelm@49644 ` 656` ``` } ``` hoelzl@37489 ` 657` ``` ultimately show ?thesis unfolding matrix_left_invertible_ker by blast ``` hoelzl@37489 ` 658` ```qed ``` hoelzl@37489 ` 659` hoelzl@37489 ` 660` ```lemma matrix_right_invertible_independent_rows: ``` hoelzl@37489 ` 661` ``` fixes A :: "real^'n^'m" ``` wenzelm@49644 ` 662` ``` shows "(\(B::real^'m^'n). A ** B = mat 1) \ ``` wenzelm@49644 ` 663` ``` (\c. setsum (\i. c i *s row i A) (UNIV :: 'm set) = 0 \ (\i. c i = 0))" ``` hoelzl@37489 ` 664` ``` unfolding left_invertible_transpose[symmetric] ``` hoelzl@37489 ` 665` ``` matrix_left_invertible_independent_columns ``` hoelzl@37489 ` 666` ``` by (simp add: column_transpose) ``` hoelzl@37489 ` 667` hoelzl@37489 ` 668` ```lemma matrix_right_invertible_span_columns: ``` wenzelm@49644 ` 669` ``` "(\(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \ ``` wenzelm@49644 ` 670` ``` span (columns A) = UNIV" (is "?lhs = ?rhs") ``` wenzelm@49644 ` 671` ```proof - ``` hoelzl@37489 ` 672` ``` let ?U = "UNIV :: 'm set" ``` hoelzl@37489 ` 673` ``` have fU: "finite ?U" by simp ``` hoelzl@37489 ` 674` ``` have lhseq: "?lhs \ (\y. \(x::real^'m). setsum (\i. (x\$i) *s column i A) ?U = y)" ``` hoelzl@37489 ` 675` ``` unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def ``` wenzelm@49644 ` 676` ``` apply (subst eq_commute) ``` wenzelm@49644 ` 677` ``` apply rule ``` wenzelm@49644 ` 678` ``` done ``` hoelzl@37489 ` 679` ``` have rhseq: "?rhs \ (\x. x \ span (columns A))" by blast ``` wenzelm@49644 ` 680` ``` { assume h: ?lhs ``` wenzelm@49644 ` 681` ``` { fix x:: "real ^'n" ``` wenzelm@49644 ` 682` ``` from h[unfolded lhseq, rule_format, of x] obtain y :: "real ^'m" ``` wenzelm@49644 ` 683` ``` where y: "setsum (\i. (y\$i) *s column i A) ?U = x" by blast ``` wenzelm@49644 ` 684` ``` have "x \ span (columns A)" ``` wenzelm@49644 ` 685` ``` unfolding y[symmetric] ``` wenzelm@49644 ` 686` ``` apply (rule span_setsum[OF fU]) ``` wenzelm@49644 ` 687` ``` apply clarify ``` hoelzl@50526 ` 688` ``` unfolding scalar_mult_eq_scaleR ``` wenzelm@49644 ` 689` ``` apply (rule span_mul) ``` wenzelm@49644 ` 690` ``` apply (rule span_superset) ``` wenzelm@49644 ` 691` ``` unfolding columns_def ``` wenzelm@49644 ` 692` ``` apply blast ``` wenzelm@49644 ` 693` ``` done ``` wenzelm@49644 ` 694` ``` } ``` wenzelm@49644 ` 695` ``` then have ?rhs unfolding rhseq by blast } ``` hoelzl@37489 ` 696` ``` moreover ``` wenzelm@49644 ` 697` ``` { assume h:?rhs ``` hoelzl@37489 ` 698` ``` let ?P = "\(y::real ^'n). \(x::real^'m). setsum (\i. (x\$i) *s column i A) ?U = y" ``` wenzelm@49644 ` 699` ``` { fix y ``` wenzelm@49644 ` 700` ``` have "?P y" ``` hoelzl@50526 ` 701` ``` proof (rule span_induct_alt[of ?P "columns A", folded scalar_mult_eq_scaleR]) ``` hoelzl@37489 ` 702` ``` show "\x\real ^ 'm. setsum (\i. (x\$i) *s column i A) ?U = 0" ``` hoelzl@37489 ` 703` ``` by (rule exI[where x=0], simp) ``` hoelzl@37489 ` 704` ``` next ``` wenzelm@49644 ` 705` ``` fix c y1 y2 ``` wenzelm@49644 ` 706` ``` assume y1: "y1 \ columns A" and y2: "?P y2" ``` hoelzl@37489 ` 707` ``` from y1 obtain i where i: "i \ ?U" "y1 = column i A" ``` hoelzl@37489 ` 708` ``` unfolding columns_def by blast ``` hoelzl@37489 ` 709` ``` from y2 obtain x:: "real ^'m" where ``` hoelzl@37489 ` 710` ``` x: "setsum (\i. (x\$i) *s column i A) ?U = y2" by blast ``` hoelzl@37489 ` 711` ``` let ?x = "(\ j. if j = i then c + (x\$i) else (x\$j))::real^'m" ``` hoelzl@37489 ` 712` ``` show "?P (c*s y1 + y2)" ``` webertj@49962 ` 713` ``` proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left cond_application_beta cong del: if_weak_cong) ``` wenzelm@49644 ` 714` ``` fix j ``` wenzelm@49644 ` 715` ``` have th: "\xa \ ?U. (if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` wenzelm@49644 ` 716` ``` else (x\$xa) * ((column xa A\$j))) = (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))" ``` wenzelm@49644 ` 717` ``` using i(1) by (simp add: field_simps) ``` wenzelm@49644 ` 718` ``` have "setsum (\xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` wenzelm@49644 ` 719` ``` else (x\$xa) * ((column xa A\$j))) ?U = setsum (\xa. (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))) ?U" ``` wenzelm@49644 ` 720` ``` apply (rule setsum_cong[OF refl]) ``` wenzelm@49644 ` 721` ``` using th apply blast ``` wenzelm@49644 ` 722` ``` done ``` wenzelm@49644 ` 723` ``` also have "\ = setsum (\xa. if xa = i then c * ((column i A)\$j) else 0) ?U + setsum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" ``` wenzelm@49644 ` 724` ``` by (simp add: setsum_addf) ``` wenzelm@49644 ` 725` ``` also have "\ = c * ((column i A)\$j) + setsum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" ``` wenzelm@49644 ` 726` ``` unfolding setsum_delta[OF fU] ``` wenzelm@49644 ` 727` ``` using i(1) by simp ``` wenzelm@49644 ` 728` ``` finally show "setsum (\xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` wenzelm@49644 ` 729` ``` else (x\$xa) * ((column xa A\$j))) ?U = c * ((column i A)\$j) + setsum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" . ``` wenzelm@49644 ` 730` ``` qed ``` wenzelm@49644 ` 731` ``` next ``` wenzelm@49644 ` 732` ``` show "y \ span (columns A)" ``` wenzelm@49644 ` 733` ``` unfolding h by blast ``` wenzelm@49644 ` 734` ``` qed ``` wenzelm@49644 ` 735` ``` } ``` wenzelm@49644 ` 736` ``` then have ?lhs unfolding lhseq .. ``` wenzelm@49644 ` 737` ``` } ``` hoelzl@37489 ` 738` ``` ultimately show ?thesis by blast ``` hoelzl@37489 ` 739` ```qed ``` hoelzl@37489 ` 740` hoelzl@37489 ` 741` ```lemma matrix_left_invertible_span_rows: ``` hoelzl@37489 ` 742` ``` "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" ``` hoelzl@37489 ` 743` ``` unfolding right_invertible_transpose[symmetric] ``` hoelzl@37489 ` 744` ``` unfolding columns_transpose[symmetric] ``` hoelzl@37489 ` 745` ``` unfolding matrix_right_invertible_span_columns ``` wenzelm@49644 ` 746` ``` .. ``` hoelzl@37489 ` 747` hoelzl@37489 ` 748` ```text {* The same result in terms of square matrices. *} ``` hoelzl@37489 ` 749` hoelzl@37489 ` 750` ```lemma matrix_left_right_inverse: ``` hoelzl@37489 ` 751` ``` fixes A A' :: "real ^'n^'n" ``` hoelzl@37489 ` 752` ``` shows "A ** A' = mat 1 \ A' ** A = mat 1" ``` wenzelm@49644 ` 753` ```proof - ``` wenzelm@49644 ` 754` ``` { fix A A' :: "real ^'n^'n" ``` wenzelm@49644 ` 755` ``` assume AA': "A ** A' = mat 1" ``` hoelzl@37489 ` 756` ``` have sA: "surj (op *v A)" ``` hoelzl@37489 ` 757` ``` unfolding surj_def ``` hoelzl@37489 ` 758` ``` apply clarify ``` hoelzl@37489 ` 759` ``` apply (rule_tac x="(A' *v y)" in exI) ``` wenzelm@49644 ` 760` ``` apply (simp add: matrix_vector_mul_assoc AA' matrix_vector_mul_lid) ``` wenzelm@49644 ` 761` ``` done ``` hoelzl@37489 ` 762` ``` from linear_surjective_isomorphism[OF matrix_vector_mul_linear sA] ``` hoelzl@37489 ` 763` ``` obtain f' :: "real ^'n \ real ^'n" ``` hoelzl@37489 ` 764` ``` where f': "linear f'" "\x. f' (A *v x) = x" "\x. A *v f' x = x" by blast ``` hoelzl@37489 ` 765` ``` have th: "matrix f' ** A = mat 1" ``` wenzelm@49644 ` 766` ``` by (simp add: matrix_eq matrix_works[OF f'(1)] ``` wenzelm@49644 ` 767` ``` matrix_vector_mul_assoc[symmetric] matrix_vector_mul_lid f'(2)[rule_format]) ``` hoelzl@37489 ` 768` ``` hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp ``` wenzelm@49644 ` 769` ``` hence "matrix f' = A'" ``` wenzelm@49644 ` 770` ``` by (simp add: matrix_mul_assoc[symmetric] AA' matrix_mul_rid matrix_mul_lid) ``` hoelzl@37489 ` 771` ``` hence "matrix f' ** A = A' ** A" by simp ``` wenzelm@49644 ` 772` ``` hence "A' ** A = mat 1" by (simp add: th) ``` wenzelm@49644 ` 773` ``` } ``` hoelzl@37489 ` 774` ``` then show ?thesis by blast ``` hoelzl@37489 ` 775` ```qed ``` hoelzl@37489 ` 776` hoelzl@37489 ` 777` ```text {* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *} ``` hoelzl@37489 ` 778` hoelzl@37489 ` 779` ```definition "rowvector v = (\ i j. (v\$j))" ``` hoelzl@37489 ` 780` hoelzl@37489 ` 781` ```definition "columnvector v = (\ i j. (v\$i))" ``` hoelzl@37489 ` 782` wenzelm@49644 ` 783` ```lemma transpose_columnvector: "transpose(columnvector v) = rowvector v" ``` huffman@44136 ` 784` ``` by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff) ``` hoelzl@37489 ` 785` hoelzl@37489 ` 786` ```lemma transpose_rowvector: "transpose(rowvector v) = columnvector v" ``` huffman@44136 ` 787` ``` by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff) ``` hoelzl@37489 ` 788` wenzelm@49644 ` 789` ```lemma dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" ``` hoelzl@37489 ` 790` ``` by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) ``` hoelzl@37489 ` 791` wenzelm@49644 ` 792` ```lemma dot_matrix_product: ``` wenzelm@49644 ` 793` ``` "(x::real^'n) \ y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))\$1)\$1" ``` huffman@44136 ` 794` ``` by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def) ``` hoelzl@37489 ` 795` hoelzl@37489 ` 796` ```lemma dot_matrix_vector_mul: ``` hoelzl@37489 ` 797` ``` fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" ``` hoelzl@37489 ` 798` ``` shows "(A *v x) \ (B *v y) = ``` hoelzl@37489 ` 799` ``` (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))\$1)\$1" ``` wenzelm@49644 ` 800` ``` unfolding dot_matrix_product transpose_columnvector[symmetric] ``` wenzelm@49644 ` 801` ``` dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc .. ``` hoelzl@37489 ` 802` hoelzl@37489 ` 803` hoelzl@50526 ` 804` ```lemma infnorm_cart:"infnorm (x::real^'n) = Sup {abs(x\$i) |i. i\UNIV}" ``` hoelzl@50526 ` 805` ``` by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right) ``` hoelzl@37489 ` 806` wenzelm@49644 ` 807` ```lemma component_le_infnorm_cart: "\x\$i\ \ infnorm (x::real^'n)" ``` hoelzl@50526 ` 808` ``` using Basis_le_infnorm[of "axis i 1" x] ``` hoelzl@50526 ` 809` ``` by (simp add: Basis_vec_def axis_eq_axis inner_axis) ``` hoelzl@37489 ` 810` wenzelm@49644 ` 811` ```lemma continuous_component: "continuous F f \ continuous F (\x. f x \$ i)" ``` huffman@44647 ` 812` ``` unfolding continuous_def by (rule tendsto_vec_nth) ``` huffman@44213 ` 813` wenzelm@49644 ` 814` ```lemma continuous_on_component: "continuous_on s f \ continuous_on s (\x. f x \$ i)" ``` huffman@44647 ` 815` ``` unfolding continuous_on_def by (fast intro: tendsto_vec_nth) ``` huffman@44213 ` 816` hoelzl@37489 ` 817` ```lemma closed_positive_orthant: "closed {x::real^'n. \i. 0 \x\$i}" ``` huffman@44233 ` 818` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le) ``` huffman@44213 ` 819` hoelzl@37489 ` 820` ```lemma bounded_component_cart: "bounded s \ bounded ((\x. x \$ i) ` s)" ``` wenzelm@49644 ` 821` ``` unfolding bounded_def ``` wenzelm@49644 ` 822` ``` apply clarify ``` wenzelm@49644 ` 823` ``` apply (rule_tac x="x \$ i" in exI) ``` wenzelm@49644 ` 824` ``` apply (rule_tac x="e" in exI) ``` wenzelm@49644 ` 825` ``` apply clarify ``` wenzelm@49644 ` 826` ``` apply (rule order_trans [OF dist_vec_nth_le], simp) ``` wenzelm@49644 ` 827` ``` done ``` hoelzl@37489 ` 828` hoelzl@37489 ` 829` ```lemma compact_lemma_cart: ``` hoelzl@37489 ` 830` ``` fixes f :: "nat \ 'a::heine_borel ^ 'n" ``` hoelzl@37489 ` 831` ``` assumes "bounded s" and "\n. f n \ s" ``` hoelzl@37489 ` 832` ``` shows "\d. ``` hoelzl@37489 ` 833` ``` \l r. subseq r \ ``` hoelzl@37489 ` 834` ``` (\e>0. eventually (\n. \i\d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)" ``` hoelzl@37489 ` 835` ```proof ``` wenzelm@49644 ` 836` ``` fix d :: "'n set" ``` wenzelm@49644 ` 837` ``` have "finite d" by simp ``` hoelzl@37489 ` 838` ``` thus "\l::'a ^ 'n. \r. subseq r \ ``` hoelzl@37489 ` 839` ``` (\e>0. eventually (\n. \i\d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)" ``` wenzelm@49644 ` 840` ``` proof (induct d) ``` wenzelm@49644 ` 841` ``` case empty ``` wenzelm@49644 ` 842` ``` thus ?case unfolding subseq_def by auto ``` wenzelm@49644 ` 843` ``` next ``` wenzelm@49644 ` 844` ``` case (insert k d) ``` wenzelm@49644 ` 845` ``` have s': "bounded ((\x. x \$ k) ` s)" ``` wenzelm@49644 ` 846` ``` using `bounded s` by (rule bounded_component_cart) ``` wenzelm@49644 ` 847` ``` obtain l1::"'a^'n" and r1 where r1:"subseq r1" ``` wenzelm@49644 ` 848` ``` and lr1:"\e>0. eventually (\n. \i\d. dist (f (r1 n) \$ i) (l1 \$ i) < e) sequentially" ``` hoelzl@37489 ` 849` ``` using insert(3) by auto ``` wenzelm@49644 ` 850` ``` have f': "\n. f (r1 n) \$ k \ (\x. x \$ k) ` s" ``` wenzelm@49644 ` 851` ``` using `\n. f n \ s` by simp ``` wenzelm@49644 ` 852` ``` obtain l2 r2 where r2: "subseq r2" ``` wenzelm@49644 ` 853` ``` and lr2: "((\i. f (r1 (r2 i)) \$ k) ---> l2) sequentially" ``` hoelzl@37489 ` 854` ``` using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto ``` wenzelm@49644 ` 855` ``` def r \ "r1 \ r2" ``` wenzelm@49644 ` 856` ``` have r: "subseq r" ``` hoelzl@37489 ` 857` ``` using r1 and r2 unfolding r_def o_def subseq_def by auto ``` hoelzl@37489 ` 858` ``` moreover ``` hoelzl@37489 ` 859` ``` def l \ "(\ i. if i = k then l2 else l1\$i)::'a^'n" ``` wenzelm@49644 ` 860` ``` { fix e :: real assume "e > 0" ``` wenzelm@49644 ` 861` ``` from lr1 `e>0` have N1:"eventually (\n. \i\d. dist (f (r1 n) \$ i) (l1 \$ i) < e) sequentially" ``` wenzelm@49644 ` 862` ``` by blast ``` wenzelm@49644 ` 863` ``` from lr2 `e>0` have N2:"eventually (\n. dist (f (r1 (r2 n)) \$ k) l2 < e) sequentially" ``` wenzelm@49644 ` 864` ``` by (rule tendstoD) ``` hoelzl@37489 ` 865` ``` from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) \$ i) (l1 \$ i) < e) sequentially" ``` hoelzl@37489 ` 866` ``` by (rule eventually_subseq) ``` hoelzl@37489 ` 867` ``` have "eventually (\n. \i\(insert k d). dist (f (r n) \$ i) (l \$ i) < e) sequentially" ``` hoelzl@37489 ` 868` ``` using N1' N2 by (rule eventually_elim2, simp add: l_def r_def) ``` hoelzl@37489 ` 869` ``` } ``` hoelzl@37489 ` 870` ``` ultimately show ?case by auto ``` hoelzl@37489 ` 871` ``` qed ``` hoelzl@37489 ` 872` ```qed ``` hoelzl@37489 ` 873` huffman@44136 ` 874` ```instance vec :: (heine_borel, finite) heine_borel ``` hoelzl@37489 ` 875` ```proof ``` hoelzl@37489 ` 876` ``` fix s :: "('a ^ 'b) set" and f :: "nat \ 'a ^ 'b" ``` hoelzl@37489 ` 877` ``` assume s: "bounded s" and f: "\n. f n \ s" ``` hoelzl@37489 ` 878` ``` then obtain l r where r: "subseq r" ``` wenzelm@49644 ` 879` ``` and l: "\e>0. eventually (\n. \i\UNIV. dist (f (r n) \$ i) (l \$ i) < e) sequentially" ``` hoelzl@37489 ` 880` ``` using compact_lemma_cart [OF s f] by blast ``` hoelzl@37489 ` 881` ``` let ?d = "UNIV::'b set" ``` hoelzl@37489 ` 882` ``` { fix e::real assume "e>0" ``` hoelzl@37489 ` 883` ``` hence "0 < e / (real_of_nat (card ?d))" ``` wenzelm@49644 ` 884` ``` using zero_less_card_finite divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto ``` hoelzl@37489 ` 885` ``` with l have "eventually (\n. \i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))) sequentially" ``` hoelzl@37489 ` 886` ``` by simp ``` hoelzl@37489 ` 887` ``` moreover ``` wenzelm@49644 ` 888` ``` { fix n ``` wenzelm@49644 ` 889` ``` assume n: "\i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))" ``` hoelzl@37489 ` 890` ``` have "dist (f (r n)) l \ (\i\?d. dist (f (r n) \$ i) (l \$ i))" ``` huffman@44136 ` 891` ``` unfolding dist_vec_def using zero_le_dist by (rule setL2_le_setsum) ``` hoelzl@37489 ` 892` ``` also have "\ < (\i\?d. e / (real_of_nat (card ?d)))" ``` hoelzl@37489 ` 893` ``` by (rule setsum_strict_mono) (simp_all add: n) ``` hoelzl@37489 ` 894` ``` finally have "dist (f (r n)) l < e" by simp ``` hoelzl@37489 ` 895` ``` } ``` hoelzl@37489 ` 896` ``` ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" ``` hoelzl@37489 ` 897` ``` by (rule eventually_elim1) ``` hoelzl@37489 ` 898` ``` } ``` wenzelm@49644 ` 899` ``` hence "((f \ r) ---> l) sequentially" unfolding o_def tendsto_iff by simp ``` hoelzl@37489 ` 900` ``` with r show "\l r. subseq r \ ((f \ r) ---> l) sequentially" by auto ``` hoelzl@37489 ` 901` ```qed ``` hoelzl@37489 ` 902` wenzelm@49644 ` 903` ```lemma interval_cart: ``` wenzelm@49644 ` 904` ``` fixes a :: "'a::ord^'n" ``` wenzelm@49644 ` 905` ``` shows "{a <..< b} = {x::'a^'n. \i. a\$i < x\$i \ x\$i < b\$i}" ``` wenzelm@49644 ` 906` ``` and "{a .. b} = {x::'a^'n. \i. a\$i \ x\$i \ x\$i \ b\$i}" ``` huffman@44136 ` 907` ``` by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def) ``` hoelzl@37489 ` 908` wenzelm@49644 ` 909` ```lemma mem_interval_cart: ``` wenzelm@49644 ` 910` ``` fixes a :: "'a::ord^'n" ``` wenzelm@49644 ` 911` ``` shows "x \ {a<.. (\i. a\$i < x\$i \ x\$i < b\$i)" ``` wenzelm@49644 ` 912` ``` and "x \ {a .. b} \ (\i. a\$i \ x\$i \ x\$i \ b\$i)" ``` wenzelm@49644 ` 913` ``` using interval_cart[of a b] by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def) ``` hoelzl@37489 ` 914` wenzelm@49644 ` 915` ```lemma interval_eq_empty_cart: ``` wenzelm@49644 ` 916` ``` fixes a :: "real^'n" ``` wenzelm@49644 ` 917` ``` shows "({a <..< b} = {} \ (\i. b\$i \ a\$i))" (is ?th1) ``` wenzelm@49644 ` 918` ``` and "({a .. b} = {} \ (\i. b\$i < a\$i))" (is ?th2) ``` wenzelm@49644 ` 919` ```proof - ``` hoelzl@37489 ` 920` ``` { fix i x assume as:"b\$i \ a\$i" and x:"x\{a <..< b}" ``` hoelzl@37489 ` 921` ``` hence "a \$ i < x \$ i \ x \$ i < b \$ i" unfolding mem_interval_cart by auto ``` hoelzl@37489 ` 922` ``` hence "a\$i < b\$i" by auto ``` wenzelm@49644 ` 923` ``` hence False using as by auto } ``` hoelzl@37489 ` 924` ``` moreover ``` hoelzl@37489 ` 925` ``` { assume as:"\i. \ (b\$i \ a\$i)" ``` hoelzl@37489 ` 926` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` hoelzl@37489 ` 927` ``` { fix i ``` hoelzl@37489 ` 928` ``` have "a\$i < b\$i" using as[THEN spec[where x=i]] by auto ``` hoelzl@37489 ` 929` ``` hence "a\$i < ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i < b\$i" ``` hoelzl@37489 ` 930` ``` unfolding vector_smult_component and vector_add_component ``` wenzelm@49644 ` 931` ``` by auto } ``` wenzelm@49644 ` 932` ``` hence "{a <..< b} \ {}" using mem_interval_cart(1)[of "?x" a b] by auto } ``` hoelzl@37489 ` 933` ``` ultimately show ?th1 by blast ``` hoelzl@37489 ` 934` hoelzl@37489 ` 935` ``` { fix i x assume as:"b\$i < a\$i" and x:"x\{a .. b}" ``` hoelzl@37489 ` 936` ``` hence "a \$ i \ x \$ i \ x \$ i \ b \$ i" unfolding mem_interval_cart by auto ``` hoelzl@37489 ` 937` ``` hence "a\$i \ b\$i" by auto ``` wenzelm@49644 ` 938` ``` hence False using as by auto } ``` hoelzl@37489 ` 939` ``` moreover ``` hoelzl@37489 ` 940` ``` { assume as:"\i. \ (b\$i < a\$i)" ``` hoelzl@37489 ` 941` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` hoelzl@37489 ` 942` ``` { fix i ``` hoelzl@37489 ` 943` ``` have "a\$i \ b\$i" using as[THEN spec[where x=i]] by auto ``` hoelzl@37489 ` 944` ``` hence "a\$i \ ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i \ b\$i" ``` hoelzl@37489 ` 945` ``` unfolding vector_smult_component and vector_add_component ``` wenzelm@49644 ` 946` ``` by auto } ``` hoelzl@37489 ` 947` ``` hence "{a .. b} \ {}" using mem_interval_cart(2)[of "?x" a b] by auto } ``` hoelzl@37489 ` 948` ``` ultimately show ?th2 by blast ``` hoelzl@37489 ` 949` ```qed ``` hoelzl@37489 ` 950` wenzelm@49644 ` 951` ```lemma interval_ne_empty_cart: ``` wenzelm@49644 ` 952` ``` fixes a :: "real^'n" ``` wenzelm@49644 ` 953` ``` shows "{a .. b} \ {} \ (\i. a\$i \ b\$i)" ``` wenzelm@49644 ` 954` ``` and "{a <..< b} \ {} \ (\i. a\$i < b\$i)" ``` hoelzl@37489 ` 955` ``` unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le) ``` hoelzl@37489 ` 956` ``` (* BH: Why doesn't just "auto" work here? *) ``` hoelzl@37489 ` 957` wenzelm@49644 ` 958` ```lemma subset_interval_imp_cart: ``` wenzelm@49644 ` 959` ``` fixes a :: "real^'n" ``` wenzelm@49644 ` 960` ``` shows "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ {c .. d} \ {a .. b}" ``` wenzelm@49644 ` 961` ``` and "(\i. a\$i < c\$i \ d\$i < b\$i) \ {c .. d} \ {a<..i. a\$i \ c\$i \ d\$i \ b\$i) \ {c<.. {a .. b}" ``` wenzelm@49644 ` 963` ``` and "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ {c<.. {a<.. {a<.. {a .. b}" ``` wenzelm@49644 ` 978` ```proof (simp add: subset_eq, rule) ``` hoelzl@37489 ` 979` ``` fix x ``` wenzelm@49644 ` 980` ``` assume x: "x \{a<.. x \$ i" ``` hoelzl@37489 ` 983` ``` using x order_less_imp_le[of "a\$i" "x\$i"] ``` huffman@44136 ` 984` ``` by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) ``` hoelzl@37489 ` 985` ``` } ``` hoelzl@37489 ` 986` ``` moreover ``` hoelzl@37489 ` 987` ``` { fix i ``` hoelzl@37489 ` 988` ``` have "x \$ i \ b \$ i" ``` hoelzl@37489 ` 989` ``` using x order_less_imp_le[of "x\$i" "b\$i"] ``` huffman@44136 ` 990` ``` by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) ``` hoelzl@37489 ` 991` ``` } ``` hoelzl@37489 ` 992` ``` ultimately ``` hoelzl@37489 ` 993` ``` show "a \ x \ x \ b" ``` huffman@44136 ` 994` ``` by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) ``` hoelzl@37489 ` 995` ```qed ``` hoelzl@37489 ` 996` wenzelm@49644 ` 997` ```lemma subset_interval_cart: ``` wenzelm@49644 ` 998` ``` fixes a :: "real^'n" ``` wenzelm@49644 ` 999` ``` shows "{c .. d} \ {a .. b} \ (\i. c\$i \ d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th1) ``` wenzelm@49644 ` 1000` ``` and "{c .. d} \ {a<.. (\i. c\$i \ d\$i) --> (\i. a\$i < c\$i \ d\$i < b\$i)" (is ?th2) ``` wenzelm@49644 ` 1001` ``` and "{c<.. {a .. b} \ (\i. c\$i < d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th3) ``` wenzelm@49644 ` 1002` ``` and "{c<.. {a<.. (\i. c\$i < d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th4) ``` hoelzl@50526 ` 1003` ``` using subset_interval[of c d a b] by (simp_all add: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 1004` wenzelm@49644 ` 1005` ```lemma disjoint_interval_cart: ``` wenzelm@49644 ` 1006` ``` fixes a::"real^'n" ``` wenzelm@49644 ` 1007` ``` shows "{a .. b} \ {c .. d} = {} \ (\i. (b\$i < a\$i \ d\$i < c\$i \ b\$i < c\$i \ d\$i < a\$i))" (is ?th1) ``` wenzelm@49644 ` 1008` ``` and "{a .. b} \ {c<.. (\i. (b\$i < a\$i \ d\$i \ c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th2) ``` wenzelm@49644 ` 1009` ``` and "{a<.. {c .. d} = {} \ (\i. (b\$i \ a\$i \ d\$i < c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th3) ``` wenzelm@49644 ` 1010` ``` and "{a<.. {c<.. (\i. (b\$i \ a\$i \ d\$i \ c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th4) ``` hoelzl@50526 ` 1011` ``` using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 1012` wenzelm@49644 ` 1013` ```lemma inter_interval_cart: ``` wenzelm@49644 ` 1014` ``` fixes a :: "'a::linorder^'n" ``` wenzelm@49644 ` 1015` ``` shows "{a .. b} \ {c .. d} = {(\ i. max (a\$i) (c\$i)) .. (\ i. min (b\$i) (d\$i))}" ``` nipkow@39302 ` 1016` ``` unfolding set_eq_iff and Int_iff and mem_interval_cart ``` hoelzl@37489 ` 1017` ``` by auto ``` hoelzl@37489 ` 1018` wenzelm@49644 ` 1019` ```lemma closed_interval_left_cart: ``` wenzelm@49644 ` 1020` ``` fixes b :: "real^'n" ``` hoelzl@37489 ` 1021` ``` shows "closed {x::real^'n. \i. x\$i \ b\$i}" ``` huffman@44233 ` 1022` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le) ``` hoelzl@37489 ` 1023` wenzelm@49644 ` 1024` ```lemma closed_interval_right_cart: ``` wenzelm@49644 ` 1025` ``` fixes a::"real^'n" ``` hoelzl@37489 ` 1026` ``` shows "closed {x::real^'n. \i. a\$i \ x\$i}" ``` huffman@44233 ` 1027` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le) ``` hoelzl@37489 ` 1028` wenzelm@49644 ` 1029` ```lemma is_interval_cart: ``` wenzelm@49644 ` 1030` ``` "is_interval (s::(real^'n) set) \ ``` wenzelm@49644 ` 1031` ``` (\a\s. \b\s. \x. (\i. ((a\$i \ x\$i \ x\$i \ b\$i) \ (b\$i \ x\$i \ x\$i \ a\$i))) \ x \ s)" ``` hoelzl@50526 ` 1032` ``` by (simp add: is_interval_def Ball_def Basis_vec_def inner_axis imp_ex) ``` hoelzl@37489 ` 1033` wenzelm@49644 ` 1034` ```lemma closed_halfspace_component_le_cart: "closed {x::real^'n. x\$i \ a}" ``` huffman@44233 ` 1035` ``` by (simp add: closed_Collect_le) ``` hoelzl@37489 ` 1036` wenzelm@49644 ` 1037` ```lemma closed_halfspace_component_ge_cart: "closed {x::real^'n. x\$i \ a}" ``` huffman@44233 ` 1038` ``` by (simp add: closed_Collect_le) ``` hoelzl@37489 ` 1039` wenzelm@49644 ` 1040` ```lemma open_halfspace_component_lt_cart: "open {x::real^'n. x\$i < a}" ``` wenzelm@49644 ` 1041` ``` by (simp add: open_Collect_less) ``` wenzelm@49644 ` 1042` wenzelm@49644 ` 1043` ```lemma open_halfspace_component_gt_cart: "open {x::real^'n. x\$i > a}" ``` huffman@44233 ` 1044` ``` by (simp add: open_Collect_less) ``` hoelzl@37489 ` 1045` wenzelm@49644 ` 1046` ```lemma Lim_component_le_cart: ``` wenzelm@49644 ` 1047` ``` fixes f :: "'a \ real^'n" ``` hoelzl@50526 ` 1048` ``` assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. f x \$i \ b) net" ``` hoelzl@37489 ` 1049` ``` shows "l\$i \ b" ``` hoelzl@50526 ` 1050` ``` by (rule tendsto_le[OF assms(2) tendsto_const tendsto_vec_nth, OF assms(1, 3)]) ``` hoelzl@37489 ` 1051` wenzelm@49644 ` 1052` ```lemma Lim_component_ge_cart: ``` wenzelm@49644 ` 1053` ``` fixes f :: "'a \ real^'n" ``` hoelzl@37489 ` 1054` ``` assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)\$i) net" ``` hoelzl@37489 ` 1055` ``` shows "b \ l\$i" ``` hoelzl@50526 ` 1056` ``` by (rule tendsto_le[OF assms(2) tendsto_vec_nth tendsto_const, OF assms(1, 3)]) ``` hoelzl@37489 ` 1057` wenzelm@49644 ` 1058` ```lemma Lim_component_eq_cart: ``` wenzelm@49644 ` 1059` ``` fixes f :: "'a \ real^'n" ``` wenzelm@49644 ` 1060` ``` assumes net: "(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\x. f(x)\$i = b) net" ``` hoelzl@37489 ` 1061` ``` shows "l\$i = b" ``` wenzelm@49644 ` 1062` ``` using ev[unfolded order_eq_iff eventually_conj_iff] and ``` wenzelm@49644 ` 1063` ``` Lim_component_ge_cart[OF net, of b i] and ``` hoelzl@37489 ` 1064` ``` Lim_component_le_cart[OF net, of i b] by auto ``` hoelzl@37489 ` 1065` wenzelm@49644 ` 1066` ```lemma connected_ivt_component_cart: ``` wenzelm@49644 ` 1067` ``` fixes x :: "real^'n" ``` wenzelm@49644 ` 1068` ``` shows "connected s \ x \ s \ y \ s \ x\$k \ a \ a \ y\$k \ (\z\s. z\$k = a)" ``` hoelzl@50526 ` 1069` ``` using connected_ivt_hyperplane[of s x y "axis k 1" a] ``` hoelzl@50526 ` 1070` ``` by (auto simp add: inner_axis inner_commute) ``` hoelzl@37489 ` 1071` wenzelm@49644 ` 1072` ```lemma subspace_substandard_cart: "subspace {x::real^_. (\i. P i \ x\$i = 0)}" ``` hoelzl@37489 ` 1073` ``` unfolding subspace_def by auto ``` hoelzl@37489 ` 1074` hoelzl@37489 ` 1075` ```lemma closed_substandard_cart: ``` huffman@44213 ` 1076` ``` "closed {x::'a::real_normed_vector ^ 'n. \i. P i \ x\$i = 0}" ``` wenzelm@49644 ` 1077` ```proof - ``` huffman@44213 ` 1078` ``` { fix i::'n ``` huffman@44213 ` 1079` ``` have "closed {x::'a ^ 'n. P i \ x\$i = 0}" ``` wenzelm@49644 ` 1080` ``` by (cases "P i") (simp_all add: closed_Collect_eq) } ``` huffman@44213 ` 1081` ``` thus ?thesis ``` huffman@44213 ` 1082` ``` unfolding Collect_all_eq by (simp add: closed_INT) ``` hoelzl@37489 ` 1083` ```qed ``` hoelzl@37489 ` 1084` wenzelm@49644 ` 1085` ```lemma dim_substandard_cart: "dim {x::real^'n. \i. i \ d \ x\$i = 0} = card d" ``` wenzelm@49644 ` 1086` ``` (is "dim ?A = _") ``` wenzelm@49644 ` 1087` ```proof - ``` hoelzl@50526 ` 1088` ``` let ?a = "\x. axis x 1 :: real^'n" ``` hoelzl@50526 ` 1089` ``` have *: "{x. \i\Basis. i \ ?a ` d \ x \ i = 0} = ?A" ``` hoelzl@50526 ` 1090` ``` by (auto simp: image_iff Basis_vec_def axis_eq_axis inner_axis) ``` hoelzl@50526 ` 1091` ``` have "?a ` d \ Basis" ``` hoelzl@50526 ` 1092` ``` by (auto simp: Basis_vec_def) ``` wenzelm@49644 ` 1093` ``` thus ?thesis ``` hoelzl@50526 ` 1094` ``` using dim_substandard[of "?a ` d"] card_image[of ?a d] ``` hoelzl@50526 ` 1095` ``` by (auto simp: axis_eq_axis inj_on_def *) ``` hoelzl@37489 ` 1096` ```qed ``` hoelzl@37489 ` 1097` hoelzl@37489 ` 1098` ```lemma affinity_inverses: ``` hoelzl@37489 ` 1099` ``` assumes m0: "m \ (0::'a::field)" ``` hoelzl@37489 ` 1100` ``` shows "(\x. m *s x + c) o (\x. inverse(m) *s x + (-(inverse(m) *s c))) = id" ``` hoelzl@37489 ` 1101` ``` "(\x. inverse(m) *s x + (-(inverse(m) *s c))) o (\x. m *s x + c) = id" ``` hoelzl@37489 ` 1102` ``` using m0 ``` wenzelm@49644 ` 1103` ``` apply (auto simp add: fun_eq_iff vector_add_ldistrib) ``` wenzelm@49644 ` 1104` ``` apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric]) ``` wenzelm@49644 ` 1105` ``` done ``` hoelzl@37489 ` 1106` hoelzl@37489 ` 1107` ```lemma vector_affinity_eq: ``` hoelzl@37489 ` 1108` ``` assumes m0: "(m::'a::field) \ 0" ``` hoelzl@37489 ` 1109` ``` shows "m *s x + c = y \ x = inverse m *s y + -(inverse m *s c)" ``` hoelzl@37489 ` 1110` ```proof ``` hoelzl@37489 ` 1111` ``` assume h: "m *s x + c = y" ``` hoelzl@37489 ` 1112` ``` hence "m *s x = y - c" by (simp add: field_simps) ``` hoelzl@37489 ` 1113` ``` hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp ``` hoelzl@37489 ` 1114` ``` then show "x = inverse m *s y + - (inverse m *s c)" ``` hoelzl@37489 ` 1115` ``` using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) ``` hoelzl@37489 ` 1116` ```next ``` hoelzl@37489 ` 1117` ``` assume h: "x = inverse m *s y + - (inverse m *s c)" ``` hoelzl@37489 ` 1118` ``` show "m *s x + c = y" unfolding h diff_minus[symmetric] ``` hoelzl@37489 ` 1119` ``` using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) ``` hoelzl@37489 ` 1120` ```qed ``` hoelzl@37489 ` 1121` hoelzl@37489 ` 1122` ```lemma vector_eq_affinity: ``` wenzelm@49644 ` 1123` ``` "(m::'a::field) \ 0 ==> (y = m *s x + c \ inverse(m) *s y + -(inverse(m) *s c) = x)" ``` hoelzl@37489 ` 1124` ``` using vector_affinity_eq[where m=m and x=x and y=y and c=c] ``` hoelzl@37489 ` 1125` ``` by metis ``` hoelzl@37489 ` 1126` hoelzl@50526 ` 1127` ```lemma vector_cart: ``` hoelzl@50526 ` 1128` ``` fixes f :: "real^'n \ real" ``` hoelzl@50526 ` 1129` ``` shows "(\ i. f (axis i 1)) = (\i\Basis. f i *\<^sub>R i)" ``` hoelzl@50526 ` 1130` ``` unfolding euclidean_eq_iff[where 'a="real^'n"] ``` hoelzl@50526 ` 1131` ``` by simp (simp add: Basis_vec_def inner_axis) ``` hoelzl@50526 ` 1132` ``` ``` hoelzl@50526 ` 1133` ```lemma const_vector_cart:"((\ i. d)::real^'n) = (\i\Basis. d *\<^sub>R i)" ``` hoelzl@50526 ` 1134` ``` by (rule vector_cart) ``` wenzelm@49644 ` 1135` huffman@44360 ` 1136` ```subsection "Convex Euclidean Space" ``` hoelzl@37489 ` 1137` hoelzl@50526 ` 1138` ```lemma Cart_1:"(1::real^'n) = \Basis" ``` hoelzl@50526 ` 1139` ``` using const_vector_cart[of 1] by (simp add: one_vec_def) ``` hoelzl@37489 ` 1140` hoelzl@37489 ` 1141` ```declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp] ``` hoelzl@37489 ` 1142` ```declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp] ``` hoelzl@37489 ` 1143` hoelzl@50526 ` 1144` ```lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component less_eq_vec_def vec_lambda_beta vector_uminus_component ``` hoelzl@37489 ` 1145` hoelzl@37489 ` 1146` ```lemma convex_box_cart: ``` hoelzl@37489 ` 1147` ``` assumes "\i. convex {x. P i x}" ``` hoelzl@37489 ` 1148` ``` shows "convex {x. \i. P i (x\$i)}" ``` hoelzl@37489 ` 1149` ``` using assms unfolding convex_def by auto ``` hoelzl@37489 ` 1150` hoelzl@37489 ` 1151` ```lemma convex_positive_orthant_cart: "convex {x::real^'n. (\i. 0 \ x\$i)}" ``` hoelzl@37489 ` 1152` ``` by (rule convex_box_cart) (simp add: atLeast_def[symmetric] convex_real_interval) ``` hoelzl@37489 ` 1153` hoelzl@37489 ` 1154` ```lemma unit_interval_convex_hull_cart: ``` hoelzl@37489 ` 1155` ``` "{0::real^'n .. 1} = convex hull {x. \i. (x\$i = 0) \ (x\$i = 1)}" (is "?int = convex hull ?points") ``` hoelzl@37489 ` 1156` ``` unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"] ``` hoelzl@50526 ` 1157` ``` by (rule arg_cong[where f="\x. convex hull x"]) (simp add: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 1158` hoelzl@37489 ` 1159` ```lemma cube_convex_hull_cart: ``` wenzelm@49644 ` 1160` ``` assumes "0 < d" ``` wenzelm@49644 ` 1161` ``` obtains s::"(real^'n) set" ``` wenzelm@49644 ` 1162` ``` where "finite s" "{x - (\ i. d) .. x + (\ i. d)} = convex hull s" ``` wenzelm@49644 ` 1163` ```proof - ``` hoelzl@50526 ` 1164` ``` from cube_convex_hull [OF assms, of x] guess s . ``` hoelzl@50526 ` 1165` ``` with that[of s] show thesis by (simp add: const_vector_cart) ``` hoelzl@37489 ` 1166` ```qed ``` hoelzl@37489 ` 1167` hoelzl@37489 ` 1168` hoelzl@37489 ` 1169` ```subsection "Derivative" ``` hoelzl@37489 ` 1170` wenzelm@49644 ` 1171` ```lemma differentiable_at_imp_differentiable_on: ``` wenzelm@49644 ` 1172` ``` "(\x\(s::(real^'n) set). f differentiable at x) \ f differentiable_on s" ``` hoelzl@37489 ` 1173` ``` unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI) ``` hoelzl@37489 ` 1174` hoelzl@37489 ` 1175` ```definition "jacobian f net = matrix(frechet_derivative f net)" ``` hoelzl@37489 ` 1176` wenzelm@49644 ` 1177` ```lemma jacobian_works: ``` wenzelm@49644 ` 1178` ``` "(f::(real^'a) \ (real^'b)) differentiable net \ ``` wenzelm@49644 ` 1179` ``` (f has_derivative (\h. (jacobian f net) *v h)) net" ``` wenzelm@49644 ` 1180` ``` apply rule ``` wenzelm@49644 ` 1181` ``` unfolding jacobian_def ``` wenzelm@49644 ` 1182` ``` apply (simp only: matrix_works[OF linear_frechet_derivative]) defer ``` wenzelm@49644 ` 1183` ``` apply (rule differentiableI) ``` wenzelm@49644 ` 1184` ``` apply assumption ``` wenzelm@49644 ` 1185` ``` unfolding frechet_derivative_works ``` wenzelm@49644 ` 1186` ``` apply assumption ``` wenzelm@49644 ` 1187` ``` done ``` hoelzl@37489 ` 1188` hoelzl@37489 ` 1189` wenzelm@49644 ` 1190` ```subsection {* Component of the differential must be zero if it exists at a local ``` wenzelm@49644 ` 1191` ``` maximum or minimum for that corresponding component. *} ``` hoelzl@37489 ` 1192` hoelzl@50526 ` 1193` ```lemma differential_zero_maxmin_cart: ``` wenzelm@49644 ` 1194` ``` fixes f::"real^'a \ real^'b" ``` wenzelm@49644 ` 1195` ``` assumes "0 < e" "((\y \ ball x e. (f y)\$k \ (f x)\$k) \ (\y\ball x e. (f x)\$k \ (f y)\$k))" ``` hoelzl@50526 ` 1196` ``` "f differentiable (at x)" ``` hoelzl@50526 ` 1197` ``` shows "jacobian f (at x) \$ k = 0" ``` hoelzl@50526 ` 1198` ``` using differential_zero_maxmin_component[of "axis k 1" e x f] assms ``` hoelzl@50526 ` 1199` ``` vector_cart[of "\j. frechet_derivative f (at x) j \$ k"] ``` hoelzl@50526 ` 1200` ``` by (simp add: Basis_vec_def axis_eq_axis inner_axis jacobian_def matrix_def) ``` wenzelm@49644 ` 1201` hoelzl@37494 ` 1202` ```subsection {* Lemmas for working on @{typ "real^1"} *} ``` hoelzl@37489 ` 1203` hoelzl@37489 ` 1204` ```lemma forall_1[simp]: "(\i::1. P i) \ P 1" ``` wenzelm@49644 ` 1205` ``` by (metis (full_types) num1_eq_iff) ``` hoelzl@37489 ` 1206` hoelzl@37489 ` 1207` ```lemma ex_1[simp]: "(\x::1. P x) \ P 1" ``` wenzelm@49644 ` 1208` ``` by auto (metis (full_types) num1_eq_iff) ``` hoelzl@37489 ` 1209` hoelzl@37489 ` 1210` ```lemma exhaust_2: ``` wenzelm@49644 ` 1211` ``` fixes x :: 2 ``` wenzelm@49644 ` 1212` ``` shows "x = 1 \ x = 2" ``` hoelzl@37489 ` 1213` ```proof (induct x) ``` hoelzl@37489 ` 1214` ``` case (of_int z) ``` hoelzl@37489 ` 1215` ``` then have "0 <= z" and "z < 2" by simp_all ``` hoelzl@37489 ` 1216` ``` then have "z = 0 | z = 1" by arith ``` hoelzl@37489 ` 1217` ``` then show ?case by auto ``` hoelzl@37489 ` 1218` ```qed ``` hoelzl@37489 ` 1219` hoelzl@37489 ` 1220` ```lemma forall_2: "(\i::2. P i) \ P 1 \ P 2" ``` hoelzl@37489 ` 1221` ``` by (metis exhaust_2) ``` hoelzl@37489 ` 1222` hoelzl@37489 ` 1223` ```lemma exhaust_3: ``` wenzelm@49644 ` 1224` ``` fixes x :: 3 ``` wenzelm@49644 ` 1225` ``` shows "x = 1 \ x = 2 \ x = 3" ``` hoelzl@37489 ` 1226` ```proof (induct x) ``` hoelzl@37489 ` 1227` ``` case (of_int z) ``` hoelzl@37489 ` 1228` ``` then have "0 <= z" and "z < 3" by simp_all ``` hoelzl@37489 ` 1229` ``` then have "z = 0 \ z = 1 \ z = 2" by arith ``` hoelzl@37489 ` 1230` ``` then show ?case by auto ``` hoelzl@37489 ` 1231` ```qed ``` hoelzl@37489 ` 1232` hoelzl@37489 ` 1233` ```lemma forall_3: "(\i::3. P i) \ P 1 \ P 2 \ P 3" ``` hoelzl@37489 ` 1234` ``` by (metis exhaust_3) ``` hoelzl@37489 ` 1235` hoelzl@37489 ` 1236` ```lemma UNIV_1 [simp]: "UNIV = {1::1}" ``` hoelzl@37489 ` 1237` ``` by (auto simp add: num1_eq_iff) ``` hoelzl@37489 ` 1238` hoelzl@37489 ` 1239` ```lemma UNIV_2: "UNIV = {1::2, 2::2}" ``` hoelzl@37489 ` 1240` ``` using exhaust_2 by auto ``` hoelzl@37489 ` 1241` hoelzl@37489 ` 1242` ```lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" ``` hoelzl@37489 ` 1243` ``` using exhaust_3 by auto ``` hoelzl@37489 ` 1244` hoelzl@37489 ` 1245` ```lemma setsum_1: "setsum f (UNIV::1 set) = f 1" ``` hoelzl@37489 ` 1246` ``` unfolding UNIV_1 by simp ``` hoelzl@37489 ` 1247` hoelzl@37489 ` 1248` ```lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2" ``` hoelzl@37489 ` 1249` ``` unfolding UNIV_2 by simp ``` hoelzl@37489 ` 1250` hoelzl@37489 ` 1251` ```lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3" ``` hoelzl@37489 ` 1252` ``` unfolding UNIV_3 by (simp add: add_ac) ``` hoelzl@37489 ` 1253` wenzelm@49644 ` 1254` ```instantiation num1 :: cart_one ``` wenzelm@49644 ` 1255` ```begin ``` wenzelm@49644 ` 1256` wenzelm@49644 ` 1257` ```instance ``` wenzelm@49644 ` 1258` ```proof ``` hoelzl@37489 ` 1259` ``` show "CARD(1) = Suc 0" by auto ``` wenzelm@49644 ` 1260` ```qed ``` wenzelm@49644 ` 1261` wenzelm@49644 ` 1262` ```end ``` hoelzl@37489 ` 1263` hoelzl@37489 ` 1264` ```subsection{* The collapse of the general concepts to dimension one. *} ``` hoelzl@37489 ` 1265` hoelzl@37489 ` 1266` ```lemma vector_one: "(x::'a ^1) = (\ i. (x\$1))" ``` huffman@44136 ` 1267` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 1268` hoelzl@37489 ` 1269` ```lemma forall_one: "(\(x::'a ^1). P x) \ (\x. P(\ i. x))" ``` hoelzl@37489 ` 1270` ``` apply auto ``` hoelzl@37489 ` 1271` ``` apply (erule_tac x= "x\$1" in allE) ``` hoelzl@37489 ` 1272` ``` apply (simp only: vector_one[symmetric]) ``` hoelzl@37489 ` 1273` ``` done ``` hoelzl@37489 ` 1274` hoelzl@37489 ` 1275` ```lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)" ``` huffman@44136 ` 1276` ``` by (simp add: norm_vec_def) ``` hoelzl@37489 ` 1277` hoelzl@37489 ` 1278` ```lemma norm_real: "norm(x::real ^ 1) = abs(x\$1)" ``` hoelzl@37489 ` 1279` ``` by (simp add: norm_vector_1) ``` hoelzl@37489 ` 1280` hoelzl@37489 ` 1281` ```lemma dist_real: "dist(x::real ^ 1) y = abs((x\$1) - (y\$1))" ``` hoelzl@37489 ` 1282` ``` by (auto simp add: norm_real dist_norm) ``` hoelzl@37489 ` 1283` wenzelm@49644 ` 1284` hoelzl@37489 ` 1285` ```subsection{* Explicit vector construction from lists. *} ``` hoelzl@37489 ` 1286` hoelzl@43995 ` 1287` ```definition "vector l = (\ i. foldr (\x f n. fun_upd (f (n+1)) n x) l (\n x. 0) 1 i)" ``` hoelzl@37489 ` 1288` hoelzl@37489 ` 1289` ```lemma vector_1: "(vector[x]) \$1 = x" ``` hoelzl@37489 ` 1290` ``` unfolding vector_def by simp ``` hoelzl@37489 ` 1291` hoelzl@37489 ` 1292` ```lemma vector_2: ``` hoelzl@37489 ` 1293` ``` "(vector[x,y]) \$1 = x" ``` hoelzl@37489 ` 1294` ``` "(vector[x,y] :: 'a^2)\$2 = (y::'a::zero)" ``` hoelzl@37489 ` 1295` ``` unfolding vector_def by simp_all ``` hoelzl@37489 ` 1296` hoelzl@37489 ` 1297` ```lemma vector_3: ``` hoelzl@37489 ` 1298` ``` "(vector [x,y,z] ::('a::zero)^3)\$1 = x" ``` hoelzl@37489 ` 1299` ``` "(vector [x,y,z] ::('a::zero)^3)\$2 = y" ``` hoelzl@37489 ` 1300` ``` "(vector [x,y,z] ::('a::zero)^3)\$3 = z" ``` hoelzl@37489 ` 1301` ``` unfolding vector_def by simp_all ``` hoelzl@37489 ` 1302` hoelzl@37489 ` 1303` ```lemma forall_vector_1: "(\v::'a::zero^1. P v) \ (\x. P(vector[x]))" ``` hoelzl@37489 ` 1304` ``` apply auto ``` hoelzl@37489 ` 1305` ``` apply (erule_tac x="v\$1" in allE) ``` hoelzl@37489 ` 1306` ``` apply (subgoal_tac "vector [v\$1] = v") ``` hoelzl@37489 ` 1307` ``` apply simp ``` hoelzl@37489 ` 1308` ``` apply (vector vector_def) ``` hoelzl@37489 ` 1309` ``` apply simp ``` hoelzl@37489 ` 1310` ``` done ``` hoelzl@37489 ` 1311` hoelzl@37489 ` 1312` ```lemma forall_vector_2: "(\v::'a::zero^2. P v) \ (\x y. P(vector[x, y]))" ``` hoelzl@37489 ` 1313` ``` apply auto ``` hoelzl@37489 ` 1314` ``` apply (erule_tac x="v\$1" in allE) ``` hoelzl@37489 ` 1315` ``` apply (erule_tac x="v\$2" in allE) ``` hoelzl@37489 ` 1316` ``` apply (subgoal_tac "vector [v\$1, v\$2] = v") ``` hoelzl@37489 ` 1317` ``` apply simp ``` hoelzl@37489 ` 1318` ``` apply (vector vector_def) ``` hoelzl@37489 ` 1319` ``` apply (simp add: forall_2) ``` hoelzl@37489 ` 1320` ``` done ``` hoelzl@37489 ` 1321` hoelzl@37489 ` 1322` ```lemma forall_vector_3: "(\v::'a::zero^3. P v) \ (\x y z. P(vector[x, y, z]))" ``` hoelzl@37489 ` 1323` ``` apply auto ``` hoelzl@37489 ` 1324` ``` apply (erule_tac x="v\$1" in allE) ``` hoelzl@37489 ` 1325` ``` apply (erule_tac x="v\$2" in allE) ``` hoelzl@37489 ` 1326` ``` apply (erule_tac x="v\$3" in allE) ``` hoelzl@37489 ` 1327` ``` apply (subgoal_tac "vector [v\$1, v\$2, v\$3] = v") ``` hoelzl@37489 ` 1328` ``` apply simp ``` hoelzl@37489 ` 1329` ``` apply (vector vector_def) ``` hoelzl@37489 ` 1330` ``` apply (simp add: forall_3) ``` hoelzl@37489 ` 1331` ``` done ``` hoelzl@37489 ` 1332` hoelzl@37489 ` 1333` ```lemma bounded_linear_component_cart[intro]: "bounded_linear (\x::real^'n. x \$ k)" ``` wenzelm@49644 ` 1334` ``` apply (rule bounded_linearI[where K=1]) ``` hoelzl@37489 ` 1335` ``` using component_le_norm_cart[of _ k] unfolding real_norm_def by auto ``` hoelzl@37489 ` 1336` wenzelm@49644 ` 1337` ```lemma integral_component_eq_cart[simp]: ``` wenzelm@49644 ` 1338` ``` fixes f :: "'n::ordered_euclidean_space \ real^'m" ``` wenzelm@49644 ` 1339` ``` assumes "f integrable_on s" ``` wenzelm@49644 ` 1340` ``` shows "integral s (\x. f x \$ k) = integral s f \$ k" ``` hoelzl@37489 ` 1341` ``` using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] . ``` hoelzl@37489 ` 1342` hoelzl@37489 ` 1343` ```lemma interval_split_cart: ``` hoelzl@37489 ` 1344` ``` "{a..b::real^'n} \ {x. x\$k \ c} = {a .. (\ i. if i = k then min (b\$k) c else b\$i)}" ``` hoelzl@37489 ` 1345` ``` "{a..b} \ {x. x\$k \ c} = {(\ i. if i = k then max (a\$k) c else a\$i) .. b}" ``` wenzelm@49644 ` 1346` ``` apply (rule_tac[!] set_eqI) ``` wenzelm@49644 ` 1347` ``` unfolding Int_iff mem_interval_cart mem_Collect_eq ``` wenzelm@49644 ` 1348` ``` unfolding vec_lambda_beta ``` wenzelm@49644 ` 1349` ``` by auto ``` hoelzl@37489 ` 1350` hoelzl@50526 ` 1351` ```lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\i. a\$i < b\$i \ u\$i < v\$i" ``` hoelzl@50526 ` 1352` ``` shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x" ``` hoelzl@50526 ` 1353` ``` using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 1354` hoelzl@37489 ` 1355` ```end ```