author  haftmann 
Mon, 23 Mar 2009 08:16:24 +0100  
changeset 30665  4cf38ea4fad2 
parent 30655  88131f2807b6 
parent 30661  54858c8ad226 
child 30960  fec1a04b7220 
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 
30661  8 
imports 
30665  9 
Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order" 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

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

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

14 

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

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

16 

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

19 

20 
lemma exhaust_2: 

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

22 
proof (induct x) 

23 
case (of_int z) 

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

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

26 
then show ?case by auto 

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

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

28 

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

31 

32 
lemma exhaust_3: 

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

34 
proof (induct x) 

35 
case (of_int z) 

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

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

38 
then show ?case by auto 

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

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

40 

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

43 

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

45 
by (auto simp add: num1_eq_iff) 

46 

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

48 
using exhaust_2 by auto 

49 

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

51 
using exhaust_3 by auto 

52 

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

54 
unfolding UNIV_1 by simp 

55 

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

57 
unfolding UNIV_2 by simp 

58 

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

60 
unfolding UNIV_3 by (simp add: add_ac) 

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

61 

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

63 

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

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

65 
begin 
30489  66 
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

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

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

69 

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

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

71 
begin 
30489  72 
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

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

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

75 

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

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

77 
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

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

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

80 

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

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

82 
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

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

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

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

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

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

89 

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

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

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

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

94 

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

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

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

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

30489  100 

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

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

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

103 

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

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

109 

110 
text{* Also the scalarvector multiplication. *} 

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

111 

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

112 
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

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

114 

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

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

116 

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

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

118 

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

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

120 

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

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

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

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

126 

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

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

129 

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

130 
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  131 
by (simp add: dot_def setsum_3) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

132 

29906  133 
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

134 

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

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

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

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

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

142 
@{thm vector_minus_def}, @{thm vector_uminus_def}, 

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

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

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

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

150 
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

151 
(* 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

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

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

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

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

157 

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

158 
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

159 
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

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 

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

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

164 

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

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

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

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

173 
lemma vector_minus_component [simp]: 

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

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

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

178 
lemma vector_mult_component [simp]: 

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

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

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

183 
lemma vector_smult_component [simp]: 

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

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

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

188 
lemma vector_uminus_component [simp]: 

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

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

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

193 
lemma vector_scaleR_component [simp]: 

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

30582  196 
by vector 
30039  197 

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

198 
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

199 

30039  200 
lemmas vector_component = 
201 
vec_component vector_add_component vector_mult_component 

202 
vector_smult_component vector_minus_component vector_uminus_component 

203 
vector_scaleR_component cond_component 

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

204 

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

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

206 

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

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

209 

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

210 

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

213 

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

215 
apply (intro_classes) by (vector algebra_simps)+ 

216 

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

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

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

219 

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

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

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

222 

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

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

225 

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

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

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

229 

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

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

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

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

233 

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

236 

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

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

239 

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

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

242 

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

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

245 

30489  246 
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

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

248 

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

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

251 

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

252 
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

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

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

255 

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

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

258 
definition vec_power_def: "op ^ \<equiv> vector_power" 
30489  259 
instance 
260 
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

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

262 

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

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

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

265 

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

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

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

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

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

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

272 

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

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

278 
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

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

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

282 

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

284 
apply intro_classes 

285 
apply (simp_all add: vector_scaleR_def ring_simps) 

286 
apply vector 

287 
apply vector 

288 
done 

289 

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

291 

30489  292 
lemma of_nat_index: 
30582  293 
"(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

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

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

300 

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

303 

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

304 
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

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

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

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

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

310 

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

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

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

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

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

317 

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

318 
instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes 
30039  319 
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

320 

30489  321 
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

322 
by (vector mult_assoc) 
30489  323 
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

324 
by (vector ring_simps) 
30489  325 
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

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

327 
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

328 
lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector 
30489  329 
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

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

331 
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

332 
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

333 
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

334 
lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector 
30489  335 
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

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

337 

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

340 

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

343 
definition 

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

345 

346 
lemma setL2_cong: 

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

348 
unfolding setL2_def by simp 

349 

350 
lemma strong_setL2_cong: 

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

352 
unfolding setL2_def simp_implies_def by simp 

353 

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

355 
unfolding setL2_def by simp 

356 

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

358 
unfolding setL2_def by simp 

359 

360 
lemma setL2_insert [simp]: 

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

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

363 
unfolding setL2_def by (simp add: setsum_nonneg) 

364 

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

366 
unfolding setL2_def by (simp add: setsum_nonneg) 

367 

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

369 
unfolding setL2_def by simp 

370 

371 
lemma setL2_mono: 

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

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

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

375 
unfolding setL2_def 

376 
by (simp add: setsum_nonneg setsum_mono power_mono prems) 

377 

378 
lemma setL2_right_distrib: 

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

380 
unfolding setL2_def 

381 
apply (simp add: power_mult_distrib) 

382 
apply (simp add: setsum_right_distrib [symmetric]) 

383 
apply (simp add: real_sqrt_mult setsum_nonneg) 

384 
done 

385 

386 
lemma setL2_left_distrib: 

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

388 
unfolding setL2_def 

389 
apply (simp add: power_mult_distrib) 

390 
apply (simp add: setsum_left_distrib [symmetric]) 

391 
apply (simp add: real_sqrt_mult setsum_nonneg) 

392 
done 

393 

394 
lemma setsum_nonneg_eq_0_iff: 

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

396 
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)" 

