src/HOL/Library/Euclidean_Space.thy
 author wenzelm Mon Mar 16 18:24:30 2009 +0100 (2009-03-16) changeset 30549 d2d7874648bd parent 30510 4120fc59dd85 child 30582 638b088bb840 permissions -rw-r--r--
simplified method setup;
 chaieb@29842 ` 1` ```(* Title: Library/Euclidean_Space ``` chaieb@29842 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` chaieb@29842 ` 3` ```*) ``` chaieb@29842 ` 4` chaieb@29842 ` 5` ```header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*} ``` chaieb@29842 ` 6` chaieb@29842 ` 7` ```theory Euclidean_Space ``` huffman@30489 ` 8` ``` imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main ``` chaieb@29842 ` 9` ``` Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type ``` huffman@30045 ` 10` ``` Inner_Product ``` chaieb@29842 ` 11` ``` uses ("normarith.ML") ``` chaieb@29842 ` 12` ```begin ``` chaieb@29842 ` 13` chaieb@29842 ` 14` ```text{* Some common special cases.*} ``` chaieb@29842 ` 15` chaieb@29842 ` 16` ```lemma forall_1: "(\(i::'a::{order,one}). 1 <= i \ i <= 1 --> P i) \ P 1" ``` chaieb@29842 ` 17` ``` by (metis order_eq_iff) ``` chaieb@29842 ` 18` ```lemma forall_dimindex_1: "(\i \ {1..dimindex(UNIV:: 1 set)}. P i) \ P 1" ``` chaieb@29842 ` 19` ``` by (simp add: dimindex_def) ``` chaieb@29842 ` 20` chaieb@29842 ` 21` ```lemma forall_2: "(\(i::nat). 1 <= i \ i <= 2 --> P i) \ P 1 \ P 2" ``` chaieb@29842 ` 22` ```proof- ``` chaieb@29842 ` 23` ``` have "\i::nat. 1 <= i \ i <= 2 \ i = 1 \ i = 2" by arith ``` chaieb@29842 ` 24` ``` thus ?thesis by metis ``` chaieb@29842 ` 25` ```qed ``` chaieb@29842 ` 26` chaieb@29842 ` 27` ```lemma forall_3: "(\(i::nat). 1 <= i \ i <= 3 --> P i) \ P 1 \ P 2 \ P 3" ``` chaieb@29842 ` 28` ```proof- ``` chaieb@29842 ` 29` ``` have "\i::nat. 1 <= i \ i <= 3 \ i = 1 \ i = 2 \ i = 3" by arith ``` chaieb@29842 ` 30` ``` thus ?thesis by metis ``` chaieb@29842 ` 31` ```qed ``` chaieb@29842 ` 32` chaieb@29842 ` 33` ```lemma setsum_singleton[simp]: "setsum f {x} = f x" by simp ``` huffman@30489 ` 34` ```lemma setsum_1: "setsum f {(1::'a::{order,one})..1} = f 1" ``` chaieb@29842 ` 35` ``` by (simp add: atLeastAtMost_singleton) ``` chaieb@29842 ` 36` huffman@30489 ` 37` ```lemma setsum_2: "setsum f {1::nat..2} = f 1 + f 2" ``` chaieb@29842 ` 38` ``` by (simp add: nat_number atLeastAtMostSuc_conv add_commute) ``` chaieb@29842 ` 39` huffman@30489 ` 40` ```lemma setsum_3: "setsum f {1::nat..3} = f 1 + f 2 + f 3" ``` chaieb@29842 ` 41` ``` by (simp add: nat_number atLeastAtMostSuc_conv add_commute) ``` chaieb@29842 ` 42` huffman@29906 ` 43` ```subsection{* Basic componentwise operations on vectors. *} ``` chaieb@29842 ` 44` chaieb@29842 ` 45` ```instantiation "^" :: (plus,type) plus ``` chaieb@29842 ` 46` ```begin ``` huffman@30489 ` 47` ```definition vector_add_def : "op + \ (\ x y. (\ i. (x\$i) + (y\$i)))" ``` chaieb@29842 ` 48` ```instance .. ``` chaieb@29842 ` 49` ```end ``` chaieb@29842 ` 50` chaieb@29842 ` 51` ```instantiation "^" :: (times,type) times ``` chaieb@29842 ` 52` ```begin ``` huffman@30489 ` 53` ``` definition vector_mult_def : "op * \ (\ x y. (\ i. (x\$i) * (y\$i)))" ``` chaieb@29842 ` 54` ``` instance .. ``` chaieb@29842 ` 55` ```end ``` chaieb@29842 ` 56` chaieb@29842 ` 57` ```instantiation "^" :: (minus,type) minus begin ``` chaieb@29842 ` 58` ``` definition vector_minus_def : "op - \ (\ x y. (\ i. (x\$i) - (y\$i)))" ``` chaieb@29842 ` 59` ```instance .. ``` chaieb@29842 ` 60` ```end ``` chaieb@29842 ` 61` chaieb@29842 ` 62` ```instantiation "^" :: (uminus,type) uminus begin ``` chaieb@29842 ` 63` ``` definition vector_uminus_def : "uminus \ (\ x. (\ i. - (x\$i)))" ``` chaieb@29842 ` 64` ```instance .. ``` chaieb@29842 ` 65` ```end ``` chaieb@29842 ` 66` ```instantiation "^" :: (zero,type) zero begin ``` huffman@30489 ` 67` ``` definition vector_zero_def : "0 \ (\ i. 0)" ``` chaieb@29842 ` 68` ```instance .. ``` chaieb@29842 ` 69` ```end ``` chaieb@29842 ` 70` chaieb@29842 ` 71` ```instantiation "^" :: (one,type) one begin ``` huffman@30489 ` 72` ``` definition vector_one_def : "1 \ (\ i. 1)" ``` chaieb@29842 ` 73` ```instance .. ``` chaieb@29842 ` 74` ```end ``` chaieb@29842 ` 75` chaieb@29842 ` 76` ```instantiation "^" :: (ord,type) ord ``` chaieb@29842 ` 77` ``` begin ``` chaieb@29842 ` 78` ```definition vector_less_eq_def: ``` chaieb@29842 ` 79` ``` "less_eq (x :: 'a ^'b) y = (ALL i : {1 .. dimindex (UNIV :: 'b set)}. ``` chaieb@29842 ` 80` ``` x\$i <= y\$i)" ``` chaieb@29842 ` 81` ```definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i : {1 .. ``` chaieb@29842 ` 82` ``` dimindex (UNIV :: 'b set)}. x\$i < y\$i)" ``` huffman@30489 ` 83` chaieb@29842 ` 84` ```instance by (intro_classes) ``` chaieb@29842 ` 85` ```end ``` chaieb@29842 ` 86` huffman@30039 ` 87` ```instantiation "^" :: (scaleR, type) scaleR ``` huffman@30039 ` 88` ```begin ``` huffman@30489 ` 89` ```definition vector_scaleR_def: "scaleR = (\ r x. (\ i. scaleR r (x\$i)))" ``` huffman@30039 ` 90` ```instance .. ``` huffman@30039 ` 91` ```end ``` huffman@30039 ` 92` huffman@30039 ` 93` ```text{* Also the scalar-vector multiplication. *} ``` chaieb@29842 ` 94` chaieb@29842 ` 95` ```definition vector_scalar_mult:: "'a::times \ 'a ^'n \ 'a ^ 'n" (infixr "*s" 75) ``` chaieb@29842 ` 96` ``` where "c *s x = (\ i. c * (x\$i))" ``` chaieb@29842 ` 97` chaieb@29842 ` 98` ```text{* Constant Vectors *} ``` chaieb@29842 ` 99` chaieb@29842 ` 100` ```definition "vec x = (\ i. x)" ``` chaieb@29842 ` 101` chaieb@29842 ` 102` ```text{* Dot products. *} ``` chaieb@29842 ` 103` chaieb@29842 ` 104` ```definition dot :: "'a::{comm_monoid_add, times} ^ 'n \ 'a ^ 'n \ 'a" (infix "\" 70) where ``` chaieb@29842 ` 105` ``` "x \ y = setsum (\i. x\$i * y\$i) {1 .. dimindex (UNIV:: 'n set)}" ``` chaieb@29842 ` 106` ```lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \ y = (x\$1) * (y\$1)" ``` chaieb@29842 ` 107` ``` by (simp add: dot_def dimindex_def) ``` chaieb@29842 ` 108` chaieb@29842 ` 109` ```lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \ y = (x\$1) * (y\$1) + (x\$2) * (y\$2)" ``` chaieb@29842 ` 110` ``` by (simp add: dot_def dimindex_def nat_number) ``` chaieb@29842 ` 111` chaieb@29842 ` 112` ```lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \ y = (x\$1) * (y\$1) + (x\$2) * (y\$2) + (x\$3) * (y\$3)" ``` chaieb@29842 ` 113` ``` by (simp add: dot_def dimindex_def nat_number) ``` chaieb@29842 ` 114` huffman@29906 ` 115` ```subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} ``` chaieb@29842 ` 116` chaieb@29842 ` 117` ```lemmas Cart_lambda_beta' = Cart_lambda_beta[rule_format] ``` chaieb@29842 ` 118` ```method_setup vector = {* ``` chaieb@29842 ` 119` ```let ``` huffman@30489 ` 120` ``` val ss1 = HOL_basic_ss addsimps [@{thm dot_def}, @{thm setsum_addf} RS sym, ``` huffman@30489 ` 121` ``` @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, ``` chaieb@29842 ` 122` ``` @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym] ``` huffman@30489 ` 123` ``` val ss2 = @{simpset} addsimps ``` huffman@30489 ` 124` ``` [@{thm vector_add_def}, @{thm vector_mult_def}, ``` huffman@30489 ` 125` ``` @{thm vector_minus_def}, @{thm vector_uminus_def}, ``` huffman@30489 ` 126` ``` @{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def}, ``` huffman@30039 ` 127` ``` @{thm vector_scaleR_def}, ``` chaieb@29842 ` 128` ``` @{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}] ``` huffman@30489 ` 129` ``` fun vector_arith_tac ths = ``` chaieb@29842 ` 130` ``` simp_tac ss1 ``` chaieb@29842 ` 131` ``` THEN' (fn i => rtac @{thm setsum_cong2} i ``` huffman@30489 ` 132` ``` ORELSE rtac @{thm setsum_0'} i ``` chaieb@29842 ` 133` ``` ORELSE simp_tac (HOL_basic_ss addsimps [@{thm "Cart_eq"}]) i) ``` chaieb@29842 ` 134` ``` (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) ``` chaieb@29842 ` 135` ``` THEN' asm_full_simp_tac (ss2 addsimps ths) ``` chaieb@29842 ` 136` ``` in ``` wenzelm@30549 ` 137` ``` Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths))) ``` wenzelm@30549 ` 138` ``` end ``` chaieb@29842 ` 139` ```*} "Lifts trivial vector statements to real arith statements" ``` chaieb@29842 ` 140` chaieb@29842 ` 141` ```lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def) ``` chaieb@29842 ` 142` ```lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def) ``` chaieb@29842 ` 143` chaieb@29842 ` 144` chaieb@29842 ` 145` chaieb@29842 ` 146` ```text{* Obvious "component-pushing". *} ``` chaieb@29842 ` 147` huffman@30489 ` 148` ```lemma vec_component: " i \ {1 .. dimindex (UNIV :: 'n set)} \ (vec x :: 'a ^ 'n)\$i = x" ``` huffman@30489 ` 149` ``` by (vector vec_def) ``` huffman@30489 ` 150` huffman@30489 ` 151` ```lemma vector_add_component: ``` chaieb@29842 ` 152` ``` fixes x y :: "'a::{plus} ^ 'n" assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" ``` chaieb@29842 ` 153` ``` shows "(x + y)\$i = x\$i + y\$i" ``` chaieb@29842 ` 154` ``` using i by vector ``` chaieb@29842 ` 155` huffman@30489 ` 156` ```lemma vector_minus_component: ``` chaieb@29842 ` 157` ``` fixes x y :: "'a::{minus} ^ 'n" assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" ``` chaieb@29842 ` 158` ``` shows "(x - y)\$i = x\$i - y\$i" ``` chaieb@29842 ` 159` ``` using i by vector ``` chaieb@29842 ` 160` huffman@30489 ` 161` ```lemma vector_mult_component: ``` chaieb@29842 ` 162` ``` fixes x y :: "'a::{times} ^ 'n" assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" ``` chaieb@29842 ` 163` ``` shows "(x * y)\$i = x\$i * y\$i" ``` chaieb@29842 ` 164` ``` using i by vector ``` chaieb@29842 ` 165` huffman@30489 ` 166` ```lemma vector_smult_component: ``` chaieb@29842 ` 167` ``` fixes y :: "'a::{times} ^ 'n" assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" ``` chaieb@29842 ` 168` ``` shows "(c *s y)\$i = c * (y\$i)" ``` chaieb@29842 ` 169` ``` using i by vector ``` chaieb@29842 ` 170` huffman@30489 ` 171` ```lemma vector_uminus_component: ``` chaieb@29842 ` 172` ``` fixes x :: "'a::{uminus} ^ 'n" assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" ``` chaieb@29842 ` 173` ``` shows "(- x)\$i = - (x\$i)" ``` chaieb@29842 ` 174` ``` using i by vector ``` chaieb@29842 ` 175` huffman@30039 ` 176` ```lemma vector_scaleR_component: ``` huffman@30039 ` 177` ``` fixes x :: "'a::scaleR ^ 'n" ``` huffman@30039 ` 178` ``` assumes i: "i \ {1 .. dimindex(UNIV :: 'n set)}" ``` huffman@30039 ` 179` ``` shows "(scaleR r x)\$i = scaleR r (x\$i)" ``` huffman@30039 ` 180` ``` using i by vector ``` huffman@30039 ` 181` chaieb@29842 ` 182` ```lemma cond_component: "(if b then x else y)\$i = (if b then x\$i else y\$i)" by vector ``` chaieb@29842 ` 183` huffman@30039 ` 184` ```lemmas vector_component = ``` huffman@30039 ` 185` ``` vec_component vector_add_component vector_mult_component ``` huffman@30039 ` 186` ``` vector_smult_component vector_minus_component vector_uminus_component ``` huffman@30039 ` 187` ``` vector_scaleR_component cond_component ``` chaieb@29842 ` 188` chaieb@29842 ` 189` ```subsection {* Some frequently useful arithmetic lemmas over vectors. *} ``` chaieb@29842 ` 190` huffman@30489 ` 191` ```instance "^" :: (semigroup_add,type) semigroup_add ``` chaieb@29842 ` 192` ``` apply (intro_classes) by (vector add_assoc) ``` chaieb@29842 ` 193` chaieb@29842 ` 194` huffman@30489 ` 195` ```instance "^" :: (monoid_add,type) monoid_add ``` huffman@30489 ` 196` ``` apply (intro_classes) by vector+ ``` huffman@30489 ` 197` huffman@30489 ` 198` ```instance "^" :: (group_add,type) group_add ``` huffman@30489 ` 199` ``` apply (intro_classes) by (vector algebra_simps)+ ``` huffman@30489 ` 200` huffman@30489 ` 201` ```instance "^" :: (ab_semigroup_add,type) ab_semigroup_add ``` chaieb@29842 ` 202` ``` apply (intro_classes) by (vector add_commute) ``` chaieb@29842 ` 203` chaieb@29842 ` 204` ```instance "^" :: (comm_monoid_add,type) comm_monoid_add ``` chaieb@29842 ` 205` ``` apply (intro_classes) by vector ``` chaieb@29842 ` 206` huffman@30489 ` 207` ```instance "^" :: (ab_group_add,type) ab_group_add ``` chaieb@29842 ` 208` ``` apply (intro_classes) by vector+ ``` chaieb@29842 ` 209` huffman@30489 ` 210` ```instance "^" :: (cancel_semigroup_add,type) cancel_semigroup_add ``` chaieb@29842 ` 211` ``` apply (intro_classes) ``` chaieb@29842 ` 212` ``` by (vector Cart_eq)+ ``` chaieb@29842 ` 213` chaieb@29842 ` 214` ```instance "^" :: (cancel_ab_semigroup_add,type) cancel_ab_semigroup_add ``` chaieb@29842 ` 215` ``` apply (intro_classes) ``` chaieb@29842 ` 216` ``` by (vector Cart_eq) ``` chaieb@29842 ` 217` huffman@30039 ` 218` ```instance "^" :: (real_vector, type) real_vector ``` huffman@30039 ` 219` ``` by default (vector scaleR_left_distrib scaleR_right_distrib)+ ``` huffman@30039 ` 220` huffman@30489 ` 221` ```instance "^" :: (semigroup_mult,type) semigroup_mult ``` chaieb@29842 ` 222` ``` apply (intro_classes) by (vector mult_assoc) ``` chaieb@29842 ` 223` huffman@30489 ` 224` ```instance "^" :: (monoid_mult,type) monoid_mult ``` chaieb@29842 ` 225` ``` apply (intro_classes) by vector+ ``` chaieb@29842 ` 226` huffman@30489 ` 227` ```instance "^" :: (ab_semigroup_mult,type) ab_semigroup_mult ``` chaieb@29842 ` 228` ``` apply (intro_classes) by (vector mult_commute) ``` chaieb@29842 ` 229` huffman@30489 ` 230` ```instance "^" :: (ab_semigroup_idem_mult,type) ab_semigroup_idem_mult ``` chaieb@29842 ` 231` ``` apply (intro_classes) by (vector mult_idem) ``` chaieb@29842 ` 232` huffman@30489 ` 233` ```instance "^" :: (comm_monoid_mult,type) comm_monoid_mult ``` chaieb@29842 ` 234` ``` apply (intro_classes) by vector ``` chaieb@29842 ` 235` chaieb@29842 ` 236` ```fun vector_power :: "('a::{one,times} ^'n) \ nat \ 'a^'n" where ``` chaieb@29842 ` 237` ``` "vector_power x 0 = 1" ``` chaieb@29842 ` 238` ``` | "vector_power x (Suc n) = x * vector_power x n" ``` chaieb@29842 ` 239` huffman@30489 ` 240` ```instantiation "^" :: (recpower,type) recpower ``` chaieb@29842 ` 241` ```begin ``` chaieb@29842 ` 242` ``` definition vec_power_def: "op ^ \ vector_power" ``` huffman@30489 ` 243` ``` instance ``` huffman@30489 ` 244` ``` apply (intro_classes) by (simp_all add: vec_power_def) ``` chaieb@29842 ` 245` ```end ``` chaieb@29842 ` 246` chaieb@29842 ` 247` ```instance "^" :: (semiring,type) semiring ``` chaieb@29842 ` 248` ``` apply (intro_classes) by (vector ring_simps)+ ``` chaieb@29842 ` 249` chaieb@29842 ` 250` ```instance "^" :: (semiring_0,type) semiring_0 ``` chaieb@29842 ` 251` ``` apply (intro_classes) by (vector ring_simps)+ ``` chaieb@29842 ` 252` ```instance "^" :: (semiring_1,type) semiring_1 ``` huffman@30489 ` 253` ``` apply (intro_classes) apply vector using dimindex_ge_1 by auto ``` chaieb@29842 ` 254` ```instance "^" :: (comm_semiring,type) comm_semiring ``` chaieb@29842 ` 255` ``` apply (intro_classes) by (vector ring_simps)+ ``` chaieb@29842 ` 256` huffman@30489 ` 257` ```instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes) ``` huffman@29905 ` 258` ```instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add .. ``` huffman@30489 ` 259` ```instance "^" :: (semiring_0_cancel,type) semiring_0_cancel by (intro_classes) ``` huffman@30489 ` 260` ```instance "^" :: (comm_semiring_0_cancel,type) comm_semiring_0_cancel by (intro_classes) ``` huffman@30489 ` 261` ```instance "^" :: (ring,type) ring by (intro_classes) ``` huffman@30489 ` 262` ```instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes) ``` chaieb@29842 ` 263` ```instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes) ``` huffman@30039 ` 264` huffman@30039 ` 265` ```instance "^" :: (ring_1,type) ring_1 .. ``` huffman@30039 ` 266` huffman@30039 ` 267` ```instance "^" :: (real_algebra,type) real_algebra ``` huffman@30039 ` 268` ``` apply intro_classes ``` huffman@30039 ` 269` ``` apply (simp_all add: vector_scaleR_def ring_simps) ``` huffman@30039 ` 270` ``` apply vector ``` huffman@30039 ` 271` ``` apply vector ``` huffman@30039 ` 272` ``` done ``` huffman@30039 ` 273` huffman@30039 ` 274` ```instance "^" :: (real_algebra_1,type) real_algebra_1 .. ``` huffman@30039 ` 275` huffman@30489 ` 276` ```lemma of_nat_index: ``` chaieb@29842 ` 277` ``` "i\{1 .. dimindex (UNIV :: 'n set)} \ (of_nat n :: 'a::semiring_1 ^'n)\$i = of_nat n" ``` chaieb@29842 ` 278` ``` apply (induct n) ``` chaieb@29842 ` 279` ``` apply vector ``` chaieb@29842 ` 280` ``` apply vector ``` chaieb@29842 ` 281` ``` done ``` huffman@30489 ` 282` ```lemma zero_index[simp]: ``` chaieb@29842 ` 283` ``` "i\{1 .. dimindex (UNIV :: 'n set)} \ (0 :: 'a::zero ^'n)\$i = 0" by vector ``` chaieb@29842 ` 284` huffman@30489 ` 285` ```lemma one_index[simp]: ``` chaieb@29842 ` 286` ``` "i\{1 .. dimindex (UNIV :: 'n set)} \ (1 :: 'a::one ^'n)\$i = 1" by vector ``` chaieb@29842 ` 287` chaieb@29842 ` 288` ```lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \ 0" ``` chaieb@29842 ` 289` ```proof- ``` chaieb@29842 ` 290` ``` have "(1::'a) + of_nat n = 0 \ of_nat 1 + of_nat n = (of_nat 0 :: 'a)" by simp ``` huffman@30489 ` 291` ``` also have "\ \ 1 + n = 0" by (simp only: of_nat_add[symmetric] of_nat_eq_iff) ``` huffman@30489 ` 292` ``` finally show ?thesis by simp ``` chaieb@29842 ` 293` ```qed ``` chaieb@29842 ` 294` huffman@30489 ` 295` ```instance "^" :: (semiring_char_0,type) semiring_char_0 ``` huffman@30489 ` 296` ```proof (intro_classes) ``` chaieb@29842 ` 297` ``` fix m n ::nat ``` chaieb@29842 ` 298` ``` show "(of_nat m :: 'a^'b) = of_nat n \ m = n" ``` chaieb@29842 ` 299` ``` proof(induct m arbitrary: n) ``` huffman@30489 ` 300` ``` case 0 thus ?case apply vector ``` chaieb@29842 ` 301` ``` apply (induct n,auto simp add: ring_simps) ``` chaieb@29842 ` 302` ``` using dimindex_ge_1 apply auto ``` chaieb@29842 ` 303` ``` apply vector ``` chaieb@29842 ` 304` ``` by (auto simp add: of_nat_index one_plus_of_nat_neq_0) ``` chaieb@29842 ` 305` ``` next ``` chaieb@29842 ` 306` ``` case (Suc n m) ``` chaieb@29842 ` 307` ``` thus ?case apply vector ``` chaieb@29842 ` 308` ``` apply (induct m, auto simp add: ring_simps of_nat_index zero_index) ``` chaieb@29842 ` 309` ``` using dimindex_ge_1 apply simp apply blast ``` chaieb@29842 ` 310` ``` apply (simp add: one_plus_of_nat_neq_0) ``` chaieb@29842 ` 311` ``` using dimindex_ge_1 apply simp apply blast ``` chaieb@29842 ` 312` ``` apply (simp add: vector_component one_index of_nat_index) ``` chaieb@29842 ` 313` ``` apply (simp only: of_nat.simps(2)[where ?'a = 'a, symmetric] of_nat_eq_iff) ``` chaieb@29842 ` 314` ``` using dimindex_ge_1 apply simp apply blast ``` chaieb@29842 ` 315` ``` apply (simp add: vector_component one_index of_nat_index) ``` chaieb@29842 ` 316` ``` apply (simp only: of_nat.simps(2)[where ?'a = 'a, symmetric] of_nat_eq_iff) ``` chaieb@29842 ` 317` ``` using dimindex_ge_1 apply simp apply blast ``` chaieb@29842 ` 318` ``` apply (simp add: vector_component one_index of_nat_index) ``` chaieb@29842 ` 319` ``` done ``` chaieb@29842 ` 320` ``` qed ``` chaieb@29842 ` 321` ```qed ``` chaieb@29842 ` 322` chaieb@29842 ` 323` ```instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes ``` huffman@30039 ` 324` ```instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes ``` chaieb@29842 ` 325` huffman@30489 ` 326` ```lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" ``` chaieb@29842 ` 327` ``` by (vector mult_assoc) ``` huffman@30489 ` 328` ```lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x" ``` chaieb@29842 ` 329` ``` by (vector ring_simps) ``` huffman@30489 ` 330` ```lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y" ``` chaieb@29842 ` 331` ``` by (vector ring_simps) ``` chaieb@29842 ` 332` ```lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector ``` chaieb@29842 ` 333` ```lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector ``` huffman@30489 ` 334` ```lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y" ``` chaieb@29842 ` 335` ``` by (vector ring_simps) ``` chaieb@29842 ` 336` ```lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector ``` chaieb@29842 ` 337` ```lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector ``` chaieb@29842 ` 338` ```lemma vector_sneg_minus1: "-x = (- (1::'a::ring_1)) *s x" by vector ``` chaieb@29842 ` 339` ```lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector ``` huffman@30489 ` 340` ```lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x" ``` chaieb@29842 ` 341` ``` by (vector ring_simps) ``` chaieb@29842 ` 342` huffman@30489 ` 343` ```lemma vec_eq[simp]: "(vec m = vec n) \ (m = n)" ``` chaieb@29842 ` 344` ``` apply (auto simp add: vec_def Cart_eq vec_component Cart_lambda_beta ) ``` chaieb@29842 ` 345` ``` using dimindex_ge_1 apply auto done ``` chaieb@29842 ` 346` huffman@30040 ` 347` ```subsection {* Square root of sum of squares *} ``` huffman@30040 ` 348` huffman@30040 ` 349` ```definition ``` huffman@30040 ` 350` ``` "setL2 f A = sqrt (\i\A. (f i)\)" ``` huffman@30040 ` 351` huffman@30040 ` 352` ```lemma setL2_cong: ``` huffman@30040 ` 353` ``` "\A = B; \x. x \ B \ f x = g x\ \ setL2 f A = setL2 g B" ``` huffman@30040 ` 354` ``` unfolding setL2_def by simp ``` huffman@30040 ` 355` huffman@30040 ` 356` ```lemma strong_setL2_cong: ``` huffman@30040 ` 357` ``` "\A = B; \x. x \ B =simp=> f x = g x\ \ setL2 f A = setL2 g B" ``` huffman@30040 ` 358` ``` unfolding setL2_def simp_implies_def by simp ``` huffman@30040 ` 359` huffman@30040 ` 360` ```lemma setL2_infinite [simp]: "\ finite A \ setL2 f A = 0" ``` huffman@30040 ` 361` ``` unfolding setL2_def by simp ``` huffman@30040 ` 362` huffman@30040 ` 363` ```lemma setL2_empty [simp]: "setL2 f {} = 0" ``` huffman@30040 ` 364` ``` unfolding setL2_def by simp ``` huffman@30040 ` 365` huffman@30040 ` 366` ```lemma setL2_insert [simp]: ``` huffman@30040 ` 367` ``` "\finite F; a \ F\ \ ``` huffman@30040 ` 368` ``` setL2 f (insert a F) = sqrt ((f a)\ + (setL2 f F)\)" ``` huffman@30040 ` 369` ``` unfolding setL2_def by (simp add: setsum_nonneg) ``` huffman@30040 ` 370` huffman@30040 ` 371` ```lemma setL2_nonneg [simp]: "0 \ setL2 f A" ``` huffman@30040 ` 372` ``` unfolding setL2_def by (simp add: setsum_nonneg) ``` huffman@30040 ` 373` huffman@30040 ` 374` ```lemma setL2_0': "\a\A. f a = 0 \ setL2 f A = 0" ``` huffman@30040 ` 375` ``` unfolding setL2_def by simp ``` huffman@30040 ` 376` huffman@30040 ` 377` ```lemma setL2_mono: ``` huffman@30040 ` 378` ``` assumes "\i. i \ K \ f i \ g i" ``` huffman@30040 ` 379` ``` assumes "\i. i \ K \ 0 \ f i" ``` huffman@30040 ` 380` ``` shows "setL2 f K \ setL2 g K" ``` huffman@30040 ` 381` ``` unfolding setL2_def ``` huffman@30040 ` 382` ``` by (simp add: setsum_nonneg setsum_mono power_mono prems) ``` huffman@30040 ` 383` huffman@30040 ` 384` ```lemma setL2_right_distrib: ``` huffman@30040 ` 385` ``` "0 \ r \ r * setL2 f A = setL2 (\x. r * f x) A" ``` huffman@30040 ` 386` ``` unfolding setL2_def ``` huffman@30040 ` 387` ``` apply (simp add: power_mult_distrib) ``` huffman@30040 ` 388` ``` apply (simp add: setsum_right_distrib [symmetric]) ``` huffman@30040 ` 389` ``` apply (simp add: real_sqrt_mult setsum_nonneg) ``` huffman@30040 ` 390` ``` done ``` huffman@30040 ` 391` huffman@30040 ` 392` ```lemma setL2_left_distrib: ``` huffman@30040 ` 393` ``` "0 \ r \ setL2 f A * r = setL2 (\x. f x * r) A" ``` huffman@30040 ` 394` ``` unfolding setL2_def ``` huffman@30040 ` 395` ``` apply (simp add: power_mult_distrib) ``` huffman@30040 ` 396` ``` apply (simp add: setsum_left_distrib [symmetric]) ``` huffman@30040 ` 397` ``` apply (simp add: real_sqrt_mult setsum_nonneg) ``` huffman@30040 ` 398` ``` done ``` huffman@30040 ` 399` huffman@30040 ` 400` ```lemma setsum_nonneg_eq_0_iff: ``` huffman@30040 ` 401` ``` fixes f :: "'a \ 'b::pordered_ab_group_add" ``` huffman@30040 ` 402` ``` shows "\finite A; \x\A. 0 \ f x\ \ setsum f A = 0 \ (\x\A. f x = 0)" ``` huffman@30040 ` 403` ``` apply (induct set: finite, simp) ``` huffman@30040 ` 404` ``` apply (simp add: add_nonneg_eq_0_iff setsum_nonneg) ``` huffman@30040 ` 405` ``` done ``` huffman@30040 ` 406` huffman@30040 ` 407` ```lemma setL2_eq_0_iff: "finite A \ setL2 f A = 0 \ (\x\A. f x = 0)" ``` huffman@30040 ` 408` ``` unfolding setL2_def ``` huffman@30040 ` 409` ``` by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff) ``` huffman@30040 ` 410` huffman@30040 ` 411` ```lemma setL2_triangle_ineq: ``` huffman@30040 ` 412` ``` shows "setL2 (\i. f i + g i) A \ setL2 f A + setL2 g A" ``` huffman@30040 ` 413` ```proof (cases "finite A") ``` huffman@30040 ` 414` ``` case False ``` huffman@30040 ` 415` ``` thus ?thesis by simp ``` huffman@30040 ` 416` ```next ``` huffman@30040 ` 417` ``` case True ``` huffman@30040 ` 418` ``` thus ?thesis ``` huffman@30040 ` 419` ``` proof (induct set: finite) ``` huffman@30040 ` 420` ``` case empty ``` huffman@30040 ` 421` ``` show ?case by simp ``` huffman@30040 ` 422` ``` next ``` huffman@30040 ` 423` ``` case (insert x F) ``` huffman@30040 ` 424` ``` hence "sqrt ((f x + g x)\ + (setL2 (\i. f i + g i) F)\) \ ``` huffman@30040 ` 425` ``` sqrt ((f x + g x)\ + (setL2 f F + setL2 g F)\)" ``` huffman@30040 ` 426` ``` by (intro real_sqrt_le_mono add_left_mono power_mono insert ``` huffman@30040 ` 427` ``` setL2_nonneg add_increasing zero_le_power2) ``` huffman@30040 ` 428` ``` also have ``` huffman@30040 ` 429` ``` "\ \ sqrt ((f x)\ + (setL2 f F)\) + sqrt ((g x)\ + (setL2 g F)\)" ``` huffman@30040 ` 430` ``` by (rule real_sqrt_sum_squares_triangle_ineq) ``` huffman@30040 ` 431` ``` finally show ?case ``` huffman@30040 ` 432` ``` using insert by simp ``` huffman@30040 ` 433` ``` qed ``` huffman@30040 ` 434` ```qed ``` huffman@30040 ` 435` huffman@30040 ` 436` ```lemma sqrt_sum_squares_le_sum: ``` huffman@30040 ` 437` ``` "\0 \ x; 0 \ y\ \ sqrt (x\ + y\) \ x + y" ``` huffman@30040 ` 438` ``` apply (rule power2_le_imp_le) ``` huffman@30040 ` 439` ``` apply (simp add: power2_sum) ``` huffman@30040 ` 440` ``` apply (simp add: mult_nonneg_nonneg) ``` huffman@30040 ` 441` ``` apply (simp add: add_nonneg_nonneg) ``` huffman@30040 ` 442` ``` done ``` huffman@30040 ` 443` huffman@30040 ` 444` ```lemma setL2_le_setsum [rule_format]: ``` huffman@30040 ` 445` ``` "(\i\A. 0 \ f i) \ setL2 f A \ setsum f A" ``` huffman@30040 ` 446` ``` apply (cases "finite A") ``` huffman@30040 ` 447` ``` apply (induct set: finite) ``` huffman@30040 ` 448` ``` apply simp ``` huffman@30040 ` 449` ``` apply clarsimp ``` huffman@30040 ` 450` ``` apply (erule order_trans [OF sqrt_sum_squares_le_sum]) ``` huffman@30040 ` 451` ``` apply simp ``` huffman@30040 ` 452` ``` apply simp ``` huffman@30040 ` 453` ``` apply simp ``` huffman@30040 ` 454` ``` done ``` huffman@30040 ` 455` huffman@30040 ` 456` ```lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\ + y\) \ \x\ + \y\" ``` huffman@30040 ` 457` ``` apply (rule power2_le_imp_le) ``` huffman@30040 ` 458` ``` apply (simp add: power2_sum) ``` huffman@30040 ` 459` ``` apply (simp add: mult_nonneg_nonneg) ``` huffman@30040 ` 460` ``` apply (simp add: add_nonneg_nonneg) ``` huffman@30040 ` 461` ``` done ``` huffman@30040 ` 462` huffman@30040 ` 463` ```lemma setL2_le_setsum_abs: "setL2 f A \ (\i\A. \f i\)" ``` huffman@30040 ` 464` ``` apply (cases "finite A") ``` huffman@30040 ` 465` ``` apply (induct set: finite) ``` huffman@30040 ` 466` ``` apply simp ``` huffman@30040 ` 467` ``` apply simp ``` huffman@30040 ` 468` ``` apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs]) ``` huffman@30040 ` 469` ``` apply simp ``` huffman@30040 ` 470` ``` apply simp ``` huffman@30040 ` 471` ``` done ``` huffman@30040 ` 472` huffman@30040 ` 473` ```lemma setL2_mult_ineq_lemma: ``` huffman@30040 ` 474` ``` fixes a b c d :: real ``` huffman@30040 ` 475` ``` shows "2 * (a * c) * (b * d) \ a\ * d\ + b\ * c\" ``` huffman@30040 ` 476` ```proof - ``` huffman@30040 ` 477` ``` have "0 \ (a * d - b * c)\" by simp ``` huffman@30040 ` 478` ``` also have "\ = a\ * d\ + b\ * c\ - 2 * (a * d) * (b * c)" ``` huffman@30040 ` 479` ``` by (simp only: power2_diff power_mult_distrib) ``` huffman@30040 ` 480` ``` also have "\ = a\ * d\ + b\ * c\ - 2 * (a * c) * (b * d)" ``` huffman@30040 ` 481` ``` by simp ``` huffman@30040 ` 482` ``` finally show "2 * (a * c) * (b * d) \ a\ * d\ + b\ * c\" ``` huffman@30040 ` 483` ``` by simp ``` huffman@30040 ` 484` ```qed ``` huffman@30040 ` 485` huffman@30040 ` 486` ```lemma setL2_mult_ineq: "(\i\A. \f i\ * \g i\) \ setL2 f A * setL2 g A" ``` huffman@30040 ` 487` ``` apply (cases "finite A") ``` huffman@30040 ` 488` ``` apply (induct set: finite) ``` huffman@30040 ` 489` ``` apply simp ``` huffman@30040 ` 490` ``` apply (rule power2_le_imp_le, simp) ``` huffman@30040 ` 491` ``` apply (rule order_trans) ``` huffman@30040 ` 492` ``` apply (rule power_mono) ``` huffman@30040 ` 493` ``` apply (erule add_left_mono) ``` huffman@30040 ` 494` ``` apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg) ``` huffman@30040 ` 495` ``` apply (simp add: power2_sum) ``` huffman@30040 ` 496` ``` apply (simp add: power_mult_distrib) ``` huffman@30040 ` 497` ``` apply (simp add: right_distrib left_distrib) ``` huffman@30040 ` 498` ``` apply (rule ord_le_eq_trans) ``` huffman@30040 ` 499` ``` apply (rule setL2_mult_ineq_lemma) ``` huffman@30040 ` 500` ``` apply simp ``` huffman@30040 ` 501` ``` apply (intro mult_nonneg_nonneg setL2_nonneg) ``` huffman@30040 ` 502` ``` apply simp ``` huffman@30040 ` 503` ``` done ``` huffman@30040 ` 504` huffman@30040 ` 505` ```lemma member_le_setL2: "\finite A; i \ A\ \ f i \ setL2 f A" ``` huffman@30040 ` 506` ``` apply (rule_tac s="insert i (A - {i})" and t="A" in subst) ``` huffman@30040 ` 507` ``` apply fast ``` huffman@30040 ` 508` ``` apply (subst setL2_insert) ``` huffman@30040 ` 509` ``` apply simp ``` huffman@30040 ` 510` ``` apply simp ``` huffman@30040 ` 511` ``` apply simp ``` huffman@30040 ` 512` ``` done ``` huffman@30040 ` 513` huffman@30040 ` 514` ```subsection {* Norms *} ``` huffman@30040 ` 515` huffman@30040 ` 516` ```instantiation "^" :: (real_normed_vector, type) real_normed_vector ``` huffman@30040 ` 517` ```begin ``` huffman@30040 ` 518` huffman@30040 ` 519` ```definition vector_norm_def: ``` huffman@30040 ` 520` ``` "norm (x::'a^'b) = setL2 (\i. norm (x\$i)) {1 .. dimindex (UNIV:: 'b set)}" ``` huffman@30040 ` 521` huffman@30040 ` 522` ```definition vector_sgn_def: ``` huffman@30040 ` 523` ``` "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" ``` huffman@30040 ` 524` huffman@30040 ` 525` ```instance proof ``` huffman@30040 ` 526` ``` fix a :: real and x y :: "'a ^ 'b" ``` huffman@30040 ` 527` ``` show "0 \ norm x" ``` huffman@30040 ` 528` ``` unfolding vector_norm_def ``` huffman@30040 ` 529` ``` by (rule setL2_nonneg) ``` huffman@30040 ` 530` ``` show "norm x = 0 \ x = 0" ``` huffman@30040 ` 531` ``` unfolding vector_norm_def ``` huffman@30040 ` 532` ``` by (simp add: setL2_eq_0_iff Cart_eq) ``` huffman@30040 ` 533` ``` show "norm (x + y) \ norm x + norm y" ``` huffman@30040 ` 534` ``` unfolding vector_norm_def ``` huffman@30040 ` 535` ``` apply (rule order_trans [OF _ setL2_triangle_ineq]) ``` huffman@30040 ` 536` ``` apply (rule setL2_mono) ``` huffman@30040 ` 537` ``` apply (simp add: vector_component norm_triangle_ineq) ``` huffman@30040 ` 538` ``` apply simp ``` huffman@30040 ` 539` ``` done ``` huffman@30040 ` 540` ``` show "norm (scaleR a x) = \a\ * norm x" ``` huffman@30040 ` 541` ``` unfolding vector_norm_def ``` huffman@30040 ` 542` ``` by (simp add: vector_component norm_scaleR setL2_right_distrib ``` huffman@30040 ` 543` ``` cong: strong_setL2_cong) ``` huffman@30040 ` 544` ``` show "sgn x = scaleR (inverse (norm x)) x" ``` huffman@30040 ` 545` ``` by (rule vector_sgn_def) ``` huffman@30040 ` 546` ```qed ``` huffman@30040 ` 547` huffman@30040 ` 548` ```end ``` huffman@30040 ` 549` huffman@30045 ` 550` ```subsection {* Inner products *} ``` huffman@30045 ` 551` huffman@30045 ` 552` ```instantiation "^" :: (real_inner, type) real_inner ``` huffman@30045 ` 553` ```begin ``` huffman@30045 ` 554` huffman@30045 ` 555` ```definition vector_inner_def: ``` huffman@30045 ` 556` ``` "inner x y = setsum (\i. inner (x\$i) (y\$i)) {1 .. dimindex(UNIV::'b set)}" ``` huffman@30045 ` 557` huffman@30045 ` 558` ```instance proof ``` huffman@30045 ` 559` ``` fix r :: real and x y z :: "'a ^ 'b" ``` huffman@30045 ` 560` ``` show "inner x y = inner y x" ``` huffman@30045 ` 561` ``` unfolding vector_inner_def ``` huffman@30045 ` 562` ``` by (simp add: inner_commute) ``` huffman@30045 ` 563` ``` show "inner (x + y) z = inner x z + inner y z" ``` huffman@30045 ` 564` ``` unfolding vector_inner_def ``` huffman@30045 ` 565` ``` by (vector inner_left_distrib) ``` huffman@30045 ` 566` ``` show "inner (scaleR r x) y = r * inner x y" ``` huffman@30045 ` 567` ``` unfolding vector_inner_def ``` huffman@30045 ` 568` ``` by (vector inner_scaleR_left) ``` huffman@30045 ` 569` ``` show "0 \ inner x x" ``` huffman@30045 ` 570` ``` unfolding vector_inner_def ``` huffman@30045 ` 571` ``` by (simp add: setsum_nonneg) ``` huffman@30045 ` 572` ``` show "inner x x = 0 \ x = 0" ``` huffman@30045 ` 573` ``` unfolding vector_inner_def ``` huffman@30045 ` 574` ``` by (simp add: Cart_eq setsum_nonneg_eq_0_iff) ``` huffman@30045 ` 575` ``` show "norm x = sqrt (inner x x)" ``` huffman@30045 ` 576` ``` unfolding vector_inner_def vector_norm_def setL2_def ``` huffman@30045 ` 577` ``` by (simp add: power2_norm_eq_inner) ``` huffman@30045 ` 578` ```qed ``` huffman@30045 ` 579` huffman@30045 ` 580` ```end ``` huffman@30045 ` 581` chaieb@29842 ` 582` ```subsection{* Properties of the dot product. *} ``` chaieb@29842 ` 583` huffman@30489 ` 584` ```lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \ y = y \ x" ``` chaieb@29842 ` 585` ``` by (vector mult_commute) ``` chaieb@29842 ` 586` ```lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \ z = (x \ z) + (y \ z)" ``` chaieb@29842 ` 587` ``` by (vector ring_simps) ``` huffman@30489 ` 588` ```lemma dot_radd: "x \ (y + (z::'a::ring ^ 'n)) = (x \ y) + (x \ z)" ``` chaieb@29842 ` 589` ``` by (vector ring_simps) ``` huffman@30489 ` 590` ```lemma dot_lsub: "((x::'a::ring ^ 'n) - y) \ z = (x \ z) - (y \ z)" ``` chaieb@29842 ` 591` ``` by (vector ring_simps) ``` huffman@30489 ` 592` ```lemma dot_rsub: "(x::'a::ring ^ 'n) \ (y - z) = (x \ y) - (x \ z)" ``` chaieb@29842 ` 593` ``` by (vector ring_simps) ``` chaieb@29842 ` 594` ```lemma dot_lmult: "(c *s x) \ y = (c::'a::ring) * (x \ y)" by (vector ring_simps) ``` chaieb@29842 ` 595` ```lemma dot_rmult: "x \ (c *s y) = (c::'a::comm_ring) * (x \ y)" by (vector ring_simps) ``` chaieb@29842 ` 596` ```lemma dot_lneg: "(-x) \ (y::'a::ring ^ 'n) = -(x \ y)" by vector ``` chaieb@29842 ` 597` ```lemma dot_rneg: "(x::'a::ring ^ 'n) \ (-y) = -(x \ y)" by vector ``` chaieb@29842 ` 598` ```lemma dot_lzero[simp]: "0 \ x = (0::'a::{comm_monoid_add, mult_zero})" by vector ``` chaieb@29842 ` 599` ```lemma dot_rzero[simp]: "x \ 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector ``` chaieb@29842 ` 600` ```lemma dot_pos_le[simp]: "(0::'a\ordered_ring_strict) <= x \ x" ``` chaieb@29842 ` 601` ``` by (simp add: dot_def setsum_nonneg) ``` chaieb@29842 ` 602` chaieb@29842 ` 603` ```lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\x \ F. f x \ (0 ::'a::pordered_ab_group_add)" shows "setsum f F = 0 \ (ALL x:F. f x = 0)" ``` chaieb@29842 ` 604` ```using fS fp setsum_nonneg[OF fp] ``` chaieb@29842 ` 605` ```proof (induct set: finite) ``` chaieb@29842 ` 606` ``` case empty thus ?case by simp ``` chaieb@29842 ` 607` ```next ``` chaieb@29842 ` 608` ``` case (insert x F) ``` chaieb@29842 ` 609` ``` from insert.prems have Fx: "f x \ 0" and Fp: "\ a \ F. f a \ 0" by simp_all ``` chaieb@29842 ` 610` ``` from insert.hyps Fp setsum_nonneg[OF Fp] ``` chaieb@29842 ` 611` ``` have h: "setsum f F = 0 \ (\a \F. f a = 0)" by metis ``` chaieb@29842 ` 612` ``` from sum_nonneg_eq_zero_iff[OF Fx setsum_nonneg[OF Fp]] insert.hyps(1,2) ``` chaieb@29842 ` 613` ``` show ?case by (simp add: h) ``` chaieb@29842 ` 614` ```qed ``` chaieb@29842 ` 615` chaieb@29842 ` 616` ```lemma dot_eq_0: "x \ x = 0 \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0" ``` chaieb@29842 ` 617` ```proof- ``` chaieb@29842 ` 618` ``` {assume f: "finite (UNIV :: 'n set)" ``` chaieb@29842 ` 619` ``` let ?S = "{Suc 0 .. card (UNIV :: 'n set)}" ``` chaieb@29842 ` 620` ``` have fS: "finite ?S" using f by simp ``` chaieb@29842 ` 621` ``` have fp: "\ i\ ?S. x\$i * x\$i>= 0" by simp ``` chaieb@29842 ` 622` ``` have ?thesis by (vector dimindex_def f setsum_squares_eq_0_iff[OF fS fp])} ``` chaieb@29842 ` 623` ``` moreover ``` chaieb@29842 ` 624` ``` {assume "\ finite (UNIV :: 'n set)" then have ?thesis by (vector dimindex_def)} ``` chaieb@29842 ` 625` ``` ultimately show ?thesis by metis ``` chaieb@29842 ` 626` ```qed ``` chaieb@29842 ` 627` huffman@30489 ` 628` ```lemma dot_pos_lt[simp]: "(0 < x \ x) \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \ 0" using dot_eq_0[of x] dot_pos_le[of x] ``` huffman@30489 ` 629` ``` by (auto simp add: le_less) ``` chaieb@29842 ` 630` huffman@30040 ` 631` ```subsection{* The collapse of the general concepts to dimension one. *} ``` chaieb@29842 ` 632` chaieb@29842 ` 633` ```lemma vector_one: "(x::'a ^1) = (\ i. (x\$1))" ``` chaieb@29842 ` 634` ``` by (vector dimindex_def) ``` chaieb@29842 ` 635` chaieb@29842 ` 636` ```lemma forall_one: "(\(x::'a ^1). P x) \ (\x. P(\ i. x))" ``` chaieb@29842 ` 637` ``` apply auto ``` chaieb@29842 ` 638` ``` apply (erule_tac x= "x\$1" in allE) ``` chaieb@29842 ` 639` ``` apply (simp only: vector_one[symmetric]) ``` chaieb@29842 ` 640` ``` done ``` chaieb@29842 ` 641` huffman@30040 ` 642` ```lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)" ``` huffman@30040 ` 643` ``` by (simp add: vector_norm_def dimindex_def) ``` huffman@30040 ` 644` huffman@30489 ` 645` ```lemma norm_real: "norm(x::real ^ 1) = abs(x\$1)" ``` huffman@30040 ` 646` ``` by (simp add: norm_vector_1) ``` chaieb@29842 ` 647` chaieb@29842 ` 648` ```text{* Metric *} ``` chaieb@29842 ` 649` huffman@30040 ` 650` ```text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *} ``` huffman@30489 ` 651` ```definition dist:: "real ^ 'n \ real ^ 'n \ real" where ``` chaieb@29842 ` 652` ``` "dist x y = norm (x - y)" ``` chaieb@29842 ` 653` chaieb@29842 ` 654` ```lemma dist_real: "dist(x::real ^ 1) y = abs((x\$1) - (y\$1))" ``` chaieb@29842 ` 655` ``` using dimindex_ge_1[of "UNIV :: 1 set"] ``` chaieb@29842 ` 656` ``` by (auto simp add: norm_real dist_def vector_component Cart_lambda_beta[where ?'a = "1"] ) ``` chaieb@29842 ` 657` chaieb@29842 ` 658` ```subsection {* A connectedness or intermediate value lemma with several applications. *} ``` chaieb@29842 ` 659` chaieb@29842 ` 660` ```lemma connected_real_lemma: ``` chaieb@29842 ` 661` ``` fixes f :: "real \ real ^ 'n" ``` chaieb@29842 ` 662` ``` assumes ab: "a \ b" and fa: "f a \ e1" and fb: "f b \ e2" ``` chaieb@29842 ` 663` ``` and dst: "\e x. a <= x \ x <= b \ 0 < e ==> \d > 0. \y. abs(y - x) < d \ dist(f y) (f x) < e" ``` chaieb@29842 ` 664` ``` and e1: "\y \ e1. \e > 0. \y'. dist y' y < e \ y' \ e1" ``` chaieb@29842 ` 665` ``` and e2: "\y \ e2. \e > 0. \y'. dist y' y < e \ y' \ e2" ``` chaieb@29842 ` 666` ``` and e12: "~(\x \ a. x <= b \ f x \ e1 \ f x \ e2)" ``` chaieb@29842 ` 667` ``` shows "\x \ a. x <= b \ f x \ e1 \ f x \ e2" (is "\ x. ?P x") ``` chaieb@29842 ` 668` ```proof- ``` chaieb@29842 ` 669` ``` let ?S = "{c. \x \ a. x <= c \ f x \ e1}" ``` huffman@30489 ` 670` ``` have Se: " \x. x \ ?S" apply (rule exI[where x=a]) by (auto simp add: fa) ``` huffman@30489 ` 671` ``` have Sub: "\y. isUb UNIV ?S y" ``` chaieb@29842 ` 672` ``` apply (rule exI[where x= b]) ``` huffman@30489 ` 673` ``` using ab fb e12 by (auto simp add: isUb_def setle_def) ``` huffman@30489 ` 674` ``` from reals_complete[OF Se Sub] obtain l where ``` chaieb@29842 ` 675` ``` l: "isLub UNIV ?S l"by blast ``` chaieb@29842 ` 676` ``` have alb: "a \ l" "l \ b" using l ab fa fb e12 ``` huffman@30489 ` 677` ``` apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) ``` chaieb@29842 ` 678` ``` by (metis linorder_linear) ``` chaieb@29842 ` 679` ``` have ale1: "\z \ a. z < l \ f z \ e1" using l ``` chaieb@29842 ` 680` ``` apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) ``` chaieb@29842 ` 681` ``` by (metis linorder_linear not_le) ``` chaieb@29842 ` 682` ``` have th1: "\z x e d :: real. z <= x + e \ e < d ==> z < x \ abs(z - x) < d" by arith ``` chaieb@29842 ` 683` ``` have th2: "\e x:: real. 0 < e ==> ~(x + e <= x)" by arith ``` chaieb@29842 ` 684` ``` have th3: "\d::real. d > 0 \ \e > 0. e < d" by dlo ``` chaieb@29842 ` 685` ``` {assume le2: "f l \ e2" ``` chaieb@29842 ` 686` ``` from le2 fa fb e12 alb have la: "l \ a" by metis ``` chaieb@29842 ` 687` ``` hence lap: "l - a > 0" using alb by arith ``` huffman@30489 ` 688` ``` from e2[rule_format, OF le2] obtain e where ``` chaieb@29842 ` 689` ``` e: "e > 0" "\y. dist y (f l) < e \ y \ e2" by metis ``` huffman@30489 ` 690` ``` from dst[OF alb e(1)] obtain d where ``` chaieb@29842 ` 691` ``` d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis ``` huffman@30489 ` 692` ``` have "\d'. d' < d \ d' >0 \ l - d' > a" using lap d(1) ``` chaieb@29842 ` 693` ``` apply ferrack by arith ``` chaieb@29842 ` 694` ``` then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis ``` chaieb@29842 ` 695` ``` from d e have th0: "\y. \y - l\ < d \ f y \ e2" by metis ``` chaieb@29842 ` 696` ``` from th0[rule_format, of "l - d'"] d' have "f (l - d') \ e2" by auto ``` chaieb@29842 ` 697` ``` moreover ``` chaieb@29842 ` 698` ``` have "f (l - d') \ e1" using ale1[rule_format, of "l -d'"] d' by auto ``` chaieb@29842 ` 699` ``` ultimately have False using e12 alb d' by auto} ``` chaieb@29842 ` 700` ``` moreover ``` chaieb@29842 ` 701` ``` {assume le1: "f l \ e1" ``` chaieb@29842 ` 702` ``` from le1 fa fb e12 alb have lb: "l \ b" by metis ``` chaieb@29842 ` 703` ``` hence blp: "b - l > 0" using alb by arith ``` huffman@30489 ` 704` ``` from e1[rule_format, OF le1] obtain e where ``` chaieb@29842 ` 705` ``` e: "e > 0" "\y. dist y (f l) < e \ y \ e1" by metis ``` huffman@30489 ` 706` ``` from dst[OF alb e(1)] obtain d where ``` chaieb@29842 ` 707` ``` d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis ``` huffman@30489 ` 708` ``` have "\d'. d' < d \ d' >0" using d(1) by dlo ``` chaieb@29842 ` 709` ``` then obtain d' where d': "d' > 0" "d' < d" by metis ``` chaieb@29842 ` 710` ``` from d e have th0: "\y. \y - l\ < d \ f y \ e1" by auto ``` chaieb@29842 ` 711` ``` hence "\y. l \ y \ y \ l + d' \ f y \ e1" using d' by auto ``` chaieb@29842 ` 712` ``` with ale1 have "\y. a \ y \ y \ l + d' \ f y \ e1" by auto ``` huffman@30489 ` 713` ``` with l d' have False ``` chaieb@29842 ` 714` ``` by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } ``` chaieb@29842 ` 715` ``` ultimately show ?thesis using alb by metis ``` chaieb@29842 ` 716` ```qed ``` chaieb@29842 ` 717` huffman@29881 ` 718` ```text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case @{typ "real^1"} *} ``` chaieb@29842 ` 719` chaieb@29842 ` 720` ```lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)" ``` chaieb@29842 ` 721` ```proof- ``` huffman@30489 ` 722` ``` have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith ``` chaieb@29842 ` 723` ``` thus ?thesis by (simp add: ring_simps power2_eq_square) ``` chaieb@29842 ` 724` ```qed ``` chaieb@29842 ` 725` chaieb@29842 ` 726` ```lemma square_continuous: "0 < (e::real) ==> \d. 0 < d \ (\y. abs(y - x) < d \ abs(y * y - x * x) < e)" ``` chaieb@29842 ` 727` ``` using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_def, rule_format, of e x] apply (auto simp add: power2_eq_square) ``` chaieb@29842 ` 728` ``` apply (rule_tac x="s" in exI) ``` chaieb@29842 ` 729` ``` apply auto ``` chaieb@29842 ` 730` ``` apply (erule_tac x=y in allE) ``` chaieb@29842 ` 731` ``` apply auto ``` chaieb@29842 ` 732` ``` done ``` chaieb@29842 ` 733` chaieb@29842 ` 734` ```lemma real_le_lsqrt: "0 <= x \ 0 <= y \ x <= y^2 ==> sqrt x <= y" ``` chaieb@29842 ` 735` ``` using real_sqrt_le_iff[of x "y^2"] by simp ``` chaieb@29842 ` 736` chaieb@29842 ` 737` ```lemma real_le_rsqrt: "x^2 \ y \ x \ sqrt y" ``` chaieb@29842 ` 738` ``` using real_sqrt_le_mono[of "x^2" y] by simp ``` chaieb@29842 ` 739` chaieb@29842 ` 740` ```lemma real_less_rsqrt: "x^2 < y \ x < sqrt y" ``` chaieb@29842 ` 741` ``` using real_sqrt_less_mono[of "x^2" y] by simp ``` chaieb@29842 ` 742` huffman@30489 ` 743` ```lemma sqrt_even_pow2: assumes n: "even n" ``` chaieb@29842 ` 744` ``` shows "sqrt(2 ^ n) = 2 ^ (n div 2)" ``` chaieb@29842 ` 745` ```proof- ``` huffman@30489 ` 746` ``` from n obtain m where m: "n = 2*m" unfolding even_nat_equiv_def2 ``` huffman@30489 ` 747` ``` by (auto simp add: nat_number) ``` chaieb@29842 ` 748` ``` from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)" ``` chaieb@29842 ` 749` ``` by (simp only: power_mult[symmetric] mult_commute) ``` huffman@30489 ` 750` ``` then show ?thesis using m by simp ``` chaieb@29842 ` 751` ```qed ``` chaieb@29842 ` 752` chaieb@29842 ` 753` ```lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)" ``` chaieb@29842 ` 754` ``` apply (cases "x = 0", simp_all) ``` chaieb@29842 ` 755` ``` using sqrt_divide_self_eq[of x] ``` chaieb@29842 ` 756` ``` apply (simp add: inverse_eq_divide real_sqrt_ge_0_iff field_simps) ``` chaieb@29842 ` 757` ``` done ``` chaieb@29842 ` 758` chaieb@29842 ` 759` ```text{* Hence derive more interesting properties of the norm. *} ``` chaieb@29842 ` 760` chaieb@30263 ` 761` ```lemma norm_0[simp]: "norm (0::real ^ 'n) = 0" ``` huffman@30040 ` 762` ``` by (rule norm_zero) ``` huffman@30040 ` 763` chaieb@30263 ` 764` ```lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x" ``` huffman@30040 ` 765` ``` by (simp add: vector_norm_def vector_component setL2_right_distrib ``` huffman@30040 ` 766` ``` abs_mult cong: strong_setL2_cong) ``` chaieb@29842 ` 767` ```lemma norm_eq_0_dot: "(norm x = 0) \ (x \ x = (0::real))" ``` huffman@30040 ` 768` ``` by (simp add: vector_norm_def dot_def setL2_def power2_eq_square) ``` huffman@30040 ` 769` ```lemma real_vector_norm_def: "norm x = sqrt (x \ x)" ``` huffman@30040 ` 770` ``` by (simp add: vector_norm_def setL2_def dot_def power2_eq_square) ``` chaieb@29842 ` 771` ```lemma norm_pow_2: "norm x ^ 2 = x \ x" ``` huffman@30040 ` 772` ``` by (simp add: real_vector_norm_def) ``` huffman@30041 ` 773` ```lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) ``` chaieb@30263 ` 774` ```lemma vector_mul_eq_0[simp]: "(a *s x = 0) \ a = (0::'a::idom) \ x = 0" ``` chaieb@29842 ` 775` ``` by vector ``` chaieb@30263 ` 776` ```lemma vector_mul_lcancel[simp]: "a *s x = a *s y \ a = (0::real) \ x = y" ``` chaieb@29842 ` 777` ``` by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) ``` chaieb@30263 ` 778` ```lemma vector_mul_rcancel[simp]: "a *s x = b *s x \ (a::real) = b \ x = 0" ``` chaieb@29842 ` 779` ``` by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) ``` chaieb@29842 ` 780` ```lemma vector_mul_lcancel_imp: "a \ (0::real) ==> a *s x = a *s y ==> (x = y)" ``` chaieb@29842 ` 781` ``` by (metis vector_mul_lcancel) ``` chaieb@29842 ` 782` ```lemma vector_mul_rcancel_imp: "x \ 0 \ (a::real) *s x = b *s x ==> a = b" ``` chaieb@29842 ` 783` ``` by (metis vector_mul_rcancel) ``` chaieb@29842 ` 784` ```lemma norm_cauchy_schwarz: "x \ y <= norm x * norm y" ``` chaieb@29842 ` 785` ```proof- ``` chaieb@29842 ` 786` ``` {assume "norm x = 0" ``` huffman@30041 ` 787` ``` hence ?thesis by (simp add: dot_lzero dot_rzero)} ``` chaieb@29842 ` 788` ``` moreover ``` huffman@30489 ` 789` ``` {assume "norm y = 0" ``` huffman@30041 ` 790` ``` hence ?thesis by (simp add: dot_lzero dot_rzero)} ``` chaieb@29842 ` 791` ``` moreover ``` chaieb@29842 ` 792` ``` {assume h: "norm x \ 0" "norm y \ 0" ``` chaieb@29842 ` 793` ``` let ?z = "norm y *s x - norm x *s y" ``` huffman@30041 ` 794` ``` from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps) ``` chaieb@29842 ` 795` ``` from dot_pos_le[of ?z] ``` chaieb@29842 ` 796` ``` have "(norm x * norm y) * (x \ y) \ norm x ^2 * norm y ^2" ``` chaieb@29842 ` 797` ``` apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps) ``` chaieb@29842 ` 798` ``` by (simp add: norm_pow_2[symmetric] power2_eq_square dot_sym) ``` chaieb@29842 ` 799` ``` hence "x\y \ (norm x ^2 * norm y ^2) / (norm x * norm y)" using p ``` chaieb@29842 ` 800` ``` by (simp add: field_simps) ``` chaieb@29842 ` 801` ``` hence ?thesis using h by (simp add: power2_eq_square)} ``` chaieb@29842 ` 802` ``` ultimately show ?thesis by metis ``` chaieb@29842 ` 803` ```qed ``` chaieb@29842 ` 804` chaieb@29842 ` 805` ```lemma norm_cauchy_schwarz_abs: "\x \ y\ \ norm x * norm y" ``` chaieb@29842 ` 806` ``` using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"] ``` huffman@30041 ` 807` ``` by (simp add: real_abs_def dot_rneg) ``` chaieb@29842 ` 808` chaieb@29842 ` 809` ```lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x - y)" ``` huffman@30041 ` 810` ``` using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps) ``` chaieb@29842 ` 811` ```lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e" ``` huffman@30041 ` 812` ``` by (metis order_trans norm_triangle_ineq) ``` chaieb@29842 ` 813` ```lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e" ``` huffman@30041 ` 814` ``` by (metis basic_trans_rules(21) norm_triangle_ineq) ``` chaieb@29842 ` 815` chaieb@29842 ` 816` ```lemma component_le_norm: "i \ {1 .. dimindex(UNIV :: 'n set)} ==> \x\$i\ <= norm (x::real ^ 'n)" ``` huffman@30040 ` 817` ``` apply (simp add: vector_norm_def) ``` huffman@30040 ` 818` ``` apply (rule member_le_setL2, simp_all) ``` huffman@30040 ` 819` ``` done ``` huffman@30040 ` 820` chaieb@29842 ` 821` ```lemma norm_bound_component_le: "norm(x::real ^ 'n) <= e ``` chaieb@29842 ` 822` ``` ==> \i \ {1 .. dimindex(UNIV:: 'n set)}. \x\$i\ <= e" ``` chaieb@29842 ` 823` ``` by (metis component_le_norm order_trans) ``` chaieb@29842 ` 824` chaieb@29842 ` 825` ```lemma norm_bound_component_lt: "norm(x::real ^ 'n) < e ``` chaieb@29842 ` 826` ``` ==> \i \ {1 .. dimindex(UNIV:: 'n set)}. \x\$i\ < e" ``` chaieb@29842 ` 827` ``` by (metis component_le_norm basic_trans_rules(21)) ``` chaieb@29842 ` 828` chaieb@29842 ` 829` ```lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\i. \x\$i\) {1..dimindex(UNIV::'n set)}" ``` huffman@30040 ` 830` ``` by (simp add: vector_norm_def setL2_le_setsum) ``` chaieb@29842 ` 831` huffman@30489 ` 832` ```lemma real_abs_norm[simp]: "\ norm x\ = norm (x :: real ^'n)" ``` huffman@30040 ` 833` ``` by (rule abs_norm_cancel) ``` chaieb@29842 ` 834` ```lemma real_abs_sub_norm: "\norm(x::real ^'n) - norm y\ <= norm(x - y)" ``` huffman@30040 ` 835` ``` by (rule norm_triangle_ineq3) ``` chaieb@29842 ` 836` ```lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \ x \ x <= y \ y" ``` chaieb@29842 ` 837` ``` by (simp add: real_vector_norm_def) ``` chaieb@29842 ` 838` ```lemma norm_lt: "norm(x::real ^'n) < norm(y) \ x \ x < y \ y" ``` chaieb@29842 ` 839` ``` by (simp add: real_vector_norm_def) ``` chaieb@29842 ` 840` ```lemma norm_eq: "norm (x::real ^'n) = norm y \ x \ x = y \ y" ``` chaieb@29842 ` 841` ``` by (simp add: order_eq_iff norm_le) ``` chaieb@29842 ` 842` ```lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \ x \ x = 1" ``` chaieb@29842 ` 843` ``` by (simp add: real_vector_norm_def) ``` chaieb@29842 ` 844` chaieb@29842 ` 845` ```text{* Squaring equations and inequalities involving norms. *} ``` chaieb@29842 ` 846` chaieb@29842 ` 847` ```lemma dot_square_norm: "x \ x = norm(x)^2" ``` chaieb@29842 ` 848` ``` by (simp add: real_vector_norm_def dot_pos_le ) ``` chaieb@29842 ` 849` chaieb@29842 ` 850` ```lemma norm_eq_square: "norm(x) = a \ 0 <= a \ x \ x = a^2" ``` huffman@30040 ` 851` ``` by (auto simp add: real_vector_norm_def) ``` chaieb@29842 ` 852` chaieb@29842 ` 853` ```lemma real_abs_le_square_iff: "\x\ \ \y\ \ (x::real)^2 \ y^2" ``` chaieb@29842 ` 854` ```proof- ``` chaieb@29842 ` 855` ``` have "x^2 \ y^2 \ (x -y) * (y + x) \ 0" by (simp add: ring_simps power2_eq_square) ``` chaieb@29842 ` 856` ``` also have "\ \ \x\ \ \y\" apply (simp add: zero_compare_simps real_abs_def not_less) by arith ``` chaieb@29842 ` 857` ```finally show ?thesis .. ``` chaieb@29842 ` 858` ```qed ``` chaieb@29842 ` 859` chaieb@29842 ` 860` ```lemma norm_le_square: "norm(x) <= a \ 0 <= a \ x \ x <= a^2" ``` huffman@30040 ` 861` ``` apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) ``` huffman@30041 ` 862` ``` using norm_ge_zero[of x] ``` chaieb@29842 ` 863` ``` apply arith ``` chaieb@29842 ` 864` ``` done ``` chaieb@29842 ` 865` huffman@30489 ` 866` ```lemma norm_ge_square: "norm(x) >= a \ a <= 0 \ x \ x >= a ^ 2" ``` huffman@30040 ` 867` ``` apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) ``` huffman@30041 ` 868` ``` using norm_ge_zero[of x] ``` chaieb@29842 ` 869` ``` apply arith ``` chaieb@29842 ` 870` ``` done ``` chaieb@29842 ` 871` chaieb@29842 ` 872` ```lemma norm_lt_square: "norm(x) < a \ 0 < a \ x \ x < a^2" ``` chaieb@29842 ` 873` ``` by (metis not_le norm_ge_square) ``` chaieb@29842 ` 874` ```lemma norm_gt_square: "norm(x) > a \ a < 0 \ x \ x > a^2" ``` chaieb@29842 ` 875` ``` by (metis norm_le_square not_less) ``` chaieb@29842 ` 876` chaieb@29842 ` 877` ```text{* Dot product in terms of the norm rather than conversely. *} ``` chaieb@29842 ` 878` chaieb@29842 ` 879` ```lemma dot_norm: "x \ y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2" ``` chaieb@29842 ` 880` ``` by (simp add: norm_pow_2 dot_ladd dot_radd dot_sym) ``` chaieb@29842 ` 881` chaieb@29842 ` 882` ```lemma dot_norm_neg: "x \ y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2" ``` chaieb@29842 ` 883` ``` by (simp add: norm_pow_2 dot_ladd dot_radd dot_lsub dot_rsub dot_sym) ``` chaieb@29842 ` 884` chaieb@29842 ` 885` chaieb@29842 ` 886` ```text{* Equality of vectors in terms of @{term "op \"} products. *} ``` chaieb@29842 ` 887` chaieb@29842 ` 888` ```lemma vector_eq: "(x:: real ^ 'n) = y \ x \ x = x \ y\ y \ y = x \ x" (is "?lhs \ ?rhs") ``` chaieb@29842 ` 889` ```proof ``` chaieb@29842 ` 890` ``` assume "?lhs" then show ?rhs by simp ``` chaieb@29842 ` 891` ```next ``` chaieb@29842 ` 892` ``` assume ?rhs ``` chaieb@29842 ` 893` ``` then have "x \ x - x \ y = 0 \ x \ y - y\ y = 0" by simp ``` huffman@30489 ` 894` ``` hence "x \ (x - y) = 0 \ y \ (x - y) = 0" ``` chaieb@29842 ` 895` ``` by (simp add: dot_rsub dot_lsub dot_sym) ``` chaieb@29842 ` 896` ``` then have "(x - y) \ (x - y) = 0" by (simp add: ring_simps dot_lsub dot_rsub) ``` chaieb@29842 ` 897` ``` then show "x = y" by (simp add: dot_eq_0) ``` chaieb@29842 ` 898` ```qed ``` chaieb@29842 ` 899` chaieb@29842 ` 900` chaieb@29842 ` 901` ```subsection{* General linear decision procedure for normed spaces. *} ``` chaieb@29842 ` 902` chaieb@29842 ` 903` ```lemma norm_cmul_rule_thm: "b >= norm(x) ==> \c\ * b >= norm(c *s x)" ``` chaieb@29842 ` 904` ``` apply (clarsimp simp add: norm_mul) ``` chaieb@29842 ` 905` ``` apply (rule mult_mono1) ``` chaieb@29842 ` 906` ``` apply simp_all ``` chaieb@29842 ` 907` ``` done ``` chaieb@29842 ` 908` chaieb@30263 ` 909` ``` (* FIXME: Move all these theorems into the ML code using lemma antiquotation *) ``` chaieb@29842 ` 910` ```lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n) \ b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)" ``` chaieb@29842 ` 911` ``` apply (rule norm_triangle_le) by simp ``` chaieb@29842 ` 912` chaieb@29842 ` 913` ```lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \ b == a - b \ 0" ``` chaieb@29842 ` 914` ``` by (simp add: ring_simps) ``` chaieb@29842 ` 915` chaieb@29842 ` 916` ```lemma pth_1: "(x::real^'n) == 1 *s x" by (simp only: vector_smult_lid) ``` chaieb@29842 ` 917` ```lemma pth_2: "x - (y::real^'n) == x + -y" by (atomize (full)) simp ``` chaieb@29842 ` 918` ```lemma pth_3: "(-x::real^'n) == -1 *s x" by vector ``` chaieb@29842 ` 919` ```lemma pth_4: "0 *s (x::real^'n) == 0" "c *s 0 = (0::real ^ 'n)" by vector+ ``` chaieb@29842 ` 920` ```lemma pth_5: "c *s (d *s x) == (c * d) *s (x::real ^ 'n)" by (atomize (full)) vector ``` chaieb@29842 ` 921` ```lemma pth_6: "(c::real) *s (x + y) == c *s x + c *s y" by (atomize (full)) (vector ring_simps) ``` huffman@30489 ` 922` ```lemma pth_7: "0 + x == (x::real^'n)" "x + 0 == x" by simp_all ``` huffman@30489 ` 923` ```lemma pth_8: "(c::real) *s x + d *s x == (c + d) *s x" by (atomize (full)) (vector ring_simps) ``` chaieb@29842 ` 924` ```lemma pth_9: "((c::real) *s x + z) + d *s x == (c + d) *s x + z" ``` chaieb@29842 ` 925` ``` "c *s x + (d *s x + z) == (c + d) *s x + z" ``` chaieb@29842 ` 926` ``` "(c *s x + w) + (d *s x + z) == (c + d) *s x + (w + z)" by ((atomize (full)), vector ring_simps)+ ``` chaieb@29842 ` 927` ```lemma pth_a: "(0::real) *s x + y == y" by (atomize (full)) vector ``` huffman@30489 ` 928` ```lemma pth_b: "(c::real) *s x + d *s y == c *s x + d *s y" ``` chaieb@29842 ` 929` ``` "(c *s x + z) + d *s y == c *s x + (z + d *s y)" ``` chaieb@29842 ` 930` ``` "c *s x + (d *s y + z) == c *s x + (d *s y + z)" ``` chaieb@29842 ` 931` ``` "(c *s x + w) + (d *s y + z) == c *s x + (w + (d *s y + z))" ``` chaieb@29842 ` 932` ``` by ((atomize (full)), vector)+ ``` chaieb@29842 ` 933` ```lemma pth_c: "(c::real) *s x + d *s y == d *s y + c *s x" ``` chaieb@29842 ` 934` ``` "(c *s x + z) + d *s y == d *s y + (c *s x + z)" ``` chaieb@29842 ` 935` ``` "c *s x + (d *s y + z) == d *s y + (c *s x + z)" ``` chaieb@29842 ` 936` ``` "(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+ ``` chaieb@29842 ` 937` ```lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector ``` chaieb@29842 ` 938` chaieb@29842 ` 939` ```lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \ norm x \ 0 \ n \ norm x" ``` huffman@30041 ` 940` ``` by (atomize) (auto simp add: norm_ge_zero) ``` chaieb@29842 ` 941` chaieb@29842 ` 942` ```lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \ 0 \ -x \ 0" by arith ``` chaieb@29842 ` 943` huffman@30489 ` 944` ```lemma norm_pths: ``` chaieb@29842 ` 945` ``` "(x::real ^'n) = y \ norm (x - y) \ 0" ``` chaieb@29842 ` 946` ``` "x \ y \ \ (norm (x - y) \ 0)" ``` huffman@30041 ` 947` ``` using norm_ge_zero[of "x - y"] by auto ``` chaieb@29842 ` 948` chaieb@29842 ` 949` ```use "normarith.ML" ``` chaieb@29842 ` 950` wenzelm@30549 ` 951` ```method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) ``` chaieb@29842 ` 952` ```*} "Proves simple linear statements about vector norms" ``` chaieb@29842 ` 953` chaieb@29842 ` 954` chaieb@29842 ` 955` chaieb@29842 ` 956` ```text{* Hence more metric properties. *} ``` chaieb@29842 ` 957` chaieb@30263 ` 958` ```lemma dist_refl[simp]: "dist x x = 0" by norm ``` chaieb@29842 ` 959` chaieb@29842 ` 960` ```lemma dist_sym: "dist x y = dist y x"by norm ``` chaieb@29842 ` 961` chaieb@30263 ` 962` ```lemma dist_pos_le[simp]: "0 <= dist x y" by norm ``` chaieb@29842 ` 963` chaieb@29842 ` 964` ```lemma dist_triangle: "dist x z <= dist x y + dist y z" by norm ``` chaieb@29842 ` 965` chaieb@29842 ` 966` ```lemma dist_triangle_alt: "dist y z <= dist x y + dist x z" by norm ``` chaieb@29842 ` 967` chaieb@30263 ` 968` ```lemma dist_eq_0[simp]: "dist x y = 0 \ x = y" by norm ``` chaieb@29842 ` 969` huffman@30489 ` 970` ```lemma dist_pos_lt: "x \ y ==> 0 < dist x y" by norm ``` huffman@30489 ` 971` ```lemma dist_nz: "x \ y \ 0 < dist x y" by norm ``` huffman@30489 ` 972` huffman@30489 ` 973` ```lemma dist_triangle_le: "dist x z + dist y z <= e \ dist x y <= e" by norm ``` huffman@30489 ` 974` huffman@30489 ` 975` ```lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e" by norm ``` huffman@30489 ` 976` huffman@30489 ` 977` ```lemma dist_triangle_half_l: "dist x1 y < e / 2 \ dist x2 y < e / 2 ==> dist x1 x2 < e" by norm ``` huffman@30489 ` 978` huffman@30489 ` 979` ```lemma dist_triangle_half_r: "dist y x1 < e / 2 \ dist y x2 < e / 2 ==> dist x1 x2 < e" by norm ``` chaieb@29842 ` 980` chaieb@29842 ` 981` ```lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'" ``` huffman@30489 ` 982` ``` by norm ``` huffman@30489 ` 983` huffman@30489 ` 984` ```lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \c\ * dist x y" ``` huffman@30489 ` 985` ``` unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul .. ``` huffman@30489 ` 986` huffman@30489 ` 987` ```lemma dist_triangle_add_half: " dist x x' < e / 2 \ dist y y' < e / 2 ==> dist(x + y) (x' + y') < e" by norm ``` huffman@30489 ` 988` huffman@30489 ` 989` ```lemma dist_le_0[simp]: "dist x y <= 0 \ x = y" by norm ``` chaieb@29842 ` 990` chaieb@29842 ` 991` ```lemma setsum_eq: "setsum f S = (\ i. setsum (\x. (f x)\$i ) S)" ``` chaieb@29842 ` 992` ``` apply vector ``` chaieb@29842 ` 993` ``` apply auto ``` chaieb@29842 ` 994` ``` apply (cases "finite S") ``` chaieb@29842 ` 995` ``` apply (rule finite_induct[of S]) ``` chaieb@29842 ` 996` ``` apply (auto simp add: vector_component zero_index) ``` chaieb@29842 ` 997` ``` done ``` chaieb@29842 ` 998` huffman@30489 ` 999` ```lemma setsum_clauses: ``` chaieb@29842 ` 1000` ``` shows "setsum f {} = 0" ``` chaieb@29842 ` 1001` ``` and "finite S \ setsum f (insert x S) = ``` chaieb@29842 ` 1002` ``` (if x \ S then setsum f S else f x + setsum f S)" ``` chaieb@29842 ` 1003` ``` by (auto simp add: insert_absorb) ``` chaieb@29842 ` 1004` huffman@30489 ` 1005` ```lemma setsum_cmul: ``` chaieb@29842 ` 1006` ``` fixes f:: "'c \ ('a::semiring_1)^'n" ``` chaieb@29842 ` 1007` ``` shows "setsum (\x. c *s f x) S = c *s setsum f S" ``` chaieb@29842 ` 1008` ``` by (simp add: setsum_eq Cart_eq Cart_lambda_beta vector_component setsum_right_distrib) ``` chaieb@29842 ` 1009` huffman@30489 ` 1010` ```lemma setsum_component: ``` chaieb@29842 ` 1011` ``` fixes f:: " 'a \ ('b::semiring_1) ^'n" ``` chaieb@29842 ` 1012` ``` assumes i: "i \ {1 .. dimindex(UNIV:: 'n set)}" ``` chaieb@29842 ` 1013` ``` shows "(setsum f S)\$i = setsum (\x. (f x)\$i) S" ``` chaieb@29842 ` 1014` ``` using i by (simp add: setsum_eq Cart_lambda_beta) ``` chaieb@29842 ` 1015` huffman@30489 ` 1016` ```lemma setsum_norm: ``` chaieb@29842 ` 1017` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` chaieb@29842 ` 1018` ``` assumes fS: "finite S" ``` chaieb@29842 ` 1019` ``` shows "norm (setsum f S) <= setsum (\x. norm(f x)) S" ``` chaieb@29842 ` 1020` ```proof(induct rule: finite_induct[OF fS]) ``` huffman@30041 ` 1021` ``` case 1 thus ?case by simp ``` chaieb@29842 ` 1022` ```next ``` chaieb@29842 ` 1023` ``` case (2 x S) ``` chaieb@29842 ` 1024` ``` from "2.hyps" have "norm (setsum f (insert x S)) \ norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq) ``` chaieb@29842 ` 1025` ``` also have "\ \ norm (f x) + setsum (\x. norm(f x)) S" ``` chaieb@29842 ` 1026` ``` using "2.hyps" by simp ``` chaieb@29842 ` 1027` ``` finally show ?case using "2.hyps" by simp ``` chaieb@29842 ` 1028` ```qed ``` chaieb@29842 ` 1029` huffman@30489 ` 1030` ```lemma real_setsum_norm: ``` chaieb@29842 ` 1031` ``` fixes f :: "'a \ real ^'n" ``` chaieb@29842 ` 1032` ``` assumes fS: "finite S" ``` chaieb@29842 ` 1033` ``` shows "norm (setsum f S) <= setsum (\x. norm(f x)) S" ``` chaieb@29842 ` 1034` ```proof(induct rule: finite_induct[OF fS]) ``` huffman@30040 ` 1035` ``` case 1 thus ?case by simp ``` chaieb@29842 ` 1036` ```next ``` chaieb@29842 ` 1037` ``` case (2 x S) ``` huffman@30040 ` 1038` ``` from "2.hyps" have "norm (setsum f (insert x S)) \ norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq) ``` chaieb@29842 ` 1039` ``` also have "\ \ norm (f x) + setsum (\x. norm(f x)) S" ``` chaieb@29842 ` 1040` ``` using "2.hyps" by simp ``` chaieb@29842 ` 1041` ``` finally show ?case using "2.hyps" by simp ``` chaieb@29842 ` 1042` ```qed ``` chaieb@29842 ` 1043` huffman@30489 ` 1044` ```lemma setsum_norm_le: ``` chaieb@29842 ` 1045` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` chaieb@29842 ` 1046` ``` assumes fS: "finite S" ``` chaieb@29842 ` 1047` ``` and fg: "\x \ S. norm (f x) \ g x" ``` chaieb@29842 ` 1048` ``` shows "norm (setsum f S) \ setsum g S" ``` chaieb@29842 ` 1049` ```proof- ``` huffman@30489 ` 1050` ``` from fg have "setsum (\x. norm(f x)) S <= setsum g S" ``` chaieb@29842 ` 1051` ``` by - (rule setsum_mono, simp) ``` chaieb@29842 ` 1052` ``` then show ?thesis using setsum_norm[OF fS, of f] fg ``` chaieb@29842 ` 1053` ``` by arith ``` chaieb@29842 ` 1054` ```qed ``` chaieb@29842 ` 1055` huffman@30489 ` 1056` ```lemma real_setsum_norm_le: ``` chaieb@29842 ` 1057` ``` fixes f :: "'a \ real ^ 'n" ``` chaieb@29842 ` 1058` ``` assumes fS: "finite S" ``` chaieb@29842 ` 1059` ``` and fg: "\x \ S. norm (f x) \ g x" ``` chaieb@29842 ` 1060` ``` shows "norm (setsum f S) \ setsum g S" ``` chaieb@29842 ` 1061` ```proof- ``` huffman@30489 ` 1062` ``` from fg have "setsum (\x. norm(f x)) S <= setsum g S" ``` chaieb@29842 ` 1063` ``` by - (rule setsum_mono, simp) ``` chaieb@29842 ` 1064` ``` then show ?thesis using real_setsum_norm[OF fS, of f] fg ``` chaieb@29842 ` 1065` ``` by arith ``` chaieb@29842 ` 1066` ```qed ``` chaieb@29842 ` 1067` chaieb@29842 ` 1068` ```lemma setsum_norm_bound: ``` chaieb@29842 ` 1069` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` chaieb@29842 ` 1070` ``` assumes fS: "finite S" ``` chaieb@29842 ` 1071` ``` and K: "\x \ S. norm (f x) \ K" ``` chaieb@29842 ` 1072` ``` shows "norm (setsum f S) \ of_nat (card S) * K" ``` chaieb@29842 ` 1073` ``` using setsum_norm_le[OF fS K] setsum_constant[symmetric] ``` chaieb@29842 ` 1074` ``` by simp ``` chaieb@29842 ` 1075` chaieb@29842 ` 1076` ```lemma real_setsum_norm_bound: ``` chaieb@29842 ` 1077` ``` fixes f :: "'a \ real ^ 'n" ``` chaieb@29842 ` 1078` ``` assumes fS: "finite S" ``` chaieb@29842 ` 1079` ``` and K: "\x \ S. norm (f x) \ K" ``` chaieb@29842 ` 1080` ``` shows "norm (setsum f S) \ of_nat (card S) * K" ``` chaieb@29842 ` 1081` ``` using real_setsum_norm_le[OF fS K] setsum_constant[symmetric] ``` chaieb@29842 ` 1082` ``` by simp ``` chaieb@29842 ` 1083` chaieb@29842 ` 1084` ```lemma setsum_vmul: ``` chaieb@29842 ` 1085` ``` fixes f :: "'a \ 'b::{real_normed_vector,semiring, mult_zero}" ``` chaieb@29842 ` 1086` ``` assumes fS: "finite S" ``` chaieb@29842 ` 1087` ``` shows "setsum f S *s v = setsum (\x. f x *s v) S" ``` chaieb@29842 ` 1088` ```proof(induct rule: finite_induct[OF fS]) ``` chaieb@29842 ` 1089` ``` case 1 then show ?case by (simp add: vector_smult_lzero) ``` chaieb@29842 ` 1090` ```next ``` chaieb@29842 ` 1091` ``` case (2 x F) ``` huffman@30489 ` 1092` ``` from "2.hyps" have "setsum f (insert x F) *s v = (f x + setsum f F) *s v" ``` chaieb@29842 ` 1093` ``` by simp ``` huffman@30489 ` 1094` ``` also have "\ = f x *s v + setsum f F *s v" ``` chaieb@29842 ` 1095` ``` by (simp add: vector_sadd_rdistrib) ``` chaieb@29842 ` 1096` ``` also have "\ = setsum (\x. f x *s v) (insert x F)" using "2.hyps" by simp ``` chaieb@29842 ` 1097` ``` finally show ?case . ``` chaieb@29842 ` 1098` ```qed ``` chaieb@29842 ` 1099` chaieb@29842 ` 1100` ```(* FIXME : Problem thm setsum_vmul[of _ "f:: 'a \ real ^'n"] --- ``` chaieb@29842 ` 1101` ``` Get rid of *s and use real_vector instead! Also prove that ^ creates a real_vector !! *) ``` chaieb@29842 ` 1102` chaieb@29842 ` 1103` ```lemma setsum_add_split: assumes mn: "(m::nat) \ n + 1" ``` chaieb@29842 ` 1104` ``` shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" ``` chaieb@29842 ` 1105` ```proof- ``` chaieb@29842 ` 1106` ``` let ?A = "{m .. n}" ``` chaieb@29842 ` 1107` ``` let ?B = "{n + 1 .. n + p}" ``` huffman@30489 ` 1108` ``` have eq: "{m .. n+p} = ?A \ ?B" using mn by auto ``` chaieb@29842 ` 1109` ``` have d: "?A \ ?B = {}" by auto ``` chaieb@29842 ` 1110` ``` from setsum_Un_disjoint[of "?A" "?B" f] eq d show ?thesis by auto ``` chaieb@29842 ` 1111` ```qed ``` chaieb@29842 ` 1112` chaieb@29842 ` 1113` ```lemma setsum_natinterval_left: ``` huffman@30489 ` 1114` ``` assumes mn: "(m::nat) <= n" ``` chaieb@29842 ` 1115` ``` shows "setsum f {m..n} = f m + setsum f {m + 1..n}" ``` chaieb@29842 ` 1116` ```proof- ``` chaieb@29842 ` 1117` ``` from mn have "{m .. n} = insert m {m+1 .. n}" by auto ``` chaieb@29842 ` 1118` ``` then show ?thesis by auto ``` chaieb@29842 ` 1119` ```qed ``` chaieb@29842 ` 1120` huffman@30489 ` 1121` ```lemma setsum_natinterval_difff: ``` chaieb@29842 ` 1122` ``` fixes f:: "nat \ ('a::ab_group_add)" ``` chaieb@29842 ` 1123` ``` shows "setsum (\k. f k - f(k + 1)) {(m::nat) .. n} = ``` chaieb@29842 ` 1124` ``` (if m <= n then f m - f(n + 1) else 0)" ``` chaieb@29842 ` 1125` ```by (induct n, auto simp add: ring_simps not_le le_Suc_eq) ``` chaieb@29842 ` 1126` chaieb@29842 ` 1127` ```lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] ``` chaieb@29842 ` 1128` chaieb@29842 ` 1129` ```lemma setsum_setsum_restrict: ``` chaieb@29842 ` 1130` ``` "finite S \ finite T \ setsum (\x. setsum (\y. f x y) {y. y\ T \ R x y}) S = setsum (\y. setsum (\x. f x y) {x. x \ S \ R x y}) T" ``` chaieb@29842 ` 1131` ``` apply (simp add: setsum_restrict_set'[unfolded mem_def] mem_def) ``` chaieb@29842 ` 1132` ``` by (rule setsum_commute) ``` chaieb@29842 ` 1133` chaieb@29842 ` 1134` ```lemma setsum_image_gen: assumes fS: "finite S" ``` chaieb@29842 ` 1135` ``` shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f ` S)" ``` chaieb@29842 ` 1136` ```proof- ``` chaieb@29842 ` 1137` ``` {fix x assume "x \ S" then have "{y. y\ f`S \ f x = y} = {f x}" by auto} ``` chaieb@29842 ` 1138` ``` note th0 = this ``` huffman@30489 ` 1139` ``` have "setsum g S = setsum (\x. setsum (\y. g x) {y. y\ f`S \ f x = y}) S" ``` huffman@30489 ` 1140` ``` apply (rule setsum_cong2) ``` chaieb@29842 ` 1141` ``` by (simp add: th0) ``` chaieb@29842 ` 1142` ``` also have "\ = setsum (\y. setsum g {x. x \ S \ f x = y}) (f ` S)" ``` chaieb@29842 ` 1143` ``` apply (rule setsum_setsum_restrict[OF fS]) ``` chaieb@29842 ` 1144` ``` by (rule finite_imageI[OF fS]) ``` chaieb@29842 ` 1145` ``` finally show ?thesis . ``` chaieb@29842 ` 1146` ```qed ``` chaieb@29842 ` 1147` chaieb@29842 ` 1148` ``` (* FIXME: Here too need stupid finiteness assumption on T!!! *) ``` chaieb@29842 ` 1149` ```lemma setsum_group: ``` chaieb@29842 ` 1150` ``` assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \ T" ``` chaieb@29842 ` 1151` ``` shows "setsum (\y. setsum g {x. x\ S \ f x = y}) T = setsum g S" ``` huffman@30489 ` 1152` chaieb@29842 ` 1153` ```apply (subst setsum_image_gen[OF fS, of g f]) ``` chaieb@30263 ` 1154` ```apply (rule setsum_mono_zero_right[OF fT fST]) ``` chaieb@29842 ` 1155` ```by (auto intro: setsum_0') ``` chaieb@29842 ` 1156` chaieb@29842 ` 1157` ```lemma vsum_norm_allsubsets_bound: ``` chaieb@29842 ` 1158` ``` fixes f:: "'a \ real ^'n" ``` huffman@30489 ` 1159` ``` assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" ``` chaieb@29842 ` 1160` ``` shows "setsum (\x. norm (f x)) P \ 2 * real (dimindex(UNIV :: 'n set)) * e" ``` chaieb@29842 ` 1161` ```proof- ``` chaieb@29842 ` 1162` ``` let ?d = "real (dimindex (UNIV ::'n set))" ``` chaieb@29842 ` 1163` ``` let ?nf = "\x. norm (f x)" ``` chaieb@29842 ` 1164` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29842 ` 1165` ``` have th0: "setsum (\x. setsum (\i. \f x \$ i\) ?U) P = setsum (\i. setsum (\x. \f x \$ i\) P) ?U" ``` chaieb@29842 ` 1166` ``` by (rule setsum_commute) ``` chaieb@29842 ` 1167` ``` have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def) ``` chaieb@29842 ` 1168` ``` have "setsum ?nf P \ setsum (\x. setsum (\i. \f x \$ i\) ?U) P" ``` chaieb@29842 ` 1169` ``` apply (rule setsum_mono) ``` chaieb@29842 ` 1170` ``` by (rule norm_le_l1) ``` chaieb@29842 ` 1171` ``` also have "\ \ 2 * ?d * e" ``` chaieb@29842 ` 1172` ``` unfolding th0 th1 ``` chaieb@29842 ` 1173` ``` proof(rule setsum_bounded) ``` chaieb@29842 ` 1174` ``` fix i assume i: "i \ ?U" ``` chaieb@29842 ` 1175` ``` let ?Pp = "{x. x\ P \ f x \$ i \ 0}" ``` chaieb@29842 ` 1176` ``` let ?Pn = "{x. x \ P \ f x \$ i < 0}" ``` chaieb@29842 ` 1177` ``` have thp: "P = ?Pp \ ?Pn" by auto ``` chaieb@29842 ` 1178` ``` have thp0: "?Pp \ ?Pn ={}" by auto ``` chaieb@29842 ` 1179` ``` have PpP: "?Pp \ P" and PnP: "?Pn \ P" by blast+ ``` chaieb@29842 ` 1180` ``` have Ppe:"setsum (\x. \f x \$ i\) ?Pp \ e" ``` chaieb@29842 ` 1181` ``` using i component_le_norm[OF i, of "setsum (\x. f x) ?Pp"] fPs[OF PpP] ``` chaieb@29842 ` 1182` ``` by (auto simp add: setsum_component intro: abs_le_D1) ``` chaieb@29842 ` 1183` ``` have Pne: "setsum (\x. \f x \$ i\) ?Pn \ e" ``` chaieb@29842 ` 1184` ``` using i component_le_norm[OF i, of "setsum (\x. - f x) ?Pn"] fPs[OF PnP] ``` huffman@30041 ` 1185` ``` by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1) ``` huffman@30489 ` 1186` ``` have "setsum (\x. \f x \$ i\) P = setsum (\x. \f x \$ i\) ?Pp + setsum (\x. \f x \$ i\) ?Pn" ``` chaieb@29842 ` 1187` ``` apply (subst thp) ``` huffman@30489 ` 1188` ``` apply (rule setsum_Un_zero) ``` chaieb@29842 ` 1189` ``` using fP thp0 by auto ``` chaieb@29842 ` 1190` ``` also have "\ \ 2*e" using Pne Ppe by arith ``` chaieb@29842 ` 1191` ``` finally show "setsum (\x. \f x \$ i\) P \ 2*e" . ``` chaieb@29842 ` 1192` ``` qed ``` chaieb@29842 ` 1193` ``` finally show ?thesis . ``` chaieb@29842 ` 1194` ```qed ``` chaieb@29842 ` 1195` chaieb@29842 ` 1196` ```lemma dot_lsum: "finite S \ setsum f S \ (y::'a::{comm_ring}^'n) = setsum (\x. f x \ y) S " ``` chaieb@30263 ` 1197` ``` by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd) ``` chaieb@29842 ` 1198` chaieb@29842 ` 1199` ```lemma dot_rsum: "finite S \ (y::'a::{comm_ring}^'n) \ setsum f S = setsum (\x. y \ f x) S " ``` chaieb@29842 ` 1200` ``` by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd) ``` chaieb@29842 ` 1201` chaieb@29842 ` 1202` ```subsection{* Basis vectors in coordinate directions. *} ``` chaieb@29842 ` 1203` chaieb@29842 ` 1204` chaieb@29842 ` 1205` ```definition "basis k = (\ i. if i = k then 1 else 0)" ``` chaieb@29842 ` 1206` huffman@30489 ` 1207` ```lemma delta_mult_idempotent: ``` chaieb@29842 ` 1208` ``` "(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) ``` chaieb@29842 ` 1209` chaieb@29842 ` 1210` ```lemma norm_basis: ``` chaieb@29842 ` 1211` ``` assumes k: "k \ {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29842 ` 1212` ``` shows "norm (basis k :: real ^'n) = 1" ``` huffman@30489 ` 1213` ``` using k ``` chaieb@29842 ` 1214` ``` apply (simp add: basis_def real_vector_norm_def dot_def) ``` chaieb@29842 ` 1215` ``` apply (vector delta_mult_idempotent) ``` chaieb@29842 ` 1216` ``` using setsum_delta[of "{1 .. dimindex (UNIV :: 'n set)}" "k" "\k. 1::real"] ``` chaieb@29842 ` 1217` ``` apply auto ``` chaieb@29842 ` 1218` ``` done ``` chaieb@29842 ` 1219` chaieb@29842 ` 1220` ```lemma norm_basis_1: "norm(basis 1 :: real ^'n) = 1" ``` chaieb@29842 ` 1221` ``` apply (simp add: basis_def real_vector_norm_def dot_def) ``` chaieb@29842 ` 1222` ``` apply (vector delta_mult_idempotent) ``` chaieb@29842 ` 1223` ``` using setsum_delta[of "{1 .. dimindex (UNIV :: 'n set)}" "1" "\k. 1::real"] dimindex_nonzero[of "UNIV :: 'n set"] ``` chaieb@29842 ` 1224` ``` apply auto ``` chaieb@29842 ` 1225` ``` done ``` chaieb@29842 ` 1226` chaieb@29842 ` 1227` ```lemma vector_choose_size: "0 <= c ==> \(x::real^'n). norm x = c" ``` chaieb@29842 ` 1228` ``` apply (rule exI[where x="c *s basis 1"]) ``` chaieb@29842 ` 1229` ``` by (simp only: norm_mul norm_basis_1) ``` chaieb@29842 ` 1230` huffman@30489 ` 1231` ```lemma vector_choose_dist: assumes e: "0 <= e" ``` chaieb@29842 ` 1232` ``` shows "\(y::real^'n). dist x y = e" ``` chaieb@29842 ` 1233` ```proof- ``` chaieb@29842 ` 1234` ``` from vector_choose_size[OF e] obtain c:: "real ^'n" where "norm c = e" ``` chaieb@29842 ` 1235` ``` by blast ``` chaieb@29842 ` 1236` ``` then have "dist x (x - c) = e" by (simp add: dist_def) ``` chaieb@29842 ` 1237` ``` then show ?thesis by blast ``` chaieb@29842 ` 1238` ```qed ``` chaieb@29842 ` 1239` chaieb@29842 ` 1240` ```lemma basis_inj: "inj_on (basis :: nat \ real ^'n) {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29842 ` 1241` ``` by (auto simp add: inj_on_def basis_def Cart_eq Cart_lambda_beta) ``` chaieb@29842 ` 1242` chaieb@29842 ` 1243` ```lemma basis_component: "i \ {1 .. dimindex(UNIV:: 'n set)} ==> (basis k ::('a::semiring_1)^'n)\$i = (if k=i then 1 else 0)" ``` chaieb@29842 ` 1244` ``` by (simp add: basis_def Cart_lambda_beta) ``` chaieb@29842 ` 1245` chaieb@29842 ` 1246` ```lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)" ``` chaieb@29842 ` 1247` ``` by auto ``` chaieb@29842 ` 1248` chaieb@29842 ` 1249` ```lemma basis_expansion: ``` chaieb@29842 ` 1250` ``` "setsum (\i. (x\$i) *s basis i) {1 .. dimindex (UNIV :: 'n set)} = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") ``` chaieb@29842 ` 1251` ``` by (auto simp add: Cart_eq basis_component[where ?'n = "'n"] setsum_component vector_component cond_value_iff setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong) ``` chaieb@29842 ` 1252` huffman@30489 ` 1253` ```lemma basis_expansion_unique: ``` chaieb@29842 ` 1254` ``` "setsum (\i. f i *s basis i) {1 .. dimindex (UNIV :: 'n set)} = (x::('a::comm_ring_1) ^'n) \ (\i\{1 .. dimindex(UNIV:: 'n set)}. f i = x\$i)" ``` chaieb@29842 ` 1255` ``` by (simp add: Cart_eq setsum_component vector_component basis_component setsum_delta cond_value_iff cong del: if_weak_cong) ``` chaieb@29842 ` 1256` chaieb@29842 ` 1257` ```lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" ``` chaieb@29842 ` 1258` ``` by auto ``` chaieb@29842 ` 1259` chaieb@29842 ` 1260` ```lemma dot_basis: ``` chaieb@29842 ` 1261` ``` assumes i: "i \ {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29842 ` 1262` ``` shows "basis i \ x = x\$i" "x \ (basis i :: 'a^'n) = (x\$i :: 'a::semiring_1)" ``` chaieb@29842 ` 1263` ``` using i ``` chaieb@29842 ` 1264` ``` by (auto simp add: dot_def basis_def Cart_lambda_beta cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong) ``` chaieb@29842 ` 1265` chaieb@29842 ` 1266` ```lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \ i \ {1..dimindex(UNIV ::'n set)}" ``` chaieb@29842 ` 1267` ``` by (auto simp add: Cart_eq basis_component zero_index) ``` chaieb@29842 ` 1268` huffman@30489 ` 1269` ```lemma basis_nonzero: ``` chaieb@29842 ` 1270` ``` assumes k: "k \ {1 .. dimindex(UNIV ::'n set)}" ``` chaieb@29842 ` 1271` ``` shows "basis k \ (0:: 'a::semiring_1 ^'n)" ``` chaieb@29842 ` 1272` ``` using k by (simp add: basis_eq_0) ``` chaieb@29842 ` 1273` chaieb@29842 ` 1274` ```lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = (z::'a::semiring_1^'n)" ``` chaieb@29842 ` 1275` ``` apply (auto simp add: Cart_eq dot_basis) ``` chaieb@29842 ` 1276` ``` apply (erule_tac x="basis i" in allE) ``` chaieb@29842 ` 1277` ``` apply (simp add: dot_basis) ``` chaieb@29842 ` 1278` ``` apply (subgoal_tac "y = z") ``` chaieb@29842 ` 1279` ``` apply simp ``` chaieb@29842 ` 1280` ``` apply vector ``` chaieb@29842 ` 1281` ``` done ``` chaieb@29842 ` 1282` chaieb@29842 ` 1283` ```lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = (y::'a::semiring_1^'n)" ``` chaieb@29842 ` 1284` ``` apply (auto simp add: Cart_eq dot_basis) ``` chaieb@29842 ` 1285` ``` apply (erule_tac x="basis i" in allE) ``` chaieb@29842 ` 1286` ``` apply (simp add: dot_basis) ``` chaieb@29842 ` 1287` ``` apply (subgoal_tac "x = y") ``` chaieb@29842 ` 1288` ``` apply simp ``` chaieb@29842 ` 1289` ``` apply vector ``` chaieb@29842 ` 1290` ``` done ``` chaieb@29842 ` 1291` chaieb@29842 ` 1292` ```subsection{* Orthogonality. *} ``` chaieb@29842 ` 1293` chaieb@29842 ` 1294` ```definition "orthogonal x y \ (x \ y = 0)" ``` chaieb@29842 ` 1295` chaieb@29842 ` 1296` ```lemma orthogonal_basis: ``` huffman@30489 ` 1297` ``` assumes i:"i \ {1 .. dimindex(UNIV ::'n set)}" ``` chaieb@29842 ` 1298` ``` shows "orthogonal (basis i :: 'a^'n) x \ x\$i = (0::'a::ring_1)" ``` chaieb@29842 ` 1299` ``` using i ``` chaieb@29842 ` 1300` ``` by (auto simp add: orthogonal_def dot_def basis_def Cart_lambda_beta cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong) ``` chaieb@29842 ` 1301` chaieb@29842 ` 1302` ```lemma orthogonal_basis_basis: ``` huffman@30489 ` 1303` ``` assumes i:"i \ {1 .. dimindex(UNIV ::'n set)}" ``` huffman@30489 ` 1304` ``` and j: "j \ {1 .. dimindex(UNIV ::'n set)}" ``` huffman@30489 ` 1305` ``` shows "orthogonal (basis i :: 'a::ring_1^'n) (basis j) \ i \ j" ``` chaieb@29842 ` 1306` ``` unfolding orthogonal_basis[OF i] basis_component[OF i] by simp ``` chaieb@29842 ` 1307` chaieb@29842 ` 1308` ``` (* FIXME : Maybe some of these require less than comm_ring, but not all*) ``` chaieb@29842 ` 1309` ```lemma orthogonal_clauses: ``` chaieb@29842 ` 1310` ``` "orthogonal a (0::'a::comm_ring ^'n)" ``` chaieb@29842 ` 1311` ``` "orthogonal a x ==> orthogonal a (c *s x)" ``` chaieb@29842 ` 1312` ``` "orthogonal a x ==> orthogonal a (-x)" ``` chaieb@29842 ` 1313` ``` "orthogonal a x \ orthogonal a y ==> orthogonal a (x + y)" ``` chaieb@29842 ` 1314` ``` "orthogonal a x \ orthogonal a y ==> orthogonal a (x - y)" ``` chaieb@29842 ` 1315` ``` "orthogonal 0 a" ``` chaieb@29842 ` 1316` ``` "orthogonal x a ==> orthogonal (c *s x) a" ``` chaieb@29842 ` 1317` ``` "orthogonal x a ==> orthogonal (-x) a" ``` chaieb@29842 ` 1318` ``` "orthogonal x a \ orthogonal y a ==> orthogonal (x + y) a" ``` chaieb@29842 ` 1319` ``` "orthogonal x a \ orthogonal y a ==> orthogonal (x - y) a" ``` chaieb@29842 ` 1320` ``` unfolding orthogonal_def dot_rneg dot_rmult dot_radd dot_rsub ``` chaieb@29842 ` 1321` ``` dot_lzero dot_rzero dot_lneg dot_lmult dot_ladd dot_lsub ``` chaieb@29842 ` 1322` ``` by simp_all ``` chaieb@29842 ` 1323` chaieb@29842 ` 1324` ```lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n)y \ orthogonal y x" ``` chaieb@29842 ` 1325` ``` by (simp add: orthogonal_def dot_sym) ``` chaieb@29842 ` 1326` chaieb@29842 ` 1327` ```subsection{* Explicit vector construction from lists. *} ``` chaieb@29842 ` 1328` chaieb@29842 ` 1329` ```lemma Cart_lambda_beta_1[simp]: "(Cart_lambda g)\$1 = g 1" ``` chaieb@29842 ` 1330` ``` apply (rule Cart_lambda_beta[rule_format]) ``` chaieb@29842 ` 1331` ``` using dimindex_ge_1 apply auto done ``` chaieb@29842 ` 1332` chaieb@29842 ` 1333` ```lemma Cart_lambda_beta_1'[simp]: "(Cart_lambda g)\$(Suc 0) = g 1" ``` chaieb@29842 ` 1334` ``` by (simp only: One_nat_def[symmetric] Cart_lambda_beta_1) ``` chaieb@29842 ` 1335` chaieb@29842 ` 1336` ```definition "vector l = (\ i. if i <= length l then l ! (i - 1) else 0)" ``` chaieb@29842 ` 1337` chaieb@29842 ` 1338` ```lemma vector_1: "(vector[x]) \$1 = x" ``` chaieb@29842 ` 1339` ``` using dimindex_ge_1 ``` chaieb@29842 ` 1340` ``` by (auto simp add: vector_def Cart_lambda_beta[rule_format]) ``` chaieb@29842 ` 1341` ```lemma dimindex_2[simp]: "2 \ {1 .. dimindex (UNIV :: 2 set)}" ``` chaieb@29842 ` 1342` ``` by (auto simp add: dimindex_def) ``` chaieb@29842 ` 1343` ```lemma dimindex_2'[simp]: "2 \ {Suc 0 .. dimindex (UNIV :: 2 set)}" ``` chaieb@29842 ` 1344` ``` by (auto simp add: dimindex_def) ``` chaieb@29842 ` 1345` ```lemma dimindex_3[simp]: "2 \ {1 .. dimindex (UNIV :: 3 set)}" "3 \ {1 .. dimindex (UNIV :: 3 set)}" ``` chaieb@29842 ` 1346` ``` by (auto simp add: dimindex_def) ``` chaieb@29842 ` 1347` chaieb@29842 ` 1348` ```lemma dimindex_3'[simp]: "2 \ {Suc 0 .. dimindex (UNIV :: 3 set)}" "3 \ {Suc 0 .. dimindex (UNIV :: 3 set)}" ``` chaieb@29842 ` 1349` ``` by (auto simp add: dimindex_def) ``` chaieb@29842 ` 1350` chaieb@29842 ` 1351` ```lemma vector_2: ``` chaieb@29842 ` 1352` ``` "(vector[x,y]) \$1 = x" ``` chaieb@29842 ` 1353` ``` "(vector[x,y] :: 'a^2)\$2 = (y::'a::zero)" ``` chaieb@29842 ` 1354` ``` apply (simp add: vector_def) ``` chaieb@29842 ` 1355` ``` using Cart_lambda_beta[rule_format, OF dimindex_2, of "\i. if i \ length [x,y] then [x,y] ! (i - 1) else (0::'a)"] ``` chaieb@29842 ` 1356` ``` apply (simp only: vector_def ) ``` chaieb@29842 ` 1357` ``` apply auto ``` chaieb@29842 ` 1358` ``` done ``` chaieb@29842 ` 1359` chaieb@29842 ` 1360` ```lemma vector_3: ``` chaieb@29842 ` 1361` ``` "(vector [x,y,z] ::('a::zero)^3)\$1 = x" ``` chaieb@29842 ` 1362` ``` "(vector [x,y,z] ::('a::zero)^3)\$2 = y" ``` chaieb@29842 ` 1363` ``` "(vector [x,y,z] ::('a::zero)^3)\$3 = z" ``` chaieb@29842 ` 1364` ```apply (simp_all add: vector_def Cart_lambda_beta dimindex_3) ``` chaieb@29842 ` 1365` ``` using Cart_lambda_beta[rule_format, OF dimindex_3(1), of "\i. if i \ length [x,y,z] then [x,y,z] ! (i - 1) else (0::'a)"] using Cart_lambda_beta[rule_format, OF dimindex_3(2), of "\i. if i \ length [x,y,z] then [x,y,z] ! (i - 1) else (0::'a)"] ``` chaieb@29842 ` 1366` ``` by simp_all ``` chaieb@29842 ` 1367` chaieb@29842 ` 1368` ```lemma forall_vector_1: "(\v::'a::zero^1. P v) \ (\x. P(vector[x]))" ``` chaieb@29842 ` 1369` ``` apply auto ``` chaieb@29842 ` 1370` ``` apply (erule_tac x="v\$1" in allE) ``` chaieb@29842 ` 1371` ``` apply (subgoal_tac "vector [v\$1] = v") ``` chaieb@29842 ` 1372` ``` apply simp ``` chaieb@29842 ` 1373` ``` by (vector vector_def dimindex_def) ``` chaieb@29842 ` 1374` chaieb@29842 ` 1375` ```lemma forall_vector_2: "(\v::'a::zero^2. P v) \ (\x y. P(vector[x, y]))" ``` chaieb@29842 ` 1376` ``` apply auto ``` chaieb@29842 ` 1377` ``` apply (erule_tac x="v\$1" in allE) ``` chaieb@29842 ` 1378` ``` apply (erule_tac x="v\$2" in allE) ``` chaieb@29842 ` 1379` ``` apply (subgoal_tac "vector [v\$1, v\$2] = v") ``` chaieb@29842 ` 1380` ``` apply simp ``` chaieb@29842 ` 1381` ``` apply (vector vector_def dimindex_def) ``` chaieb@29842 ` 1382` ``` apply auto ``` chaieb@29842 ` 1383` ``` apply (subgoal_tac "i = 1 \ i =2", auto) ``` chaieb@29842 ` 1384` ``` done ``` chaieb@29842 ` 1385` chaieb@29842 ` 1386` ```lemma forall_vector_3: "(\v::'a::zero^3. P v) \ (\x y z. P(vector[x, y, z]))" ``` chaieb@29842 ` 1387` ``` apply auto ``` chaieb@29842 ` 1388` ``` apply (erule_tac x="v\$1" in allE) ``` chaieb@29842 ` 1389` ``` apply (erule_tac x="v\$2" in allE) ``` chaieb@29842 ` 1390` ``` apply (erule_tac x="v\$3" in allE) ``` chaieb@29842 ` 1391` ``` apply (subgoal_tac "vector [v\$1, v\$2, v\$3] = v") ``` chaieb@29842 ` 1392` ``` apply simp ``` chaieb@29842 ` 1393` ``` apply (vector vector_def dimindex_def) ``` chaieb@29842 ` 1394` ``` apply auto ``` chaieb@29842 ` 1395` ``` apply (subgoal_tac "i = 1 \ i =2 \ i = 3", auto) ``` chaieb@29842 ` 1396` ``` done ``` chaieb@29842 ` 1397` chaieb@29842 ` 1398` ```subsection{* Linear functions. *} ``` chaieb@29842 ` 1399` chaieb@29842 ` 1400` ```definition "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *s x) = c *s f x)" ``` chaieb@29842 ` 1401` chaieb@29842 ` 1402` ```lemma linear_compose_cmul: "linear f ==> linear (\x. (c::'a::comm_semiring) *s f x)" ``` chaieb@29842 ` 1403` ``` by (vector linear_def Cart_eq Cart_lambda_beta[rule_format] ring_simps) ``` chaieb@29842 ` 1404` chaieb@29842 ` 1405` ```lemma linear_compose_neg: "linear (f :: 'a ^'n \ 'a::comm_ring ^'m) ==> linear (\x. -(f(x)))" by (vector linear_def Cart_eq) ``` chaieb@29842 ` 1406` chaieb@29842 ` 1407` ```lemma linear_compose_add: "linear (f :: 'a ^'n \ 'a::semiring_1 ^'m) \ linear g ==> linear (\x. f(x) + g(x))" ``` chaieb@29842 ` 1408` ``` by (vector linear_def Cart_eq ring_simps) ``` chaieb@29842 ` 1409` chaieb@29842 ` 1410` ```lemma linear_compose_sub: "linear (f :: 'a ^'n \ 'a::ring_1 ^'m) \ linear g ==> linear (\x. f x - g x)" ``` chaieb@29842 ` 1411` ``` by (vector linear_def Cart_eq ring_simps) ``` chaieb@29842 ` 1412` chaieb@29842 ` 1413` ```lemma linear_compose: "linear f \ linear g ==> linear (g o f)" ``` chaieb@29842 ` 1414` ``` by (simp add: linear_def) ``` chaieb@29842 ` 1415` chaieb@29842 ` 1416` ```lemma linear_id: "linear id" by (simp add: linear_def id_def) ``` chaieb@29842 ` 1417` chaieb@29842 ` 1418` ```lemma linear_zero: "linear (\x. 0::'a::semiring_1 ^ 'n)" by (simp add: linear_def) ``` chaieb@29842 ` 1419` chaieb@29842 ` 1420` ```lemma linear_compose_setsum: ``` chaieb@29842 ` 1421` ``` assumes fS: "finite S" and lS: "\a \ S. linear (f a :: 'a::semiring_1 ^ 'n \ 'a ^ 'm)" ``` chaieb@29842 ` 1422` ``` shows "linear(\x. setsum (\a. f a x :: 'a::semiring_1 ^'m) S)" ``` chaieb@29842 ` 1423` ``` using lS ``` chaieb@29842 ` 1424` ``` apply (induct rule: finite_induct[OF fS]) ``` chaieb@29842 ` 1425` ``` by (auto simp add: linear_zero intro: linear_compose_add) ``` chaieb@29842 ` 1426` chaieb@29842 ` 1427` ```lemma linear_vmul_component: ``` chaieb@29842 ` 1428` ``` fixes f:: "'a::semiring_1^'m \ 'a^'n" ``` chaieb@29842 ` 1429` ``` assumes lf: "linear f" and k: "k \ {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29842 ` 1430` ``` shows "linear (\x. f x \$ k *s v)" ``` chaieb@29842 ` 1431` ``` using lf k ``` chaieb@29842 ` 1432` ``` apply (auto simp add: linear_def ) ``` chaieb@29842 ` 1433` ``` by (vector ring_simps)+ ``` chaieb@29842 ` 1434` chaieb@29842 ` 1435` ```lemma linear_0: "linear f ==> f 0 = (0::'a::semiring_1 ^'n)" ``` chaieb@29842 ` 1436` ``` unfolding linear_def ``` chaieb@29842 ` 1437` ``` apply clarsimp ``` chaieb@29842 ` 1438` ``` apply (erule allE[where x="0::'a"]) ``` chaieb@29842 ` 1439` ``` apply simp ``` chaieb@29842 ` 1440` ``` done ``` chaieb@29842 ` 1441` chaieb@29842 ` 1442` ```lemma linear_cmul: "linear f ==> f(c*s x) = c *s f x" by (simp add: linear_def) ``` chaieb@29842 ` 1443` chaieb@29842 ` 1444` ```lemma linear_neg: "linear (f :: 'a::ring_1 ^'n \ _) ==> f (-x) = - f x" ``` chaieb@29842 ` 1445` ``` unfolding vector_sneg_minus1 ``` huffman@30489 ` 1446` ``` using linear_cmul[of f] by auto ``` huffman@30489 ` 1447` huffman@30489 ` 1448` ```lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def) ``` chaieb@29842 ` 1449` chaieb@29842 ` 1450` ```lemma linear_sub: "linear (f::'a::ring_1 ^'n \ _) ==> f(x - y) = f x - f y" ``` chaieb@29842 ` 1451` ``` by (simp add: diff_def linear_add linear_neg) ``` chaieb@29842 ` 1452` huffman@30489 ` 1453` ```lemma linear_setsum: ``` chaieb@29842 ` 1454` ``` fixes f:: "'a::semiring_1^'n \ _" ``` chaieb@29842 ` 1455` ``` assumes lf: "linear f" and fS: "finite S" ``` chaieb@29842 ` 1456` ``` shows "f (setsum g S) = setsum (f o g) S" ``` chaieb@29842 ` 1457` ```proof (induct rule: finite_induct[OF fS]) ``` chaieb@29842 ` 1458` ``` case 1 thus ?case by (simp add: linear_0[OF lf]) ``` chaieb@29842 ` 1459` ```next ``` chaieb@29842 ` 1460` ``` case (2 x F) ``` chaieb@29842 ` 1461` ``` have "f (setsum g (insert x F)) = f (g x + setsum g F)" using "2.hyps" ``` chaieb@29842 ` 1462` ``` by simp ``` chaieb@29842 ` 1463` ``` also have "\ = f (g x) + f (setsum g F)" using linear_add[OF lf] by simp ``` chaieb@29842 ` 1464` ``` also have "\ = setsum (f o g) (insert x F)" using "2.hyps" by simp ``` chaieb@29842 ` 1465` ``` finally show ?case . ``` chaieb@29842 ` 1466` ```qed ``` chaieb@29842 ` 1467` chaieb@29842 ` 1468` ```lemma linear_setsum_mul: ``` chaieb@29842 ` 1469` ``` fixes f:: "'a ^'n \ 'a::semiring_1^'m" ``` chaieb@29842 ` 1470` ``` assumes lf: "linear f" and fS: "finite S" ``` chaieb@29842 ` 1471` ``` shows "f (setsum (\i. c i *s v i) S) = setsum (\i. c i *s f (v i)) S" ``` chaieb@29842 ` 1472` ``` using linear_setsum[OF lf fS, of "\i. c i *s v i" , unfolded o_def] ``` huffman@30489 ` 1473` ``` linear_cmul[OF lf] by simp ``` chaieb@29842 ` 1474` chaieb@29842 ` 1475` ```lemma linear_injective_0: ``` chaieb@29842 ` 1476` ``` assumes lf: "linear (f:: 'a::ring_1 ^ 'n \ _)" ``` chaieb@29842 ` 1477` ``` shows "inj f \ (\x. f x = 0 \ x = 0)" ``` chaieb@29842 ` 1478` ```proof- ``` chaieb@29842 ` 1479` ``` have "inj f \ (\ x y. f x = f y \ x = y)" by (simp add: inj_on_def) ``` chaieb@29842 ` 1480` ``` also have "\ \ (\ x y. f x - f y = 0 \ x - y = 0)" by simp ``` huffman@30489 ` 1481` ``` also have "\ \ (\ x y. f (x - y) = 0 \ x - y = 0)" ``` chaieb@29842 ` 1482` ``` by (simp add: linear_sub[OF lf]) ``` chaieb@29842 ` 1483` ``` also have "\ \ (\ x. f x = 0 \ x = 0)" by auto ``` chaieb@29842 ` 1484` ``` finally show ?thesis . ``` chaieb@29842 ` 1485` ```qed ``` chaieb@29842 ` 1486` chaieb@29842 ` 1487` ```lemma linear_bounded: ``` chaieb@29842 ` 1488` ``` fixes f:: "real ^'m \ real ^'n" ``` chaieb@29842 ` 1489` ``` assumes lf: "linear f" ``` chaieb@29842 ` 1490` ``` shows "\B. \x. norm (f x) \ B * norm x" ``` chaieb@29842 ` 1491` ```proof- ``` chaieb@29842 ` 1492` ``` let ?S = "{1..dimindex(UNIV:: 'm set)}" ``` chaieb@29842 ` 1493` ``` let ?B = "setsum (\i. norm(f(basis i))) ?S" ``` chaieb@29842 ` 1494` ``` have fS: "finite ?S" by simp ``` chaieb@29842 ` 1495` ``` {fix x:: "real ^ 'm" ``` chaieb@29842 ` 1496` ``` let ?g = "(\i::nat. (x\$i) *s (basis i) :: real ^ 'm)" ``` chaieb@29842 ` 1497` ``` have "norm (f x) = norm (f (setsum (\i. (x\$i) *s (basis i)) ?S))" ``` chaieb@29842 ` 1498` ``` by (simp only: basis_expansion) ``` chaieb@29842 ` 1499` ``` also have "\ = norm (setsum (\i. (x\$i) *s f (basis i))?S)" ``` chaieb@29842 ` 1500` ``` using linear_setsum[OF lf fS, of ?g, unfolded o_def] linear_cmul[OF lf] ``` chaieb@29842 ` 1501` ``` by auto ``` chaieb@29842 ` 1502` ``` finally have th0: "norm (f x) = norm (setsum (\i. (x\$i) *s f (basis i))?S)" . ``` chaieb@29842 ` 1503` ``` {fix i assume i: "i \ ?S" ``` chaieb@29842 ` 1504` ``` from component_le_norm[OF i, of x] ``` chaieb@29842 ` 1505` ``` have "norm ((x\$i) *s f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" ``` chaieb@29842 ` 1506` ``` unfolding norm_mul ``` chaieb@29842 ` 1507` ``` apply (simp only: mult_commute) ``` chaieb@29842 ` 1508` ``` apply (rule mult_mono) ``` huffman@30041 ` 1509` ``` by (auto simp add: ring_simps norm_ge_zero) } ``` chaieb@29842 ` 1510` ``` then have th: "\i\ ?S. norm ((x\$i) *s f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" by metis ``` chaieb@29842 ` 1511` ``` from real_setsum_norm_le[OF fS, of "\i. (x\$i) *s (f (basis i))", OF th] ``` chaieb@29842 ` 1512` ``` have "norm (f x) \ ?B * norm x" unfolding th0 setsum_left_distrib by metis} ``` chaieb@29842 ` 1513` ``` then show ?thesis by blast ``` chaieb@29842 ` 1514` ```qed ``` chaieb@29842 ` 1515` chaieb@29842 ` 1516` ```lemma linear_bounded_pos: ``` chaieb@29842 ` 1517` ``` fixes f:: "real ^'n \ real ^ 'm" ``` chaieb@29842 ` 1518` ``` assumes lf: "linear f" ``` chaieb@29842 ` 1519` ``` shows "\B > 0. \x. norm (f x) \ B * norm x" ``` chaieb@29842 ` 1520` ```proof- ``` huffman@30489 ` 1521` ``` from linear_bounded[OF lf] obtain B where ``` chaieb@29842 ` 1522` ``` B: "\x. norm (f x) \ B * norm x" by blast ``` chaieb@29842 ` 1523` ``` let ?K = "\B\ + 1" ``` chaieb@29842 ` 1524` ``` have Kp: "?K > 0" by arith ``` chaieb@29842 ` 1525` ``` {assume C: "B < 0" ``` huffman@30041 ` 1526` ``` have "norm (1::real ^ 'n) > 0" by (simp add: zero_less_norm_iff) ``` chaieb@29842 ` 1527` ``` with C have "B * norm (1:: real ^ 'n) < 0" ``` chaieb@29842 ` 1528` ``` by (simp add: zero_compare_simps) ``` huffman@30041 ` 1529` ``` with B[rule_format, of 1] norm_ge_zero[of "f 1"] have False by simp ``` chaieb@29842 ` 1530` ``` } ``` chaieb@29842 ` 1531` ``` then have Bp: "B \ 0" by ferrack ``` chaieb@29842 ` 1532` ``` {fix x::"real ^ 'n" ``` chaieb@29842 ` 1533` ``` have "norm (f x) \ ?K * norm x" ``` huffman@30041 ` 1534` ``` using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp ``` huffman@30040 ` 1535` ``` apply (auto simp add: ring_simps split add: abs_split) ``` huffman@30040 ` 1536` ``` apply (erule order_trans, simp) ``` huffman@30040 ` 1537` ``` done ``` chaieb@29842 ` 1538` ``` } ``` chaieb@29842 ` 1539` ``` then show ?thesis using Kp by blast ``` chaieb@29842 ` 1540` ```qed ``` chaieb@29842 ` 1541` chaieb@29842 ` 1542` ```subsection{* Bilinear functions. *} ``` chaieb@29842 ` 1543` chaieb@29842 ` 1544` ```definition "bilinear f \ (\x. linear(\y. f x y)) \ (\y. linear(\x. f x y))" ``` chaieb@29842 ` 1545` chaieb@29842 ` 1546` ```lemma bilinear_ladd: "bilinear h ==> h (x + y) z = (h x z) + (h y z)" ``` chaieb@29842 ` 1547` ``` by (simp add: bilinear_def linear_def) ``` chaieb@29842 ` 1548` ```lemma bilinear_radd: "bilinear h ==> h x (y + z) = (h x y) + (h x z)" ``` chaieb@29842 ` 1549` ``` by (simp add: bilinear_def linear_def) ``` chaieb@29842 ` 1550` chaieb@29842 ` 1551` ```lemma bilinear_lmul: "bilinear h ==> h (c *s x) y = c *s (h x y)" ``` chaieb@29842 ` 1552` ``` by (simp add: bilinear_def linear_def) ``` chaieb@29842 ` 1553` chaieb@29842 ` 1554` ```lemma bilinear_rmul: "bilinear h ==> h x (c *s y) = c *s (h x y)" ``` chaieb@29842 ` 1555` ``` by (simp add: bilinear_def linear_def) ``` chaieb@29842 ` 1556` chaieb@29842 ` 1557` ```lemma bilinear_lneg: "bilinear h ==> h (- (x:: 'a::ring_1 ^ 'n)) y = -(h x y)" ``` chaieb@29842 ` 1558` ``` by (simp only: vector_sneg_minus1 bilinear_lmul) ``` chaieb@29842 ` 1559` chaieb@29842 ` 1560` ```lemma bilinear_rneg: "bilinear h ==> h x (- (y:: 'a::ring_1 ^ 'n)) = - h x y" ``` chaieb@29842 ` 1561` ``` by (simp only: vector_sneg_minus1 bilinear_rmul) ``` chaieb@29842 ` 1562` chaieb@29842 ` 1563` ```lemma (in ab_group_add) eq_add_iff: "x = x + y \ y = 0" ``` chaieb@29842 ` 1564` ``` using add_imp_eq[of x y 0] by auto ``` huffman@30489 ` 1565` huffman@30489 ` 1566` ```lemma bilinear_lzero: ``` chaieb@29842 ` 1567` ``` fixes h :: "'a::ring^'n \ _" assumes bh: "bilinear h" shows "h 0 x = 0" ``` huffman@30489 ` 1568` ``` using bilinear_ladd[OF bh, of 0 0 x] ``` chaieb@29842 ` 1569` ``` by (simp add: eq_add_iff ring_simps) ``` chaieb@29842 ` 1570` huffman@30489 ` 1571` ```lemma bilinear_rzero: ``` chaieb@29842 ` 1572` ``` fixes h :: "'a::ring^'n \ _" assumes bh: "bilinear h" shows "h x 0 = 0" ``` huffman@30489 ` 1573` ``` using bilinear_radd[OF bh, of x 0 0 ] ``` chaieb@29842 ` 1574` ``` by (simp add: eq_add_iff ring_simps) ``` chaieb@29842 ` 1575` chaieb@29842 ` 1576` ```lemma bilinear_lsub: "bilinear h ==> h (x - (y:: 'a::ring_1 ^ 'n)) z = h x z - h y z" ``` chaieb@29842 ` 1577` ``` by (simp add: diff_def bilinear_ladd bilinear_lneg) ``` chaieb@29842 ` 1578` chaieb@29842 ` 1579` ```lemma bilinear_rsub: "bilinear h ==> h z (x - (y:: 'a::ring_1 ^ 'n)) = h z x - h z y" ``` chaieb@29842 ` 1580` ``` by (simp add: diff_def bilinear_radd bilinear_rneg) ``` chaieb@29842 ` 1581` chaieb@29842 ` 1582` ```lemma bilinear_setsum: ``` chaieb@29842 ` 1583` ``` fixes h:: "'a ^'n \ 'a::semiring_1^'m \ 'a ^ 'k" ``` chaieb@29842 ` 1584` ``` assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T" ``` chaieb@29842 ` 1585` ``` shows "h (setsum f S) (setsum g T) = setsum (\(i,j). h (f i) (g j)) (S \ T) " ``` huffman@30489 ` 1586` ```proof- ``` chaieb@29842 ` 1587` ``` have "h (setsum f S) (setsum g T) = setsum (\x. h (f x) (setsum g T)) S" ``` chaieb@29842 ` 1588` ``` apply (rule linear_setsum[unfolded o_def]) ``` chaieb@29842 ` 1589` ``` using bh fS by (auto simp add: bilinear_def) ``` chaieb@29842 ` 1590` ``` also have "\ = setsum (\x. setsum (\y. h (f x) (g y)) T) S" ``` chaieb@29842 ` 1591` ``` apply (rule setsum_cong, simp) ``` chaieb@29842 ` 1592` ``` apply (rule linear_setsum[unfolded o_def]) ``` chaieb@29842 ` 1593` ``` using bh fT by (auto simp add: bilinear_def) ``` chaieb@29842 ` 1594` ``` finally show ?thesis unfolding setsum_cartesian_product . ``` chaieb@29842 ` 1595` ```qed ``` chaieb@29842 ` 1596` chaieb@29842 ` 1597` ```lemma bilinear_bounded: ``` chaieb@29842 ` 1598` ``` fixes h:: "real ^'m \ real^'n \ real ^ 'k" ``` chaieb@29842 ` 1599` ``` assumes bh: "bilinear h" ``` chaieb@29842 ` 1600` ``` shows "\B. \x y. norm (h x y) \ B * norm x * norm y" ``` huffman@30489 ` 1601` ```proof- ``` chaieb@29842 ` 1602` ``` let ?M = "{1 .. dimindex (UNIV :: 'm set)}" ``` chaieb@29842 ` 1603` ``` let ?N = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29842 ` 1604` ``` let ?B = "setsum (\(i,j). norm (h (basis i) (basis j))) (?M \ ?N)" ``` chaieb@29842 ` 1605` ``` have fM: "finite ?M" and fN: "finite ?N" by simp_all ``` chaieb@29842 ` 1606` ``` {fix x:: "real ^ 'm" and y :: "real^'n" ``` chaieb@29842 ` 1607` ``` have "norm (h x y) = norm (h (setsum (\i. (x\$i) *s basis i) ?M) (setsum (\i. (y\$i) *s basis i) ?N))" unfolding basis_expansion .. ``` chaieb@29842 ` 1608` ``` also have "\ = norm (setsum (\ (i,j). h ((x\$i) *s basis i) ((y\$j) *s basis j)) (?M \ ?N))" unfolding bilinear_setsum[OF bh fM fN] .. ``` chaieb@29842 ` 1609` ``` finally have th: "norm (h x y) = \" . ``` chaieb@29842 ` 1610` ``` have "norm (h x y) \ ?B * norm x * norm y" ``` chaieb@29842 ` 1611` ``` apply (simp add: setsum_left_distrib th) ``` chaieb@29842 ` 1612` ``` apply (rule real_setsum_norm_le) ``` chaieb@29842 ` 1613` ``` using fN fM ``` chaieb@29842 ` 1614` ``` apply simp ``` chaieb@29842 ` 1615` ``` apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul ring_simps) ``` chaieb@29842 ` 1616` ``` apply (rule mult_mono) ``` huffman@30041 ` 1617` ``` apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm) ``` chaieb@29842 ` 1618` ``` apply (rule mult_mono) ``` huffman@30041 ` 1619` ``` apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm) ``` chaieb@29842 ` 1620` ``` done} ``` chaieb@29842 ` 1621` ``` then show ?thesis by metis ``` chaieb@29842 ` 1622` ```qed ``` chaieb@29842 ` 1623` chaieb@29842 ` 1624` ```lemma bilinear_bounded_pos: ``` chaieb@29842 ` 1625` ``` fixes h:: "real ^'m \ real^'n \ real ^ 'k" ``` chaieb@29842 ` 1626` ``` assumes bh: "bilinear h" ``` chaieb@29842 ` 1627` ``` shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y" ``` chaieb@29842 ` 1628` ```proof- ``` huffman@30489 ` 1629` ``` from bilinear_bounded[OF bh] obtain B where ``` chaieb@29842 ` 1630` ``` B: "\x y. norm (h x y) \ B * norm x * norm y" by blast ``` chaieb@29842 ` 1631` ``` let ?K = "\B\ + 1" ``` chaieb@29842 ` 1632` ``` have Kp: "?K > 0" by arith ``` chaieb@29842 ` 1633` ``` have KB: "B < ?K" by arith ``` chaieb@29842 ` 1634` ``` {fix x::"real ^'m" and y :: "real ^'n" ``` chaieb@29842 ` 1635` ``` from KB Kp ``` chaieb@29842 ` 1636` ``` have "B * norm x * norm y \ ?K * norm x * norm y" ``` huffman@30489 ` 1637` ``` apply - ``` chaieb@29842 ` 1638` ``` apply (rule mult_right_mono, rule mult_right_mono) ``` huffman@30041 ` 1639` ``` by (auto simp add: norm_ge_zero) ``` chaieb@29842 ` 1640` ``` then have "norm (h x y) \ ?K * norm x * norm y" ``` huffman@30489 ` 1641` ``` using B[rule_format, of x y] by simp} ``` chaieb@29842 ` 1642` ``` with Kp show ?thesis by blast ``` chaieb@29842 ` 1643` ```qed ``` chaieb@29842 ` 1644` chaieb@29842 ` 1645` ```subsection{* Adjoints. *} ``` chaieb@29842 ` 1646` chaieb@29842 ` 1647` ```definition "adjoint f = (SOME f'. \x y. f x \ y = x \ f' y)" ``` chaieb@29842 ` 1648` chaieb@29842 ` 1649` ```lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis ``` chaieb@29842 ` 1650` chaieb@29842 ` 1651` ```lemma adjoint_works_lemma: ``` chaieb@29842 ` 1652` ``` fixes f:: "'a::ring_1 ^'n \ 'a ^ 'm" ``` chaieb@29842 ` 1653` ``` assumes lf: "linear f" ``` chaieb@29842 ` 1654` ``` shows "\x y. f x \ y = x \ adjoint f y" ``` chaieb@29842 ` 1655` ```proof- ``` chaieb@29842 ` 1656` ``` let ?N = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29842 ` 1657` ``` let ?M = "{1 .. dimindex (UNIV :: 'm set)}" ``` chaieb@29842 ` 1658` ``` have fN: "finite ?N" by simp ``` chaieb@29842 ` 1659` ``` have fM: "finite ?M" by simp ``` chaieb@29842 ` 1660` ``` {fix y:: "'a ^ 'm" ``` chaieb@29842 ` 1661` ``` let ?w = "(\ i. (f (basis i) \ y)) :: 'a ^ 'n" ``` chaieb@29842 ` 1662` ``` {fix x ``` chaieb@29842 ` 1663` ``` have "f x \ y = f (setsum (\i. (x\$i) *s basis i) ?N) \ y" ``` chaieb@29842 ` 1664` ``` by (simp only: basis_expansion) ``` chaieb@29842 ` 1665` ``` also have "\ = (setsum (\i. (x\$i) *s f (basis i)) ?N) \ y" ``` huffman@30489 ` 1666` ``` unfolding linear_setsum[OF lf fN] ``` chaieb@29842 ` 1667` ``` by (simp add: linear_cmul[OF lf]) ``` chaieb@29842 ` 1668` ``` finally have "f x \ y = x \ ?w" ``` chaieb@29842 ` 1669` ``` apply (simp only: ) ``` chaieb@29842 ` 1670` ``` apply (simp add: dot_def setsum_component Cart_lambda_beta setsum_left_distrib setsum_right_distrib vector_component setsum_commute[of _ ?M ?N] ring_simps del: One_nat_def) ``` chaieb@29842 ` 1671` ``` done} ``` chaieb@29842 ` 1672` ``` } ``` huffman@30489 ` 1673` ``` then show ?thesis unfolding adjoint_def ``` chaieb@29842 ` 1674` ``` some_eq_ex[of "\f'. \x y. f x \ y = x \ f' y"] ``` chaieb@29842 ` 1675` ``` using choice_iff[of "\a b. \x. f x \ a = x \ b "] ``` chaieb@29842 ` 1676` ``` by metis ``` chaieb@29842 ` 1677` ```qed ``` chaieb@29842 ` 1678` chaieb@29842 ` 1679` ```lemma adjoint_works: ``` chaieb@29842 ` 1680` ``` fixes f:: "'a::ring_1 ^'n \ 'a ^ 'm" ``` chaieb@29842 ` 1681` ``` assumes lf: "linear f" ``` chaieb@29842 ` 1682` ``` shows "x \ adjoint f y = f x \ y" ``` chaieb@29842 ` 1683` ``` using adjoint_works_lemma[OF lf] by metis ``` chaieb@29842 ` 1684` chaieb@29842 ` 1685` chaieb@29842 ` 1686` ```lemma adjoint_linear: ``` chaieb@29842 ` 1687` ``` fixes f :: "'a::comm_ring_1 ^'n \ 'a ^ 'm" ``` chaieb@29842 ` 1688` ``` assumes lf: "linear f" ``` chaieb@29842 ` 1689` ``` shows "linear (adjoint f)" ``` chaieb@29842 ` 1690` ``` by (simp add: linear_def vector_eq_ldot[symmetric] dot_radd dot_rmult adjoint_works[OF lf]) ``` chaieb@29842 ` 1691` chaieb@29842 ` 1692` ```lemma adjoint_clauses: ``` chaieb@29842 ` 1693` ``` fixes f:: "'a::comm_ring_1 ^'n \ 'a ^ 'm" ``` chaieb@29842 ` 1694` ``` assumes lf: "linear f" ``` chaieb@29842 ` 1695` ``` shows "x \ adjoint f y = f x \ y" ``` chaieb@29842 ` 1696` ``` and "adjoint f y \ x = y \ f x" ``` chaieb@29842 ` 1697` ``` by (simp_all add: adjoint_works[OF lf] dot_sym ) ``` chaieb@29842 ` 1698` chaieb@29842 ` 1699` ```lemma adjoint_adjoint: ``` chaieb@29842 ` 1700` ``` fixes f:: "'a::comm_ring_1 ^ 'n \ _" ``` chaieb@29842 ` 1701` ``` assumes lf: "linear f" ``` chaieb@29842 ` 1702` ``` shows "adjoint (adjoint f) = f" ``` chaieb@29842 ` 1703` ``` apply (rule ext) ``` chaieb@29842 ` 1704` ``` by (simp add: vector_eq_ldot[symmetric] adjoint_clauses[OF adjoint_linear[OF lf]] adjoint_clauses[OF lf]) ``` chaieb@29842 ` 1705` chaieb@29842 ` 1706` ```lemma adjoint_unique: ``` chaieb@29842 ` 1707` ``` fixes f:: "'a::comm_ring_1 ^ 'n \ 'a ^ 'm" ``` chaieb@29842 ` 1708` ``` assumes lf: "linear f" and u: "\x y. f' x \ y = x \ f y" ``` chaieb@29842 ` 1709` ``` shows "f' = adjoint f" ``` chaieb@29842 ` 1710` ``` apply (rule ext) ``` chaieb@29842 ` 1711` ``` using u ``` chaieb@29842 ` 1712` ``` by (simp add: vector_eq_rdot[symmetric] adjoint_clauses[OF lf]) ``` chaieb@29842 ` 1713` huffman@29881 ` 1714` ```text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *} ``` chaieb@29842 ` 1715` chaieb@29842 ` 1716` ```consts generic_mult :: "'a \ 'b \ 'c" (infixr "\" 75) ``` chaieb@29842 ` 1717` huffman@30489 ` 1718` ```defs (overloaded) ``` chaieb@29842 ` 1719` ```matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^'n^'m) \ (m' :: 'a ^'p^'n) \ (\ i j. setsum (\k. ((m\$i)\$k) * ((m'\$k)\$j)) {1 .. dimindex (UNIV :: 'n set)}) ::'a ^ 'p ^'m" ``` chaieb@29842 ` 1720` huffman@30489 ` 1721` ```abbreviation ``` chaieb@29842 ` 1722` ``` matrix_matrix_mult' :: "('a::semiring_1) ^'n^'m \ 'a ^'p^'n \ 'a ^ 'p ^'m" (infixl "**" 70) ``` chaieb@29842 ` 1723` ``` where "m ** m' == m\ m'" ``` chaieb@29842 ` 1724` huffman@30489 ` 1725` ```defs (overloaded) ``` chaieb@29842 ` 1726` ``` matrix_vector_mult_def: "(m::('a::semiring_1) ^'n^'m) \ (x::'a ^'n) \ (\ i. setsum (\j. ((m\$i)\$j) * (x\$j)) {1..dimindex(UNIV ::'n set)}) :: 'a^'m" ``` chaieb@29842 ` 1727` huffman@30489 ` 1728` ```abbreviation ``` chaieb@29842 ` 1729` ``` matrix_vector_mult' :: "('a::semiring_1) ^'n^'m \ 'a ^'n \ 'a ^ 'm" (infixl "*v" 70) ``` huffman@30489 ` 1730` ``` where ``` chaieb@29842 ` 1731` ``` "m *v v == m \ v" ``` chaieb@29842 ` 1732` huffman@30489 ` 1733` ```defs (overloaded) ``` chaieb@29842 ` 1734` ``` vector_matrix_mult_def: "(x::'a^'m) \ (m::('a::semiring_1) ^'n^'m) \ (\ j. setsum (\i. ((m\$i)\$j) * (x\$i)) {1..dimindex(UNIV :: 'm set)}) :: 'a^'n" ``` chaieb@29842 ` 1735` huffman@30489 ` 1736` ```abbreviation ``` chaieb@29842 ` 1737` ``` vactor_matrix_mult' :: "'a ^ 'm \ ('a::semiring_1) ^'n^'m \ 'a ^'n " (infixl "v*" 70) ``` huffman@30489 ` 1738` ``` where ``` chaieb@29842 ` 1739` ``` "v v* m == v \ m" ``` chaieb@29842 ` 1740` chaieb@29842 ` 1741` ```definition "(mat::'a::zero => 'a ^'n^'m) k = (\ i j. if i = j then k else 0)" ``` chaieb@29842 ` 1742` ```definition "(transp::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A\$j)\$i))" ``` chaieb@29842 ` 1743` ```definition "(row::nat => 'a ^'n^'m \ 'a ^'n) i A = (\ j. ((A\$i)\$j))" ``` chaieb@29842 ` 1744` ```definition "(column::nat =>'a^'n^'m =>'a^'m) j A = (\ i. ((A\$i)\$j))" ``` chaieb@29842 ` 1745` ```definition "rows(A::'a^'n^'m) = { row i A | i. i \ {1 .. dimindex(UNIV :: 'm set)}}" ``` chaieb@29842 ` 1746` ```definition "columns(A::'a^'n^'m) = { column i A | i. i \ {1 .. dimindex(UNIV :: 'n set)}}" ``` chaieb@29842 ` 1747` chaieb@29842 ` 1748` ```lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) ``` chaieb@29842 ` 1749` ```lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \ B) + (A \ C)" ``` chaieb@29842 ` 1750` ``` by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps) ``` chaieb@29842 ` 1751` huffman@30489 ` 1752` ```lemma setsum_delta': ``` huffman@30489 ` 1753` ``` assumes fS: "finite S" shows ``` huffman@30489 ` 1754` ``` "setsum (\k. if a = k then b k else 0) S = ``` chaieb@29842 ` 1755` ``` (if a\ S then b a else 0)" ``` huffman@30489 ` 1756` ``` using setsum_delta[OF fS, of a b, symmetric] ``` chaieb@29842 ` 1757` ``` by (auto intro: setsum_cong) ``` chaieb@29842 ` 1758` chaieb@29842 ` 1759` ```lemma matrix_mul_lid: "mat 1 ** A = A" ``` chaieb@29842 ` 1760` ``` apply (simp add: matrix_matrix_mult_def mat_def) ``` chaieb@29842 ` 1761` ``` apply vector ``` chaieb@29842 ` 1762` ``` by (auto simp only: cond_value_iff cond_application_beta setsum_delta'[OF finite_atLeastAtMost] mult_1_left mult_zero_left if_True) ``` chaieb@29842 ` 1763` chaieb@29842 ` 1764` chaieb@29842 ` 1765` ```lemma matrix_mul_rid: "A ** mat 1 = A" ``` chaieb@29842 ` 1766` ``` apply (simp add: matrix_matrix_mult_def mat_def) ``` chaieb@29842 ` 1767` ``` apply vector ``` chaieb@29842 ` 1768` ``` by (auto simp only: cond_value_iff cond_application_beta setsum_delta[OF finite_atLeastAtMost] mult_1_right mult_zero_right if_True cong: if_cong) ``` chaieb@29842 ` 1769` chaieb@29842 ` 1770` ```lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" ``` chaieb@29842 ` 1771` ``` apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc) ``` chaieb@29842 ` 1772` ``` apply (subst setsum_commute) ``` chaieb@29842 ` 1773` ``` apply simp ``` chaieb@29842 ` 1774` ``` done ``` chaieb@29842 ` 1775` chaieb@29842 ` 1776` ```lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" ``` chaieb@29842 ` 1777` ``` apply (vector matrix_matrix_mult_def matrix_vector_mult_def setsum_right_distrib setsum_left_distrib mult_assoc) ``` chaieb@29842 ` 1778` ``` apply (subst setsum_commute) ``` chaieb@29842 ` 1779` ``` apply simp ``` chaieb@29842 ` 1780` ``` done ``` chaieb@29842 ` 1781` chaieb@29842 ` 1782` ```lemma matrix_vector_mul_lid: "mat 1 *v x = x" ``` chaieb@29842 ` 1783` ``` apply (vector matrix_vector_mult_def mat_def) ``` huffman@30489 ` 1784` ``` by (simp add: cond_value_iff cond_application_beta ``` chaieb@29842 ` 1785` ``` setsum_delta' cong del: if_weak_cong) ``` chaieb@29842 ` 1786` chaieb@29842 ` 1787` ```lemma matrix_transp_mul: "transp(A ** B) = transp B ** transp (A::'a::comm_semiring_1^'m^'n)" ``` chaieb@29842 ` 1788` ``` by (simp add: matrix_matrix_mult_def transp_def Cart_eq Cart_lambda_beta mult_commute) ``` chaieb@29842 ` 1789` chaieb@29842 ` 1790` ```lemma matrix_eq: "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") ``` chaieb@29842 ` 1791` ``` apply auto ``` chaieb@29842 ` 1792` ``` apply (subst Cart_eq) ``` chaieb@29842 ` 1793` ``` apply clarify ``` chaieb@29842 ` 1794` ``` apply (clarsimp simp add: matrix_vector_mult_def basis_def cond_value_iff cond_application_beta Cart_eq Cart_lambda_beta cong del: if_weak_cong) ``` chaieb@29842 ` 1795` ``` apply (erule_tac x="basis ia" in allE) ``` chaieb@29842 ` 1796` ``` apply (erule_tac x="i" in ballE) ``` chaieb@29842 ` 1797` ``` by (auto simp add: basis_def cond_value_iff cond_application_beta Cart_lambda_beta setsum_delta[OF finite_atLeastAtMost] cong del: if_weak_cong) ``` chaieb@29842 ` 1798` huffman@30489 ` 1799` ```lemma matrix_vector_mul_component: ``` chaieb@29842 ` 1800` ``` assumes k: "k \ {1.. dimindex (UNIV :: 'm set)}" ``` chaieb@29842 ` 1801` ``` shows "((A::'a::semiring_1^'n'^'m) *v x)\$k = (A\$k) \ x" ``` chaieb@29842 ` 1802` ``` using k ``` chaieb@29842 ` 1803` ``` by (simp add: matrix_vector_mult_def Cart_lambda_beta dot_def) ``` chaieb@29842 ` 1804` chaieb@29842 ` 1805` ```lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^'n) v* A) \ y = x \ (A *v y)" ``` chaieb@29842 ` 1806` ``` apply (simp add: dot_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib Cart_lambda_beta mult_ac) ``` chaieb@29842 ` 1807` ``` apply (subst setsum_commute) ``` chaieb@29842 ` 1808` ``` by simp ``` chaieb@29842 ` 1809` chaieb@29842 ` 1810` ```lemma transp_mat: "transp (mat n) = mat n" ``` chaieb@29842 ` 1811` ``` by (vector transp_def mat_def) ``` chaieb@29842 ` 1812` chaieb@29842 ` 1813` ```lemma transp_transp: "transp(transp A) = A" ``` chaieb@29842 ` 1814` ``` by (vector transp_def) ``` chaieb@29842 ` 1815` huffman@30489 ` 1816` ```lemma row_transp: ``` chaieb@29842 ` 1817` ``` fixes A:: "'a::semiring_1^'n^'m" ``` chaieb@29842 ` 1818` ``` assumes i: "i \ {1.. dimindex (UNIV :: 'n set)}" ``` chaieb@29842 ` 1819` ``` shows "row i (transp A) = column i A" ``` huffman@30489 ` 1820` ``` using i ``` chaieb@29842 ` 1821` ``` by (simp add: row_def column_def transp_def Cart_eq Cart_lambda_beta) ``` chaieb@29842 ` 1822` chaieb@29842 ` 1823` ```lemma column_transp: ``` chaieb@29842 ` 1824` ``` fixes A:: "'a::semiring_1^'n^'m" ``` chaieb@29842 ` 1825` ``` assumes i: "i \ {1.. dimindex (UNIV :: 'm set)}" ``` chaieb@29842 ` 1826` ``` shows "column i (transp A) = row i A" ``` huffman@30489 ` 1827` ``` using i ``` chaieb@29842 ` 1828` ``` by (simp add: row_def column_def transp_def Cart_eq Cart_lambda_beta) ``` chaieb@29842 ` 1829` chaieb@29842 ` 1830` ```lemma rows_transp: "rows(transp (A::'a::semiring_1^'n^'m)) = columns A" ``` chaieb@29842 ` 1831` ```apply (auto simp add: rows_def columns_def row_transp intro: set_ext) ``` chaieb@29842 ` 1832` ```apply (rule_tac x=i in exI) ``` chaieb@29842 ` 1833` ```apply (auto simp add: row_transp) ``` chaieb@29842 ` 1834` ```done ``` chaieb@29842 ` 1835` chaieb@29842 ` 1836` ```lemma columns_transp: "columns(transp (A::'a::semiring_1^'n^'m)) = rows A" by (metis transp_transp rows_transp) ``` chaieb@29842 ` 1837` chaieb@29842 ` 1838` ```text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *} ``` chaieb@29842 ` 1839` chaieb@29842 ` 1840` ```lemma matrix_mult_dot: "A *v x = (\ i. A\$i \ x)" ``` chaieb@29842 ` 1841` ``` by (simp add: matrix_vector_mult_def dot_def) ``` chaieb@29842 ` 1842` chaieb@29842 ` 1843` ```lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\i. (x\$i) *s column i A) {1 .. dimindex(UNIV:: 'n set)}" ``` chaieb@29842 ` 1844` ``` by (simp add: matrix_vector_mult_def Cart_eq setsum_component Cart_lambda_beta vector_component column_def mult_commute) ``` chaieb@29842 ` 1845` chaieb@29842 ` 1846` ```lemma vector_componentwise: ``` chaieb@29842 ` 1847` ``` "(x::'a::ring_1^'n) = (\ j. setsum (\i. (x\$i) * (basis i :: 'a^'n)\$j) {1..dimindex(UNIV :: 'n set)})" ``` chaieb@29842 ` 1848` ``` apply (subst basis_expansion[symmetric]) ``` chaieb@29842 ` 1849` ``` by (vector Cart_eq Cart_lambda_beta setsum_component) ``` chaieb@29842 ` 1850` chaieb@29842 ` 1851` ```lemma linear_componentwise: ``` chaieb@29842 ` 1852` ``` fixes f:: "'a::ring_1 ^ 'm \ 'a ^ 'n" ``` chaieb@29842 ` 1853` ``` assumes lf: "linear f" and j: "j \ {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29842 ` 1854` ``` shows "(f x)\$j = setsum (\i. (x\$i) * (f (basis i)\$j)) {1 .. dimindex (UNIV :: 'm set)}" (is "?lhs = ?rhs") ``` chaieb@29842 ` 1855` ```proof- ``` chaieb@29842 ` 1856` ``` let ?M = "{1 .. dimindex (UNIV :: 'm set)}" ``` chaieb@29842 ` 1857` ``` let ?N = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29842 ` 1858` ``` have fM: "finite ?M" by simp ``` chaieb@29842 ` 1859` ``` have "?rhs = (setsum (\i.(x\$i) *s f (basis i) ) ?M)\$j" ``` chaieb@29842 ` 1860` ``` unfolding vector_smult_component[OF j, symmetric] ``` chaieb@29842 ` 1861` ``` unfolding setsum_component[OF j, of "(\i.(x\$i) *s f (basis i :: 'a^'m))" ?M] ``` chaieb@29842 ` 1862` ``` .. ``` chaieb@29842 ` 1863` ``` then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion .. ``` chaieb@29842 ` 1864` ```qed ``` chaieb@29842 ` 1865` chaieb@29842 ` 1866` ```text{* Inverse matrices (not necessarily square) *} ``` chaieb@29842 ` 1867` chaieb@29842 ` 1868` ```definition "invertible(A::'a::semiring_1^'n^'m) \ (\A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" ``` chaieb@29842 ` 1869` chaieb@29842 ` 1870` ```definition "matrix_inv(A:: 'a::semiring_1^'n^'m) = ``` chaieb@29842 ` 1871` ``` (SOME A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" ``` chaieb@29842 ` 1872` chaieb@29842 ` 1873` ```text{* Correspondence between matrices and linear operators. *} ``` chaieb@29842 ` 1874` chaieb@29842 ` 1875` ```definition matrix:: "('a::{plus,times, one, zero}^'m \ 'a ^ 'n) \ 'a^'m^'n" ``` chaieb@29842 ` 1876` ```where "matrix f = (\ i j. (f(basis j))\$i)" ``` chaieb@29842 ` 1877` chaieb@29842 ` 1878` ```lemma matrix_vector_mul_linear: "linear(\x. A *v (x::'a::comm_semiring_1 ^ 'n))" ``` chaieb@29842 ` 1879` ``` by (simp add: linear_def matrix_vector_mult_def Cart_eq Cart_lambda_beta vector_component ring_simps setsum_right_distrib setsum_addf) ``` chaieb@29842 ` 1880` chaieb@29842 ` 1881` ```lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n)" ``` chaieb@29842 ` 1882` ```apply (simp add: matrix_def matrix_vector_mult_def Cart_eq Cart_lambda_beta mult_commute del: One_nat_def) ``` chaieb@29842 ` 1883` ```apply clarify ``` chaieb@29842 ` 1884` ```apply (rule linear_componentwise[OF lf, symmetric]) ``` chaieb@29842 ` 1885` ```apply simp ``` chaieb@29842 ` 1886` ```done ``` chaieb@29842 ` 1887` chaieb@29842 ` 1888` ```lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::'a::comm_ring_1 ^ 'n))" by (simp add: ext matrix_works) ``` chaieb@29842 ` 1889` chaieb@29842 ` 1890` ```lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: 'a:: comm_ring_1 ^ 'n)) = A" ``` chaieb@29842 ` 1891` ``` by (simp add: matrix_eq matrix_vector_mul_linear matrix_works) ``` chaieb@29842 ` 1892` huffman@30489 ` 1893` ```lemma matrix_compose: ``` huffman@30489 ` 1894` ``` assumes lf: "linear (f::'a::comm_ring_1^'n \ _)" and lg: "linear g" ``` chaieb@29842 ` 1895` ``` shows "matrix (g o f) = matrix g ** matrix f" ``` chaieb@29842 ` 1896` ``` using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]] ``` chaieb@29842 ` 1897` ``` by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) ``` chaieb@29842 ` 1898` chaieb@29842 ` 1899` ```lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\i. (x\$i) *s ((transp A)\$i)) {1..dimindex(UNIV:: 'n set)}" ``` chaieb@29842 ` 1900` ``` by (simp add: matrix_vector_mult_def transp_def Cart_eq Cart_lambda_beta setsum_component vector_component mult_commute) ``` chaieb@29842 ` 1901` chaieb@29842 ` 1902` ```lemma adjoint_matrix: "adjoint(\x. (A::'a::comm_ring_1^'n^'m) *v x) = (\x. transp A *v x)" ``` chaieb@29842 ` 1903` ``` apply (rule adjoint_unique[symmetric]) ``` chaieb@29842 ` 1904` ``` apply (rule matrix_vector_mul_linear) ``` chaieb@29842 ` 1905` ``` apply (simp add: transp_def dot_def Cart_lambda_beta matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) ``` chaieb@29842 ` 1906` ``` apply (subst setsum_commute) ``` chaieb@29842 ` 1907` ``` apply (auto simp add: mult_ac) ``` chaieb@29842 ` 1908` ``` done ``` chaieb@29842 ` 1909` chaieb@29842 ` 1910` ```lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \ 'a ^ 'm)" ``` chaieb@29842 ` 1911` ``` shows "matrix(adjoint f) = transp(matrix f)" ``` chaieb@29842 ` 1912` ``` apply (subst matrix_vector_mul[OF lf]) ``` chaieb@29842 ` 1913` ``` unfolding adjoint_matrix matrix_of_matrix_vector_mul .. ``` chaieb@29842 ` 1914` chaieb@29842 ` 1915` ```subsection{* Interlude: Some properties of real sets *} ``` chaieb@29842 ` 1916` chaieb@29842 ` 1917` ```lemma seq_mono_lemma: assumes "\(n::nat) \ m. (d n :: real) < e n" and "\n \ m. e n <= e m" ``` chaieb@29842 ` 1918` ``` shows "\n \ m. d n < e m" ``` chaieb@29842 ` 1919` ``` using prems apply auto ``` chaieb@29842 ` 1920` ``` apply (erule_tac x="n" in allE) ``` chaieb@29842 ` 1921` ``` apply (erule_tac x="n" in allE) ``` chaieb@29842 ` 1922` ``` apply auto ``` chaieb@29842 ` 1923` ``` done ``` chaieb@29842 ` 1924` chaieb@29842 ` 1925` huffman@30489 ` 1926` ```lemma real_convex_bound_lt: ``` chaieb@29842 ` 1927` ``` assumes xa: "(x::real) < a" and ya: "y < a" and u: "0 <= u" and v: "0 <= v" ``` huffman@30489 ` 1928` ``` and uv: "u + v = 1" ``` chaieb@29842 ` 1929` ``` shows "u * x + v * y < a" ``` chaieb@29842 ` 1930` ```proof- ``` chaieb@29842 ` 1931` ``` have uv': "u = 0 \ v \ 0" using u v uv by arith ``` chaieb@29842 ` 1932` ``` have "a = a * (u + v)" unfolding uv by simp ``` chaieb@29842 ` 1933` ``` hence th: "u * a + v * a = a" by (simp add: ring_simps) ``` chaieb@29842 ` 1934` ``` from xa u have "u \ 0 \ u*x < u*a" by (simp add: mult_compare_simps) ``` chaieb@29842 ` 1935` ``` from ya v have "v \ 0 \ v * y < v * a" by (simp add: mult_compare_simps) ``` chaieb@29842 ` 1936` ``` from xa ya u v have "u * x + v * y < u * a + v * a" ``` chaieb@29842 ` 1937` ``` apply (cases "u = 0", simp_all add: uv') ``` chaieb@29842 ` 1938` ``` apply(rule mult_strict_left_mono) ``` chaieb@29842 ` 1939` ``` using uv' apply simp_all ``` huffman@30489 ` 1940` chaieb@29842 ` 1941` ``` apply (rule add_less_le_mono) ``` chaieb@29842 ` 1942` ``` apply(rule mult_strict_left_mono) ``` chaieb@29842 ` 1943` ``` apply simp_all ``` chaieb@29842 ` 1944` ``` apply (rule mult_left_mono) ``` chaieb@29842 ` 1945` ``` apply simp_all ``` chaieb@29842 ` 1946` ``` done ``` chaieb@29842 ` 1947` ``` thus ?thesis unfolding th . ``` chaieb@29842 ` 1948` ```qed ``` chaieb@29842 ` 1949` huffman@30489 ` 1950` ```lemma real_convex_bound_le: ``` chaieb@29842 ` 1951` ``` assumes xa: "(x::real) \ a" and ya: "y \ a" and u: "0 <= u" and v: "0 <= v" ``` huffman@30489 ` 1952` ``` and uv: "u + v = 1" ``` chaieb@29842 ` 1953` ``` shows "u * x + v * y \ a" ``` chaieb@29842 ` 1954` ```proof- ``` chaieb@29842 ` 1955` ``` from xa ya u v have "u * x + v * y \ u * a + v * a" by (simp add: add_mono mult_left_mono) ``` chaieb@29842 ` 1956` ``` also have "\ \ (u + v) * a" by (simp add: ring_simps) ``` chaieb@29842 ` 1957` ``` finally show ?thesis unfolding uv by simp ``` chaieb@29842 ` 1958` ```qed ``` chaieb@29842 ` 1959` chaieb@29842 ` 1960` ```lemma infinite_enumerate: assumes fS: "infinite S" ``` chaieb@29842 ` 1961` ``` shows "\r. subseq r \ (\n. r n \ S)" ``` chaieb@29842 ` 1962` ```unfolding subseq_def ``` chaieb@29842 ` 1963` ```using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto ``` chaieb@29842 ` 1964` chaieb@29842 ` 1965` ```lemma approachable_lt_le: "(\(d::real)>0. \x. f x < d \ P x) \ (\d>0. \x. f x \ d \ P x)" ``` chaieb@29842 ` 1966` ```apply auto ``` chaieb@29842 ` 1967` ```apply (rule_tac x="d/2" in exI) ``` chaieb@29842 ` 1968` ```apply auto ``` chaieb@29842 ` 1969` ```done ``` chaieb@29842 ` 1970` chaieb@29842 ` 1971` huffman@30489 ` 1972` ```lemma triangle_lemma: ``` chaieb@29842 ` 1973` ``` assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2" ``` chaieb@29842 ` 1974` ``` shows "x <= y + z" ``` chaieb@29842 ` 1975` ```proof- ``` chaieb@29842 ` 1976` ``` have "y^2 + z^2 \ y^2 + 2*y*z + z^2" using z y by (simp add: zero_compare_simps) ``` chaieb@29842 ` 1977` ``` with xy have th: "x ^2 \ (y+z)^2" by (simp add: power2_eq_square ring_simps) ``` chaieb@29842 ` 1978` ``` from y z have yz: "y + z \ 0" by arith ``` chaieb@29842 ` 1979` ``` from power2_le_imp_le[OF th yz] show ?thesis . ``` chaieb@29842 ` 1980` ```qed ``` chaieb@29842 ` 1981` chaieb@29842 ` 1982` chaieb@29842 ` 1983` ```lemma lambda_skolem: "(\i \ {1 .. dimindex(UNIV :: 'n set)}. \x. P i x) \ ``` chaieb@29842 ` 1984` ``` (\x::'a ^ 'n. \i \ {1 .. dimindex(UNIV:: 'n set)}. P i (x\$i))" (is "?lhs \ ?rhs") ``` chaieb@29842 ` 1985` ```proof- ``` chaieb@29842 ` 1986` ``` let ?S = "{1 .. dimindex(UNIV :: 'n set)}" ``` chaieb@29842 ` 1987` ``` {assume H: "?rhs" ``` chaieb@29842 ` 1988` ``` then have ?lhs by auto} ``` chaieb@29842 ` 1989` ``` moreover ``` chaieb@29842 ` 1990` ``` {assume H: "?lhs" ``` chaieb@29842 ` 1991` ``` then obtain f where f:"\i\ ?S. P i (f i)" unfolding Ball_def choice_iff by metis ``` chaieb@29842 ` 1992` ``` let ?x = "(\ i. (f i)) :: 'a ^ 'n" ``` chaieb@29842 ` 1993` ``` {fix i assume i: "i \ ?S" ``` chaieb@29842 ` 1994` ``` with f i have "P i (f i)" by metis ``` huffman@30489 ` 1995` ``` then have "P i (?x\$i)" using Cart_lambda_beta[of f, rule_format, OF i] by auto ``` chaieb@29842 ` 1996` ``` } ``` chaieb@29842 ` 1997` ``` hence "\i \ ?S. P i (?x\$i)" by metis ``` chaieb@29842 ` 1998` ``` hence ?rhs by metis } ``` chaieb@29842 ` 1999` ``` ultimately show ?thesis by metis ``` huffman@30489 ` 2000` ```qed ``` chaieb@29842 ` 2001` chaieb@29842 ` 2002` ```(* Supremum and infimum of real sets *) ``` chaieb@29842 ` 2003` chaieb@29842 ` 2004` chaieb@29842 ` 2005` ```definition rsup:: "real set \ real" where ``` chaieb@29842 ` 2006` ``` "rsup S = (SOME a. isLub UNIV S a)" ``` chaieb@29842 ` 2007` chaieb@29842 ` 2008` ```lemma rsup_alt: "rsup S = (SOME a. (\x \ S. x \ a) \ (\b. (\x \ S. x \ b) \ a \ b))" by (auto simp add: isLub_def rsup_def leastP_def isUb_def setle_def setge_def) ``` chaieb@29842 ` 2009` chaieb@29842 ` 2010` ```lemma rsup: assumes Se: "S \ {}" and b: "\b. S *<= b" ``` chaieb@29842 ` 2011` ``` shows "isLub UNIV S (rsup S)" ``` chaieb@29842 ` 2012` ```using Se b ``` chaieb@29842 ` 2013` ```unfolding rsup_def ``` chaieb@29842 ` 2014` ```apply clarify ``` chaieb@29842 ` 2015` ```apply (rule someI_ex) ``` chaieb@29842 ` 2016` ```apply (rule reals_complete) ``` chaieb@29842 ` 2017` ```by (auto simp add: isUb_def setle_def) ``` chaieb@29842 ` 2018` chaieb@29842 ` 2019` ```lemma rsup_le: assumes Se: "S \ {}" and Sb: "S *<= b" shows "rsup S \ b" ``` chaieb@29842 ` 2020` ```proof- ``` chaieb@29842 ` 2021` ``` from Sb have bu: "isUb UNIV S b" by (simp add: isUb_def setle_def) ``` huffman@30489 ` 2022` ``` from rsup[OF Se] Sb have "isLub UNIV S (rsup S)" by blast ``` chaieb@29842 ` 2023` ``` then show ?thesis using bu by (auto simp add: isLub_def leastP_def setle_def setge_def) ``` chaieb@29842 ` 2024` ```qed ``` chaieb@29842 ` 2025` chaieb@29842 ` 2026` ```lemma rsup_finite_Max: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2027` ``` shows "rsup S = Max S" ``` chaieb@29842 ` 2028` ```using fS Se ``` chaieb@29842 ` 2029` ```proof- ``` chaieb@29842 ` 2030` ``` let ?m = "Max S" ``` chaieb@29842 ` 2031` ``` from Max_ge[OF fS] have Sm: "\ x\ S. x \ ?m" by metis ``` chaieb@29842 ` 2032` ``` with rsup[OF Se] have lub: "isLub UNIV S (rsup S)" by (metis setle_def) ``` huffman@30489 ` 2033` ``` from Max_in[OF fS Se] lub have mrS: "?m \ rsup S" ``` chaieb@29842 ` 2034` ``` by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) ``` huffman@30489 ` 2035` ``` moreover ``` chaieb@29842 ` 2036` ``` have "rsup S \ ?m" using Sm lub ``` chaieb@29842 ` 2037` ``` by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) ``` huffman@30489 ` 2038` ``` ultimately show ?thesis by arith ``` chaieb@29842 ` 2039` ```qed ``` chaieb@29842 ` 2040` chaieb@29842 ` 2041` ```lemma rsup_finite_in: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2042` ``` shows "rsup S \ S" ``` chaieb@29842 ` 2043` ``` using rsup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis ``` chaieb@29842 ` 2044` chaieb@29842 ` 2045` ```lemma rsup_finite_Ub: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2046` ``` shows "isUb S S (rsup S)" ``` chaieb@29842 ` 2047` ``` using rsup_finite_Max[OF fS Se] rsup_finite_in[OF fS Se] Max_ge[OF fS] ``` chaieb@29842 ` 2048` ``` unfolding isUb_def setle_def by metis ``` chaieb@29842 ` 2049` chaieb@29842 ` 2050` ```lemma rsup_finite_ge_iff: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2051` ``` shows "a \ rsup S \ (\ x \ S. a \ x)" ``` chaieb@29842 ` 2052` ```using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def) ``` chaieb@29842 ` 2053` chaieb@29842 ` 2054` ```lemma rsup_finite_le_iff: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2055` ``` shows "a \ rsup S \ (\ x \ S. a \ x)" ``` chaieb@29842 ` 2056` ```using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def) ``` chaieb@29842 ` 2057` chaieb@29842 ` 2058` ```lemma rsup_finite_gt_iff: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2059` ``` shows "a < rsup S \ (\ x \ S. a < x)" ``` chaieb@29842 ` 2060` ```using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def) ``` chaieb@29842 ` 2061` chaieb@29842 ` 2062` ```lemma rsup_finite_lt_iff: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2063` ``` shows "a > rsup S \ (\ x \ S. a > x)" ``` chaieb@29842 ` 2064` ```using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def) ``` chaieb@29842 ` 2065` chaieb@29842 ` 2066` ```lemma rsup_unique: assumes b: "S *<= b" and S: "\b' < b. \x \ S. b' < x" ``` chaieb@29842 ` 2067` ``` shows "rsup S = b" ``` huffman@30489 ` 2068` ```using b S ``` chaieb@29842 ` 2069` ```unfolding setle_def rsup_alt ``` chaieb@29842 ` 2070` ```apply - ``` chaieb@29842 ` 2071` ```apply (rule some_equality) ``` chaieb@29842 ` 2072` ```apply (metis linorder_not_le order_eq_iff[symmetric])+ ``` chaieb@29842 ` 2073` ```done ``` chaieb@29842 ` 2074` chaieb@29842 ` 2075` ```lemma rsup_le_subset: "S\{} \ S \ T \ (\b. T *<= b) \ rsup S \ rsup T" ``` chaieb@29842 ` 2076` ``` apply (rule rsup_le) ``` chaieb@29842 ` 2077` ``` apply simp ``` chaieb@29842 ` 2078` ``` using rsup[of T] by (auto simp add: isLub_def leastP_def setge_def setle_def isUb_def) ``` chaieb@29842 ` 2079` chaieb@29842 ` 2080` ```lemma isUb_def': "isUb R S = (\x. S *<= x \ x \ R)" ``` chaieb@29842 ` 2081` ``` apply (rule ext) ``` chaieb@29842 ` 2082` ``` by (metis isUb_def) ``` chaieb@29842 ` 2083` chaieb@29842 ` 2084` ```lemma UNIV_trivial: "UNIV x" using UNIV_I[of x] by (metis mem_def) ``` chaieb@29842 ` 2085` ```lemma rsup_bounds: assumes Se: "S \ {}" and l: "a <=* S" and u: "S *<= b" ``` chaieb@29842 ` 2086` ``` shows "a \ rsup S \ rsup S \ b" ``` chaieb@29842 ` 2087` ```proof- ``` chaieb@29842 ` 2088` ``` from rsup[OF Se] u have lub: "isLub UNIV S (rsup S)" by blast ``` chaieb@29842 ` 2089` ``` hence b: "rsup S \ b" using u by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def') ``` chaieb@29842 ` 2090` ``` from Se obtain y where y: "y \ S" by blast ``` chaieb@29842 ` 2091` ``` from lub l have "a \ rsup S" apply (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def') ``` chaieb@29842 ` 2092` ``` apply (erule ballE[where x=y]) ``` chaieb@29842 ` 2093` ``` apply (erule ballE[where x=y]) ``` chaieb@29842 ` 2094` ``` apply arith ``` chaieb@29842 ` 2095` ``` using y apply auto ``` chaieb@29842 ` 2096` ``` done ``` chaieb@29842 ` 2097` ``` with b show ?thesis by blast ``` chaieb@29842 ` 2098` ```qed ``` chaieb@29842 ` 2099` chaieb@29842 ` 2100` ```lemma rsup_abs_le: "S \ {} \ (\x\S. \x\ \ a) \ \rsup S\ \ a" ``` chaieb@29842 ` 2101` ``` unfolding abs_le_interval_iff using rsup_bounds[of S "-a" a] ``` chaieb@29842 ` 2102` ``` by (auto simp add: setge_def setle_def) ``` chaieb@29842 ` 2103` chaieb@29842 ` 2104` ```lemma rsup_asclose: assumes S:"S \ {}" and b: "\x\S. \x - l\ \ e" shows "\rsup S - l\ \ e" ``` chaieb@29842 ` 2105` ```proof- ``` chaieb@29842 ` 2106` ``` have th: "\(x::real) l e. \x - l\ \ e \ l - e \ x \ x \ l + e" by arith ``` huffman@30489 ` 2107` ``` show ?thesis using S b rsup_bounds[of S "l - e" "l+e"] unfolding th ``` chaieb@29842 ` 2108` ``` by (auto simp add: setge_def setle_def) ``` chaieb@29842 ` 2109` ```qed ``` chaieb@29842 ` 2110` chaieb@29842 ` 2111` ```definition rinf:: "real set \ real" where ``` chaieb@29842 ` 2112` ``` "rinf S = (SOME a. isGlb UNIV S a)" ``` chaieb@29842 ` 2113` chaieb@29842 ` 2114` ```lemma rinf_alt: "rinf S = (SOME a. (\x \ S. x \ a) \ (\b. (\x \ S. x \ b) \ a \ b))" by (auto simp add: isGlb_def rinf_def greatestP_def isLb_def setle_def setge_def) ``` chaieb@29842 ` 2115` chaieb@29842 ` 2116` ```lemma reals_complete_Glb: assumes Se: "\x. x \ S" and lb: "\ y. isLb UNIV S y" ``` chaieb@29842 ` 2117` ``` shows "\(t::real). isGlb UNIV S t" ``` chaieb@29842 ` 2118` ```proof- ``` chaieb@29842 ` 2119` ``` let ?M = "uminus ` S" ``` chaieb@29842 ` 2120` ``` from lb have th: "\y. isUb UNIV ?M y" apply (auto simp add: isUb_def isLb_def setle_def setge_def) ``` chaieb@29842 ` 2121` ``` by (rule_tac x="-y" in exI, auto) ``` chaieb@29842 ` 2122` ``` from Se have Me: "\x. x \ ?M" by blast ``` chaieb@29842 ` 2123` ``` from reals_complete[OF Me th] obtain t where t: "isLub UNIV ?M t" by blast ``` chaieb@29842 ` 2124` ``` have "isGlb UNIV S (- t)" using t ``` chaieb@29842 ` 2125` ``` apply (auto simp add: isLub_def isGlb_def leastP_def greatestP_def setle_def setge_def isUb_def isLb_def) ``` chaieb@29842 ` 2126` ``` apply (erule_tac x="-y" in allE) ``` chaieb@29842 ` 2127` ``` apply auto ``` chaieb@29842 ` 2128` ``` done ``` chaieb@29842 ` 2129` ``` then show ?thesis by metis ``` chaieb@29842 ` 2130` ```qed ``` chaieb@29842 ` 2131` chaieb@29842 ` 2132` ```lemma rinf: assumes Se: "S \ {}" and b: "\b. b <=* S" ``` chaieb@29842 ` 2133` ``` shows "isGlb UNIV S (rinf S)" ``` chaieb@29842 ` 2134` ```using Se b ``` chaieb@29842 ` 2135` ```unfolding rinf_def ``` chaieb@29842 ` 2136` ```apply clarify ``` chaieb@29842 ` 2137` ```apply (rule someI_ex) ``` chaieb@29842 ` 2138` ```apply (rule reals_complete_Glb) ``` chaieb@29842 ` 2139` ```apply (auto simp add: isLb_def setle_def setge_def) ``` chaieb@29842 ` 2140` ```done ``` chaieb@29842 ` 2141` chaieb@29842 ` 2142` ```lemma rinf_ge: assumes Se: "S \ {}" and Sb: "b <=* S" shows "rinf S \ b" ``` chaieb@29842 ` 2143` ```proof- ``` chaieb@29842 ` 2144` ``` from Sb have bu: "isLb UNIV S b" by (simp add: isLb_def setge_def) ``` huffman@30489 ` 2145` ``` from rinf[OF Se] Sb have "isGlb UNIV S (rinf S)" by blast ``` chaieb@29842 ` 2146` ``` then show ?thesis using bu by (auto simp add: isGlb_def greatestP_def setle_def setge_def) ``` chaieb@29842 ` 2147` ```qed ``` chaieb@29842 ` 2148` chaieb@29842 ` 2149` ```lemma rinf_finite_Min: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2150` ``` shows "rinf S = Min S" ``` chaieb@29842 ` 2151` ```using fS Se ``` chaieb@29842 ` 2152` ```proof- ``` chaieb@29842 ` 2153` ``` let ?m = "Min S" ``` chaieb@29842 ` 2154` ``` from Min_le[OF fS] have Sm: "\ x\ S. x \ ?m" by metis ``` chaieb@29842 ` 2155` ``` with rinf[OF Se] have glb: "isGlb UNIV S (rinf S)" by (metis setge_def) ``` huffman@30489 ` 2156` ``` from Min_in[OF fS Se] glb have mrS: "?m \ rinf S" ``` chaieb@29842 ` 2157` ``` by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def) ``` huffman@30489 ` 2158` ``` moreover ``` chaieb@29842 ` 2159` ``` have "rinf S \ ?m" using Sm glb ``` chaieb@29842 ` 2160` ``` by (auto simp add: isGlb_def greatestP_def isLb_def setle_def setge_def) ``` huffman@30489 ` 2161` ``` ultimately show ?thesis by arith ``` chaieb@29842 ` 2162` ```qed ``` chaieb@29842 ` 2163` chaieb@29842 ` 2164` ```lemma rinf_finite_in: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2165` ``` shows "rinf S \ S" ``` chaieb@29842 ` 2166` ``` using rinf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis ``` chaieb@29842 ` 2167` chaieb@29842 ` 2168` ```lemma rinf_finite_Lb: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2169` ``` shows "isLb S S (rinf S)" ``` chaieb@29842 ` 2170` ``` using rinf_finite_Min[OF fS Se] rinf_finite_in[OF fS Se] Min_le[OF fS] ``` chaieb@29842 ` 2171` ``` unfolding isLb_def setge_def by metis ``` chaieb@29842 ` 2172` chaieb@29842 ` 2173` ```lemma rinf_finite_ge_iff: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2174` ``` shows "a \ rinf S \ (\ x \ S. a \ x)" ``` chaieb@29842 ` 2175` ```using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def) ``` chaieb@29842 ` 2176` chaieb@29842 ` 2177` ```lemma rinf_finite_le_iff: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2178` ``` shows "a \ rinf S \ (\ x \ S. a \ x)" ``` chaieb@29842 ` 2179` ```using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def) ``` chaieb@29842 ` 2180` chaieb@29842 ` 2181` ```lemma rinf_finite_gt_iff: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2182` ``` shows "a < rinf S \ (\ x \ S. a < x)" ``` chaieb@29842 ` 2183` ```using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def) ``` chaieb@29842 ` 2184` chaieb@29842 ` 2185` ```lemma rinf_finite_lt_iff: assumes fS: "finite S" and Se: "S \ {}" ``` chaieb@29842 ` 2186` ``` shows "a > rinf S \ (\ x \ S. a > x)" ``` chaieb@29842 ` 2187` ```using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def) ``` chaieb@29842 ` 2188` chaieb@29842 ` 2189` ```lemma rinf_unique: assumes b: "b <=* S" and S: "\b' > b. \x \ S. b' > x" ``` chaieb@29842 ` 2190` ``` shows "rinf S = b" ``` huffman@30489 ` 2191` ```using b S ``` chaieb@29842 ` 2192` ```unfolding setge_def rinf_alt ``` chaieb@29842 ` 2193` ```apply - ``` chaieb@29842 ` 2194` ```apply (rule some_equality) ``` chaieb@29842 ` 2195` ```apply (metis linorder_not_le order_eq_iff[symmetric])+ ``` chaieb@29842 ` 2196` ```done ``` chaieb@29842 ` 2197` chaieb@29842 ` 2198` ```lemma rinf_ge_subset: "S\{} \ S \ T \ (\b. b <=* T) \ rinf S >= rinf T" ``` chaieb@29842 ` 2199` ``` apply (rule rinf_ge) ``` chaieb@29842 ` 2200` ``` apply simp ``` chaieb@29842 ` 2201` ``` using rinf[of T] by (auto simp add: isGlb_def greatestP_def setge_def setle_def isLb_def) ``` chaieb@29842 ` 2202` chaieb@29842 ` 2203` ```lemma isLb_def': "isLb R S = (\x. x <=* S \ x \ R)" ``` chaieb@29842 ` 2204` ``` apply (rule ext) ``` chaieb@29842 ` 2205` ``` by (metis isLb_def) ``` chaieb@29842 ` 2206` chaieb@29842 ` 2207` ```lemma rinf_bounds: assumes Se: "S \ {}" and l: "a <=* S" and u: "S *<= b" ``` chaieb@29842 ` 2208` ``` shows "a \ rinf S \ rinf S \ b" ``` chaieb@29842 ` 2209` ```proof- ``` chaieb@29842 ` 2210` ``` from rinf[OF Se] l have lub: "isGlb UNIV S (rinf S)" by blast ``` chaieb@29842 ` 2211` ``` hence b: "a \ rinf S" using l by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def') ``` chaieb@29842 ` 2212` ``` from Se obtain y where y: "y \ S" by blast ``` chaieb@29842 ` 2213` ``` from lub u have "b \ rinf S" apply (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def') ``` chaieb@29842 ` 2214` ``` apply (erule ballE[where x=y]) ``` chaieb@29842 ` 2215` ``` apply (erule ballE[where x=y]) ``` chaieb@29842 ` 2216` ``` apply arith ``` chaieb@29842 ` 2217` ``` using y apply auto ``` chaieb@29842 ` 2218` ``` done ``` chaieb@29842 ` 2219` ``` with b show ?thesis by blast ``` chaieb@29842 ` 2220` ```qed ``` chaieb@29842 ` 2221` chaieb@29842 ` 2222` ```lemma rinf_abs_ge: "S \ {} \ (\x\S. \x\ \ a) \ \rinf S\ \ a" ``` chaieb@29842 ` 2223` ``` unfolding abs_le_interval_iff using rinf_bounds[of S "-a" a] ``` chaieb@29842 ` 2224` ``` by (auto simp add: setge_def setle_def) ``` chaieb@29842 ` 2225` chaieb@29842 ` 2226` ```lemma rinf_asclose: assumes S:"S \ {}" and b: "\x\S. \x - l\ \ e" shows "\rinf S - l\ \ e" ``` chaieb@29842 ` 2227` ```proof- ``` chaieb@29842 ` 2228` ``` have th: "\(x::real) l e. \x - l\ \ e \ l - e \ x \ x \ l + e" by arith ``` huffman@30489 ` 2229` ``` show ?thesis using S b rinf_bounds[of S "l - e" "l+e"] unfolding th ``` chaieb@29842 ` 2230` ``` by (auto simp add: setge_def setle_def) ``` chaieb@29842 ` 2231` ```qed ``` chaieb@29842 ` 2232` chaieb@29842 ` 2233` chaieb@29842 ` 2234` chaieb@29842 ` 2235` ```subsection{* Operator norm. *} ``` chaieb@29842 ` 2236` chaieb@29842 ` 2237` ```definition "onorm f = rsup {norm (f x)| x. norm x = 1}" ``` chaieb@29842 ` 2238` chaieb@29842 ` 2239` ```lemma norm_bound_generalize: ``` chaieb@29842 ` 2240` ``` fixes f:: "real ^'n \ real^'m" ``` chaieb@29842 ` 2241` ``` assumes lf: "linear f" ``` chaieb@29842 ` 2242` ``` shows "(\x. norm x = 1 \ norm (f x) \ b) \ (\x. norm (f x) \ b * norm x)" (is "?lhs \ ?rhs") ``` chaieb@29842 ` 2243` ```proof- ``` chaieb@29842 ` 2244` ``` {assume H: ?rhs ``` chaieb@29842 ` 2245` ``` {fix x :: "real^'n" assume x: "norm x = 1" ``` chaieb@29842 ` 2246` ``` from H[rule_format, of x] x have "norm (f x) \ b" by simp} ``` chaieb@29842 ` 2247` ``` then have ?lhs by blast } ``` chaieb@29842 ` 2248` chaieb@29842 ` 2249` ``` moreover ``` chaieb@29842 ` 2250` ``` {assume H: ?lhs ``` huffman@30489 ` 2251` ``` from H[rule_format, of "basis 1"] ``` huffman@30041 ` 2252` ``` have bp: "b \ 0" using norm_ge_zero[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"] ``` huffman@30040 ` 2253` ``` by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero]) ``` chaieb@29842 ` 2254` ``` {fix x :: "real ^'n" ``` chaieb@29842 ` 2255` ``` {assume "x = 0" ``` huffman@30041 ` 2256` ``` then have "norm (f x) \ b * norm x" by (simp add: linear_0[OF lf] bp)} ``` chaieb@29842 ` 2257` ``` moreover ``` chaieb@29842 ` 2258` ``` {assume x0: "x \ 0" ``` huffman@30041 ` 2259` ``` hence n0: "norm x \ 0" by (metis norm_eq_zero) ``` chaieb@29842 ` 2260` ``` let ?c = "1/ norm x" ``` huffman@30040 ` 2261` ``` have "norm (?c*s x) = 1" using x0 by (simp add: n0 norm_mul) ``` chaieb@29842 ` 2262` ``` with H have "norm (f(?c*s x)) \ b" by blast ``` huffman@30489 ` 2263` ``` hence "?c * norm (f x) \ b" ``` chaieb@29842 ` 2264` ``` by (simp add: linear_cmul[OF lf] norm_mul) ``` huffman@30489 ` 2265` ``` hence "norm (f x) \ b * norm x" ``` huffman@30041 ` 2266` ``` using n0 norm_ge_zero[of x] by (auto simp add: field_simps)} ``` chaieb@29842 ` 2267` ``` ultimately have "norm (f x) \ b * norm x" by blast} ``` chaieb@29842 ` 2268` ``` then have ?rhs by blast} ``` chaieb@29842 ` 2269` ``` ultimately show ?thesis by blast ``` chaieb@29842 ` 2270` ```qed ``` chaieb@29842 ` 2271` chaieb@29842 ` 2272` ```lemma onorm: ``` chaieb@29842 ` 2273` ``` fixes f:: "real ^'n \ real ^'m" ``` chaieb@29842 ` 2274` ``` assumes lf: "linear f" ``` chaieb@29842 ` 2275` ``` shows "norm (f x) <= onorm f * norm x" ``` chaieb@29842 ` 2276` ``` and "\x. norm (f x) <= b * norm x \ onorm f <= b" ``` chaieb@29842 ` 2277` ```proof- ``` chaieb@29842 ` 2278` ``` { ``` chaieb@29842 ` 2279` ``` let ?S = "{norm (f x) |x. norm x = 1}" ``` chaieb@29842 ` 2280` ``` have Se: "?S \ {}" using norm_basis_1 by auto ``` huffman@30489 ` 2281` ``` from linear_bounded[OF lf] have b: "\ b. ?S *<= b" ``` chaieb@29842 ` 2282` ``` unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def) ``` chaieb@29842 ` 2283` ``` {from rsup[OF Se b, unfolded onorm_def[symmetric]] ``` huffman@30489 ` 2284` ``` show "norm (f x) <= onorm f * norm x" ``` huffman@30489 ` 2285` ``` apply - ``` chaieb@29842 ` 2286` ``` apply (rule spec[where x = x]) ``` chaieb@29842 ` 2287` ``` unfolding norm_bound_generalize[OF lf, symmetric] ``` chaieb@29842 ` 2288` ``` by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} ``` chaieb@29842 ` 2289` ``` { ``` huffman@30489 ` 2290` ``` show "\x. norm (f x) <= b * norm x \ onorm f <= b" ``` chaieb@29842 ` 2291` ``` using rsup[OF Se b, unfolded onorm_def[symmetric]] ``` chaieb@29842 ` 2292` ``` unfolding norm_bound_generalize[OF lf, symmetric] ``` chaieb@29842 ` 2293` ``` by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} ``` chaieb@29842 ` 2294` ``` } ``` chaieb@29842 ` 2295` ```qed ``` chaieb@29842 ` 2296` chaieb@29842 ` 2297` ```lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \ real ^'m)" shows "0 <= onorm f" ``` huffman@30041 ` 2298` ``` using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp ``` chaieb@29842 ` 2299` huffman@30489 ` 2300` ```lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \ real ^'m)" ``` chaieb@29842 ` 2301` ``` shows "onorm f = 0 \ (\x. f x = 0)" ``` chaieb@29842 ` 2302` ``` using onorm[OF lf] ``` huffman@30041 ` 2303` ``` apply (auto simp add: onorm_pos_le) ``` chaieb@29842 ` 2304` ``` apply atomize ``` chaieb@29842 ` 2305` ``` apply (erule allE[where x="0::real"]) ``` chaieb@29842 ` 2306` ``` using onorm_pos_le[OF lf] ``` chaieb@29842 ` 2307` ``` apply arith ``` chaieb@29842 ` 2308` ``` done ``` chaieb@29842 ` 2309` chaieb@29842 ` 2310` ```lemma onorm_const: "onorm(\x::real^'n. (y::real ^ 'm)) = norm y" ``` chaieb@29842 ` 2311` ```proof- ``` chaieb@29842 ` 2312` ``` let ?f = "\x::real^'n. (y::real ^ 'm)" ``` chaieb@29842 ` 2313` ``` have th: "{norm (?f x)| x. norm x = 1} = {norm y}" ``` chaieb@29842 ` 2314` ``` by(auto intro: vector_choose_size set_ext) ``` chaieb@29842 ` 2315` ``` show ?thesis ``` chaieb@29842 ` 2316` ``` unfolding onorm_def th ``` chaieb@29842 ` 2317` ``` apply (rule rsup_unique) by (simp_all add: setle_def) ``` chaieb@29842 ` 2318` ```qed ``` chaieb@29842 ` 2319` huffman@30489 ` 2320` ```lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n \ real ^'m)" ``` chaieb@29842 ` 2321` ``` shows "0 < onorm f \ ~(\x. f x = 0)" ``` chaieb@29842 ` 2322` ``` unfolding onorm_eq_0[OF lf, symmetric] ``` chaieb@29842 ` 2323` ``` using onorm_pos_le[OF lf] by arith ``` chaieb@29842 ` 2324` chaieb@29842 ` 2325` ```lemma onorm_compose: ``` chaieb@29842 ` 2326` ``` assumes lf: "linear (f::real ^'n \ real ^'m)" and lg: "linear g" ``` chaieb@29842 ` 2327` ``` shows "onorm (f o g) <= onorm f * onorm g" ``` chaieb@29842 ` 2328` ``` apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format]) ``` chaieb@29842 ` 2329` ``` unfolding o_def ``` chaieb@29842 ` 2330` ``` apply (subst mult_assoc) ``` chaieb@29842 ` 2331` ``` apply (rule order_trans) ``` chaieb@29842 ` 2332` ``` apply (rule onorm(1)[OF lf]) ``` chaieb@29842 ` 2333` ``` apply (rule mult_mono1) ``` chaieb@29842 ` 2334` ``` apply (rule onorm(1)[OF lg]) ``` chaieb@29842 ` 2335` ``` apply (rule onorm_pos_le[OF lf]) ``` chaieb@29842 ` 2336` ``` done ``` chaieb@29842 ` 2337` chaieb@29842 ` 2338` ```lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \ real^'m)" ``` chaieb@29842 ` 2339` ``` shows "onorm (\x. - f x) \ onorm f" ``` chaieb@29842 ` 2340` ``` using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf] ``` huffman@30041 ` 2341` ``` unfolding norm_minus_cancel by metis ``` chaieb@29842 ` 2342` chaieb@29842 ` 2343` ```lemma onorm_neg: assumes lf: "linear (f::real ^'n \ real^'m)" ``` chaieb@29842 ` 2344` ``` shows "onorm (\x. - f x) = onorm f" ``` chaieb@29842 ` 2345` ``` using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]] ``` chaieb@29842 ` 2346` ``` by simp ``` chaieb@29842 ` 2347` chaieb@29842 ` 2348` ```lemma onorm_triangle: ``` chaieb@29842 ` 2349` ``` assumes lf: "linear (f::real ^'n \ real ^'m)" and lg: "linear g" ``` chaieb@29842 ` 2350` ``` shows "onorm (\x. f x + g x) <= onorm f + onorm g" ``` chaieb@29842 ` 2351` ``` apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format]) ``` chaieb@29842 ` 2352` ``` apply (rule order_trans) ``` huffman@30041 ` 2353` ``` apply (rule norm_triangle_ineq) ``` chaieb@29842 ` 2354` ``` apply (simp add: distrib) ``` chaieb@29842 ` 2355` ``` apply (rule add_mono) ``` chaieb@29842 ` 2356` ``` apply (rule onorm(1)[OF lf]) ``` chaieb@29842 ` 2357` ``` apply (rule onorm(1)[OF lg]) ``` chaieb@29842 ` 2358` ``` done ``` chaieb@29842 ` 2359` chaieb@29842 ` 2360` ```lemma onorm_triangle_le: "linear (f::real ^'n \ real ^'m) \ linear g \ onorm(f) + onorm(g) <= e ``` chaieb@29842 ` 2361` ``` \ onorm(\x. f x + g x) <= e" ``` chaieb@29842 ` 2362` ``` apply (rule order_trans) ``` chaieb@29842 ` 2363` ``` apply (rule onorm_triangle) ``` chaieb@29842 ` 2364` ``` apply assumption+ ``` chaieb@29842 ` 2365` ``` done ``` chaieb@29842 ` 2366` chaieb@29842 ` 2367` ```lemma onorm_triangle_lt: "linear (f::real ^'n \ real ^'m) \ linear g \ onorm(f) + onorm(g) < e ``` chaieb@29842 ` 2368` ``` ==> onorm(\x. f x + g x) < e" ``` chaieb@29842 ` 2369` ``` apply (rule order_le_less_trans) ``` chaieb@29842 ` 2370` ``` apply (rule onorm_triangle) ``` chaieb@29842 ` 2371` ``` by assumption+ ``` chaieb@29842 ` 2372` chaieb@29842 ` 2373` ```(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *) ``` chaieb@29842 ` 2374` chaieb@29842 ` 2375` ```definition vec1:: "'a \ 'a ^ 1" where "vec1 x = (\ i. x)" ``` chaieb@29842 ` 2376` huffman@30489 ` 2377` ```definition dest_vec1:: "'a ^1 \ 'a" ``` chaieb@29842 ` 2378` ``` where "dest_vec1 x = (x\$1)" ``` chaieb@29842 ` 2379` chaieb@29842 ` 2380` `lemma vec1_component[simp]: "(ve`