author  haftmann 
Sun, 22 Mar 2009 20:46:11 +0100  
changeset 30655  88131f2807b6 
parent 30582  638b088bb840 
child 30665  4cf38ea4fad2 
permissions  rwrr 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1 
(* Title: Library/Euclidean_Space 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

2 
Author: Amine Chaieb, University of Cambridge 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

3 
*) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

4 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

5 
header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

6 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

7 
theory Euclidean_Space 
30655  8 
imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

9 
Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type 
30045  10 
Inner_Product 
30655  11 
uses ("normarith.ML") 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

12 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

13 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

14 
text{* Some common special cases.*} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

15 

30582  16 
lemma forall_1: "(\<forall>i::1. P i) \<longleftrightarrow> P 1" 
17 
by (metis num1_eq_iff) 

18 

19 
lemma exhaust_2: 

20 
fixes x :: 2 shows "x = 1 \<or> x = 2" 

21 
proof (induct x) 

22 
case (of_int z) 

23 
then have "0 <= z" and "z < 2" by simp_all 

24 
then have "z = 0  z = 1" by arith 

25 
then show ?case by auto 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

26 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

27 

30582  28 
lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2" 
29 
by (metis exhaust_2) 

30 

31 
lemma exhaust_3: 

32 
fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3" 

33 
proof (induct x) 

34 
case (of_int z) 

35 
then have "0 <= z" and "z < 3" by simp_all 

36 
then have "z = 0 \<or> z = 1 \<or> z = 2" by arith 

37 
then show ?case by auto 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

38 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

39 

30582  40 
lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3" 
41 
by (metis exhaust_3) 

42 

43 
lemma UNIV_1: "UNIV = {1::1}" 

44 
by (auto simp add: num1_eq_iff) 

45 

46 
lemma UNIV_2: "UNIV = {1::2, 2::2}" 

47 
using exhaust_2 by auto 

48 

49 
lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" 

50 
using exhaust_3 by auto 

51 

52 
lemma setsum_1: "setsum f (UNIV::1 set) = f 1" 

53 
unfolding UNIV_1 by simp 

54 

55 
lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2" 

56 
unfolding UNIV_2 by simp 

57 

58 
lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3" 

59 
unfolding UNIV_3 by (simp add: add_ac) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

60 

29906  61 
subsection{* Basic componentwise operations on vectors. *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

62 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

63 
instantiation "^" :: (plus,type) plus 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

64 
begin 
30489  65 
definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

66 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

67 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

68 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

69 
instantiation "^" :: (times,type) times 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

70 
begin 
30489  71 
definition vector_mult_def : "op * \<equiv> (\<lambda> x y. (\<chi> i. (x$i) * (y$i)))" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

72 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

73 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

74 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

75 
instantiation "^" :: (minus,type) minus begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

76 
definition vector_minus_def : "op  \<equiv> (\<lambda> x y. (\<chi> i. (x$i)  (y$i)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

77 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

78 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

79 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

80 
instantiation "^" :: (uminus,type) uminus begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

81 
definition vector_uminus_def : "uminus \<equiv> (\<lambda> x. (\<chi> i.  (x$i)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

82 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

83 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

84 
instantiation "^" :: (zero,type) zero begin 
30489  85 
definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

86 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

87 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

88 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

89 
instantiation "^" :: (one,type) one begin 
30489  90 
definition vector_one_def : "1 \<equiv> (\<chi> i. 1)" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

91 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

92 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

93 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

94 
instantiation "^" :: (ord,type) ord 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

95 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

96 
definition vector_less_eq_def: 
30582  97 
"less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)" 
98 
definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)" 

30489  99 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

100 
instance by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

101 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

102 

30039  103 
instantiation "^" :: (scaleR, type) scaleR 
104 
begin 

30489  105 
definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" 
30039  106 
instance .. 
107 
end 

108 

109 
text{* Also the scalarvector multiplication. *} 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

110 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

111 
definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

112 
where "c *s x = (\<chi> i. c * (x$i))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

113 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

114 
text{* Constant Vectors *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

115 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

116 
definition "vec x = (\<chi> i. x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

117 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

118 
text{* Dot products. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

119 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

120 
definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where 
30582  121 
"x \<bullet> y = setsum (\<lambda>i. x$i * y$i) UNIV" 
122 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

123 
lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x$1) * (y$1)" 
30582  124 
by (simp add: dot_def setsum_1) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

125 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

126 
lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2)" 
30582  127 
by (simp add: dot_def setsum_2) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

128 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

129 
lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)" 
30582  130 
by (simp add: dot_def setsum_3) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

131 

29906  132 
subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

133 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

134 
method_setup vector = {* 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

135 
let 
30489  136 
val ss1 = HOL_basic_ss addsimps [@{thm dot_def}, @{thm setsum_addf} RS sym, 
137 
@{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

138 
@{thm setsum_left_distrib}, @{thm setsum_negf} RS sym] 
30489  139 
val ss2 = @{simpset} addsimps 
140 
[@{thm vector_add_def}, @{thm vector_mult_def}, 

141 
@{thm vector_minus_def}, @{thm vector_uminus_def}, 

142 
@{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def}, 

30039  143 
@{thm vector_scaleR_def}, 
30582  144 
@{thm Cart_lambda_beta}, @{thm vector_scalar_mult_def}] 
30489  145 
fun vector_arith_tac ths = 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

146 
simp_tac ss1 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

147 
THEN' (fn i => rtac @{thm setsum_cong2} i 
30489  148 
ORELSE rtac @{thm setsum_0'} i 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

149 
ORELSE simp_tac (HOL_basic_ss addsimps [@{thm "Cart_eq"}]) i) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

150 
(* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

151 
THEN' asm_full_simp_tac (ss2 addsimps ths) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

152 
in 
30549  153 
Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths))) 
154 
end 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

155 
*} "Lifts trivial vector statements to real arith statements" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

156 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

157 
lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

158 
lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

159 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

160 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

161 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

