src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
 author huffman Sun Aug 21 09:46:20 2011 -0700 (2011-08-21) changeset 44360 ea609ebdeebf parent 44282 f0de18b62d63 child 44452 4d910cc3f5f0 permissions -rw-r--r--
section -> subsection
 hoelzl@37489 ` 1` hoelzl@37489 ` 2` ```header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*} ``` hoelzl@37489 ` 3` hoelzl@37489 ` 4` ```theory Cartesian_Euclidean_Space ``` hoelzl@37489 ` 5` ```imports Finite_Cartesian_Product Integration ``` hoelzl@37489 ` 6` ```begin ``` hoelzl@37489 ` 7` hoelzl@37489 ` 8` ```lemma delta_mult_idempotent: ``` hoelzl@37489 ` 9` ``` "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto) ``` hoelzl@37489 ` 10` hoelzl@37489 ` 11` ```lemma setsum_Plus: ``` hoelzl@37489 ` 12` ``` "\finite A; finite B\ \ ``` hoelzl@37489 ` 13` ``` (\x\A <+> B. g x) = (\x\A. g (Inl x)) + (\x\B. g (Inr x))" ``` hoelzl@37489 ` 14` ``` unfolding Plus_def ``` hoelzl@37489 ` 15` ``` by (subst setsum_Un_disjoint, auto simp add: setsum_reindex) ``` hoelzl@37489 ` 16` hoelzl@37489 ` 17` ```lemma setsum_UNIV_sum: ``` hoelzl@37489 ` 18` ``` fixes g :: "'a::finite + 'b::finite \ _" ``` hoelzl@37489 ` 19` ``` shows "(\x\UNIV. g x) = (\x\UNIV. g (Inl x)) + (\x\UNIV. g (Inr x))" ``` hoelzl@37489 ` 20` ``` apply (subst UNIV_Plus_UNIV [symmetric]) ``` hoelzl@37489 ` 21` ``` apply (rule setsum_Plus [OF finite finite]) ``` hoelzl@37489 ` 22` ``` done ``` hoelzl@37489 ` 23` hoelzl@37489 ` 24` ```lemma setsum_mult_product: ``` hoelzl@37489 ` 25` ``` "setsum h {..i\{..j\{..j. j + i * B) {..j. j + i * B) ` {.. {i * B.. (\j. j + i * B) ` {.. (\ x y. (\ i. (x\$i) * (y\$i)))" ``` hoelzl@37489 ` 42` ``` instance .. ``` hoelzl@37489 ` 43` ```end ``` hoelzl@37489 ` 44` huffman@44136 ` 45` ```instantiation vec :: (one, finite) one ``` hoelzl@37489 ` 46` ```begin ``` huffman@44136 ` 47` ``` definition "1 \ (\ i. 1)" ``` hoelzl@37489 ` 48` ``` instance .. ``` hoelzl@37489 ` 49` ```end ``` hoelzl@37489 ` 50` huffman@44136 ` 51` ```instantiation vec :: (ord, finite) ord ``` hoelzl@37489 ` 52` ```begin ``` huffman@44136 ` 53` ``` definition "x \ y \ (\i. x\$i \ y\$i)" ``` huffman@44136 ` 54` ``` definition "x < y \ (\i. x\$i < y\$i)" ``` huffman@44136 ` 55` ``` instance .. ``` hoelzl@37489 ` 56` ```end ``` hoelzl@37489 ` 57` hoelzl@37489 ` 58` ```text{* The ordering on one-dimensional vectors is linear. *} ``` hoelzl@37489 ` 59` hoelzl@37489 ` 60` ```class cart_one = assumes UNIV_one: "card (UNIV \ 'a set) = Suc 0" ``` hoelzl@37489 ` 61` ```begin ``` hoelzl@37489 ` 62` ``` subclass finite ``` hoelzl@37489 ` 63` ``` proof from UNIV_one show "finite (UNIV :: 'a set)" ``` hoelzl@37489 ` 64` ``` by (auto intro!: card_ge_0_finite) qed ``` hoelzl@37489 ` 65` ```end ``` hoelzl@37489 ` 66` huffman@44136 ` 67` ```instantiation vec :: (linorder,cart_one) linorder begin ``` hoelzl@37489 ` 68` ```instance proof ``` hoelzl@37489 ` 69` ``` guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+ ``` hoelzl@37489 ` 70` ``` hence *:"UNIV = {a}" by auto ``` hoelzl@37489 ` 71` ``` have "\P. (\i\UNIV. P i) \ P a" unfolding * by auto hence all:"\P. (\i. P i) \ P a" by auto ``` huffman@44136 ` 72` ``` fix x y z::"'a^'b::cart_one" note * = less_eq_vec_def less_vec_def all vec_eq_iff ``` hoelzl@37489 ` 73` ``` show "x\x" "(x < y) = (x \ y \ \ y \ x)" "x\y \ y\x" unfolding * by(auto simp only:field_simps) ``` hoelzl@37489 ` 74` ``` { assume "x\y" "y\z" thus "x\z" unfolding * by(auto simp only:field_simps) } ``` hoelzl@37489 ` 75` ``` { assume "x\y" "y\x" thus "x=y" unfolding * by(auto simp only:field_simps) } ``` hoelzl@37489 ` 76` ```qed end ``` hoelzl@37489 ` 77` hoelzl@37489 ` 78` ```text{* Constant Vectors *} ``` hoelzl@37489 ` 79` hoelzl@37489 ` 80` ```definition "vec x = (\ i. x)" ``` hoelzl@37489 ` 81` hoelzl@37489 ` 82` ```text{* Also the scalar-vector multiplication. *} ``` hoelzl@37489 ` 83` hoelzl@37489 ` 84` ```definition vector_scalar_mult:: "'a::times \ 'a ^ 'n \ 'a ^ 'n" (infixl "*s" 70) ``` hoelzl@37489 ` 85` ``` where "c *s x = (\ i. c * (x\$i))" ``` hoelzl@37489 ` 86` hoelzl@37489 ` 87` ```subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} ``` hoelzl@37489 ` 88` hoelzl@37489 ` 89` ```method_setup vector = {* ``` hoelzl@37489 ` 90` ```let ``` hoelzl@37489 ` 91` ``` val ss1 = HOL_basic_ss addsimps [@{thm setsum_addf} RS sym, ``` hoelzl@37489 ` 92` ``` @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, ``` hoelzl@37489 ` 93` ``` @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym] ``` hoelzl@37489 ` 94` ``` val ss2 = @{simpset} addsimps ``` huffman@44136 ` 95` ``` [@{thm plus_vec_def}, @{thm times_vec_def}, ``` huffman@44136 ` 96` ``` @{thm minus_vec_def}, @{thm uminus_vec_def}, ``` huffman@44136 ` 97` ``` @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def}, ``` huffman@44136 ` 98` ``` @{thm scaleR_vec_def}, ``` huffman@44136 ` 99` ``` @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}] ``` hoelzl@37489 ` 100` ``` fun vector_arith_tac ths = ``` hoelzl@37489 ` 101` ``` simp_tac ss1 ``` hoelzl@37489 ` 102` ``` THEN' (fn i => rtac @{thm setsum_cong2} i ``` hoelzl@37489 ` 103` ``` ORELSE rtac @{thm setsum_0'} i ``` huffman@44136 ` 104` ``` ORELSE simp_tac (HOL_basic_ss addsimps [@{thm vec_eq_iff}]) i) ``` hoelzl@37489 ` 105` ``` (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) ``` hoelzl@37489 ` 106` ``` THEN' asm_full_simp_tac (ss2 addsimps ths) ``` hoelzl@37489 ` 107` ``` in ``` hoelzl@37489 ` 108` ``` Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths))) ``` hoelzl@37489 ` 109` ``` end ``` wenzelm@42814 ` 110` ```*} "lift trivial vector statements to real arith statements" ``` hoelzl@37489 ` 111` huffman@44136 ` 112` ```lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def) ``` huffman@44136 ` 113` ```lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def) ``` hoelzl@37489 ` 114` hoelzl@37489 ` 115` ```lemma vec_inj[simp]: "vec x = vec y \ x = y" by vector ``` hoelzl@37489 ` 116` hoelzl@37489 ` 117` ```lemma vec_in_image_vec: "vec x \ (vec ` S) \ x \ S" by auto ``` hoelzl@37489 ` 118` hoelzl@37489 ` 119` ```lemma vec_add: "vec(x + y) = vec x + vec y" by (vector vec_def) ``` hoelzl@37489 ` 120` ```lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def) ``` hoelzl@37489 ` 121` ```lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def) ``` hoelzl@37489 ` 122` ```lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def) ``` hoelzl@37489 ` 123` hoelzl@37489 ` 124` ```lemma vec_setsum: assumes fS: "finite S" ``` hoelzl@37489 ` 125` ``` shows "vec(setsum f S) = setsum (vec o f) S" ``` hoelzl@37489 ` 126` ``` apply (induct rule: finite_induct[OF fS]) ``` hoelzl@37489 ` 127` ``` apply (simp) ``` hoelzl@37489 ` 128` ``` apply (auto simp add: vec_add) ``` hoelzl@37489 ` 129` ``` done ``` hoelzl@37489 ` 130` hoelzl@37489 ` 131` ```text{* Obvious "component-pushing". *} ``` hoelzl@37489 ` 132` hoelzl@37489 ` 133` ```lemma vec_component [simp]: "vec x \$ i = x" ``` hoelzl@37489 ` 134` ``` by (vector vec_def) ``` hoelzl@37489 ` 135` hoelzl@37489 ` 136` ```lemma vector_mult_component [simp]: "(x * y)\$i = x\$i * y\$i" ``` hoelzl@37489 ` 137` ``` by vector ``` hoelzl@37489 ` 138` hoelzl@37489 ` 139` ```lemma vector_smult_component [simp]: "(c *s y)\$i = c * (y\$i)" ``` hoelzl@37489 ` 140` ``` by vector ``` hoelzl@37489 ` 141` hoelzl@37489 ` 142` ```lemma cond_component: "(if b then x else y)\$i = (if b then x\$i else y\$i)" by vector ``` hoelzl@37489 ` 143` hoelzl@37489 ` 144` ```lemmas vector_component = ``` hoelzl@37489 ` 145` ``` vec_component vector_add_component vector_mult_component ``` hoelzl@37489 ` 146` ``` vector_smult_component vector_minus_component vector_uminus_component ``` hoelzl@37489 ` 147` ``` vector_scaleR_component cond_component ``` hoelzl@37489 ` 148` hoelzl@37489 ` 149` ```subsection {* Some frequently useful arithmetic lemmas over vectors. *} ``` hoelzl@37489 ` 150` huffman@44136 ` 151` ```instance vec :: (semigroup_mult, finite) semigroup_mult ``` huffman@44136 ` 152` ``` by default (vector mult_assoc) ``` hoelzl@37489 ` 153` huffman@44136 ` 154` ```instance vec :: (monoid_mult, finite) monoid_mult ``` huffman@44136 ` 155` ``` by default vector+ ``` hoelzl@37489 ` 156` huffman@44136 ` 157` ```instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult ``` huffman@44136 ` 158` ``` by default (vector mult_commute) ``` hoelzl@37489 ` 159` huffman@44136 ` 160` ```instance vec :: (ab_semigroup_idem_mult, finite) ab_semigroup_idem_mult ``` huffman@44136 ` 161` ``` by default (vector mult_idem) ``` hoelzl@37489 ` 162` huffman@44136 ` 163` ```instance vec :: (comm_monoid_mult, finite) comm_monoid_mult ``` huffman@44136 ` 164` ``` by default vector ``` hoelzl@37489 ` 165` huffman@44136 ` 166` ```instance vec :: (semiring, finite) semiring ``` huffman@44136 ` 167` ``` by default (vector field_simps)+ ``` hoelzl@37489 ` 168` huffman@44136 ` 169` ```instance vec :: (semiring_0, finite) semiring_0 ``` huffman@44136 ` 170` ``` by default (vector field_simps)+ ``` huffman@44136 ` 171` ```instance vec :: (semiring_1, finite) semiring_1 ``` huffman@44136 ` 172` ``` by default vector ``` huffman@44136 ` 173` ```instance vec :: (comm_semiring, finite) comm_semiring ``` huffman@44136 ` 174` ``` by default (vector field_simps)+ ``` hoelzl@37489 ` 175` huffman@44136 ` 176` ```instance vec :: (comm_semiring_0, finite) comm_semiring_0 .. ``` huffman@44136 ` 177` ```instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. ``` huffman@44136 ` 178` ```instance vec :: (semiring_0_cancel, finite) semiring_0_cancel .. ``` huffman@44136 ` 179` ```instance vec :: (comm_semiring_0_cancel, finite) comm_semiring_0_cancel .. ``` huffman@44136 ` 180` ```instance vec :: (ring, finite) ring .. ``` huffman@44136 ` 181` ```instance vec :: (semiring_1_cancel, finite) semiring_1_cancel .. ``` huffman@44136 ` 182` ```instance vec :: (comm_semiring_1, finite) comm_semiring_1 .. ``` hoelzl@37489 ` 183` huffman@44136 ` 184` ```instance vec :: (ring_1, finite) ring_1 .. ``` hoelzl@37489 ` 185` huffman@44136 ` 186` ```instance vec :: (real_algebra, finite) real_algebra ``` hoelzl@37489 ` 187` ``` apply intro_classes ``` huffman@44136 ` 188` ``` apply (simp_all add: vec_eq_iff) ``` hoelzl@37489 ` 189` ``` done ``` hoelzl@37489 ` 190` huffman@44136 ` 191` ```instance vec :: (real_algebra_1, finite) real_algebra_1 .. ``` hoelzl@37489 ` 192` hoelzl@37489 ` 193` ```lemma of_nat_index: ``` hoelzl@37489 ` 194` ``` "(of_nat n :: 'a::semiring_1 ^'n)\$i = of_nat n" ``` hoelzl@37489 ` 195` ``` apply (induct n) ``` hoelzl@37489 ` 196` ``` apply vector ``` hoelzl@37489 ` 197` ``` apply vector ``` hoelzl@37489 ` 198` ``` done ``` hoelzl@37489 ` 199` hoelzl@37489 ` 200` ```lemma one_index[simp]: ``` hoelzl@37489 ` 201` ``` "(1 :: 'a::one ^'n)\$i = 1" by vector ``` hoelzl@37489 ` 202` huffman@44136 ` 203` ```instance vec :: (semiring_char_0, finite) semiring_char_0 ``` haftmann@38621 ` 204` ```proof ``` haftmann@38621 ` 205` ``` fix m n :: nat ``` haftmann@38621 ` 206` ``` show "inj (of_nat :: nat \ 'a ^ 'b)" ``` huffman@44136 ` 207` ``` by (auto intro!: injI simp add: vec_eq_iff of_nat_index) ``` hoelzl@37489 ` 208` ```qed ``` hoelzl@37489 ` 209` huffman@44136 ` 210` ```instance vec :: (comm_ring_1, finite) comm_ring_1 .. ``` huffman@44136 ` 211` ```instance vec :: (ring_char_0, finite) ring_char_0 .. ``` hoelzl@37489 ` 212` hoelzl@37489 ` 213` ```lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" ``` hoelzl@37489 ` 214` ``` by (vector mult_assoc) ``` hoelzl@37489 ` 215` ```lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x" ``` hoelzl@37489 ` 216` ``` by (vector field_simps) ``` hoelzl@37489 ` 217` ```lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y" ``` hoelzl@37489 ` 218` ``` by (vector field_simps) ``` hoelzl@37489 ` 219` ```lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector ``` hoelzl@37489 ` 220` ```lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector ``` hoelzl@37489 ` 221` ```lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y" ``` hoelzl@37489 ` 222` ``` by (vector field_simps) ``` hoelzl@37489 ` 223` ```lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector ``` hoelzl@37489 ` 224` ```lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector ``` hoelzl@37489 ` 225` ```lemma vector_sneg_minus1: "-x = (- (1::'a::ring_1)) *s x" by vector ``` hoelzl@37489 ` 226` ```lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector ``` hoelzl@37489 ` 227` ```lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x" ``` hoelzl@37489 ` 228` ``` by (vector field_simps) ``` hoelzl@37489 ` 229` hoelzl@37489 ` 230` ```lemma vec_eq[simp]: "(vec m = vec n) \ (m = n)" ``` huffman@44136 ` 231` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 232` hoelzl@37489 ` 233` ```lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) ``` hoelzl@37489 ` 234` ```lemma vector_mul_eq_0[simp]: "(a *s x = 0) \ a = (0::'a::idom) \ x = 0" ``` hoelzl@37489 ` 235` ``` by vector ``` hoelzl@37489 ` 236` ```lemma vector_mul_lcancel[simp]: "a *s x = a *s y \ a = (0::real) \ x = y" ``` hoelzl@37489 ` 237` ``` by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) ``` hoelzl@37489 ` 238` ```lemma vector_mul_rcancel[simp]: "a *s x = b *s x \ (a::real) = b \ x = 0" ``` hoelzl@37489 ` 239` ``` by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) ``` hoelzl@37489 ` 240` ```lemma vector_mul_lcancel_imp: "a \ (0::real) ==> a *s x = a *s y ==> (x = y)" ``` hoelzl@37489 ` 241` ``` by (metis vector_mul_lcancel) ``` hoelzl@37489 ` 242` ```lemma vector_mul_rcancel_imp: "x \ 0 \ (a::real) *s x = b *s x ==> a = b" ``` hoelzl@37489 ` 243` ``` by (metis vector_mul_rcancel) ``` hoelzl@37489 ` 244` hoelzl@37489 ` 245` ```lemma component_le_norm_cart: "\x\$i\ <= norm x" ``` huffman@44136 ` 246` ``` apply (simp add: norm_vec_def) ``` hoelzl@37489 ` 247` ``` apply (rule member_le_setL2, simp_all) ``` hoelzl@37489 ` 248` ``` done ``` hoelzl@37489 ` 249` hoelzl@37489 ` 250` ```lemma norm_bound_component_le_cart: "norm x <= e ==> \x\$i\ <= e" ``` hoelzl@37489 ` 251` ``` by (metis component_le_norm_cart order_trans) ``` hoelzl@37489 ` 252` hoelzl@37489 ` 253` ```lemma norm_bound_component_lt_cart: "norm x < e ==> \x\$i\ < e" ``` hoelzl@37489 ` 254` ``` by (metis component_le_norm_cart basic_trans_rules(21)) ``` hoelzl@37489 ` 255` hoelzl@37489 ` 256` ```lemma norm_le_l1_cart: "norm x <= setsum(\i. \x\$i\) UNIV" ``` huffman@44136 ` 257` ``` by (simp add: norm_vec_def setL2_le_setsum) ``` hoelzl@37489 ` 258` hoelzl@37489 ` 259` ```lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x" ``` huffman@44136 ` 260` ``` unfolding scaleR_vec_def vector_scalar_mult_def by simp ``` hoelzl@37489 ` 261` hoelzl@37489 ` 262` ```lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \c\ * dist x y" ``` hoelzl@37489 ` 263` ``` unfolding dist_norm scalar_mult_eq_scaleR ``` hoelzl@37489 ` 264` ``` unfolding scaleR_right_diff_distrib[symmetric] by simp ``` hoelzl@37489 ` 265` hoelzl@37489 ` 266` ```lemma setsum_component [simp]: ``` hoelzl@37489 ` 267` ``` fixes f:: " 'a \ ('b::comm_monoid_add) ^'n" ``` hoelzl@37489 ` 268` ``` shows "(setsum f S)\$i = setsum (\x. (f x)\$i) S" ``` hoelzl@37489 ` 269` ``` by (cases "finite S", induct S set: finite, simp_all) ``` hoelzl@37489 ` 270` hoelzl@37489 ` 271` ```lemma setsum_eq: "setsum f S = (\ i. setsum (\x. (f x)\$i ) S)" ``` huffman@44136 ` 272` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 273` hoelzl@37489 ` 274` ```lemma setsum_cmul: ``` hoelzl@37489 ` 275` ``` fixes f:: "'c \ ('a::semiring_1)^'n" ``` hoelzl@37489 ` 276` ``` shows "setsum (\x. c *s f x) S = c *s setsum f S" ``` huffman@44136 ` 277` ``` by (simp add: vec_eq_iff setsum_right_distrib) ``` hoelzl@37489 ` 278` hoelzl@37489 ` 279` ```(* TODO: use setsum_norm_allsubsets_bound *) ``` hoelzl@37489 ` 280` ```lemma setsum_norm_allsubsets_bound_cart: ``` hoelzl@37489 ` 281` ``` fixes f:: "'a \ real ^'n" ``` hoelzl@37489 ` 282` ``` assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" ``` hoelzl@37489 ` 283` ``` shows "setsum (\x. norm (f x)) P \ 2 * real CARD('n) * e" ``` hoelzl@37489 ` 284` ```proof- ``` hoelzl@37489 ` 285` ``` let ?d = "real CARD('n)" ``` hoelzl@37489 ` 286` ``` let ?nf = "\x. norm (f x)" ``` hoelzl@37489 ` 287` ``` let ?U = "UNIV :: 'n set" ``` hoelzl@37489 ` 288` ``` have th0: "setsum (\x. setsum (\i. \f x \$ i\) ?U) P = setsum (\i. setsum (\x. \f x \$ i\) P) ?U" ``` hoelzl@37489 ` 289` ``` by (rule setsum_commute) ``` hoelzl@37489 ` 290` ``` have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def) ``` hoelzl@37489 ` 291` ``` have "setsum ?nf P \ setsum (\x. setsum (\i. \f x \$ i\) ?U) P" ``` hoelzl@37489 ` 292` ``` apply (rule setsum_mono) by (rule norm_le_l1_cart) ``` hoelzl@37489 ` 293` ``` also have "\ \ 2 * ?d * e" ``` hoelzl@37489 ` 294` ``` unfolding th0 th1 ``` hoelzl@37489 ` 295` ``` proof(rule setsum_bounded) ``` hoelzl@37489 ` 296` ``` fix i assume i: "i \ ?U" ``` hoelzl@37489 ` 297` ``` let ?Pp = "{x. x\ P \ f x \$ i \ 0}" ``` hoelzl@37489 ` 298` ``` let ?Pn = "{x. x \ P \ f x \$ i < 0}" ``` hoelzl@37489 ` 299` ``` have thp: "P = ?Pp \ ?Pn" by auto ``` hoelzl@37489 ` 300` ``` have thp0: "?Pp \ ?Pn ={}" by auto ``` hoelzl@37489 ` 301` ``` have PpP: "?Pp \ P" and PnP: "?Pn \ P" by blast+ ``` hoelzl@37489 ` 302` ``` have Ppe:"setsum (\x. \f x \$ i\) ?Pp \ e" ``` hoelzl@37489 ` 303` ``` using component_le_norm_cart[of "setsum (\x. f x) ?Pp" i] fPs[OF PpP] ``` hoelzl@37489 ` 304` ``` by (auto intro: abs_le_D1) ``` hoelzl@37489 ` 305` ``` have Pne: "setsum (\x. \f x \$ i\) ?Pn \ e" ``` hoelzl@37489 ` 306` ``` using component_le_norm_cart[of "setsum (\x. - f x) ?Pn" i] fPs[OF PnP] ``` hoelzl@37489 ` 307` ``` by (auto simp add: setsum_negf intro: abs_le_D1) ``` hoelzl@37489 ` 308` ``` have "setsum (\x. \f x \$ i\) P = setsum (\x. \f x \$ i\) ?Pp + setsum (\x. \f x \$ i\) ?Pn" ``` hoelzl@37489 ` 309` ``` apply (subst thp) ``` hoelzl@37489 ` 310` ``` apply (rule setsum_Un_zero) ``` hoelzl@37489 ` 311` ``` using fP thp0 by auto ``` hoelzl@37489 ` 312` ``` also have "\ \ 2*e" using Pne Ppe by arith ``` hoelzl@37489 ` 313` ``` finally show "setsum (\x. \f x \$ i\) P \ 2*e" . ``` hoelzl@37489 ` 314` ``` qed ``` hoelzl@37489 ` 315` ``` finally show ?thesis . ``` hoelzl@37489 ` 316` ```qed ``` hoelzl@37489 ` 317` hoelzl@37489 ` 318` ```lemma if_distr: "(if P then f else g) \$ i = (if P then f \$ i else g \$ i)" by simp ``` hoelzl@37489 ` 319` hoelzl@37489 ` 320` ```lemma split_dimensions'[consumes 1]: ``` huffman@44129 ` 321` ``` assumes "k < DIM('a::euclidean_space^'b)" ``` huffman@44129 ` 322` ``` obtains i j where "i < CARD('b::finite)" and "j < DIM('a::euclidean_space)" and "k = j + i * DIM('a::euclidean_space)" ``` hoelzl@37489 ` 323` ```using split_times_into_modulo[OF assms[simplified]] . ``` hoelzl@37489 ` 324` hoelzl@37489 ` 325` ```lemma cart_euclidean_bound[intro]: ``` huffman@44129 ` 326` ``` assumes j:"j < DIM('a::euclidean_space)" ``` huffman@44129 ` 327` ``` shows "j + \' (i::'b::finite) * DIM('a) < CARD('b) * DIM('a::euclidean_space)" ``` hoelzl@37489 ` 328` ``` using linear_less_than_times[OF pi'_range j, of i] . ``` hoelzl@37489 ` 329` huffman@44129 ` 330` ```lemma (in euclidean_space) forall_CARD_DIM: ``` hoelzl@37489 ` 331` ``` "(\i (\(i::'b::finite) j. j P (j + \' i * DIM('a)))" ``` hoelzl@37489 ` 332` ``` (is "?l \ ?r") ``` hoelzl@37489 ` 333` ```proof (safe elim!: split_times_into_modulo) ``` hoelzl@37489 ` 334` ``` fix i :: 'b and j assume "j < DIM('a)" ``` hoelzl@37489 ` 335` ``` note linear_less_than_times[OF pi'_range[of i] this] ``` hoelzl@37489 ` 336` ``` moreover assume "?l" ``` hoelzl@37489 ` 337` ``` ultimately show "P (j + \' i * DIM('a))" by auto ``` hoelzl@37489 ` 338` ```next ``` hoelzl@37489 ` 339` ``` fix i j assume "i < CARD('b)" "j < DIM('a)" and "?r" ``` hoelzl@37489 ` 340` ``` from `?r`[rule_format, OF `j < DIM('a)`, of "\ i"] `i < CARD('b)` ``` hoelzl@37489 ` 341` ``` show "P (j + i * DIM('a))" by simp ``` hoelzl@37489 ` 342` ```qed ``` hoelzl@37489 ` 343` huffman@44129 ` 344` ```lemma (in euclidean_space) exists_CARD_DIM: ``` hoelzl@37489 ` 345` ``` "(\i (\i::'b::finite. \j' i * DIM('a)))" ``` hoelzl@37489 ` 346` ``` using forall_CARD_DIM[where 'b='b, of "\x. \ P x"] by blast ``` hoelzl@37489 ` 347` hoelzl@37489 ` 348` ```lemma forall_CARD: ``` hoelzl@37489 ` 349` ``` "(\i (\i::'b::finite. P (\' i))" ``` hoelzl@37489 ` 350` ``` using forall_CARD_DIM[where 'a=real, of P] by simp ``` hoelzl@37489 ` 351` hoelzl@37489 ` 352` ```lemma exists_CARD: ``` hoelzl@37489 ` 353` ``` "(\i (\i::'b::finite. P (\' i))" ``` hoelzl@37489 ` 354` ``` using exists_CARD_DIM[where 'a=real, of P] by simp ``` hoelzl@37489 ` 355` hoelzl@37489 ` 356` ```lemmas cart_simps = forall_CARD_DIM exists_CARD_DIM forall_CARD exists_CARD ``` hoelzl@37489 ` 357` hoelzl@37489 ` 358` ```lemma cart_euclidean_nth[simp]: ``` huffman@44136 ` 359` ``` fixes x :: "('a::euclidean_space, 'b::finite) vec" ``` hoelzl@37489 ` 360` ``` assumes j:"j < DIM('a)" ``` hoelzl@37489 ` 361` ``` shows "x \$\$ (j + \' i * DIM('a)) = x \$ i \$\$ j" ``` huffman@44136 ` 362` ``` unfolding euclidean_component_def inner_vec_def basis_eq_pi'[OF j] if_distrib cond_application_beta ``` hoelzl@37489 ` 363` ``` by (simp add: setsum_cases) ``` hoelzl@37489 ` 364` hoelzl@37489 ` 365` ```lemma real_euclidean_nth: ``` hoelzl@37489 ` 366` ``` fixes x :: "real^'n" ``` hoelzl@37489 ` 367` ``` shows "x \$\$ \' i = (x \$ i :: real)" ``` hoelzl@37489 ` 368` ``` using cart_euclidean_nth[where 'a=real, of 0 x i] by simp ``` hoelzl@37489 ` 369` hoelzl@37489 ` 370` ```lemmas nth_conv_component = real_euclidean_nth[symmetric] ``` hoelzl@37489 ` 371` hoelzl@37489 ` 372` ```lemma mult_split_eq: ``` hoelzl@37489 ` 373` ``` fixes A :: nat assumes "x < A" "y < A" ``` hoelzl@37489 ` 374` ``` shows "x + i * A = y + j * A \ x = y \ i = j" ``` hoelzl@37489 ` 375` ```proof ``` hoelzl@37489 ` 376` ``` assume *: "x + i * A = y + j * A" ``` hoelzl@37489 ` 377` ``` { fix x y i j assume "i < j" "x < A" and *: "x + i * A = y + j * A" ``` hoelzl@37489 ` 378` ``` hence "x + i * A < Suc i * A" using `x < A` by simp ``` hoelzl@37489 ` 379` ``` also have "\ \ j * A" using `i < j` unfolding mult_le_cancel2 by simp ``` hoelzl@37489 ` 380` ``` also have "\ \ y + j * A" by simp ``` hoelzl@37489 ` 381` ``` finally have "i = j" using * by simp } ``` hoelzl@37489 ` 382` ``` note eq = this ``` hoelzl@37489 ` 383` hoelzl@37489 ` 384` ``` have "i = j" ``` hoelzl@37489 ` 385` ``` proof (cases rule: linorder_cases) ``` hoelzl@37489 ` 386` ``` assume "i < j" from eq[OF this `x < A` *] show "i = j" by simp ``` hoelzl@37489 ` 387` ``` next ``` hoelzl@37489 ` 388` ``` assume "j < i" from eq[OF this `y < A` *[symmetric]] show "i = j" by simp ``` hoelzl@37489 ` 389` ``` qed simp ``` hoelzl@37489 ` 390` ``` thus "x = y \ i = j" using * by simp ``` hoelzl@37489 ` 391` ```qed simp ``` hoelzl@37489 ` 392` huffman@44136 ` 393` ```instance vec :: (ordered_euclidean_space, finite) ordered_euclidean_space ``` hoelzl@37489 ` 394` ```proof ``` hoelzl@37489 ` 395` ``` fix x y::"'a^'b" ``` huffman@44136 ` 396` ``` show "(x \ y) = (\i y \$\$ i)" ``` huffman@44136 ` 397` ``` unfolding less_eq_vec_def apply(subst eucl_le) by (simp add: cart_simps) ``` huffman@44136 ` 398` ``` show"(x < y) = (\i i. if i = k then 1 else 0)" ``` hoelzl@37489 ` 405` hoelzl@37489 ` 406` ```lemma basis_component [simp]: "cart_basis k \$ i = (if k=i then 1 else 0)" ``` hoelzl@37489 ` 407` ``` unfolding cart_basis_def by simp ``` hoelzl@37489 ` 408` hoelzl@37489 ` 409` ```lemma norm_basis[simp]: ``` hoelzl@37489 ` 410` ``` shows "norm (cart_basis k :: real ^'n) = 1" ``` huffman@44136 ` 411` ``` apply (simp add: cart_basis_def norm_eq_sqrt_inner) unfolding inner_vec_def ``` hoelzl@37489 ` 412` ``` apply (vector delta_mult_idempotent) ``` hoelzl@37489 ` 413` ``` using setsum_delta[of "UNIV :: 'n set" "k" "\k. 1::real"] by auto ``` hoelzl@37489 ` 414` hoelzl@37489 ` 415` ```lemma norm_basis_1: "norm(cart_basis 1 :: real ^'n::{finite,one}) = 1" ``` hoelzl@37489 ` 416` ``` by (rule norm_basis) ``` hoelzl@37489 ` 417` hoelzl@37489 ` 418` ```lemma vector_choose_size: "0 <= c ==> \(x::real^'n). norm x = c" ``` hoelzl@37489 ` 419` ``` by (rule exI[where x="c *\<^sub>R cart_basis arbitrary"]) simp ``` hoelzl@37489 ` 420` hoelzl@37489 ` 421` ```lemma vector_choose_dist: assumes e: "0 <= e" ``` hoelzl@37489 ` 422` ``` shows "\(y::real^'n). dist x y = e" ``` hoelzl@37489 ` 423` ```proof- ``` hoelzl@37489 ` 424` ``` from vector_choose_size[OF e] obtain c:: "real ^'n" where "norm c = e" ``` hoelzl@37489 ` 425` ``` by blast ``` hoelzl@37489 ` 426` ``` then have "dist x (x - c) = e" by (simp add: dist_norm) ``` hoelzl@37489 ` 427` ``` then show ?thesis by blast ``` hoelzl@37489 ` 428` ```qed ``` hoelzl@37489 ` 429` hoelzl@37489 ` 430` ```lemma basis_inj[intro]: "inj (cart_basis :: 'n \ real ^'n)" ``` huffman@44136 ` 431` ``` by (simp add: inj_on_def vec_eq_iff) ``` hoelzl@37489 ` 432` hoelzl@37489 ` 433` ```lemma basis_expansion: ``` hoelzl@37489 ` 434` ``` "setsum (\i. (x\$i) *s cart_basis i) UNIV = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") ``` huffman@44136 ` 435` ``` by (auto simp add: vec_eq_iff if_distrib setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong) ``` hoelzl@37489 ` 436` hoelzl@37489 ` 437` ```lemma smult_conv_scaleR: "c *s x = scaleR c x" ``` huffman@44136 ` 438` ``` unfolding vector_scalar_mult_def scaleR_vec_def by simp ``` hoelzl@37489 ` 439` hoelzl@37489 ` 440` ```lemma basis_expansion': ``` hoelzl@37489 ` 441` ``` "setsum (\i. (x\$i) *\<^sub>R cart_basis i) UNIV = x" ``` hoelzl@37489 ` 442` ``` by (rule basis_expansion [where 'a=real, unfolded smult_conv_scaleR]) ``` hoelzl@37489 ` 443` hoelzl@37489 ` 444` ```lemma basis_expansion_unique: ``` hoelzl@37489 ` 445` ``` "setsum (\i. f i *s cart_basis i) UNIV = (x::('a::comm_ring_1) ^'n) \ (\i. f i = x\$i)" ``` huffman@44136 ` 446` ``` by (simp add: vec_eq_iff setsum_delta if_distrib cong del: if_weak_cong) ``` hoelzl@37489 ` 447` hoelzl@37489 ` 448` ```lemma dot_basis: ``` hoelzl@37489 ` 449` ``` shows "cart_basis i \ x = x\$i" "x \ (cart_basis i) = (x\$i)" ``` huffman@44136 ` 450` ``` by (auto simp add: inner_vec_def cart_basis_def cond_application_beta if_distrib setsum_delta ``` hoelzl@37489 ` 451` ``` cong del: if_weak_cong) ``` hoelzl@37489 ` 452` hoelzl@37489 ` 453` ```lemma inner_basis: ``` hoelzl@37489 ` 454` ``` fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n" ``` hoelzl@37489 ` 455` ``` shows "inner (cart_basis i) x = inner 1 (x \$ i)" ``` hoelzl@37489 ` 456` ``` and "inner x (cart_basis i) = inner (x \$ i) 1" ``` huffman@44136 ` 457` ``` unfolding inner_vec_def cart_basis_def ``` hoelzl@37489 ` 458` ``` by (auto simp add: cond_application_beta if_distrib setsum_delta cong del: if_weak_cong) ``` hoelzl@37489 ` 459` hoelzl@37489 ` 460` ```lemma basis_eq_0: "cart_basis i = (0::'a::semiring_1^'n) \ False" ``` huffman@44136 ` 461` ``` by (auto simp add: vec_eq_iff) ``` hoelzl@37489 ` 462` hoelzl@37489 ` 463` ```lemma basis_nonzero: ``` hoelzl@37489 ` 464` ``` shows "cart_basis k \ (0:: 'a::semiring_1 ^'n)" ``` hoelzl@37489 ` 465` ``` by (simp add: basis_eq_0) ``` hoelzl@37489 ` 466` hoelzl@37489 ` 467` ```text {* some lemmas to map between Eucl and Cart *} ``` hoelzl@37489 ` 468` ```lemma basis_real_n[simp]:"(basis (\' i)::real^'a) = cart_basis i" ``` huffman@44136 ` 469` ``` unfolding basis_vec_def using pi'_range[where 'n='a] ``` huffman@44166 ` 470` ``` by (auto simp: vec_eq_iff axis_def) ``` hoelzl@37489 ` 471` hoelzl@37489 ` 472` ```subsection {* Orthogonality on cartesian products *} ``` hoelzl@37489 ` 473` hoelzl@37489 ` 474` ```lemma orthogonal_basis: ``` hoelzl@37489 ` 475` ``` shows "orthogonal (cart_basis i) x \ x\$i = (0::real)" ``` huffman@44136 ` 476` ``` by (auto simp add: orthogonal_def inner_vec_def cart_basis_def if_distrib ``` hoelzl@37489 ` 477` ``` cond_application_beta setsum_delta cong del: if_weak_cong) ``` hoelzl@37489 ` 478` hoelzl@37489 ` 479` ```lemma orthogonal_basis_basis: ``` hoelzl@37489 ` 480` ``` shows "orthogonal (cart_basis i :: real^'n) (cart_basis j) \ i \ j" ``` hoelzl@37489 ` 481` ``` unfolding orthogonal_basis[of i] basis_component[of j] by simp ``` hoelzl@37489 ` 482` hoelzl@37489 ` 483` ```subsection {* Linearity on cartesian products *} ``` hoelzl@37489 ` 484` hoelzl@37489 ` 485` ```lemma linear_vmul_component: ``` hoelzl@37489 ` 486` ``` assumes lf: "linear f" ``` hoelzl@37489 ` 487` ``` shows "linear (\x. f x \$ k *\<^sub>R v)" ``` hoelzl@37489 ` 488` ``` using lf ``` hoelzl@37489 ` 489` ``` by (auto simp add: linear_def algebra_simps) ``` hoelzl@37489 ` 490` hoelzl@37489 ` 491` hoelzl@37489 ` 492` ```subsection{* Adjoints on cartesian products *} ``` hoelzl@37489 ` 493` hoelzl@37489 ` 494` ```text {* TODO: The following lemmas about adjoints should hold for any ``` hoelzl@37489 ` 495` ```Hilbert space (i.e. complete inner product space). ``` hoelzl@37489 ` 496` ```(see \url{http://en.wikipedia.org/wiki/Hermitian_adjoint}) ``` hoelzl@37489 ` 497` ```*} ``` hoelzl@37489 ` 498` hoelzl@37489 ` 499` ```lemma adjoint_works_lemma: ``` hoelzl@37489 ` 500` ``` fixes f:: "real ^'n \ real ^'m" ``` hoelzl@37489 ` 501` ``` assumes lf: "linear f" ``` hoelzl@37489 ` 502` ``` shows "\x y. f x \ y = x \ adjoint f y" ``` hoelzl@37489 ` 503` ```proof- ``` hoelzl@37489 ` 504` ``` let ?N = "UNIV :: 'n set" ``` hoelzl@37489 ` 505` ``` let ?M = "UNIV :: 'm set" ``` hoelzl@37489 ` 506` ``` have fN: "finite ?N" by simp ``` hoelzl@37489 ` 507` ``` have fM: "finite ?M" by simp ``` hoelzl@37489 ` 508` ``` {fix y:: "real ^ 'm" ``` hoelzl@37489 ` 509` ``` let ?w = "(\ i. (f (cart_basis i) \ y)) :: real ^ 'n" ``` hoelzl@37489 ` 510` ``` {fix x ``` hoelzl@37489 ` 511` ``` have "f x \ y = f (setsum (\i. (x\$i) *\<^sub>R cart_basis i) ?N) \ y" ``` hoelzl@37489 ` 512` ``` by (simp only: basis_expansion') ``` hoelzl@37489 ` 513` ``` also have "\ = (setsum (\i. (x\$i) *\<^sub>R f (cart_basis i)) ?N) \ y" ``` hoelzl@37489 ` 514` ``` unfolding linear_setsum[OF lf fN] ``` hoelzl@37489 ` 515` ``` by (simp add: linear_cmul[OF lf]) ``` hoelzl@37489 ` 516` ``` finally have "f x \ y = x \ ?w" ``` hoelzl@37489 ` 517` ``` apply (simp only: ) ``` huffman@44136 ` 518` ``` apply (simp add: inner_vec_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] field_simps) ``` hoelzl@37489 ` 519` ``` done} ``` hoelzl@37489 ` 520` ``` } ``` hoelzl@37489 ` 521` ``` then show ?thesis unfolding adjoint_def ``` hoelzl@37489 ` 522` ``` some_eq_ex[of "\f'. \x y. f x \ y = x \ f' y"] ``` hoelzl@37489 ` 523` ``` using choice_iff[of "\a b. \x. f x \ a = x \ b "] ``` hoelzl@37489 ` 524` ``` by metis ``` hoelzl@37489 ` 525` ```qed ``` hoelzl@37489 ` 526` hoelzl@37489 ` 527` ```lemma adjoint_works: ``` hoelzl@37489 ` 528` ``` fixes f:: "real ^'n \ real ^'m" ``` hoelzl@37489 ` 529` ``` assumes lf: "linear f" ``` hoelzl@37489 ` 530` ``` shows "x \ adjoint f y = f x \ y" ``` hoelzl@37489 ` 531` ``` using adjoint_works_lemma[OF lf] by metis ``` hoelzl@37489 ` 532` hoelzl@37489 ` 533` ```lemma adjoint_linear: ``` hoelzl@37489 ` 534` ``` fixes f:: "real ^'n \ real ^'m" ``` hoelzl@37489 ` 535` ``` assumes lf: "linear f" ``` hoelzl@37489 ` 536` ``` shows "linear (adjoint f)" ``` hoelzl@37489 ` 537` ``` unfolding linear_def vector_eq_ldot[where 'a="real^'n", symmetric] apply safe ``` hoelzl@37489 ` 538` ``` unfolding inner_simps smult_conv_scaleR adjoint_works[OF lf] by auto ``` hoelzl@37489 ` 539` hoelzl@37489 ` 540` ```lemma adjoint_clauses: ``` hoelzl@37489 ` 541` ``` fixes f:: "real ^'n \ real ^'m" ``` hoelzl@37489 ` 542` ``` assumes lf: "linear f" ``` hoelzl@37489 ` 543` ``` shows "x \ adjoint f y = f x \ y" ``` hoelzl@37489 ` 544` ``` and "adjoint f y \ x = y \ f x" ``` hoelzl@37489 ` 545` ``` by (simp_all add: adjoint_works[OF lf] inner_commute) ``` hoelzl@37489 ` 546` hoelzl@37489 ` 547` ```lemma adjoint_adjoint: ``` hoelzl@37489 ` 548` ``` fixes f:: "real ^'n \ real ^'m" ``` hoelzl@37489 ` 549` ``` assumes lf: "linear f" ``` hoelzl@37489 ` 550` ``` shows "adjoint (adjoint f) = f" ``` hoelzl@37489 ` 551` ``` by (rule adjoint_unique, simp add: adjoint_clauses [OF lf]) ``` hoelzl@37489 ` 552` hoelzl@37489 ` 553` hoelzl@37489 ` 554` ```subsection {* Matrix operations *} ``` hoelzl@37489 ` 555` hoelzl@37489 ` 556` ```text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *} ``` hoelzl@37489 ` 557` hoelzl@37489 ` 558` ```definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \ 'a ^'p^'n \ 'a ^ 'p ^'m" (infixl "**" 70) ``` hoelzl@37489 ` 559` ``` where "m ** m' == (\ i j. setsum (\k. ((m\$i)\$k) * ((m'\$k)\$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m" ``` hoelzl@37489 ` 560` hoelzl@37489 ` 561` ```definition matrix_vector_mult :: "('a::semiring_1) ^'n^'m \ 'a ^'n \ 'a ^ 'm" (infixl "*v" 70) ``` hoelzl@37489 ` 562` ``` where "m *v x \ (\ i. setsum (\j. ((m\$i)\$j) * (x\$j)) (UNIV ::'n set)) :: 'a^'m" ``` hoelzl@37489 ` 563` hoelzl@37489 ` 564` ```definition vector_matrix_mult :: "'a ^ 'm \ ('a::semiring_1) ^'n^'m \ 'a ^'n " (infixl "v*" 70) ``` hoelzl@37489 ` 565` ``` where "v v* m == (\ j. setsum (\i. ((m\$i)\$j) * (v\$i)) (UNIV :: 'm set)) :: 'a^'n" ``` hoelzl@37489 ` 566` hoelzl@37489 ` 567` ```definition "(mat::'a::zero => 'a ^'n^'n) k = (\ i j. if i = j then k else 0)" ``` hoelzl@37489 ` 568` ```definition transpose where ``` hoelzl@37489 ` 569` ``` "(transpose::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A\$j)\$i))" ``` hoelzl@37489 ` 570` ```definition "(row::'m => 'a ^'n^'m \ 'a ^'n) i A = (\ j. ((A\$i)\$j))" ``` hoelzl@37489 ` 571` ```definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\ i. ((A\$i)\$j))" ``` hoelzl@37489 ` 572` ```definition "rows(A::'a^'n^'m) = { row i A | i. i \ (UNIV :: 'm set)}" ``` hoelzl@37489 ` 573` ```definition "columns(A::'a^'n^'m) = { column i A | i. i \ (UNIV :: 'n set)}" ``` hoelzl@37489 ` 574` hoelzl@37489 ` 575` ```lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) ``` hoelzl@37489 ` 576` ```lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" ``` hoelzl@37489 ` 577` ``` by (vector matrix_matrix_mult_def setsum_addf[symmetric] field_simps) ``` hoelzl@37489 ` 578` hoelzl@37489 ` 579` ```lemma matrix_mul_lid: ``` hoelzl@37489 ` 580` ``` fixes A :: "'a::semiring_1 ^ 'm ^ 'n" ``` hoelzl@37489 ` 581` ``` shows "mat 1 ** A = A" ``` hoelzl@37489 ` 582` ``` apply (simp add: matrix_matrix_mult_def mat_def) ``` hoelzl@37489 ` 583` ``` apply vector ``` hoelzl@37489 ` 584` ``` by (auto simp only: if_distrib cond_application_beta setsum_delta'[OF finite] mult_1_left mult_zero_left if_True UNIV_I) ``` hoelzl@37489 ` 585` hoelzl@37489 ` 586` hoelzl@37489 ` 587` ```lemma matrix_mul_rid: ``` hoelzl@37489 ` 588` ``` fixes A :: "'a::semiring_1 ^ 'm ^ 'n" ``` hoelzl@37489 ` 589` ``` shows "A ** mat 1 = A" ``` hoelzl@37489 ` 590` ``` apply (simp add: matrix_matrix_mult_def mat_def) ``` hoelzl@37489 ` 591` ``` apply vector ``` hoelzl@37489 ` 592` ``` by (auto simp only: if_distrib cond_application_beta setsum_delta[OF finite] mult_1_right mult_zero_right if_True UNIV_I cong: if_cong) ``` hoelzl@37489 ` 593` hoelzl@37489 ` 594` ```lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" ``` hoelzl@37489 ` 595` ``` apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc) ``` hoelzl@37489 ` 596` ``` apply (subst setsum_commute) ``` hoelzl@37489 ` 597` ``` apply simp ``` hoelzl@37489 ` 598` ``` done ``` hoelzl@37489 ` 599` hoelzl@37489 ` 600` ```lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" ``` hoelzl@37489 ` 601` ``` apply (vector matrix_matrix_mult_def matrix_vector_mult_def setsum_right_distrib setsum_left_distrib mult_assoc) ``` hoelzl@37489 ` 602` ``` apply (subst setsum_commute) ``` hoelzl@37489 ` 603` ``` apply simp ``` hoelzl@37489 ` 604` ``` done ``` hoelzl@37489 ` 605` hoelzl@37489 ` 606` ```lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" ``` hoelzl@37489 ` 607` ``` apply (vector matrix_vector_mult_def mat_def) ``` hoelzl@37489 ` 608` ``` by (simp add: if_distrib cond_application_beta ``` hoelzl@37489 ` 609` ``` setsum_delta' cong del: if_weak_cong) ``` hoelzl@37489 ` 610` hoelzl@37489 ` 611` ```lemma matrix_transpose_mul: "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)" ``` huffman@44136 ` 612` ``` by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult_commute) ``` hoelzl@37489 ` 613` hoelzl@37489 ` 614` ```lemma matrix_eq: ``` hoelzl@37489 ` 615` ``` fixes A B :: "'a::semiring_1 ^ 'n ^ 'm" ``` hoelzl@37489 ` 616` ``` shows "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") ``` hoelzl@37489 ` 617` ``` apply auto ``` huffman@44136 ` 618` ``` apply (subst vec_eq_iff) ``` hoelzl@37489 ` 619` ``` apply clarify ``` huffman@44136 ` 620` ``` apply (clarsimp simp add: matrix_vector_mult_def cart_basis_def if_distrib cond_application_beta vec_eq_iff cong del: if_weak_cong) ``` hoelzl@37489 ` 621` ``` apply (erule_tac x="cart_basis ia" in allE) ``` hoelzl@37489 ` 622` ``` apply (erule_tac x="i" in allE) ``` hoelzl@37489 ` 623` ``` by (auto simp add: cart_basis_def if_distrib cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong) ``` hoelzl@37489 ` 624` hoelzl@37489 ` 625` ```lemma matrix_vector_mul_component: ``` hoelzl@37489 ` 626` ``` shows "((A::real^_^_) *v x)\$k = (A\$k) \ x" ``` huffman@44136 ` 627` ``` by (simp add: matrix_vector_mult_def inner_vec_def) ``` hoelzl@37489 ` 628` hoelzl@37489 ` 629` ```lemma dot_lmul_matrix: "((x::real ^_) v* A) \ y = x \ (A *v y)" ``` huffman@44136 ` 630` ``` apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac) ``` hoelzl@37489 ` 631` ``` apply (subst setsum_commute) ``` hoelzl@37489 ` 632` ``` by simp ``` hoelzl@37489 ` 633` hoelzl@37489 ` 634` ```lemma transpose_mat: "transpose (mat n) = mat n" ``` hoelzl@37489 ` 635` ``` by (vector transpose_def mat_def) ``` hoelzl@37489 ` 636` hoelzl@37489 ` 637` ```lemma transpose_transpose: "transpose(transpose A) = A" ``` hoelzl@37489 ` 638` ``` by (vector transpose_def) ``` hoelzl@37489 ` 639` hoelzl@37489 ` 640` ```lemma row_transpose: ``` hoelzl@37489 ` 641` ``` fixes A:: "'a::semiring_1^_^_" ``` hoelzl@37489 ` 642` ``` shows "row i (transpose A) = column i A" ``` huffman@44136 ` 643` ``` by (simp add: row_def column_def transpose_def vec_eq_iff) ``` hoelzl@37489 ` 644` hoelzl@37489 ` 645` ```lemma column_transpose: ``` hoelzl@37489 ` 646` ``` fixes A:: "'a::semiring_1^_^_" ``` hoelzl@37489 ` 647` ``` shows "column i (transpose A) = row i A" ``` huffman@44136 ` 648` ``` by (simp add: row_def column_def transpose_def vec_eq_iff) ``` hoelzl@37489 ` 649` hoelzl@37489 ` 650` ```lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A" ``` nipkow@39302 ` 651` ```by (auto simp add: rows_def columns_def row_transpose intro: set_eqI) ``` hoelzl@37489 ` 652` hoelzl@37489 ` 653` ```lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" by (metis transpose_transpose rows_transpose) ``` hoelzl@37489 ` 654` hoelzl@37489 ` 655` ```text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *} ``` hoelzl@37489 ` 656` hoelzl@37489 ` 657` ```lemma matrix_mult_dot: "A *v x = (\ i. A\$i \ x)" ``` huffman@44136 ` 658` ``` by (simp add: matrix_vector_mult_def inner_vec_def) ``` hoelzl@37489 ` 659` hoelzl@37489 ` 660` ```lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\i. (x\$i) *s column i A) (UNIV:: 'n set)" ``` huffman@44136 ` 661` ``` by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult_commute) ``` hoelzl@37489 ` 662` hoelzl@37489 ` 663` ```lemma vector_componentwise: ``` hoelzl@37489 ` 664` ``` "(x::'a::ring_1^'n) = (\ j. setsum (\i. (x\$i) * (cart_basis i :: 'a^'n)\$j) (UNIV :: 'n set))" ``` hoelzl@37489 ` 665` ``` apply (subst basis_expansion[symmetric]) ``` huffman@44136 ` 666` ``` by (vector vec_eq_iff setsum_component) ``` hoelzl@37489 ` 667` hoelzl@37489 ` 668` ```lemma linear_componentwise: ``` hoelzl@37489 ` 669` ``` fixes f:: "real ^'m \ real ^ _" ``` hoelzl@37489 ` 670` ``` assumes lf: "linear f" ``` hoelzl@37489 ` 671` ``` shows "(f x)\$j = setsum (\i. (x\$i) * (f (cart_basis i)\$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") ``` hoelzl@37489 ` 672` ```proof- ``` hoelzl@37489 ` 673` ``` let ?M = "(UNIV :: 'm set)" ``` hoelzl@37489 ` 674` ``` let ?N = "(UNIV :: 'n set)" ``` hoelzl@37489 ` 675` ``` have fM: "finite ?M" by simp ``` hoelzl@37489 ` 676` ``` have "?rhs = (setsum (\i.(x\$i) *\<^sub>R f (cart_basis i) ) ?M)\$j" ``` hoelzl@37489 ` 677` ``` unfolding vector_smult_component[symmetric] smult_conv_scaleR ``` hoelzl@37489 ` 678` ``` unfolding setsum_component[of "(\i.(x\$i) *\<^sub>R f (cart_basis i :: real^'m))" ?M] ``` hoelzl@37489 ` 679` ``` .. ``` hoelzl@37489 ` 680` ``` then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion' .. ``` hoelzl@37489 ` 681` ```qed ``` hoelzl@37489 ` 682` hoelzl@37489 ` 683` ```text{* Inverse matrices (not necessarily square) *} ``` hoelzl@37489 ` 684` hoelzl@37489 ` 685` ```definition "invertible(A::'a::semiring_1^'n^'m) \ (\A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" ``` hoelzl@37489 ` 686` hoelzl@37489 ` 687` ```definition "matrix_inv(A:: 'a::semiring_1^'n^'m) = ``` hoelzl@37489 ` 688` ``` (SOME A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" ``` hoelzl@37489 ` 689` hoelzl@37489 ` 690` ```text{* Correspondence between matrices and linear operators. *} ``` hoelzl@37489 ` 691` hoelzl@37489 ` 692` ```definition matrix:: "('a::{plus,times, one, zero}^'m \ 'a ^ 'n) \ 'a^'m^'n" ``` hoelzl@37489 ` 693` ```where "matrix f = (\ i j. (f(cart_basis j))\$i)" ``` hoelzl@37489 ` 694` hoelzl@37489 ` 695` ```lemma matrix_vector_mul_linear: "linear(\x. A *v (x::real ^ _))" ``` huffman@44136 ` 696` ``` by (simp add: linear_def matrix_vector_mult_def vec_eq_iff field_simps setsum_right_distrib setsum_addf) ``` hoelzl@37489 ` 697` hoelzl@37489 ` 698` ```lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::real ^ 'n)" ``` huffman@44136 ` 699` ```apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult_commute) ``` hoelzl@37489 ` 700` ```apply clarify ``` hoelzl@37489 ` 701` ```apply (rule linear_componentwise[OF lf, symmetric]) ``` hoelzl@37489 ` 702` ```done ``` hoelzl@37489 ` 703` hoelzl@37489 ` 704` ```lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::real ^ 'n))" by (simp add: ext matrix_works) ``` hoelzl@37489 ` 705` hoelzl@37489 ` 706` ```lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: real ^ 'n)) = A" ``` hoelzl@37489 ` 707` ``` by (simp add: matrix_eq matrix_vector_mul_linear matrix_works) ``` hoelzl@37489 ` 708` hoelzl@37489 ` 709` ```lemma matrix_compose: ``` hoelzl@37489 ` 710` ``` assumes lf: "linear (f::real^'n \ real^'m)" ``` hoelzl@37489 ` 711` ``` and lg: "linear (g::real^'m \ real^_)" ``` hoelzl@37489 ` 712` ``` shows "matrix (g o f) = matrix g ** matrix f" ``` hoelzl@37489 ` 713` ``` using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]] ``` hoelzl@37489 ` 714` ``` by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) ``` hoelzl@37489 ` 715` hoelzl@37489 ` 716` ```lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\i. (x\$i) *s ((transpose A)\$i)) (UNIV:: 'n set)" ``` huffman@44136 ` 717` ``` by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult_commute) ``` hoelzl@37489 ` 718` hoelzl@37489 ` 719` ```lemma adjoint_matrix: "adjoint(\x. (A::real^'n^'m) *v x) = (\x. transpose A *v x)" ``` hoelzl@37489 ` 720` ``` apply (rule adjoint_unique) ``` huffman@44136 ` 721` ``` apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) ``` hoelzl@37489 ` 722` ``` apply (subst setsum_commute) ``` hoelzl@37489 ` 723` ``` apply (auto simp add: mult_ac) ``` hoelzl@37489 ` 724` ``` done ``` hoelzl@37489 ` 725` hoelzl@37489 ` 726` ```lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \ real ^'m)" ``` hoelzl@37489 ` 727` ``` shows "matrix(adjoint f) = transpose(matrix f)" ``` hoelzl@37489 ` 728` ``` apply (subst matrix_vector_mul[OF lf]) ``` hoelzl@37489 ` 729` ``` unfolding adjoint_matrix matrix_of_matrix_vector_mul .. ``` hoelzl@37489 ` 730` huffman@44360 ` 731` ```subsection {* lambda skolemization on cartesian products *} ``` hoelzl@37489 ` 732` hoelzl@37489 ` 733` ```(* FIXME: rename do choice_cart *) ``` hoelzl@37489 ` 734` hoelzl@37489 ` 735` ```lemma lambda_skolem: "(\i. \x. P i x) \ ``` hoelzl@37494 ` 736` ``` (\x::'a ^ 'n. \i. P i (x \$ i))" (is "?lhs \ ?rhs") ``` hoelzl@37489 ` 737` ```proof- ``` hoelzl@37489 ` 738` ``` let ?S = "(UNIV :: 'n set)" ``` hoelzl@37489 ` 739` ``` {assume H: "?rhs" ``` hoelzl@37489 ` 740` ``` then have ?lhs by auto} ``` hoelzl@37489 ` 741` ``` moreover ``` hoelzl@37489 ` 742` ``` {assume H: "?lhs" ``` hoelzl@37489 ` 743` ``` then obtain f where f:"\i. P i (f i)" unfolding choice_iff by metis ``` hoelzl@37489 ` 744` ``` let ?x = "(\ i. (f i)) :: 'a ^ 'n" ``` hoelzl@37489 ` 745` ``` {fix i ``` hoelzl@37489 ` 746` ``` from f have "P i (f i)" by metis ``` hoelzl@37494 ` 747` ``` then have "P i (?x \$ i)" by auto ``` hoelzl@37489 ` 748` ``` } ``` hoelzl@37489 ` 749` ``` hence "\i. P i (?x\$i)" by metis ``` hoelzl@37489 ` 750` ``` hence ?rhs by metis } ``` hoelzl@37489 ` 751` ``` ultimately show ?thesis by metis ``` hoelzl@37489 ` 752` ```qed ``` hoelzl@37489 ` 753` hoelzl@37489 ` 754` ```subsection {* Standard bases are a spanning set, and obviously finite. *} ``` hoelzl@37489 ` 755` hoelzl@37489 ` 756` ```lemma span_stdbasis:"span {cart_basis i :: real^'n | i. i \ (UNIV :: 'n set)} = UNIV" ``` nipkow@39302 ` 757` ```apply (rule set_eqI) ``` hoelzl@37489 ` 758` ```apply auto ``` hoelzl@37489 ` 759` ```apply (subst basis_expansion'[symmetric]) ``` hoelzl@37489 ` 760` ```apply (rule span_setsum) ``` hoelzl@37489 ` 761` ```apply simp ``` hoelzl@37489 ` 762` ```apply auto ``` hoelzl@37489 ` 763` ```apply (rule span_mul) ``` hoelzl@37489 ` 764` ```apply (rule span_superset) ``` huffman@44170 ` 765` ```apply auto ``` hoelzl@37489 ` 766` ```done ``` hoelzl@37489 ` 767` hoelzl@37489 ` 768` ```lemma finite_stdbasis: "finite {cart_basis i ::real^'n |i. i\ (UNIV:: 'n set)}" (is "finite ?S") ``` hoelzl@37489 ` 769` ```proof- ``` hoelzl@37489 ` 770` ``` have eq: "?S = cart_basis ` UNIV" by blast ``` hoelzl@37489 ` 771` ``` show ?thesis unfolding eq by auto ``` hoelzl@37489 ` 772` ```qed ``` hoelzl@37489 ` 773` hoelzl@37489 ` 774` ```lemma card_stdbasis: "card {cart_basis i ::real^'n |i. i\ (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _") ``` hoelzl@37489 ` 775` ```proof- ``` hoelzl@37489 ` 776` ``` have eq: "?S = cart_basis ` UNIV" by blast ``` hoelzl@37489 ` 777` ``` show ?thesis unfolding eq using card_image[OF basis_inj] by simp ``` hoelzl@37489 ` 778` ```qed ``` hoelzl@37489 ` 779` hoelzl@37489 ` 780` hoelzl@37489 ` 781` ```lemma independent_stdbasis_lemma: ``` hoelzl@37489 ` 782` ``` assumes x: "(x::real ^ 'n) \ span (cart_basis ` S)" ``` hoelzl@37489 ` 783` ``` and iS: "i \ S" ``` hoelzl@37489 ` 784` ``` shows "(x\$i) = 0" ``` hoelzl@37489 ` 785` ```proof- ``` hoelzl@37489 ` 786` ``` let ?U = "UNIV :: 'n set" ``` hoelzl@37489 ` 787` ``` let ?B = "cart_basis ` S" ``` huffman@44170 ` 788` ``` let ?P = "{(x::real^_). \i\ ?U. i \ S \ x\$i =0}" ``` hoelzl@37489 ` 789` ``` {fix x::"real^_" assume xS: "x\ ?B" ``` huffman@44170 ` 790` ``` from xS have "x \ ?P" by auto} ``` hoelzl@37489 ` 791` ``` moreover ``` hoelzl@37489 ` 792` ``` have "subspace ?P" ``` huffman@44170 ` 793` ``` by (auto simp add: subspace_def) ``` hoelzl@37489 ` 794` ``` ultimately show ?thesis ``` hoelzl@37489 ` 795` ``` using x span_induct[of ?B ?P x] iS by blast ``` hoelzl@37489 ` 796` ```qed ``` hoelzl@37489 ` 797` hoelzl@37489 ` 798` ```lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\ (UNIV :: 'n set)}" ``` hoelzl@37489 ` 799` ```proof- ``` hoelzl@37489 ` 800` ``` let ?I = "UNIV :: 'n set" ``` hoelzl@37489 ` 801` ``` let ?b = "cart_basis :: _ \ real ^'n" ``` hoelzl@37489 ` 802` ``` let ?B = "?b ` ?I" ``` hoelzl@37489 ` 803` ``` have eq: "{?b i|i. i \ ?I} = ?B" ``` hoelzl@37489 ` 804` ``` by auto ``` hoelzl@37489 ` 805` ``` {assume d: "dependent ?B" ``` hoelzl@37489 ` 806` ``` then obtain k where k: "k \ ?I" "?b k \ span (?B - {?b k})" ``` hoelzl@37489 ` 807` ``` unfolding dependent_def by auto ``` hoelzl@37489 ` 808` ``` have eq1: "?B - {?b k} = ?B - ?b ` {k}" by simp ``` hoelzl@37489 ` 809` ``` have eq2: "?B - {?b k} = ?b ` (?I - {k})" ``` hoelzl@37489 ` 810` ``` unfolding eq1 ``` hoelzl@37489 ` 811` ``` apply (rule inj_on_image_set_diff[symmetric]) ``` hoelzl@37489 ` 812` ``` apply (rule basis_inj) using k(1) by auto ``` hoelzl@37489 ` 813` ``` from k(2) have th0: "?b k \ span (?b ` (?I - {k}))" unfolding eq2 . ``` hoelzl@37489 ` 814` ``` from independent_stdbasis_lemma[OF th0, of k, simplified] ``` hoelzl@37489 ` 815` ``` have False by simp} ``` hoelzl@37489 ` 816` ``` then show ?thesis unfolding eq dependent_def .. ``` hoelzl@37489 ` 817` ```qed ``` hoelzl@37489 ` 818` hoelzl@37489 ` 819` ```lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \ (x - ((b \ x) / (b \ b)) *s b) = 0" ``` hoelzl@37489 ` 820` ``` unfolding inner_simps smult_conv_scaleR by auto ``` hoelzl@37489 ` 821` hoelzl@37489 ` 822` ```lemma linear_eq_stdbasis_cart: ``` hoelzl@37489 ` 823` ``` assumes lf: "linear (f::real^'m \ _)" and lg: "linear g" ``` hoelzl@37489 ` 824` ``` and fg: "\i. f (cart_basis i) = g(cart_basis i)" ``` hoelzl@37489 ` 825` ``` shows "f = g" ``` hoelzl@37489 ` 826` ```proof- ``` hoelzl@37489 ` 827` ``` let ?U = "UNIV :: 'm set" ``` hoelzl@37489 ` 828` ``` let ?I = "{cart_basis i:: real^'m|i. i \ ?U}" ``` hoelzl@37489 ` 829` ``` {fix x assume x: "x \ (UNIV :: (real^'m) set)" ``` hoelzl@37489 ` 830` ``` from equalityD2[OF span_stdbasis] ``` hoelzl@37489 ` 831` ``` have IU: " (UNIV :: (real^'m) set) \ span ?I" by blast ``` hoelzl@37489 ` 832` ``` from linear_eq[OF lf lg IU] fg x ``` huffman@44170 ` 833` ``` have "f x = g x" unfolding Ball_def mem_Collect_eq by metis} ``` hoelzl@37489 ` 834` ``` then show ?thesis by (auto intro: ext) ``` hoelzl@37489 ` 835` ```qed ``` hoelzl@37489 ` 836` hoelzl@37489 ` 837` ```lemma bilinear_eq_stdbasis_cart: ``` hoelzl@37489 ` 838` ``` assumes bf: "bilinear (f:: real^'m \ real^'n \ _)" ``` hoelzl@37489 ` 839` ``` and bg: "bilinear g" ``` hoelzl@37489 ` 840` ``` and fg: "\i j. f (cart_basis i) (cart_basis j) = g (cart_basis i) (cart_basis j)" ``` hoelzl@37489 ` 841` ``` shows "f = g" ``` hoelzl@37489 ` 842` ```proof- ``` hoelzl@37489 ` 843` ``` from fg have th: "\x \ {cart_basis i| i. i\ (UNIV :: 'm set)}. \y\ {cart_basis j |j. j \ (UNIV :: 'n set)}. f x y = g x y" by blast ``` hoelzl@37489 ` 844` ``` from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by (blast intro: ext) ``` hoelzl@37489 ` 845` ```qed ``` hoelzl@37489 ` 846` hoelzl@37489 ` 847` ```lemma left_invertible_transpose: ``` hoelzl@37489 ` 848` ``` "(\(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" ``` hoelzl@37489 ` 849` ``` by (metis matrix_transpose_mul transpose_mat transpose_transpose) ``` hoelzl@37489 ` 850` hoelzl@37489 ` 851` ```lemma right_invertible_transpose: ``` hoelzl@37489 ` 852` ``` "(\(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(B). B ** A = mat 1)" ``` hoelzl@37489 ` 853` ``` by (metis matrix_transpose_mul transpose_mat transpose_transpose) ``` hoelzl@37489 ` 854` hoelzl@37489 ` 855` ```lemma matrix_left_invertible_injective: ``` hoelzl@37489 ` 856` ```"(\B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x y. A *v x = A *v y \ x = y)" ``` hoelzl@37489 ` 857` ```proof- ``` hoelzl@37489 ` 858` ``` {fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y" ``` hoelzl@37489 ` 859` ``` from xy have "B*v (A *v x) = B *v (A*v y)" by simp ``` hoelzl@37489 ` 860` ``` hence "x = y" ``` hoelzl@37489 ` 861` ``` unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid .} ``` hoelzl@37489 ` 862` ``` moreover ``` hoelzl@37489 ` 863` ``` {assume A: "\x y. A *v x = A *v y \ x = y" ``` hoelzl@37489 ` 864` ``` hence i: "inj (op *v A)" unfolding inj_on_def by auto ``` hoelzl@37489 ` 865` ``` from linear_injective_left_inverse[OF matrix_vector_mul_linear i] ``` hoelzl@37489 ` 866` ``` obtain g where g: "linear g" "g o op *v A = id" by blast ``` hoelzl@37489 ` 867` ``` have "matrix g ** A = mat 1" ``` hoelzl@37489 ` 868` ``` unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] ``` huffman@44165 ` 869` ``` using g(2) by (simp add: fun_eq_iff) ``` hoelzl@37489 ` 870` ``` then have "\B. (B::real ^'m^'n) ** A = mat 1" by blast} ``` hoelzl@37489 ` 871` ``` ultimately show ?thesis by blast ``` hoelzl@37489 ` 872` ```qed ``` hoelzl@37489 ` 873` hoelzl@37489 ` 874` ```lemma matrix_left_invertible_ker: ``` hoelzl@37489 ` 875` ``` "(\B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x. A *v x = 0 \ x = 0)" ``` hoelzl@37489 ` 876` ``` unfolding matrix_left_invertible_injective ``` hoelzl@37489 ` 877` ``` using linear_injective_0[OF matrix_vector_mul_linear, of A] ``` hoelzl@37489 ` 878` ``` by (simp add: inj_on_def) ``` hoelzl@37489 ` 879` hoelzl@37489 ` 880` ```lemma matrix_right_invertible_surjective: ``` hoelzl@37489 ` 881` ```"(\B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \ surj (\x. A *v x)" ``` hoelzl@37489 ` 882` ```proof- ``` hoelzl@37489 ` 883` ``` {fix B :: "real ^'m^'n" assume AB: "A ** B = mat 1" ``` hoelzl@37489 ` 884` ``` {fix x :: "real ^ 'm" ``` hoelzl@37489 ` 885` ``` have "A *v (B *v x) = x" ``` hoelzl@37489 ` 886` ``` by (simp add: matrix_vector_mul_lid matrix_vector_mul_assoc AB)} ``` hoelzl@37489 ` 887` ``` hence "surj (op *v A)" unfolding surj_def by metis } ``` hoelzl@37489 ` 888` ``` moreover ``` hoelzl@37489 ` 889` ``` {assume sf: "surj (op *v A)" ``` hoelzl@37489 ` 890` ``` from linear_surjective_right_inverse[OF matrix_vector_mul_linear sf] ``` hoelzl@37489 ` 891` ``` obtain g:: "real ^'m \ real ^'n" where g: "linear g" "op *v A o g = id" ``` hoelzl@37489 ` 892` ``` by blast ``` hoelzl@37489 ` 893` hoelzl@37489 ` 894` ``` have "A ** (matrix g) = mat 1" ``` hoelzl@37489 ` 895` ``` unfolding matrix_eq matrix_vector_mul_lid ``` hoelzl@37489 ` 896` ``` matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] ``` huffman@44165 ` 897` ``` using g(2) unfolding o_def fun_eq_iff id_def ``` hoelzl@37489 ` 898` ``` . ``` hoelzl@37489 ` 899` ``` hence "\B. A ** (B::real^'m^'n) = mat 1" by blast ``` hoelzl@37489 ` 900` ``` } ``` hoelzl@37489 ` 901` ``` ultimately show ?thesis unfolding surj_def by blast ``` hoelzl@37489 ` 902` ```qed ``` hoelzl@37489 ` 903` hoelzl@37489 ` 904` ```lemma matrix_left_invertible_independent_columns: ``` hoelzl@37489 ` 905` ``` fixes A :: "real^'n^'m" ``` hoelzl@37489 ` 906` ``` shows "(\(B::real ^'m^'n). B ** A = mat 1) \ (\c. setsum (\i. c i *s column i A) (UNIV :: 'n set) = 0 \ (\i. c i = 0))" ``` hoelzl@37489 ` 907` ``` (is "?lhs \ ?rhs") ``` hoelzl@37489 ` 908` ```proof- ``` hoelzl@37489 ` 909` ``` let ?U = "UNIV :: 'n set" ``` hoelzl@37489 ` 910` ``` {assume k: "\x. A *v x = 0 \ x = 0" ``` hoelzl@37489 ` 911` ``` {fix c i assume c: "setsum (\i. c i *s column i A) ?U = 0" ``` hoelzl@37489 ` 912` ``` and i: "i \ ?U" ``` hoelzl@37489 ` 913` ``` let ?x = "\ i. c i" ``` hoelzl@37489 ` 914` ``` have th0:"A *v ?x = 0" ``` hoelzl@37489 ` 915` ``` using c ``` huffman@44136 ` 916` ``` unfolding matrix_mult_vsum vec_eq_iff ``` hoelzl@37489 ` 917` ``` by auto ``` hoelzl@37489 ` 918` ``` from k[rule_format, OF th0] i ``` huffman@44136 ` 919` ``` have "c i = 0" by (vector vec_eq_iff)} ``` hoelzl@37489 ` 920` ``` hence ?rhs by blast} ``` hoelzl@37489 ` 921` ``` moreover ``` hoelzl@37489 ` 922` ``` {assume H: ?rhs ``` hoelzl@37489 ` 923` ``` {fix x assume x: "A *v x = 0" ``` hoelzl@37489 ` 924` ``` let ?c = "\i. ((x\$i ):: real)" ``` hoelzl@37489 ` 925` ``` from H[rule_format, of ?c, unfolded matrix_mult_vsum[symmetric], OF x] ``` hoelzl@37489 ` 926` ``` have "x = 0" by vector}} ``` hoelzl@37489 ` 927` ``` ultimately show ?thesis unfolding matrix_left_invertible_ker by blast ``` hoelzl@37489 ` 928` ```qed ``` hoelzl@37489 ` 929` hoelzl@37489 ` 930` ```lemma matrix_right_invertible_independent_rows: ``` hoelzl@37489 ` 931` ``` fixes A :: "real^'n^'m" ``` hoelzl@37489 ` 932` ``` shows "(\(B::real^'m^'n). A ** B = mat 1) \ (\c. setsum (\i. c i *s row i A) (UNIV :: 'm set) = 0 \ (\i. c i = 0))" ``` hoelzl@37489 ` 933` ``` unfolding left_invertible_transpose[symmetric] ``` hoelzl@37489 ` 934` ``` matrix_left_invertible_independent_columns ``` hoelzl@37489 ` 935` ``` by (simp add: column_transpose) ``` hoelzl@37489 ` 936` hoelzl@37489 ` 937` ```lemma matrix_right_invertible_span_columns: ``` hoelzl@37489 ` 938` ``` "(\(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \ span (columns A) = UNIV" (is "?lhs = ?rhs") ``` hoelzl@37489 ` 939` ```proof- ``` hoelzl@37489 ` 940` ``` let ?U = "UNIV :: 'm set" ``` hoelzl@37489 ` 941` ``` have fU: "finite ?U" by simp ``` hoelzl@37489 ` 942` ``` have lhseq: "?lhs \ (\y. \(x::real^'m). setsum (\i. (x\$i) *s column i A) ?U = y)" ``` hoelzl@37489 ` 943` ``` unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def ``` hoelzl@37489 ` 944` ``` apply (subst eq_commute) .. ``` hoelzl@37489 ` 945` ``` have rhseq: "?rhs \ (\x. x \ span (columns A))" by blast ``` hoelzl@37489 ` 946` ``` {assume h: ?lhs ``` hoelzl@37489 ` 947` ``` {fix x:: "real ^'n" ``` hoelzl@37489 ` 948` ``` from h[unfolded lhseq, rule_format, of x] obtain y:: "real ^'m" ``` hoelzl@37489 ` 949` ``` where y: "setsum (\i. (y\$i) *s column i A) ?U = x" by blast ``` hoelzl@37489 ` 950` ``` have "x \ span (columns A)" ``` hoelzl@37489 ` 951` ``` unfolding y[symmetric] ``` hoelzl@37489 ` 952` ``` apply (rule span_setsum[OF fU]) ``` hoelzl@37489 ` 953` ``` apply clarify ``` hoelzl@37489 ` 954` ``` unfolding smult_conv_scaleR ``` hoelzl@37489 ` 955` ``` apply (rule span_mul) ``` hoelzl@37489 ` 956` ``` apply (rule span_superset) ``` hoelzl@37489 ` 957` ``` unfolding columns_def ``` hoelzl@37489 ` 958` ``` by blast} ``` hoelzl@37489 ` 959` ``` then have ?rhs unfolding rhseq by blast} ``` hoelzl@37489 ` 960` ``` moreover ``` hoelzl@37489 ` 961` ``` {assume h:?rhs ``` hoelzl@37489 ` 962` ``` let ?P = "\(y::real ^'n). \(x::real^'m). setsum (\i. (x\$i) *s column i A) ?U = y" ``` hoelzl@37489 ` 963` ``` {fix y have "?P y" ``` hoelzl@37489 ` 964` ``` proof(rule span_induct_alt[of ?P "columns A", folded smult_conv_scaleR]) ``` hoelzl@37489 ` 965` ``` show "\x\real ^ 'm. setsum (\i. (x\$i) *s column i A) ?U = 0" ``` hoelzl@37489 ` 966` ``` by (rule exI[where x=0], simp) ``` hoelzl@37489 ` 967` ``` next ``` hoelzl@37489 ` 968` ``` fix c y1 y2 assume y1: "y1 \ columns A" and y2: "?P y2" ``` hoelzl@37489 ` 969` ``` from y1 obtain i where i: "i \ ?U" "y1 = column i A" ``` hoelzl@37489 ` 970` ``` unfolding columns_def by blast ``` hoelzl@37489 ` 971` ``` from y2 obtain x:: "real ^'m" where ``` hoelzl@37489 ` 972` ``` x: "setsum (\i. (x\$i) *s column i A) ?U = y2" by blast ``` hoelzl@37489 ` 973` ``` let ?x = "(\ j. if j = i then c + (x\$i) else (x\$j))::real^'m" ``` hoelzl@37489 ` 974` ``` show "?P (c*s y1 + y2)" ``` hoelzl@37489 ` 975` ``` proof(rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib right_distrib cond_application_beta cong del: if_weak_cong) ``` hoelzl@37489 ` 976` ``` fix j ``` hoelzl@37489 ` 977` ``` have th: "\xa \ ?U. (if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` hoelzl@37489 ` 978` ``` else (x\$xa) * ((column xa A\$j))) = (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))" using i(1) ``` hoelzl@37489 ` 979` ``` by (simp add: field_simps) ``` hoelzl@37489 ` 980` ``` have "setsum (\xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` hoelzl@37489 ` 981` ``` else (x\$xa) * ((column xa A\$j))) ?U = setsum (\xa. (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))) ?U" ``` hoelzl@37489 ` 982` ``` apply (rule setsum_cong[OF refl]) ``` hoelzl@37489 ` 983` ``` using th by blast ``` hoelzl@37489 ` 984` ``` also have "\ = setsum (\xa. if xa = i then c * ((column i A)\$j) else 0) ?U + setsum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" ``` hoelzl@37489 ` 985` ``` by (simp add: setsum_addf) ``` hoelzl@37489 ` 986` ``` also have "\ = c * ((column i A)\$j) + setsum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" ``` hoelzl@37489 ` 987` ``` unfolding setsum_delta[OF fU] ``` hoelzl@37489 ` 988` ``` using i(1) by simp ``` hoelzl@37489 ` 989` ``` finally show "setsum (\xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` hoelzl@37489 ` 990` ``` else (x\$xa) * ((column xa A\$j))) ?U = c * ((column i A)\$j) + setsum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" . ``` hoelzl@37489 ` 991` ``` qed ``` hoelzl@37489 ` 992` ``` next ``` hoelzl@37489 ` 993` ``` show "y \ span (columns A)" unfolding h by blast ``` hoelzl@37489 ` 994` ``` qed} ``` hoelzl@37489 ` 995` ``` then have ?lhs unfolding lhseq ..} ``` hoelzl@37489 ` 996` ``` ultimately show ?thesis by blast ``` hoelzl@37489 ` 997` ```qed ``` hoelzl@37489 ` 998` hoelzl@37489 ` 999` ```lemma matrix_left_invertible_span_rows: ``` hoelzl@37489 ` 1000` ``` "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" ``` hoelzl@37489 ` 1001` ``` unfolding right_invertible_transpose[symmetric] ``` hoelzl@37489 ` 1002` ``` unfolding columns_transpose[symmetric] ``` hoelzl@37489 ` 1003` ``` unfolding matrix_right_invertible_span_columns ``` hoelzl@37489 ` 1004` ``` .. ``` hoelzl@37489 ` 1005` hoelzl@37489 ` 1006` ```text {* The same result in terms of square matrices. *} ``` hoelzl@37489 ` 1007` hoelzl@37489 ` 1008` ```lemma matrix_left_right_inverse: ``` hoelzl@37489 ` 1009` ``` fixes A A' :: "real ^'n^'n" ``` hoelzl@37489 ` 1010` ``` shows "A ** A' = mat 1 \ A' ** A = mat 1" ``` hoelzl@37489 ` 1011` ```proof- ``` hoelzl@37489 ` 1012` ``` {fix A A' :: "real ^'n^'n" assume AA': "A ** A' = mat 1" ``` hoelzl@37489 ` 1013` ``` have sA: "surj (op *v A)" ``` hoelzl@37489 ` 1014` ``` unfolding surj_def ``` hoelzl@37489 ` 1015` ``` apply clarify ``` hoelzl@37489 ` 1016` ``` apply (rule_tac x="(A' *v y)" in exI) ``` hoelzl@37489 ` 1017` ``` by (simp add: matrix_vector_mul_assoc AA' matrix_vector_mul_lid) ``` hoelzl@37489 ` 1018` ``` from linear_surjective_isomorphism[OF matrix_vector_mul_linear sA] ``` hoelzl@37489 ` 1019` ``` obtain f' :: "real ^'n \ real ^'n" ``` hoelzl@37489 ` 1020` ``` where f': "linear f'" "\x. f' (A *v x) = x" "\x. A *v f' x = x" by blast ``` hoelzl@37489 ` 1021` ``` have th: "matrix f' ** A = mat 1" ``` hoelzl@37489 ` 1022` ``` by (simp add: matrix_eq matrix_works[OF f'(1)] matrix_vector_mul_assoc[symmetric] matrix_vector_mul_lid f'(2)[rule_format]) ``` hoelzl@37489 ` 1023` ``` hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp ``` hoelzl@37489 ` 1024` ``` hence "matrix f' = A'" by (simp add: matrix_mul_assoc[symmetric] AA' matrix_mul_rid matrix_mul_lid) ``` hoelzl@37489 ` 1025` ``` hence "matrix f' ** A = A' ** A" by simp ``` hoelzl@37489 ` 1026` ``` hence "A' ** A = mat 1" by (simp add: th)} ``` hoelzl@37489 ` 1027` ``` then show ?thesis by blast ``` hoelzl@37489 ` 1028` ```qed ``` hoelzl@37489 ` 1029` hoelzl@37489 ` 1030` ```text {* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *} ``` hoelzl@37489 ` 1031` hoelzl@37489 ` 1032` ```definition "rowvector v = (\ i j. (v\$j))" ``` hoelzl@37489 ` 1033` hoelzl@37489 ` 1034` ```definition "columnvector v = (\ i j. (v\$i))" ``` hoelzl@37489 ` 1035` hoelzl@37489 ` 1036` ```lemma transpose_columnvector: ``` hoelzl@37489 ` 1037` ``` "transpose(columnvector v) = rowvector v" ``` huffman@44136 ` 1038` ``` by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff) ``` hoelzl@37489 ` 1039` hoelzl@37489 ` 1040` ```lemma transpose_rowvector: "transpose(rowvector v) = columnvector v" ``` huffman@44136 ` 1041` ``` by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff) ``` hoelzl@37489 ` 1042` hoelzl@37489 ` 1043` ```lemma dot_rowvector_columnvector: ``` hoelzl@37489 ` 1044` ``` "columnvector (A *v v) = A ** columnvector v" ``` hoelzl@37489 ` 1045` ``` by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) ``` hoelzl@37489 ` 1046` hoelzl@37489 ` 1047` ```lemma dot_matrix_product: "(x::real^'n) \ y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))\$1)\$1" ``` huffman@44136 ` 1048` ``` by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def) ``` hoelzl@37489 ` 1049` hoelzl@37489 ` 1050` ```lemma dot_matrix_vector_mul: ``` hoelzl@37489 ` 1051` ``` fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" ``` hoelzl@37489 ` 1052` ``` shows "(A *v x) \ (B *v y) = ``` hoelzl@37489 ` 1053` ``` (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))\$1)\$1" ``` hoelzl@37489 ` 1054` ```unfolding dot_matrix_product transpose_columnvector[symmetric] ``` hoelzl@37489 ` 1055` ``` dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc .. ``` hoelzl@37489 ` 1056` hoelzl@37489 ` 1057` hoelzl@37489 ` 1058` ```lemma infnorm_cart:"infnorm (x::real^'n) = Sup {abs(x\$i) |i. i\ (UNIV :: 'n set)}" ``` hoelzl@37489 ` 1059` ``` unfolding infnorm_def apply(rule arg_cong[where f=Sup]) apply safe ``` hoelzl@37489 ` 1060` ``` apply(rule_tac x="\ i" in exI) defer ``` hoelzl@37489 ` 1061` ``` apply(rule_tac x="\' i" in exI) unfolding nth_conv_component using pi'_range by auto ``` hoelzl@37489 ` 1062` hoelzl@37489 ` 1063` ```lemma infnorm_set_image_cart: ``` hoelzl@37489 ` 1064` ``` "{abs(x\$i) |i. i\ (UNIV :: _ set)} = ``` hoelzl@37489 ` 1065` ``` (\i. abs(x\$i)) ` (UNIV)" by blast ``` hoelzl@37489 ` 1066` hoelzl@37489 ` 1067` ```lemma infnorm_set_lemma_cart: ``` hoelzl@37489 ` 1068` ``` shows "finite {abs((x::'a::abs ^'n)\$i) |i. i\ (UNIV :: 'n set)}" ``` hoelzl@37489 ` 1069` ``` and "{abs(x\$i) |i. i\ (UNIV :: 'n::finite set)} \ {}" ``` hoelzl@37489 ` 1070` ``` unfolding infnorm_set_image_cart ``` nipkow@40786 ` 1071` ``` by auto ``` hoelzl@37489 ` 1072` hoelzl@37489 ` 1073` ```lemma component_le_infnorm_cart: ``` hoelzl@37489 ` 1074` ``` shows "\x\$i\ \ infnorm (x::real^'n)" ``` hoelzl@37489 ` 1075` ``` unfolding nth_conv_component ``` hoelzl@37489 ` 1076` ``` using component_le_infnorm[of x] . ``` hoelzl@37489 ` 1077` huffman@44136 ` 1078` ```instance vec :: (perfect_space, finite) perfect_space ``` hoelzl@37489 ` 1079` ```proof ``` hoelzl@37489 ` 1080` ``` fix x :: "'a ^ 'b" ``` huffman@44077 ` 1081` ``` show "x islimpt UNIV" ``` huffman@44077 ` 1082` ``` apply (rule islimptI) ``` huffman@44136 ` 1083` ``` apply (unfold open_vec_def) ``` huffman@44077 ` 1084` ``` apply (drule (1) bspec) ``` huffman@44077 ` 1085` ``` apply clarsimp ``` huffman@44077 ` 1086` ``` apply (subgoal_tac "\i\UNIV. \y. y \ A i \ y \ x \$ i") ``` huffman@44077 ` 1087` ``` apply (drule finite_choice [OF finite_UNIV], erule exE) ``` huffman@44136 ` 1088` ``` apply (rule_tac x="vec_lambda f" in exI) ``` huffman@44136 ` 1089` ``` apply (simp add: vec_eq_iff) ``` huffman@44077 ` 1090` ``` apply (rule ballI, drule_tac x=i in spec, clarify) ``` huffman@44077 ` 1091` ``` apply (cut_tac x="x \$ i" in islimpt_UNIV) ``` huffman@44077 ` 1092` ``` apply (simp add: islimpt_def) ``` huffman@44077 ` 1093` ``` done ``` hoelzl@37489 ` 1094` ```qed ``` hoelzl@37489 ` 1095` huffman@44213 ` 1096` ```lemma continuous_at_component: "continuous (at a) (\x. x \$ i)" ``` huffman@44213 ` 1097` ```unfolding continuous_at by (intro tendsto_intros) ``` huffman@44213 ` 1098` huffman@44213 ` 1099` ```lemma continuous_on_component: "continuous_on s (\x. x \$ i)" ``` huffman@44213 ` 1100` ```unfolding continuous_on_def by (intro ballI tendsto_intros) ``` huffman@44213 ` 1101` hoelzl@37489 ` 1102` ```lemma closed_positive_orthant: "closed {x::real^'n. \i. 0 \x\$i}" ``` huffman@44233 ` 1103` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le) ``` huffman@44213 ` 1104` hoelzl@37489 ` 1105` ```lemma Lim_component_cart: ``` hoelzl@37489 ` 1106` ``` fixes f :: "'a \ 'b::metric_space ^ 'n" ``` hoelzl@37489 ` 1107` ``` shows "(f ---> l) net \ ((\a. f a \$i) ---> l\$i) net" ``` huffman@44213 ` 1108` ``` by (intro tendsto_intros) ``` hoelzl@37489 ` 1109` hoelzl@37489 ` 1110` ```lemma bounded_component_cart: "bounded s \ bounded ((\x. x \$ i) ` s)" ``` hoelzl@37489 ` 1111` ```unfolding bounded_def ``` hoelzl@37489 ` 1112` ```apply clarify ``` hoelzl@37489 ` 1113` ```apply (rule_tac x="x \$ i" in exI) ``` hoelzl@37489 ` 1114` ```apply (rule_tac x="e" in exI) ``` hoelzl@37489 ` 1115` ```apply clarify ``` huffman@44136 ` 1116` ```apply (rule order_trans [OF dist_vec_nth_le], simp) ``` hoelzl@37489 ` 1117` ```done ``` hoelzl@37489 ` 1118` hoelzl@37489 ` 1119` ```lemma compact_lemma_cart: ``` hoelzl@37489 ` 1120` ``` fixes f :: "nat \ 'a::heine_borel ^ 'n" ``` hoelzl@37489 ` 1121` ``` assumes "bounded s" and "\n. f n \ s" ``` hoelzl@37489 ` 1122` ``` shows "\d. ``` hoelzl@37489 ` 1123` ``` \l r. subseq r \ ``` hoelzl@37489 ` 1124` ``` (\e>0. eventually (\n. \i\d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)" ``` hoelzl@37489 ` 1125` ```proof ``` hoelzl@37489 ` 1126` ``` fix d::"'n set" have "finite d" by simp ``` hoelzl@37489 ` 1127` ``` thus "\l::'a ^ 'n. \r. subseq r \ ``` hoelzl@37489 ` 1128` ``` (\e>0. eventually (\n. \i\d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)" ``` hoelzl@37489 ` 1129` ``` proof(induct d) case empty thus ?case unfolding subseq_def by auto ``` hoelzl@37489 ` 1130` ``` next case (insert k d) ``` hoelzl@37489 ` 1131` ``` have s': "bounded ((\x. x \$ k) ` s)" using `bounded s` by (rule bounded_component_cart) ``` hoelzl@37489 ` 1132` ``` obtain l1::"'a^'n" and r1 where r1:"subseq r1" and lr1:"\e>0. eventually (\n. \i\d. dist (f (r1 n) \$ i) (l1 \$ i) < e) sequentially" ``` hoelzl@37489 ` 1133` ``` using insert(3) by auto ``` hoelzl@37489 ` 1134` ``` have f': "\n. f (r1 n) \$ k \ (\x. x \$ k) ` s" using `\n. f n \ s` by simp ``` hoelzl@37489 ` 1135` ``` obtain l2 r2 where r2:"subseq r2" and lr2:"((\i. f (r1 (r2 i)) \$ k) ---> l2) sequentially" ``` hoelzl@37489 ` 1136` ``` using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto ``` hoelzl@37489 ` 1137` ``` def r \ "r1 \ r2" have r:"subseq r" ``` hoelzl@37489 ` 1138` ``` using r1 and r2 unfolding r_def o_def subseq_def by auto ``` hoelzl@37489 ` 1139` ``` moreover ``` hoelzl@37489 ` 1140` ``` def l \ "(\ i. if i = k then l2 else l1\$i)::'a^'n" ``` hoelzl@37489 ` 1141` ``` { fix e::real assume "e>0" ``` hoelzl@37489 ` 1142` ``` from lr1 `e>0` have N1:"eventually (\n. \i\d. dist (f (r1 n) \$ i) (l1 \$ i) < e) sequentially" by blast ``` hoelzl@37489 ` 1143` ``` from lr2 `e>0` have N2:"eventually (\n. dist (f (r1 (r2 n)) \$ k) l2 < e) sequentially" by (rule tendstoD) ``` hoelzl@37489 ` 1144` ``` from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) \$ i) (l1 \$ i) < e) sequentially" ``` hoelzl@37489 ` 1145` ``` by (rule eventually_subseq) ``` hoelzl@37489 ` 1146` ``` have "eventually (\n. \i\(insert k d). dist (f (r n) \$ i) (l \$ i) < e) sequentially" ``` hoelzl@37489 ` 1147` ``` using N1' N2 by (rule eventually_elim2, simp add: l_def r_def) ``` hoelzl@37489 ` 1148` ``` } ``` hoelzl@37489 ` 1149` ``` ultimately show ?case by auto ``` hoelzl@37489 ` 1150` ``` qed ``` hoelzl@37489 ` 1151` ```qed ``` hoelzl@37489 ` 1152` huffman@44136 ` 1153` ```instance vec :: (heine_borel, finite) heine_borel ``` hoelzl@37489 ` 1154` ```proof ``` hoelzl@37489 ` 1155` ``` fix s :: "('a ^ 'b) set" and f :: "nat \ 'a ^ 'b" ``` hoelzl@37489 ` 1156` ``` assume s: "bounded s" and f: "\n. f n \ s" ``` hoelzl@37489 ` 1157` ``` then obtain l r where r: "subseq r" ``` hoelzl@37489 ` 1158` ``` and l: "\e>0. eventually (\n. \i\UNIV. dist (f (r n) \$ i) (l \$ i) < e) sequentially" ``` hoelzl@37489 ` 1159` ``` using compact_lemma_cart [OF s f] by blast ``` hoelzl@37489 ` 1160` ``` let ?d = "UNIV::'b set" ``` hoelzl@37489 ` 1161` ``` { fix e::real assume "e>0" ``` hoelzl@37489 ` 1162` ``` hence "0 < e / (real_of_nat (card ?d))" ``` hoelzl@37489 ` 1163` ``` using zero_less_card_finite using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto ``` hoelzl@37489 ` 1164` ``` with l have "eventually (\n. \i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))) sequentially" ``` hoelzl@37489 ` 1165` ``` by simp ``` hoelzl@37489 ` 1166` ``` moreover ``` hoelzl@37489 ` 1167` ``` { fix n assume n: "\i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))" ``` hoelzl@37489 ` 1168` ``` have "dist (f (r n)) l \ (\i\?d. dist (f (r n) \$ i) (l \$ i))" ``` huffman@44136 ` 1169` ``` unfolding dist_vec_def using zero_le_dist by (rule setL2_le_setsum) ``` hoelzl@37489 ` 1170` ``` also have "\ < (\i\?d. e / (real_of_nat (card ?d)))" ``` hoelzl@37489 ` 1171` ``` by (rule setsum_strict_mono) (simp_all add: n) ``` hoelzl@37489 ` 1172` ``` finally have "dist (f (r n)) l < e" by simp ``` hoelzl@37489 ` 1173` ``` } ``` hoelzl@37489 ` 1174` ``` ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" ``` hoelzl@37489 ` 1175` ``` by (rule eventually_elim1) ``` hoelzl@37489 ` 1176` ``` } ``` hoelzl@37489 ` 1177` ``` hence *:"((f \ r) ---> l) sequentially" unfolding o_def tendsto_iff by simp ``` hoelzl@37489 ` 1178` ``` with r show "\l r. subseq r \ ((f \ r) ---> l) sequentially" by auto ``` hoelzl@37489 ` 1179` ```qed ``` hoelzl@37489 ` 1180` hoelzl@37489 ` 1181` ```lemma interval_cart: fixes a :: "'a::ord^'n" shows ``` hoelzl@37489 ` 1182` ``` "{a <..< b} = {x::'a^'n. \i. a\$i < x\$i \ x\$i < b\$i}" and ``` hoelzl@37489 ` 1183` ``` "{a .. b} = {x::'a^'n. \i. a\$i \ x\$i \ x\$i \ b\$i}" ``` huffman@44136 ` 1184` ``` by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def) ``` hoelzl@37489 ` 1185` hoelzl@37489 ` 1186` ```lemma mem_interval_cart: fixes a :: "'a::ord^'n" shows ``` hoelzl@37489 ` 1187` ``` "x \ {a<.. (\i. a\$i < x\$i \ x\$i < b\$i)" ``` hoelzl@37489 ` 1188` ``` "x \ {a .. b} \ (\i. a\$i \ x\$i \ x\$i \ b\$i)" ``` huffman@44136 ` 1189` ``` using interval_cart[of a b] by(auto simp add: set_eq_iff less_vec_def less_eq_vec_def) ``` hoelzl@37489 ` 1190` hoelzl@37489 ` 1191` ```lemma interval_eq_empty_cart: fixes a :: "real^'n" shows ``` hoelzl@37489 ` 1192` ``` "({a <..< b} = {} \ (\i. b\$i \ a\$i))" (is ?th1) and ``` hoelzl@37489 ` 1193` ``` "({a .. b} = {} \ (\i. b\$i < a\$i))" (is ?th2) ``` hoelzl@37489 ` 1194` ```proof- ``` hoelzl@37489 ` 1195` ``` { fix i x assume as:"b\$i \ a\$i" and x:"x\{a <..< b}" ``` hoelzl@37489 ` 1196` ``` hence "a \$ i < x \$ i \ x \$ i < b \$ i" unfolding mem_interval_cart by auto ``` hoelzl@37489 ` 1197` ``` hence "a\$i < b\$i" by auto ``` hoelzl@37489 ` 1198` ``` hence False using as by auto } ``` hoelzl@37489 ` 1199` ``` moreover ``` hoelzl@37489 ` 1200` ``` { assume as:"\i. \ (b\$i \ a\$i)" ``` hoelzl@37489 ` 1201` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` hoelzl@37489 ` 1202` ``` { fix i ``` hoelzl@37489 ` 1203` ``` have "a\$i < b\$i" using as[THEN spec[where x=i]] by auto ``` hoelzl@37489 ` 1204` ``` hence "a\$i < ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i < b\$i" ``` hoelzl@37489 ` 1205` ``` unfolding vector_smult_component and vector_add_component ``` hoelzl@37489 ` 1206` ``` by auto } ``` hoelzl@37489 ` 1207` ``` hence "{a <..< b} \ {}" using mem_interval_cart(1)[of "?x" a b] by auto } ``` hoelzl@37489 ` 1208` ``` ultimately show ?th1 by blast ``` hoelzl@37489 ` 1209` hoelzl@37489 ` 1210` ``` { fix i x assume as:"b\$i < a\$i" and x:"x\{a .. b}" ``` hoelzl@37489 ` 1211` ``` hence "a \$ i \ x \$ i \ x \$ i \ b \$ i" unfolding mem_interval_cart by auto ``` hoelzl@37489 ` 1212` ``` hence "a\$i \ b\$i" by auto ``` hoelzl@37489 ` 1213` ``` hence False using as by auto } ``` hoelzl@37489 ` 1214` ``` moreover ``` hoelzl@37489 ` 1215` ``` { assume as:"\i. \ (b\$i < a\$i)" ``` hoelzl@37489 ` 1216` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` hoelzl@37489 ` 1217` ``` { fix i ``` hoelzl@37489 ` 1218` ``` have "a\$i \ b\$i" using as[THEN spec[where x=i]] by auto ``` hoelzl@37489 ` 1219` ``` hence "a\$i \ ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i \ b\$i" ``` hoelzl@37489 ` 1220` ``` unfolding vector_smult_component and vector_add_component ``` hoelzl@37489 ` 1221` ``` by auto } ``` hoelzl@37489 ` 1222` ``` hence "{a .. b} \ {}" using mem_interval_cart(2)[of "?x" a b] by auto } ``` hoelzl@37489 ` 1223` ``` ultimately show ?th2 by blast ``` hoelzl@37489 ` 1224` ```qed ``` hoelzl@37489 ` 1225` hoelzl@37489 ` 1226` ```lemma interval_ne_empty_cart: fixes a :: "real^'n" shows ``` hoelzl@37489 ` 1227` ``` "{a .. b} \ {} \ (\i. a\$i \ b\$i)" and ``` hoelzl@37489 ` 1228` ``` "{a <..< b} \ {} \ (\i. a\$i < b\$i)" ``` hoelzl@37489 ` 1229` ``` unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le) ``` hoelzl@37489 ` 1230` ``` (* BH: Why doesn't just "auto" work here? *) ``` hoelzl@37489 ` 1231` hoelzl@37489 ` 1232` ```lemma subset_interval_imp_cart: fixes a :: "real^'n" shows ``` hoelzl@37489 ` 1233` ``` "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ {c .. d} \ {a .. b}" and ``` hoelzl@37489 ` 1234` ``` "(\i. a\$i < c\$i \ d\$i < b\$i) \ {c .. d} \ {a<..i. a\$i \ c\$i \ d\$i \ b\$i) \ {c<.. {a .. b}" and ``` hoelzl@37489 ` 1236` ``` "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ {c<.. {a<.. {a<.. {a .. b}" ``` hoelzl@37489 ` 1249` ```proof(simp add: subset_eq, rule) ``` hoelzl@37489 ` 1250` ``` fix x ``` hoelzl@37489 ` 1251` ``` assume x:"x \{a<.. x \$ i" ``` hoelzl@37489 ` 1254` ``` using x order_less_imp_le[of "a\$i" "x\$i"] ``` huffman@44136 ` 1255` ``` by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) ``` hoelzl@37489 ` 1256` ``` } ``` hoelzl@37489 ` 1257` ``` moreover ``` hoelzl@37489 ` 1258` ``` { fix i ``` hoelzl@37489 ` 1259` ``` have "x \$ i \ b \$ i" ``` hoelzl@37489 ` 1260` ``` using x order_less_imp_le[of "x\$i" "b\$i"] ``` huffman@44136 ` 1261` ``` by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) ``` hoelzl@37489 ` 1262` ``` } ``` hoelzl@37489 ` 1263` ``` ultimately ``` hoelzl@37489 ` 1264` ``` show "a \ x \ x \ b" ``` huffman@44136 ` 1265` ``` by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) ``` hoelzl@37489 ` 1266` ```qed ``` hoelzl@37489 ` 1267` hoelzl@37489 ` 1268` ```lemma subset_interval_cart: fixes a :: "real^'n" shows ``` hoelzl@37489 ` 1269` ``` "{c .. d} \ {a .. b} \ (\i. c\$i \ d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th1) and ``` hoelzl@37489 ` 1270` ``` "{c .. d} \ {a<.. (\i. c\$i \ d\$i) --> (\i. a\$i < c\$i \ d\$i < b\$i)" (is ?th2) and ``` hoelzl@37489 ` 1271` ``` "{c<.. {a .. b} \ (\i. c\$i < d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th3) and ``` hoelzl@37489 ` 1272` ``` "{c<.. {a<.. (\i. c\$i < d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th4) ``` hoelzl@37489 ` 1273` ``` using subset_interval[of c d a b] by (simp_all add: cart_simps real_euclidean_nth) ``` hoelzl@37489 ` 1274` hoelzl@37489 ` 1275` ```lemma disjoint_interval_cart: fixes a::"real^'n" shows ``` hoelzl@37489 ` 1276` ``` "{a .. b} \ {c .. d} = {} \ (\i. (b\$i < a\$i \ d\$i < c\$i \ b\$i < c\$i \ d\$i < a\$i))" (is ?th1) and ``` hoelzl@37489 ` 1277` ``` "{a .. b} \ {c<.. (\i. (b\$i < a\$i \ d\$i \ c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th2) and ``` hoelzl@37489 ` 1278` ``` "{a<.. {c .. d} = {} \ (\i. (b\$i \ a\$i \ d\$i < c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th3) and ``` hoelzl@37489 ` 1279` ``` "{a<.. {c<.. (\i. (b\$i \ a\$i \ d\$i \ c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th4) ``` hoelzl@37489 ` 1280` ``` using disjoint_interval[of a b c d] by (simp_all add: cart_simps real_euclidean_nth) ``` hoelzl@37489 ` 1281` hoelzl@37489 ` 1282` ```lemma inter_interval_cart: fixes a :: "'a::linorder^'n" shows ``` hoelzl@37489 ` 1283` ``` "{a .. b} \ {c .. d} = {(\ i. max (a\$i) (c\$i)) .. (\ i. min (b\$i) (d\$i))}" ``` nipkow@39302 ` 1284` ``` unfolding set_eq_iff and Int_iff and mem_interval_cart ``` hoelzl@37489 ` 1285` ``` by auto ``` hoelzl@37489 ` 1286` hoelzl@37489 ` 1287` ```lemma closed_interval_left_cart: fixes b::"real^'n" ``` hoelzl@37489 ` 1288` ``` shows "closed {x::real^'n. \i. x\$i \ b\$i}" ``` huffman@44233 ` 1289` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le) ``` hoelzl@37489 ` 1290` hoelzl@37489 ` 1291` ```lemma closed_interval_right_cart: fixes a::"real^'n" ``` hoelzl@37489 ` 1292` ``` shows "closed {x::real^'n. \i. a\$i \ x\$i}" ``` huffman@44233 ` 1293` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le) ``` hoelzl@37489 ` 1294` hoelzl@37489 ` 1295` ```lemma is_interval_cart:"is_interval (s::(real^'n) set) \ ``` hoelzl@37489 ` 1296` ``` (\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@37489 ` 1297` ``` unfolding is_interval_def Ball_def by (simp add: cart_simps real_euclidean_nth) ``` hoelzl@37489 ` 1298` hoelzl@37489 ` 1299` ```lemma closed_halfspace_component_le_cart: ``` hoelzl@37489 ` 1300` ``` shows "closed {x::real^'n. x\$i \ a}" ``` huffman@44233 ` 1301` ``` by (simp add: closed_Collect_le) ``` hoelzl@37489 ` 1302` hoelzl@37489 ` 1303` ```lemma closed_halfspace_component_ge_cart: ``` hoelzl@37489 ` 1304` ``` shows "closed {x::real^'n. x\$i \ a}" ``` huffman@44233 ` 1305` ``` by (simp add: closed_Collect_le) ``` hoelzl@37489 ` 1306` hoelzl@37489 ` 1307` ```lemma open_halfspace_component_lt_cart: ``` hoelzl@37489 ` 1308` ``` shows "open {x::real^'n. x\$i < a}" ``` huffman@44233 ` 1309` ``` by (simp add: open_Collect_less) ``` hoelzl@37489 ` 1310` hoelzl@37489 ` 1311` ```lemma open_halfspace_component_gt_cart: ``` hoelzl@37489 ` 1312` ``` shows "open {x::real^'n. x\$i > a}" ``` huffman@44233 ` 1313` ``` by (simp add: open_Collect_less) ``` hoelzl@37489 ` 1314` hoelzl@37489 ` 1315` ```lemma Lim_component_le_cart: fixes f :: "'a \ real^'n" ``` hoelzl@37489 ` 1316` ``` assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. f(x)\$i \ b) net" ``` hoelzl@37489 ` 1317` ``` shows "l\$i \ b" ``` hoelzl@37489 ` 1318` ```proof- ``` hoelzl@37489 ` 1319` ``` { fix x have "x \ {x::real^'n. inner (cart_basis i) x \ b} \ x\$i \ b" unfolding inner_basis by auto } note * = this ``` hoelzl@37489 ` 1320` ``` show ?thesis using Lim_in_closed_set[of "{x. inner (cart_basis i) x \ b}" f net l] unfolding * ``` hoelzl@37489 ` 1321` ``` using closed_halfspace_le[of "(cart_basis i)::real^'n" b] and assms(1,2,3) by auto ``` hoelzl@37489 ` 1322` ```qed ``` hoelzl@37489 ` 1323` hoelzl@37489 ` 1324` ```lemma Lim_component_ge_cart: fixes f :: "'a \ real^'n" ``` hoelzl@37489 ` 1325` ``` assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)\$i) net" ``` hoelzl@37489 ` 1326` ``` shows "b \ l\$i" ``` hoelzl@37489 ` 1327` ```proof- ``` hoelzl@37489 ` 1328` ``` { fix x have "x \ {x::real^'n. inner (cart_basis i) x \ b} \ x\$i \ b" unfolding inner_basis by auto } note * = this ``` hoelzl@37489 ` 1329` ``` show ?thesis using Lim_in_closed_set[of "{x. inner (cart_basis i) x \ b}" f net l] unfolding * ``` hoelzl@37489 ` 1330` ``` using closed_halfspace_ge[of b "(cart_basis i)::real^'n"] and assms(1,2,3) by auto ``` hoelzl@37489 ` 1331` ```qed ``` hoelzl@37489 ` 1332` hoelzl@37489 ` 1333` ```lemma Lim_component_eq_cart: fixes f :: "'a \ real^'n" ``` hoelzl@37489 ` 1334` ``` assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\x. f(x)\$i = b) net" ``` hoelzl@37489 ` 1335` ``` shows "l\$i = b" ``` huffman@44211 ` 1336` ``` using ev[unfolded order_eq_iff eventually_conj_iff] using Lim_component_ge_cart[OF net, of b i] and ``` hoelzl@37489 ` 1337` ``` Lim_component_le_cart[OF net, of i b] by auto ``` hoelzl@37489 ` 1338` hoelzl@37489 ` 1339` ```lemma connected_ivt_component_cart: fixes x::"real^'n" shows ``` hoelzl@37489 ` 1340` ``` "connected s \ x \ s \ y \ s \ x\$k \ a \ a \ y\$k \ (\z\s. z\$k = a)" ``` hoelzl@37489 ` 1341` ``` using connected_ivt_hyperplane[of s x y "(cart_basis k)::real^'n" a] by (auto simp add: inner_basis) ``` hoelzl@37489 ` 1342` hoelzl@37489 ` 1343` ```lemma subspace_substandard_cart: ``` hoelzl@37489 ` 1344` ``` "subspace {x::real^_. (\i. P i \ x\$i = 0)}" ``` hoelzl@37489 ` 1345` ``` unfolding subspace_def by auto ``` hoelzl@37489 ` 1346` hoelzl@37489 ` 1347` ```lemma closed_substandard_cart: ``` huffman@44213 ` 1348` ``` "closed {x::'a::real_normed_vector ^ 'n. \i. P i \ x\$i = 0}" ``` hoelzl@37489 ` 1349` ```proof- ``` huffman@44213 ` 1350` ``` { fix i::'n ``` huffman@44213 ` 1351` ``` have "closed {x::'a ^ 'n. P i \ x\$i = 0}" ``` huffman@44233 ` 1352` ``` by (cases "P i", simp_all add: closed_Collect_eq) } ``` huffman@44213 ` 1353` ``` thus ?thesis ``` huffman@44213 ` 1354` ``` unfolding Collect_all_eq by (simp add: closed_INT) ``` hoelzl@37489 ` 1355` ```qed ``` hoelzl@37489 ` 1356` hoelzl@37489 ` 1357` ```lemma dim_substandard_cart: ``` hoelzl@37489 ` 1358` ``` shows "dim {x::real^'n. \i. i \ d \ x\$i = 0} = card d" (is "dim ?A = _") ``` huffman@44136 ` 1359` ```proof- have *:"{x. \i \' ` d \ x \$\$ i = 0} = ``` hoelzl@37489 ` 1360` ``` {x::real^'n. \i. i \ d \ x\$i = 0}"apply safe ``` hoelzl@37489 ` 1361` ``` apply(erule_tac x="\' i" in allE) defer ``` hoelzl@37489 ` 1362` ``` apply(erule_tac x="\ i" in allE) ``` hoelzl@37489 ` 1363` ``` unfolding image_iff real_euclidean_nth[symmetric] by (auto simp: pi'_inj[THEN inj_eq]) ``` huffman@44136 ` 1364` ``` have " \' ` d \ {..'" d] using pi'_inj unfolding inj_on_def by auto ``` hoelzl@37489 ` 1367` ```qed ``` hoelzl@37489 ` 1368` hoelzl@37489 ` 1369` ```lemma affinity_inverses: ``` hoelzl@37489 ` 1370` ``` assumes m0: "m \ (0::'a::field)" ``` hoelzl@37489 ` 1371` ``` shows "(\x. m *s x + c) o (\x. inverse(m) *s x + (-(inverse(m) *s c))) = id" ``` hoelzl@37489 ` 1372` ``` "(\x. inverse(m) *s x + (-(inverse(m) *s c))) o (\x. m *s x + c) = id" ``` hoelzl@37489 ` 1373` ``` using m0 ``` nipkow@39302 ` 1374` ```apply (auto simp add: fun_eq_iff vector_add_ldistrib) ``` hoelzl@37489 ` 1375` ```by (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric]) ``` hoelzl@37489 ` 1376` hoelzl@37489 ` 1377` ```lemma vector_affinity_eq: ``` hoelzl@37489 ` 1378` ``` assumes m0: "(m::'a::field) \ 0" ``` hoelzl@37489 ` 1379` ``` shows "m *s x + c = y \ x = inverse m *s y + -(inverse m *s c)" ``` hoelzl@37489 ` 1380` ```proof ``` hoelzl@37489 ` 1381` ``` assume h: "m *s x + c = y" ``` hoelzl@37489 ` 1382` ``` hence "m *s x = y - c" by (simp add: field_simps) ``` hoelzl@37489 ` 1383` ``` hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp ``` hoelzl@37489 ` 1384` ``` then show "x = inverse m *s y + - (inverse m *s c)" ``` hoelzl@37489 ` 1385` ``` using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) ``` hoelzl@37489 ` 1386` ```next ``` hoelzl@37489 ` 1387` ``` assume h: "x = inverse m *s y + - (inverse m *s c)" ``` hoelzl@37489 ` 1388` ``` show "m *s x + c = y" unfolding h diff_minus[symmetric] ``` hoelzl@37489 ` 1389` ``` using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) ``` hoelzl@37489 ` 1390` ```qed ``` hoelzl@37489 ` 1391` hoelzl@37489 ` 1392` ```lemma vector_eq_affinity: ``` hoelzl@37489 ` 1393` ``` "(m::'a::field) \ 0 ==> (y = m *s x + c \ inverse(m) *s y + -(inverse(m) *s c) = x)" ``` hoelzl@37489 ` 1394` ``` using vector_affinity_eq[where m=m and x=x and y=y and c=c] ``` hoelzl@37489 ` 1395` ``` by metis ``` hoelzl@37489 ` 1396` hoelzl@37489 ` 1397` ```lemma const_vector_cart:"((\ i. d)::real^'n) = (\\ i. d)" ``` hoelzl@37489 ` 1398` ``` apply(subst euclidean_eq) ``` hoelzl@37489 ` 1399` ```proof safe case goal1 ``` hoelzl@37489 ` 1400` ``` hence *:"(basis i::real^'n) = cart_basis (\ i)" ``` hoelzl@37489 ` 1401` ``` unfolding basis_real_n[THEN sym] by auto ``` hoelzl@37489 ` 1402` ``` have "((\ i. d)::real^'n) \$\$ i = d" unfolding euclidean_component_def * ``` hoelzl@37489 ` 1403` ``` unfolding dot_basis by auto ``` hoelzl@37489 ` 1404` ``` thus ?case using goal1 by auto ``` hoelzl@37489 ` 1405` ```qed ``` hoelzl@37489 ` 1406` huffman@44360 ` 1407` ```subsection "Convex Euclidean Space" ``` hoelzl@37489 ` 1408` hoelzl@37489 ` 1409` ```lemma Cart_1:"(1::real^'n) = (\\ i. 1)" ``` hoelzl@37489 ` 1410` ``` apply(subst euclidean_eq) ``` hoelzl@37489 ` 1411` ```proof safe case goal1 thus ?case using nth_conv_component[THEN sym,where i1="\ i" and x1="1::real^'n"] by auto ``` hoelzl@37489 ` 1412` ```qed ``` hoelzl@37489 ` 1413` hoelzl@37489 ` 1414` ```declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp] ``` hoelzl@37489 ` 1415` ```declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp] ``` hoelzl@37489 ` 1416` huffman@44136 ` 1417` ```lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component less_eq_vec_def vec_lambda_beta basis_component vector_uminus_component ``` hoelzl@37489 ` 1418` hoelzl@37489 ` 1419` ```lemma convex_box_cart: ``` hoelzl@37489 ` 1420` ``` assumes "\i. convex {x. P i x}" ``` hoelzl@37489 ` 1421` ``` shows "convex {x. \i. P i (x\$i)}" ``` hoelzl@37489 ` 1422` ``` using assms unfolding convex_def by auto ``` hoelzl@37489 ` 1423` hoelzl@37489 ` 1424` ```lemma convex_positive_orthant_cart: "convex {x::real^'n. (\i. 0 \ x\$i)}" ``` hoelzl@37489 ` 1425` ``` by (rule convex_box_cart) (simp add: atLeast_def[symmetric] convex_real_interval) ``` hoelzl@37489 ` 1426` hoelzl@37489 ` 1427` ```lemma unit_interval_convex_hull_cart: ``` hoelzl@37489 ` 1428` ``` "{0::real^'n .. 1} = convex hull {x. \i. (x\$i = 0) \ (x\$i = 1)}" (is "?int = convex hull ?points") ``` hoelzl@37489 ` 1429` ``` unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"] ``` nipkow@39302 ` 1430` ``` apply(rule arg_cong[where f="\x. convex hull x"]) apply(rule set_eqI) unfolding mem_Collect_eq ``` hoelzl@37489 ` 1431` ``` apply safe apply(erule_tac x="\' i" in allE) unfolding nth_conv_component defer ``` hoelzl@37489 ` 1432` ``` apply(erule_tac x="\ i" in allE) by auto ``` hoelzl@37489 ` 1433` hoelzl@37489 ` 1434` ```lemma cube_convex_hull_cart: ``` hoelzl@37489 ` 1435` ``` assumes "0 < d" obtains s::"(real^'n) set" where "finite s" "{x - (\ i. d) .. x + (\ i. d)} = convex hull s" ``` hoelzl@37489 ` 1436` ```proof- from cube_convex_hull[OF assms, where 'a="real^'n" and x=x] guess s . note s=this ``` hoelzl@37489 ` 1437` ``` show thesis apply(rule that[OF s(1)]) unfolding s(2)[THEN sym] const_vector_cart .. ``` hoelzl@37489 ` 1438` ```qed ``` hoelzl@37489 ` 1439` hoelzl@37489 ` 1440` ```lemma std_simplex_cart: ``` hoelzl@37489 ` 1441` ``` "(insert (0::real^'n) { cart_basis i | i. i\UNIV}) = ``` huffman@44136 ` 1442` ``` (insert 0 { basis i | i. i i. u\$i + (x\$i - a\$i) / (b\$i - a\$i) * (v\$i - u\$i))::real^'n)" ``` hoelzl@37489 ` 1468` ``` unfolding interval_bij_def apply(rule ext)+ apply safe ``` huffman@44136 ` 1469` ``` unfolding vec_eq_iff vec_lambda_beta unfolding nth_conv_component ``` hoelzl@37489 ` 1470` ``` apply rule apply(subst euclidean_lambda_beta) using pi'_range by auto ``` hoelzl@37489 ` 1471` hoelzl@37489 ` 1472` ```lemma interval_bij_affine_cart: ``` hoelzl@37489 ` 1473` ``` "interval_bij (a,b) (u,v) = (\x. (\ i. (v\$i - u\$i) / (b\$i - a\$i) * x\$i) + ``` hoelzl@37489 ` 1474` ``` (\ i. u\$i - (v\$i - u\$i) / (b\$i - a\$i) * a\$i)::real^'n)" ``` huffman@44136 ` 1475` ``` apply rule unfolding vec_eq_iff interval_bij_cart vector_component_simps ``` hoelzl@37489 ` 1476` ``` by(auto simp add: field_simps add_divide_distrib[THEN sym]) ``` hoelzl@37489 ` 1477` hoelzl@37489 ` 1478` ```subsection "Derivative" ``` hoelzl@37489 ` 1479` hoelzl@37489 ` 1480` ```lemma has_derivative_vmul_component_cart: fixes c::"real^'a \ real^'b" and v::"real^'c" ``` hoelzl@37489 ` 1481` ``` assumes "(c has_derivative c') net" ``` huffman@44140 ` 1482` ``` shows "((\x. c(x)\$k *\<^sub>R v) has_derivative (\x. (c' x)\$k *\<^sub>R v)) net" ``` huffman@44140 ` 1483` ``` unfolding nth_conv_component ``` huffman@44140 ` 1484` ``` by (intro has_derivative_intros assms) ``` hoelzl@37489 ` 1485` hoelzl@37489 ` 1486` ```lemma differentiable_at_imp_differentiable_on: "(\x\(s::(real^'n) set). f differentiable at x) \ f differentiable_on s" ``` hoelzl@37489 ` 1487` ``` unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI) ``` hoelzl@37489 ` 1488` hoelzl@37489 ` 1489` ```definition "jacobian f net = matrix(frechet_derivative f net)" ``` hoelzl@37489 ` 1490` hoelzl@37489 ` 1491` ```lemma jacobian_works: "(f::(real^'a) \ (real^'b)) differentiable net \ (f has_derivative (\h. (jacobian f net) *v h)) net" ``` hoelzl@37489 ` 1492` ``` apply rule unfolding jacobian_def apply(simp only: matrix_works[OF linear_frechet_derivative]) defer ``` hoelzl@37489 ` 1493` ``` apply(rule differentiableI) apply assumption unfolding frechet_derivative_works by assumption ``` hoelzl@37489 ` 1494` hoelzl@37489 ` 1495` ```subsection {* Component of the differential must be zero if it exists at a local *) ``` hoelzl@37489 ` 1496` ```(* maximum or minimum for that corresponding component. *} ``` hoelzl@37489 ` 1497` hoelzl@37489 ` 1498` ```lemma differential_zero_maxmin_component: fixes f::"real^'a \ real^'b" ``` hoelzl@37489 ` 1499` ``` assumes "0 < e" "((\y \ ball x e. (f y)\$k \ (f x)\$k) \ (\y\ball x e. (f x)\$k \ (f y)\$k))" ``` hoelzl@37489 ` 1500` ``` "f differentiable (at x)" shows "jacobian f (at x) \$ k = 0" ``` hoelzl@37489 ` 1501` ```(* FIXME: reuse proof of generic differential_zero_maxmin_component*) ``` hoelzl@37489 ` 1502` hoelzl@37489 ` 1503` ```proof(rule ccontr) ``` hoelzl@37489 ` 1504` ``` def D \ "jacobian f (at x)" assume "jacobian f (at x) \$ k \ 0" ``` huffman@44136 ` 1505` ``` then obtain j where j:"D\$k\$j \ 0" unfolding vec_eq_iff D_def by auto ``` hoelzl@37489 ` 1506` ``` hence *:"abs (jacobian f (at x) \$ k \$ j) / 2 > 0" unfolding D_def by auto ``` hoelzl@37489 ` 1507` ``` note as = assms(3)[unfolded jacobian_works has_derivative_at_alt] ``` hoelzl@37489 ` 1508` ``` guess e' using as[THEN conjunct2,rule_format,OF *] .. note e' = this ``` hoelzl@37489 ` 1509` ``` guess d using real_lbound_gt_zero[OF assms(1) e'[THEN conjunct1]] .. note d = this ``` hoelzl@37489 ` 1510` ``` { fix c assume "abs c \ d" ``` hoelzl@37489 ` 1511` ``` hence *:"norm (x + c *\<^sub>R cart_basis j - x) < e'" using norm_basis[of j] d by auto ``` hoelzl@37489 ` 1512` ``` have "\(f (x + c *\<^sub>R cart_basis j) - f x - D *v (c *\<^sub>R cart_basis j)) \$ k\ \ norm (f (x + c *\<^sub>R cart_basis j) - f x - D *v (c *\<^sub>R cart_basis j))" ``` hoelzl@37489 ` 1513` ``` by(rule component_le_norm_cart) ``` hoelzl@37489 ` 1514` ``` also have "\ \ \D \$ k \$ j\ / 2 * \c\" using e'[THEN conjunct2,rule_format,OF *] and norm_basis[of j] unfolding D_def[symmetric] by auto ``` hoelzl@37489 ` 1515` ``` finally have "\(f (x + c *\<^sub>R cart_basis j) - f x - D *v (c *\<^sub>R cart_basis j)) \$ k\ \ \D \$ k \$ j\ / 2 * \c\" by simp ``` hoelzl@37489 ` 1516` ``` hence "\f (x + c *\<^sub>R cart_basis j) \$ k - f x \$ k - c * D \$ k \$ j\ \ \D \$ k \$ j\ / 2 * \c\" ``` hoelzl@37489 ` 1517` ``` unfolding vector_component_simps matrix_vector_mul_component unfolding smult_conv_scaleR[symmetric] ``` hoelzl@37489 ` 1518` ``` unfolding inner_simps dot_basis smult_conv_scaleR by simp } note * = this ``` hoelzl@37489 ` 1519` ``` have "x + d *\<^sub>R cart_basis j \ ball x e" "x - d *\<^sub>R cart_basis j \ ball x e" ``` hoelzl@37489 ` 1520` ``` unfolding mem_ball dist_norm using norm_basis[of j] d by auto ``` hoelzl@37489 ` 1521` ``` hence **:"((f (x - d *\<^sub>R cart_basis j))\$k \ (f x)\$k \ (f (x + d *\<^sub>R cart_basis j))\$k \ (f x)\$k) \ ``` hoelzl@37489 ` 1522` ``` ((f (x - d *\<^sub>R cart_basis j))\$k \ (f x)\$k \ (f (x + d *\<^sub>R cart_basis j))\$k \ (f x)\$k)" using assms(2) by auto ``` hoelzl@37489 ` 1523` ``` have ***:"\y y1 y2 d dx::real. (y1\y\y2\y) \ (y\y1\y\y2) \ d < abs dx \ abs(y1 - y - - dx) \ d \ (abs (y2 - y - dx) \ d) \ False" by arith ``` hoelzl@37489 ` 1524` ``` show False apply(rule ***[OF **, where dx="d * D \$ k \$ j" and d="\D \$ k \$ j\ / 2 * \d\"]) ``` hoelzl@37489 ` 1525` ``` using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left ``` huffman@44282 ` 1526` ``` unfolding abs_mult diff_minus_eq_add scaleR_minus_left unfolding algebra_simps by (auto intro: mult_pos_pos) ``` hoelzl@37489 ` 1527` ```qed ``` hoelzl@37489 ` 1528` hoelzl@37494 ` 1529` ```subsection {* Lemmas for working on @{typ "real^1"} *} ``` hoelzl@37489 ` 1530` hoelzl@37489 ` 1531` ```lemma forall_1[simp]: "(\i::1. P i) \ P 1" ``` hoelzl@37489 ` 1532` ``` by (metis num1_eq_iff) ``` hoelzl@37489 ` 1533` hoelzl@37489 ` 1534` ```lemma ex_1[simp]: "(\x::1. P x) \ P 1" ``` hoelzl@37489 ` 1535` ``` by auto (metis num1_eq_iff) ``` hoelzl@37489 ` 1536` hoelzl@37489 ` 1537` ```lemma exhaust_2: ``` hoelzl@37489 ` 1538` ``` fixes x :: 2 shows "x = 1 \ x = 2" ``` hoelzl@37489 ` 1539` ```proof (induct x) ``` hoelzl@37489 ` 1540` ``` case (of_int z) ``` hoelzl@37489 ` 1541` ``` then have "0 <= z" and "z < 2" by simp_all ``` hoelzl@37489 ` 1542` ``` then have "z = 0 | z = 1" by arith ``` hoelzl@37489 ` 1543` ``` then show ?case by auto ``` hoelzl@37489 ` 1544` ```qed ``` hoelzl@37489 ` 1545` hoelzl@37489 ` 1546` ```lemma forall_2: "(\i::2. P i) \ P 1 \ P 2" ``` hoelzl@37489 ` 1547` ``` by (metis exhaust_2) ``` hoelzl@37489 ` 1548` hoelzl@37489 ` 1549` ```lemma exhaust_3: ``` hoelzl@37489 ` 1550` ``` fixes x :: 3 shows "x = 1 \ x = 2 \ x = 3" ``` hoelzl@37489 ` 1551` ```proof (induct x) ``` hoelzl@37489 ` 1552` ``` case (of_int z) ``` hoelzl@37489 ` 1553` ``` then have "0 <= z" and "z < 3" by simp_all ``` hoelzl@37489 ` 1554` ``` then have "z = 0 \ z = 1 \ z = 2" by arith ``` hoelzl@37489 ` 1555` ``` then show ?case by auto ``` hoelzl@37489 ` 1556` ```qed ``` hoelzl@37489 ` 1557` hoelzl@37489 ` 1558` ```lemma forall_3: "(\i::3. P i) \ P 1 \ P 2 \ P 3" ``` hoelzl@37489 ` 1559` ``` by (metis exhaust_3) ``` hoelzl@37489 ` 1560` hoelzl@37489 ` 1561` ```lemma UNIV_1 [simp]: "UNIV = {1::1}" ``` hoelzl@37489 ` 1562` ``` by (auto simp add: num1_eq_iff) ``` hoelzl@37489 ` 1563` hoelzl@37489 ` 1564` ```lemma UNIV_2: "UNIV = {1::2, 2::2}" ``` hoelzl@37489 ` 1565` ``` using exhaust_2 by auto ``` hoelzl@37489 ` 1566` hoelzl@37489 ` 1567` ```lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" ``` hoelzl@37489 ` 1568` ``` using exhaust_3 by auto ``` hoelzl@37489 ` 1569` hoelzl@37489 ` 1570` ```lemma setsum_1: "setsum f (UNIV::1 set) = f 1" ``` hoelzl@37489 ` 1571` ``` unfolding UNIV_1 by simp ``` hoelzl@37489 ` 1572` hoelzl@37489 ` 1573` ```lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2" ``` hoelzl@37489 ` 1574` ``` unfolding UNIV_2 by simp ``` hoelzl@37489 ` 1575` hoelzl@37489 ` 1576` ```lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3" ``` hoelzl@37489 ` 1577` ``` unfolding UNIV_3 by (simp add: add_ac) ``` hoelzl@37489 ` 1578` hoelzl@37489 ` 1579` ```instantiation num1 :: cart_one begin ``` hoelzl@37489 ` 1580` ```instance proof ``` hoelzl@37489 ` 1581` ``` show "CARD(1) = Suc 0" by auto ``` hoelzl@37489 ` 1582` ```qed end ``` hoelzl@37489 ` 1583` hoelzl@37489 ` 1584` ```(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *) ``` hoelzl@37489 ` 1585` hoelzl@37489 ` 1586` ```abbreviation vec1:: "'a \ 'a ^ 1" where "vec1 x \ vec x" ``` hoelzl@37489 ` 1587` hoelzl@37489 ` 1588` ```abbreviation dest_vec1:: "'a ^1 \ 'a" ``` hoelzl@37489 ` 1589` ``` where "dest_vec1 x \ (x\$1)" ``` hoelzl@37489 ` 1590` huffman@44167 ` 1591` ```lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" ``` huffman@44167 ` 1592` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 1593` hoelzl@37489 ` 1594` ```lemma forall_vec1: "(\x. P x) \ (\x. P (vec1 x))" ``` hoelzl@37489 ` 1595` ``` by (metis vec1_dest_vec1(1)) ``` hoelzl@37489 ` 1596` hoelzl@37489 ` 1597` ```lemma exists_vec1: "(\x. P x) \ (\x. P(vec1 x))" ``` hoelzl@37489 ` 1598` ``` by (metis vec1_dest_vec1(1)) ``` hoelzl@37489 ` 1599` hoelzl@37489 ` 1600` ```lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \ x = y" ``` hoelzl@37489 ` 1601` ``` by (metis vec1_dest_vec1(1)) ``` hoelzl@37489 ` 1602` hoelzl@37489 ` 1603` ```subsection{* The collapse of the general concepts to dimension one. *} ``` hoelzl@37489 ` 1604` hoelzl@37489 ` 1605` ```lemma vector_one: "(x::'a ^1) = (\ i. (x\$1))" ``` huffman@44136 ` 1606` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 1607` hoelzl@37489 ` 1608` ```lemma forall_one: "(\(x::'a ^1). P x) \ (\x. P(\ i. x))" ``` hoelzl@37489 ` 1609` ``` apply auto ``` hoelzl@37489 ` 1610` ``` apply (erule_tac x= "x\$1" in allE) ``` hoelzl@37489 ` 1611` ``` apply (simp only: vector_one[symmetric]) ``` hoelzl@37489 ` 1612` ``` done ``` hoelzl@37489 ` 1613` hoelzl@37489 ` 1614` ```lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)" ``` huffman@44136 ` 1615` ``` by (simp add: norm_vec_def) ``` hoelzl@37489 ` 1616` hoelzl@37489 ` 1617` ```lemma norm_real: "norm(x::real ^ 1) = abs(x\$1)" ``` hoelzl@37489 ` 1618` ``` by (simp add: norm_vector_1) ``` hoelzl@37489 ` 1619` hoelzl@37489 ` 1620` ```lemma dist_real: "dist(x::real ^ 1) y = abs((x\$1) - (y\$1))" ``` hoelzl@37489 ` 1621` ``` by (auto simp add: norm_real dist_norm) ``` hoelzl@37489 ` 1622` hoelzl@37489 ` 1623` ```subsection{* Explicit vector construction from lists. *} ``` hoelzl@37489 ` 1624` hoelzl@43995 ` 1625` ```definition "vector l = (\ i. foldr (\x f n. fun_upd (f (n+1)) n x) l (\n x. 0) 1 i)" ``` hoelzl@37489 ` 1626` hoelzl@37489 ` 1627` ```lemma vector_1: "(vector[x]) \$1 = x" ``` hoelzl@37489 ` 1628` ``` unfolding vector_def by simp ``` hoelzl@37489 ` 1629` hoelzl@37489 ` 1630` ```lemma vector_2: ``` hoelzl@37489 ` 1631` ``` "(vector[x,y]) \$1 = x" ``` hoelzl@37489 ` 1632` ``` "(vector[x,y] :: 'a^2)\$2 = (y::'a::zero)" ``` hoelzl@37489 ` 1633` ``` unfolding vector_def by simp_all ``` hoelzl@37489 ` 1634` hoelzl@37489 ` 1635` ```lemma vector_3: ``` hoelzl@37489 ` 1636` ``` "(vector [x,y,z] ::('a::zero)^3)\$1 = x" ``` hoelzl@37489 ` 1637` ``` "(vector [x,y,z] ::('a::zero)^3)\$2 = y" ``` hoelzl@37489 ` 1638` ``` "(vector [x,y,z] ::('a::zero)^3)\$3 = z" ``` hoelzl@37489 ` 1639` ``` unfolding vector_def by simp_all ``` hoelzl@37489 ` 1640` hoelzl@37489 ` 1641` ```lemma forall_vector_1: "(\v::'a::zero^1. P v) \ (\x. P(vector[x]))" ``` hoelzl@37489 ` 1642` ``` apply auto ``` hoelzl@37489 ` 1643` ``` apply (erule_tac x="v\$1" in allE) ``` hoelzl@37489 ` 1644` ``` apply (subgoal_tac "vector [v\$1] = v") ``` hoelzl@37489 ` 1645` ``` apply simp ``` hoelzl@37489 ` 1646` ``` apply (vector vector_def) ``` hoelzl@37489 ` 1647` ``` apply simp ``` hoelzl@37489 ` 1648` ``` done ``` hoelzl@37489 ` 1649` hoelzl@37489 ` 1650` ```lemma forall_vector_2: "(\v::'a::zero^2. P v) \ (\x y. P(vector[x, y]))" ``` hoelzl@37489 ` 1651` ``` apply auto ``` hoelzl@37489 ` 1652` ``` apply (erule_tac x="v\$1" in allE) ``` hoelzl@37489 ` 1653` ``` apply (erule_tac x="v\$2" in allE) ``` hoelzl@37489 ` 1654` ``` apply (subgoal_tac "vector [v\$1, v\$2] = v") ``` hoelzl@37489 ` 1655` ``` apply simp ``` hoelzl@37489 ` 1656` ``` apply (vector vector_def) ``` hoelzl@37489 ` 1657` ``` apply (simp add: forall_2) ``` hoelzl@37489 ` 1658` ``` done ``` hoelzl@37489 ` 1659` hoelzl@37489 ` 1660` ```lemma forall_vector_3: "(\v::'a::zero^3. P v) \ (\x y z. P(vector[x, y, z]))" ``` hoelzl@37489 ` 1661` ``` apply auto ``` hoelzl@37489 ` 1662` ``` apply (erule_tac x="v\$1" in allE) ``` hoelzl@37489 ` 1663` ``` apply (erule_tac x="v\$2" in allE) ``` hoelzl@37489 ` 1664` ``` apply (erule_tac x="v\$3" in allE) ``` hoelzl@37489 ` 1665` ``` apply (subgoal_tac "vector [v\$1, v\$2, v\$3] = v") ``` hoelzl@37489 ` 1666` ``` apply simp ``` hoelzl@37489 ` 1667` ``` apply (vector vector_def) ``` hoelzl@37489 ` 1668` ``` apply (simp add: forall_3) ``` hoelzl@37489 ` 1669` ``` done ``` hoelzl@37489 ` 1670` nipkow@39302 ` 1671` ```lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_eqI,rule) unfolding image_iff defer ``` hoelzl@37489 ` 1672` ``` apply(rule_tac x="dest_vec1 x" in bexI) by auto ``` hoelzl@37489 ` 1673` hoelzl@37489 ` 1674` ```lemma dest_vec1_lambda: "dest_vec1(\ i. x i) = x 1" ``` hoelzl@37489 ` 1675` ``` by (simp) ``` hoelzl@37489 ` 1676` hoelzl@37489 ` 1677` ```lemma dest_vec1_vec: "dest_vec1(vec x) = x" ``` hoelzl@37489 ` 1678` ``` by (simp) ``` hoelzl@37489 ` 1679` hoelzl@37489 ` 1680` ```lemma dest_vec1_sum: assumes fS: "finite S" ``` hoelzl@37489 ` 1681` ``` shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S" ``` hoelzl@37489 ` 1682` ``` apply (induct rule: finite_induct[OF fS]) ``` hoelzl@37489 ` 1683` ``` apply simp ``` hoelzl@37489 ` 1684` ``` apply auto ``` hoelzl@37489 ` 1685` ``` done ``` hoelzl@37489 ` 1686` hoelzl@37489 ` 1687` ```lemma norm_vec1 [simp]: "norm(vec1 x) = abs(x)" ``` hoelzl@37489 ` 1688` ``` by (simp add: vec_def norm_real) ``` hoelzl@37489 ` 1689` hoelzl@37489 ` 1690` ```lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)" ``` huffman@44167 ` 1691` ``` by (simp only: dist_real vec_component) ``` hoelzl@37489 ` 1692` ```lemma abs_dest_vec1: "norm x = \dest_vec1 x\" ``` hoelzl@37489 ` 1693` ``` by (metis vec1_dest_vec1(1) norm_vec1) ``` hoelzl@37489 ` 1694` hoelzl@37489 ` 1695` ```lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component ``` huffman@44167 ` 1696` ``` vec_inj[where 'b=1] vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def real_norm_def ``` hoelzl@37489 ` 1697` hoelzl@37489 ` 1698` ```lemma bounded_linear_vec1:"bounded_linear (vec1::real\real^1)" ``` hoelzl@37489 ` 1699` ``` unfolding bounded_linear_def additive_def bounded_linear_axioms_def ``` hoelzl@37489 ` 1700` ``` unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps ``` hoelzl@37489 ` 1701` ``` apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto ``` hoelzl@37489 ` 1702` hoelzl@37489 ` 1703` ```lemma linear_vmul_dest_vec1: ``` hoelzl@37489 ` 1704` ``` fixes f:: "real^_ \ real^1" ``` hoelzl@37489 ` 1705` ``` shows "linear f \ linear (\x. dest_vec1(f x) *s v)" ``` hoelzl@37489 ` 1706` ``` unfolding smult_conv_scaleR ``` hoelzl@37489 ` 1707` ``` by (rule linear_vmul_component) ``` hoelzl@37489 ` 1708` hoelzl@37489 ` 1709` ```lemma linear_from_scalars: ``` hoelzl@37489 ` 1710` ``` assumes lf: "linear (f::real^1 \ real^_)" ``` hoelzl@37489 ` 1711` ``` shows "f = (\x. dest_vec1 x *s column 1 (matrix f))" ``` hoelzl@37489 ` 1712` ``` unfolding smult_conv_scaleR ``` hoelzl@37489 ` 1713` ``` apply (rule ext) ``` hoelzl@37489 ` 1714` ``` apply (subst matrix_works[OF lf, symmetric]) ``` huffman@44136 ` 1715` ``` apply (auto simp add: vec_eq_iff matrix_vector_mult_def column_def mult_commute) ``` hoelzl@37489 ` 1716` ``` done ``` hoelzl@37489 ` 1717` hoelzl@37489 ` 1718` ```lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \ real^1)" ``` hoelzl@37489 ` 1719` ``` shows "f = (\x. vec1(row 1 (matrix f) \ x))" ``` hoelzl@37489 ` 1720` ``` apply (rule ext) ``` hoelzl@37489 ` 1721` ``` apply (subst matrix_works[OF lf, symmetric]) ``` huffman@44136 ` 1722` ``` apply (simp add: vec_eq_iff matrix_vector_mult_def row_def inner_vec_def mult_commute) ``` hoelzl@37489 ` 1723` ``` done ``` hoelzl@37489 ` 1724` hoelzl@37489 ` 1725` ```lemma dest_vec1_eq_0: "dest_vec1 x = 0 \ x = 0" ``` hoelzl@37489 ` 1726` ``` by (simp add: dest_vec1_eq[symmetric]) ``` hoelzl@37489 ` 1727` hoelzl@37489 ` 1728` ```lemma setsum_scalars: assumes fS: "finite S" ``` hoelzl@37489 ` 1729` ``` shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)" ``` hoelzl@37489 ` 1730` ``` unfolding vec_setsum[OF fS] by simp ``` hoelzl@37489 ` 1731` hoelzl@37489 ` 1732` ```lemma dest_vec1_wlog_le: "(\(x::'a::linorder ^ 1) y. P x y \ P y x) \ (\x y. dest_vec1 x <= dest_vec1 y ==> P x y) \ P x y" ``` hoelzl@37489 ` 1733` ``` apply (cases "dest_vec1 x \ dest_vec1 y") ``` hoelzl@37489 ` 1734` ``` apply simp ``` hoelzl@37489 ` 1735` ``` apply (subgoal_tac "dest_vec1 y \ dest_vec1 x") ``` hoelzl@37489 ` 1736` ``` apply (auto) ``` hoelzl@37489 ` 1737` ``` done ``` hoelzl@37489 ` 1738` hoelzl@37489 ` 1739` ```text{* Lifting and dropping *} ``` hoelzl@37489 ` 1740` hoelzl@37489 ` 1741` ```lemma continuous_on_o_dest_vec1: fixes f::"real \ 'a::real_normed_vector" ``` hoelzl@37489 ` 1742` ``` assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)" ``` hoelzl@37489 ` 1743` ``` using assms unfolding continuous_on_iff apply safe ``` hoelzl@37489 ` 1744` ``` apply(erule_tac x="x\$1" in ballE,erule_tac x=e in allE) apply safe ``` hoelzl@37489 ` 1745` ``` apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real ``` huffman@44136 ` 1746` ``` apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:less_eq_vec_def) ``` hoelzl@37489 ` 1747` hoelzl@37489 ` 1748` ```lemma continuous_on_o_vec1: fixes f::"real^1 \ 'a::real_normed_vector" ``` hoelzl@37489 ` 1749` ``` assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)" ``` hoelzl@37489 ` 1750` ``` using assms unfolding continuous_on_iff apply safe ``` hoelzl@37489 ` 1751` ``` apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe ``` hoelzl@37489 ` 1752` ``` apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real ``` huffman@44136 ` 1753` ``` apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:less_eq_vec_def) ``` hoelzl@37489 ` 1754` hoelzl@37489 ` 1755` ```lemma continuous_on_vec1:"continuous_on A (vec1::real\real^1)" ``` hoelzl@37489 ` 1756` ``` by(rule linear_continuous_on[OF bounded_linear_vec1]) ``` hoelzl@37489 ` 1757` hoelzl@37489 ` 1758` ```lemma mem_interval_1: fixes x :: "real^1" shows ``` hoelzl@37489 ` 1759` ``` "(x \ {a .. b} \ dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b)" ``` hoelzl@37489 ` 1760` ``` "(x \ {a<.. dest_vec1 a < dest_vec1 x \ dest_vec1 x < dest_vec1 b)" ``` huffman@44136 ` 1761` ```by(simp_all add: vec_eq_iff less_vec_def less_eq_vec_def) ``` hoelzl@37489 ` 1762` hoelzl@37489 ` 1763` ```lemma vec1_interval:fixes a::"real" shows ``` hoelzl@37489 ` 1764` ``` "vec1 ` {a .. b} = {vec1 a .. vec1 b}" ``` hoelzl@37489 ` 1765` ``` "vec1 ` {a<.. {a .. b} ==> x \ {a<.. (x = a) \ (x = b)" ``` huffman@44136 ` 1775` ``` unfolding vec_eq_iff less_vec_def less_eq_vec_def mem_interval_cart by(auto simp del:dest_vec1_eq) ``` hoelzl@37489 ` 1776` hoelzl@37489 ` 1777` ```lemma in_interval_1: fixes x :: "real^1" shows ``` hoelzl@37489 ` 1778` ``` "(x \ {a .. b} \ dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b) \ ``` hoelzl@37489 ` 1779` ``` (x \ {a<.. dest_vec1 a < dest_vec1 x \ dest_vec1 x < dest_vec1 b)" ``` huffman@44136 ` 1780` ``` unfolding vec_eq_iff less_vec_def less_eq_vec_def mem_interval_cart by(auto simp del:dest_vec1_eq) ``` hoelzl@37489 ` 1781` hoelzl@37489 ` 1782` ```lemma interval_eq_empty_1: fixes a :: "real^1" shows ``` hoelzl@37489 ` 1783` ``` "{a .. b} = {} \ dest_vec1 b < dest_vec1 a" ``` hoelzl@37489 ` 1784` ``` "{a<.. dest_vec1 b \ dest_vec1 a" ``` hoelzl@37489 ` 1785` ``` unfolding interval_eq_empty_cart and ex_1 by auto ``` hoelzl@37489 ` 1786` hoelzl@37489 ` 1787` ```lemma subset_interval_1: fixes a :: "real^1" shows ``` hoelzl@37489 ` 1788` ``` "({a .. b} \ {c .. d} \ dest_vec1 b < dest_vec1 a \ ``` hoelzl@37489 ` 1789` ``` dest_vec1 c \ dest_vec1 a \ dest_vec1 a \ dest_vec1 b \ dest_vec1 b \ dest_vec1 d)" ``` hoelzl@37489 ` 1790` ``` "({a .. b} \ {c<.. dest_vec1 b < dest_vec1 a \ ``` hoelzl@37489 ` 1791` ``` dest_vec1 c < dest_vec1 a \ dest_vec1 a \ dest_vec1 b \ dest_vec1 b < dest_vec1 d)" ``` hoelzl@37489 ` 1792` ``` "({a<.. {c .. d} \ dest_vec1 b \ dest_vec1 a \ ``` hoelzl@37489 ` 1793` ``` dest_vec1 c \ dest_vec1 a \ dest_vec1 a < dest_vec1 b \ dest_vec1 b \ dest_vec1 d)" ``` hoelzl@37489 ` 1794` ``` "({a<.. {c<.. dest_vec1 b \ dest_vec1 a \ ``` hoelzl@37489 ` 1795` ``` dest_vec1 c \ dest_vec1 a \ dest_vec1 a < dest_vec1 b \ dest_vec1 b \ dest_vec1 d)" ``` hoelzl@37489 ` 1796` ``` unfolding subset_interval_cart[of a b c d] unfolding forall_1 by auto ``` hoelzl@37489 ` 1797` hoelzl@37489 ` 1798` ```lemma eq_interval_1: fixes a :: "real^1" shows ``` hoelzl@37489 ` 1799` ``` "{a .. b} = {c .. d} \ ``` hoelzl@37489 ` 1800` ``` dest_vec1 b < dest_vec1 a \ dest_vec1 d < dest_vec1 c \ ``` hoelzl@37489 ` 1801` ``` dest_vec1 a = dest_vec1 c \ dest_vec1 b = dest_vec1 d" ``` hoelzl@37489 ` 1802` ```unfolding set_eq_subset[of "{a .. b}" "{c .. d}"] ``` hoelzl@37489 ` 1803` ```unfolding subset_interval_1(1)[of a b c d] ``` hoelzl@37489 ` 1804` ```unfolding subset_interval_1(1)[of c d a b] ``` hoelzl@37489 ` 1805` ```by auto ``` hoelzl@37489 ` 1806` hoelzl@37489 ` 1807` ```lemma disjoint_interval_1: fixes a :: "real^1" shows ``` hoelzl@37489 ` 1808` ``` "{a .. b} \ {c .. d} = {} \ dest_vec1 b < dest_vec1 a \ dest_vec1 d < dest_vec1 c \ dest_vec1 b < dest_vec1 c \ dest_vec1 d < dest_vec1 a" ``` hoelzl@37489 ` 1809` ``` "{a .. b} \ {c<.. dest_vec1 b < dest_vec1 a \ dest_vec1 d \ dest_vec1 c \ dest_vec1 b \ dest_vec1 c \ dest_vec1 d \ dest_vec1 a" ``` hoelzl@37489 ` 1810` ``` "{a<.. {c .. d} = {} \ dest_vec1 b \ dest_vec1 a \ dest_vec1 d < dest_vec1 c \ dest_vec1 b \ dest_vec1 c \ dest_vec1 d \ dest_vec1 a" ``` hoelzl@37489 ` 1811` ``` "{a<.. {c<.. dest_vec1 b \ dest_vec1 a \ dest_vec1 d \ dest_vec1 c \ dest_vec1 b \ dest_vec1 c \ dest_vec1 d \ dest_vec1 a" ``` hoelzl@37489 ` 1812` ``` unfolding disjoint_interval_cart and ex_1 by auto ``` hoelzl@37489 ` 1813` hoelzl@37489 ` 1814` ```lemma open_closed_interval_1: fixes a :: "real^1" shows ``` hoelzl@37489 ` 1815` ``` "{a<.. dest_vec1 b ==> {a .. b} = {a<.. {a,b}" ``` huffman@44136 ` 1819` ``` unfolding set_eq_iff apply simp unfolding less_vec_def and less_eq_vec_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq) ``` hoelzl@37489 ` 1820` hoelzl@37489 ` 1821` ```lemma Lim_drop_le: fixes f :: "'a \ real^1" shows ``` hoelzl@37489 ` 1822` ``` "(f ---> l) net \ ~(trivial_limit net) \ eventually (\x. dest_vec1 (f x) \ b) net ==> dest_vec1 l \ b" ``` hoelzl@37489 ` 1823` ``` using Lim_component_le_cart[of f l net 1 b] by auto ``` hoelzl@37489 ` 1824` hoelzl@37489 ` 1825` ```lemma Lim_drop_ge: fixes f :: "'a \ real^1" shows ``` hoelzl@37489 ` 1826` ``` "(f ---> l) net \ ~(trivial_limit net) \ eventually (\x. b \ dest_vec1 (f x)) net ==> b \ dest_vec1 l" ``` hoelzl@37489 ` 1827` ``` using Lim_component_ge_cart[of f l net b 1] by auto ``` hoelzl@37489 ` 1828` hoelzl@37489 ` 1829` ```text{* Also more convenient formulations of monotone convergence. *} ``` hoelzl@37489 ` 1830` hoelzl@37489 ` 1831` ```lemma bounded_increasing_convergent: fixes s::"nat \ real^1" ``` hoelzl@37489 ` 1832` ``` assumes "bounded {s n| n::nat. True}" "\n. dest_vec1(s n) \ dest_vec1(s(Suc n))" ``` hoelzl@37489 ` 1833` ``` shows "\l. (s ---> l) sequentially" ``` hoelzl@37489 ` 1834` ```proof- ``` hoelzl@37489 ` 1835` ``` obtain a where a:"\n. \dest_vec1 (s n)\ \ a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto ``` hoelzl@37489 ` 1836` ``` { fix m::nat ``` hoelzl@37489 ` 1837` ``` have "\ n. n\m \ dest_vec1 (s m) \ dest_vec1 (s n)" ``` hoelzl@37489 ` 1838` ``` apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq) } ``` hoelzl@37489 ` 1839` ``` hence "\m n. m \ n \ dest_vec1 (s m) \ dest_vec1 (s n)" by auto ``` hoelzl@37489 ` 1840` ``` then obtain l where "\e>0. \N. \n\N. \dest_vec1 (s n) - l\ < e" using convergent_bounded_monotone[OF a] unfolding monoseq_def by auto ``` hoelzl@37489 ` 1841` ``` thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI) ``` hoelzl@37489 ` 1842` ``` unfolding dist_norm unfolding abs_dest_vec1 by auto ``` hoelzl@37489 ` 1843` ```qed ``` hoelzl@37489 ` 1844` hoelzl@37489 ` 1845` ```lemma dest_vec1_simps[simp]: fixes a::"real^1" ``` hoelzl@37489 ` 1846` ``` shows "a\$1 = 0 \ a = 0" (*"a \ 1 \ dest_vec1 a \ 1" "0 \ a \ 0 \ dest_vec1 a"*) ``` hoelzl@37489 ` 1847` ``` "a \ b \ dest_vec1 a \ dest_vec1 b" "dest_vec1 (1::real^1) = 1" ``` huffman@44136 ` 1848` ``` by(auto simp add: less_eq_vec_def vec_eq_iff) ``` hoelzl@37489 ` 1849` hoelzl@37489 ` 1850` ```lemma dest_vec1_inverval: ``` hoelzl@37489 ` 1851` ``` "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}" ``` hoelzl@37489 ` 1852` ``` "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}" ``` hoelzl@37489 ` 1853` ``` "dest_vec1 ` {a ..x. dest_vec1 (f x)) S" ``` hoelzl@37489 ` 1864` ``` using dest_vec1_sum[OF assms] by auto ``` hoelzl@37489 ` 1865` hoelzl@37489 ` 1866` ```lemma open_dest_vec1_vimage: "open S \ open (dest_vec1 -` S)" ``` huffman@44136 ` 1867` ```unfolding open_vec_def forall_1 by auto ``` hoelzl@37489 ` 1868` hoelzl@37489 ` 1869` ```lemma tendsto_dest_vec1 [tendsto_intros]: ``` hoelzl@37489 ` 1870` ``` "(f ---> l) net \ ((\x. dest_vec1 (f x)) ---> dest_vec1 l) net" ``` huffman@44136 ` 1871` ```by(rule tendsto_vec_nth) ``` hoelzl@37489 ` 1872` hoelzl@37489 ` 1873` ```lemma continuous_dest_vec1: "continuous net f \ continuous net (\x. dest_vec1 (f x))" ``` hoelzl@37489 ` 1874` ``` unfolding continuous_def by (rule tendsto_dest_vec1) ``` hoelzl@37489 ` 1875` hoelzl@37489 ` 1876` ```lemma forall_dest_vec1: "(\x. P x) \ (\x. P(dest_vec1 x))" ``` hoelzl@37489 ` 1877` ``` apply safe defer apply(erule_tac x="vec1 x" in allE) by auto ``` hoelzl@37489 ` 1878` hoelzl@37489 ` 1879` ```lemma forall_of_dest_vec1: "(\v. P (\x. dest_vec1 (v x))) \ (\x. P x)" ``` hoelzl@37489 ` 1880` ``` apply rule apply rule apply(erule_tac x="(vec1 \ x)" in allE) unfolding o_def vec1_dest_vec1 by auto ``` hoelzl@37489 ` 1881` hoelzl@37489 ` 1882` ```lemma forall_of_dest_vec1': "(\v. P (dest_vec1 v)) \ (\x. P x)" ``` hoelzl@37489 ` 1883` ``` apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule ``` hoelzl@37489 ` 1884` ``` apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto ``` hoelzl@37489 ` 1885` hoelzl@37489 ` 1886` ```lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding dist_norm by auto ``` hoelzl@37489 ` 1887` hoelzl@37489 ` 1888` ```lemma bounded_linear_vec1_dest_vec1: fixes f::"real \ real" ``` hoelzl@37489 ` 1889` ``` shows "linear (vec1 \ f \ dest_vec1) = bounded_linear f" (is "?l = ?r") proof- ``` hoelzl@37489 ` 1890` ``` { assume ?l guess K using linear_bounded[OF `?l`] .. ``` hoelzl@37489 ` 1891` ``` hence "\K. \x. \f x\ \ \x\ * K" apply(rule_tac x=K in exI) ``` hoelzl@37489 ` 1892` ``` unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) } ``` hoelzl@37489 ` 1893` ``` thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def ``` hoelzl@37489 ` 1894` ``` unfolding vec1_dest_vec1_simps by auto qed ``` hoelzl@37489 ` 1895` hoelzl@37489 ` 1896` ```lemma vec1_le[simp]:fixes a::real shows "vec1 a \ vec1 b \ a \ b" ``` huffman@44136 ` 1897` ``` unfolding less_eq_vec_def by auto ``` hoelzl@37489 ` 1898` ```lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \ a < b" ``` huffman@44136 ` 1899` ``` unfolding less_vec_def by auto ``` hoelzl@37489 ` 1900` hoelzl@37489 ` 1901` hoelzl@37489 ` 1902` ```subsection {* Derivatives on real = Derivatives on @{typ "real^1"} *} ``` hoelzl@37489 ` 1903` hoelzl@37489 ` 1904` ```lemma has_derivative_within_vec1_dest_vec1: fixes f::"real\real" shows ``` hoelzl@37489 ` 1905` ``` "((vec1 \ f \ dest_vec1) has_derivative (vec1 \ f' \ dest_vec1)) (at (vec1 x) within vec1 ` s) ``` hoelzl@37489 ` 1906` ``` = (f has_derivative f') (at x within s)" ``` hoelzl@37489 ` 1907` ``` unfolding has_derivative_within unfolding bounded_linear_vec1_dest_vec1[unfolded linear_conv_bounded_linear] ``` hoelzl@37489 ` 1908` ``` unfolding o_def Lim_within Ball_def unfolding forall_vec1 ``` hoelzl@37489 ` 1909` ``` unfolding vec1_dest_vec1_simps dist_vec1_0 image_iff by auto ``` hoelzl@37489 ` 1910` hoelzl@37489 ` 1911` ```lemma has_derivative_at_vec1_dest_vec1: fixes f::"real\real" shows ``` hoelzl@37489 ` 1912` ``` "((vec1 \ f \ dest_vec1) has_derivative (vec1 \ f' \ dest_vec1)) (at (vec1 x)) = (f has_derivative f') (at x)" ``` hoelzl@37489 ` 1913` ``` using has_derivative_within_vec1_dest_vec1[where s=UNIV, unfolded range_vec1 within_UNIV] by auto ``` hoelzl@37489 ` 1914` hoelzl@37489 ` 1915` ```lemma bounded_linear_vec1': fixes f::"'a::real_normed_vector\real" ``` hoelzl@37489 ` 1916` ``` shows "bounded_linear f = bounded_linear (vec1 \ f)" ``` hoelzl@37489 ` 1917` ``` unfolding bounded_linear_def additive_def bounded_linear_axioms_def o_def ``` hoelzl@37489 ` 1918` ``` unfolding vec1_dest_vec1_simps by auto ``` hoelzl@37489 ` 1919` hoelzl@37489 ` 1920` ```lemma bounded_linear_dest_vec1: fixes f::"real\'a::real_normed_vector" ``` hoelzl@37489 ` 1921` ``` shows "bounded_linear f = bounded_linear (f \ dest_vec1)" ``` hoelzl@37489 ` 1922` ``` unfolding bounded_linear_def additive_def bounded_linear_axioms_def o_def ``` hoelzl@37489 ` 1923` ``` unfolding vec1_dest_vec1_simps by auto ``` hoelzl@37489 ` 1924` hoelzl@37489 ` 1925` ```lemma has_derivative_at_vec1: fixes f::"'a::real_normed_vector\real" shows ``` hoelzl@37489 ` 1926` ``` "(f has_derivative f') (at x) = ((vec1 \ f) has_derivative (vec1 \ f')) (at x)" ``` hoelzl@37489 ` 1927` ``` unfolding has_derivative_at unfolding bounded_linear_vec1'[unfolded linear_conv_bounded_linear] ``` hoelzl@37489 ` 1928` ``` unfolding o_def Lim_at unfolding vec1_dest_vec1_simps dist_vec1_0 by auto ``` hoelzl@37489 ` 1929` hoelzl@37489 ` 1930` ```lemma has_derivative_within_dest_vec1:fixes f::"real\'a::real_normed_vector" shows ``` hoelzl@37489 ` 1931` ``` "((f \ dest_vec1) has_derivative (f' \ dest_vec1)) (at (vec1 x) within vec1 ` s) = (f has_derivative f') (at x within s)" ``` hoelzl@37489 ` 1932` ``` unfolding has_derivative_within bounded_linear_dest_vec1 unfolding o_def Lim_within Ball_def ``` hoelzl@37489 ` 1933` ``` unfolding vec1_dest_vec1_simps dist_vec1_0 image_iff by auto ``` hoelzl@37489 ` 1934` hoelzl@37489 ` 1935` ```lemma has_derivative_at_dest_vec1:fixes f::"real\'a::real_normed_vector" shows ``` hoelzl@37489 ` 1936` ``` "((f \ dest_vec1) has_derivative (f' \ dest_vec1)) (at (vec1 x)) = (f has_derivative f') (at x)" ``` hoelzl@37489 ` 1937` ``` using has_derivative_within_dest_vec1[where s=UNIV] by(auto simp add:within_UNIV) ``` hoelzl@37489 ` 1938` hoelzl@37489 ` 1939` ```subsection {* In particular if we have a mapping into @{typ "real^1"}. *} ``` hoelzl@37489 ` 1940` hoelzl@37489 ` 1941` ```lemma onorm_vec1: fixes f::"real \ real" ``` hoelzl@37489 ` 1942` ``` shows "onorm (\x. vec1 (f (dest_vec1 x))) = onorm f" proof- ``` huffman@44136 ` 1943` ``` have "\x::real^1. norm x = 1 \ x\{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:vec_eq_iff) ``` hoelzl@37489 ` 1944` ``` hence 1:"{x. norm x = 1} = {vec1 -1, vec1 (1::real)}" by auto ``` hoelzl@37489 ` 1945` ``` have 2:"{norm (vec1 (f (dest_vec1 x))) |x. norm x = 1} = (\x. norm (vec1 (f (dest_vec1 x)))) ` {x. norm x=1}" by auto ``` hoelzl@37489 ` 1946` ``` have "\x::real. norm x = 1 \ x\{-1, 1}" by auto hence 3:"{x. norm x = 1} = {-1, (1::real)}" by auto ``` hoelzl@37489 ` 1947` ``` have 4:"{norm (f x) |x. norm x = 1} = (\x. norm (f x)) ` {x. norm x=1}" by auto ``` hoelzl@37489 ` 1948` ``` show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max) qed ``` hoelzl@37489 ` 1949` hoelzl@37489 ` 1950` ```lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)" ``` hoelzl@37489 ` 1951` ``` unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto ``` hoelzl@37489 ` 1952` hoelzl@37489 ` 1953` ```lemma bounded_linear_component_cart[intro]: "bounded_linear (\x::real^'n. x \$ k)" ``` hoelzl@37489 ` 1954` ``` apply(rule bounded_linearI[where K=1]) ``` hoelzl@37489 ` 1955` ``` using component_le_norm_cart[of _ k] unfolding real_norm_def by auto ``` hoelzl@37489 ` 1956` hoelzl@37489 ` 1957` ```lemma bounded_vec1[intro]: "bounded s \ bounded (vec1 ` (s::real set))" ``` hoelzl@37489 ` 1958` ``` unfolding bounded_def apply safe apply(rule_tac x="vec1 x" in exI,rule_tac x=e in exI) ``` hoelzl@37489 ` 1959` ``` by(auto simp add: dist_real dist_real_def) ``` hoelzl@37489 ` 1960` hoelzl@37489 ` 1961` ```(*lemma content_closed_interval_cases_cart: ``` hoelzl@37489 ` 1962` ``` "content {a..b::real^'n} = ``` hoelzl@37489 ` 1963` ``` (if {a..b} = {} then 0 else setprod (\i. b\$i - a\$i) UNIV)" ``` hoelzl@37489 ` 1964` ```proof(cases "{a..b} = {}") ``` hoelzl@37489 ` 1965` ``` case True thus ?thesis unfolding content_def by auto ``` hoelzl@37489 ` 1966` ```next case Falsethus ?thesis unfolding content_def unfolding if_not_P[OF False] ``` hoelzl@37489 ` 1967` ``` proof(cases "\i. a \$ i \ b \$ i") ``` hoelzl@37489 ` 1968` ``` case False thus ?thesis unfolding content_def using t by auto ``` hoelzl@37489 ` 1969` ``` next case True note interval_eq_empty ``` hoelzl@37489 ` 1970` ``` apply auto ``` hoelzl@37489 ` 1971` ``` ``` hoelzl@37489 ` 1972` ``` sorry*) ``` hoelzl@37489 ` 1973` hoelzl@37489 ` 1974` ```lemma integral_component_eq_cart[simp]: fixes f::"'n::ordered_euclidean_space \ real^'m" ``` hoelzl@37489 ` 1975` ``` assumes "f integrable_on s" shows "integral s (\x. f x \$ k) = integral s f \$ k" ``` hoelzl@37489 ` 1976` ``` using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] . ``` hoelzl@37489 ` 1977` hoelzl@37489 ` 1978` ```lemma interval_split_cart: ``` hoelzl@37489 ` 1979` ``` "{a..b::real^'n} \ {x. x\$k \ c} = {a .. (\ i. if i = k then min (b\$k) c else b\$i)}" ``` hoelzl@37489 ` 1980` ``` "{a..b} \ {x. x\$k \ c} = {(\ i. if i = k then max (a\$k) c else a\$i) .. b}" ``` nipkow@39302 ` 1981` ``` apply(rule_tac[!] set_eqI) unfolding Int_iff mem_interval_cart mem_Collect_eq ``` huffman@44136 ` 1982` ``` unfolding vec_lambda_beta by auto ``` hoelzl@37489 ` 1983` hoelzl@37489 ` 1984` ```(*lemma content_split_cart: ``` hoelzl@37489 ` 1985` ``` "content {a..b::real^'n} = content({a..b} \ {x. x\$k \ c}) + content({a..b} \ {x. x\$k >= c})" ``` huffman@44136 ` 1986` ```proof- note simps = interval_split_cart content_closed_interval_cases_cart vec_lambda_beta less_eq_vec_def ``` hoelzl@37489 ` 1987` ``` { presume "a\b \ ?thesis" thus ?thesis apply(cases "a\b") unfolding simps by auto } ``` hoelzl@37489 ` 1988` ``` have *:"UNIV = insert k (UNIV - {k})" "\x. finite (UNIV-{x::'n})" "\x. x\UNIV-{x}" by auto ``` hoelzl@37489 ` 1989` ``` have *:"\X Y Z. (\i\UNIV. Z i (if i = k then X else Y i)) = Z k X * (\i\UNIV-{k}. Z i (Y i))" ``` hoelzl@37489 ` 1990` ``` "(\i\UNIV. b\$i - a\$i) = (\i\UNIV-{k}. b\$i - a\$i) * (b\$k - a\$k)" ``` hoelzl@37489 ` 1991` ``` apply(subst *(1)) defer apply(subst *(1)) unfolding setprod_insert[OF *(2-)] by auto ``` hoelzl@37489 ` 1992` ``` assume as:"a\b" moreover have "\x. min (b \$ k) c = max (a \$ k) c ``` hoelzl@37489 ` 1993` ``` \ x* (b\$k - a\$k) = x*(max (a \$ k) c - a \$ k) + x*(b \$ k - max (a \$ k) c)" ``` hoelzl@37489 ` 1994` ``` by (auto simp add:field_simps) ``` hoelzl@37489 ` 1995` ``` moreover have "\ a \$ k \ c \ \ c \ b \$ k \ False" ``` huffman@44136 ` 1996` ``` unfolding not_le using as[unfolded less_eq_vec_def,rule_format,of k] by auto ``` hoelzl@37489 ` 1997` ``` ultimately show ?thesis ``` hoelzl@37489 ` 1998` ``` unfolding simps unfolding *(1)[of "\i x. b\$i - x"] *(1)[of "\i x. x - a\$i"] *(2) by(auto) ``` hoelzl@37489 ` 1999` ```qed*) ``` hoelzl@37489 ` 2000` hoelzl@37489 ` 2001` ```lemma has_integral_vec1: assumes "(f has_integral k) {a..b}" ``` hoelzl@37489 ` 2002` ``` shows "((\x. vec1 (f x)) has_integral (vec1 k)) {a..b}" ``` hoelzl@37489 ` 2003` ```proof- have *:"\p. (\(x, k)\p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\(x, k)\p. content k *\<^sub>R f x) - k)" ``` huffman@44136 ` 2004` ``` unfolding vec_sub vec_eq_iff by(auto simp add: split_beta) ``` hoelzl@37489 ` 2005` ``` show ?thesis using assms unfolding has_integral apply safe ``` hoelzl@37489 ` 2006` ``` apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe) ``` hoelzl@37489 ` 2007` ``` apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed ``` hoelzl@37489 ` 2008` hoelzl@37489 ` 2009` ```end ```