author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 44749  5b1e1432c320 
child 51002  496013a6eb38 
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 

44575  157 
subsubsection {* Continuity of operations *} 
158 

159 
lemma tendsto_fst [tendsto_intros]: 

160 
assumes "(f > a) F" 

161 
shows "((\<lambda>x. fst (f x)) > fst a) F" 

162 
proof (rule topological_tendstoI) 

163 
fix S assume "open S" and "fst a \<in> S" 

164 
then have "open (fst ` S)" and "a \<in> fst ` S" 

165 
by (simp_all add: open_vimage_fst) 

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

167 
by (rule topological_tendstoD) 

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

169 
by simp 

170 
qed 

171 

172 
lemma tendsto_snd [tendsto_intros]: 

173 
assumes "(f > a) F" 

174 
shows "((\<lambda>x. snd (f x)) > snd a) F" 

175 
proof (rule topological_tendstoI) 

176 
fix S assume "open S" and "snd a \<in> S" 

177 
then have "open (snd ` S)" and "a \<in> snd ` S" 

178 
by (simp_all add: open_vimage_snd) 

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

180 
by (rule topological_tendstoD) 

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

182 
by simp 

183 
qed 

184 

185 
lemma tendsto_Pair [tendsto_intros]: 

186 
assumes "(f > a) F" and "(g > b) F" 

187 
shows "((\<lambda>x. (f x, g x)) > (a, b)) F" 

188 
proof (rule topological_tendstoI) 

189 
fix S assume "open S" and "(a, b) \<in> S" 

190 
then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S" 

191 
unfolding open_prod_def by fast 

192 
have "eventually (\<lambda>x. f x \<in> A) F" 

193 
using `(f > a) F` `open A` `a \<in> A` 

194 
by (rule topological_tendstoD) 

195 
moreover 

196 
have "eventually (\<lambda>x. g x \<in> B) F" 

197 
using `(g > b) F` `open B` `b \<in> B` 

198 
by (rule topological_tendstoD) 

199 
ultimately 

200 
show "eventually (\<lambda>x. (f x, g x) \<in> S) F" 

201 
by (rule eventually_elim2) 

202 
(simp add: subsetD [OF `A \<times> B \<subseteq> S`]) 

203 
qed 

204 

205 
lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a" 

206 
unfolding isCont_def by (rule tendsto_fst) 

207 

208 
lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a" 

209 
unfolding isCont_def by (rule tendsto_snd) 

210 

211 
lemma isCont_Pair [simp]: 

212 
"\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a" 

213 
unfolding isCont_def by (rule tendsto_Pair) 

214 

215 
subsubsection {* Separation axioms *} 

44214
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

216 

1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

217 
lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B" 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

218 
by (induct x) simp (* TODO: move elsewhere *) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

219 

1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

220 
instance prod :: (t0_space, t0_space) t0_space 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

221 
proof 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

222 
fix x y :: "'a \<times> 'b" assume "x \<noteq> y" 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

223 
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y" 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

224 
by (simp add: prod_eq_iff) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

225 
thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)" 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

226 
apply (rule disjE) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

227 
apply (drule t0_space, erule exE, rule_tac x="U \<times> UNIV" in exI) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

228 
apply (simp add: open_Times mem_Times_iff) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

229 
apply (drule t0_space, erule exE, rule_tac x="UNIV \<times> U" in exI) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

230 
apply (simp add: open_Times mem_Times_iff) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

231 
done 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

232 
qed 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

233 

1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

234 
instance prod :: (t1_space, t1_space) t1_space 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

235 
proof 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

236 
fix x y :: "'a \<times> 'b" assume "x \<noteq> y" 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

237 
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y" 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

238 
by (simp add: prod_eq_iff) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

239 
thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U" 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

240 
apply (rule disjE) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

241 
apply (drule t1_space, erule exE, rule_tac x="U \<times> UNIV" in exI) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

242 
apply (simp add: open_Times mem_Times_iff) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

243 
apply (drule t1_space, erule exE, rule_tac x="UNIV \<times> U" in exI) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

