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