author  huffman 
Fri, 10 Nov 2006 00:46:00 +0100  
changeset 21282  dd647b4d7952 
parent 21257  b7f090c5057d 
child 21399  700ae58d2273 
permissions  rwrr 
10751  1 
(* Title : Lim.thy 
14477  2 
ID : $Id$ 
10751  3 
Author : Jacques D. Fleuriot 
4 
Copyright : 1998 University of Cambridge 

14477  5 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
10751  6 
*) 
7 

21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

8 
header{* Limits and Continuity *} 
10751  9 

15131  10 
theory Lim 
15360  11 
imports SEQ 
15131  12 
begin 
14477  13 

14 
text{*Standard and Nonstandard Definitions*} 

10751  15 

19765  16 
definition 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

17 
LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

18 
("((_)/  (_)/ > (_))" [60, 0, 60] 60) 
19765  19 
"f  a > L = 
20563  20 
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x  a) < s 
21 
> norm (f x  L) < r)" 

10751  22 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

23 
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

24 
("((_)/  (_)/ NS> (_))" [60, 0, 60] 60) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

25 
"f  a NS> L = 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

26 
(\<forall>x. (x \<noteq> star_of a & x @= star_of a > ( *f* f) x @= star_of L))" 
10751  27 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

28 
isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" 
19765  29 
"isCont f a = (f  a > (f a))" 
10751  30 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

31 
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" 
15228  32 
{*NS definition dispenses with limit notions*} 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

33 
"isNSCont f a = (\<forall>y. y @= star_of a > 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

34 
( *f* f) y @= star_of (f a))" 
10751  35 

20752  36 
isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" 
37 
"isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x  y) < s \<longrightarrow> norm (f x  f y) < r)" 

10751  38 

20752  39 
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" 
19765  40 
"isNSUCont f = (\<forall>x y. x @= y > ( *f* f) x @= ( *f* f) y)" 
10751  41 

42 

20755  43 
subsection {* Limits of Functions *} 
14477  44 

20755  45 
subsubsection {* Purely standard proofs *} 
14477  46 

47 
lemma LIM_eq: 

48 
"f  a > L = 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

49 
(\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r)" 
14477  50 
by (simp add: LIM_def diff_minus) 
51 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

52 
lemma LIM_I: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

53 
"(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

54 
==> f  a > L" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

55 
by (simp add: LIM_eq) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

56 

14477  57 
lemma LIM_D: 
58 
"[ f  a > L; 0<r ] 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

59 
==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r" 
14477  60 
by (simp add: LIM_eq) 
61 

21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

62 
lemma LIM_offset: "f  a > L \<Longrightarrow> (\<lambda>x. f (x + k))  a  k > L" 
20756  63 
apply (rule LIM_I) 
64 
apply (drule_tac r="r" in LIM_D, safe) 

65 
apply (rule_tac x="s" in exI, safe) 

66 
apply (drule_tac x="x + k" in spec) 

67 
apply (simp add: compare_rls) 

68 
done 

69 

21239  70 
lemma LIM_offset_zero: "f  a > L \<Longrightarrow> (\<lambda>h. f (a + h))  0 > L" 
71 
by (drule_tac k="a" in LIM_offset, simp add: add_commute) 

72 

73 
lemma LIM_offset_zero_cancel: "(\<lambda>h. f (a + h))  0 > L \<Longrightarrow> f  a > L" 

74 
by (drule_tac k=" a" in LIM_offset, simp) 

75 

15228  76 
lemma LIM_const [simp]: "(%x. k)  x > k" 
14477  77 
by (simp add: LIM_def) 
78 

79 
lemma LIM_add: 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

80 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
14477  81 
assumes f: "f  a > L" and g: "g  a > M" 
82 
shows "(%x. f x + g(x))  a > (L + M)" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

83 
proof (rule LIM_I) 
14477  84 
fix r :: real 
20409  85 
assume r: "0 < r" 
14477  86 
from LIM_D [OF f half_gt_zero [OF r]] 
87 
obtain fs 

88 
where fs: "0 < fs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

89 
and fs_lt: "\<forall>x. x \<noteq> a & norm (xa) < fs > norm (f x  L) < r/2" 
14477  90 
by blast 
91 
from LIM_D [OF g half_gt_zero [OF r]] 

92 
obtain gs 

93 
where gs: "0 < gs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

94 
and gs_lt: "\<forall>x. x \<noteq> a & norm (xa) < gs > norm (g x  M) < r/2" 
14477  95 
by blast 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

96 
show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (xa) < s \<longrightarrow> norm (f x + g x  (L + M)) < r" 
14477  97 
proof (intro exI conjI strip) 
98 
show "0 < min fs gs" by (simp add: fs gs) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

99 
fix x :: 'a 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

100 
assume "x \<noteq> a \<and> norm (xa) < min fs gs" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

101 
hence "x \<noteq> a \<and> norm (xa) < fs \<and> norm (xa) < gs" by simp 
14477  102 
with fs_lt gs_lt 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

103 
have "norm (f x  L) < r/2" and "norm (g x  M) < r/2" by blast+ 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

104 
hence "norm (f x  L) + norm (g x  M) < r" by arith 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

105 
thus "norm (f x + g x  (L + M)) < r" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

106 
by (blast intro: norm_diff_triangle_ineq order_le_less_trans) 
14477  107 
qed 
108 
qed 

109 

21257  110 
lemma LIM_add_zero: 
111 
"\<lbrakk>f  a > 0; g  a > 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x)  a > 0" 

112 
by (drule (1) LIM_add, simp) 

113 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

114 
lemma minus_diff_minus: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

115 
fixes a b :: "'a::ab_group_add" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

116 
shows "( a)  ( b) =  (a  b)" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

117 
by simp 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

118 

14477  119 
lemma LIM_minus: "f  a > L ==> (%x. f(x))  a > L" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

120 
by (simp only: LIM_eq minus_diff_minus norm_minus_cancel) 
14477  121 

122 
lemma LIM_add_minus: 

123 
"[ f  x > l; g  x > m ] ==> (%x. f(x) + g(x))  x > (l + m)" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

124 
by (intro LIM_add LIM_minus) 
14477  125 

126 
lemma LIM_diff: 

127 
"[ f  x > l; g  x > m ] ==> (%x. f(x)  g(x))  x > lm" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

128 
by (simp only: diff_minus LIM_add LIM_minus) 
14477  129 