244 
apply (simp add: open_Times mem_Times_iff) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

245 
done 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

246 
qed 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

247 

1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

248 
instance prod :: (t2_space, t2_space) t2_space 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

249 
proof 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

250 
fix x y :: "'a \<times> 'b" assume "x \<noteq> y" 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

251 
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y" 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

252 
by (simp add: prod_eq_iff) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

253 
thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

254 
apply (rule disjE) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

255 
apply (drule hausdorff, clarify) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

256 
apply (rule_tac x="U \<times> UNIV" in exI, rule_tac x="V \<times> UNIV" in exI) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

257 
apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

258 
apply (drule hausdorff, clarify) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

259 
apply (rule_tac x="UNIV \<times> U" in exI, rule_tac x="UNIV \<times> V" in exI) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

260 
apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal) 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

261 
done 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

262 
qed 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

263 

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

264 
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

265 

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

266 
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

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

268 

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

269 
definition dist_prod_def: 
44214
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

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

271 

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

272 
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

273 
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

274 

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

277 

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

279 
unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2) 

280 

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

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

282 
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

283 
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

284 
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

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

286 
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

287 
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

288 
unfolding dist_prod_def 
31563  289 
by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq] 
290 
real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist) 

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

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

293 
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
31563  294 
proof 
36332  295 
assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" 
296 
proof 

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

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

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

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

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

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

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

304 
let ?e = "min r s" 

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

306 
proof (intro allI impI conjI) 

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

308 
next 

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

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

311 
by simp_all 

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

313 
by (auto intro: le_less_trans dist_fst_le dist_snd_le) 

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

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

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

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

318 
qed 

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

320 
qed 

31563  321 
next 
44575  322 
assume *: "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" show "open S" 
323 
proof (rule open_prod_intro) 

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

325 
then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S" 

326 
using * by fast 

327 
def r \<equiv> "e / sqrt 2" and s \<equiv> "e / sqrt 2" 

328 
from `0 < e` have "0 < r" and "0 < s" 

329 
unfolding r_def s_def by (simp_all add: divide_pos_pos) 

330 
from `0 < e` have "e = sqrt (r\<twosuperior> + s\<twosuperior>)" 

331 
unfolding r_def s_def by (simp add: power_divide) 

332 
def A \<equiv> "{y. dist (fst x) y < r}" and B \<equiv> "{y. dist (snd x) y < s}" 

333 
have "open A" and "open B" 

334 
unfolding A_def B_def by (simp_all add: open_ball) 

335 
moreover have "x \<in> A \<times> B" 

336 
unfolding A_def B_def mem_Times_iff 

337 
using `0 < r` and `0 < s` by simp 

338 
moreover have "A \<times> B \<subseteq> S" 

339 
proof (clarify) 

340 
fix a b assume "a \<in> A" and "b \<in> B" 

341 
hence "dist a (fst x) < r" and "dist b (snd x) < s" 

342 
unfolding A_def B_def by (simp_all add: dist_commute) 

343 
hence "dist (a, b) x < e" 

344 
unfolding dist_prod_def `e = sqrt (r\<twosuperior> + s\<twosuperior>)` 

345 
by (simp add: add_strict_mono power_strict_mono) 

346 
thus "(a, b) \<in> S" 

347 
by (simp add: S) 

348 
qed 

349 
ultimately show "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" by fast 

350 
qed 

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

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

353 

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

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

355 

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

356 
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

357 
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

358 

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

359 
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

360 
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

361 

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

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

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

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

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

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

367 
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

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

369 
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

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

371 
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

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

373 
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

374 
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

375 
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

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

377 

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

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

379 

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

380 
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

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

382 
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

383 
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

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

385 
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

386 
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

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

388 
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

389 
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

390 
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

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

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

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

394 

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

395 
subsection {* Product is a normed vector space *} 
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 
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

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

399 

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

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

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

402 

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

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

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

405 

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

406 
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

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

408 

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

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

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

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

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

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

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

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

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

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

418 
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

419 
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

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

421 
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

