src/HOL/Analysis/Cartesian_Euclidean_Space.thy
 author paulson Wed May 02 23:32:47 2018 +0100 (13 months ago) changeset 68069 36209dfb981e parent 68062 ee88c0fccbae child 68073 fad29d2a17a5 permissions -rw-r--r--
tidying up and using real induction methods
 lp15@68038 ` 1` ```(* Title: HOL/Analysis/Cartesian_Euclidean_Space.thy ``` lp15@68043 ` 2` ``` Some material by Jose Divasón, Tim Makarios and L C Paulson ``` lp15@68038 ` 3` ```*) ``` lp15@68038 ` 4` nipkow@67968 ` 5` ```section \Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\ ``` hoelzl@37489 ` 6` hoelzl@37489 ` 7` ```theory Cartesian_Euclidean_Space ``` immler@67685 ` 8` ```imports Finite_Cartesian_Product Derivative ``` hoelzl@37489 ` 9` ```begin ``` hoelzl@37489 ` 10` lp15@67982 ` 11` ```lemma norm_le_componentwise: ``` lp15@67982 ` 12` ``` "(\b. b \ Basis \ abs(x \ b) \ abs(y \ b)) \ norm x \ norm y" ``` lp15@67982 ` 13` ``` by (auto simp: norm_le euclidean_inner [of x x] euclidean_inner [of y y] abs_le_square_iff power2_eq_square intro!: sum_mono) ``` lp15@67982 ` 14` lp15@67982 ` 15` ```lemma norm_le_componentwise_cart: ``` lp15@67982 ` 16` ``` fixes x :: "real^'n" ``` lp15@67982 ` 17` ``` shows "(\i. abs(x\$i) \ abs(y\$i)) \ norm x \ norm y" ``` lp15@67982 ` 18` ``` unfolding cart_eq_inner_axis ``` lp15@67982 ` 19` ``` by (rule norm_le_componentwise) (metis axis_index) ``` lp15@67982 ` 20` ``` ``` lp15@63016 ` 21` ```lemma subspace_special_hyperplane: "subspace {x. x \$ k = 0}" ``` lp15@63016 ` 22` ``` by (simp add: subspace_def) ``` lp15@63016 ` 23` nipkow@64267 ` 24` ```lemma sum_mult_product: ``` nipkow@64267 ` 25` ``` "sum h {..i\{..j\{..j. j + i * B) {..j. j + i * B) ` {.. {i * B.. (\j. j + i * B) ` {..Basic componentwise operations on vectors\ ``` hoelzl@37489 ` 39` huffman@44136 ` 40` ```instantiation vec :: (times, finite) times ``` hoelzl@37489 ` 41` ```begin ``` wenzelm@49644 ` 42` nipkow@67399 ` 43` ```definition "( * ) \ (\ x y. (\ i. (x\$i) * (y\$i)))" ``` wenzelm@49644 ` 44` ```instance .. ``` wenzelm@49644 ` 45` hoelzl@37489 ` 46` ```end ``` hoelzl@37489 ` 47` huffman@44136 ` 48` ```instantiation vec :: (one, finite) one ``` hoelzl@37489 ` 49` ```begin ``` wenzelm@49644 ` 50` wenzelm@49644 ` 51` ```definition "1 \ (\ i. 1)" ``` wenzelm@49644 ` 52` ```instance .. ``` wenzelm@49644 ` 53` hoelzl@37489 ` 54` ```end ``` hoelzl@37489 ` 55` huffman@44136 ` 56` ```instantiation vec :: (ord, finite) ord ``` hoelzl@37489 ` 57` ```begin ``` wenzelm@49644 ` 58` wenzelm@49644 ` 59` ```definition "x \ y \ (\i. x\$i \ y\$i)" ``` immler@54776 ` 60` ```definition "x < (y::'a^'b) \ x \ y \ \ y \ x" ``` wenzelm@49644 ` 61` ```instance .. ``` wenzelm@49644 ` 62` hoelzl@37489 ` 63` ```end ``` hoelzl@37489 ` 64` wenzelm@60420 ` 65` ```text\The ordering on one-dimensional vectors is linear.\ ``` hoelzl@37489 ` 66` wenzelm@49197 ` 67` ```class cart_one = ``` wenzelm@61076 ` 68` ``` assumes UNIV_one: "card (UNIV :: 'a set) = Suc 0" ``` hoelzl@37489 ` 69` ```begin ``` wenzelm@49197 ` 70` wenzelm@49197 ` 71` ```subclass finite ``` wenzelm@49197 ` 72` ```proof ``` wenzelm@49197 ` 73` ``` from UNIV_one show "finite (UNIV :: 'a set)" ``` wenzelm@49197 ` 74` ``` by (auto intro!: card_ge_0_finite) ``` wenzelm@49197 ` 75` ```qed ``` wenzelm@49197 ` 76` hoelzl@37489 ` 77` ```end ``` hoelzl@37489 ` 78` immler@54776 ` 79` ```instance vec:: (order, finite) order ``` wenzelm@61169 ` 80` ``` by standard (auto simp: less_eq_vec_def less_vec_def vec_eq_iff ``` immler@54776 ` 81` ``` intro: order.trans order.antisym order.strict_implies_order) ``` wenzelm@49197 ` 82` immler@54776 ` 83` ```instance vec :: (linorder, cart_one) linorder ``` wenzelm@49197 ` 84` ```proof ``` wenzelm@49197 ` 85` ``` obtain a :: 'b where all: "\P. (\i. P i) \ P a" ``` wenzelm@49197 ` 86` ``` proof - ``` wenzelm@49197 ` 87` ``` have "card (UNIV :: 'b set) = Suc 0" by (rule UNIV_one) ``` wenzelm@49197 ` 88` ``` then obtain b :: 'b where "UNIV = {b}" by (auto iff: card_Suc_eq) ``` wenzelm@49197 ` 89` ``` then have "\P. (\i\UNIV. P i) \ P b" by auto ``` wenzelm@49197 ` 90` ``` then show thesis by (auto intro: that) ``` wenzelm@49197 ` 91` ``` qed ``` immler@54776 ` 92` ``` fix x y :: "'a^'b::cart_one" ``` wenzelm@49197 ` 93` ``` note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps ``` immler@54776 ` 94` ``` show "x \ y \ y \ x" by auto ``` wenzelm@49197 ` 95` ```qed ``` wenzelm@49197 ` 96` wenzelm@60420 ` 97` ```text\Constant Vectors\ ``` hoelzl@37489 ` 98` hoelzl@37489 ` 99` ```definition "vec x = (\ i. x)" ``` hoelzl@37489 ` 100` immler@56188 ` 101` ```lemma interval_cbox_cart: "{a::real^'n..b} = cbox a b" ``` immler@56188 ` 102` ``` by (auto simp add: less_eq_vec_def mem_box Basis_vec_def inner_axis) ``` immler@56188 ` 103` wenzelm@60420 ` 104` ```text\Also the scalar-vector multiplication.\ ``` hoelzl@37489 ` 105` hoelzl@37489 ` 106` ```definition vector_scalar_mult:: "'a::times \ 'a ^ 'n \ 'a ^ 'n" (infixl "*s" 70) ``` hoelzl@37489 ` 107` ``` where "c *s x = (\ i. c * (x\$i))" ``` hoelzl@37489 ` 108` wenzelm@49644 ` 109` nipkow@67968 ` 110` ```subsection \A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\ ``` hoelzl@37489 ` 111` nipkow@64267 ` 112` ```lemma sum_cong_aux: ``` nipkow@64267 ` 113` ``` "(\x. x \ A \ f x = g x) \ sum f A = sum g A" ``` nipkow@64267 ` 114` ``` by (auto intro: sum.cong) ``` haftmann@57418 ` 115` nipkow@64267 ` 116` ```hide_fact (open) sum_cong_aux ``` haftmann@57418 ` 117` wenzelm@60420 ` 118` ```method_setup vector = \ ``` hoelzl@37489 ` 119` ```let ``` wenzelm@51717 ` 120` ``` val ss1 = ``` wenzelm@51717 ` 121` ``` simpset_of (put_simpset HOL_basic_ss @{context} ``` nipkow@64267 ` 122` ``` addsimps [@{thm sum.distrib} RS sym, ``` nipkow@64267 ` 123` ``` @{thm sum_subtractf} RS sym, @{thm sum_distrib_left}, ``` nipkow@64267 ` 124` ``` @{thm sum_distrib_right}, @{thm sum_negf} RS sym]) ``` wenzelm@51717 ` 125` ``` val ss2 = ``` wenzelm@51717 ` 126` ``` simpset_of (@{context} addsimps ``` huffman@44136 ` 127` ``` [@{thm plus_vec_def}, @{thm times_vec_def}, ``` huffman@44136 ` 128` ``` @{thm minus_vec_def}, @{thm uminus_vec_def}, ``` huffman@44136 ` 129` ``` @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def}, ``` huffman@44136 ` 130` ``` @{thm scaleR_vec_def}, ``` wenzelm@51717 ` 131` ``` @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}]) ``` wenzelm@51717 ` 132` ``` fun vector_arith_tac ctxt ths = ``` wenzelm@51717 ` 133` ``` simp_tac (put_simpset ss1 ctxt) ``` nipkow@64267 ` 134` ``` THEN' (fn i => resolve_tac ctxt @{thms Cartesian_Euclidean_Space.sum_cong_aux} i ``` nipkow@64267 ` 135` ``` ORELSE resolve_tac ctxt @{thms sum.neutral} i ``` wenzelm@51717 ` 136` ``` ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i) ``` wenzelm@49644 ` 137` ``` (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) ``` wenzelm@51717 ` 138` ``` THEN' asm_full_simp_tac (put_simpset ss2 ctxt addsimps ths) ``` wenzelm@49644 ` 139` ```in ``` wenzelm@51717 ` 140` ``` Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (vector_arith_tac ctxt ths)) ``` wenzelm@49644 ` 141` ```end ``` wenzelm@60420 ` 142` ```\ "lift trivial vector statements to real arith statements" ``` hoelzl@37489 ` 143` wenzelm@57865 ` 144` ```lemma vec_0[simp]: "vec 0 = 0" by vector ``` wenzelm@57865 ` 145` ```lemma vec_1[simp]: "vec 1 = 1" by vector ``` hoelzl@37489 ` 146` hoelzl@37489 ` 147` ```lemma vec_inj[simp]: "vec x = vec y \ x = y" by vector ``` hoelzl@37489 ` 148` hoelzl@37489 ` 149` ```lemma vec_in_image_vec: "vec x \ (vec ` S) \ x \ S" by auto ``` hoelzl@37489 ` 150` wenzelm@57865 ` 151` ```lemma vec_add: "vec(x + y) = vec x + vec y" by vector ``` wenzelm@57865 ` 152` ```lemma vec_sub: "vec(x - y) = vec x - vec y" by vector ``` wenzelm@57865 ` 153` ```lemma vec_cmul: "vec(c * x) = c *s vec x " by vector ``` wenzelm@57865 ` 154` ```lemma vec_neg: "vec(- x) = - vec x " by vector ``` hoelzl@37489 ` 155` lp15@67979 ` 156` ```lemma vec_scaleR: "vec(c * x) = c *\<^sub>R vec x" ``` lp15@67979 ` 157` ``` by vector ``` lp15@67979 ` 158` nipkow@64267 ` 159` ```lemma vec_sum: ``` wenzelm@49644 ` 160` ``` assumes "finite S" ``` nipkow@64267 ` 161` ``` shows "vec(sum f S) = sum (vec \ f) S" ``` wenzelm@49644 ` 162` ``` using assms ``` wenzelm@49644 ` 163` ```proof induct ``` wenzelm@49644 ` 164` ``` case empty ``` wenzelm@49644 ` 165` ``` then show ?case by simp ``` wenzelm@49644 ` 166` ```next ``` wenzelm@49644 ` 167` ``` case insert ``` wenzelm@49644 ` 168` ``` then show ?case by (auto simp add: vec_add) ``` wenzelm@49644 ` 169` ```qed ``` hoelzl@37489 ` 170` wenzelm@60420 ` 171` ```text\Obvious "component-pushing".\ ``` hoelzl@37489 ` 172` hoelzl@37489 ` 173` ```lemma vec_component [simp]: "vec x \$ i = x" ``` wenzelm@57865 ` 174` ``` by vector ``` hoelzl@37489 ` 175` hoelzl@37489 ` 176` ```lemma vector_mult_component [simp]: "(x * y)\$i = x\$i * y\$i" ``` hoelzl@37489 ` 177` ``` by vector ``` hoelzl@37489 ` 178` hoelzl@37489 ` 179` ```lemma vector_smult_component [simp]: "(c *s y)\$i = c * (y\$i)" ``` hoelzl@37489 ` 180` ``` by vector ``` hoelzl@37489 ` 181` hoelzl@37489 ` 182` ```lemma cond_component: "(if b then x else y)\$i = (if b then x\$i else y\$i)" by vector ``` hoelzl@37489 ` 183` hoelzl@37489 ` 184` ```lemmas vector_component = ``` hoelzl@37489 ` 185` ``` vec_component vector_add_component vector_mult_component ``` hoelzl@37489 ` 186` ``` vector_smult_component vector_minus_component vector_uminus_component ``` hoelzl@37489 ` 187` ``` vector_scaleR_component cond_component ``` hoelzl@37489 ` 188` wenzelm@49644 ` 189` nipkow@67968 ` 190` ```subsection \Some frequently useful arithmetic lemmas over vectors\ ``` hoelzl@37489 ` 191` huffman@44136 ` 192` ```instance vec :: (semigroup_mult, finite) semigroup_mult ``` wenzelm@61169 ` 193` ``` by standard (vector mult.assoc) ``` hoelzl@37489 ` 194` huffman@44136 ` 195` ```instance vec :: (monoid_mult, finite) monoid_mult ``` wenzelm@61169 ` 196` ``` by standard vector+ ``` hoelzl@37489 ` 197` huffman@44136 ` 198` ```instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult ``` wenzelm@61169 ` 199` ``` by standard (vector mult.commute) ``` hoelzl@37489 ` 200` huffman@44136 ` 201` ```instance vec :: (comm_monoid_mult, finite) comm_monoid_mult ``` wenzelm@61169 ` 202` ``` by standard vector ``` hoelzl@37489 ` 203` huffman@44136 ` 204` ```instance vec :: (semiring, finite) semiring ``` wenzelm@61169 ` 205` ``` by standard (vector field_simps)+ ``` hoelzl@37489 ` 206` huffman@44136 ` 207` ```instance vec :: (semiring_0, finite) semiring_0 ``` wenzelm@61169 ` 208` ``` by standard (vector field_simps)+ ``` huffman@44136 ` 209` ```instance vec :: (semiring_1, finite) semiring_1 ``` wenzelm@61169 ` 210` ``` by standard vector ``` huffman@44136 ` 211` ```instance vec :: (comm_semiring, finite) comm_semiring ``` wenzelm@61169 ` 212` ``` by standard (vector field_simps)+ ``` hoelzl@37489 ` 213` huffman@44136 ` 214` ```instance vec :: (comm_semiring_0, finite) comm_semiring_0 .. ``` huffman@44136 ` 215` ```instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. ``` huffman@44136 ` 216` ```instance vec :: (semiring_0_cancel, finite) semiring_0_cancel .. ``` huffman@44136 ` 217` ```instance vec :: (comm_semiring_0_cancel, finite) comm_semiring_0_cancel .. ``` huffman@44136 ` 218` ```instance vec :: (ring, finite) ring .. ``` huffman@44136 ` 219` ```instance vec :: (semiring_1_cancel, finite) semiring_1_cancel .. ``` huffman@44136 ` 220` ```instance vec :: (comm_semiring_1, finite) comm_semiring_1 .. ``` hoelzl@37489 ` 221` huffman@44136 ` 222` ```instance vec :: (ring_1, finite) ring_1 .. ``` hoelzl@37489 ` 223` huffman@44136 ` 224` ```instance vec :: (real_algebra, finite) real_algebra ``` wenzelm@61169 ` 225` ``` by standard (simp_all add: vec_eq_iff) ``` hoelzl@37489 ` 226` huffman@44136 ` 227` ```instance vec :: (real_algebra_1, finite) real_algebra_1 .. ``` hoelzl@37489 ` 228` wenzelm@49644 ` 229` ```lemma of_nat_index: "(of_nat n :: 'a::semiring_1 ^'n)\$i = of_nat n" ``` wenzelm@49644 ` 230` ```proof (induct n) ``` wenzelm@49644 ` 231` ``` case 0 ``` wenzelm@49644 ` 232` ``` then show ?case by vector ``` wenzelm@49644 ` 233` ```next ``` wenzelm@49644 ` 234` ``` case Suc ``` wenzelm@49644 ` 235` ``` then show ?case by vector ``` wenzelm@49644 ` 236` ```qed ``` hoelzl@37489 ` 237` haftmann@54489 ` 238` ```lemma one_index [simp]: "(1 :: 'a :: one ^ 'n) \$ i = 1" ``` haftmann@54489 ` 239` ``` by vector ``` haftmann@54489 ` 240` haftmann@54489 ` 241` ```lemma neg_one_index [simp]: "(- 1 :: 'a :: {one, uminus} ^ 'n) \$ i = - 1" ``` wenzelm@49644 ` 242` ``` by vector ``` hoelzl@37489 ` 243` huffman@44136 ` 244` ```instance vec :: (semiring_char_0, finite) semiring_char_0 ``` haftmann@38621 ` 245` ```proof ``` haftmann@38621 ` 246` ``` fix m n :: nat ``` haftmann@38621 ` 247` ``` show "inj (of_nat :: nat \ 'a ^ 'b)" ``` huffman@44136 ` 248` ``` by (auto intro!: injI simp add: vec_eq_iff of_nat_index) ``` hoelzl@37489 ` 249` ```qed ``` hoelzl@37489 ` 250` huffman@47108 ` 251` ```instance vec :: (numeral, finite) numeral .. ``` huffman@47108 ` 252` ```instance vec :: (semiring_numeral, finite) semiring_numeral .. ``` huffman@47108 ` 253` huffman@47108 ` 254` ```lemma numeral_index [simp]: "numeral w \$ i = numeral w" ``` wenzelm@49644 ` 255` ``` by (induct w) (simp_all only: numeral.simps vector_add_component one_index) ``` huffman@47108 ` 256` haftmann@54489 ` 257` ```lemma neg_numeral_index [simp]: "- numeral w \$ i = - numeral w" ``` haftmann@54489 ` 258` ``` by (simp only: vector_uminus_component numeral_index) ``` huffman@47108 ` 259` huffman@44136 ` 260` ```instance vec :: (comm_ring_1, finite) comm_ring_1 .. ``` huffman@44136 ` 261` ```instance vec :: (ring_char_0, finite) ring_char_0 .. ``` hoelzl@37489 ` 262` hoelzl@37489 ` 263` ```lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" ``` haftmann@57512 ` 264` ``` by (vector mult.assoc) ``` hoelzl@37489 ` 265` ```lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x" ``` hoelzl@37489 ` 266` ``` by (vector field_simps) ``` hoelzl@37489 ` 267` ```lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y" ``` hoelzl@37489 ` 268` ``` by (vector field_simps) ``` hoelzl@37489 ` 269` ```lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector ``` hoelzl@37489 ` 270` ```lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector ``` hoelzl@37489 ` 271` ```lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y" ``` hoelzl@37489 ` 272` ``` by (vector field_simps) ``` hoelzl@37489 ` 273` ```lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector ``` hoelzl@37489 ` 274` ```lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector ``` huffman@47108 ` 275` ```lemma vector_sneg_minus1: "-x = (-1::'a::ring_1) *s x" by vector ``` hoelzl@37489 ` 276` ```lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector ``` hoelzl@37489 ` 277` ```lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x" ``` hoelzl@37489 ` 278` ``` by (vector field_simps) ``` hoelzl@37489 ` 279` hoelzl@37489 ` 280` ```lemma vec_eq[simp]: "(vec m = vec n) \ (m = n)" ``` huffman@44136 ` 281` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 282` lp15@67979 ` 283` ```lemma linear_vec [simp]: "linear vec" ``` lp15@67979 ` 284` ``` by (simp add: linearI vec_add vec_eq_iff) ``` lp15@67979 ` 285` lp15@67979 ` 286` ```lemma differentiable_vec: ``` lp15@67979 ` 287` ``` fixes S :: "'a::euclidean_space set" ``` lp15@67979 ` 288` ``` shows "vec differentiable_on S" ``` lp15@67979 ` 289` ``` by (simp add: linear_linear bounded_linear_imp_differentiable_on) ``` lp15@67979 ` 290` lp15@67979 ` 291` ```lemma continuous_vec [continuous_intros]: ``` lp15@67979 ` 292` ``` fixes x :: "'a::euclidean_space" ``` lp15@67979 ` 293` ``` shows "isCont vec x" ``` lp15@67979 ` 294` ``` apply (clarsimp simp add: continuous_def LIM_def dist_vec_def L2_set_def) ``` lp15@67979 ` 295` ``` apply (rule_tac x="r / sqrt (real CARD('b))" in exI) ``` lp15@67979 ` 296` ``` by (simp add: mult.commute pos_less_divide_eq real_sqrt_mult) ``` lp15@67979 ` 297` lp15@67979 ` 298` ```lemma box_vec_eq_empty [simp]: ``` lp15@67979 ` 299` ``` shows "cbox (vec a) (vec b) = {} \ cbox a b = {}" ``` lp15@67979 ` 300` ``` "box (vec a) (vec b) = {} \ box a b = {}" ``` lp15@67979 ` 301` ``` by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis) ``` lp15@67979 ` 302` lp15@67683 ` 303` ```lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1" ``` lp15@67683 ` 304` ``` by (simp add: inner_axis' norm_eq_1) ``` lp15@67683 ` 305` hoelzl@37489 ` 306` ```lemma vector_mul_eq_0[simp]: "(a *s x = 0) \ a = (0::'a::idom) \ x = 0" ``` hoelzl@37489 ` 307` ``` by vector ``` lp15@67683 ` 308` hoelzl@37489 ` 309` ```lemma vector_mul_lcancel[simp]: "a *s x = a *s y \ a = (0::real) \ x = y" ``` hoelzl@37489 ` 310` ``` by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) ``` lp15@67683 ` 311` hoelzl@37489 ` 312` ```lemma vector_mul_rcancel[simp]: "a *s x = b *s x \ (a::real) = b \ x = 0" ``` hoelzl@37489 ` 313` ``` by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) ``` lp15@67683 ` 314` lp15@67979 ` 315` ```lemma component_le_norm_cart: "\x\$i\ \ norm x" ``` huffman@44136 ` 316` ``` apply (simp add: norm_vec_def) ``` nipkow@67155 ` 317` ``` apply (rule member_le_L2_set, simp_all) ``` hoelzl@37489 ` 318` ``` done ``` hoelzl@37489 ` 319` lp15@67979 ` 320` ```lemma norm_bound_component_le_cart: "norm x \ e ==> \x\$i\ \ e" ``` hoelzl@37489 ` 321` ``` by (metis component_le_norm_cart order_trans) ``` hoelzl@37489 ` 322` hoelzl@37489 ` 323` ```lemma norm_bound_component_lt_cart: "norm x < e ==> \x\$i\ < e" ``` huffman@53595 ` 324` ``` by (metis component_le_norm_cart le_less_trans) ``` hoelzl@37489 ` 325` lp15@67979 ` 326` ```lemma norm_le_l1_cart: "norm x \ sum(\i. \x\$i\) UNIV" ``` nipkow@67155 ` 327` ``` by (simp add: norm_vec_def L2_set_le_sum) ``` hoelzl@37489 ` 328` lp15@67969 ` 329` ```lemma scalar_mult_eq_scaleR [simp]: "c *s x = c *\<^sub>R x" ``` huffman@44136 ` 330` ``` unfolding scaleR_vec_def vector_scalar_mult_def by simp ``` hoelzl@37489 ` 331` hoelzl@37489 ` 332` ```lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \c\ * dist x y" ``` hoelzl@37489 ` 333` ``` unfolding dist_norm scalar_mult_eq_scaleR ``` hoelzl@37489 ` 334` ``` unfolding scaleR_right_diff_distrib[symmetric] by simp ``` hoelzl@37489 ` 335` nipkow@64267 ` 336` ```lemma sum_component [simp]: ``` hoelzl@37489 ` 337` ``` fixes f:: " 'a \ ('b::comm_monoid_add) ^'n" ``` nipkow@64267 ` 338` ``` shows "(sum f S)\$i = sum (\x. (f x)\$i) S" ``` wenzelm@49644 ` 339` ```proof (cases "finite S") ``` wenzelm@49644 ` 340` ``` case True ``` wenzelm@49644 ` 341` ``` then show ?thesis by induct simp_all ``` wenzelm@49644 ` 342` ```next ``` wenzelm@49644 ` 343` ``` case False ``` wenzelm@49644 ` 344` ``` then show ?thesis by simp ``` wenzelm@49644 ` 345` ```qed ``` hoelzl@37489 ` 346` nipkow@64267 ` 347` ```lemma sum_eq: "sum f S = (\ i. sum (\x. (f x)\$i ) S)" ``` huffman@44136 ` 348` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 349` nipkow@64267 ` 350` ```lemma sum_cmul: ``` hoelzl@37489 ` 351` ``` fixes f:: "'c \ ('a::semiring_1)^'n" ``` nipkow@64267 ` 352` ``` shows "sum (\x. c *s f x) S = c *s sum f S" ``` nipkow@64267 ` 353` ``` by (simp add: vec_eq_iff sum_distrib_left) ``` hoelzl@37489 ` 354` nipkow@64267 ` 355` ```lemma sum_norm_allsubsets_bound_cart: ``` hoelzl@37489 ` 356` ``` fixes f:: "'a \ real ^'n" ``` nipkow@64267 ` 357` ``` assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (sum f Q) \ e" ``` nipkow@64267 ` 358` ``` shows "sum (\x. norm (f x)) P \ 2 * real CARD('n) * e" ``` nipkow@64267 ` 359` ``` using sum_norm_allsubsets_bound[OF assms] ``` wenzelm@57865 ` 360` ``` by simp ``` hoelzl@37489 ` 361` lp15@62397 ` 362` ```subsection\Closures and interiors of halfspaces\ ``` lp15@62397 ` 363` lp15@62397 ` 364` ```lemma interior_halfspace_le [simp]: ``` lp15@62397 ` 365` ``` assumes "a \ 0" ``` lp15@62397 ` 366` ``` shows "interior {x. a \ x \ b} = {x. a \ x < b}" ``` lp15@62397 ` 367` ```proof - ``` lp15@62397 ` 368` ``` have *: "a \ x < b" if x: "x \ S" and S: "S \ {x. a \ x \ b}" and "open S" for S x ``` lp15@62397 ` 369` ``` proof - ``` lp15@62397 ` 370` ``` obtain e where "e>0" and e: "cball x e \ S" ``` lp15@62397 ` 371` ``` using \open S\ open_contains_cball x by blast ``` lp15@62397 ` 372` ``` then have "x + (e / norm a) *\<^sub>R a \ cball x e" ``` lp15@62397 ` 373` ``` by (simp add: dist_norm) ``` lp15@62397 ` 374` ``` then have "x + (e / norm a) *\<^sub>R a \ S" ``` lp15@62397 ` 375` ``` using e by blast ``` lp15@62397 ` 376` ``` then have "x + (e / norm a) *\<^sub>R a \ {x. a \ x \ b}" ``` lp15@62397 ` 377` ``` using S by blast ``` lp15@62397 ` 378` ``` moreover have "e * (a \ a) / norm a > 0" ``` lp15@62397 ` 379` ``` by (simp add: \0 < e\ assms) ``` lp15@62397 ` 380` ``` ultimately show ?thesis ``` lp15@62397 ` 381` ``` by (simp add: algebra_simps) ``` lp15@62397 ` 382` ``` qed ``` lp15@62397 ` 383` ``` show ?thesis ``` lp15@62397 ` 384` ``` by (rule interior_unique) (auto simp: open_halfspace_lt *) ``` lp15@62397 ` 385` ```qed ``` lp15@62397 ` 386` lp15@62397 ` 387` ```lemma interior_halfspace_ge [simp]: ``` lp15@62397 ` 388` ``` "a \ 0 \ interior {x. a \ x \ b} = {x. a \ x > b}" ``` lp15@62397 ` 389` ```using interior_halfspace_le [of "-a" "-b"] by simp ``` lp15@62397 ` 390` lp15@62397 ` 391` ```lemma interior_halfspace_component_le [simp]: ``` wenzelm@67731 ` 392` ``` "interior {x. x\$k \ a} = {x :: (real^'n). x\$k < a}" (is "?LE") ``` lp15@62397 ` 393` ``` and interior_halfspace_component_ge [simp]: ``` wenzelm@67731 ` 394` ``` "interior {x. x\$k \ a} = {x :: (real^'n). x\$k > a}" (is "?GE") ``` lp15@62397 ` 395` ```proof - ``` lp15@62397 ` 396` ``` have "axis k (1::real) \ 0" ``` lp15@62397 ` 397` ``` by (simp add: axis_def vec_eq_iff) ``` lp15@62397 ` 398` ``` moreover have "axis k (1::real) \ x = x\$k" for x ``` lp15@62397 ` 399` ``` by (simp add: cart_eq_inner_axis inner_commute) ``` lp15@62397 ` 400` ``` ultimately show ?LE ?GE ``` lp15@62397 ` 401` ``` using interior_halfspace_le [of "axis k (1::real)" a] ``` lp15@62397 ` 402` ``` interior_halfspace_ge [of "axis k (1::real)" a] by auto ``` lp15@62397 ` 403` ```qed ``` lp15@62397 ` 404` lp15@62397 ` 405` ```lemma closure_halfspace_lt [simp]: ``` lp15@62397 ` 406` ``` assumes "a \ 0" ``` lp15@62397 ` 407` ``` shows "closure {x. a \ x < b} = {x. a \ x \ b}" ``` lp15@62397 ` 408` ```proof - ``` lp15@62397 ` 409` ``` have [simp]: "-{x. a \ x < b} = {x. a \ x \ b}" ``` lp15@62397 ` 410` ``` by (force simp:) ``` lp15@62397 ` 411` ``` then show ?thesis ``` lp15@62397 ` 412` ``` using interior_halfspace_ge [of a b] assms ``` lp15@62397 ` 413` ``` by (force simp: closure_interior) ``` lp15@62397 ` 414` ```qed ``` lp15@62397 ` 415` lp15@62397 ` 416` ```lemma closure_halfspace_gt [simp]: ``` lp15@62397 ` 417` ``` "a \ 0 \ closure {x. a \ x > b} = {x. a \ x \ b}" ``` lp15@62397 ` 418` ```using closure_halfspace_lt [of "-a" "-b"] by simp ``` lp15@62397 ` 419` lp15@62397 ` 420` ```lemma closure_halfspace_component_lt [simp]: ``` wenzelm@67731 ` 421` ``` "closure {x. x\$k < a} = {x :: (real^'n). x\$k \ a}" (is "?LE") ``` lp15@62397 ` 422` ``` and closure_halfspace_component_gt [simp]: ``` wenzelm@67731 ` 423` ``` "closure {x. x\$k > a} = {x :: (real^'n). x\$k \ a}" (is "?GE") ``` lp15@62397 ` 424` ```proof - ``` lp15@62397 ` 425` ``` have "axis k (1::real) \ 0" ``` lp15@62397 ` 426` ``` by (simp add: axis_def vec_eq_iff) ``` lp15@62397 ` 427` ``` moreover have "axis k (1::real) \ x = x\$k" for x ``` lp15@62397 ` 428` ``` by (simp add: cart_eq_inner_axis inner_commute) ``` lp15@62397 ` 429` ``` ultimately show ?LE ?GE ``` lp15@62397 ` 430` ``` using closure_halfspace_lt [of "axis k (1::real)" a] ``` lp15@62397 ` 431` ``` closure_halfspace_gt [of "axis k (1::real)" a] by auto ``` lp15@62397 ` 432` ```qed ``` lp15@62397 ` 433` lp15@62397 ` 434` ```lemma interior_hyperplane [simp]: ``` lp15@62397 ` 435` ``` assumes "a \ 0" ``` lp15@62397 ` 436` ``` shows "interior {x. a \ x = b} = {}" ``` lp15@62397 ` 437` ```proof - ``` lp15@62397 ` 438` ``` have [simp]: "{x. a \ x = b} = {x. a \ x \ b} \ {x. a \ x \ b}" ``` lp15@62397 ` 439` ``` by (force simp:) ``` lp15@62397 ` 440` ``` then show ?thesis ``` lp15@62397 ` 441` ``` by (auto simp: assms) ``` lp15@62397 ` 442` ```qed ``` lp15@62397 ` 443` lp15@62397 ` 444` ```lemma frontier_halfspace_le: ``` lp15@62397 ` 445` ``` assumes "a \ 0 \ b \ 0" ``` lp15@62397 ` 446` ``` shows "frontier {x. a \ x \ b} = {x. a \ x = b}" ``` lp15@62397 ` 447` ```proof (cases "a = 0") ``` lp15@62397 ` 448` ``` case True with assms show ?thesis by simp ``` lp15@62397 ` 449` ```next ``` lp15@62397 ` 450` ``` case False then show ?thesis ``` lp15@62397 ` 451` ``` by (force simp: frontier_def closed_halfspace_le) ``` lp15@62397 ` 452` ```qed ``` lp15@62397 ` 453` lp15@62397 ` 454` ```lemma frontier_halfspace_ge: ``` lp15@62397 ` 455` ``` assumes "a \ 0 \ b \ 0" ``` lp15@62397 ` 456` ``` shows "frontier {x. a \ x \ b} = {x. a \ x = b}" ``` lp15@62397 ` 457` ```proof (cases "a = 0") ``` lp15@62397 ` 458` ``` case True with assms show ?thesis by simp ``` lp15@62397 ` 459` ```next ``` lp15@62397 ` 460` ``` case False then show ?thesis ``` lp15@62397 ` 461` ``` by (force simp: frontier_def closed_halfspace_ge) ``` lp15@62397 ` 462` ```qed ``` lp15@62397 ` 463` lp15@62397 ` 464` ```lemma frontier_halfspace_lt: ``` lp15@62397 ` 465` ``` assumes "a \ 0 \ b \ 0" ``` lp15@62397 ` 466` ``` shows "frontier {x. a \ x < b} = {x. a \ x = b}" ``` lp15@62397 ` 467` ```proof (cases "a = 0") ``` lp15@62397 ` 468` ``` case True with assms show ?thesis by simp ``` lp15@62397 ` 469` ```next ``` lp15@62397 ` 470` ``` case False then show ?thesis ``` lp15@62397 ` 471` ``` by (force simp: frontier_def interior_open open_halfspace_lt) ``` lp15@62397 ` 472` ```qed ``` lp15@62397 ` 473` lp15@62397 ` 474` ```lemma frontier_halfspace_gt: ``` lp15@62397 ` 475` ``` assumes "a \ 0 \ b \ 0" ``` lp15@62397 ` 476` ``` shows "frontier {x. a \ x > b} = {x. a \ x = b}" ``` lp15@62397 ` 477` ```proof (cases "a = 0") ``` lp15@62397 ` 478` ``` case True with assms show ?thesis by simp ``` lp15@62397 ` 479` ```next ``` lp15@62397 ` 480` ``` case False then show ?thesis ``` lp15@62397 ` 481` ``` by (force simp: frontier_def interior_open open_halfspace_gt) ``` lp15@62397 ` 482` ```qed ``` lp15@62397 ` 483` lp15@62397 ` 484` ```lemma interior_standard_hyperplane: ``` wenzelm@67731 ` 485` ``` "interior {x :: (real^'n). x\$k = a} = {}" ``` lp15@62397 ` 486` ```proof - ``` lp15@62397 ` 487` ``` have "axis k (1::real) \ 0" ``` lp15@62397 ` 488` ``` by (simp add: axis_def vec_eq_iff) ``` lp15@62397 ` 489` ``` moreover have "axis k (1::real) \ x = x\$k" for x ``` lp15@62397 ` 490` ``` by (simp add: cart_eq_inner_axis inner_commute) ``` lp15@62397 ` 491` ``` ultimately show ?thesis ``` lp15@62397 ` 492` ``` using interior_hyperplane [of "axis k (1::real)" a] ``` lp15@62397 ` 493` ``` by force ``` lp15@62397 ` 494` ```qed ``` lp15@62397 ` 495` wenzelm@60420 ` 496` ```subsection \Matrix operations\ ``` hoelzl@37489 ` 497` wenzelm@60420 ` 498` ```text\Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"}\ ``` hoelzl@37489 ` 499` immler@67962 ` 500` ```definition map_matrix::"('a \ 'b) \ (('a, 'i::finite)vec, 'j::finite) vec \ (('b, 'i)vec, 'j) vec" where ``` immler@67962 ` 501` ``` "map_matrix f x = (\ i j. f (x \$ i \$ j))" ``` immler@67962 ` 502` immler@67962 ` 503` ```lemma nth_map_matrix[simp]: "map_matrix f x \$ i \$ j = f (x \$ i \$ j)" ``` immler@67962 ` 504` ``` by (simp add: map_matrix_def) ``` immler@67962 ` 505` wenzelm@49644 ` 506` ```definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \ 'a ^'p^'n \ 'a ^ 'p ^'m" ``` wenzelm@49644 ` 507` ``` (infixl "**" 70) ``` nipkow@64267 ` 508` ``` where "m ** m' == (\ i j. sum (\k. ((m\$i)\$k) * ((m'\$k)\$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m" ``` hoelzl@37489 ` 509` wenzelm@49644 ` 510` ```definition matrix_vector_mult :: "('a::semiring_1) ^'n^'m \ 'a ^'n \ 'a ^ 'm" ``` wenzelm@49644 ` 511` ``` (infixl "*v" 70) ``` nipkow@64267 ` 512` ``` where "m *v x \ (\ i. sum (\j. ((m\$i)\$j) * (x\$j)) (UNIV ::'n set)) :: 'a^'m" ``` hoelzl@37489 ` 513` wenzelm@49644 ` 514` ```definition vector_matrix_mult :: "'a ^ 'm \ ('a::semiring_1) ^'n^'m \ 'a ^'n " ``` wenzelm@49644 ` 515` ``` (infixl "v*" 70) ``` nipkow@64267 ` 516` ``` where "v v* m == (\ j. sum (\i. ((m\$i)\$j) * (v\$i)) (UNIV :: 'm set)) :: 'a^'n" ``` hoelzl@37489 ` 517` hoelzl@37489 ` 518` ```definition "(mat::'a::zero => 'a ^'n^'n) k = (\ i j. if i = j then k else 0)" ``` hoelzl@63332 ` 519` ```definition transpose where ``` hoelzl@37489 ` 520` ``` "(transpose::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A\$j)\$i))" ``` hoelzl@37489 ` 521` ```definition "(row::'m => 'a ^'n^'m \ 'a ^'n) i A = (\ j. ((A\$i)\$j))" ``` hoelzl@37489 ` 522` ```definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\ i. ((A\$i)\$j))" ``` hoelzl@37489 ` 523` ```definition "rows(A::'a^'n^'m) = { row i A | i. i \ (UNIV :: 'm set)}" ``` hoelzl@37489 ` 524` ```definition "columns(A::'a^'n^'m) = { column i A | i. i \ (UNIV :: 'n set)}" ``` lp15@68038 ` 525` ``` ``` lp15@68038 ` 526` ```lemma times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" ``` lp15@68038 ` 527` ``` by (simp add: matrix_matrix_mult_def zero_vec_def) ``` lp15@68038 ` 528` lp15@68038 ` 529` ```lemma times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0" ``` lp15@68038 ` 530` ``` by (simp add: matrix_matrix_mult_def zero_vec_def) ``` hoelzl@37489 ` 531` hoelzl@37489 ` 532` ```lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) ``` hoelzl@37489 ` 533` ```lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" ``` nipkow@64267 ` 534` ``` by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps) ``` hoelzl@37489 ` 535` lp15@67673 ` 536` ```lemma matrix_mul_lid [simp]: ``` hoelzl@37489 ` 537` ``` fixes A :: "'a::semiring_1 ^ 'm ^ 'n" ``` hoelzl@37489 ` 538` ``` shows "mat 1 ** A = A" ``` hoelzl@37489 ` 539` ``` apply (simp add: matrix_matrix_mult_def mat_def) ``` hoelzl@37489 ` 540` ``` apply vector ``` nipkow@64267 ` 541` ``` apply (auto simp only: if_distrib cond_application_beta sum.delta'[OF finite] ``` wenzelm@49644 ` 542` ``` mult_1_left mult_zero_left if_True UNIV_I) ``` wenzelm@49644 ` 543` ``` done ``` hoelzl@37489 ` 544` lp15@67673 ` 545` ```lemma matrix_mul_rid [simp]: ``` hoelzl@37489 ` 546` ``` fixes A :: "'a::semiring_1 ^ 'm ^ 'n" ``` hoelzl@37489 ` 547` ``` shows "A ** mat 1 = A" ``` hoelzl@37489 ` 548` ``` apply (simp add: matrix_matrix_mult_def mat_def) ``` hoelzl@37489 ` 549` ``` apply vector ``` nipkow@64267 ` 550` ``` apply (auto simp only: if_distrib cond_application_beta sum.delta[OF finite] ``` wenzelm@49644 ` 551` ``` mult_1_right mult_zero_right if_True UNIV_I cong: if_cong) ``` wenzelm@49644 ` 552` ``` done ``` hoelzl@37489 ` 553` hoelzl@37489 ` 554` ```lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" ``` nipkow@64267 ` 555` ``` apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc) ``` haftmann@66804 ` 556` ``` apply (subst sum.swap) ``` hoelzl@37489 ` 557` ``` apply simp ``` hoelzl@37489 ` 558` ``` done ``` hoelzl@37489 ` 559` hoelzl@37489 ` 560` ```lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" ``` wenzelm@49644 ` 561` ``` apply (vector matrix_matrix_mult_def matrix_vector_mult_def ``` nipkow@64267 ` 562` ``` sum_distrib_left sum_distrib_right mult.assoc) ``` haftmann@66804 ` 563` ``` apply (subst sum.swap) ``` hoelzl@37489 ` 564` ``` apply simp ``` hoelzl@37489 ` 565` ``` done ``` hoelzl@37489 ` 566` lp15@68038 ` 567` ```lemma scalar_matrix_assoc: ``` lp15@68045 ` 568` ``` fixes A :: "('a::real_algebra_1)^'m^'n" ``` lp15@68038 ` 569` ``` shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B" ``` lp15@68045 ` 570` ``` by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff scaleR_sum_right) ``` lp15@68038 ` 571` lp15@68038 ` 572` ```lemma matrix_scalar_ac: ``` lp15@68045 ` 573` ``` fixes A :: "('a::real_algebra_1)^'m^'n" ``` lp15@68038 ` 574` ``` shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B" ``` lp15@68038 ` 575` ``` by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff) ``` lp15@68038 ` 576` lp15@67673 ` 577` ```lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" ``` hoelzl@37489 ` 578` ``` apply (vector matrix_vector_mult_def mat_def) ``` nipkow@64267 ` 579` ``` apply (simp add: if_distrib cond_application_beta sum.delta' cong del: if_weak_cong) ``` wenzelm@49644 ` 580` ``` done ``` hoelzl@37489 ` 581` wenzelm@49644 ` 582` ```lemma matrix_transpose_mul: ``` wenzelm@49644 ` 583` ``` "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)" ``` haftmann@57512 ` 584` ``` by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute) ``` hoelzl@37489 ` 585` hoelzl@37489 ` 586` ```lemma matrix_eq: ``` hoelzl@37489 ` 587` ``` fixes A B :: "'a::semiring_1 ^ 'n ^ 'm" ``` hoelzl@37489 ` 588` ``` shows "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") ``` hoelzl@37489 ` 589` ``` apply auto ``` huffman@44136 ` 590` ``` apply (subst vec_eq_iff) ``` hoelzl@37489 ` 591` ``` apply clarify ``` hoelzl@50526 ` 592` ``` apply (clarsimp simp add: matrix_vector_mult_def if_distrib cond_application_beta vec_eq_iff cong del: if_weak_cong) ``` hoelzl@50526 ` 593` ``` apply (erule_tac x="axis ia 1" in allE) ``` hoelzl@37489 ` 594` ``` apply (erule_tac x="i" in allE) ``` hoelzl@50526 ` 595` ``` apply (auto simp add: if_distrib cond_application_beta axis_def ``` nipkow@64267 ` 596` ``` sum.delta[OF finite] cong del: if_weak_cong) ``` wenzelm@49644 ` 597` ``` done ``` hoelzl@37489 ` 598` lp15@68050 ` 599` ```lemma matrix_vector_mul_component: "(A *v x)\$k = (A\$k) \ x" ``` huffman@44136 ` 600` ``` by (simp add: matrix_vector_mult_def inner_vec_def) ``` hoelzl@37489 ` 601` hoelzl@37489 ` 602` ```lemma dot_lmul_matrix: "((x::real ^_) v* A) \ y = x \ (A *v y)" ``` nipkow@64267 ` 603` ``` apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps) ``` haftmann@66804 ` 604` ``` apply (subst sum.swap) ``` wenzelm@49644 ` 605` ``` apply simp ``` wenzelm@49644 ` 606` ``` done ``` hoelzl@37489 ` 607` lp15@67673 ` 608` ```lemma transpose_mat [simp]: "transpose (mat n) = mat n" ``` hoelzl@37489 ` 609` ``` by (vector transpose_def mat_def) ``` hoelzl@37489 ` 610` lp15@67683 ` 611` ```lemma transpose_transpose [simp]: "transpose(transpose A) = A" ``` hoelzl@37489 ` 612` ``` by (vector transpose_def) ``` hoelzl@37489 ` 613` lp15@67673 ` 614` ```lemma row_transpose [simp]: ``` hoelzl@37489 ` 615` ``` fixes A:: "'a::semiring_1^_^_" ``` hoelzl@37489 ` 616` ``` shows "row i (transpose A) = column i A" ``` huffman@44136 ` 617` ``` by (simp add: row_def column_def transpose_def vec_eq_iff) ``` hoelzl@37489 ` 618` lp15@67673 ` 619` ```lemma column_transpose [simp]: ``` hoelzl@37489 ` 620` ``` fixes A:: "'a::semiring_1^_^_" ``` hoelzl@37489 ` 621` ``` shows "column i (transpose A) = row i A" ``` huffman@44136 ` 622` ``` by (simp add: row_def column_def transpose_def vec_eq_iff) ``` hoelzl@37489 ` 623` lp15@67683 ` 624` ```lemma rows_transpose [simp]: "rows(transpose (A::'a::semiring_1^_^_)) = columns A" ``` wenzelm@49644 ` 625` ``` by (auto simp add: rows_def columns_def row_transpose intro: set_eqI) ``` hoelzl@37489 ` 626` lp15@67683 ` 627` ```lemma columns_transpose [simp]: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" ``` wenzelm@49644 ` 628` ``` by (metis transpose_transpose rows_transpose) ``` hoelzl@37489 ` 629` lp15@68038 ` 630` ```lemma transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A" ``` lp15@68038 ` 631` ``` unfolding transpose_def ``` lp15@68038 ` 632` ``` by (simp add: vec_eq_iff) ``` lp15@68038 ` 633` lp15@68038 ` 634` ```lemma transpose_iff [iff]: "transpose A = transpose B \ A = B" ``` lp15@68038 ` 635` ``` by (metis transpose_transpose) ``` lp15@68038 ` 636` lp15@67673 ` 637` ```lemma matrix_mult_transpose_dot_column: ``` lp15@67673 ` 638` ``` shows "transpose A ** A = (\ i j. (column i A) \ (column j A))" ``` lp15@67673 ` 639` ``` by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def) ``` lp15@67673 ` 640` lp15@67673 ` 641` ```lemma matrix_mult_transpose_dot_row: ``` lp15@67673 ` 642` ``` shows "A ** transpose A = (\ i j. (row i A) \ (row j A))" ``` lp15@67673 ` 643` ``` by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def) ``` lp15@67673 ` 644` wenzelm@60420 ` 645` ```text\Two sometimes fruitful ways of looking at matrix-vector multiplication.\ ``` hoelzl@37489 ` 646` hoelzl@37489 ` 647` ```lemma matrix_mult_dot: "A *v x = (\ i. A\$i \ x)" ``` huffman@44136 ` 648` ``` by (simp add: matrix_vector_mult_def inner_vec_def) ``` hoelzl@37489 ` 649` lp15@67673 ` 650` ```lemma matrix_mult_sum: ``` nipkow@64267 ` 651` ``` "(A::'a::comm_semiring_1^'n^'m) *v x = sum (\i. (x\$i) *s column i A) (UNIV:: 'n set)" ``` haftmann@57512 ` 652` ``` by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult.commute) ``` hoelzl@37489 ` 653` hoelzl@37489 ` 654` ```lemma vector_componentwise: ``` hoelzl@50526 ` 655` ``` "(x::'a::ring_1^'n) = (\ j. \i\UNIV. (x\$i) * (axis i 1 :: 'a^'n) \$ j)" ``` nipkow@64267 ` 656` ``` by (simp add: axis_def if_distrib sum.If_cases vec_eq_iff) ``` hoelzl@50526 ` 657` nipkow@64267 ` 658` ```lemma basis_expansion: "sum (\i. (x\$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" ``` nipkow@64267 ` 659` ``` by (auto simp add: axis_def vec_eq_iff if_distrib sum.If_cases cong del: if_weak_cong) ``` hoelzl@37489 ` 660` lp15@63938 ` 661` ```lemma linear_componentwise_expansion: ``` hoelzl@37489 ` 662` ``` fixes f:: "real ^'m \ real ^ _" ``` hoelzl@37489 ` 663` ``` assumes lf: "linear f" ``` nipkow@64267 ` 664` ``` shows "(f x)\$j = sum (\i. (x\$i) * (f (axis i 1)\$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") ``` wenzelm@49644 ` 665` ```proof - ``` hoelzl@37489 ` 666` ``` let ?M = "(UNIV :: 'm set)" ``` hoelzl@37489 ` 667` ``` let ?N = "(UNIV :: 'n set)" ``` nipkow@64267 ` 668` ``` have "?rhs = (sum (\i.(x\$i) *\<^sub>R f (axis i 1) ) ?M)\$j" ``` nipkow@64267 ` 669` ``` unfolding sum_component by simp ``` wenzelm@49644 ` 670` ``` then show ?thesis ``` nipkow@64267 ` 671` ``` unfolding linear_sum_mul[OF lf, symmetric] ``` hoelzl@50526 ` 672` ``` unfolding scalar_mult_eq_scaleR[symmetric] ``` hoelzl@50526 ` 673` ``` unfolding basis_expansion ``` hoelzl@50526 ` 674` ``` by simp ``` hoelzl@37489 ` 675` ```qed ``` hoelzl@37489 ` 676` lp15@67719 ` 677` ```subsection\Inverse matrices (not necessarily square)\ ``` hoelzl@37489 ` 678` wenzelm@49644 ` 679` ```definition ``` wenzelm@49644 ` 680` ``` "invertible(A::'a::semiring_1^'n^'m) \ (\A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" ``` hoelzl@37489 ` 681` wenzelm@49644 ` 682` ```definition ``` wenzelm@49644 ` 683` ``` "matrix_inv(A:: 'a::semiring_1^'n^'m) = ``` wenzelm@49644 ` 684` ``` (SOME A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" ``` hoelzl@37489 ` 685` wenzelm@60420 ` 686` ```text\Correspondence between matrices and linear operators.\ ``` hoelzl@37489 ` 687` wenzelm@49644 ` 688` ```definition matrix :: "('a::{plus,times, one, zero}^'m \ 'a ^ 'n) \ 'a^'m^'n" ``` hoelzl@50526 ` 689` ``` where "matrix f = (\ i j. (f(axis j 1))\$i)" ``` hoelzl@37489 ` 690` lp15@67986 ` 691` ```lemma matrix_id_mat_1: "matrix id = mat 1" ``` lp15@67986 ` 692` ``` by (simp add: mat_def matrix_def axis_def) ``` lp15@67986 ` 693` lp15@67986 ` 694` ```lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r" ``` lp15@67986 ` 695` ``` by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong) ``` lp15@67986 ` 696` lp15@68050 ` 697` ```lemma matrix_vector_mul_linear: "linear(\x. A *v (x::('a::real_algebra_1) ^ _))" ``` lp15@68050 ` 698` ``` by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum.distrib scaleR_right.sum) ``` hoelzl@37489 ` 699` lp15@67683 ` 700` ```lemma ``` lp15@68050 ` 701` ``` fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m" ``` lp15@67683 ` 702` ``` shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z" ``` lp15@67683 ` 703` ``` and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)" ``` lp15@67683 ` 704` ``` by (simp_all add: linear_linear linear_continuous_at linear_continuous_on matrix_vector_mul_linear) ``` lp15@67683 ` 705` lp15@68043 ` 706` ```lemma vector_matrix_left_distrib [algebra_simps]: ``` lp15@68043 ` 707` ``` shows "(x + y) v* A = x v* A + y v* A" ``` lp15@68043 ` 708` ``` unfolding vector_matrix_mult_def ``` lp15@68043 ` 709` ``` by (simp add: algebra_simps sum.distrib vec_eq_iff) ``` lp15@68043 ` 710` lp15@68043 ` 711` ```lemma matrix_vector_right_distrib [algebra_simps]: ``` immler@67728 ` 712` ``` "A *v (x + y) = A *v x + A *v y" ``` immler@67728 ` 713` ``` by (vector matrix_vector_mult_def sum.distrib distrib_left) ``` lp15@67673 ` 714` lp15@67673 ` 715` ```lemma matrix_vector_mult_diff_distrib [algebra_simps]: ``` immler@67728 ` 716` ``` fixes A :: "'a::ring_1^'n^'m" ``` lp15@67673 ` 717` ``` shows "A *v (x - y) = A *v x - A *v y" ``` immler@67728 ` 718` ``` by (vector matrix_vector_mult_def sum_subtractf right_diff_distrib) ``` lp15@67673 ` 719` lp15@67673 ` 720` ```lemma matrix_vector_mult_scaleR[algebra_simps]: ``` lp15@67673 ` 721` ``` fixes A :: "real^'n^'m" ``` lp15@67673 ` 722` ``` shows "A *v (c *\<^sub>R x) = c *\<^sub>R (A *v x)" ``` lp15@67673 ` 723` ``` using linear_iff matrix_vector_mul_linear by blast ``` lp15@67673 ` 724` lp15@67673 ` 725` ```lemma matrix_vector_mult_0_right [simp]: "A *v 0 = 0" ``` lp15@67673 ` 726` ``` by (simp add: matrix_vector_mult_def vec_eq_iff) ``` lp15@67673 ` 727` lp15@67673 ` 728` ```lemma matrix_vector_mult_0 [simp]: "0 *v w = 0" ``` lp15@67673 ` 729` ``` by (simp add: matrix_vector_mult_def vec_eq_iff) ``` lp15@67673 ` 730` lp15@67673 ` 731` ```lemma matrix_vector_mult_add_rdistrib [algebra_simps]: ``` immler@67728 ` 732` ``` "(A + B) *v x = (A *v x) + (B *v x)" ``` immler@67728 ` 733` ``` by (vector matrix_vector_mult_def sum.distrib distrib_right) ``` lp15@67673 ` 734` lp15@67673 ` 735` ```lemma matrix_vector_mult_diff_rdistrib [algebra_simps]: ``` immler@67728 ` 736` ``` fixes A :: "'a :: ring_1^'n^'m" ``` lp15@67673 ` 737` ``` shows "(A - B) *v x = (A *v x) - (B *v x)" ``` immler@67728 ` 738` ``` by (vector matrix_vector_mult_def sum_subtractf left_diff_distrib) ``` lp15@67673 ` 739` wenzelm@49644 ` 740` ```lemma matrix_works: ``` wenzelm@49644 ` 741` ``` assumes lf: "linear f" ``` wenzelm@49644 ` 742` ``` shows "matrix f *v x = f (x::real ^ 'n)" ``` haftmann@57512 ` 743` ``` apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute) ``` lp15@63938 ` 744` ``` by (simp add: linear_componentwise_expansion lf) ``` hoelzl@37489 ` 745` wenzelm@49644 ` 746` ```lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::real ^ 'n))" ``` wenzelm@49644 ` 747` ``` by (simp add: ext matrix_works) ``` hoelzl@37489 ` 748` lp15@67683 ` 749` ```declare matrix_vector_mul [symmetric, simp] ``` lp15@67683 ` 750` lp15@67673 ` 751` ```lemma matrix_of_matrix_vector_mul [simp]: "matrix(\x. A *v (x :: real ^ 'n)) = A" ``` hoelzl@37489 ` 752` ``` by (simp add: matrix_eq matrix_vector_mul_linear matrix_works) ``` hoelzl@37489 ` 753` hoelzl@37489 ` 754` ```lemma matrix_compose: ``` hoelzl@37489 ` 755` ``` assumes lf: "linear (f::real^'n \ real^'m)" ``` wenzelm@49644 ` 756` ``` and lg: "linear (g::real^'m \ real^_)" ``` wenzelm@61736 ` 757` ``` shows "matrix (g \ f) = matrix g ** matrix f" ``` hoelzl@37489 ` 758` ``` using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]] ``` wenzelm@49644 ` 759` ``` by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) ``` hoelzl@37489 ` 760` wenzelm@49644 ` 761` ```lemma matrix_vector_column: ``` nipkow@64267 ` 762` ``` "(A::'a::comm_semiring_1^'n^_) *v x = sum (\i. (x\$i) *s ((transpose A)\$i)) (UNIV:: 'n set)" ``` haftmann@57512 ` 763` ``` by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute) ``` hoelzl@37489 ` 764` hoelzl@37489 ` 765` ```lemma adjoint_matrix: "adjoint(\x. (A::real^'n^'m) *v x) = (\x. transpose A *v x)" ``` hoelzl@37489 ` 766` ``` apply (rule adjoint_unique) ``` wenzelm@49644 ` 767` ``` apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def ``` nipkow@64267 ` 768` ``` sum_distrib_right sum_distrib_left) ``` haftmann@66804 ` 769` ``` apply (subst sum.swap) ``` haftmann@57514 ` 770` ``` apply (auto simp add: ac_simps) ``` hoelzl@37489 ` 771` ``` done ``` hoelzl@37489 ` 772` hoelzl@37489 ` 773` ```lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \ real ^'m)" ``` hoelzl@37489 ` 774` ``` shows "matrix(adjoint f) = transpose(matrix f)" ``` hoelzl@37489 ` 775` ``` apply (subst matrix_vector_mul[OF lf]) ``` wenzelm@49644 ` 776` ``` unfolding adjoint_matrix matrix_of_matrix_vector_mul ``` wenzelm@49644 ` 777` ``` apply rule ``` wenzelm@49644 ` 778` ``` done ``` wenzelm@49644 ` 779` lp15@67981 ` 780` ```lemma inj_matrix_vector_mult: ``` lp15@67981 ` 781` ``` fixes A::"'a::field^'n^'m" ``` lp15@67981 ` 782` ``` assumes "invertible A" ``` lp15@67981 ` 783` ``` shows "inj (( *v) A)" ``` lp15@67981 ` 784` ``` by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid) ``` lp15@67981 ` 785` lp15@68038 ` 786` ```lemma scalar_invertible: ``` lp15@68050 ` 787` ``` fixes A :: "('a::real_algebra_1)^'m^'n" ``` lp15@68038 ` 788` ``` assumes "k \ 0" and "invertible A" ``` lp15@68038 ` 789` ``` shows "invertible (k *\<^sub>R A)" ``` lp15@68038 ` 790` ```proof - ``` lp15@68038 ` 791` ``` obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1" ``` lp15@68038 ` 792` ``` using assms unfolding invertible_def by auto ``` lp15@68038 ` 793` ``` with `k \ 0` ``` lp15@68038 ` 794` ``` have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1" ``` lp15@68038 ` 795` ``` by (simp_all add: assms matrix_scalar_ac) ``` lp15@68038 ` 796` ``` thus "invertible (k *\<^sub>R A)" ``` lp15@68038 ` 797` ``` unfolding invertible_def by auto ``` lp15@68038 ` 798` ```qed ``` lp15@68038 ` 799` lp15@68038 ` 800` ```lemma scalar_invertible_iff: ``` lp15@68050 ` 801` ``` fixes A :: "('a::real_algebra_1)^'m^'n" ``` lp15@68038 ` 802` ``` assumes "k \ 0" and "invertible A" ``` lp15@68038 ` 803` ``` shows "invertible (k *\<^sub>R A) \ k \ 0 \ invertible A" ``` lp15@68038 ` 804` ``` by (simp add: assms scalar_invertible) ``` lp15@68038 ` 805` lp15@68038 ` 806` ```lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x" ``` lp15@68038 ` 807` ``` unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def ``` lp15@68038 ` 808` ``` by simp ``` lp15@68038 ` 809` lp15@68038 ` 810` ```lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A" ``` lp15@68038 ` 811` ``` unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def ``` lp15@68038 ` 812` ``` by simp ``` lp15@68038 ` 813` lp15@68043 ` 814` ```lemma vector_scalar_commute: ``` lp15@68043 ` 815` ``` fixes A :: "'a::{field}^'m^'n" ``` lp15@68043 ` 816` ``` shows "A *v (c *s x) = c *s (A *v x)" ``` lp15@68043 ` 817` ``` by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left) ``` lp15@68043 ` 818` lp15@68043 ` 819` ```lemma scalar_vector_matrix_assoc: ``` lp15@68043 ` 820` ``` fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n" ``` lp15@68043 ` 821` ``` shows "(k *s x) v* A = k *s (x v* A)" ``` lp15@68043 ` 822` ``` by (metis transpose_matrix_vector vector_scalar_commute) ``` lp15@68043 ` 823` ``` ``` lp15@68043 ` 824` ```lemma vector_matrix_mult_0 [simp]: "0 v* A = 0" ``` lp15@68043 ` 825` ``` unfolding vector_matrix_mult_def by (simp add: zero_vec_def) ``` lp15@68043 ` 826` lp15@68043 ` 827` ```lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0" ``` lp15@68043 ` 828` ``` unfolding vector_matrix_mult_def by (simp add: zero_vec_def) ``` lp15@68043 ` 829` lp15@68043 ` 830` ```lemma vector_matrix_mul_rid [simp]: ``` lp15@68038 ` 831` ``` fixes v :: "('a::semiring_1)^'n" ``` lp15@68038 ` 832` ``` shows "v v* mat 1 = v" ``` lp15@68038 ` 833` ``` by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix) ``` lp15@68038 ` 834` lp15@68043 ` 835` ```lemma scaleR_vector_matrix_assoc: ``` lp15@68038 ` 836` ``` fixes k :: real and x :: "real^'n" and A :: "real^'m^'n" ``` lp15@68038 ` 837` ``` shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)" ``` lp15@68038 ` 838` ``` by (metis matrix_vector_mult_scaleR transpose_matrix_vector) ``` lp15@68038 ` 839` lp15@68043 ` 840` ```lemma vector_scaleR_matrix_ac: ``` lp15@68038 ` 841` ``` fixes k :: real and x :: "real^'n" and A :: "real^'m^'n" ``` lp15@68038 ` 842` ``` shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)" ``` lp15@68038 ` 843` ```proof - ``` lp15@68038 ` 844` ``` have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A" ``` lp15@68038 ` 845` ``` unfolding vector_matrix_mult_def ``` lp15@68038 ` 846` ``` by (simp add: algebra_simps) ``` lp15@68043 ` 847` ``` with scaleR_vector_matrix_assoc ``` lp15@68038 ` 848` ``` show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)" ``` lp15@68038 ` 849` ``` by auto ``` lp15@68038 ` 850` ```qed ``` lp15@68038 ` 851` hoelzl@37489 ` 852` nipkow@67968 ` 853` ```subsection\Some bounds on components etc. relative to operator norm\ ``` lp15@67719 ` 854` lp15@67719 ` 855` ```lemma norm_column_le_onorm: ``` lp15@67719 ` 856` ``` fixes A :: "real^'n^'m" ``` lp15@67719 ` 857` ``` shows "norm(column i A) \ onorm(( *v) A)" ``` lp15@67719 ` 858` ```proof - ``` lp15@67719 ` 859` ``` have bl: "bounded_linear (( *v) A)" ``` lp15@67719 ` 860` ``` by (simp add: linear_linear matrix_vector_mul_linear) ``` lp15@67719 ` 861` ``` have "norm (\ j. A \$ j \$ i) \ norm (A *v axis i 1)" ``` lp15@67719 ` 862` ``` by (simp add: matrix_mult_dot cart_eq_inner_axis) ``` lp15@67719 ` 863` ``` also have "\ \ onorm (( *v) A)" ``` lp15@67982 ` 864` ``` using onorm [OF bl, of "axis i 1"] by auto ``` lp15@67719 ` 865` ``` finally have "norm (\ j. A \$ j \$ i) \ onorm (( *v) A)" . ``` lp15@67719 ` 866` ``` then show ?thesis ``` lp15@67719 ` 867` ``` unfolding column_def . ``` lp15@67719 ` 868` ```qed ``` lp15@67719 ` 869` lp15@67719 ` 870` ```lemma matrix_component_le_onorm: ``` lp15@67719 ` 871` ``` fixes A :: "real^'n^'m" ``` lp15@67719 ` 872` ``` shows "\A \$ i \$ j\ \ onorm(( *v) A)" ``` lp15@67719 ` 873` ```proof - ``` lp15@67719 ` 874` ``` have "\A \$ i \$ j\ \ norm (\ n. (A \$ n \$ j))" ``` lp15@67719 ` 875` ``` by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta) ``` lp15@67719 ` 876` ``` also have "\ \ onorm (( *v) A)" ``` lp15@67719 ` 877` ``` by (metis (no_types) column_def norm_column_le_onorm) ``` lp15@67719 ` 878` ``` finally show ?thesis . ``` lp15@67719 ` 879` ```qed ``` lp15@67719 ` 880` lp15@67719 ` 881` ```lemma component_le_onorm: ``` lp15@67719 ` 882` ``` fixes f :: "real^'m \ real^'n" ``` lp15@67719 ` 883` ``` shows "linear f \ \matrix f \$ i \$ j\ \ onorm f" ``` lp15@67719 ` 884` ``` by (metis matrix_component_le_onorm matrix_vector_mul) ``` hoelzl@37489 ` 885` lp15@67719 ` 886` ```lemma onorm_le_matrix_component_sum: ``` lp15@67719 ` 887` ``` fixes A :: "real^'n^'m" ``` lp15@67719 ` 888` ``` shows "onorm(( *v) A) \ (\i\UNIV. \j\UNIV. \A \$ i \$ j\)" ``` lp15@67719 ` 889` ```proof (rule onorm_le) ``` lp15@67719 ` 890` ``` fix x ``` lp15@67719 ` 891` ``` have "norm (A *v x) \ (\i\UNIV. \(A *v x) \$ i\)" ``` lp15@67719 ` 892` ``` by (rule norm_le_l1_cart) ``` lp15@67719 ` 893` ``` also have "\ \ (\i\UNIV. \j\UNIV. \A \$ i \$ j\ * norm x)" ``` lp15@67719 ` 894` ``` proof (rule sum_mono) ``` lp15@67719 ` 895` ``` fix i ``` lp15@67719 ` 896` ``` have "\(A *v x) \$ i\ \ \\j\UNIV. A \$ i \$ j * x \$ j\" ``` lp15@67719 ` 897` ``` by (simp add: matrix_vector_mult_def) ``` lp15@67719 ` 898` ``` also have "\ \ (\j\UNIV. \A \$ i \$ j * x \$ j\)" ``` lp15@67719 ` 899` ``` by (rule sum_abs) ``` lp15@67719 ` 900` ``` also have "\ \ (\j\UNIV. \A \$ i \$ j\ * norm x)" ``` lp15@67719 ` 901` ``` by (rule sum_mono) (simp add: abs_mult component_le_norm_cart mult_left_mono) ``` lp15@67719 ` 902` ``` finally show "\(A *v x) \$ i\ \ (\j\UNIV. \A \$ i \$ j\ * norm x)" . ``` lp15@67719 ` 903` ``` qed ``` lp15@67719 ` 904` ``` finally show "norm (A *v x) \ (\i\UNIV. \j\UNIV. \A \$ i \$ j\) * norm x" ``` lp15@67719 ` 905` ``` by (simp add: sum_distrib_right) ``` lp15@67719 ` 906` ```qed ``` lp15@67719 ` 907` lp15@67719 ` 908` ```lemma onorm_le_matrix_component: ``` lp15@67719 ` 909` ``` fixes A :: "real^'n^'m" ``` lp15@67719 ` 910` ``` assumes "\i j. abs(A\$i\$j) \ B" ``` lp15@67719 ` 911` ``` shows "onorm(( *v) A) \ real (CARD('m)) * real (CARD('n)) * B" ``` lp15@67719 ` 912` ```proof (rule onorm_le) ``` wenzelm@67731 ` 913` ``` fix x :: "real^'n::_" ``` lp15@67719 ` 914` ``` have "norm (A *v x) \ (\i\UNIV. \(A *v x) \$ i\)" ``` lp15@67719 ` 915` ``` by (rule norm_le_l1_cart) ``` lp15@67719 ` 916` ``` also have "\ \ (\i::'m \UNIV. real (CARD('n)) * B * norm x)" ``` lp15@67719 ` 917` ``` proof (rule sum_mono) ``` lp15@67719 ` 918` ``` fix i ``` lp15@67719 ` 919` ``` have "\(A *v x) \$ i\ \ norm(A \$ i) * norm x" ``` lp15@67719 ` 920` ``` by (simp add: matrix_mult_dot Cauchy_Schwarz_ineq2) ``` lp15@67719 ` 921` ``` also have "\ \ (\j\UNIV. \A \$ i \$ j\) * norm x" ``` lp15@67719 ` 922` ``` by (simp add: mult_right_mono norm_le_l1_cart) ``` lp15@67719 ` 923` ``` also have "\ \ real (CARD('n)) * B * norm x" ``` lp15@67719 ` 924` ``` by (simp add: assms sum_bounded_above mult_right_mono) ``` lp15@67719 ` 925` ``` finally show "\(A *v x) \$ i\ \ real (CARD('n)) * B * norm x" . ``` lp15@67719 ` 926` ``` qed ``` lp15@67719 ` 927` ``` also have "\ \ CARD('m) * real (CARD('n)) * B * norm x" ``` lp15@67719 ` 928` ``` by simp ``` lp15@67719 ` 929` ``` finally show "norm (A *v x) \ CARD('m) * real (CARD('n)) * B * norm x" . ``` lp15@67719 ` 930` ```qed ``` lp15@67719 ` 931` lp15@67719 ` 932` ```subsection \lambda skolemization on cartesian products\ ``` hoelzl@37489 ` 933` hoelzl@37489 ` 934` ```lemma lambda_skolem: "(\i. \x. P i x) \ ``` hoelzl@37494 ` 935` ``` (\x::'a ^ 'n. \i. P i (x \$ i))" (is "?lhs \ ?rhs") ``` wenzelm@49644 ` 936` ```proof - ``` hoelzl@37489 ` 937` ``` let ?S = "(UNIV :: 'n set)" ``` wenzelm@49644 ` 938` ``` { assume H: "?rhs" ``` wenzelm@49644 ` 939` ``` then have ?lhs by auto } ``` hoelzl@37489 ` 940` ``` moreover ``` wenzelm@49644 ` 941` ``` { assume H: "?lhs" ``` hoelzl@37489 ` 942` ``` then obtain f where f:"\i. P i (f i)" unfolding choice_iff by metis ``` hoelzl@37489 ` 943` ``` let ?x = "(\ i. (f i)) :: 'a ^ 'n" ``` wenzelm@49644 ` 944` ``` { fix i ``` hoelzl@37489 ` 945` ``` from f have "P i (f i)" by metis ``` hoelzl@37494 ` 946` ``` then have "P i (?x \$ i)" by auto ``` hoelzl@37489 ` 947` ``` } ``` hoelzl@37489 ` 948` ``` hence "\i. P i (?x\$i)" by metis ``` hoelzl@37489 ` 949` ``` hence ?rhs by metis } ``` hoelzl@37489 ` 950` ``` ultimately show ?thesis by metis ``` hoelzl@37489 ` 951` ```qed ``` hoelzl@37489 ` 952` lp15@67719 ` 953` ```lemma rational_approximation: ``` lp15@67719 ` 954` ``` assumes "e > 0" ``` lp15@67719 ` 955` ``` obtains r::real where "r \ \" "\r - x\ < e" ``` lp15@67719 ` 956` ``` using Rats_dense_in_real [of "x - e/2" "x + e/2"] assms by auto ``` lp15@67719 ` 957` lp15@67719 ` 958` ```lemma matrix_rational_approximation: ``` lp15@67719 ` 959` ``` fixes A :: "real^'n^'m" ``` lp15@67719 ` 960` ``` assumes "e > 0" ``` lp15@67719 ` 961` ``` obtains B where "\i j. B\$i\$j \ \" "onorm(\x. (A - B) *v x) < e" ``` lp15@67719 ` 962` ```proof - ``` lp15@67719 ` 963` ``` have "\i j. \q \ \. \q - A \$ i \$ j\ < e / (2 * CARD('m) * CARD('n))" ``` lp15@67719 ` 964` ``` using assms by (force intro: rational_approximation [of "e / (2 * CARD('m) * CARD('n))"]) ``` lp15@67719 ` 965` ``` then obtain B where B: "\i j. B\$i\$j \ \" and Bclo: "\i j. \B\$i\$j - A \$ i \$ j\ < e / (2 * CARD('m) * CARD('n))" ``` lp15@67719 ` 966` ``` by (auto simp: lambda_skolem Bex_def) ``` lp15@67719 ` 967` ``` show ?thesis ``` lp15@67719 ` 968` ``` proof ``` lp15@67719 ` 969` ``` have "onorm (( *v) (A - B)) \ real CARD('m) * real CARD('n) * ``` lp15@67719 ` 970` ``` (e / (2 * real CARD('m) * real CARD('n)))" ``` lp15@67719 ` 971` ``` apply (rule onorm_le_matrix_component) ``` lp15@67719 ` 972` ``` using Bclo by (simp add: abs_minus_commute less_imp_le) ``` lp15@67719 ` 973` ``` also have "\ < e" ``` lp15@67719 ` 974` ``` using \0 < e\ by (simp add: divide_simps) ``` lp15@67719 ` 975` ``` finally show "onorm (( *v) (A - B)) < e" . ``` lp15@67719 ` 976` ``` qed (use B in auto) ``` lp15@67719 ` 977` ```qed ``` lp15@67719 ` 978` hoelzl@37489 ` 979` ```lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \ (x - ((b \ x) / (b \ b)) *s b) = 0" ``` hoelzl@50526 ` 980` ``` unfolding inner_simps scalar_mult_eq_scaleR by auto ``` hoelzl@37489 ` 981` hoelzl@37489 ` 982` ```lemma left_invertible_transpose: ``` hoelzl@37489 ` 983` ``` "(\(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" ``` hoelzl@37489 ` 984` ``` by (metis matrix_transpose_mul transpose_mat transpose_transpose) ``` hoelzl@37489 ` 985` hoelzl@37489 ` 986` ```lemma right_invertible_transpose: ``` hoelzl@37489 ` 987` ``` "(\(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(B). B ** A = mat 1)" ``` hoelzl@37489 ` 988` ``` by (metis matrix_transpose_mul transpose_mat transpose_transpose) ``` hoelzl@37489 ` 989` hoelzl@37489 ` 990` ```lemma matrix_left_invertible_injective: ``` lp15@67986 ` 991` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 992` ``` shows "(\B. B ** A = mat 1) \ inj (( *v) A)" ``` lp15@67986 ` 993` ```proof safe ``` lp15@67986 ` 994` ``` fix B ``` lp15@67986 ` 995` ``` assume B: "B ** A = mat 1" ``` lp15@67986 ` 996` ``` show "inj (( *v) A)" ``` lp15@67986 ` 997` ``` unfolding inj_on_def ``` lp15@67986 ` 998` ``` by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid) ``` lp15@67986 ` 999` ```next ``` lp15@67986 ` 1000` ``` assume "inj (( *v) A)" ``` lp15@67986 ` 1001` ``` with linear_injective_left_inverse[OF matrix_vector_mul_linear] ``` lp15@67986 ` 1002` ``` obtain g where "linear g" and g: "g \ ( *v) A = id" ``` lp15@67986 ` 1003` ``` by blast ``` lp15@67986 ` 1004` ``` have "matrix g ** A = mat 1" ``` lp15@67986 ` 1005` ``` by (metis \linear g\ g matrix_compose matrix_id_mat_1 matrix_of_matrix_vector_mul matrix_vector_mul_linear) ``` lp15@67986 ` 1006` ``` then show "\B. B ** A = mat 1" ``` lp15@67986 ` 1007` ``` by metis ``` hoelzl@37489 ` 1008` ```qed ``` hoelzl@37489 ` 1009` hoelzl@37489 ` 1010` ```lemma matrix_left_invertible_ker: ``` hoelzl@37489 ` 1011` ``` "(\B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x. A *v x = 0 \ x = 0)" ``` hoelzl@37489 ` 1012` ``` unfolding matrix_left_invertible_injective ``` hoelzl@37489 ` 1013` ``` using linear_injective_0[OF matrix_vector_mul_linear, of A] ``` hoelzl@37489 ` 1014` ``` by (simp add: inj_on_def) ``` hoelzl@37489 ` 1015` hoelzl@37489 ` 1016` ```lemma matrix_right_invertible_surjective: ``` wenzelm@49644 ` 1017` ``` "(\B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \ surj (\x. A *v x)" ``` wenzelm@49644 ` 1018` ```proof - ``` wenzelm@49644 ` 1019` ``` { fix B :: "real ^'m^'n" ``` wenzelm@49644 ` 1020` ``` assume AB: "A ** B = mat 1" ``` wenzelm@49644 ` 1021` ``` { fix x :: "real ^ 'm" ``` hoelzl@37489 ` 1022` ``` have "A *v (B *v x) = x" ``` wenzelm@49644 ` 1023` ``` by (simp add: matrix_vector_mul_lid matrix_vector_mul_assoc AB) } ``` nipkow@67399 ` 1024` ``` hence "surj (( *v) A)" unfolding surj_def by metis } ``` hoelzl@37489 ` 1025` ``` moreover ``` nipkow@67399 ` 1026` ``` { assume sf: "surj (( *v) A)" ``` hoelzl@37489 ` 1027` ``` from linear_surjective_right_inverse[OF matrix_vector_mul_linear sf] ``` nipkow@67399 ` 1028` ``` obtain g:: "real ^'m \ real ^'n" where g: "linear g" "( *v) A \ g = id" ``` hoelzl@37489 ` 1029` ``` by blast ``` hoelzl@37489 ` 1030` hoelzl@37489 ` 1031` ``` have "A ** (matrix g) = mat 1" ``` hoelzl@37489 ` 1032` ``` unfolding matrix_eq matrix_vector_mul_lid ``` hoelzl@37489 ` 1033` ``` matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] ``` huffman@44165 ` 1034` ``` using g(2) unfolding o_def fun_eq_iff id_def ``` hoelzl@37489 ` 1035` ``` . ``` hoelzl@37489 ` 1036` ``` hence "\B. A ** (B::real^'m^'n) = mat 1" by blast ``` hoelzl@37489 ` 1037` ``` } ``` hoelzl@37489 ` 1038` ``` ultimately show ?thesis unfolding surj_def by blast ``` hoelzl@37489 ` 1039` ```qed ``` hoelzl@37489 ` 1040` hoelzl@37489 ` 1041` ```lemma matrix_left_invertible_independent_columns: ``` hoelzl@37489 ` 1042` ``` fixes A :: "real^'n^'m" ``` wenzelm@49644 ` 1043` ``` shows "(\(B::real ^'m^'n). B ** A = mat 1) \ ``` nipkow@64267 ` 1044` ``` (\c. sum (\i. c i *s column i A) (UNIV :: 'n set) = 0 \ (\i. c i = 0))" ``` wenzelm@49644 ` 1045` ``` (is "?lhs \ ?rhs") ``` wenzelm@49644 ` 1046` ```proof - ``` hoelzl@37489 ` 1047` ``` let ?U = "UNIV :: 'n set" ``` wenzelm@49644 ` 1048` ``` { assume k: "\x. A *v x = 0 \ x = 0" ``` wenzelm@49644 ` 1049` ``` { fix c i ``` nipkow@64267 ` 1050` ``` assume c: "sum (\i. c i *s column i A) ?U = 0" and i: "i \ ?U" ``` hoelzl@37489 ` 1051` ``` let ?x = "\ i. c i" ``` hoelzl@37489 ` 1052` ``` have th0:"A *v ?x = 0" ``` hoelzl@37489 ` 1053` ``` using c ``` lp15@67673 ` 1054` ``` unfolding matrix_mult_sum vec_eq_iff ``` hoelzl@37489 ` 1055` ``` by auto ``` hoelzl@37489 ` 1056` ``` from k[rule_format, OF th0] i ``` huffman@44136 ` 1057` ``` have "c i = 0" by (vector vec_eq_iff)} ``` wenzelm@49644 ` 1058` ``` hence ?rhs by blast } ``` hoelzl@37489 ` 1059` ``` moreover ``` wenzelm@49644 ` 1060` ``` { assume H: ?rhs ``` wenzelm@49644 ` 1061` ``` { fix x assume x: "A *v x = 0" ``` hoelzl@37489 ` 1062` ``` let ?c = "\i. ((x\$i ):: real)" ``` lp15@67673 ` 1063` ``` from H[rule_format, of ?c, unfolded matrix_mult_sum[symmetric], OF x] ``` wenzelm@49644 ` 1064` ``` have "x = 0" by vector } ``` wenzelm@49644 ` 1065` ``` } ``` hoelzl@37489 ` 1066` ``` ultimately show ?thesis unfolding matrix_left_invertible_ker by blast ``` hoelzl@37489 ` 1067` ```qed ``` hoelzl@37489 ` 1068` hoelzl@37489 ` 1069` ```lemma matrix_right_invertible_independent_rows: ``` hoelzl@37489 ` 1070` ``` fixes A :: "real^'n^'m" ``` wenzelm@49644 ` 1071` ``` shows "(\(B::real^'m^'n). A ** B = mat 1) \ ``` nipkow@64267 ` 1072` ``` (\c. sum (\i. c i *s row i A) (UNIV :: 'm set) = 0 \ (\i. c i = 0))" ``` hoelzl@37489 ` 1073` ``` unfolding left_invertible_transpose[symmetric] ``` hoelzl@37489 ` 1074` ``` matrix_left_invertible_independent_columns ``` hoelzl@37489 ` 1075` ``` by (simp add: column_transpose) ``` hoelzl@37489 ` 1076` hoelzl@37489 ` 1077` ```lemma matrix_right_invertible_span_columns: ``` wenzelm@49644 ` 1078` ``` "(\(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \ ``` wenzelm@49644 ` 1079` ``` span (columns A) = UNIV" (is "?lhs = ?rhs") ``` wenzelm@49644 ` 1080` ```proof - ``` hoelzl@37489 ` 1081` ``` let ?U = "UNIV :: 'm set" ``` hoelzl@37489 ` 1082` ``` have fU: "finite ?U" by simp ``` nipkow@64267 ` 1083` ``` have lhseq: "?lhs \ (\y. \(x::real^'m). sum (\i. (x\$i) *s column i A) ?U = y)" ``` lp15@67673 ` 1084` ``` unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def ``` lp15@68041 ` 1085` ``` by (simp add: eq_commute) ``` hoelzl@37489 ` 1086` ``` have rhseq: "?rhs \ (\x. x \ span (columns A))" by blast ``` wenzelm@49644 ` 1087` ``` { assume h: ?lhs ``` wenzelm@49644 ` 1088` ``` { fix x:: "real ^'n" ``` wenzelm@49644 ` 1089` ``` from h[unfolded lhseq, rule_format, of x] obtain y :: "real ^'m" ``` nipkow@64267 ` 1090` ``` where y: "sum (\i. (y\$i) *s column i A) ?U = x" by blast ``` wenzelm@49644 ` 1091` ``` have "x \ span (columns A)" ``` lp15@68041 ` 1092` ``` unfolding y[symmetric] scalar_mult_eq_scaleR ``` lp15@68041 ` 1093` ``` proof (rule span_sum [OF span_mul]) ``` lp15@68041 ` 1094` ``` show "column i A \ span (columns A)" for i ``` lp15@68041 ` 1095` ``` using columns_def span_inc by auto ``` lp15@68041 ` 1096` ``` qed ``` wenzelm@49644 ` 1097` ``` } ``` wenzelm@49644 ` 1098` ``` then have ?rhs unfolding rhseq by blast } ``` hoelzl@37489 ` 1099` ``` moreover ``` wenzelm@49644 ` 1100` ``` { assume h:?rhs ``` nipkow@64267 ` 1101` ``` let ?P = "\(y::real ^'n). \(x::real^'m). sum (\i. (x\$i) *s column i A) ?U = y" ``` wenzelm@49644 ` 1102` ``` { fix y ``` lp15@68069 ` 1103` ``` have "y \ span (columns A)" ``` lp15@68069 ` 1104` ``` using h by auto ``` lp15@68069 ` 1105` ``` then have "?P y" ``` lp15@68069 ` 1106` ``` proof (induction rule: span_induct_alt) ``` lp15@68069 ` 1107` ``` case base ``` lp15@68069 ` 1108` ``` then show ?case ``` lp15@68069 ` 1109` ``` by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right) ``` hoelzl@37489 ` 1110` ``` next ``` lp15@68069 ` 1111` ``` case (step c y1 y2) ``` lp15@68069 ` 1112` ``` then obtain i where i: "i \ ?U" "y1 = column i A" ``` hoelzl@37489 ` 1113` ``` unfolding columns_def by blast ``` lp15@68069 ` 1114` ``` obtain x:: "real ^'m" where x: "sum (\i. (x\$i) *s column i A) ?U = y2" ``` lp15@68069 ` 1115` ``` using step by blast ``` hoelzl@37489 ` 1116` ``` let ?x = "(\ j. if j = i then c + (x\$i) else (x\$j))::real^'m" ``` lp15@68069 ` 1117` ``` show ?case ``` webertj@49962 ` 1118` ``` 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 ` 1119` ``` fix j ``` wenzelm@49644 ` 1120` ``` have th: "\xa \ ?U. (if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` wenzelm@49644 ` 1121` ``` 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 ` 1122` ``` using i(1) by (simp add: field_simps) ``` nipkow@64267 ` 1123` ``` have "sum (\xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` nipkow@64267 ` 1124` ``` else (x\$xa) * ((column xa A\$j))) ?U = sum (\xa. (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))) ?U" ``` lp15@68041 ` 1125` ``` by (rule sum.cong[OF refl]) (use th in blast) ``` nipkow@64267 ` 1126` ``` also have "\ = sum (\xa. if xa = i then c * ((column i A)\$j) else 0) ?U + sum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" ``` nipkow@64267 ` 1127` ``` by (simp add: sum.distrib) ``` nipkow@64267 ` 1128` ``` also have "\ = c * ((column i A)\$j) + sum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" ``` nipkow@64267 ` 1129` ``` unfolding sum.delta[OF fU] ``` wenzelm@49644 ` 1130` ``` using i(1) by simp ``` nipkow@64267 ` 1131` ``` finally show "sum (\xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` nipkow@64267 ` 1132` ``` else (x\$xa) * ((column xa A\$j))) ?U = c * ((column i A)\$j) + sum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" . ``` wenzelm@49644 ` 1133` ``` qed ``` wenzelm@49644 ` 1134` ``` qed ``` wenzelm@49644 ` 1135` ``` } ``` wenzelm@49644 ` 1136` ``` then have ?lhs unfolding lhseq .. ``` wenzelm@49644 ` 1137` ``` } ``` hoelzl@37489 ` 1138` ``` ultimately show ?thesis by blast ``` hoelzl@37489 ` 1139` ```qed ``` hoelzl@37489 ` 1140` hoelzl@37489 ` 1141` ```lemma matrix_left_invertible_span_rows: ``` hoelzl@37489 ` 1142` ``` "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" ``` hoelzl@37489 ` 1143` ``` unfolding right_invertible_transpose[symmetric] ``` hoelzl@37489 ` 1144` ``` unfolding columns_transpose[symmetric] ``` hoelzl@37489 ` 1145` ``` unfolding matrix_right_invertible_span_columns ``` wenzelm@49644 ` 1146` ``` .. ``` hoelzl@37489 ` 1147` wenzelm@60420 ` 1148` ```text \The same result in terms of square matrices.\ ``` hoelzl@37489 ` 1149` hoelzl@37489 ` 1150` ```lemma matrix_left_right_inverse: ``` hoelzl@37489 ` 1151` ``` fixes A A' :: "real ^'n^'n" ``` hoelzl@37489 ` 1152` ``` shows "A ** A' = mat 1 \ A' ** A = mat 1" ``` wenzelm@49644 ` 1153` ```proof - ``` wenzelm@49644 ` 1154` ``` { fix A A' :: "real ^'n^'n" ``` wenzelm@49644 ` 1155` ``` assume AA': "A ** A' = mat 1" ``` nipkow@67399 ` 1156` ``` have sA: "surj (( *v) A)" ``` lp15@68038 ` 1157` ``` using AA' matrix_right_invertible_surjective by auto ``` hoelzl@37489 ` 1158` ``` from linear_surjective_isomorphism[OF matrix_vector_mul_linear sA] ``` hoelzl@37489 ` 1159` ``` obtain f' :: "real ^'n \ real ^'n" ``` hoelzl@37489 ` 1160` ``` where f': "linear f'" "\x. f' (A *v x) = x" "\x. A *v f' x = x" by blast ``` hoelzl@37489 ` 1161` ``` have th: "matrix f' ** A = mat 1" ``` wenzelm@49644 ` 1162` ``` by (simp add: matrix_eq matrix_works[OF f'(1)] ``` lp15@68041 ` 1163` ``` matrix_vector_mul_assoc[symmetric] f'(2)[rule_format]) ``` hoelzl@37489 ` 1164` ``` hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp ``` wenzelm@49644 ` 1165` ``` hence "matrix f' = A'" ``` lp15@68041 ` 1166` ``` by (simp add: matrix_mul_assoc[symmetric] AA') ``` hoelzl@37489 ` 1167` ``` hence "matrix f' ** A = A' ** A" by simp ``` wenzelm@49644 ` 1168` ``` hence "A' ** A = mat 1" by (simp add: th) ``` wenzelm@49644 ` 1169` ``` } ``` hoelzl@37489 ` 1170` ``` then show ?thesis by blast ``` hoelzl@37489 ` 1171` ```qed ``` hoelzl@37489 ` 1172` lp15@68038 ` 1173` ```lemma invertible_mult: ``` lp15@68045 ` 1174` ``` assumes inv_A: "invertible A" ``` lp15@68045 ` 1175` ``` and inv_B: "invertible B" ``` lp15@68045 ` 1176` ``` shows "invertible (A**B)" ``` lp15@68045 ` 1177` ```proof - ``` lp15@68045 ` 1178` ``` obtain A' where AA': "A ** A' = mat 1" and A'A: "A' ** A = mat 1" ``` lp15@68045 ` 1179` ``` using inv_A unfolding invertible_def by blast ``` lp15@68045 ` 1180` ``` obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1" ``` lp15@68045 ` 1181` ``` using inv_B unfolding invertible_def by blast ``` lp15@68045 ` 1182` ``` show ?thesis ``` lp15@68045 ` 1183` ``` proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI) ``` lp15@68045 ` 1184` ``` have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))" ``` lp15@68045 ` 1185` ``` using matrix_mul_assoc[of A B "(B' ** A')", symmetric] . ``` lp15@68045 ` 1186` ``` also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] .. ``` lp15@68045 ` 1187` ``` also have "... = A ** (mat 1 ** A')" unfolding BB' .. ``` lp15@68045 ` 1188` ``` also have "... = A ** A'" unfolding matrix_mul_lid .. ``` lp15@68045 ` 1189` ``` also have "... = mat 1" unfolding AA' .. ``` lp15@68045 ` 1190` ``` finally show "A ** B ** (B' ** A') = mat (1::'a)" . ``` lp15@68045 ` 1191` ``` have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] . ``` lp15@68045 ` 1192` ``` also have "... = B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] .. ``` lp15@68045 ` 1193` ``` also have "... = B' ** (mat 1 ** B)" unfolding A'A .. ``` lp15@68045 ` 1194` ``` also have "... = B' ** B" unfolding matrix_mul_lid .. ``` lp15@68045 ` 1195` ``` also have "... = mat 1" unfolding B'B .. ``` lp15@68045 ` 1196` ``` finally show "B' ** A' ** (A ** B) = mat 1" . ``` lp15@68045 ` 1197` ``` qed ``` lp15@68045 ` 1198` ```qed ``` lp15@68038 ` 1199` lp15@68038 ` 1200` ```lemma transpose_invertible: ``` lp15@68038 ` 1201` ``` fixes A :: "real^'n^'n" ``` lp15@68038 ` 1202` ``` assumes "invertible A" ``` lp15@68038 ` 1203` ``` shows "invertible (transpose A)" ``` lp15@68038 ` 1204` ``` by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose) ``` lp15@68038 ` 1205` lp15@68041 ` 1206` ```lemma vector_matrix_mul_assoc: ``` lp15@68041 ` 1207` ``` fixes v :: "('a::comm_semiring_1)^'n" ``` lp15@68041 ` 1208` ``` shows "(v v* M) v* N = v v* (M ** N)" ``` lp15@68041 ` 1209` ```proof - ``` lp15@68041 ` 1210` ``` from matrix_vector_mul_assoc ``` lp15@68041 ` 1211` ``` have "transpose N *v (transpose M *v v) = (transpose N ** transpose M) *v v" by fast ``` lp15@68041 ` 1212` ``` thus "(v v* M) v* N = v v* (M ** N)" ``` lp15@68041 ` 1213` ``` by (simp add: matrix_transpose_mul [symmetric]) ``` lp15@68041 ` 1214` ```qed ``` lp15@68041 ` 1215` lp15@68043 ` 1216` ```lemma matrix_scaleR_vector_ac: ``` lp15@68041 ` 1217` ``` fixes A :: "real^('m::finite)^'n" ``` lp15@68041 ` 1218` ``` shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v" ``` lp15@68043 ` 1219` ``` by (metis matrix_vector_mult_scaleR transpose_scalar vector_scaleR_matrix_ac vector_transpose_matrix) ``` lp15@68041 ` 1220` lp15@68043 ` 1221` ```lemma scaleR_matrix_vector_assoc: ``` lp15@68041 ` 1222` ``` fixes A :: "real^('m::finite)^'n" ``` lp15@68041 ` 1223` ``` shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v" ``` lp15@68043 ` 1224` ``` by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR) ``` lp15@68041 ` 1225` wenzelm@60420 ` 1226` ```text \Considering an n-element vector as an n-by-1 or 1-by-n matrix.\ ``` hoelzl@37489 ` 1227` hoelzl@37489 ` 1228` ```definition "rowvector v = (\ i j. (v\$j))" ``` hoelzl@37489 ` 1229` hoelzl@37489 ` 1230` ```definition "columnvector v = (\ i j. (v\$i))" ``` hoelzl@37489 ` 1231` wenzelm@49644 ` 1232` ```lemma transpose_columnvector: "transpose(columnvector v) = rowvector v" ``` huffman@44136 ` 1233` ``` by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff) ``` hoelzl@37489 ` 1234` hoelzl@37489 ` 1235` ```lemma transpose_rowvector: "transpose(rowvector v) = columnvector v" ``` huffman@44136 ` 1236` ``` by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff) ``` hoelzl@37489 ` 1237` wenzelm@49644 ` 1238` ```lemma dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" ``` hoelzl@37489 ` 1239` ``` by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) ``` hoelzl@37489 ` 1240` wenzelm@49644 ` 1241` ```lemma dot_matrix_product: ``` wenzelm@49644 ` 1242` ``` "(x::real^'n) \ y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))\$1)\$1" ``` huffman@44136 ` 1243` ``` by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def) ``` hoelzl@37489 ` 1244` hoelzl@37489 ` 1245` ```lemma dot_matrix_vector_mul: ``` hoelzl@37489 ` 1246` ``` fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" ``` hoelzl@37489 ` 1247` ``` shows "(A *v x) \ (B *v y) = ``` hoelzl@37489 ` 1248` ``` (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))\$1)\$1" ``` wenzelm@49644 ` 1249` ``` unfolding dot_matrix_product transpose_columnvector[symmetric] ``` wenzelm@49644 ` 1250` ``` dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc .. ``` hoelzl@37489 ` 1251` wenzelm@61945 ` 1252` ```lemma infnorm_cart:"infnorm (x::real^'n) = Sup {\x\$i\ |i. i\UNIV}" ``` hoelzl@50526 ` 1253` ``` by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right) ``` hoelzl@37489 ` 1254` wenzelm@49644 ` 1255` ```lemma component_le_infnorm_cart: "\x\$i\ \ infnorm (x::real^'n)" ``` hoelzl@50526 ` 1256` ``` using Basis_le_infnorm[of "axis i 1" x] ``` hoelzl@50526 ` 1257` ``` by (simp add: Basis_vec_def axis_eq_axis inner_axis) ``` hoelzl@37489 ` 1258` hoelzl@63334 ` 1259` ```lemma continuous_component[continuous_intros]: "continuous F f \ continuous F (\x. f x \$ i)" ``` huffman@44647 ` 1260` ``` unfolding continuous_def by (rule tendsto_vec_nth) ``` huffman@44213 ` 1261` hoelzl@63334 ` 1262` ```lemma continuous_on_component[continuous_intros]: "continuous_on s f \ continuous_on s (\x. f x \$ i)" ``` huffman@44647 ` 1263` ``` unfolding continuous_on_def by (fast intro: tendsto_vec_nth) ``` huffman@44213 ` 1264` hoelzl@63334 ` 1265` ```lemma continuous_on_vec_lambda[continuous_intros]: ``` hoelzl@63334 ` 1266` ``` "(\i. continuous_on S (f i)) \ continuous_on S (\x. \ i. f i x)" ``` hoelzl@63334 ` 1267` ``` unfolding continuous_on_def by (auto intro: tendsto_vec_lambda) ``` hoelzl@63334 ` 1268` hoelzl@37489 ` 1269` ```lemma closed_positive_orthant: "closed {x::real^'n. \i. 0 \x\$i}" ``` hoelzl@63332 ` 1270` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) ``` huffman@44213 ` 1271` hoelzl@37489 ` 1272` ```lemma bounded_component_cart: "bounded s \ bounded ((\x. x \$ i) ` s)" ``` wenzelm@49644 ` 1273` ``` unfolding bounded_def ``` wenzelm@49644 ` 1274` ``` apply clarify ``` wenzelm@49644 ` 1275` ``` apply (rule_tac x="x \$ i" in exI) ``` wenzelm@49644 ` 1276` ``` apply (rule_tac x="e" in exI) ``` wenzelm@49644 ` 1277` ``` apply clarify ``` wenzelm@49644 ` 1278` ``` apply (rule order_trans [OF dist_vec_nth_le], simp) ``` wenzelm@49644 ` 1279` ``` done ``` hoelzl@37489 ` 1280` hoelzl@37489 ` 1281` ```lemma compact_lemma_cart: ``` hoelzl@37489 ` 1282` ``` fixes f :: "nat \ 'a::heine_borel ^ 'n" ``` hoelzl@50998 ` 1283` ``` assumes f: "bounded (range f)" ``` eberlm@66447 ` 1284` ``` shows "\l r. strict_mono r \ ``` hoelzl@37489 ` 1285` ``` (\e>0. eventually (\n. \i\d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)" ``` immler@62127 ` 1286` ``` (is "?th d") ``` immler@62127 ` 1287` ```proof - ``` immler@62127 ` 1288` ``` have "\d' \ d. ?th d'" ``` immler@62127 ` 1289` ``` by (rule compact_lemma_general[where unproj=vec_lambda]) ``` immler@62127 ` 1290` ``` (auto intro!: f bounded_component_cart simp: vec_lambda_eta) ``` immler@62127 ` 1291` ``` then show "?th d" by simp ``` hoelzl@37489 ` 1292` ```qed ``` hoelzl@37489 ` 1293` huffman@44136 ` 1294` ```instance vec :: (heine_borel, finite) heine_borel ``` hoelzl@37489 ` 1295` ```proof ``` hoelzl@50998 ` 1296` ``` fix f :: "nat \ 'a ^ 'b" ``` hoelzl@50998 ` 1297` ``` assume f: "bounded (range f)" ``` eberlm@66447 ` 1298` ``` then obtain l r where r: "strict_mono r" ``` wenzelm@49644 ` 1299` ``` and l: "\e>0. eventually (\n. \i\UNIV. dist (f (r n) \$ i) (l \$ i) < e) sequentially" ``` hoelzl@50998 ` 1300` ``` using compact_lemma_cart [OF f] by blast ``` hoelzl@37489 ` 1301` ``` let ?d = "UNIV::'b set" ``` hoelzl@37489 ` 1302` ``` { fix e::real assume "e>0" ``` hoelzl@37489 ` 1303` ``` hence "0 < e / (real_of_nat (card ?d))" ``` wenzelm@49644 ` 1304` ``` using zero_less_card_finite divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto ``` hoelzl@37489 ` 1305` ``` with l have "eventually (\n. \i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))) sequentially" ``` hoelzl@37489 ` 1306` ``` by simp ``` hoelzl@37489 ` 1307` ``` moreover ``` wenzelm@49644 ` 1308` ``` { fix n ``` wenzelm@49644 ` 1309` ``` assume n: "\i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))" ``` hoelzl@37489 ` 1310` ``` have "dist (f (r n)) l \ (\i\?d. dist (f (r n) \$ i) (l \$ i))" ``` nipkow@67155 ` 1311` ``` unfolding dist_vec_def using zero_le_dist by (rule L2_set_le_sum) ``` hoelzl@37489 ` 1312` ``` also have "\ < (\i\?d. e / (real_of_nat (card ?d)))" ``` nipkow@64267 ` 1313` ``` by (rule sum_strict_mono) (simp_all add: n) ``` hoelzl@37489 ` 1314` ``` finally have "dist (f (r n)) l < e" by simp ``` hoelzl@37489 ` 1315` ``` } ``` hoelzl@37489 ` 1316` ``` ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" ``` lp15@61810 ` 1317` ``` by (rule eventually_mono) ``` hoelzl@37489 ` 1318` ``` } ``` wenzelm@61973 ` 1319` ``` hence "((f \ r) \ l) sequentially" unfolding o_def tendsto_iff by simp ``` eberlm@66447 ` 1320` ``` with r show "\l r. strict_mono r \ ((f \ r) \ l) sequentially" by auto ``` hoelzl@37489 ` 1321` ```qed ``` hoelzl@37489 ` 1322` wenzelm@49644 ` 1323` ```lemma interval_cart: ``` immler@54775 ` 1324` ``` fixes a :: "real^'n" ``` immler@54775 ` 1325` ``` shows "box a b = {x::real^'n. \i. a\$i < x\$i \ x\$i < b\$i}" ``` immler@56188 ` 1326` ``` and "cbox a b = {x::real^'n. \i. a\$i \ x\$i \ x\$i \ b\$i}" ``` immler@56188 ` 1327` ``` by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def mem_box Basis_vec_def inner_axis) ``` hoelzl@37489 ` 1328` lp15@67673 ` 1329` ```lemma mem_box_cart: ``` immler@54775 ` 1330` ``` fixes a :: "real^'n" ``` immler@54775 ` 1331` ``` shows "x \ box a b \ (\i. a\$i < x\$i \ x\$i < b\$i)" ``` immler@56188 ` 1332` ``` and "x \ cbox a b \ (\i. a\$i \ x\$i \ x\$i \ b\$i)" ``` wenzelm@49644 ` 1333` ``` using interval_cart[of a b] by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def) ``` hoelzl@37489 ` 1334` wenzelm@49644 ` 1335` ```lemma interval_eq_empty_cart: ``` wenzelm@49644 ` 1336` ``` fixes a :: "real^'n" ``` immler@54775 ` 1337` ``` shows "(box a b = {} \ (\i. b\$i \ a\$i))" (is ?th1) ``` immler@56188 ` 1338` ``` and "(cbox a b = {} \ (\i. b\$i < a\$i))" (is ?th2) ``` wenzelm@49644 ` 1339` ```proof - ``` immler@54775 ` 1340` ``` { fix i x assume as:"b\$i \ a\$i" and x:"x\box a b" ``` lp15@67673 ` 1341` ``` hence "a \$ i < x \$ i \ x \$ i < b \$ i" unfolding mem_box_cart by auto ``` hoelzl@37489 ` 1342` ``` hence "a\$i < b\$i" by auto ``` wenzelm@49644 ` 1343` ``` hence False using as by auto } ``` hoelzl@37489 ` 1344` ``` moreover ``` hoelzl@37489 ` 1345` ``` { assume as:"\i. \ (b\$i \ a\$i)" ``` hoelzl@37489 ` 1346` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` hoelzl@37489 ` 1347` ``` { fix i ``` hoelzl@37489 ` 1348` ``` have "a\$i < b\$i" using as[THEN spec[where x=i]] by auto ``` hoelzl@37489 ` 1349` ``` hence "a\$i < ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i < b\$i" ``` hoelzl@37489 ` 1350` ``` unfolding vector_smult_component and vector_add_component ``` wenzelm@49644 ` 1351` ``` by auto } ``` lp15@67673 ` 1352` ``` hence "box a b \ {}" using mem_box_cart(1)[of "?x" a b] by auto } ``` hoelzl@37489 ` 1353` ``` ultimately show ?th1 by blast ``` hoelzl@37489 ` 1354` immler@56188 ` 1355` ``` { fix i x assume as:"b\$i < a\$i" and x:"x\cbox a b" ``` lp15@67673 ` 1356` ``` hence "a \$ i \ x \$ i \ x \$ i \ b \$ i" unfolding mem_box_cart by auto ``` hoelzl@37489 ` 1357` ``` hence "a\$i \ b\$i" by auto ``` wenzelm@49644 ` 1358` ``` hence False using as by auto } ``` hoelzl@37489 ` 1359` ``` moreover ``` hoelzl@37489 ` 1360` ``` { assume as:"\i. \ (b\$i < a\$i)" ``` hoelzl@37489 ` 1361` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` hoelzl@37489 ` 1362` ``` { fix i ``` hoelzl@37489 ` 1363` ``` have "a\$i \ b\$i" using as[THEN spec[where x=i]] by auto ``` hoelzl@37489 ` 1364` ``` hence "a\$i \ ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i \ b\$i" ``` hoelzl@37489 ` 1365` ``` unfolding vector_smult_component and vector_add_component ``` wenzelm@49644 ` 1366` ``` by auto } ``` lp15@67673 ` 1367` ``` hence "cbox a b \ {}" using mem_box_cart(2)[of "?x" a b] by auto } ``` hoelzl@37489 ` 1368` ``` ultimately show ?th2 by blast ``` hoelzl@37489 ` 1369` ```qed ``` hoelzl@37489 ` 1370` wenzelm@49644 ` 1371` ```lemma interval_ne_empty_cart: ``` wenzelm@49644 ` 1372` ``` fixes a :: "real^'n" ``` immler@56188 ` 1373` ``` shows "cbox a b \ {} \ (\i. a\$i \ b\$i)" ``` immler@54775 ` 1374` ``` and "box a b \ {} \ (\i. a\$i < b\$i)" ``` hoelzl@37489 ` 1375` ``` unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le) ``` hoelzl@37489 ` 1376` ``` (* BH: Why doesn't just "auto" work here? *) ``` hoelzl@37489 ` 1377` wenzelm@49644 ` 1378` ```lemma subset_interval_imp_cart: ``` wenzelm@49644 ` 1379` ``` fixes a :: "real^'n" ``` immler@56188 ` 1380` ``` shows "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ cbox c d \ cbox a b" ``` immler@56188 ` 1381` ``` and "(\i. a\$i < c\$i \ d\$i < b\$i) \ cbox c d \ box a b" ``` immler@56188 ` 1382` ``` and "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ box c d \ cbox a b" ``` immler@54775 ` 1383` ``` and "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ box c d \ box a b" ``` lp15@67673 ` 1384` ``` unfolding subset_eq[unfolded Ball_def] unfolding mem_box_cart ``` hoelzl@37489 ` 1385` ``` by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *) ``` hoelzl@37489 ` 1386` wenzelm@49644 ` 1387` ```lemma interval_sing: ``` wenzelm@49644 ` 1388` ``` fixes a :: "'a::linorder^'n" ``` wenzelm@49644 ` 1389` ``` shows "{a .. a} = {a} \ {a<.. cbox a b \ (\i. c\$i \ d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th1) ``` immler@56188 ` 1396` ``` and "cbox c d \ box a b \ (\i. c\$i \ d\$i) --> (\i. a\$i < c\$i \ d\$i < b\$i)" (is ?th2) ``` immler@56188 ` 1397` ``` and "box c d \ cbox a b \ (\i. c\$i < d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th3) ``` immler@54775 ` 1398` ``` and "box c d \ box a b \ (\i. c\$i < d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th4) ``` immler@56188 ` 1399` ``` using subset_box[of c d a b] by (simp_all add: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 1400` wenzelm@49644 ` 1401` ```lemma disjoint_interval_cart: ``` wenzelm@49644 ` 1402` ``` fixes a::"real^'n" ``` immler@56188 ` 1403` ``` shows "cbox a b \ cbox c d = {} \ (\i. (b\$i < a\$i \ d\$i < c\$i \ b\$i < c\$i \ d\$i < a\$i))" (is ?th1) ``` immler@56188 ` 1404` ``` and "cbox a b \ box c d = {} \ (\i. (b\$i < a\$i \ d\$i \ c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th2) ``` immler@56188 ` 1405` ``` and "box a b \ cbox c d = {} \ (\i. (b\$i \ a\$i \ d\$i < c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th3) ``` immler@54775 ` 1406` ``` and "box a b \ box c d = {} \ (\i. (b\$i \ a\$i \ d\$i \ c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th4) ``` hoelzl@50526 ` 1407` ``` using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 1408` lp15@67719 ` 1409` ```lemma Int_interval_cart: ``` immler@54775 ` 1410` ``` fixes a :: "real^'n" ``` immler@56188 ` 1411` ``` shows "cbox a b \ cbox c d = {(\ i. max (a\$i) (c\$i)) .. (\ i. min (b\$i) (d\$i))}" ``` lp15@63945 ` 1412` ``` unfolding Int_interval ``` immler@56188 ` 1413` ``` by (auto simp: mem_box less_eq_vec_def) ``` immler@56188 ` 1414` ``` (auto simp: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 1415` wenzelm@49644 ` 1416` ```lemma closed_interval_left_cart: ``` wenzelm@49644 ` 1417` ``` fixes b :: "real^'n" ``` hoelzl@37489 ` 1418` ``` shows "closed {x::real^'n. \i. x\$i \ b\$i}" ``` hoelzl@63332 ` 1419` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) ``` hoelzl@37489 ` 1420` wenzelm@49644 ` 1421` ```lemma closed_interval_right_cart: ``` wenzelm@49644 ` 1422` ``` fixes a::"real^'n" ``` hoelzl@37489 ` 1423` ``` shows "closed {x::real^'n. \i. a\$i \ x\$i}" ``` hoelzl@63332 ` 1424` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) ``` hoelzl@37489 ` 1425` wenzelm@49644 ` 1426` ```lemma is_interval_cart: ``` wenzelm@49644 ` 1427` ``` "is_interval (s::(real^'n) set) \ ``` wenzelm@49644 ` 1428` ``` (\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 ` 1429` ``` by (simp add: is_interval_def Ball_def Basis_vec_def inner_axis imp_ex) ``` hoelzl@37489 ` 1430` wenzelm@49644 ` 1431` ```lemma closed_halfspace_component_le_cart: "closed {x::real^'n. x\$i \ a}" ``` hoelzl@63332 ` 1432` ``` by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) ``` hoelzl@37489 ` 1433` wenzelm@49644 ` 1434` ```lemma closed_halfspace_component_ge_cart: "closed {x::real^'n. x\$i \ a}" ``` hoelzl@63332 ` 1435` ``` by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) ``` hoelzl@37489 ` 1436` wenzelm@49644 ` 1437` ```lemma open_halfspace_component_lt_cart: "open {x::real^'n. x\$i < a}" ``` hoelzl@63332 ` 1438` ``` by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component) ``` wenzelm@49644 ` 1439` wenzelm@49644 ` 1440` ```lemma open_halfspace_component_gt_cart: "open {x::real^'n. x\$i > a}" ``` hoelzl@63332 ` 1441` ``` by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component) ``` hoelzl@37489 ` 1442` wenzelm@49644 ` 1443` ```lemma Lim_component_le_cart: ``` wenzelm@49644 ` 1444` ``` fixes f :: "'a \ real^'n" ``` wenzelm@61973 ` 1445` ``` assumes "(f \ l) net" "\ (trivial_limit net)" "eventually (\x. f x \$i \ b) net" ``` hoelzl@37489 ` 1446` ``` shows "l\$i \ b" ``` hoelzl@50526 ` 1447` ``` by (rule tendsto_le[OF assms(2) tendsto_const tendsto_vec_nth, OF assms(1, 3)]) ``` hoelzl@37489 ` 1448` wenzelm@49644 ` 1449` ```lemma Lim_component_ge_cart: ``` wenzelm@49644 ` 1450` ``` fixes f :: "'a \ real^'n" ``` wenzelm@61973 ` 1451` ``` assumes "(f \ l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)\$i) net" ``` hoelzl@37489 ` 1452` ``` shows "b \ l\$i" ``` hoelzl@50526 ` 1453` ``` by (rule tendsto_le[OF assms(2) tendsto_vec_nth tendsto_const, OF assms(1, 3)]) ``` hoelzl@37489 ` 1454` wenzelm@49644 ` 1455` ```lemma Lim_component_eq_cart: ``` wenzelm@49644 ` 1456` ``` fixes f :: "'a \ real^'n" ``` wenzelm@61973 ` 1457` ``` assumes net: "(f \ l) net" "~(trivial_limit net)" and ev:"eventually (\x. f(x)\$i = b) net" ``` hoelzl@37489 ` 1458` ``` shows "l\$i = b" ``` wenzelm@49644 ` 1459` ``` using ev[unfolded order_eq_iff eventually_conj_iff] and ``` wenzelm@49644 ` 1460` ``` Lim_component_ge_cart[OF net, of b i] and ``` hoelzl@37489 ` 1461` ``` Lim_component_le_cart[OF net, of i b] by auto ``` hoelzl@37489 ` 1462` wenzelm@49644 ` 1463` ```lemma connected_ivt_component_cart: ``` wenzelm@49644 ` 1464` ``` fixes x :: "real^'n" ``` wenzelm@49644 ` 1465` ``` shows "connected s \ x \ s \ y \ s \ x\$k \ a \ a \ y\$k \ (\z\s. z\$k = a)" ``` hoelzl@50526 ` 1466` ``` using connected_ivt_hyperplane[of s x y "axis k 1" a] ``` hoelzl@50526 ` 1467` ``` by (auto simp add: inner_axis inner_commute) ``` hoelzl@37489 ` 1468` wenzelm@49644 ` 1469` ```lemma subspace_substandard_cart: "subspace {x::real^_. (\i. P i \ x\$i = 0)}" ``` hoelzl@37489 ` 1470` ``` unfolding subspace_def by auto ``` hoelzl@37489 ` 1471` hoelzl@37489 ` 1472` ```lemma closed_substandard_cart: ``` huffman@44213 ` 1473` ``` "closed {x::'a::real_normed_vector ^ 'n. \i. P i \ x\$i = 0}" ``` wenzelm@49644 ` 1474` ```proof - ``` huffman@44213 ` 1475` ``` { fix i::'n ``` huffman@44213 ` 1476` ``` have "closed {x::'a ^ 'n. P i \ x\$i = 0}" ``` hoelzl@63332 ` 1477` ``` by (cases "P i") (simp_all add: closed_Collect_eq continuous_on_const continuous_on_id continuous_on_component) } ``` huffman@44213 ` 1478` ``` thus ?thesis ``` huffman@44213 ` 1479` ``` unfolding Collect_all_eq by (simp add: closed_INT) ``` hoelzl@37489 ` 1480` ```qed ``` hoelzl@37489 ` 1481` wenzelm@49644 ` 1482` ```lemma dim_substandard_cart: "dim {x::real^'n. \i. i \ d \ x\$i = 0} = card d" ``` wenzelm@49644 ` 1483` ``` (is "dim ?A = _") ``` wenzelm@49644 ` 1484` ```proof - ``` hoelzl@50526 ` 1485` ``` let ?a = "\x. axis x 1 :: real^'n" ``` hoelzl@50526 ` 1486` ``` have *: "{x. \i\Basis. i \ ?a ` d \ x \ i = 0} = ?A" ``` hoelzl@50526 ` 1487` ``` by (auto simp: image_iff Basis_vec_def axis_eq_axis inner_axis) ``` hoelzl@50526 ` 1488` ``` have "?a ` d \ Basis" ``` hoelzl@50526 ` 1489` ``` by (auto simp: Basis_vec_def) ``` wenzelm@49644 ` 1490` ``` thus ?thesis ``` hoelzl@50526 ` 1491` ``` using dim_substandard[of "?a ` d"] card_image[of ?a d] ``` hoelzl@50526 ` 1492` ``` by (auto simp: axis_eq_axis inj_on_def *) ``` hoelzl@37489 ` 1493` ```qed ``` hoelzl@37489 ` 1494` lp15@67719 ` 1495` ```lemma dim_subset_UNIV_cart: ``` lp15@67719 ` 1496` ``` fixes S :: "(real^'n) set" ``` lp15@67719 ` 1497` ``` shows "dim S \ CARD('n)" ``` lp15@67719 ` 1498` ``` by (metis dim_subset_UNIV DIM_cart DIM_real mult.right_neutral) ``` lp15@67719 ` 1499` hoelzl@37489 ` 1500` ```lemma affinity_inverses: ``` hoelzl@37489 ` 1501` ``` assumes m0: "m \ (0::'a::field)" ``` wenzelm@61736 ` 1502` ``` shows "(\x. m *s x + c) \ (\x. inverse(m) *s x + (-(inverse(m) *s c))) = id" ``` wenzelm@61736 ` 1503` ``` "(\x. inverse(m) *s x + (-(inverse(m) *s c))) \ (\x. m *s x + c) = id" ``` hoelzl@37489 ` 1504` ``` using m0 ``` haftmann@54230 ` 1505` ``` apply (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff) ``` haftmann@54230 ` 1506` ``` apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1 [symmetric]) ``` wenzelm@49644 ` 1507` ``` done ``` hoelzl@37489 ` 1508` hoelzl@37489 ` 1509` ```lemma vector_affinity_eq: ``` hoelzl@37489 ` 1510` ``` assumes m0: "(m::'a::field) \ 0" ``` hoelzl@37489 ` 1511` ``` shows "m *s x + c = y \ x = inverse m *s y + -(inverse m *s c)" ``` hoelzl@37489 ` 1512` ```proof ``` hoelzl@37489 ` 1513` ``` assume h: "m *s x + c = y" ``` hoelzl@37489 ` 1514` ``` hence "m *s x = y - c" by (simp add: field_simps) ``` hoelzl@37489 ` 1515` ``` hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp ``` hoelzl@37489 ` 1516` ``` then show "x = inverse m *s y + - (inverse m *s c)" ``` hoelzl@37489 ` 1517` ``` using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) ``` hoelzl@37489 ` 1518` ```next ``` hoelzl@37489 ` 1519` ``` assume h: "x = inverse m *s y + - (inverse m *s c)" ``` haftmann@54230 ` 1520` ``` show "m *s x + c = y" unfolding h ``` hoelzl@37489 ` 1521` ``` using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) ``` hoelzl@37489 ` 1522` ```qed ``` hoelzl@37489 ` 1523` hoelzl@37489 ` 1524` ```lemma vector_eq_affinity: ``` wenzelm@49644 ` 1525` ``` "(m::'a::field) \ 0 ==> (y = m *s x + c \ inverse(m) *s y + -(inverse(m) *s c) = x)" ``` hoelzl@37489 ` 1526` ``` using vector_affinity_eq[where m=m and x=x and y=y and c=c] ``` hoelzl@37489 ` 1527` ``` by metis ``` hoelzl@37489 ` 1528` hoelzl@50526 ` 1529` ```lemma vector_cart: ``` hoelzl@50526 ` 1530` ``` fixes f :: "real^'n \ real" ``` hoelzl@50526 ` 1531` ``` shows "(\ i. f (axis i 1)) = (\i\Basis. f i *\<^sub>R i)" ``` hoelzl@50526 ` 1532` ``` unfolding euclidean_eq_iff[where 'a="real^'n"] ``` hoelzl@50526 ` 1533` ``` by simp (simp add: Basis_vec_def inner_axis) ``` hoelzl@63332 ` 1534` hoelzl@50526 ` 1535` ```lemma const_vector_cart:"((\ i. d)::real^'n) = (\i\Basis. d *\<^sub>R i)" ``` hoelzl@50526 ` 1536` ``` by (rule vector_cart) ``` wenzelm@49644 ` 1537` huffman@44360 ` 1538` ```subsection "Convex Euclidean Space" ``` hoelzl@37489 ` 1539` hoelzl@50526 ` 1540` ```lemma Cart_1:"(1::real^'n) = \Basis" ``` hoelzl@50526 ` 1541` ``` using const_vector_cart[of 1] by (simp add: one_vec_def) ``` hoelzl@37489 ` 1542` hoelzl@37489 ` 1543` ```declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp] ``` hoelzl@37489 ` 1544` ```declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp] ``` hoelzl@37489 ` 1545` hoelzl@50526 ` 1546` ```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 ` 1547` hoelzl@37489 ` 1548` ```lemma convex_box_cart: ``` hoelzl@37489 ` 1549` ``` assumes "\i. convex {x. P i x}" ``` hoelzl@37489 ` 1550` ``` shows "convex {x. \i. P i (x\$i)}" ``` hoelzl@37489 ` 1551` ``` using assms unfolding convex_def by auto ``` hoelzl@37489 ` 1552` hoelzl@37489 ` 1553` ```lemma convex_positive_orthant_cart: "convex {x::real^'n. (\i. 0 \ x\$i)}" ``` hoelzl@63334 ` 1554` ``` by (rule convex_box_cart) (simp add: atLeast_def[symmetric]) ``` hoelzl@37489 ` 1555` hoelzl@37489 ` 1556` ```lemma unit_interval_convex_hull_cart: ``` immler@56188 ` 1557` ``` "cbox (0::real^'n) 1 = convex hull {x. \i. (x\$i = 0) \ (x\$i = 1)}" ``` immler@56188 ` 1558` ``` unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"] box_real[symmetric] ``` hoelzl@50526 ` 1559` ``` by (rule arg_cong[where f="\x. convex hull x"]) (simp add: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 1560` hoelzl@37489 ` 1561` ```lemma cube_convex_hull_cart: ``` wenzelm@49644 ` 1562` ``` assumes "0 < d" ``` wenzelm@49644 ` 1563` ``` obtains s::"(real^'n) set" ``` immler@56188 ` 1564` ``` where "finite s" "cbox (x - (\ i. d)) (x + (\ i. d)) = convex hull s" ``` wenzelm@49644 ` 1565` ```proof - ``` wenzelm@55522 ` 1566` ``` from assms obtain s where "finite s" ``` nipkow@67399 ` 1567` ``` and "cbox (x - sum (( *\<^sub>R) d) Basis) (x + sum (( *\<^sub>R) d) Basis) = convex hull s" ``` wenzelm@55522 ` 1568` ``` by (rule cube_convex_hull) ``` wenzelm@55522 ` 1569` ``` with that[of s] show thesis ``` wenzelm@55522 ` 1570` ``` by (simp add: const_vector_cart) ``` hoelzl@37489 ` 1571` ```qed ``` hoelzl@37489 ` 1572` hoelzl@37489 ` 1573` hoelzl@37489 ` 1574` ```subsection "Derivative" ``` hoelzl@37489 ` 1575` hoelzl@37489 ` 1576` ```definition "jacobian f net = matrix(frechet_derivative f net)" ``` hoelzl@37489 ` 1577` wenzelm@49644 ` 1578` ```lemma jacobian_works: ``` wenzelm@49644 ` 1579` ``` "(f::(real^'a) \ (real^'b)) differentiable net \ ``` lp15@67986 ` 1580` ``` (f has_derivative (\h. (jacobian f net) *v h)) net" (is "?lhs = ?rhs") ``` lp15@67986 ` 1581` ```proof ``` lp15@67986 ` 1582` ``` assume ?lhs then show ?rhs ``` lp15@67986 ` 1583` ``` by (simp add: frechet_derivative_works has_derivative_linear jacobian_def) ``` lp15@67986 ` 1584` ```next ``` lp15@67986 ` 1585` ``` assume ?rhs then show ?lhs ``` lp15@67986 ` 1586` ``` by (rule differentiableI) ``` lp15@67986 ` 1587` ```qed ``` hoelzl@37489 ` 1588` hoelzl@37489 ` 1589` wenzelm@60420 ` 1590` ```subsection \Component of the differential must be zero if it exists at a local ``` nipkow@67968 ` 1591` ``` maximum or minimum for that corresponding component\ ``` hoelzl@37489 ` 1592` hoelzl@50526 ` 1593` ```lemma differential_zero_maxmin_cart: ``` wenzelm@49644 ` 1594` ``` fixes f::"real^'a \ real^'b" ``` wenzelm@49644 ` 1595` ``` 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 ` 1596` ``` "f differentiable (at x)" ``` hoelzl@50526 ` 1597` ``` shows "jacobian f (at x) \$ k = 0" ``` hoelzl@50526 ` 1598` ``` using differential_zero_maxmin_component[of "axis k 1" e x f] assms ``` hoelzl@50526 ` 1599` ``` vector_cart[of "\j. frechet_derivative f (at x) j \$ k"] ``` hoelzl@50526 ` 1600` ``` by (simp add: Basis_vec_def axis_eq_axis inner_axis jacobian_def matrix_def) ``` wenzelm@49644 ` 1601` wenzelm@60420 ` 1602` ```subsection \Lemmas for working on @{typ "real^1"}\ ``` hoelzl@37489 ` 1603` hoelzl@37489 ` 1604` ```lemma forall_1[simp]: "(\i::1. P i) \ P 1" ``` wenzelm@49644 ` 1605` ``` by (metis (full_types) num1_eq_iff) ``` hoelzl@37489 ` 1606` hoelzl@37489 ` 1607` ```lemma ex_1[simp]: "(\x::1. P x) \ P 1" ``` wenzelm@49644 ` 1608` ``` by auto (metis (full_types) num1_eq_iff) ``` hoelzl@37489 ` 1609` hoelzl@37489 ` 1610` ```lemma exhaust_2: ``` wenzelm@49644 ` 1611` ``` fixes x :: 2 ``` wenzelm@49644 ` 1612` ``` shows "x = 1 \ x = 2" ``` hoelzl@37489 ` 1613` ```proof (induct x) ``` hoelzl@37489 ` 1614` ``` case (of_int z) ``` lp15@67979 ` 1615` ``` then have "0 \ z" and "z < 2" by simp_all ``` hoelzl@37489 ` 1616` ``` then have "z = 0 | z = 1" by arith ``` hoelzl@37489 ` 1617` ``` then show ?case by auto ``` hoelzl@37489 ` 1618` ```qed ``` hoelzl@37489 ` 1619` hoelzl@37489 ` 1620` ```lemma forall_2: "(\i::2. P i) \ P 1 \ P 2" ``` hoelzl@37489 ` 1621` ``` by (metis exhaust_2) ``` hoelzl@37489 ` 1622` hoelzl@37489 ` 1623` ```lemma exhaust_3: ``` wenzelm@49644 ` 1624` ``` fixes x :: 3 ``` wenzelm@49644 ` 1625` ``` shows "x = 1 \ x = 2 \ x = 3" ``` hoelzl@37489 ` 1626` ```proof (induct x) ``` hoelzl@37489 ` 1627` ``` case (of_int z) ``` lp15@67979 ` 1628` ``` then have "0 \ z" and "z < 3" by simp_all ``` hoelzl@37489 ` 1629` ``` then have "z = 0 \ z = 1 \ z = 2" by arith ``` hoelzl@37489 ` 1630` ``` then show ?case by auto ``` hoelzl@37489 ` 1631` ```qed ``` hoelzl@37489 ` 1632` hoelzl@37489 ` 1633` ```lemma forall_3: "(\i::3. P i) \ P 1 \ P 2 \ P 3" ``` hoelzl@37489 ` 1634` ``` by (metis exhaust_3) ``` hoelzl@37489 ` 1635` hoelzl@37489 ` 1636` ```lemma UNIV_1 [simp]: "UNIV = {1::1}" ``` hoelzl@37489 ` 1637` ``` by (auto simp add: num1_eq_iff) ``` hoelzl@37489 ` 1638` hoelzl@37489 ` 1639` ```lemma UNIV_2: "UNIV = {1::2, 2::2}" ``` hoelzl@37489 ` 1640` ``` using exhaust_2 by auto ``` hoelzl@37489 ` 1641` hoelzl@37489 ` 1642` ```lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" ``` hoelzl@37489 ` 1643` ``` using exhaust_3 by auto ``` hoelzl@37489 ` 1644` nipkow@64267 ` 1645` ```lemma sum_1: "sum f (UNIV::1 set) = f 1" ``` hoelzl@37489 ` 1646` ``` unfolding UNIV_1 by simp ``` hoelzl@37489 ` 1647` nipkow@64267 ` 1648` ```lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2" ``` hoelzl@37489 ` 1649` ``` unfolding UNIV_2 by simp ``` hoelzl@37489 ` 1650` nipkow@64267 ` 1651` ```lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3" ``` haftmann@57514 ` 1652` ``` unfolding UNIV_3 by (simp add: ac_simps) ``` hoelzl@37489 ` 1653` lp15@67979 ` 1654` ```lemma num1_eqI: ``` lp15@67979 ` 1655` ``` fixes a::num1 shows "a = b" ``` lp15@67979 ` 1656` ``` by (metis (full_types) UNIV_1 UNIV_I empty_iff insert_iff) ``` lp15@67979 ` 1657` lp15@67979 ` 1658` ```lemma num1_eq1 [simp]: ``` lp15@67979 ` 1659` ``` fixes a::num1 shows "a = 1" ``` lp15@67979 ` 1660` ``` by (rule num1_eqI) ``` lp15@67979 ` 1661` wenzelm@49644 ` 1662` ```instantiation num1 :: cart_one ``` wenzelm@49644 ` 1663` ```begin ``` wenzelm@49644 ` 1664` wenzelm@49644 ` 1665` ```instance ``` wenzelm@49644 ` 1666` ```proof ``` hoelzl@37489 ` 1667` ``` show "CARD(1) = Suc 0" by auto ``` wenzelm@49644 ` 1668` ```qed ``` wenzelm@49644 ` 1669` wenzelm@49644 ` 1670` ```end ``` hoelzl@37489 ` 1671` lp15@67979 ` 1672` ```instantiation num1 :: linorder begin ``` lp15@67979 ` 1673` ```definition "a < b \ Rep_num1 a < Rep_num1 b" ``` lp15@67979 ` 1674` ```definition "a \ b \ Rep_num1 a \ Rep_num1 b" ``` lp15@67979 ` 1675` ```instance ``` lp15@67979 ` 1676` ``` by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI) ``` lp15@67979 ` 1677` ```end ``` lp15@67979 ` 1678` lp15@67979 ` 1679` ```instance num1 :: wellorder ``` lp15@67979 ` 1680` ``` by intro_classes (auto simp: less_eq_num1_def less_num1_def) ``` lp15@67979 ` 1681` nipkow@67968 ` 1682` ```subsection\The collapse of the general concepts to dimension one\ ``` hoelzl@37489 ` 1683` hoelzl@37489 ` 1684` ```lemma vector_one: "(x::'a ^1) = (\ i. (x\$1))" ``` huffman@44136 ` 1685` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 1686` hoelzl@37489 ` 1687` ```lemma forall_one: "(\(x::'a ^1). P x) \ (\x. P(\ i. x))" ``` hoelzl@37489 ` 1688` ``` apply auto ``` hoelzl@37489 ` 1689` ``` apply (erule_tac x= "x\$1" in allE) ``` hoelzl@37489 ` 1690` ``` apply (simp only: vector_one[symmetric]) ``` hoelzl@37489 ` 1691` ``` done ``` hoelzl@37489 ` 1692` hoelzl@37489 ` 1693` ```lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)" ``` huffman@44136 ` 1694` ``` by (simp add: norm_vec_def) ``` hoelzl@37489 ` 1695` lp15@67979 ` 1696` ```lemma dist_vector_1: ``` lp15@67979 ` 1697` ``` fixes x :: "'a::real_normed_vector^1" ``` lp15@67979 ` 1698` ``` shows "dist x y = dist (x\$1) (y\$1)" ``` lp15@67979 ` 1699` ``` by (simp add: dist_norm norm_vector_1) ``` lp15@67979 ` 1700` wenzelm@61945 ` 1701` ```lemma norm_real: "norm(x::real ^ 1) = \x\$1\" ``` hoelzl@37489 ` 1702` ``` by (simp add: norm_vector_1) ``` hoelzl@37489 ` 1703` wenzelm@61945 ` 1704` ```lemma dist_real: "dist(x::real ^ 1) y = \(x\$1) - (y\$1)\" ``` hoelzl@37489 ` 1705` ``` by (auto simp add: norm_real dist_norm) ``` hoelzl@37489 ` 1706` lp15@67986 ` 1707` ```subsection\ Rank of a matrix\ ``` lp15@67986 ` 1708` lp15@67986 ` 1709` ```text\Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\ ``` lp15@67986 ` 1710` lp15@67986 ` 1711` ```lemma matrix_vector_mult_in_columnspace: ``` lp15@67986 ` 1712` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1713` ``` shows "(A *v x) \ span(columns A)" ``` lp15@67986 ` 1714` ``` apply (simp add: matrix_vector_column columns_def transpose_def column_def) ``` lp15@67986 ` 1715` ``` apply (intro span_sum span_mul) ``` lp15@67986 ` 1716` ``` apply (force intro: span_superset) ``` lp15@67986 ` 1717` ``` done ``` lp15@67986 ` 1718` lp15@67986 ` 1719` ```lemma orthogonal_nullspace_rowspace: ``` lp15@67986 ` 1720` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1721` ``` assumes 0: "A *v x = 0" and y: "y \ span(rows A)" ``` lp15@67986 ` 1722` ``` shows "orthogonal x y" ``` lp15@67986 ` 1723` ```proof (rule span_induct [OF y]) ``` lp15@67986 ` 1724` ``` show "subspace {a. orthogonal x a}" ``` lp15@67986 ` 1725` ``` by (simp add: subspace_orthogonal_to_vector) ``` lp15@67986 ` 1726` ```next ``` lp15@67986 ` 1727` ``` fix v ``` lp15@67986 ` 1728` ``` assume "v \ rows A" ``` lp15@67986 ` 1729` ``` then obtain i where "v = row i A" ``` lp15@67986 ` 1730` ``` by (auto simp: rows_def) ``` lp15@67986 ` 1731` ``` with 0 show "orthogonal x v" ``` lp15@67986 ` 1732` ``` unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def ``` lp15@67986 ` 1733` ``` by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index) ``` lp15@67986 ` 1734` ```qed ``` lp15@67986 ` 1735` lp15@67986 ` 1736` ```lemma nullspace_inter_rowspace: ``` lp15@67986 ` 1737` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1738` ``` shows "A *v x = 0 \ x \ span(rows A) \ x = 0" ``` lp15@67986 ` 1739` ``` using orthogonal_nullspace_rowspace orthogonal_self by auto ``` lp15@67986 ` 1740` lp15@67986 ` 1741` ```lemma matrix_vector_mul_injective_on_rowspace: ``` lp15@67986 ` 1742` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1743` ``` shows "\A *v x = A *v y; x \ span(rows A); y \ span(rows A)\ \ x = y" ``` lp15@67986 ` 1744` ``` using nullspace_inter_rowspace [of A "x-y"] ``` lp15@67986 ` 1745` ``` by (metis eq_iff_diff_eq_0 matrix_vector_mult_diff_distrib span_diff) ``` lp15@67986 ` 1746` lp15@67986 ` 1747` ```definition rank :: "real^'n^'m=>nat" ``` lp15@67986 ` 1748` ``` where "rank A \ dim(columns A)" ``` lp15@67986 ` 1749` lp15@67986 ` 1750` ```lemma dim_rows_le_dim_columns: ``` lp15@67986 ` 1751` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1752` ``` shows "dim(rows A) \ dim(columns A)" ``` lp15@67986 ` 1753` ```proof - ``` lp15@67986 ` 1754` ``` have "dim (span (rows A)) \ dim (span (columns A))" ``` lp15@67986 ` 1755` ``` proof - ``` lp15@67986 ` 1756` ``` obtain B where "independent B" "span(rows A) \ span B" ``` lp15@67986 ` 1757` ``` and B: "B \ span(rows A)""card B = dim (span(rows A))" ``` lp15@68069 ` 1758` ``` using basis_exists [of "span(rows A)"] by metis ``` lp15@67986 ` 1759` ``` with span_subspace have eq: "span B = span(rows A)" ``` lp15@67986 ` 1760` ``` by auto ``` lp15@67986 ` 1761` ``` then have inj: "inj_on (( *v) A) (span B)" ``` lp15@67986 ` 1762` ``` using inj_on_def matrix_vector_mul_injective_on_rowspace by blast ``` lp15@67986 ` 1763` ``` then have ind: "independent (( *v) A ` B)" ``` lp15@67986 ` 1764` ``` by (rule independent_inj_on_image [OF \independent B\ matrix_vector_mul_linear]) ``` lp15@67986 ` 1765` ``` then have "finite (( *v) A ` B) \ card (( *v) A ` B) \ dim (( *v) A ` B)" ``` lp15@67986 ` 1766` ``` by (rule independent_bound_general) ``` lp15@67986 ` 1767` ``` then show ?thesis ``` lp15@67986 ` 1768` ``` by (metis (no_types, lifting) B ind inj eq card_image image_subset_iff independent_card_le_dim inj_on_subset matrix_vector_mult_in_columnspace) ``` lp15@67986 ` 1769` ``` qed ``` lp15@67986 ` 1770` ``` then show ?thesis ``` lp15@67986 ` 1771` ``` by simp ``` lp15@67986 ` 1772` ```qed ``` lp15@67986 ` 1773` lp15@67986 ` 1774` ```lemma rank_row: ``` lp15@67986 ` 1775` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1776` ``` shows "rank A = dim(rows A)" ``` lp15@67986 ` 1777` ``` unfolding rank_def ``` lp15@67986 ` 1778` ``` by (metis dim_rows_le_dim_columns columns_transpose dual_order.antisym rows_transpose) ``` lp15@67986 ` 1779` lp15@67986 ` 1780` ```lemma rank_transpose: ``` lp15@67986 ` 1781` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1782` ``` shows "rank(transpose A) = rank A" ``` lp15@67986 ` 1783` ``` by (metis rank_def rank_row rows_transpose) ``` lp15@67986 ` 1784` lp15@67986 ` 1785` ```lemma matrix_vector_mult_basis: ``` lp15@67986 ` 1786` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1787` ``` shows "A *v (axis k 1) = column k A" ``` lp15@67986 ` 1788` ``` by (simp add: cart_eq_inner_axis column_def matrix_mult_dot) ``` lp15@67986 ` 1789` lp15@67986 ` 1790` ```lemma columns_image_basis: ``` lp15@67986 ` 1791` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1792` ``` shows "columns A = ( *v) A ` (range (\i. axis i 1))" ``` lp15@67986 ` 1793` ``` by (force simp: columns_def matrix_vector_mult_basis [symmetric]) ``` lp15@67986 ` 1794` lp15@67986 ` 1795` ```lemma rank_dim_range: ``` lp15@67986 ` 1796` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1797` ``` shows "rank A = dim(range (\x. A *v x))" ``` lp15@67986 ` 1798` ``` unfolding rank_def ``` lp15@67986 ` 1799` ```proof (rule span_eq_dim) ``` lp15@67986 ` 1800` ``` show "span (columns A) = span (range (( *v) A))" ``` lp15@67986 ` 1801` ``` apply (auto simp: columns_image_basis span_linear_image matrix_vector_mul_linear) ``` lp15@67986 ` 1802` ``` by (metis columns_image_basis matrix_vector_mul_linear matrix_vector_mult_in_columnspace span_linear_image) ``` lp15@67986 ` 1803` ```qed ``` lp15@67986 ` 1804` lp15@67986 ` 1805` ```lemma rank_bound: ``` lp15@67986 ` 1806` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1807` ``` shows "rank A \ min CARD('m) (CARD('n))" ``` lp15@67986 ` 1808` ``` by (metis (mono_tags, hide_lams) min.bounded_iff DIM_cart DIM_real dim_subset_UNIV mult.right_neutral rank_def rank_transpose) ``` lp15@67986 ` 1809` lp15@67986 ` 1810` ```lemma full_rank_injective: ``` lp15@67986 ` 1811` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1812` ``` shows "rank A = CARD('n) \ inj (( *v) A)" ``` lp15@67986 ` 1813` ``` by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows rank_row dim_eq_full [symmetric]) ``` lp15@67986 ` 1814` lp15@67986 ` 1815` ```lemma full_rank_surjective: ``` lp15@67986 ` 1816` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1817` ``` shows "rank A = CARD('m) \ surj (( *v) A)" ``` lp15@67986 ` 1818` ``` by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric] ``` lp15@67986 ` 1819` ``` matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose) ``` lp15@67986 ` 1820` lp15@67986 ` 1821` ```lemma rank_I: "rank(mat 1::real^'n^'n) = CARD('n)" ``` lp15@67986 ` 1822` ``` by (simp add: full_rank_injective inj_on_def) ``` lp15@67986 ` 1823` lp15@67986 ` 1824` ```lemma less_rank_noninjective: ``` lp15@67986 ` 1825` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1826` ``` shows "rank A < CARD('n) \ \ inj (( *v) A)" ``` lp15@67986 ` 1827` ```using less_le rank_bound by (auto simp: full_rank_injective [symmetric]) ``` lp15@67986 ` 1828` lp15@67986 ` 1829` ```lemma matrix_nonfull_linear_equations_eq: ``` lp15@67986 ` 1830` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1831` ``` shows "(\x. (x \ 0) \ A *v x = 0) \ ~(rank A = CARD('n))" ``` lp15@67986 ` 1832` ``` by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker) ``` lp15@67986 ` 1833` lp15@67986 ` 1834` ```lemma rank_eq_0: "rank A = 0 \ A = 0" and rank_0 [simp]: "rank 0 = 0" ``` lp15@67986 ` 1835` ``` by (auto simp: rank_dim_range matrix_eq) ``` lp15@67986 ` 1836` lp15@67986 ` 1837` lp15@67986 ` 1838` ```lemma rank_mul_le_right: ``` lp15@67986 ` 1839` ``` fixes A :: "real^'n^'m" and B :: "real^'p^'n" ``` lp15@67986 ` 1840` ``` shows "rank(A ** B) \ rank B" ``` lp15@67986 ` 1841` ```proof - ``` lp15@67986 ` 1842` ``` have "rank(A ** B) \ dim (( *v) A ` range (( *v) B))" ``` lp15@67986 ` 1843` ``` by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc) ``` lp15@67986 ` 1844` ``` also have "\ \ rank B" ``` lp15@67986 ` 1845` ``` by (simp add: rank_dim_range matrix_vector_mul_linear dim_image_le) ``` lp15@67986 ` 1846` ``` finally show ?thesis . ``` lp15@67986 ` 1847` ```qed ``` lp15@67986 ` 1848` lp15@67986 ` 1849` ```lemma rank_mul_le_left: ``` lp15@67986 ` 1850` ``` fixes A :: "real^'n^'m" and B :: "real^'p^'n" ``` lp15@67986 ` 1851` ``` shows "rank(A ** B) \ rank A" ``` lp15@67986 ` 1852` ``` by (metis matrix_transpose_mul rank_mul_le_right rank_transpose) ``` lp15@67986 ` 1853` lp15@67981 ` 1854` ```subsection\Routine results connecting the types @{typ "real^1"} and @{typ real}\ ``` lp15@67981 ` 1855` lp15@67981 ` 1856` ```lemma vector_one_nth [simp]: ``` lp15@67981 ` 1857` ``` fixes x :: "'a^1" shows "vec (x \$ 1) = x" ``` lp15@67981 ` 1858` ``` by (metis vec_def vector_one) ``` lp15@67981 ` 1859` lp15@67981 ` 1860` ```lemma vec_cbox_1_eq [simp]: ``` lp15@67981 ` 1861` ``` shows "vec ` cbox u v = cbox (vec u) (vec v ::real^1)" ``` lp15@67981 ` 1862` ``` by (force simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box) ``` lp15@67981 ` 1863` lp15@67981 ` 1864` ```lemma vec_nth_cbox_1_eq [simp]: ``` lp15@67981 ` 1865` ``` fixes u v :: "'a::euclidean_space^1" ``` lp15@67981 ` 1866` ``` shows "(\x. x \$ 1) ` cbox u v = cbox (u\$1) (v\$1)" ``` lp15@67981 ` 1867` ``` by (auto simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box image_iff Bex_def inner_axis) (metis vec_component) ``` lp15@67981 ` 1868` lp15@67981 ` 1869` ```lemma vec_nth_1_iff_cbox [simp]: ``` lp15@67981 ` 1870` ``` fixes a b :: "'a::euclidean_space" ``` lp15@67981 ` 1871` ``` shows "(\x::'a^1. x \$ 1) ` S = cbox a b \ S = cbox (vec a) (vec b)" ``` lp15@67981 ` 1872` ``` (is "?lhs = ?rhs") ``` lp15@67981 ` 1873` ```proof ``` lp15@67981 ` 1874` ``` assume L: ?lhs show ?rhs ``` lp15@67981 ` 1875` ``` proof (intro equalityI subsetI) ``` lp15@67981 ` 1876` ``` fix x ``` lp15@67981 ` 1877` ``` assume "x \ S" ``` lp15@67981 ` 1878` ``` then have "x \$ 1 \ (\v. v \$ (1::1)) ` cbox (vec a) (vec b)" ``` lp15@67981 ` 1879` ``` using L by auto ``` lp15@67981 ` 1880` ``` then show "x \ cbox (vec a) (vec b)" ``` lp15@67981 ` 1881` ``` by (metis (no_types, lifting) imageE vector_one_nth) ``` lp15@67981 ` 1882` ``` next ``` lp15@67981 ` 1883` ``` fix x :: "'a^1" ``` lp15@67981 ` 1884` ``` assume "x \ cbox (vec a) (vec b)" ``` lp15@67981 ` 1885` ``` then show "x \ S" ``` lp15@67981 ` 1886` ``` by (metis (no_types, lifting) L imageE imageI vec_component vec_nth_cbox_1_eq vector_one_nth) ``` lp15@67981 ` 1887` ``` qed ``` lp15@67981 ` 1888` ```qed simp ``` wenzelm@49644 ` 1889` lp15@67979 ` 1890` ```lemma tendsto_at_within_vector_1: ``` lp15@67979 ` 1891` ``` fixes S :: "'a :: metric_space set" ``` lp15@67979 ` 1892` ``` assumes "(f \ fx) (at x within S)" ``` lp15@67979 ` 1893` ``` shows "((\y::'a^1. \ i. f (y \$ 1)) \ (vec fx::'a^1)) (at (vec x) within vec ` S)" ``` lp15@67979 ` 1894` ```proof (rule topological_tendstoI) ``` lp15@67979 ` 1895` ``` fix T :: "('a^1) set" ``` lp15@67979 ` 1896` ``` assume "open T" "vec fx \ T" ``` lp15@67979 ` 1897` ``` have "\\<^sub>F x in at x within S. f x \ (\x. x \$ 1) ` T" ``` lp15@67979 ` 1898` ``` using \open T\ \vec fx \ T\ assms open_image_vec_nth tendsto_def by fastforce ``` lp15@67979 ` 1899` ``` then show "\\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\ i. f (x \$ 1)) \ T" ``` lp15@67979 ` 1900` ``` unfolding eventually_at dist_norm [symmetric] ``` lp15@67979 ` 1901` ``` by (rule ex_forward) ``` lp15@67979 ` 1902` ``` (use \open T\ in ``` lp15@67979 ` 1903` ``` \fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\) ``` lp15@67979 ` 1904` ```qed ``` lp15@67979 ` 1905` lp15@67979 ` 1906` ```lemma has_derivative_vector_1: ``` lp15@67979 ` 1907` ``` assumes der_g: "(g has_derivative (\x. x * g' a)) (at a within S)" ``` lp15@67979 ` 1908` ``` shows "((\x. vec (g (x \$ 1))) has_derivative ( *\<^sub>R) (g' a)) ``` lp15@67979 ` 1909` ``` (at ((vec a)::real^1) within vec ` S)" ``` lp15@67979 ` 1910` ``` using der_g ``` lp15@67979 ` 1911` ``` apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1) ``` lp15@67979 ` 1912` ``` apply (drule tendsto_at_within_vector_1, vector) ``` lp15@67979 ` 1913` ``` apply (auto simp: algebra_simps eventually_at tendsto_def) ``` lp15@67979 ` 1914` ``` done ``` lp15@67979 ` 1915` lp15@67979 ` 1916` nipkow@67968 ` 1917` ```subsection\Explicit vector construction from lists\ ``` hoelzl@37489 ` 1918` hoelzl@43995 ` 1919` ```definition "vector l = (\ i. foldr (\x f n. fun_upd (f (n+1)) n x) l (\n x. 0) 1 i)" ``` hoelzl@37489 ` 1920` lp15@68054 ` 1921` ```lemma vector_1 [simp]: "(vector[x]) \$1 = x" ``` hoelzl@37489 ` 1922` ``` unfolding vector_def by simp ``` hoelzl@37489 ` 1923` lp15@68054 ` 1924` ```lemma vector_2 [simp]: "(vector[x,y]) \$1 = x" "(vector[x,y] :: 'a^2)\$2 = (y::'a::zero)" ``` hoelzl@37489 ` 1925` ``` unfolding vector_def by simp_all ``` hoelzl@37489 ` 1926` lp15@68054 ` 1927` ```lemma vector_3 [simp]: ``` hoelzl@37489 ` 1928` ``` "(vector [x,y,z] ::('a::zero)^3)\$1 = x" ``` hoelzl@37489 ` 1929` ``` "(vector [x,y,z] ::('a::zero)^3)\$2 = y" ``` hoelzl@37489 ` 1930` ``` "(vector [x,y,z] ::('a::zero)^3)\$3 = z" ``` hoelzl@37489 ` 1931` ``` unfolding vector_def by simp_all ``` hoelzl@37489 ` 1932` hoelzl@37489 ` 1933` ```lemma forall_vector_1: "(\v::'a::zero^1. P v) \ (\x. P(vector[x]))" ``` lp15@67719 ` 1934` ``` by (metis vector_1 vector_one) ``` hoelzl@37489 ` 1935` hoelzl@37489 ` 1936` ```lemma forall_vector_2: "(\v::'a::zero^2. P v) \ (\x y. P(vector[x, y]))" ``` hoelzl@37489 ` 1937` ``` apply auto ``` hoelzl@37489 ` 1938` ``` apply (erule_tac x="v\$1" in allE) ``` hoelzl@37489 ` 1939` ``` apply (erule_tac x="v\$2" in allE) ``` hoelzl@37489 ` 1940` ``` apply (subgoal_tac "vector [v\$1, v\$2] = v") ``` hoelzl@37489 ` 1941` ``` apply simp ``` hoelzl@37489 ` 1942` ``` apply (vector vector_def) ``` hoelzl@37489 ` 1943` ``` apply (simp add: forall_2) ``` hoelzl@37489 ` 1944` ``` done ``` hoelzl@37489 ` 1945` hoelzl@37489 ` 1946` ```lemma forall_vector_3: "(\v::'a::zero^3. P v) \ (\x y z. P(vector[x, y, z]))" ``` hoelzl@37489 ` 1947` ``` apply auto ``` hoelzl@37489 ` 1948` ``` apply (erule_tac x="v\$1" in allE) ``` hoelzl@37489 ` 1949` ``` apply (erule_tac x="v\$2" in allE) ``` hoelzl@37489 ` 1950` ``` apply (erule_tac x="v\$3" in allE) ``` hoelzl@37489 ` 1951` ``` apply (subgoal_tac "vector [v\$1, v\$2, v\$3] = v") ``` hoelzl@37489 ` 1952` ``` apply simp ``` hoelzl@37489 ` 1953` ``` apply (vector vector_def) ``` hoelzl@37489 ` 1954` ``` apply (simp add: forall_3) ``` hoelzl@37489 ` 1955` ``` done ``` hoelzl@37489 ` 1956` hoelzl@37489 ` 1957` ```lemma bounded_linear_component_cart[intro]: "bounded_linear (\x::real^'n. x \$ k)" ``` lp15@68062 ` 1958` ``` apply (rule bounded_linear_intro[where K=1]) ``` hoelzl@37489 ` 1959` ``` using component_le_norm_cart[of _ k] unfolding real_norm_def by auto ``` hoelzl@37489 ` 1960` hoelzl@37489 ` 1961` ```lemma interval_split_cart: ``` hoelzl@37489 ` 1962` ``` "{a..b::real^'n} \ {x. x\$k \ c} = {a .. (\ i. if i = k then min (b\$k) c else b\$i)}" ``` immler@56188 ` 1963` ``` "cbox a b \ {x. x\$k \ c} = {(\ i. if i = k then max (a\$k) c else a\$i) .. b}" ``` wenzelm@49644 ` 1964` ``` apply (rule_tac[!] set_eqI) ``` lp15@67673 ` 1965` ``` unfolding Int_iff mem_box_cart mem_Collect_eq interval_cbox_cart ``` wenzelm@49644 ` 1966` ``` unfolding vec_lambda_beta ``` wenzelm@49644 ` 1967` ``` by auto ``` hoelzl@37489 ` 1968` immler@67685 ` 1969` ```lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] = ``` immler@67685 ` 1970` ``` bounded_linear.uniform_limit[OF blinfun.bounded_linear_right] ``` immler@67685 ` 1971` ``` bounded_linear.uniform_limit[OF bounded_linear_vec_nth] ``` immler@67685 ` 1972` ``` bounded_linear.uniform_limit[OF bounded_linear_component_cart] ``` immler@67685 ` 1973` hoelzl@37489 ` 1974` ```end ```