author  huffman 
Tue, 09 Aug 2011 10:42:07 0700  
changeset 44126  ce44e70d0c47 
parent 44066  d74182c93f04 
child 44127  7b57b9295d98 
permissions  rwrr 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

1 
(* Title: HOL/Library/Product_Vector.thy 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

2 
Author: Brian Huffman 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

3 
*) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

4 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

5 
header {* Cartesian Products as Vector Spaces *} 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

6 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

7 
theory Product_Vector 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

8 
imports Inner_Product Product_plus 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

9 
begin 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

10 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

11 
subsection {* Product is a real vector space *} 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

12 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset

13 
instantiation prod :: (real_vector, real_vector) real_vector 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

14 
begin 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

15 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

16 
definition scaleR_prod_def: 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

17 
"scaleR r A = (scaleR r (fst A), scaleR r (snd A))" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

18 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

19 
lemma fst_scaleR [simp]: "fst (scaleR r A) = scaleR r (fst A)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

20 
unfolding scaleR_prod_def by simp 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

21 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

22 
lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

23 
unfolding scaleR_prod_def by simp 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

24 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

25 
lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

26 
unfolding scaleR_prod_def by simp 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

27 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

28 
instance proof 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

29 
fix a b :: real and x y :: "'a \<times> 'b" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

30 
show "scaleR a (x + y) = scaleR a x + scaleR a y" 
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset

31 
by (simp add: prod_eq_iff scaleR_right_distrib) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

32 
show "scaleR (a + b) x = scaleR a x + scaleR b x" 
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset

33 
by (simp add: prod_eq_iff scaleR_left_distrib) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

34 
show "scaleR a (scaleR b x) = scaleR (a * b) x" 
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset

35 
by (simp add: prod_eq_iff) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

36 
show "scaleR 1 x = x" 
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset

37 
by (simp add: prod_eq_iff) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

38 
qed 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

39 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

40 
end 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

41 

31415  42 
subsection {* Product is a topological space *} 
43 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset

44 
instantiation prod :: (topological_space, topological_space) topological_space 
31415  45 
begin 
46 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

47 
definition open_prod_def: 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

48 
"open (S :: ('a \<times> 'b) set) \<longleftrightarrow> 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

49 
(\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)" 
31415  50 

36332  51 
lemma open_prod_elim: 
52 
assumes "open S" and "x \<in> S" 

53 
obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S" 

54 
using assms unfolding open_prod_def by fast 

55 

56 
lemma open_prod_intro: 

57 
assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" 

58 
shows "open S" 

59 
using assms unfolding open_prod_def by fast 

60 

31415  61 
instance proof 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

62 
show "open (UNIV :: ('a \<times> 'b) set)" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

63 
unfolding open_prod_def by auto 
31415  64 
next 
65 
fix S T :: "('a \<times> 'b) set" 

36332  66 
assume "open S" "open T" 
67 
show "open (S \<inter> T)" 

68 
proof (rule open_prod_intro) 

69 
fix x assume x: "x \<in> S \<inter> T" 

70 
from x have "x \<in> S" by simp 

71 
obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S" 

72 
using `open S` and `x \<in> S` by (rule open_prod_elim) 

73 
from x have "x \<in> T" by simp 

74 
obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T" 

75 
using `open T` and `x \<in> T` by (rule open_prod_elim) 

76 
let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb" 

77 
have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T" 

78 
using A B by (auto simp add: open_Int) 

79 
thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T" 

80 
by fast 

81 
qed 

31415  82 
next 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

83 
fix K :: "('a \<times> 'b) set set" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

84 
assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

85 
unfolding open_prod_def by fast 
31415  86 
qed 
87 

88 
end 

89 

31562  90 
lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)" 
91 
unfolding open_prod_def by auto 

92 

93 
lemma fst_vimage_eq_Times: "fst ` S = S \<times> UNIV" 

94 
by auto 

95 

96 
lemma snd_vimage_eq_Times: "snd ` S = UNIV \<times> S" 