21239  130 
lemma LIM_zero: "f  a > l \<Longrightarrow> (\<lambda>x. f x  l)  a > 0" 
131 
by (simp add: LIM_def) 

132 

133 
lemma LIM_zero_cancel: "(\<lambda>x. f x  l)  a > 0 \<Longrightarrow> f  a > l" 

134 
by (simp add: LIM_def) 

135 

21257  136 
lemma LIM_imp_LIM: 
137 
assumes f: "f  a > l" 

138 
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x  m) \<le> norm (f x  l)" 

139 
shows "g  a > m" 

140 
apply (rule LIM_I, drule LIM_D [OF f], safe) 

141 
apply (rule_tac x="s" in exI, safe) 

142 
apply (drule_tac x="x" in spec, safe) 

143 
apply (erule (1) order_le_less_trans [OF le]) 

144 
done 

145 

146 
lemma LIM_norm: "f  a > l \<Longrightarrow> (\<lambda>x. norm (f x))  a > norm l" 

147 
by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3) 

148 

149 
lemma LIM_norm_zero: "f  a > 0 \<Longrightarrow> (\<lambda>x. norm (f x))  a > 0" 

150 
by (drule LIM_norm, simp) 

151 

152 
lemma LIM_norm_zero_cancel: "(\<lambda>x. norm (f x))  a > 0 \<Longrightarrow> f  a > 0" 

153 
by (erule LIM_imp_LIM, simp) 

154 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

155 
lemma LIM_const_not_eq: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

156 
fixes a :: "'a::real_normed_div_algebra" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

157 
shows "k \<noteq> L ==> ~ ((%x. k)  a > L)" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

158 
apply (simp add: LIM_eq) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

159 
apply (rule_tac x="norm (k  L)" in exI, simp, safe) 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

160 
apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

161 
done 
14477  162 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

163 
lemma LIM_const_eq: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

164 
fixes a :: "'a::real_normed_div_algebra" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

165 
shows "(%x. k)  a > L ==> k = L" 
14477  166 
apply (rule ccontr) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

167 
apply (blast dest: LIM_const_not_eq) 
14477  168 
done 
169 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

170 
lemma LIM_unique: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

171 
fixes a :: "'a::real_normed_div_algebra" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

172 
shows "[ f  a > L; f  a > M ] ==> L = M" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

173 
apply (drule LIM_diff, assumption) 
14477  174 
apply (auto dest!: LIM_const_eq) 
175 
done 

176 

177 
lemma LIM_mult_zero: 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

178 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 
14477  179 
assumes f: "f  a > 0" and g: "g  a > 0" 
180 
shows "(%x. f(x) * g(x))  a > 0" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

181 
proof (rule LIM_I, simp) 
14477  182 
fix r :: real 
183 
assume r: "0<r" 

184 
from LIM_D [OF f zero_less_one] 

185 
obtain fs 

186 
where fs: "0 < fs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

187 
and fs_lt: "\<forall>x. x \<noteq> a & norm (xa) < fs > norm (f x) < 1" 
14477  188 
by auto 
189 
from LIM_D [OF g r] 

190 
obtain gs 

191 
where gs: "0 < gs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

192 
and gs_lt: "\<forall>x. x \<noteq> a & norm (xa) < gs > norm (g x) < r" 
14477  193 
by auto 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

194 
show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> norm (xa) < s \<longrightarrow> norm (f x * g x) < r)" 
14477  195 
proof (intro exI conjI strip) 
196 
show "0 < min fs gs" by (simp add: fs gs) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

197 
fix x :: 'a 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

198 
assume "x \<noteq> a \<and> norm (xa) < min fs gs" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

199 
hence "x \<noteq> a \<and> norm (xa) < fs \<and> norm (xa) < gs" by simp 
14477  200 
with fs_lt gs_lt 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

201 
have "norm (f x) < 1" and "norm (g x) < r" by blast+ 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

202 
hence "norm (f x) * norm (g x) < 1*r" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

203 
by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero]) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

204 
thus "norm (f x * g x) < r" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

205 
by (simp add: order_le_less_trans [OF norm_mult_ineq]) 
14477  206 
qed 
207 
qed 

208 

209 
lemma LIM_self: "(%x. x)  a > a" 

210 
by (auto simp add: LIM_def) 

211 

212 
text{*Limits are equal for functions equal except at limit point*} 

213 
lemma LIM_equal: 

214 
"[ \<forall>x. x \<noteq> a > (f x = g x) ] ==> (f  a > l) = (g  a > l)" 

215 
by (simp add: LIM_def) 

216 

20796  217 
lemma LIM_cong: 
218 
"\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk> 

219 
\<Longrightarrow> (f  a > l) = (g  b > m)" 

220 
by (simp add: LIM_def) 

221 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

222 
lemma LIM_equal2: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

223 
assumes 1: "0 < R" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

224 
assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < R\<rbrakk> \<Longrightarrow> f x = g x" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

225 
shows "g  a > l \<Longrightarrow> f  a > l" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