397 
apply (induct set: finite, simp) 

398 
apply (simp add: add_nonneg_eq_0_iff setsum_nonneg) 

399 
done 

400 

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

402 
unfolding setL2_def 

403 
by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff) 

404 

405 
lemma setL2_triangle_ineq: 

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

407 
proof (cases "finite A") 

408 
case False 

409 
thus ?thesis by simp 

410 
next 

411 
case True 

412 
thus ?thesis 

413 
proof (induct set: finite) 

414 
case empty 

415 
show ?case by simp 

416 
next 

417 
case (insert x F) 

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

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

420 
by (intro real_sqrt_le_mono add_left_mono power_mono insert 

421 
setL2_nonneg add_increasing zero_le_power2) 

422 
also have 

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

424 
by (rule real_sqrt_sum_squares_triangle_ineq) 

425 
finally show ?case 

426 
using insert by simp 

427 
qed 

428 
qed 

429 

430 
lemma sqrt_sum_squares_le_sum: 

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

432 
apply (rule power2_le_imp_le) 

433 
apply (simp add: power2_sum) 

434 
apply (simp add: mult_nonneg_nonneg) 

435 
apply (simp add: add_nonneg_nonneg) 

436 
done 

437 

438 
lemma setL2_le_setsum [rule_format]: 

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

440 
apply (cases "finite A") 

441 
apply (induct set: finite) 

442 
apply simp 

443 
apply clarsimp 

444 
apply (erule order_trans [OF sqrt_sum_squares_le_sum]) 

445 
apply simp 

446 
apply simp 

447 
apply simp 

448 
done 

449 

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

451 
apply (rule power2_le_imp_le) 

452 
apply (simp add: power2_sum) 

453 
apply (simp add: mult_nonneg_nonneg) 

454 
apply (simp add: add_nonneg_nonneg) 

455 
done 

456 

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

458 
apply (cases "finite A") 

459 
apply (induct set: finite) 

460 
apply simp 

461 
apply simp 

462 
apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs]) 

463 
apply simp 

464 
apply simp 

465 
done 

466 

467 
lemma setL2_mult_ineq_lemma: 

468 
fixes a b c d :: real 

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

470 
proof  

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

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

473 
by (simp only: power2_diff power_mult_distrib) 

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

475 
by simp 

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

477 
by simp 

478 
qed 

479 

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

481 
apply (cases "finite A") 