162 
text{* Obvious "componentpushing". *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

163 

30582  164 
lemma vec_component [simp]: "(vec x :: 'a ^ 'n)$i = x" 
30489  165 
by (vector vec_def) 
166 

30582  167 
lemma vector_add_component [simp]: 
168 
fixes x y :: "'a::{plus} ^ 'n" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

169 
shows "(x + y)$i = x$i + y$i" 
30582  170 
by vector 
171 

172 
lemma vector_minus_component [simp]: 

173 
fixes x y :: "'a::{minus} ^ 'n" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

174 
shows "(x  y)$i = x$i  y$i" 
30582  175 
by vector 
176 

177 
lemma vector_mult_component [simp]: 

178 
fixes x y :: "'a::{times} ^ 'n" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

179 
shows "(x * y)$i = x$i * y$i" 
30582  180 
by vector 
181 

182 
lemma vector_smult_component [simp]: 

183 
fixes y :: "'a::{times} ^ 'n" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

184 
shows "(c *s y)$i = c * (y$i)" 
30582  185 
by vector 
186 

187 
lemma vector_uminus_component [simp]: 

188 
fixes x :: "'a::{uminus} ^ 'n" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

189 
shows "( x)$i =  (x$i)" 
30582  190 
by vector 
191 

192 
lemma vector_scaleR_component [simp]: 

30039  193 
fixes x :: "'a::scaleR ^ 'n" 
194 
shows "(scaleR r x)$i = scaleR r (x$i)" 

30582  195 
by vector 
30039  196 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

197 
lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

198 

30039  199 
lemmas vector_component = 
200 
vec_component vector_add_component vector_mult_component 

201 
vector_smult_component vector_minus_component vector_uminus_component 

202 
vector_scaleR_component cond_component 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

203 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

204 
subsection {* Some frequently useful arithmetic lemmas over vectors. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

205 

30489  206 
instance "^" :: (semigroup_add,type) semigroup_add 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

207 
apply (intro_classes) by (vector add_assoc) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

208 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

209 

30489  210 
instance "^" :: (monoid_add,type) monoid_add 
211 
apply (intro_classes) by vector+ 

212 

213 
instance "^" :: (group_add,type) group_add 

214 
apply (intro_classes) by (vector algebra_simps)+ 

215 

216 
instance "^" :: (ab_semigroup_add,type) ab_semigroup_add 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

217 
apply (intro_classes) by (vector add_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

218 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

219 
instance "^" :: (comm_monoid_add,type) comm_monoid_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

220 
apply (intro_classes) by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

221 

30489  222 
instance "^" :: (ab_group_add,type) ab_group_add 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

223 
apply (intro_classes) by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

224 

30489  225 
instance "^" :: (cancel_semigroup_add,type) cancel_semigroup_add 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

226 
apply (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

227 
by (vector Cart_eq)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

228 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

229 
instance "^" :: (cancel_ab_semigroup_add,type) cancel_ab_semigroup_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

230 
apply (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

231 
by (vector Cart_eq) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

232 

30039  233 
instance "^" :: (real_vector, type) real_vector 
234 
by default (vector scaleR_left_distrib scaleR_right_distrib)+ 

235 

30489  236 
instance "^" :: (semigroup_mult,type) semigroup_mult 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

237 
apply (intro_classes) by (vector mult_assoc) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

238 

30489  239 
instance "^" :: (monoid_mult,type) monoid_mult 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

240 
apply (intro_classes) by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

241 

30489  242 
instance "^" :: (ab_semigroup_mult,type) ab_semigroup_mult 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

243 
apply (intro_classes) by (vector mult_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

244 

30489  245 
instance "^" :: (ab_semigroup_idem_mult,type) ab_semigroup_idem_mult 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

246 
apply (intro_classes) by (vector mult_idem) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

247 

30489  248 
instance "^" :: (comm_monoid_mult,type) comm_monoid_mult 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

249 
apply (intro_classes) by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

250 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

251 
fun vector_power :: "('a::{one,times} ^'n) \<Rightarrow> nat \<Rightarrow> 'a^'n" where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

252 
"vector_power x 0 = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

253 
 "vector_power x (Suc n) = x * vector_power x n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

254 

30489  255 
instantiation "^" :: (recpower,type) recpower 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

256 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

257 
definition vec_power_def: "op ^ \<equiv> vector_power" 
30489  258 
instance 
259 
apply (intro_classes) by (simp_all add: vec_power_def) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

260 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

261 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

262 
instance "^" :: (semiring,type) semiring 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

263 
apply (intro_classes) by (vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

264 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

265 
instance "^" :: (semiring_0,type) semiring_0 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

266 
apply (intro_classes) by (vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

267 
instance "^" :: (semiring_1,type) semiring_1 
30582  268 
apply (intro_classes) by vector 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

269 
instance "^" :: (comm_semiring,type) comm_semiring 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

270 
apply (intro_classes) by (vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

271 

30489  272 
instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes) 
29905  273 
instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add .. 
30489  274 
instance "^" :: (semiring_0_cancel,type) semiring_0_cancel by (intro_classes) 
275 
instance "^" :: (comm_semiring_0_cancel,type) comm_semiring_0_cancel by (intro_classes) 

276 
instance "^" :: (ring,type) ring by (intro_classes) 

277 
instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

278 
instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes) 
30039  279 

280 
instance "^" :: (ring_1,type) ring_1 .. 

281 

282 
instance "^" :: (real_algebra,type) real_algebra 

283 
apply intro_classes 

284 
apply (simp_all add: vector_scaleR_def ring_simps) 

285 
apply vector 

286 
apply vector 

287 
done 

288 

289 
instance "^" :: (real_algebra_1,type) real_algebra_1 .. 

290 

30489  291 
lemma of_nat_index: 
30582  292 
"(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

293 
apply (induct n) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

294 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

295 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

296 
done 
30489  297 
lemma zero_index[simp]: 
30582  298 
"(0 :: 'a::zero ^'n)$i = 0" by vector 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

299 

30489  300 
lemma one_index[simp]: 
30582  301 
"(1 :: 'a::one ^'n)$i = 1" by vector 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

302 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

303 
lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \<noteq> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

304 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

305 
have "(1::'a) + of_nat n = 0 \<longleftrightarrow> of_nat 1 + of_nat n = (of_nat 0 :: 'a)" by simp 
30489  306 
also have "\<dots> \<longleftrightarrow> 1 + n = 0" by (simp only: of_nat_add[symmetric] of_nat_eq_iff) 
307 
finally show ?thesis by simp 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

308 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

309 

30489  310 
instance "^" :: (semiring_char_0,type) semiring_char_0 
311 
proof (intro_classes) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

312 
fix m n ::nat 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

313 
show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n" 
30582  314 
by (simp add: Cart_eq of_nat_index) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

315 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

316 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

317 
instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes 
30039  318 
instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

319 

30489  320 
lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

321 
by (vector mult_assoc) 
30489  322 
lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

323 
by (vector ring_simps) 
30489  324 
lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

325 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

326 
lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

327 
lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector 
30489  328 
lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x  y) = c *s x  c *s y" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

329 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

330 
lemma vector_smult_rneg: "(c::'a::ring) *s x = (c *s x)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

331 
lemma vector_smult_lneg: " (c::'a::ring) *s x = (c *s x)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

332 
lemma vector_sneg_minus1: "x = ( (1::'a::ring_1)) *s x" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

333 
lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector 
30489  334 
lemma vector_sub_rdistrib: "((a::'a::ring)  b) *s x = a *s x  b *s x" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

335 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

336 

30489  337 
lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)" 
30582  338 
by (simp add: Cart_eq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

339 

30040  340 
subsection {* Square root of sum of squares *} 
341 

342 
definition 

343 
"setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)" 

344 

345 
lemma setL2_cong: 

346 
"\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B" 

347 
unfolding setL2_def by simp 

348 

349 
lemma strong_setL2_cong: 

350 
"\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B" 

351 
unfolding setL2_def simp_implies_def by simp 

352 

353 
lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0" 

354 
unfolding setL2_def by simp 

355 

356 
lemma setL2_empty [simp]: "setL2 f {} = 0" 

357 
unfolding setL2_def by simp 

358 

359 
lemma setL2_insert [simp]: 

360 
"\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow> 

361 
setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)" 

362 
unfolding setL2_def by (simp add: setsum_nonneg) 

363 

364 
lemma setL2_nonneg [simp]: "0 \<le> setL2 f A" 

365 
unfolding setL2_def by (simp add: setsum_nonneg) 

366 

367 
lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0" 

368 
unfolding setL2_def by simp 

369 

370 
lemma setL2_mono: 

371 
assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i" 

372 
assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i" 

373 
shows "setL2 f K \<le> setL2 g K" 

374 
unfolding setL2_def 

375 
by (simp add: setsum_nonneg setsum_mono power_mono prems) 

376 

377 
lemma setL2_right_distrib: 

378 
"0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A" 

379 
unfolding setL2_def 

380 
apply (simp add: power_mult_distrib) 

381 
apply (simp add: setsum_right_distrib [symmetric]) 

382 
apply (simp add: real_sqrt_mult setsum_nonneg) 

383 
done 

384 

385 
lemma setL2_left_distrib: 

386 
"0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A" 

387 
unfolding setL2_def 

388 
apply (simp add: power_mult_distrib) 

389 
apply (simp add: setsum_left_distrib [symmetric]) 

390 
apply (simp add: real_sqrt_mult setsum_nonneg) 

391 
done 

392 

393 
lemma setsum_nonneg_eq_0_iff: 

394 
fixes f :: "'a \<Rightarrow> 'b::pordered_ab_group_add" 

395 
shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" 

396 
apply (induct set: finite, simp) 

397 
apply (simp add: add_nonneg_eq_0_iff setsum_nonneg) 

398 
done 

399 

400 
lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" 

401 
unfolding setL2_def 

402 
by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff) 

403 

404 
lemma setL2_triangle_ineq: 

405 
shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A" 

406 
proof (cases "finite A") 

407 
case False 

408 
thus ?thesis by simp 

409 
next 

410 
case True 

411 
thus ?thesis 

412 
proof (induct set: finite) 

413 
case empty 

414 
show ?case by simp 

415 
next 

416 
case (insert x F) 

417 
hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le> 

418 
sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)" 

419 
by (intro real_sqrt_le_mono add_left_mono power_mono insert 

420 
setL2_nonneg add_increasing zero_le_power2) 

421 
also have 

422 
"\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)" 

423 
by (rule real_sqrt_sum_squares_triangle_ineq) 

424 
finally show ?case 

425 
using insert by simp 

426 
qed 

427 
qed 

428 

429 
lemma sqrt_sum_squares_le_sum: 

430 
"\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y" 

431 
apply (rule power2_le_imp_le) 

432 
apply (simp add: power2_sum) 

433 
apply (simp add: mult_nonneg_nonneg) 

434 
apply (simp add: add_nonneg_nonneg) 

435 
done 

436 

437 
lemma setL2_le_setsum [rule_format]: 

438 
"(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A" 

439 
apply (cases "finite A") 

440 
apply (induct set: finite) 

441 
apply simp 

442 
apply clarsimp 

443 
apply (erule order_trans [OF sqrt_sum_squares_le_sum]) 

444 
apply simp 

445 
apply simp 

446 
apply simp 

447 
done 

448 

449 
lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>" 

450 
apply (rule power2_le_imp_le) 

451 
apply (simp add: power2_sum) 

452 
apply (simp add: mult_nonneg_nonneg) 

453 
apply (simp add: add_nonneg_nonneg) 

454 
done 

455 

456 
lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)" 

457 
apply (cases "finite A") 

458 
apply (induct set: finite) 

459 
apply simp 

460 
apply simp 

461 
apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs]) 