97 
by auto 

98 

99 
lemma open_vimage_fst: "open S \<Longrightarrow> open (fst ` S)" 

100 
by (simp add: fst_vimage_eq_Times open_Times) 

101 

102 
lemma open_vimage_snd: "open S \<Longrightarrow> open (snd ` S)" 

103 
by (simp add: snd_vimage_eq_Times open_Times) 

104 

31568  105 
lemma closed_vimage_fst: "closed S \<Longrightarrow> closed (fst ` S)" 
106 
unfolding closed_open vimage_Compl [symmetric] 

107 
by (rule open_vimage_fst) 

108 

109 
lemma closed_vimage_snd: "closed S \<Longrightarrow> closed (snd ` S)" 

110 
unfolding closed_open vimage_Compl [symmetric] 

111 
by (rule open_vimage_snd) 

112 

113 
lemma closed_Times: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)" 

114 
proof  

115 
have "S \<times> T = (fst ` S) \<inter> (snd ` T)" by auto 

116 
thus "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<times> T)" 

117 
by (simp add: closed_vimage_fst closed_vimage_snd closed_Int) 

118 
qed 

119 

34110  120 
lemma openI: (* TODO: move *) 
121 
assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S" 

122 
shows "open S" 

123 
proof  

124 
have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto 

125 
moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms) 

126 
ultimately show "open S" by simp 

127 
qed 

128 

129 
lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S" 

130 
unfolding image_def subset_eq by force 

131 

132 
lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S" 

133 
unfolding image_def subset_eq by force 

134 

135 
lemma open_image_fst: assumes "open S" shows "open (fst ` S)" 

136 
proof (rule openI) 

137 
fix x assume "x \<in> fst ` S" 

138 
then obtain y where "(x, y) \<in> S" by auto 

139 
then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S" 

140 
using `open S` unfolding open_prod_def by auto 

141 
from `A \<times> B \<subseteq> S` `y \<in> B` have "A \<subseteq> fst ` S" by (rule subset_fst_imageI) 

142 
with `open A` `x \<in> A` have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp 

143 
then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by  (rule exI) 

144 
qed 

145 

146 
lemma open_image_snd: assumes "open S" shows "open (snd ` S)" 

147 
proof (rule openI) 

148 
fix y assume "y \<in> snd ` S" 

149 
then obtain x where "(x, y) \<in> S" by auto 

150 
then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S" 

151 
using `open S` unfolding open_prod_def by auto 

152 
from `A \<times> B \<subseteq> S` `x \<in> A` have "B \<subseteq> snd ` S" by (rule subset_snd_imageI) 

153 
with `open B` `y \<in> B` have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp 

154 
then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by  (rule exI) 

155 
qed 

31568  156 

31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

157 
subsection {* Product is a metric space *} 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

158 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset

159 
instantiation prod :: (metric_space, metric_space) metric_space 
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

160 
begin 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

161 

b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

162 
definition dist_prod_def: 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

163 
"dist (x::'a \<times> 'b) y = sqrt ((dist (fst x) (fst y))\<twosuperior> + (dist (snd x) (snd y))\<twosuperior>)" 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

164 

b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

165 
lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<twosuperior> + (dist b d)\<twosuperior>)" 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

166 
unfolding dist_prod_def by simp 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

167 

36332  168 
lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y" 
169 
unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1) 

170 

171 
lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y" 

172 
unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2) 

173 

31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

174 
instance proof 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

175 
fix x y :: "'a \<times> 'b" 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

176 
show "dist x y = 0 \<longleftrightarrow> x = y" 
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset

177 
unfolding dist_prod_def prod_eq_iff by simp 
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

178 
next 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

179 
fix x y z :: "'a \<times> 'b" 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

180 
show "dist x y \<le> dist x z + dist y z" 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

181 
unfolding dist_prod_def 
31563  182 
by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq] 
183 
real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist) 

31415  184 
next 
185 
(* FIXME: long proof! *) 

186 
(* Maybe it would be easier to define topological spaces *) 