482 
apply (induct set: finite) 

483 
apply simp 

484 
apply (rule power2_le_imp_le, simp) 

485 
apply (rule order_trans) 

486 
apply (rule power_mono) 

487 
apply (erule add_left_mono) 

488 
apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg) 

489 
apply (simp add: power2_sum) 

490 
apply (simp add: power_mult_distrib) 

491 
apply (simp add: right_distrib left_distrib) 

492 
apply (rule ord_le_eq_trans) 

493 
apply (rule setL2_mult_ineq_lemma) 

494 
apply simp 

495 
apply (intro mult_nonneg_nonneg setL2_nonneg) 

496 
apply simp 

497 
done 

498 

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

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

501 
apply fast 

502 
apply (subst setL2_insert) 

503 
apply simp 

504 
apply simp 

505 
apply simp 

506 
done 

507 

508 
subsection {* Norms *} 

509 

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

513 
definition vector_norm_def: 

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

516 
definition vector_sgn_def: 

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

518 

519 
instance proof 

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

521 
show "0 \<le> norm x" 

522 
unfolding vector_norm_def 

523 
by (rule setL2_nonneg) 

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

525 
unfolding vector_norm_def 

526 
by (simp add: setL2_eq_0_iff Cart_eq) 

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

528 
unfolding vector_norm_def 

529 
apply (rule order_trans [OF _ setL2_triangle_ineq]) 

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

533 
unfolding vector_norm_def 

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

537 
qed 

538 

539 
end 

540 

30045  541 
subsection {* Inner products *} 
542 

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

546 
definition vector_inner_def: 

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

549 
instance proof 

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

551 
show "inner x y = inner y x" 

552 
unfolding vector_inner_def 

553 
by (simp add: inner_commute) 

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

555 
unfolding vector_inner_def 

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

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

562 
by (simp add: setsum_nonneg) 

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

564 
unfolding vector_inner_def 

565 
by (simp add: Cart_eq setsum_nonneg_eq_0_iff) 

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

567 
unfolding vector_inner_def vector_norm_def setL2_def 

568 
by (simp add: power2_norm_eq_inner) 

569 
qed 

570 

571 
end 

572 

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

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

574 

30489  575 
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

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

577 
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

578 
by (vector ring_simps) 
30489  579 
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

580 
by (vector ring_simps) 
30489  581 
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

582 
by (vector ring_simps) 
30489  583 
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

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

585 
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

586 
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

587 
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

588 
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

589 
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

590 
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

591 
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

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

593 

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

594 
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

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

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

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

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

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

600 
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

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

602 
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

603 
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

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

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

606 

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

609 

610 
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  611 
by (auto simp add: le_less) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

612 

30040  613 
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

614 

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

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

617 

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

618 
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

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

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

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

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

623 

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

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

629 

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

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

631 

30040  632 
text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *} 
30582  633 
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

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

635 

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

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

638 

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

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

640 

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

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

643 
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

644 
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

645 
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

646 
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

647 
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

648 
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

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

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

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

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

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

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

657 
have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12 
30489  658 
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

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

660 
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

661 
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

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

663 
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

664 
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

665 
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

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

667 
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

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

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

672 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis 
30489  673 
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

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

675 
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

676 
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

677 
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

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

679 
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

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

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

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

683 
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

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

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

688 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis 
30489  689 
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

690 
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

691 
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

692 
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

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

695 
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

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

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

698 

29881  699 
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

700 

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

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

702 
proof 
30489  703 
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

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

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

706 

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

707 
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

708 
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

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

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

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

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

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

714 

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

715 
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

716 
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

717 

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

718 
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

719 
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

720 

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

721 
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

722 
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

723 

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

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

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

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

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

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

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

733 

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

734 
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

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

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

737 
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

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

739 

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

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

741 

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

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

745 
*} 

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

30040  747 
by (rule norm_zero) 
748 

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

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

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

755 
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

