author  huffman 
Sun, 28 Aug 2011 09:20:12 0700  
changeset 44568  e6f291cb5810 
parent 44282  f0de18b62d63 
child 44575  c5e42b8590dd 
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 

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

157 
text {* Product preserves separation axioms. *} 
1e0414bda9af
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
huffman
parents:
44127
diff
changeset

158 

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

159 
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

160 
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

161 

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

162 
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

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

164 
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

165 
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

166 
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

167 
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

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

169 
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

170 
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

171 
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

172 
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

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

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

175 

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

176 
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

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

178 
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

179 
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

180 
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

181 
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

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

183 
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

184 
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

185 
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

186 
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

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

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

189 

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

190 
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

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

192 
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

193 
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

194 
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

195 
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

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

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

198 
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

199 
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

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

201 
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

202 
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

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

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

205 

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

206 
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

207 

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

208 
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

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

210 

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

211 
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

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

213 

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

214 
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

215 
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

216 

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

219 

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

221 
unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2) 

222 

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

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

224 
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

225 
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

226 
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

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

228 
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

229 
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

230 
unfolding dist_prod_def 
31563  231 
by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq] 
232 
real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist) 

31415  233 
next 
234 
(* FIXME: long proof! *) 

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

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

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

238 
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
31563  239 
proof 
36332  240 
assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" 
241 
proof 

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

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

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

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

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

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

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

249 
let ?e = "min r s" 

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

251 
proof (intro allI impI conjI) 

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

253 
next 

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

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

256 
by simp_all 

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

258 
by (auto intro: le_less_trans dist_fst_le dist_snd_le) 

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

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

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

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

263 
qed 

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

265 
qed 

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

268 
unfolding open_prod_def open_dist 

269 
apply safe 

31415  270 
apply (drule (1) bspec) 
271 
apply clarify 

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

273 
apply clarify 

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

274 
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

275 
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

276 
apply (rule conjI) 
31415  277 
apply clarify 
278 
apply (rule_tac x="r  dist x a" in exI, rule conjI, simp) 

279 
apply clarify 

31563  280 
apply (simp add: less_diff_eq) 
281 
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

282 
apply (rule conjI) 
31415  283 
apply clarify 
284 
apply (rule_tac x="s  dist x b" in exI, rule conjI, simp) 

285 
apply clarify 

31563  286 
apply (simp add: less_diff_eq) 
287 
apply (erule le_less_trans [OF dist_triangle]) 

31415  288 
apply (rule conjI) 
289 
apply simp 

290 
apply (clarify, rename_tac c d) 

291 
apply (drule spec, erule mp) 

292 
apply (simp add: dist_Pair_Pair add_strict_mono power_strict_mono) 

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

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

295 
apply (simp add: power_divide) 

296 
done 

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

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

299 

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

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

301 

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

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

303 

31565  304 
lemma tendsto_fst [tendsto_intros]: 
31491  305 
assumes "(f > a) net" 
306 
shows "((\<lambda>x. fst (f x)) > fst a) net" 

307 
proof (rule topological_tendstoI) 

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

308 
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

309 
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

310 
unfolding open_prod_def 
31491  311 
apply simp_all 
312 
apply clarify 

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

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

314 
apply (rule exI, rule conjI [OF open_UNIV]) 
31491  315 
apply auto 
316 
done 

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

318 
by (rule topological_tendstoD) 

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

320 
by simp 

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

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

322 

31565  323 
lemma tendsto_snd [tendsto_intros]: 
31491  324 
assumes "(f > a) net" 
325 
shows "((\<lambda>x. snd (f x)) > snd a) net" 

326 
proof (rule topological_tendstoI) 

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

327 
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

328 
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

329 
unfolding open_prod_def 
31491  330 
apply simp_all 
331 
apply clarify 

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

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

333 
apply (rule exI, erule conjI) 
31491  334 
apply auto 
335 
done 

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

337 
by (rule topological_tendstoD) 

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

339 
by simp 

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

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

341 

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

345 
proof (rule topological_tendstoI) 

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

346 
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

347 
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

348 
unfolding open_prod_def by auto 
31491  349 
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

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

352 
moreover 
31491  353 
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

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

356 
ultimately 
31491  357 
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

358 
by (rule eventually_elim2) 
31491  359 
(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

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

361 

44233  362 
lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a" 
363 
unfolding isCont_def by (rule tendsto_fst) 

364 

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

366 
unfolding isCont_def by (rule tendsto_snd) 

367 

368 
lemma isCont_Pair [simp]: 

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

370 
unfolding isCont_def by (rule tendsto_Pair) 

371 

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

372 
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

373 
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

374 

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

375 
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

376 
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

377 

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

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

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

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

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

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

383 
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

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

385 
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

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

387 
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

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

389 
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

390 
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

391 
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

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

393 

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

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

395 

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

396 
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

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

398 
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

399 
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

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

401 
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

402 
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

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

404 
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

405 
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

406 
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

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

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

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

410 

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

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

412 

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

413 
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

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

415 

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

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

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

418 

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

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

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

421 

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

422 
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

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

424 

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

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

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

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

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

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

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

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

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

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

434 
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

435 
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

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

437 
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

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

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

441 
apply (simp add: real_sqrt_mult_distrib) 
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 
show "sgn x = scaleR (inverse (norm x)) x" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

444 
by (rule sgn_prod_def) 
31290  445 
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

446 
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

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

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

449 

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

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

451 

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

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

453 

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

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

455 

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

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

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

458 

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

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

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

461 

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

462 
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

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

464 

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

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

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

467 
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

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

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

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

471 
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

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

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

474 
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

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

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

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

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

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

480 
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

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

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

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

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

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

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

487 

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

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

489 

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

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

491 

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

492 
lemma bounded_linear_fst: "bounded_linear fst" 
44127  493 
using fst_add fst_scaleR 
494 
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

495 

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

496 
lemma bounded_linear_snd: "bounded_linear snd" 
44127  497 
using snd_add snd_scaleR 
498 
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

499 

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

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

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

502 
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

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

504 
apply (rule power2_le_imp_le) 
44126  505 
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

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

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

509 

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

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

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

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

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

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

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

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

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

518 
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

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

520 
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

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

522 
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

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

524 
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

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

526 
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

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

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

529 
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

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

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

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

533 
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

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

535 

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

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

537 

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

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

539 
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

540 
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

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

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

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

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

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

546 
apply (rule real_LIM_sandwich_zero) 
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44282
diff
changeset

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

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

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

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

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

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

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

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

555 
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

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

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

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

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

560 

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

561 
end 