462 
apply simp 

463 
apply simp 

464 
done 

465 

466 
lemma setL2_mult_ineq_lemma: 

467 
fixes a b c d :: real 

468 
shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>" 

469 
proof  

470 
have "0 \<le> (a * d  b * c)\<twosuperior>" by simp 

471 
also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>  2 * (a * d) * (b * c)" 

472 
by (simp only: power2_diff power_mult_distrib) 

473 
also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>  2 * (a * c) * (b * d)" 

474 
by simp 

475 
finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>" 

476 
by simp 

477 
qed 

478 

479 
lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A" 

480 
apply (cases "finite A") 

481 
apply (induct set: finite) 

482 
apply simp 

483 
apply (rule power2_le_imp_le, simp) 

484 
apply (rule order_trans) 

485 
apply (rule power_mono) 

486 
apply (erule add_left_mono) 

487 
apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg) 

488 
apply (simp add: power2_sum) 

489 
apply (simp add: power_mult_distrib) 

490 
apply (simp add: right_distrib left_distrib) 

491 
apply (rule ord_le_eq_trans) 

492 
apply (rule setL2_mult_ineq_lemma) 

493 
apply simp 

494 
apply (intro mult_nonneg_nonneg setL2_nonneg) 

495 
apply simp 

496 
done 

497 

498 
lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A" 

499 
apply (rule_tac s="insert i (A  {i})" and t="A" in subst) 

500 
apply fast 

501 
apply (subst setL2_insert) 

502 
apply simp 

503 
apply simp 

504 
apply simp 

505 
done 

506 

507 
subsection {* Norms *} 

508 

30582  509 
instantiation "^" :: (real_normed_vector, finite) real_normed_vector 
30040  510 
begin 
511 

512 
definition vector_norm_def: 

30582  513 
"norm (x::'a^'b) = setL2 (\<lambda>i. norm (x$i)) UNIV" 
30040  514 

515 
definition vector_sgn_def: 

516 
"sgn (x::'a^'b) = scaleR (inverse (norm x)) x" 

517 

518 
instance proof 

519 
fix a :: real and x y :: "'a ^ 'b" 

520 
show "0 \<le> norm x" 

521 
unfolding vector_norm_def 

522 
by (rule setL2_nonneg) 

523 
show "norm x = 0 \<longleftrightarrow> x = 0" 

524 
unfolding vector_norm_def 

525 
by (simp add: setL2_eq_0_iff Cart_eq) 

526 
show "norm (x + y) \<le> norm x + norm y" 

527 
unfolding vector_norm_def 

528 
apply (rule order_trans [OF _ setL2_triangle_ineq]) 

30582  529 
apply (simp add: setL2_mono norm_triangle_ineq) 
30040  530 
done 
531 
show "norm (scaleR a x) = \<bar>a\<bar> * norm x" 

532 
unfolding vector_norm_def 

30582  533 
by (simp add: norm_scaleR setL2_right_distrib) 
30040  534 
show "sgn x = scaleR (inverse (norm x)) x" 
535 
by (rule vector_sgn_def) 

