author  huffman 
Thu, 28 May 2009 17:09:51 0700  
changeset 31290  f41c023d90bc 
parent 30729  461ee3e49ad3 
child 31339  b4660351e8e7 
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 

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

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

43 

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

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

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

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

47 

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

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

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

50 

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

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

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

53 

31290  54 
definition dist_prod_def: 
55 
"dist (x::'a \<times> 'b) y = norm (x  y)" 

56 

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

57 
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

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

59 

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

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

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

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

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

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

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

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

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

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

69 
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

70 
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

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

72 
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

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

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

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

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

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

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

79 
by (rule sgn_prod_def) 
31290  80 
show "dist x y = norm (x  y)" 
81 
by (rule dist_prod_def) 

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

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

83 

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

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

85 

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

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

87 

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

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

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

90 

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

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

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

93 

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

94 
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

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

96 

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

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

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

99 
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

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

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

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

103 
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

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

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

106 
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

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

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

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

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

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

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

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

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

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

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

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

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

119 

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

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

121 

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

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

123 

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

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

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

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

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

128 
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

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

130 

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

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

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

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

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

135 
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

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

137 

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

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

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

140 
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

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

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

143 
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

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

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

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

147 

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

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

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

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

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

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

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

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

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

156 
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

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

158 
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

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

160 
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

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

162 
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

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

164 
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

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

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

167 
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

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

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

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

171 
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

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

173 

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

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

175 
TODO: The next three proofs are nearly identical to each other. 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

176 
Is there a good way to factor out the common parts? 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

178 

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

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

180 
assumes "X > a" and "Y > b" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

181 
shows "(\<lambda>n. (X n, Y n)) > (a, b)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

182 
proof (rule LIMSEQ_I) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

183 
fix r :: real assume "0 < r" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

184 
then have "0 < r / sqrt 2" (is "0 < ?s") 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

186 
obtain M where M: "\<forall>n\<ge>M. norm (X n  a) < ?s" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

187 
using LIMSEQ_D [OF `X > a` `0 < ?s`] .. 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

188 
obtain N where N: "\<forall>n\<ge>N. norm (Y n  b) < ?s" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

189 
using LIMSEQ_D [OF `Y > b` `0 < ?s`] .. 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

190 
have "\<forall>n\<ge>max M N. norm ((X n, Y n)  (a, b)) < r" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

191 
using M N by (simp add: real_sqrt_sum_squares_less norm_Pair) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

192 
then show "\<exists>n0. \<forall>n\<ge>n0. norm ((X n, Y n)  (a, b)) < r" .. 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

194 

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

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

196 
assumes "Cauchy X" and "Cauchy Y" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

197 
shows "Cauchy (\<lambda>n. (X n, Y n))" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

198 
proof (rule CauchyI) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

199 
fix r :: real assume "0 < r" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

200 
then have "0 < r / sqrt 2" (is "0 < ?s") 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

202 
obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m  X n) < ?s" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

203 
using CauchyD [OF `Cauchy X` `0 < ?s`] .. 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

204 
obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (Y m  Y n) < ?s" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

205 
using CauchyD [OF `Cauchy Y` `0 < ?s`] .. 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

206 
have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. norm ((X m, Y m)  (X n, Y n)) < r" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

207 
using M N by (simp add: real_sqrt_sum_squares_less norm_Pair) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

208 
then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. norm ((X m, Y m)  (X n, Y n)) < r" .. 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

210 

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

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

212 
assumes "f  x > a" and "g  x > b" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

214 
proof (rule LIM_I) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

215 
fix r :: real assume "0 < r" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

216 
then have "0 < r / sqrt 2" (is "0 < ?e") 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

218 
obtain s where s: "0 < s" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

219 
"\<forall>z. z \<noteq> x \<and> norm (z  x) < s \<longrightarrow> norm (f z  a) < ?e" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

220 
using LIM_D [OF `f  x > a` `0 < ?e`] by fast 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

221 
obtain t where t: "0 < t" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

222 
"\<forall>z. z \<noteq> x \<and> norm (z  x) < t \<longrightarrow> norm (g z  b) < ?e" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

223 
using LIM_D [OF `g  x > b` `0 < ?e`] by fast 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

224 
have "0 < min s t \<and> 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

225 
(\<forall>z. z \<noteq> x \<and> norm (z  x) < min s t \<longrightarrow> norm ((f z, g z)  (a, b)) < r)" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

226 
using s t by (simp add: real_sqrt_sum_squares_less norm_Pair) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

228 
"\<exists>s>0. \<forall>z. z \<noteq> x \<and> norm (z  x) < s \<longrightarrow> norm ((f z, g z)  (a, b)) < r" .. 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

230 

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

231 
lemma isCont_Pair [simp]: 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

232 
"\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

233 
unfolding isCont_def by (rule LIM_Pair) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

234 

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

235 

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

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

237 

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

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

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

240 
fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

241 
have 1: "(\<lambda>n. fst (X n)) > lim (\<lambda>n. fst (X n))" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

242 
using fst.Cauchy [OF `Cauchy X`] 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

244 
have 2: "(\<lambda>n. snd (X n)) > lim (\<lambda>n. snd (X n))" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

245 
using snd.Cauchy [OF `Cauchy X`] 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

247 
have "X > (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

248 
using LIMSEQ_Pair [OF 1 2] by simp 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

249 
then show "convergent X" 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

250 
by (rule convergentI) 
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
diff
changeset

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

252 

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

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

254 

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

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

256 
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

257 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

272 
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

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

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

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

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

277 

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

278 
end 