187 
(* in terms of neighborhoods instead of open sets? *) 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

188 
fix S :: "('a \<times> 'b) set" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

189 
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
31563  190 
proof 
36332  191 
assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" 
192 
proof 

193 
fix x assume "x \<in> S" 

194 
obtain A B where "open A" "open B" "x \<in> A \<times> B" "A \<times> B \<subseteq> S" 

195 
using `open S` and `x \<in> S` by (rule open_prod_elim) 

196 
obtain r where r: "0 < r" "\<forall>y. dist y (fst x) < r \<longrightarrow> y \<in> A" 

197 
using `open A` and `x \<in> A \<times> B` unfolding open_dist by auto 

198 
obtain s where s: "0 < s" "\<forall>y. dist y (snd x) < s \<longrightarrow> y \<in> B" 

199 
using `open B` and `x \<in> A \<times> B` unfolding open_dist by auto 

200 
let ?e = "min r s" 

201 
have "0 < ?e \<and> (\<forall>y. dist y x < ?e \<longrightarrow> y \<in> S)" 

202 
proof (intro allI impI conjI) 

203 
show "0 < min r s" by (simp add: r(1) s(1)) 

204 
next 

205 
fix y assume "dist y x < min r s" 

206 
hence "dist y x < r" and "dist y x < s" 

207 
by simp_all 

208 
hence "dist (fst y) (fst x) < r" and "dist (snd y) (snd x) < s" 

209 
by (auto intro: le_less_trans dist_fst_le dist_snd_le) 

210 
hence "fst y \<in> A" and "snd y \<in> B" 

211 
by (simp_all add: r(2) s(2)) 

212 
hence "y \<in> A \<times> B" by (induct y, simp) 

213 
with `A \<times> B \<subseteq> S` show "y \<in> S" .. 

214 
qed 

215 
thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" .. 

216 
qed 

31563  217 
next 
218 
assume "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" thus "open S" 

219 
unfolding open_prod_def open_dist 

220 
apply safe 

31415  221 
apply (drule (1) bspec) 
222 
apply clarify 

223 
apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)") 

224 
apply clarify 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

225 
apply (rule_tac x="{y. dist y a < r}" in exI) 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

226 
apply (rule_tac x="{y. dist y b < s}" in exI) 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

227 
apply (rule conjI) 
31415  228 
apply clarify 
229 
apply (rule_tac x="r  dist x a" in exI, rule conjI, simp) 

230 
apply clarify 

31563  231 
apply (simp add: less_diff_eq) 
232 
apply (erule le_less_trans [OF dist_triangle]) 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

233 
apply (rule conjI) 
31415  234 
apply clarify 
235 
apply (rule_tac x="s  dist x b" in exI, rule conjI, simp) 

236 
apply clarify 

31563  237 
apply (simp add: less_diff_eq) 
238 
apply (erule le_less_trans [OF dist_triangle]) 

31415  239 
apply (rule conjI) 
240 
apply simp 

241 
apply (clarify, rename_tac c d) 

242 
apply (drule spec, erule mp) 

243 
apply (simp add: dist_Pair_Pair add_strict_mono power_strict_mono) 

244 
apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos) 

245 
apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos) 

246 
apply (simp add: power_divide) 

247 
done 

31563  248 
qed 
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

249 
qed 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

250 

b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

251 
end 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

252 

31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

253 
subsection {* Continuity of operations *} 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

254 

31565  255 
lemma tendsto_fst [tendsto_intros]: 
31491  256 
assumes "(f > a) net" 
257 
shows "((\<lambda>x. fst (f x)) > fst a) net" 

258 
proof (rule topological_tendstoI) 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

259 
fix S assume "open S" "fst a \<in> S" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

260 
then have "open (fst ` S)" "a \<in> fst ` S" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

261 
unfolding open_prod_def 
31491  262 
apply simp_all 
263 
apply clarify 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

264 
apply (rule exI, erule conjI) 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