422 
unfolding norm_prod_def 
31587  423 
apply (simp add: power_mult_distrib) 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44749
diff
changeset

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

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

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

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

428 
by (rule sgn_prod_def) 
31290  429 
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

430 
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

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

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

433 

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

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

435 

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

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

437 

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

439 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

440 
lemma bounded_linear_fst: "bounded_linear fst" 
44127  441 
using fst_add fst_scaleR 
442 
by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) 

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

443 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

444 
lemma bounded_linear_snd: "bounded_linear snd" 
44127  445 
using snd_add snd_scaleR 
446 
by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) 

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

447 

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

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

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

450 
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

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

452 
apply (rule power2_le_imp_le) 
44749
5b1e1432c320
remove redundant lemma real_sum_squared_expand in favor of power2_sum
huffman
parents:
44575
diff
changeset

453 
apply (simp add: power2_sum x y) 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

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

457 

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

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

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

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

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

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

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

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

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

466 
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

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

468 
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

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

470 
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

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

472 
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

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

474 
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

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

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

477 
apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp) 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44749
diff
changeset

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

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

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

481 
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

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

483 

44575  484 
subsubsection {* Frechet derivatives involving pairs *} 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

485 

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

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

487 
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

488 
shows "FDERIV (\<lambda>x. (f x, g x)) x :> (\<lambda>h. (f' h, g' h))" 
44575  489 
proof (rule FDERIV_I) 
490 
show "bounded_linear (\<lambda>h. (f' h, g' h))" 

491 
using f g by (intro bounded_linear_Pair FDERIV_bounded_linear) 

492 
let ?Rf = "\<lambda>h. f (x + h)  f x  f' h" 

493 
let ?Rg = "\<lambda>h. g (x + h)  g x  g' h" 

494 
let ?R = "\<lambda>h. ((f (x + h), g (x + h))  (f x, g x)  (f' h, g' h))" 

495 
show "(\<lambda>h. norm (?R h) / norm h)  0 > 0" 

496 
proof (rule real_LIM_sandwich_zero) 

497 
show "(\<lambda>h. norm (?Rf h) / norm h + norm (?Rg h) / norm h)  0 > 0" 

498 
using f g by (intro tendsto_add_zero FDERIV_D) 

499 
fix h :: 'a assume "h \<noteq> 0" 

500 
thus "0 \<le> norm (?R h) / norm h" 

501 
by (simp add: divide_nonneg_pos) 

502 
show "norm (?R h) / norm h \<le> norm (?Rf h) / norm h + norm (?Rg h) / norm h" 

503 
unfolding add_divide_distrib [symmetric] 

504 
by (simp add: norm_Pair divide_right_mono 

505 
order_trans [OF sqrt_add_le_add_sqrt]) 

506 
qed 

507 
qed 

508 

509 
subsection {* Product is an inner product space *} 

510 

511 
instantiation prod :: (real_inner, real_inner) real_inner 

512 
begin 

513 

514 
definition inner_prod_def: 

515 
"inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)" 

516 

517 
lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d" 

518 
unfolding inner_prod_def by simp 

519 

520 
instance proof 

521 
fix r :: real 

522 
fix x y z :: "'a::real_inner \<times> 'b::real_inner" 

523 
show "inner x y = inner y x" 

524 
unfolding inner_prod_def 

525 
by (simp add: inner_commute) 

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

527 
unfolding inner_prod_def 

528 
by (simp add: inner_add_left) 

529 
show "inner (scaleR r x) y = r * inner x y" 

530 
unfolding inner_prod_def 

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44749
diff
changeset

531 
by (simp add: distrib_left) 
44575  532 
show "0 \<le> inner x x" 
533 
unfolding inner_prod_def 

534 
by (intro add_nonneg_nonneg inner_ge_zero) 

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

536 
unfolding inner_prod_def prod_eq_iff 

537 
by (simp add: add_nonneg_eq_0_iff) 

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

539 
unfolding norm_prod_def inner_prod_def 

540 
by (simp add: power2_norm_eq_inner) 

541 
qed 

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

542 

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

543 
end 
44575  544 

545 
end 