author  huffman 
Thu, 11 Jun 2009 08:26:08 0700  
changeset 31562  10d0fb526643 
parent 31492  5400beeddb55 
child 31563  ded2364d14d4 
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 

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

13 
instantiation "*" :: (real_vector, real_vector) real_vector 
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" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

31 
by (simp add: expand_prod_eq scaleR_right_distrib) 
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" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

33 
by (simp add: expand_prod_eq scaleR_left_distrib) 
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" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

36 
show "scaleR 1 x = x" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

37 
by (simp add: expand_prod_eq) 
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 

44 
instantiation 

45 
"*" :: (topological_space, topological_space) topological_space 

46 
begin 

47 

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

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

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

50 
(\<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  51 

52 
instance proof 

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

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

54 
unfolding open_prod_def by auto 
31415  55 
next 
56 
fix S T :: "('a \<times> 'b) set" 

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

57 
assume "open S" "open T" thus "open (S \<inter> T)" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

58 
unfolding open_prod_def 
31415  59 
apply clarify 
60 
apply (drule (1) bspec)+ 

61 
apply (clarify, rename_tac Sa Ta Sb Tb) 

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

62 
apply (rule_tac x="Sa \<inter> Ta" in exI) 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

63 
apply (rule_tac x="Sb \<inter> Tb" in exI) 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

64 
apply (simp add: open_Int) 
31415  65 
apply fast 
66 
done 

67 
next 

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

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

69 
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

70 
unfolding open_prod_def by fast 
31415  71 
qed 
72 

73 
end 

74 

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

77 

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

79 
by auto 

80 

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

82 
by auto 

83 

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

85 
by (simp add: fst_vimage_eq_Times open_Times) 

86 

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

88 
by (simp add: snd_vimage_eq_Times open_Times) 

89 

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

90 
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

91 

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

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

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

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

95 

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

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

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

98 

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

99 
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

100 
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

101 

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

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

103 
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

104 
show "dist x y = 0 \<longleftrightarrow> x = y" 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

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

106 
by (simp add: expand_prod_eq) 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

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

108 
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

109 
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

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

111 
apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]) 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

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

113 
apply (rule order_trans [OF add_mono]) 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

114 
apply (rule power_mono [OF dist_triangle2 [of _ _ "fst z"] zero_le_dist]) 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

115 
apply (rule power_mono [OF dist_triangle2 [of _ _ "snd z"] zero_le_dist]) 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

116 
apply (simp only: real_sum_squared_expand) 
b4660351e8e7
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
huffman
parents:
31290
diff
changeset

117 
done 
31415  118 
next 
119 
(* FIXME: long proof! *) 

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

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

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

123 
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31491
diff
changeset

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

125 
apply safe 
31415  126 
apply (drule (1) bspec) 
127 
apply clarify 

128 
apply (drule (1) bspec)+ 

129 
apply (clarify, rename_tac r s) 

130 
apply (rule_tac x="min r s" in exI, simp) 

131 
apply (clarify, rename_tac c d) 

132 
apply (erule subsetD) 

133 
apply (simp add: dist_Pair_Pair) 

134 
apply (rule conjI) 

135 
apply (drule spec, erule mp) 

136 
apply (erule le_less_trans [OF real_sqrt_sum_squares_ge1]) 

137 
apply (drule spec, erule mp) 

138 
apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2]) 

139 

140 
apply (drule (1) bspec) 

141 
apply clarify 

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

143 
apply clarify 

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

144 
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

145 
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

146 
apply (rule conjI) 
31415  147 
apply clarify 
148 
apply (rule_tac x="r  dist x a" in exI, rule conjI, simp) 

149 
apply clarify 

150 
apply (rule le_less_trans [OF dist_triangle]) 

151 
apply (erule less_le_trans [OF add_strict_right_mono], simp) 

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

152 
apply (rule conjI) 
31415  153 
apply clarify 
154 
apply (rule_tac x="s  dist x b" in exI, rule conjI, simp) 

155 
apply clarify 

156 
apply (rule le_less_trans [OF dist_triangle]) 

157 
apply (erule less_le_trans [OF add_strict_right_mono], simp) 

158 
apply (rule conjI) 

159 
apply simp 

160 
apply (clarify, rename_tac c d) 