265 
apply (rule exI, rule conjI [OF open_UNIV]) 
31491  266 
apply auto 
267 
done 

268 
with assms have "eventually (\<lambda>x. f x \<in> fst ` S) net" 

269 
by (rule topological_tendstoD) 

270 
then show "eventually (\<lambda>x. fst (f x) \<in> S) net" 

271 
by simp 

31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

272 
qed 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

273 

31565  274 
lemma tendsto_snd [tendsto_intros]: 
31491  275 
assumes "(f > a) net" 
276 
shows "((\<lambda>x. snd (f x)) > snd a) net" 

277 
proof (rule topological_tendstoI) 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

278 
fix S assume "open S" "snd a \<in> S" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

279 
then have "open (snd ` S)" "a \<in> snd ` S" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

280 
unfolding open_prod_def 
31491  281 
apply simp_all 
282 
apply clarify 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

283 
apply (rule exI, rule conjI [OF open_UNIV]) 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

284 
apply (rule exI, erule conjI) 
31491  285 
apply auto 
286 
done 

287 
with assms have "eventually (\<lambda>x. f x \<in> snd ` S) net" 

288 
by (rule topological_tendstoD) 

289 
then show "eventually (\<lambda>x. snd (f x) \<in> S) net" 

290 
by simp 

31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

291 
qed 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

292 

31565  293 
lemma tendsto_Pair [tendsto_intros]: 
31491  294 
assumes "(f > a) net" and "(g > b) net" 
295 
shows "((\<lambda>x. (f x, g x)) > (a, b)) net" 

296 
proof (rule topological_tendstoI) 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

297 
fix S assume "open S" "(a, b) \<in> S" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

298 
then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

299 
unfolding open_prod_def by auto 
31491  300 
have "eventually (\<lambda>x. f x \<in> A) net" 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

301 
using `(f > a) net` `open A` `a \<in> A` 
31491  302 
by (rule topological_tendstoD) 
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

303 
moreover 
31491  304 
have "eventually (\<lambda>x. g x \<in> B) net" 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

305 
using `(g > b) net` `open B` `b \<in> B` 
31491  306 
by (rule topological_tendstoD) 
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

307 
ultimately 
31491  308 
show "eventually (\<lambda>x. (f x, g x) \<in> S) net" 
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

309 
by (rule eventually_elim2) 
31491  310 
(simp add: subsetD [OF `A \<times> B \<subseteq> S`]) 
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

311 
qed 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

312 

1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

313 
lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

314 
unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le]) 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

315 

1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

316 
lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n))" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

317 
unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le]) 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

318 

1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

319 
lemma Cauchy_Pair: 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

320 
assumes "Cauchy X" and "Cauchy Y" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

321 
shows "Cauchy (\<lambda>n. (X n, Y n))" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

322 
proof (rule metric_CauchyI) 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

323 
fix r :: real assume "0 < r" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

324 
then have "0 < r / sqrt 2" (is "0 < ?s") 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

325 
by (simp add: divide_pos_pos) 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

326 
obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < ?s" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

327 
using metric_CauchyD [OF `Cauchy X` `0 < ?s`] .. 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

328 
obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (Y m) (Y n) < ?s" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

329 
using metric_CauchyD [OF `Cauchy Y` `0 < ?s`] .. 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

330 
have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. dist (X m, Y m) (X n, Y n) < r" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

331 
using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair) 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

332 
then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" .. 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

333 
qed 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

334 

1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

335 
lemma isCont_Pair [simp]: 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

336 
"\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x" 
36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
36660
diff
changeset

337 
unfolding isCont_def by (rule tendsto_Pair) 
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

338 

1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

339 
subsection {* Product is a complete metric space *} 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

340 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset

341 
instance prod :: (complete_space, complete_space) complete_space 
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

342 
proof 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

343 
fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

344 
have 1: "(\<lambda>n. fst (X n)) > lim (\<lambda>n. fst (X n))" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

345 
using Cauchy_fst [OF `Cauchy X`] 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

346 
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