536 
qed 

537 

538 
end 

539 

30045  540 
subsection {* Inner products *} 
541 

30582  542 
instantiation "^" :: (real_inner, finite) real_inner 
30045  543 
begin 
544 

545 
definition vector_inner_def: 

30582  546 
"inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV" 
30045  547 

548 
instance proof 

549 
fix r :: real and x y z :: "'a ^ 'b" 

550 
show "inner x y = inner y x" 

551 
unfolding vector_inner_def 

552 
by (simp add: inner_commute) 

553 
show "inner (x + y) z = inner x z + inner y z" 

554 
unfolding vector_inner_def 

30582  555 
by (simp add: inner_left_distrib setsum_addf) 
30045  556 
show "inner (scaleR r x) y = r * inner x y" 
557 
unfolding vector_inner_def 

30582  558 
by (simp add: inner_scaleR_left setsum_right_distrib) 
30045  559 
show "0 \<le> inner x x" 
560 
unfolding vector_inner_def 

561 
by (simp add: setsum_nonneg) 

562 
show "inner x x = 0 \<longleftrightarrow> x = 0" 

563 
unfolding vector_inner_def 

564 
by (simp add: Cart_eq setsum_nonneg_eq_0_iff) 

565 
show "norm x = sqrt (inner x x)" 

566 
unfolding vector_inner_def vector_norm_def setL2_def 

567 
by (simp add: power2_norm_eq_inner) 

568 
qed 

569 

570 
end 

571 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

572 
subsection{* Properties of the dot product. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

573 

30489  574 
lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

575 
by (vector mult_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

576 
lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

577 
by (vector ring_simps) 
30489  578 
lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n)) = (x \<bullet> y) + (x \<bullet> z)" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

579 
by (vector ring_simps) 
30489  580 
lemma dot_lsub: "((x::'a::ring ^ 'n)  y) \<bullet> z = (x \<bullet> z)  (y \<bullet> z)" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

581 
by (vector ring_simps) 
30489  582 
lemma dot_rsub: "(x::'a::ring ^ 'n) \<bullet> (y  z) = (x \<bullet> y)  (x \<bullet> z)" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

583 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

584 
lemma dot_lmult: "(c *s x) \<bullet> y = (c::'a::ring) * (x \<bullet> y)" by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

585 
lemma dot_rmult: "x \<bullet> (c *s y) = (c::'a::comm_ring) * (x \<bullet> y)" by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

586 
lemma dot_lneg: "(x) \<bullet> (y::'a::ring ^ 'n) = (x \<bullet> y)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

587 
lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (y) = (x \<bullet> y)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

588 
lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

589 
lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

590 
lemma dot_pos_le[simp]: "(0::'a\<Colon>ordered_ring_strict) <= x \<bullet> x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

591 
by (simp add: dot_def setsum_nonneg) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

592 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

593 
lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::pordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

594 
using fS fp setsum_nonneg[OF fp] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

595 
proof (induct set: finite) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

596 
case empty thus ?case by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

597 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

598 
case (insert x F) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

599 
from insert.prems have Fx: "f x \<ge> 0" and Fp: "\<forall> a \<in> F. f a \<ge> 0" by simp_all 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

600 
from insert.hyps Fp setsum_nonneg[OF Fp] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

601 
have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

602 
from sum_nonneg_eq_zero_iff[OF Fx setsum_nonneg[OF Fp]] insert.hyps(1,2) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

603 
show ?case by (simp add: h) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

604 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

605 

30582  606 
lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) = 0" 
607 
by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq) 

608 

609 
lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x] 

30489  610 
by (auto simp add: le_less) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

611 

30040  612 
subsection{* The collapse of the general concepts to dimension one. *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

613 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

614 
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))" 
30582  615 
by (simp add: Cart_eq forall_1) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

616 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

617 
lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

618 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

619 
apply (erule_tac x= "x$1" in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

620 
apply (simp only: vector_one[symmetric]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

621 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

622 

30040  623 
lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)" 
30582  624 
by (simp add: vector_norm_def UNIV_1) 
30040  625 

30489  626 
lemma norm_real: "norm(x::real ^ 1) = abs(x$1)" 
30040  627 
by (simp add: norm_vector_1) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

628 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

629 
text{* Metric *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

630 

30040  631 
text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *} 
30582  632 
definition dist:: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real" where 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

633 
"dist x y = norm (x  y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

634 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

635 
lemma dist_real: "dist(x::real ^ 1) y = abs((x$1)  (y$1))" 
30582  636 
by (auto simp add: norm_real dist_def) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

637 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

638 
subsection {* A connectedness or intermediate value lemma with several applications. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

639 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

640 
lemma connected_real_lemma: 
30582  641 
fixes f :: "real \<Rightarrow> real ^ 'n::finite" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

642 
assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

643 
and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y  x) < d \<longrightarrow> dist(f y) (f x) < e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

644 
and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

645 
and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

646 
and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

647 
shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

648 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

649 
let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}" 
30489  650 
have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa) 
651 
have Sub: "\<exists>y. isUb UNIV ?S y" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

652 
apply (rule exI[where x= b]) 
30489  653 
using ab fb e12 by (auto simp add: isUb_def setle_def) 
654 
from reals_complete[OF Se Sub] obtain l where 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

655 
l: "isLub UNIV ?S l"by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

656 
have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12 
30489  657 
apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

658 
by (metis linorder_linear) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

659 
have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

660 
apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

661 
by (metis linorder_linear not_le) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

662 
have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z  x) < d" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

663 
have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

664 
have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by dlo 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

665 
{assume le2: "f l \<in> e2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

666 
from le2 fa fb e12 alb have la: "l \<noteq> a" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

667 
hence lap: "l  a > 0" using alb by arith 
30489  668 
from e2[rule_format, OF le2] obtain e where 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

669 
e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis 
30489  670 
from dst[OF alb e(1)] obtain d where 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

671 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis 
30489  672 
have "\<exists>d'. d' < d \<and> d' >0 \<and> l  d' > a" using lap d(1) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

673 
apply ferrack by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

674 
then obtain d' where d': "d' > 0" "d' < d" "l  d' > a" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

675 
from d e have th0: "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> f y \<in> e2" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

676 
from th0[rule_format, of "l  d'"] d' have "f (l  d') \<in> e2" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

677 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

678 
have "f (l  d') \<in> e1" using ale1[rule_format, of "l d'"] d' by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

679 
ultimately have False using e12 alb d' by auto} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

680 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