161 
apply (drule spec, erule mp) 

162 
apply (simp add: dist_Pair_Pair add_strict_mono power_strict_mono) 

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

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

165 
apply (simp add: power_divide) 

166 
done 

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

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

168 

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

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

170 

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

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

172 

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

173 
lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

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

175 

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

176 
lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

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

178 

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

179 
lemma tendsto_fst: 
31491  180 
assumes "(f > a) net" 
181 
shows "((\<lambda>x. fst (f x)) > fst a) net" 

182 
proof (rule topological_tendstoI) 

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

183 
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

184 
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

185 
unfolding open_prod_def 
31491  186 
apply simp_all 
187 
apply clarify 

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

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

189 
apply (rule exI, rule conjI [OF open_UNIV]) 
31491  190 
apply auto 
191 
done 

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

193 
by (rule topological_tendstoD) 

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

195 
by simp 

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

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

197 

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

198 
lemma tendsto_snd: 
31491  199 
assumes "(f > a) net" 
200 
shows "((\<lambda>x. snd (f x)) > snd a) net" 

201 
proof (rule topological_tendstoI) 

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

202 
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

203 
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

204 
unfolding open_prod_def 
31491  205 
apply simp_all 
206 
apply clarify 

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

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

208 
apply (rule exI, erule conjI) 
31491  209 
apply auto 
210 
done 

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

212 
by (rule topological_tendstoD) 

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

214 
by simp 

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

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

216 

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

217 
lemma tendsto_Pair: 
31491  218 
assumes "(f > a) net" and "(g > b) net" 
219 
shows "((\<lambda>x. (f x, g x)) > (a, b)) net" 

220 
proof (rule topological_tendstoI) 

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

221 
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

222 
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

223 
unfolding open_prod_def by auto 
31491  224 
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

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

227 
moreover 
31491  228 
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

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

231 
ultimately 
31491  232 
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

233 
by (rule eventually_elim2) 
31491  234 
(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

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

236 

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

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

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

239 

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

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

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

242 

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

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

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

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

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

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

248 

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

249 
lemma LIM_fst: "f  x > a \<Longrightarrow> (\<lambda>x. fst (f x))  x > fst a" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

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

251 

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

252 
lemma LIM_snd: "f  x > a \<Longrightarrow> (\<lambda>x. snd (f x))  x > snd a" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

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

254 

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

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

256 
assumes "f  x > a" and "g  x > b" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

257 
shows "(\<lambda>x. (f x, g x))  x > (a, b)" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

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

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

260 

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

261 
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

262 
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

263 

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

264 
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

265 
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

266 

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

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

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

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

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

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

272 
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

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

274 
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

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

276 
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

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

278 
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

279 
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

280 
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

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

282 

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

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

284 
"\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x" 
1f72869f1a2e
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
huffman
parents:
31388
diff
changeset

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

286 

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

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

288 

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

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

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

291 
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

292 
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

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

294 
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

295 
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

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

297 
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

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

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

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

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

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

303 

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

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

305 

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

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

307 
"*" :: (real_normed_vector, real_normed_vector) real_normed_vector 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

309 

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

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

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

312 

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

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

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

315 

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

316 
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

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

318 

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

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

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

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

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

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

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

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

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

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

328 
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

329 
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

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

331 
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

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

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

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

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

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

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

338 
by (rule sgn_prod_def) 
31290  339 
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

340 
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

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

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

343 

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

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

345 

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

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

347 

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

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

349 

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

350 
instantiation "*" :: (real_inner, real_inner) real_inner 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

352 

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

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

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

355 

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

356 
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

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

358 

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

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

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

361 
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

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

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

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

365 
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

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

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

368 
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

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

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

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

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

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

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

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

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

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

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

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

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

381 

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

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

383 

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

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

385 

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

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

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

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

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

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

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

392 

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

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

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

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

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

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

398 
done 
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 
text {* TODO: move to NthRoot *} 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

402 
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

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

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

405 
apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

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

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

409 

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

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

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

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

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

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

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

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

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

418 
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

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

420 
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

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

422 
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

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

424 
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

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

426 
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

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

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

429 
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

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

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

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

433 
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

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

435 

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

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

437 

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

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

439 
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

440 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

455 
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

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

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

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

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

460 

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

461 
end 