226 
apply (unfold LIM_def, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

227 
apply (drule_tac x="r" in spec, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

228 
apply (rule_tac x="min s R" in exI, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

229 
apply (simp add: 1) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

230 
apply (simp add: 2) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

231 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

232 

14477  233 
text{*Two uses in Hyperreal/Transcendental.ML*} 
234 
lemma LIM_trans: 

235 
"[ (%x. f(x) + g(x))  a > 0; g  a > l ] ==> f  a > l" 

236 
apply (drule LIM_add, assumption) 

237 
apply (auto simp add: add_assoc) 

238 
done 

239 

21239  240 
lemma LIM_compose: 
241 
assumes g: "g  l > g l" 

242 
assumes f: "f  a > l" 

243 
shows "(\<lambda>x. g (f x))  a > g l" 

244 
proof (rule LIM_I) 

245 
fix r::real assume r: "0 < r" 

246 
obtain s where s: "0 < s" 

247 
and less_r: "\<And>y. \<lbrakk>y \<noteq> l; norm (y  l) < s\<rbrakk> \<Longrightarrow> norm (g y  g l) < r" 

248 
using LIM_D [OF g r] by fast 

249 
obtain t where t: "0 < t" 

250 
and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < t\<rbrakk> \<Longrightarrow> norm (f x  l) < s" 

251 
using LIM_D [OF f s] by fast 

252 

253 
show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < t \<longrightarrow> norm (g (f x)  g l) < r" 

254 
proof (rule exI, safe) 

255 
show "0 < t" using t . 

256 
next 

257 
fix x assume "x \<noteq> a" and "norm (x  a) < t" 

258 
hence "norm (f x  l) < s" by (rule less_s) 

259 
thus "norm (g (f x)  g l) < r" 

260 
using r less_r by (case_tac "f x = l", simp_all) 

261 
qed 

262 
qed 

263 

264 
lemma LIM_o: "\<lbrakk>g  l > g l; f  a > l\<rbrakk> \<Longrightarrow> (g \<circ> f)  a > g l" 

265 
unfolding o_def by (rule LIM_compose) 

266 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

267 
lemma real_LIM_sandwich_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

268 
fixes f g :: "'a::real_normed_vector \<Rightarrow> real" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

269 
assumes f: "f  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

270 
assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

271 
assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

272 
shows "g  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

273 
proof (rule LIM_imp_LIM [OF f]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

274 
fix x assume x: "x \<noteq> a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

275 
have "norm (g x  0) = g x" by (simp add: 1 x) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

276 
also have "g x \<le> f x" by (rule 2 [OF x]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

277 
also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

278 
also have "\<bar>f x\<bar> = norm (f x  0)" by simp 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

279 
finally show "norm (g x  0) \<le> norm (f x  0)" . 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

280 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

281 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

282 
subsubsection {* Bounded Linear Operators *} 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

283 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

284 
locale bounded_linear = additive + 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

285 
constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

286 
assumes scaleR: "f (scaleR r x) = scaleR r (f x)" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

287 
assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

288 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

289 
lemma (in bounded_linear) pos_bounded: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

290 
"\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

291 
apply (cut_tac bounded, erule exE) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

292 
apply (rule_tac x="max 1 K" in exI, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

293 
apply (rule order_less_le_trans [OF zero_less_one le_maxI1]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

294 
apply (drule spec, erule order_trans) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

295 
apply (rule mult_left_mono [OF le_maxI2 norm_ge_zero]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

296 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

297 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

298 
lemma (in bounded_linear) pos_boundedE: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

299 
obtains K where "0 < K" and "\<forall>x. norm (f x) \<le> norm x * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

300 
using pos_bounded by fast 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

301 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

302 
lemma (in bounded_linear) cont: "f  a > f a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

303 
proof (rule LIM_I) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

304 
fix r::real assume r: "0 < r" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

305 
obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

306 
using pos_bounded by fast 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

307 
show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < s \<longrightarrow> norm (f x  f a) < r" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

308 
proof (rule exI, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

309 
from r K show "0 < r / K" by (rule divide_pos_pos) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

310 
next 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

311 
fix x assume x: "norm (x  a) < r / K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

312 
have "norm (f x  f a) = norm (f (x  a))" by (simp only: diff) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

313 
also have "\<dots> \<le> norm (x  a) * K" by (rule norm_le) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

314 
also from K x have "\<dots> < r" by (simp only: pos_less_divide_eq) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

315 
finally show "norm (f x  f a) < r" . 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

316 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

317 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

318 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

319 
lemma (in bounded_linear) LIM: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

320 
"g  a > l \<Longrightarrow> (\<lambda>x. f (g x))  a > f l" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

321 
by (rule LIM_compose [OF cont]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

322 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

323 
lemma (in bounded_linear) LIM_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

324 
"g  a > 0 \<Longrightarrow> (\<lambda>x. f (g x))  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

325 
by (drule LIM, simp only: zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

326 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

327 
subsubsection {* Bounded Bilinear Operators *} 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

328 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

329 
locale bounded_bilinear = 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

330 
fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector] 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

331 
\<Rightarrow> 'c::real_normed_vector" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

332 
(infixl "**" 70) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

333 
assumes add_left: "prod (a + a') b = prod a b + prod a' b" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

334 
assumes add_right: "prod a (b + b') = prod a b + prod a b'" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

335 
assumes scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

336 
assumes scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

337 
assumes bounded: "\<exists>K. \<forall>a b. norm (prod a b) \<le> norm a * norm b * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

338 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

339 
lemma (in bounded_bilinear) pos_bounded: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

340 
"\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

341 
apply (cut_tac bounded, erule exE) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

342 
apply (rule_tac x="max 1 K" in exI, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

343 
apply (rule order_less_le_trans [OF zero_less_one le_maxI1]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

344 
apply (drule spec, drule spec, erule order_trans) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

345 
apply (rule mult_left_mono [OF le_maxI2]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

346 
apply (intro mult_nonneg_nonneg norm_ge_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

347 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

348 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

349 
lemma (in bounded_bilinear) additive_right: "additive (\<lambda>b. prod a b)" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

350 
by (rule additive.intro, rule add_right) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

351 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

352 
lemma (in bounded_bilinear) additive_left: "additive (\<lambda>a. prod a b)" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

353 
by (rule additive.intro, rule add_left) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

354 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

355 
lemma (in bounded_bilinear) zero_left: "prod 0 b = 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

356 
by (rule additive.zero [OF additive_left]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

357 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

358 
lemma (in bounded_bilinear) zero_right: "prod a 0 = 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

359 
by (rule additive.zero [OF additive_right]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

360 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

361 
lemma (in bounded_bilinear) minus_left: "prod ( a) b =  prod a b" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

362 
by (rule additive.minus [OF additive_left]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

363 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

364 
lemma (in bounded_bilinear) minus_right: "prod a ( b) =  prod a b" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

365 
by (rule additive.minus [OF additive_right]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

366 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

367 
lemma (in bounded_bilinear) diff_left: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

368 
"prod (a  a') b = prod a b  prod a' b" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

369 
by (rule additive.diff [OF additive_left]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

370 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

371 
lemma (in bounded_bilinear) diff_right: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

372 
"prod a (b  b') = prod a b  prod a b'" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

373 
by (rule additive.diff [OF additive_right]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

374 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

375 
lemma (in bounded_bilinear) LIM_prod_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

376 
assumes f: "f  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

377 
assumes g: "g  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

378 
shows "(\<lambda>x. f x ** g x)  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

379 
proof (rule LIM_I) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

380 
fix r::real assume r: "0 < r" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

381 
obtain K where K: "0 < K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

382 
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

383 
using pos_bounded by fast 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

384 
from K have K': "0 < inverse K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

385 
by (rule positive_imp_inverse_positive) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

386 
obtain s where s: "0 < s" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

387 
and norm_f: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < s\<rbrakk> \<Longrightarrow> norm (f x) < r" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

388 
using LIM_D [OF f r] by auto 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

389 
obtain t where t: "0 < t" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

390 
and norm_g: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < t\<rbrakk> \<Longrightarrow> norm (g x) < inverse K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

391 
using LIM_D [OF g K'] by auto 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

392 
show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < s \<longrightarrow> norm (f x ** g x  0) < r" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

393 
proof (rule exI, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

394 
from s t show "0 < min s t" by simp 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

395 
next 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

396 
fix x assume x: "x \<noteq> a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

397 
assume "norm (x  a) < min s t" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

398 
hence xs: "norm (x  a) < s" and xt: "norm (x  a) < t" by simp_all 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

399 
from x xs have 1: "norm (f x) < r" by (rule norm_f) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

400 
from x xt have 2: "norm (g x) < inverse K" by (rule norm_g) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

401 
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" by (rule norm_le) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

402 
also from 1 2 K have "\<dots> < r * inverse K * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

403 
by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

404 
also from K have "r * inverse K * K = r" by simp 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

405 
finally show "norm (f x ** g x  0) < r" by simp 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

406 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

407 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

408 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

409 
lemma (in bounded_bilinear) bounded_linear_left: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

410 
"bounded_linear (\<lambda>a. a ** b)" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

411 
apply (unfold_locales) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

412 
apply (rule add_left) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

413 
apply (rule scaleR_left) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

414 
apply (cut_tac bounded, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

415 
apply (rule_tac x="norm b * K" in exI) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

416 
apply (simp add: mult_ac) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

417 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

418 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

419 
lemma (in bounded_bilinear) bounded_linear_right: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

420 
"bounded_linear (\<lambda>b. a ** b)" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

421 
apply (unfold_locales) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

422 
apply (rule add_right) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

423 
apply (rule scaleR_right) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

424 
apply (cut_tac bounded, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

425 
apply (rule_tac x="norm a * K" in exI) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

426 
apply (simp add: mult_ac) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

427 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

428 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

429 
lemma (in bounded_bilinear) LIM_left_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

430 
"f  a > 0 \<Longrightarrow> (\<lambda>x. f x ** c)  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

431 
by (rule bounded_linear.LIM_zero [OF bounded_linear_left]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

432 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

433 
lemma (in bounded_bilinear) LIM_right_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

434 
"f  a > 0 \<Longrightarrow> (\<lambda>x. c ** f x)  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

435 
by (rule bounded_linear.LIM_zero [OF bounded_linear_right]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

436 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

437 
lemma (in bounded_bilinear) prod_diff_prod: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

438 
"(x ** y  a ** b) = (x  a) ** (y  b) + (x  a) ** b + a ** (y  b)" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

439 
by (simp add: diff_left diff_right) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

440 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

441 
lemma (in bounded_bilinear) LIM: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

442 
"\<lbrakk>f  a > L; g  a > M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x)  a > L ** M" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

443 
apply (drule LIM_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

444 
apply (drule LIM_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

445 
apply (rule LIM_zero_cancel) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

446 
apply (subst prod_diff_prod) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

447 
apply (rule LIM_add_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

448 
apply (rule LIM_add_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

449 
apply (erule (1) LIM_prod_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

450 
apply (erule LIM_left_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

451 
apply (erule LIM_right_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

452 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

453 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

454 
interpretation bounded_bilinear_mult: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

455 
bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"] 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

456 
apply (rule bounded_bilinear.intro) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

457 
apply (rule left_distrib) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

458 
apply (rule right_distrib) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

459 
apply (rule mult_scaleR_left) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

460 
apply (rule mult_scaleR_right) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

461 
apply (rule_tac x="1" in exI) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

462 
apply (simp add: norm_mult_ineq) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

463 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

464 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

465 
interpretation bounded_bilinear_scaleR: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

466 
bounded_bilinear ["scaleR"] 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

467 
apply (rule bounded_bilinear.intro) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

468 
apply (rule scaleR_left_distrib) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

469 
apply (rule scaleR_right_distrib) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

470 
apply (simp add: real_scaleR_def) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

471 
apply (rule scaleR_left_commute) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

472 
apply (rule_tac x="1" in exI) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

473 
apply (simp add: norm_scaleR) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

474 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

475 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

476 
lemmas LIM_mult = bounded_bilinear_mult.LIM 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

477 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

478 
lemmas LIM_mult_zero = bounded_bilinear_mult.LIM_prod_zero 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

479 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

480 
lemmas LIM_mult_left_zero = bounded_bilinear_mult.LIM_left_zero 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

481 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

482 
lemmas LIM_mult_right_zero = bounded_bilinear_mult.LIM_right_zero 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

483 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

484 
lemmas LIM_scaleR = bounded_bilinear_scaleR.LIM 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

485 

20755  486 
subsubsection {* Purely nonstandard proofs *} 
14477  487 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

488 
lemma NSLIM_I: 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

489 
"(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

490 
\<Longrightarrow> f  a NS> L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

491 
by (simp add: NSLIM_def) 
14477  492 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

493 
lemma NSLIM_D: 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

494 
"\<lbrakk>f  a NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

495 
\<Longrightarrow> starfun f x \<approx> star_of L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

496 
by (simp add: NSLIM_def) 
14477  497 

20755  498 
text{*Proving properties of limits using nonstandard definition. 
499 
The properties hold for standard limits as well!*} 

500 

501 
lemma NSLIM_mult: 

502 
fixes l m :: "'a::real_normed_algebra" 

503 
shows "[ f  x NS> l; g  x NS> m ] 

504 
==> (%x. f(x) * g(x))  x NS> (l * m)" 

505 
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite) 

506 

20794  507 
lemma starfun_scaleR [simp]: 
508 
"starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))" 

509 
by transfer (rule refl) 

510 

511 
lemma NSLIM_scaleR: 

512 
"[ f  x NS> l; g  x NS> m ] 

513 
==> (%x. f(x) *# g(x))  x NS> (l *# m)" 

514 
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite) 

515 

20755  516 
lemma NSLIM_add: 
517 
"[ f  x NS> l; g  x NS> m ] 

518 
==> (%x. f(x) + g(x))  x NS> (l + m)" 

519 
by (auto simp add: NSLIM_def intro!: approx_add) 

520 

521 
lemma NSLIM_const [simp]: "(%x. k)  x NS> k" 

522 
by (simp add: NSLIM_def) 

523 

524 
lemma NSLIM_minus: "f  a NS> L ==> (%x. f(x))  a NS> L" 

525 
by (simp add: NSLIM_def) 

526 

527 
lemma NSLIM_add_minus: "[ f  x NS> l; g  x NS> m ] ==> (%x. f(x) + g(x))  x NS> (l + m)" 

528 
by (simp only: NSLIM_add NSLIM_minus) 

529 

530 
lemma NSLIM_inverse: 

531 
fixes L :: "'a::real_normed_div_algebra" 

532 
shows "[ f  a NS> L; L \<noteq> 0 ] 

533 
==> (%x. inverse(f(x)))  a NS> (inverse L)" 

534 
apply (simp add: NSLIM_def, clarify) 

535 
apply (drule spec) 

536 
apply (auto simp add: star_of_approx_inverse) 

537 
done 

538 

539 
lemma NSLIM_zero: 

540 
assumes f: "f  a NS> l" shows "(%x. f(x) + l)  a NS> 0" 

541 
proof  

542 
have "(\<lambda>x. f x +  l)  a NS> l + l" 

543 
by (rule NSLIM_add_minus [OF f NSLIM_const]) 

544 
thus ?thesis by simp 

545 
qed 

546 

547 
lemma NSLIM_zero_cancel: "(%x. f(x)  l)  x NS> 0 ==> f  x NS> l" 

548 
apply (drule_tac g = "%x. l" and m = l in NSLIM_add) 

549 
apply (auto simp add: diff_minus add_assoc) 

550 
done 

551 

552 
lemma NSLIM_const_not_eq: 

553 
fixes a :: real (* TODO: generalize to real_normed_div_algebra *) 

554 
shows "k \<noteq> L ==> ~ ((%x. k)  a NS> L)" 

555 
apply (simp add: NSLIM_def) 

556 
apply (rule_tac x="star_of a + epsilon" in exI) 

557 
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] 

558 
simp add: hypreal_epsilon_not_zero) 

559 
done 

560 

561 
lemma NSLIM_not_zero: 

562 
fixes a :: real 

563 
shows "k \<noteq> 0 ==> ~ ((%x. k)  a NS> 0)" 

564 
by (rule NSLIM_const_not_eq) 

565 

566 
lemma NSLIM_const_eq: 

567 
fixes a :: real 

568 
shows "(%x. k)  a NS> L ==> k = L" 

569 
apply (rule ccontr) 

570 
apply (blast dest: NSLIM_const_not_eq) 

571 
done 

572 

573 
text{* can actually be proved more easily by unfolding the definition!*} 

574 
lemma NSLIM_unique: 

575 
fixes a :: real 

576 
shows "[ f  a NS> L; f  a NS> M ] ==> L = M" 

577 
apply (drule NSLIM_minus) 

578 
apply (drule NSLIM_add, assumption) 

579 
apply (auto dest!: NSLIM_const_eq [symmetric]) 

580 
apply (simp add: diff_def [symmetric]) 

581 
done 

582 

583 
lemma NSLIM_mult_zero: 

584 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 

585 
shows "[ f  x NS> 0; g  x NS> 0 ] ==> (%x. f(x)*g(x))  x NS> 0" 

586 
by (drule NSLIM_mult, auto) 

587 

588 
lemma NSLIM_self: "(%x. x)  a NS> a" 

589 
by (simp add: NSLIM_def) 

590 

591 
subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *} 

592 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

593 
lemma LIM_NSLIM: 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

594 
assumes f: "f  a > L" shows "f  a NS> L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

595 
proof (rule NSLIM_I) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

596 
fix x 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

597 
assume neq: "x \<noteq> star_of a" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

598 
assume approx: "x \<approx> star_of a" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

599 
have "starfun f x  star_of L \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

600 
proof (rule InfinitesimalI2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

601 
fix r::real assume r: "0 < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

602 
from LIM_D [OF f r] 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

603 
obtain s where s: "0 < s" and 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

604 
less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < s\<rbrakk> \<Longrightarrow> norm (f x  L) < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

605 
by fast 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

606 
from less_r have less_r': 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

607 
"\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x  star_of a) < star_of s\<rbrakk> 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

608 
\<Longrightarrow> hnorm (starfun f x  star_of L) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

609 
by transfer 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

610 
from approx have "x  star_of a \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

611 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

612 
hence "hnorm (x  star_of a) < star_of s" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

613 
using s by (rule InfinitesimalD2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

614 
with neq show "hnorm (starfun f x  star_of L) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

615 
by (rule less_r') 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

616 
qed 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

617 
thus "starfun f x \<approx> star_of L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

618 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

619 
qed 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

620 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

621 
lemma NSLIM_LIM: 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

622 
assumes f: "f  a NS> L" shows "f  a > L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

623 
proof (rule LIM_I) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

624 
fix r::real assume r: "0 < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

625 
have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x  star_of a) < s 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

626 
\<longrightarrow> hnorm (starfun f x  star_of L) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

627 
proof (rule exI, safe) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

628 
show "0 < epsilon" by (rule hypreal_epsilon_gt_zero) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

629 
next 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

630 
fix x assume neq: "x \<noteq> star_of a" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

631 
assume "hnorm (x  star_of a) < epsilon" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

632 
with Infinitesimal_epsilon 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

633 
have "x  star_of a \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

634 
by (rule hnorm_less_Infinitesimal) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

635 
hence "x \<approx> star_of a" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

636 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

637 
with f neq have "starfun f x \<approx> star_of L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

638 
by (rule NSLIM_D) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

639 
hence "starfun f x  star_of L \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

640 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

641 
thus "hnorm (starfun f x  star_of L) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

642 
using r by (rule InfinitesimalD2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

643 
qed 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

644 
thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < s \<longrightarrow> norm (f x  L) < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

645 
by transfer 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

646 
qed 
14477  647 

15228  648 
theorem LIM_NSLIM_iff: "(f  x > L) = (f  x NS> L)" 
14477  649 
by (blast intro: LIM_NSLIM NSLIM_LIM) 
650 

20755  651 
subsubsection {* Derived theorems about @{term LIM} *} 
14477  652 

15228  653 
lemma LIM_mult2: 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

654 
fixes l m :: "'a::real_normed_algebra" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

655 
shows "[ f  x > l; g  x > m ] 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

656 
==> (%x. f(x) * g(x))  x > (l * m)" 
14477  657 
by (simp add: LIM_NSLIM_iff NSLIM_mult) 
658 

20794  659 
lemma LIM_scaleR: 
660 
"[ f  x > l; g  x > m ] 

661 
==> (%x. f(x) *# g(x))  x > (l *# m)" 

662 
by (simp add: LIM_NSLIM_iff NSLIM_scaleR) 

663 

15228  664 
lemma LIM_add2: 
665 
"[ f  x > l; g  x > m ] ==> (%x. f(x) + g(x))  x > (l + m)" 

14477  666 
by (simp add: LIM_NSLIM_iff NSLIM_add) 
667 

668 
lemma LIM_const2: "(%x. k)  x > k" 

669 
by (simp add: LIM_NSLIM_iff) 

670 

671 
lemma LIM_minus2: "f  a > L ==> (%x. f(x))  a > L" 

672 
by (simp add: LIM_NSLIM_iff NSLIM_minus) 

673 

674 
lemma LIM_add_minus2: "[ f  x > l; g  x > m ] ==> (%x. f(x) + g(x))  x > (l + m)" 

675 
by (simp add: LIM_NSLIM_iff NSLIM_add_minus) 

676 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

677 
lemma LIM_inverse: 
20653
24cda2c5fd40
removed division_by_zero class requirements from several lemmas
huffman
parents:
20635
diff
changeset

678 
fixes L :: "'a::real_normed_div_algebra" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

679 
shows "[ f  a > L; L \<noteq> 0 ] 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

680 
==> (%x. inverse(f(x)))  a > (inverse L)" 
14477  681 
by (simp add: LIM_NSLIM_iff NSLIM_inverse) 
682 

683 
lemma LIM_zero2: "f  a > l ==> (%x. f(x) + l)  a > 0" 

684 
by (simp add: LIM_NSLIM_iff NSLIM_zero) 

685 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

686 
lemma LIM_unique2: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

687 
fixes a :: real 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

688 
shows "[ f  a > L; f  a > M ] ==> L = M" 
14477  689 
by (simp add: LIM_NSLIM_iff NSLIM_unique) 
690 

691 
(* we can use the corresponding thm LIM_mult2 *) 

692 
(* for standard definition of limit *) 

693 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

694 
lemma LIM_mult_zero2: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

695 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

696 
shows "[ f  x > 0; g  x > 0 ] ==> (%x. f(x)*g(x))  x > 0" 
14477  697 
by (drule LIM_mult2, auto) 
698 

699 

20755  700 
subsection {* Continuity *} 
14477  701 

21239  702 
subsubsection {* Purely standard proofs *} 
703 

704 
lemma LIM_isCont_iff: "(f  a > f a) = ((\<lambda>h. f (a + h))  0 > f a)" 

705 
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) 

706 

707 
lemma isCont_iff: "isCont f x = (\<lambda>h. f (x + h))  0 > f x" 

708 
by (simp add: isCont_def LIM_isCont_iff) 

709 

710 
lemma isCont_Id: "isCont (\<lambda>x. x) a" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

711 
unfolding isCont_def by (rule LIM_self) 
21239  712 

713 
lemma isCont_const [simp]: "isCont (%x. k) a" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

714 
unfolding isCont_def by (rule LIM_const) 
21239  715 

716 
lemma isCont_add: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

717 
unfolding isCont_def by (rule LIM_add) 
21239  718 

719 
lemma isCont_minus: "isCont f a \<Longrightarrow> isCont (\<lambda>x.  f x) a" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

720 
unfolding isCont_def by (rule LIM_minus) 
21239  721 

722 
lemma isCont_diff: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x  g x) a" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

723 
unfolding isCont_def by (rule LIM_diff) 
21239  724 

725 
lemma isCont_mult: 

726 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 

727 
shows "[ isCont f a; isCont g a ] ==> isCont (%x. f(x) * g(x)) a" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

728 
unfolding isCont_def by (rule LIM_mult) 
21239  729 

730 
lemma isCont_inverse: 

731 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra" 

732 
shows "[ isCont f x; f x \<noteq> 0 ] ==> isCont (%x. inverse (f x)) x" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

733 
unfolding isCont_def by (rule LIM_inverse) 
21239  734 

735 
lemma isCont_LIM_compose: 

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

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

737 
unfolding isCont_def by (rule LIM_compose) 
21239  738 

739 
lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

740 
unfolding isCont_def by (rule LIM_compose) 
21239  741 

742 
lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

743 
unfolding o_def by (rule isCont_o2) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

744 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

745 
lemma (in bounded_linear) isCont: "isCont f a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

746 
unfolding isCont_def by (rule cont) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

747 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

748 
lemma (in bounded_bilinear) isCont: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

749 
"\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

750 
unfolding isCont_def by (rule LIM) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

751 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

752 
lemmas isCont_scaleR = bounded_bilinear_scaleR.isCont 
21239  753 

754 
subsubsection {* Nonstandard proofs *} 

755 

14477  756 
lemma isNSContD: "[ isNSCont f a; y \<approx> hypreal_of_real a ] ==> ( *f* f) y \<approx> hypreal_of_real (f a)" 
757 
by (simp add: isNSCont_def) 

758 

759 
lemma isNSCont_NSLIM: "isNSCont f a ==> f  a NS> (f a) " 

760 
by (simp add: isNSCont_def NSLIM_def) 

761 

762 
lemma NSLIM_isNSCont: "f  a NS> (f a) ==> isNSCont f a" 

763 
apply (simp add: isNSCont_def NSLIM_def, auto) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

764 
apply (case_tac "y = star_of a", auto) 
14477  765 
done 
766 

15228  767 
text{*NS continuity can be defined using NS Limit in 
768 
similar fashion to standard def of continuity*} 

14477  769 
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f  a NS> (f a))" 
770 
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont) 

771 

15228  772 
text{*Hence, NS continuity can be given 
773 
in terms of standard limit*} 

14477  774 
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f  a > (f a))" 
775 
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff) 

776 

15228  777 
text{*Moreover, it's trivial now that NS continuity 
778 
is equivalent to standard continuity*} 

14477  779 
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)" 
780 
apply (simp add: isCont_def) 

781 
apply (rule isNSCont_LIM_iff) 

782 
done 

783 

15228  784 
text{*Standard continuity ==> NS continuity*} 
14477  785 
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a" 
786 
by (erule isNSCont_isCont_iff [THEN iffD2]) 

787 

15228  788 
text{*NS continuity ==> Standard continuity*} 
14477  789 
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a" 
790 
by (erule isNSCont_isCont_iff [THEN iffD1]) 

791 

792 
text{*Alternative definition of continuity*} 

793 
(* Prove equivalence between NS limits  *) 

794 
(* seems easier than using standard def *) 

795 
lemma NSLIM_h_iff: "(f  a NS> L) = ((%h. f(a + h))  0 NS> L)" 

796 
apply (simp add: NSLIM_def, auto) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

797 
apply (drule_tac x = "star_of a + x" in spec) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

798 
apply (drule_tac [2] x = " star_of a + x" in spec, safe, simp) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

799 
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]]) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

800 
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1]) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

801 
prefer 2 apply (simp add: add_commute diff_def [symmetric]) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

802 
apply (rule_tac x = x in star_cases) 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

803 
apply (rule_tac [2] x = x in star_cases) 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

804 
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) 
14477  805 
done 
806 

807 
lemma NSLIM_isCont_iff: "(f  a NS> f a) = ((%h. f(a + h))  0 NS> f a)" 

808 
by (rule NSLIM_h_iff) 

809 

810 
lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x.  f x) a" 

811 
by (simp add: isNSCont_def) 

812 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

813 
lemma isNSCont_inverse: 
20653
24cda2c5fd40
removed division_by_zero class requirements from several lemmas
huffman
parents:
20635
diff
changeset

814 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

815 
shows "[ isNSCont f x; f x \<noteq> 0 ] ==> isNSCont (%x. inverse (f x)) x" 
14477  816 
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff) 
817 

15228  818 
lemma isNSCont_const [simp]: "isNSCont (%x. k) a" 
14477  819 
by (simp add: isNSCont_def) 
820 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

821 
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" 
14477  822 
apply (simp add: isNSCont_def) 
823 
apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs) 

824 
done 

825 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

826 
lemma isCont_abs [simp]: "isCont abs (a::real)" 
14477  827 
by (auto simp add: isNSCont_isCont_iff [symmetric]) 
15228  828 

14477  829 

830 
(**************************************************************** 

831 
(%* Leave as commented until I add topology theory or remove? *%) 

832 
(%* 

833 
Elementary topology proof for a characterisation of 

834 
continuity now: a function f is continuous if and only 

835 
if the inverse image, {x. f(x) \<in> A}, of any open set A 

836 
is always an open set 

837 
*%) 

838 
Goal "[ isNSopen A; \<forall>x. isNSCont f x ] 

839 
==> isNSopen {x. f x \<in> A}" 

840 
by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); 

841 
by (dtac (mem_monad_approx RS approx_sym); 

842 
by (dres_inst_tac [("x","a")] spec 1); 

843 
by (dtac isNSContD 1 THEN assume_tac 1) 

844 
by (dtac bspec 1 THEN assume_tac 1) 

845 
by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1); 

846 
by (blast_tac (claset() addIs [starfun_mem_starset]); 

847 
qed "isNSCont_isNSopen"; 

848 

849 
Goalw [isNSCont_def] 

850 
"\<forall>A. isNSopen A > isNSopen {x. f x \<in> A} \ 

851 
\ ==> isNSCont f x"; 

852 
by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS 

853 
(approx_minus_iff RS iffD2)],simpset() addsimps 

854 
[Infinitesimal_def,SReal_iff])); 

855 
by (dres_inst_tac [("x","{z. abs(z + f(x)) < ya}")] spec 1); 

856 
by (etac (isNSopen_open_interval RSN (2,impE)); 

857 
by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def])); 

858 
by (dres_inst_tac [("x","x")] spec 1); 

859 
by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad], 

860 
simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus])); 

861 
qed "isNSopen_isNSCont"; 

862 

863 
Goal "(\<forall>x. isNSCont f x) = \ 

864 
\ (\<forall>A. isNSopen A > isNSopen {x. f(x) \<in> A})"; 

865 
by (blast_tac (claset() addIs [isNSCont_isNSopen, 

866 
isNSopen_isNSCont]); 

867 
qed "isNSCont_isNSopen_iff"; 

868 

869 
(%* Standard version of same theorem *%) 

870 
Goal "(\<forall>x. isCont f x) = \ 

871 
\ (\<forall>A. isopen A > isopen {x. f(x) \<in> A})"; 

872 
by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff], 

873 
simpset() addsimps [isNSopen_isopen_iff RS sym, 

874 
isNSCont_isCont_iff RS sym])); 

875 
qed "isCont_isopen_iff"; 

876 
*******************************************************************) 

877 

20755  878 
subsection {* Uniform Continuity *} 
879 

14477  880 
lemma isNSUContD: "[ isNSUCont f; x \<approx> y] ==> ( *f* f) x \<approx> ( *f* f) y" 
881 
by (simp add: isNSUCont_def) 

882 

883 
lemma isUCont_isCont: "isUCont f ==> isCont f x" 

884 
by (simp add: isUCont_def isCont_def LIM_def, meson) 

885 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

886 
lemma isUCont_isNSUCont: 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

887 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

888 
assumes f: "isUCont f" shows "isNSUCont f" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

889 
proof (unfold isNSUCont_def, safe) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

890 
fix x y :: "'a star" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

891 
assume approx: "x \<approx> y" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

892 
have "starfun f x  starfun f y \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

893 
proof (rule InfinitesimalI2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

894 
fix r::real assume r: "0 < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

895 
with f obtain s where s: "0 < s" and 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

896 
less_r: "\<And>x y. norm (x  y) < s \<Longrightarrow> norm (f x  f y) < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

897 
by (auto simp add: isUCont_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

898 
from less_r have less_r': 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

899 
"\<And>x y. hnorm (x  y) < star_of s 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

900 
\<Longrightarrow> hnorm (starfun f x  starfun f y) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

901 
by transfer 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

902 
from approx have "x  y \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

903 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

904 
hence "hnorm (x  y) < star_of s" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

905 
using s by (rule InfinitesimalD2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

906 
thus "hnorm (starfun f x  starfun f y) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

907 
by (rule less_r') 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

908 
qed 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

909 
thus "starfun f x \<approx> starfun f y" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

910 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

911 
qed 
14477  912 

913 
lemma isNSUCont_isUCont: 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

914 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

915 
assumes f: "isNSUCont f" shows "isUCont f" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

916 
proof (unfold isUCont_def, safe) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

917 
fix r::real assume r: "0 < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

918 
have "\<exists>s>0. \<forall>x y. hnorm (x  y) < s 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

919 
\<longrightarrow> hnorm (starfun f x  starfun f y) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

920 
proof (rule exI, safe) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

921 
show "0 < epsilon" by (rule hypreal_epsilon_gt_zero) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

922 
next 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

923 
fix x y :: "'a star" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

924 
assume "hnorm (x  y) < epsilon" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

925 
with Infinitesimal_epsilon 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

926 
have "x  y \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

927 
by (rule hnorm_less_Infinitesimal) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

928 
hence "x \<approx> y" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

929 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

930 
with f have "starfun f x \<approx> starfun f y" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

931 
by (simp add: isNSUCont_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

932 
hence "starfun f x  starfun f y \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

933 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

934 
thus "hnorm (starfun f x  starfun f y) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

935 
using r by (rule InfinitesimalD2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

936 
qed 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

937 
thus "\<exists>s>0. \<forall>x y. norm (x  y) < s \<longrightarrow> norm (f x  f y) < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

938 
by transfer 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

939 
qed 
14477  940 

21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

941 
subsection {* Relation of LIM and LIMSEQ *} 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

942 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

943 
lemma LIMSEQ_SEQ_conv1: 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

944 
fixes a :: "'a::real_normed_vector" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

945 
assumes X: "X  a > L" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

946 
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

947 
proof (safe intro!: LIMSEQ_I) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

948 
fix S :: "nat \<Rightarrow> 'a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

949 
fix r :: real 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

950 
assume rgz: "0 < r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

951 
assume as: "\<forall>n. S n \<noteq> a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

952 
assume S: "S > a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

953 
from LIM_D [OF X rgz] obtain s 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

954 
where sgz: "0 < s" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

955 
and aux: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < s\<rbrakk> \<Longrightarrow> norm (X x  L) < r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

956 
by fast 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

957 
from LIMSEQ_D [OF S sgz] 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

958 
obtain no where "\<forall>n\<ge>no. norm (S n  a) < s" by fast 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

959 
hence "\<forall>n\<ge>no. norm (X (S n)  L) < r" by (simp add: aux as) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

960 
thus "\<exists>no. \<forall>n\<ge>no. norm (X (S n)  L) < r" .. 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

961 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

962 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

963 
lemma LIMSEQ_SEQ_conv2: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

964 
fixes a :: real 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

965 
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

966 
shows "X  a > L" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

967 
proof (rule ccontr) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

968 
assume "\<not> (X  a > L)" 
20563  969 
hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x  a) < s > norm (X x  L) < r)" by (unfold LIM_def) 
970 
hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x  a\<bar> < s > norm (X x  L) < r)" by simp 

971 
hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x  a\<bar> < s \<and> norm (X x  L) \<ge> r)" by (simp add: linorder_not_less) 

972 
then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x  a\<bar> < s \<and> norm (X x  L) \<ge> r))" by auto 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

973 

20563  974 
let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x  a\<bar> < inverse (real (Suc n)) \<and> norm (X x  L) \<ge> r" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

975 
have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x  a\<bar> < inverse (real (Suc n)) \<and> norm (X x  L) \<ge> r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

976 
using rdef by simp 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

977 
hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n  a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n)  L) \<ge> r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

978 
by (rule someI_ex) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

979 
hence F1: "\<And>n. ?F n \<noteq> a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

980 
and F2: "\<And>n. \<bar>?F n  a\<bar> < inverse (real (Suc n))" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

981 
and F3: "\<And>n. norm (X (?F n)  L) \<ge> r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

982 
by fast+ 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

983 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

984 
have "?F > a" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

985 
proof (rule LIMSEQ_I, unfold real_norm_def) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

986 
fix e::real 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

987 
assume "0 < e" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

988 
(* choose no such that inverse (real (Suc n)) < e *) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

989 
have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

990 
then obtain m where nodef: "inverse (real (Suc m)) < e" by auto 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

991 
show "\<exists>no. \<forall>n. no \<le> n > \<bar>?F n  a\<bar> < e" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

992 
proof (intro exI allI impI) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

993 
fix n 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

994 
assume mlen: "m \<le> n" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

995 
have "\<bar>?F n  a\<bar> < inverse (real (Suc n))" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

996 
by (rule F2) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

997 
also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

998 
by auto 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

999 
also from nodef have 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1000 
"inverse (real (Suc m)) < e" . 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

1001 
finally show "\<bar>?F n  a\<bar> < e" . 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

1002 
qed 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1003 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1004 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1005 
moreover have "\<forall>n. ?F n \<noteq> a" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

1006 
by (rule allI) (rule F1) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

1007 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1008 
moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1009 
ultimately have "(\<lambda>n. X (?F n)) > L" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1010 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1011 
moreover have "\<not> ((\<lambda>n. X (?F n)) > L)" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1012 
proof  
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1013 
{ 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1014 
fix no::nat 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1015 
obtain n where "n = no + 1" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1016 
then have nolen: "no \<le> n" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1017 
(* We prove this by showing that for any m there is an n\<ge>m such that X (?F n)  L \<ge> r *) 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

1018 
have "norm (X (?F n)  L) \<ge> r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

1019 
by (rule F3) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

1020 
with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n)  L) \<ge> r" by fast 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1021 
} 
20563  1022 
then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n)  L) \<ge> r)" by simp 
1023 
with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n)  L) \<ge> e)" by auto 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1024 
thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1025 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1026 
ultimately show False by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1027 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1028 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1029 
lemma LIMSEQ_SEQ_conv: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

1030 
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > (a::real) \<longrightarrow> (\<lambda>n. X (S n)) > L) = 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

1031 
(X  a > L)" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1032 
proof 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1033 
assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1034 
show "X  a > L" by (rule LIMSEQ_SEQ_conv2) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1035 
next 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1036 
assume "(X  a > L)" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1037 
show "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" by (rule LIMSEQ_SEQ_conv1) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1038 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

1039 

10751  1040 
end 