681 
{assume le1: "f l \<in> e1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

682 
from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

683 
hence blp: "b  l > 0" using alb by arith 
30489  684 
from e1[rule_format, OF le1] obtain e where 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

685 
e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis 
30489  686 
from dst[OF alb e(1)] obtain d where 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

687 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis 
30489  688 
have "\<exists>d'. d' < d \<and> d' >0" using d(1) by dlo 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

689 
then obtain d' where d': "d' > 0" "d' < d" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

690 
from d e have th0: "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> f y \<in> e1" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

691 
hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

692 
with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto 
30489  693 
with l d' have False 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

694 
by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

695 
ultimately show ?thesis using alb by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

696 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

697 

29881  698 
text{* One immediately useful corollary is the existence of square roots!  Should help to get rid of all the development of squareroot for reals as a special case @{typ "real^1"} *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

699 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

700 
lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

701 
proof 
30489  702 
have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

703 
thus ?thesis by (simp add: ring_simps power2_eq_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

704 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

705 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

706 
lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y  x) < d \<longrightarrow> abs(y * y  x * x) < e)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

707 
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) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

708 
apply (rule_tac x="s" in exI) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

709 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

710 
apply (erule_tac x=y in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

711 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

712 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

713 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

714 
lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

715 
using real_sqrt_le_iff[of x "y^2"] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

716 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

717 
lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

718 
using real_sqrt_le_mono[of "x^2" y] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

719 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

720 
lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

721 
using real_sqrt_less_mono[of "x^2" y] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

722 

30489  723 
lemma sqrt_even_pow2: assumes n: "even n" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

724 
shows "sqrt(2 ^ n) = 2 ^ (n div 2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

725 
proof 
30489  726 
from n obtain m where m: "n = 2*m" unfolding even_nat_equiv_def2 
727 
by (auto simp add: nat_number) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

728 
from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

729 
by (simp only: power_mult[symmetric] mult_commute) 
30489  730 
then show ?thesis using m by simp 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

731 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

732 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

733 
lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

734 
apply (cases "x = 0", simp_all) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

735 
using sqrt_divide_self_eq[of x] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

736 
apply (simp add: inverse_eq_divide real_sqrt_ge_0_iff field_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

737 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

738 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

739 
text{* Hence derive more interesting properties of the norm. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

740 

30582  741 
text {* 
742 
This typespecific version is only here 

743 
to make @{text normarith.ML} happy. 

744 
*} 

745 
lemma norm_0: "norm (0::real ^ _) = 0" 

30040  746 
by (rule norm_zero) 
747 

30263  748 
lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x" 
30040  749 
by (simp add: vector_norm_def vector_component setL2_right_distrib 
750 
abs_mult cong: strong_setL2_cong) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

751 
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))" 
30040  752 
by (simp add: vector_norm_def dot_def setL2_def power2_eq_square) 
753 
lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)" 

754 
by (simp add: vector_norm_def setL2_def dot_def power2_eq_square) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

755 
lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x" 
30040  756 
by (simp add: real_vector_norm_def) 
30582  757 
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n::finite)" by (metis norm_eq_zero) 
30263  758 
lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

759 
by vector 
30263  760 
lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

761 
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) 
30263  762 
lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

763 
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

764 
lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==> a *s x = a *s y ==> (x = y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

765 
by (metis vector_mul_lcancel) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

766 
lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

767 
by (metis vector_mul_rcancel) 
30582  768 
lemma norm_cauchy_schwarz: 
769 
fixes x y :: "real ^ 'n::finite" 

770 
shows "x \<bullet> y <= norm x * norm y" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

771 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

772 
{assume "norm x = 0" 
30041  773 
hence ?thesis by (simp add: dot_lzero dot_rzero)} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

774 
moreover 
30489  775 
{assume "norm y = 0" 
30041  776 
hence ?thesis by (simp add: dot_lzero dot_rzero)} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

777 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

778 
{assume h: "norm x \<noteq> 0" "norm y \<noteq> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

779 
let ?z = "norm y *s x  norm x *s y" 
30041  780 
from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

781 
from dot_pos_le[of ?z] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

782 
have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

783 
apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

784 
by (simp add: norm_pow_2[symmetric] power2_eq_square dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

785 
hence "x\<bullet>y \<le> (norm x ^2 * norm y ^2) / (norm x * norm y)" using p 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

786 
by (simp add: field_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

787 
hence ?thesis using h by (simp add: power2_eq_square)} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

788 
ultimately show ?thesis by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

789 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

790 

30582  791 
lemma norm_cauchy_schwarz_abs: 
792 
fixes x y :: "real ^ 'n::finite" 

793 
shows "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

794 
using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "y"] 
30041  795 
by (simp add: real_abs_def dot_rneg) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

796 

30582  797 
lemma norm_triangle_sub: "norm (x::real ^'n::finite) <= norm(y) + norm(x  y)" 
30041  798 
using norm_triangle_ineq[of "y" "x  y"] by (simp add: ring_simps) 
30582  799 
lemma norm_triangle_le: "norm(x::real ^'n::finite) + norm y <= e ==> norm(x + y) <= e" 
30041  800 
by (metis order_trans norm_triangle_ineq) 
30582  801 
lemma norm_triangle_lt: "norm(x::real ^'n::finite) + norm(y) < e ==> norm(x + y) < e" 
30041  802 
by (metis basic_trans_rules(21) norm_triangle_ineq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

803 

30582  804 
lemma setsum_delta: 
805 
assumes fS: "finite S" 

806 
shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)" 

807 
proof 

808 
let ?f = "(\<lambda>k. if k=a then b k else 0)" 

809 
{assume a: "a \<notin> S" 

810 
hence "\<forall> k\<in> S. ?f k = 0" by simp 

811 
hence ?thesis using a by simp} 

812 
moreover 

813 
{assume a: "a \<in> S" 

814 
let ?A = "S  {a}" 

815 
let ?B = "{a}" 

816 
have eq: "S = ?A \<union> ?B" using a by blast 

817 
have dj: "?A \<inter> ?B = {}" by simp 

818 
from fS have fAB: "finite ?A" "finite ?B" by auto 

819 
have "setsum ?f S = setsum ?f ?A + setsum ?f ?B" 

820 
using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] 

821 
by simp 

822 
then have ?thesis using a by simp} 

823 
ultimately show ?thesis by blast 

824 
qed 

825 

826 
lemma component_le_norm: "\<bar>x$i\<bar> <= norm (x::real ^ 'n::finite)" 

30040  827 
apply (simp add: vector_norm_def) 
828 
apply (rule member_le_setL2, simp_all) 

829 
done 

830 

30582  831 
lemma norm_bound_component_le: "norm(x::real ^ 'n::finite) <= e 
832 
==> \<bar>x$i\<bar> <= e" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

833 
by (metis component_le_norm order_trans) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

834 

30582  835 
lemma norm_bound_component_lt: "norm(x::real ^ 'n::finite) < e 
836 
==> \<bar>x$i\<bar> < e" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

837 
by (metis component_le_norm basic_trans_rules(21)) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

838 

30582  839 
lemma norm_le_l1: "norm (x:: real ^'n::finite) <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV" 
30040  840 
by (simp add: vector_norm_def setL2_le_setsum) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

841 

30582  842 
lemma real_abs_norm: "\<bar>norm x\<bar> = norm (x :: real ^ _)" 
30040  843 
by (rule abs_norm_cancel) 
30582  844 
lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n::finite)  norm y\<bar> <= norm(x  y)" 
30040  845 
by (rule norm_triangle_ineq3) 
30582  846 
lemma norm_le: "norm(x::real ^ _) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