347 
have 2: "(\<lambda>n. snd (X n)) > lim (\<lambda>n. snd (X n))" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

348 
using Cauchy_snd [OF `Cauchy X`] 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

349 
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

350 
have "X > (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))" 
36660
1cc4ab4b7ff7
make (X > L) an abbreviation for (X > L) sequentially
huffman
parents:
36332
diff
changeset

351 
using tendsto_Pair [OF 1 2] by simp 
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

352 
then show "convergent X" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

353 
by (rule convergentI) 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

354 
qed 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

355 

30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

356 
subsection {* Product is a normed vector space *} 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

357 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset

358 
instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

359 
begin 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

360 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

361 
definition norm_prod_def: 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

362 
"norm x = sqrt ((norm (fst x))\<twosuperior> + (norm (snd x))\<twosuperior>)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

363 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

364 
definition sgn_prod_def: 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

365 
"sgn (x::'a \<times> 'b) = scaleR (inverse (norm x)) x" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

366 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

367 
lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<twosuperior> + (norm b)\<twosuperior>)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

368 
unfolding norm_prod_def by simp 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

369 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

370 
instance proof 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

371 
fix r :: real and x y :: "'a \<times> 'b" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

372 
show "0 \<le> norm x" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

373 
unfolding norm_prod_def by simp 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

374 
show "norm x = 0 \<longleftrightarrow> x = 0" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

375 
unfolding norm_prod_def 
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset

376 
by (simp add: prod_eq_iff) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

377 
show "norm (x + y) \<le> norm x + norm y" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

378 
unfolding norm_prod_def 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

379 
apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

380 
apply (simp add: add_mono power_mono norm_triangle_ineq) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

381 
done 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

382 
show "norm (scaleR r x) = \<bar>r\<bar> * norm x" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

383 
unfolding norm_prod_def 
31587  384 
apply (simp add: power_mult_distrib) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

385 
apply (simp add: right_distrib [symmetric]) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

386 
apply (simp add: real_sqrt_mult_distrib) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

387 
done 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

388 
show "sgn x = scaleR (inverse (norm x)) x" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

389 
by (rule sgn_prod_def) 
31290  390 
show "dist x y = norm (x  y)" 
31339
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

391 
unfolding dist_prod_def norm_prod_def 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

392 
by (simp add: dist_norm) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

393 
qed 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

394 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

395 
end 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

396 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset

397 
instance prod :: (banach, banach) banach .. 
31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

398 

30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

399 
subsection {* Product is an inner product space *} 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

400 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36661
diff
changeset

401 
instantiation prod :: (real_inner, real_inner) real_inner 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

402 
begin 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

403 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

404 
definition inner_prod_def: 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

405 
"inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

406 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

407 
lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

408 
unfolding inner_prod_def by simp 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

409 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

410 
instance proof 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

411 
fix r :: real 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

412 
fix x y z :: "'a::real_inner * 'b::real_inner" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

413 
show "inner x y = inner y x" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

414 
unfolding inner_prod_def 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

415 
by (simp add: inner_commute) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

416 
show "inner (x + y) z = inner x z + inner y z" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

417 
unfolding inner_prod_def 
31590
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31587
diff
changeset

418 
by (simp add: inner_add_left) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

419 
show "inner (scaleR r x) y = r * inner x y" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

420 
unfolding inner_prod_def 
31590
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31587
diff
changeset

421 
by (simp add: right_distrib) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

422 
show "0 \<le> inner x x" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

423 
unfolding inner_prod_def 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

424 
by (intro add_nonneg_nonneg inner_ge_zero) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

425 
show "inner x x = 0 \<longleftrightarrow> x = 0" 
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
37678
diff
changeset

426 
unfolding inner_prod_def prod_eq_iff 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

427 
by (simp add: add_nonneg_eq_0_iff) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

428 
show "norm x = sqrt (inner x x)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

429 
unfolding norm_prod_def inner_prod_def 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

430 
by (simp add: power2_norm_eq_inner) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

431 
qed 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

432 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

433 
end 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

434 