756 
lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x" 
30040  757 
by (simp add: real_vector_norm_def) 
30582  758 
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n::finite)" by (metis norm_eq_zero) 
30263  759 
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

760 
by vector 
30263  761 
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

762 
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) 
30263  763 
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

764 
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

765 
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

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

767 
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

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

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

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

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

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

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

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

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

780 
let ?z = "norm y *s x  norm x *s y" 
30041  781 
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

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

783 
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

784 
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

785 
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

786 
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

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

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

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

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

791 

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

794 
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

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

797 

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

804 

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

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

808 
proof 

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

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

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

812 
hence ?thesis using a by simp} 

813 
moreover 

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

815 
let ?A = "S  {a}" 

816 
let ?B = "{a}" 

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

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

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

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

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

822 
by simp 

823 
then have ?thesis using a by simp} 

824 
ultimately show ?thesis by blast 

825 
qed 

826 

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

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

830 
done 

831 

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

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

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

835 

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

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

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

839 

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

842 

30582  843 
lemma real_abs_norm: "\<bar>norm x\<bar> = norm (x :: real ^ _)" 
30040  844 
by (rule abs_norm_cancel) 
30582  845 
lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n::finite)  norm y\<bar> <= norm(x  y)" 
30040  846 
by (rule norm_triangle_ineq3) 
30582  847 
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

848 
by (simp add: real_vector_norm_def) 
30582  849 
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

850 
by (simp add: real_vector_norm_def) 
30582  851 
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

852 
by (simp add: order_eq_iff norm_le) 
30582  853 
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

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

855 

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

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

857 

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

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

860 

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

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

863 

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

864 
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

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

866 
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

867 
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

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

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

870 

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

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

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

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

876 

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

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

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

882 

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

883 
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

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

885 
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

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

887 

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

888 
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

889 

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

890 
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

891 
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

892 

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

893 
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

894 
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

895 

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

896 

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

897 
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

898 

30582  899 
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

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

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

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

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

904 
then have "x \<bullet> x  x \<bullet> y = 0 \<and> x \<bullet> y  y\<bullet> y = 0" by simp 
30489  905 
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

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

907 
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

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

909 
qed 
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 

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

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

913 

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

914 
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

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

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

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

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

919 

30263  920 
(* FIXME: Move all these theorems into the ML code using lemma antiquotation *) 
30582  921 
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

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

923 

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

924 
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

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

926 

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

927 
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

928 
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

929 
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

930 
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

931 
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

932 
lemma pth_6: "(c::real) *s (x + y) == c *s x + c *s y" by (atomize (full)) (vector ring_simps) 
30489  933 
lemma pth_7: "0 + x == (x::real^'n)" "x + 0 == x" by simp_all 
934 
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

935 
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

936 
"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

937 
"(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

938 
lemma pth_a: "(0::real) *s x + y == y" by (atomize (full)) vector 
30489  939 
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

940 
"(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

941 
"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

942 
"(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

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

944 
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

945 
"(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

946 
"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

947 
"(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

948 
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

949 

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

952 

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

953 
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

954 

30489  955 
lemma norm_pths: 
30582  956 
"(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

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

959 

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

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

961 

30549  962 
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

963 
*} "Proves simple linear statements about vector norms" 
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 

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

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

968 

30263  969 
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

970 

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

971 
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

972 

30263  973 
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

974 

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

975 
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

976 

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

977 
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

978 

30263  979 
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

980 

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

983 

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

985 

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

987 

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

989 

990 
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

991 

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

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

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

996 
unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul .. 

997 

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

999 

1000 
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

1001 

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

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

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

1006 

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

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

1009 

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

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

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