847 
by (simp add: real_vector_norm_def) 
30582  848 
lemma norm_lt: "norm(x::real ^ _) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

849 
by (simp add: real_vector_norm_def) 
30582  850 
lemma norm_eq: "norm (x::real ^ _) = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

851 
by (simp add: order_eq_iff norm_le) 
30582  852 
lemma norm_eq_1: "norm(x::real ^ _) = 1 \<longleftrightarrow> x \<bullet> x = 1" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

853 
by (simp add: real_vector_norm_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

854 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

855 
text{* Squaring equations and inequalities involving norms. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

856 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

857 
lemma dot_square_norm: "x \<bullet> x = norm(x)^2" 
30582  858 
by (simp add: real_vector_norm_def) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

859 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

860 
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2" 
30040  861 
by (auto simp add: real_vector_norm_def) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

862 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

863 
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

864 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

865 
have "x^2 \<le> y^2 \<longleftrightarrow> (x y) * (y + x) \<le> 0" by (simp add: ring_simps power2_eq_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

866 
also have "\<dots> \<longleftrightarrow> \<bar>x\<bar> \<le> \<bar>y\<bar>" apply (simp add: zero_compare_simps real_abs_def not_less) by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

867 
finally show ?thesis .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

868 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

869 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

870 
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2" 
30040  871 
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) 
30041  872 
using norm_ge_zero[of x] 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

873 
apply arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

874 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

875 

30489  876 
lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2" 
30040  877 
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) 
30041  878 
using norm_ge_zero[of x] 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

879 
apply arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

880 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

881 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

882 
lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

883 
by (metis not_le norm_ge_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

884 
lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

885 
by (metis norm_le_square not_less) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

886 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

887 
text{* Dot product in terms of the norm rather than conversely. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

888 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

889 
lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2  norm x ^ 2  norm y ^ 2) / 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

890 
by (simp add: norm_pow_2 dot_ladd dot_radd dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

891 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

892 
lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2)  norm(x  y) ^ 2) / 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

893 
by (simp add: norm_pow_2 dot_ladd dot_radd dot_lsub dot_rsub dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

894 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

895 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

896 
text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

897 

30582  898 
lemma vector_eq: "(x:: real ^ 'n::finite) = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y\<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs") 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

899 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

900 
assume "?lhs" then show ?rhs by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

901 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

902 
assume ?rhs 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

903 
then have "x \<bullet> x  x \<bullet> y = 0 \<and> x \<bullet> y  y\<bullet> y = 0" by simp 
30489  904 
hence "x \<bullet> (x  y) = 0 \<and> y \<bullet> (x  y) = 0" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

905 
by (simp add: dot_rsub dot_lsub dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

906 
then have "(x  y) \<bullet> (x  y) = 0" by (simp add: ring_simps dot_lsub dot_rsub) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

907 
then show "x = y" by (simp add: dot_eq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

908 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

909 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

910 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

911 
subsection{* General linear decision procedure for normed spaces. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

912 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

913 
lemma norm_cmul_rule_thm: "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(c *s x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

914 
apply (clarsimp simp add: norm_mul) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

915 
apply (rule mult_mono1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

916 
apply simp_all 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

917 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

918 

30263  919 
(* FIXME: Move all these theorems into the ML code using lemma antiquotation *) 
30582  920 
lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n::finite) \<Longrightarrow> b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

921 
apply (rule norm_triangle_le) by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

922 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

923 
lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \<ge> b == a  b \<ge> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

924 
by (simp add: ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

925 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

926 
lemma pth_1: "(x::real^'n) == 1 *s x" by (simp only: vector_smult_lid) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

927 
lemma pth_2: "x  (y::real^'n) == x + y" by (atomize (full)) simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

928 
lemma pth_3: "(x::real^'n) == 1 *s x" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

929 
lemma pth_4: "0 *s (x::real^'n) == 0" "c *s 0 = (0::real ^ 'n)" by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

930 
lemma pth_5: "c *s (d *s x) == (c * d) *s (x::real ^ 'n)" by (atomize (full)) vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

931 
lemma pth_6: "(c::real) *s (x + y) == c *s x + c *s y" by (atomize (full)) (vector ring_simps) 
30489  932 
lemma pth_7: "0 + x == (x::real^'n)" "x + 0 == x" by simp_all 
933 
lemma pth_8: "(c::real) *s x + d *s x == (c + d) *s x" by (atomize (full)) (vector ring_simps) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

934 
lemma pth_9: "((c::real) *s x + z) + d *s x == (c + d) *s x + z" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

935 
"c *s x + (d *s x + z) == (c + d) *s x + z" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

936 
"(c *s x + w) + (d *s x + z) == (c + d) *s x + (w + z)" by ((atomize (full)), vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

937 
lemma pth_a: "(0::real) *s x + y == y" by (atomize (full)) vector 
30489  938 
lemma pth_b: "(c::real) *s x + d *s y == c *s x + d *s y" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

939 
"(c *s x + z) + d *s y == c *s x + (z + d *s y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

940 
"c *s x + (d *s y + z) == c *s x + (d *s y + z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

941 
"(c *s x + w) + (d *s y + z) == c *s x + (w + (d *s y + z))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

942 
by ((atomize (full)), vector)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

943 
lemma pth_c: "(c::real) *s x + d *s y == d *s y + c *s x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

944 
"(c *s x + z) + d *s y == d *s y + (c *s x + z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

945 
"c *s x + (d *s y + z) == d *s y + (c *s x + z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

946 
"(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

947 
lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

948 

30582  949 
lemma norm_imp_pos_and_ge: "norm (x::real ^ _) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x" 
30041  950 
by (atomize) (auto simp add: norm_ge_zero) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

951 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

952 
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> x \<ge> 0" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

953 

30489  954 
lemma norm_pths: 
30582  955 
"(x::real ^'n::finite) = y \<longleftrightarrow> norm (x  y) \<le> 0" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

956 
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x  y) \<le> 0)" 
30041  957 
using norm_ge_zero[of "x  y"] by auto 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

958 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

959 
use "normarith.ML" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

960 

30549  961 
method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

962 
*} "Proves simple linear statements about vector norms" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

963 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

964 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

965 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

966 
text{* Hence more metric properties. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

967 

30263  968 
lemma dist_refl[simp]: "dist x x = 0" by norm 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

969 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

970 
lemma dist_sym: "dist x y = dist y x"by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

971 

30263  972 
lemma dist_pos_le[simp]: "0 <= dist x y" by norm 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

973 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

974 
lemma dist_triangle: "dist x z <= dist x y + dist y z" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

975 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

976 
lemma dist_triangle_alt: "dist y z <= dist x y + dist x z" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

977 

30263  978 
lemma dist_eq_0[simp]: "dist x y = 0 \<longleftrightarrow> x = y" by norm 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

979 

30489  980 
lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by norm 
981 
lemma dist_nz: "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by norm 

982 

983 
lemma dist_triangle_le: "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e" by norm 

984 

985 
lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e" by norm 

986 

987 
lemma dist_triangle_half_l: "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 ==> dist x1 x2 < e" by norm 

988 

989 
lemma dist_triangle_half_r: "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 ==> dist x1 x2 < e" by norm 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

990 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

991 
lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'" 
30489  992 
by norm 
993 

994 
lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y" 

995 
unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul .. 

996 

997 
lemma dist_triangle_add_half: " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 ==> dist(x + y) (x' + y') < e" by norm 

998 

999 
lemma dist_le_0[simp]: "dist x y <= 0 \<longleftrightarrow> x = y" by norm 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1000 

30582  1001 
lemma setsum_component [simp]: 
1002 
fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n" 

1003 
shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S" 

1004 
by (cases "finite S", induct S set: finite, simp_all) 

1005 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1006 
lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)" 
30582  1007 
by (simp add: Cart_eq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1008 

30489  1009 
lemma setsum_clauses: 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1010 
shows "setsum f {} = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1011 
and "finite S \<Longrightarrow> setsum f (insert x S) = 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1012 
(if x \<in> S then setsum f S else f x + setsum f S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1013 
by (auto simp add: insert_absorb) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1014 

30489  1015 
lemma setsum_cmul: 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1016 
fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1017 
shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S" 
30582  1018 
by (simp add: Cart_eq setsum_right_distrib) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1019 

30489  1020 
lemma setsum_norm: 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1021 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1022 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1023 
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1024 
proof(induct rule: finite_induct[OF fS]) 
30041  1025 
case 1 thus ?case by simp 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1026 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1027 
case (2 x S) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1028 
from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1029 
also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1030 
using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1031 
finally show ?case using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1032 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1033 

30489  1034 
lemma real_setsum_norm: 
30582  1035 
fixes f :: "'a \<Rightarrow> real ^'n::finite" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1036 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1037 
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1038 
proof(induct rule: finite_induct[OF fS]) 
30040  1039 
case 1 thus ?case by simp 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1040 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1041 
case (2 x S) 
30040  1042 
from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1043 
also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1044 
using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1045 
finally show ?case using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1046 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1047 

30489  1048 
lemma setsum_norm_le: 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1049 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1050 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1051 
and fg: "\<forall>x \<in> S. norm (f x) \<le> g x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1052 
shows "norm (setsum f S) \<le> setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1053 
proof 
30489  1054 
from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1055 
by  (rule setsum_mono, simp) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1056 
then show ?thesis using setsum_norm[OF fS, of f] fg 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1057 
by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1058 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1059 

30489  1060 
lemma real_setsum_norm_le: 
30582  1061 
fixes f :: "'a \<Rightarrow> real ^ 'n::finite" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1062 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1063 
and fg: "\<forall>x \<in> S. norm (f x) \<le> g x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1064 
shows "norm (setsum f S) \<le> setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1065 
proof 
30489  1066 
from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1067 
by  (rule setsum_mono, simp) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1068 
then show ?thesis using real_setsum_norm[OF fS, of f] fg 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1069 
by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1070 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1071 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1072 
lemma setsum_norm_bound: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1073 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1074 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1075 
and K: "\<forall>x \<in> S. norm (f x) \<le> K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1076 
shows "norm (setsum f S) \<le> of_nat (card S) * K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1077 
using setsum_norm_le[OF fS K] setsum_constant[symmetric] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1078 
by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1079 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1080 
lemma real_setsum_norm_bound: 
30582  1081 
fixes f :: "'a \<Rightarrow> real ^ 'n::finite" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1082 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1083 
and K: "\<forall>x \<in> S. norm (f x) \<le> K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1084 
shows "norm (setsum f S) \<le> of_nat (card S) * K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1085 
using real_setsum_norm_le[OF fS K] setsum_constant[symmetric] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1086 
by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1087 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1088 
lemma setsum_vmul: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1089 
fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector,semiring, mult_zero}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1090 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1091 
shows "setsum f S *s v = setsum (\<lambda>x. f x *s v) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1092 
proof(induct rule: finite_induct[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1093 
case 1 then show ?case by (simp add: vector_smult_lzero) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1094 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1095 
case (2 x F) 
30489  1096 
from "2.hyps" have "setsum f (insert x F) *s v = (f x + setsum f F) *s v" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1097 
by simp 
30489  1098 
also have "\<dots> = f x *s v + setsum f F *s v" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1099 
by (simp add: vector_sadd_rdistrib) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1100 
also have "\<dots> = setsum (\<lambda>x. f x *s v) (insert x F)" using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1101 
finally show ?case . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1102 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1103 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1104 
(* FIXME : Problem thm setsum_vmul[of _ "f:: 'a \<Rightarrow> real ^'n"]  
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1105 
Get rid of *s and use real_vector instead! Also prove that ^ creates a real_vector !! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1106 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1107 
lemma setsum_add_split: assumes mn: "(m::nat) \<le> n + 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1108 
shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1109 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1110 
let ?A = "{m .. n}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1111 
let ?B = "{n + 1 .. n + p}" 
30489  1112 
have eq: "{m .. n+p} = ?A \<union> ?B" using mn by auto 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1113 
have d: "?A \<inter> ?B = {}" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1114 
from setsum_Un_disjoint[of "?A" "?B" f] eq d show ?thesis by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1115 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1116 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1117 
lemma setsum_natinterval_left: 
30489  1118 
assumes mn: "(m::nat) <= n" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1119 
shows "setsum f {m..n} = f m + setsum f {m + 1..n}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1120 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1121 
from mn have "{m .. n} = insert m {m+1 .. n}" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1122 
then show ?thesis by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1123 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1124 

30489  1125 
lemma setsum_natinterval_difff: 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1126 
fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1127 
shows "setsum (\<lambda>k. f k  f(k + 1)) {(m::nat) .. n} = 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1128 
(if m <= n then f m  f(n + 1) else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1129 
by (induct n, auto simp add: ring_simps not_le le_Suc_eq) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1130 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1131 
lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1132 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1133 
lemma setsum_setsum_restrict: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1134 
"finite S \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1135 
apply (simp add: setsum_restrict_set'[unfolded mem_def] mem_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1136 
by (rule setsum_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1137 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1138 
lemma setsum_image_gen: assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1139 
shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1140 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1141 
{fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1142 
note th0 = this 
30489  1143 
have "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S" 
1144 
apply (rule setsum_cong2) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1145 
by (simp add: th0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1146 
also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1147 
apply (rule setsum_setsum_restrict[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1148 
by (rule finite_imageI[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1149 
finally show ?thesis . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1150 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1151 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1152 
(* FIXME: Here too need stupid finiteness assumption on T!!! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1153 
lemma setsum_group: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1154 
assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1155 
shows "setsum (\<lambda>y. setsum g {x. x\<in> S \<and> f x = y}) T = setsum g S" 
30489  1156 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1157 
apply (subst setsum_image_gen[OF fS, of g f]) 
30263  1158 
apply (rule setsum_mono_zero_right[OF fT fST]) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1159 
by (auto intro: setsum_0') 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1160 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1161 
lemma vsum_norm_allsubsets_bound: 
30582  1162 
fixes f:: "'a \<Rightarrow> real ^'n::finite" 
30489  1163 
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e" 
30582  1164 
shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) * e" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1165 
proof 
30582  1166 
let ?d = "real CARD('n)" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1167 
let ?nf = "\<lambda>x. norm (f x)" 
30582  1168 
let ?U = "UNIV :: 'n set" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1169 
have th0: "setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $ i\<bar>) ?U) P = setsum (\<lambda>i. setsum (\<lambda>x. \<bar>f x $ i\<bar>) P) ?U" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1170 
by (rule setsum_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1171 
have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1172 
have "setsum ?nf P \<le> setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $ i\<bar>) ?U) P" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1173 
apply (rule setsum_mono) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1174 
by (rule norm_le_l1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1175 
also have "\<dots> \<le> 2 * ?d * e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1176 
unfolding th0 th1 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1177 
proof(rule setsum_bounded) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1178 
fix i assume i: "i \<in> ?U" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1179 
let ?Pp = "{x. x\<in> P \<and> f x $ i \<ge> 0}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1180 
let ?Pn = "{x. x \<in> P \<and> f x $ i < 0}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1181 
have thp: "P = ?Pp \<union> ?Pn" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1182 
have thp0: "?Pp \<inter> ?Pn ={}" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1183 
have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1184 
have Ppe:"setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp \<le> e" 
30582  1185 
using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i] fPs[OF PpP] 
1186 
by (auto intro: abs_le_D1) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1187 
have Pne: "setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn \<le> e" 
30582  1188 
using component_le_norm[of "setsum (\<lambda>x.  f x) ?Pn" i] fPs[OF PnP] 
1189 
by (auto simp add: setsum_negf intro: abs_le_D1) 

30489  1190 
have "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1191 
apply (subst thp) 
30489  1192 
apply (rule setsum_Un_zero) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1193 
using fP thp0 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1194 
also have "\<dots> \<le> 2*e" using Pne Ppe by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1195 
finally show "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P \<le> 2*e" . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1196 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1197 
finally show ?thesis . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1198 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1199 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1200 
lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n) = setsum (\<lambda>x. f x \<bullet> y) S " 
30263  1201 
by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1202 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1203 
lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{comm_ring}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S " 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1204 
by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1205 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1206 
subsection{* Basis vectors in coordinate directions. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1207 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1208 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1209 
definition "basis k = (\<chi> i. if i = k then 1 else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1210 

30582  1211 
lemma basis_component [simp]: "basis k $ i = (if k=i then 1 else 0)" 
1212 
unfolding basis_def by simp 

1213 

30489  1214 
lemma delta_mult_idempotent: 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1215 
"(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) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1216 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1217 
lemma norm_basis: 
30582  1218 
shows "norm (basis k :: real ^'n::finite) = 1" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1219 
apply (simp add: basis_def real_vector_norm_def dot_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1220 
apply (vector delta_mult_idempotent) 
30582  1221 
using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"] 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1222 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1223 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1224 

30582  1225 
lemma norm_basis_1: "norm(basis 1 :: real ^'n::{finite,one}) = 1" 
1226 
by (rule norm_basis) 

1227 

1228 
lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n::finite). norm x = c" 

1229 
apply (rule exI[where x="c *s basis arbitrary"]) 

1230 
by (simp only: norm_mul norm_basis) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1231 

30489  1232 
lemma vector_choose_dist: assumes e: "0 <= e" 
30582  1233 
shows "\<exists>(y::real^'n::finite). dist x y = e" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1234 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1235 
from vector_choose_size[OF e] obtain c:: "real ^'n" where "norm c = e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1236 
by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1237 
then have "dist x (x  c) = e" by (simp add: dist_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1238 
then show ?thesis by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1239 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1240 

30582  1241 
lemma basis_inj: "inj (basis :: 'n \<Rightarrow> real ^'n::finite)" 
1242 
by (simp add: inj_on_def Cart_eq) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1243 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1244 
lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1245 
by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1246 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1247 
lemma basis_expansion: 
30582  1248 
"setsum (\<lambda>i. (x$i) *s basis i) UNIV = (x::('a::ring_1) ^'n::finite)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") 
1249 
by (auto simp add: Cart_eq cond_value_iff setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1250 

30489  1251 
lemma basis_expansion_unique: 
30582  1252 
"setsum (\<lambda>i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n::finite) \<longleftrightarrow> (\<forall>i. f i = x$i)" 
1253 
by (simp add: Cart_eq setsum_delta cond_value_iff cong del: if_weak_cong) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1254 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1255 
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1256 
by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1257 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1258 
lemma dot_basis: 
30582  1259 
shows "basis i \<bullet> x = x$i" "x \<bullet> (basis i :: 'a^'n::finite) = (x$i :: 'a::semiring_1)" 
1260 
by (auto simp add: dot_def basis_def cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong) 

1261 

1262 
lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> False" 

1263 
by (auto simp add: Cart_eq) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1264 

30489  1265 
lemma basis_nonzero: 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1266 
shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n)" 
30582  1267 
by (simp add: basis_eq_0) 
1268 

1269 
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::'a::semiring_1^'n::finite)" 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1270 
apply (auto simp add: Cart_eq dot_basis) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1271 
apply (erule_tac x="basis i" in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1272 
apply (simp add: dot_basis) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1273 
apply (subgoal_tac "y = z") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1274 
apply simp 
30582  1275 
apply (simp add: Cart_eq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1276 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1277 

30582  1278 
lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::'a::semiring_1^'n::finite)" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1279 
apply (auto simp add: Cart_eq dot_basis) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1280 
apply (erule_tac x="basis i" in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1281 
apply (simp add: dot_basis) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1282 
apply (subgoal_tac "x = y") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1283 
apply simp 
30582  1284 
apply (simp add: Cart_eq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1285 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1286 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1287 
subsection{* Orthogonality. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1288 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1289 
definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1290 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1291 
lemma orthogonal_basis: 
30582  1292 
shows "orthogonal (basis i :: 'a^'n::finite) x \<longleftrightarrow> x$i = (0::'a::ring_1)" 
1293 
by (auto simp add: orthogonal_def dot_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1294 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1295 
lemma orthogonal_basis_basis: 
30582  1296 
shows "orthogonal (basis i :: 'a::ring_1^'n::finite) (basis j) \<longleftrightarrow> i \<noteq> j" 
1297 
unfolding orthogonal_basis[of i] basis_component[of j] by simp 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1298 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1299 
(* FIXME : Maybe some of these require less than comm_ring, but not all*) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1300 
lemma orthogonal_clauses: 