31405
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

435 
subsection {* Pair operations are linear *} 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

436 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30019
diff
changeset

437 
interpretation fst: bounded_linear fst 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

438 
apply (unfold_locales) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

439 
apply (rule fst_add) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

440 
apply (rule fst_scaleR) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

441 
apply (rule_tac x="1" in exI, simp add: norm_Pair) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

442 
done 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

443 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30019
diff
changeset

444 
interpretation snd: bounded_linear snd 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

445 
apply (unfold_locales) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

446 
apply (rule snd_add) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

447 
apply (rule snd_scaleR) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

448 
apply (rule_tac x="1" in exI, simp add: norm_Pair) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

449 
done 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

450 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

451 
text {* TODO: move to NthRoot *} 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

452 
lemma sqrt_add_le_add_sqrt: 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

453 
assumes x: "0 \<le> x" and y: "0 \<le> y" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

454 
shows "sqrt (x + y) \<le> sqrt x + sqrt y" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

455 
apply (rule power2_le_imp_le) 
44126  456 
apply (simp add: real_sum_squared_expand x y) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

457 
apply (simp add: mult_nonneg_nonneg x y) 
44126  458 
apply (simp add: x y) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

459 
done 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

460 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

461 
lemma bounded_linear_Pair: 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

462 
assumes f: "bounded_linear f" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

463 
assumes g: "bounded_linear g" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

464 
shows "bounded_linear (\<lambda>x. (f x, g x))" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

465 
proof 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

466 
interpret f: bounded_linear f by fact 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

467 
interpret g: bounded_linear g by fact 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

468 
fix x y and r :: real 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

469 
show "(f (x + y), g (x + y)) = (f x, g x) + (f y, g y)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

470 
by (simp add: f.add g.add) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

471 
show "(f (r *\<^sub>R x), g (r *\<^sub>R x)) = r *\<^sub>R (f x, g x)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

472 
by (simp add: f.scaleR g.scaleR) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

473 
obtain Kf where "0 < Kf" and norm_f: "\<And>x. norm (f x) \<le> norm x * Kf" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

474 
using f.pos_bounded by fast 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

475 
obtain Kg where "0 < Kg" and norm_g: "\<And>x. norm (g x) \<le> norm x * Kg" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

476 
using g.pos_bounded by fast 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

477 
have "\<forall>x. norm (f x, g x) \<le> norm x * (Kf + Kg)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

478 
apply (rule allI) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

479 
apply (simp add: norm_Pair) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

480 
apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

481 
apply (simp add: right_distrib) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

482 
apply (rule add_mono [OF norm_f norm_g]) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

483 
done 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

484 
then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" .. 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

485 
qed 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

486 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

487 
subsection {* Frechet derivatives involving pairs *} 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

488 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

489 
lemma FDERIV_Pair: 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

490 
assumes f: "FDERIV f x :> f'" and g: "FDERIV g x :> g'" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

491 
shows "FDERIV (\<lambda>x. (f x, g x)) x :> (\<lambda>h. (f' h, g' h))" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

492 
apply (rule FDERIV_I) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

493 
apply (rule bounded_linear_Pair) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

494 
apply (rule FDERIV_bounded_linear [OF f]) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

495 
apply (rule FDERIV_bounded_linear [OF g]) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

496 
apply (simp add: norm_Pair) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

497 
apply (rule real_LIM_sandwich_zero) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

498 
apply (rule LIM_add_zero) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

499 
apply (rule FDERIV_D [OF f]) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

500 
apply (rule FDERIV_D [OF g]) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

501 
apply (rename_tac h) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

502 
apply (simp add: divide_nonneg_pos) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

503 
apply (rename_tac h) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

504 
apply (subst add_divide_distrib [symmetric]) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

505 
apply (rule divide_right_mono [OF _ norm_ge_zero]) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

506 
apply (rule order_trans [OF sqrt_add_le_add_sqrt]) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

507 
apply simp 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

508 
apply simp 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

509 
apply simp 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

510 
done 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

511 

a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

512 
end 