1013 
(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

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

1015 

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

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

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

1020 

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

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

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

1024 
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

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

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

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

1029 
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

1030 
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

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

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

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

1034 

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

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

1038 
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

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

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

1042 
case (2 x S) 
30040  1043 
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

1044 
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

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

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

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

1048 

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

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

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

1052 
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

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

1054 
proof 
30489  1055 
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

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

1057 
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

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

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

1060 

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

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

1064 
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

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

1066 
proof 
30489  1067 
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

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

1069 
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

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

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

1072 

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

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

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

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

1076 
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

1077 
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

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

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

1080 

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

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

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

1084 
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

1085 
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

1086 
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

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

1088 

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

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

1090 
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

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

1092 
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

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

1094 
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

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

1096 
case (2 x F) 
30489  1097 
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

1098 
by simp 
30489  1099 
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

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

1101 
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

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

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

1104 

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

1105 
(* 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

1106 
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

1107 

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

1108 
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

1109 
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

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

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

1112 
let ?B = "{n + 1 .. n + p}" 
30489  1113 
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

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

1115 
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

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

1117 

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

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

1120 
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

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

1122 
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

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

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

1125 

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

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

1128 
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

1129 
(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

1130 
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

1131 

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

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

1133 

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

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

1135 
"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

1136 
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

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

1138 

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

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

1140 
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

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

1142 
{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

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

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

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

1147 
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

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

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

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

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

1152 

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

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

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

1155 
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

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

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

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

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

1161 

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

1162 
lemma vsum_norm_allsubsets_bound: 
30582  1163 
fixes f:: "'a \<Rightarrow> real ^'n::finite" 
30489  1164 
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e" 
30582  1165 
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

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

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

1170 
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

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

1172 
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

1173 
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

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

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

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

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

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

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

1180 
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

1181 
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

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

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

1184 
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

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

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

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

30489  1191 
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

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

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

1195 
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

1196 
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

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

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

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

1200 

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

1201 
lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n) = setsum (\<lambda>x. f x \<bullet> y) S " 
30263  1202 
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

1203 

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

1204 
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

1205 
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

1206 

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

1207 
subsection{* Basis vectors in coordinate directions. *} 
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 

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

1210 
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

1211 

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

1214 

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

1216 
"(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

1217 

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

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

1220 
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

1221 
apply (vector delta_mult_idempotent) 
30582  1222 
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

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

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

1225 

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

1228 

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

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

1231 
by (simp only: norm_mul norm_basis) 

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

1232 

30489  1233 
lemma vector_choose_dist: assumes e: "0 <= e" 
30582  1234 
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

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

1236 
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

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

1238 
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

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

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

1241 

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

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

1244 

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

1245 
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

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

1247 

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

1248 
lemma basis_expansion: 
30582  1249 
"setsum (\<lambda>i. (x$i) *s basis i) UNIV = (x::('a::ring_1) ^'n::finite)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") 
1250 
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

1251 

30489  1252 
lemma basis_expansion_unique: 
30582  1253 
"setsum (\<lambda>i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n::finite) \<longleftrightarrow> (\<forall>i. f i = x$i)" 
1254 
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

1255 

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

1256 
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

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

1258 

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

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

1262 

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

1264 
by (auto simp add: Cart_eq) 

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

1265 

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

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

1270 
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

1271 
apply (auto simp add: Cart_eq dot_basis) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

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

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

1274 
apply (subgoal_tac "y = z") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1275 
apply simp 
30582  1276 
apply (simp add: Cart_eq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

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

1278 

30582  1279 
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

1280 
apply (auto simp add: Cart_eq dot_basis) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

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

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

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

1284 
apply simp 
30582  1285 
apply (simp add: Cart_eq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

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

1287 

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

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

1289 

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

1290 
definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1291 

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

1292 
lemma orthogonal_basis: 
30582  1293 
shows "orthogonal (basis i :: 'a^'n::finite) x \<longleftrightarrow> x$i = (0::'a::ring_1)" 
1294 
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

1295 

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

1296 
lemma orthogonal_basis_basis: 
30582  1297 
shows "orthogonal (basis i :: 'a::ring_1^'n::finite) (basis j) \<longleftrightarrow> i \<noteq> j" 
1298 
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

1299 

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