8 |
8 |
9 theory Lim |
9 theory Lim |
10 imports SEQ |
10 imports SEQ |
11 begin |
11 begin |
12 |
12 |
13 text{*Standard Definitions*} |
|
14 |
|
15 abbreviation |
|
16 LIM :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a, 'b] \<Rightarrow> bool" |
|
17 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where |
|
18 "f -- a --> L \<equiv> (f ---> L) (at a)" |
|
19 |
|
20 definition |
|
21 isCont :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a] \<Rightarrow> bool" where |
|
22 "isCont f a = (f -- a --> (f a))" |
|
23 |
|
24 definition |
13 definition |
25 isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where |
14 isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where |
26 "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)" |
15 "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)" |
27 |
16 |
28 subsection {* Limits of Functions *} |
17 subsection {* Limits of Functions *} |
29 |
|
30 lemma LIM_def: "f -- a --> L = |
|
31 (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s |
|
32 --> dist (f x) L < r)" |
|
33 unfolding tendsto_iff eventually_at .. |
|
34 |
18 |
35 lemma metric_LIM_I: |
19 lemma metric_LIM_I: |
36 "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r) |
20 "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r) |
37 \<Longrightarrow> f -- a --> L" |
21 \<Longrightarrow> f -- a --> L" |
38 by (simp add: LIM_def) |
22 by (simp add: LIM_def) |
79 lemma LIM_offset_zero_cancel: |
63 lemma LIM_offset_zero_cancel: |
80 fixes a :: "'a::real_normed_vector" |
64 fixes a :: "'a::real_normed_vector" |
81 shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L" |
65 shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L" |
82 by (drule_tac k="- a" in LIM_offset, simp) |
66 by (drule_tac k="- a" in LIM_offset, simp) |
83 |
67 |
84 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp |
|
85 |
|
86 lemma LIM_zero: |
68 lemma LIM_zero: |
87 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
69 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
88 shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F" |
70 shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F" |
89 unfolding tendsto_iff dist_norm by simp |
71 unfolding tendsto_iff dist_norm by simp |
90 |
72 |
111 assumes f: "f -- a --> l" |
93 assumes f: "f -- a --> l" |
112 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)" |
94 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)" |
113 shows "g -- a --> m" |
95 shows "g -- a --> m" |
114 by (rule metric_LIM_imp_LIM [OF f], |
96 by (rule metric_LIM_imp_LIM [OF f], |
115 simp add: dist_norm le) |
97 simp add: dist_norm le) |
116 |
|
117 lemma LIM_const_not_eq: |
|
118 fixes a :: "'a::perfect_space" |
|
119 fixes k L :: "'b::t2_space" |
|
120 shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L" |
|
121 by (simp add: tendsto_const_iff) |
|
122 |
|
123 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0] |
|
124 |
|
125 lemma LIM_const_eq: |
|
126 fixes a :: "'a::perfect_space" |
|
127 fixes k L :: "'b::t2_space" |
|
128 shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L" |
|
129 by (simp add: tendsto_const_iff) |
|
130 |
|
131 lemma LIM_unique: |
|
132 fixes a :: "'a::perfect_space" |
|
133 fixes L M :: "'b::t2_space" |
|
134 shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M" |
|
135 using at_neq_bot by (rule tendsto_unique) |
|
136 |
|
137 text{*Limits are equal for functions equal except at limit point*} |
|
138 lemma LIM_equal: |
|
139 "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)" |
|
140 unfolding tendsto_def eventually_at_topological by simp |
|
141 |
|
142 lemma LIM_cong: |
|
143 "\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk> |
|
144 \<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)" |
|
145 by (simp add: LIM_equal) |
|
146 |
98 |
147 lemma metric_LIM_equal2: |
99 lemma metric_LIM_equal2: |
148 assumes 1: "0 < R" |
100 assumes 1: "0 < R" |
149 assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x" |
101 assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x" |
150 shows "g -- a --> l \<Longrightarrow> f -- a --> l" |
102 shows "g -- a --> l \<Longrightarrow> f -- a --> l" |
161 assumes 1: "0 < R" |
113 assumes 1: "0 < R" |
162 assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x" |
114 assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x" |
163 shows "g -- a --> l \<Longrightarrow> f -- a --> l" |
115 shows "g -- a --> l \<Longrightarrow> f -- a --> l" |
164 by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm) |
116 by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm) |
165 |
117 |
166 lemma LIM_compose_eventually: |
|
167 assumes f: "f -- a --> b" |
|
168 assumes g: "g -- b --> c" |
|
169 assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)" |
|
170 shows "(\<lambda>x. g (f x)) -- a --> c" |
|
171 using g f inj by (rule tendsto_compose_eventually) |
|
172 |
|
173 lemma metric_LIM_compose2: |
118 lemma metric_LIM_compose2: |
174 assumes f: "f -- a --> b" |
119 assumes f: "f -- a --> b" |
175 assumes g: "g -- b --> c" |
120 assumes g: "g -- b --> c" |
176 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b" |
121 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b" |
177 shows "(\<lambda>x. g (f x)) -- a --> c" |
122 shows "(\<lambda>x. g (f x)) -- a --> c" |
184 assumes g: "g -- b --> c" |
129 assumes g: "g -- b --> c" |
185 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b" |
130 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b" |
186 shows "(\<lambda>x. g (f x)) -- a --> c" |
131 shows "(\<lambda>x. g (f x)) -- a --> c" |
187 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) |
132 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) |
188 |
133 |
189 lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l" |
|
190 unfolding o_def by (rule tendsto_compose) |
|
191 |
|
192 lemma real_LIM_sandwich_zero: |
134 lemma real_LIM_sandwich_zero: |
193 fixes f g :: "'a::topological_space \<Rightarrow> real" |
135 fixes f g :: "'a::topological_space \<Rightarrow> real" |
194 assumes f: "f -- a --> 0" |
136 assumes f: "f -- a --> 0" |
195 assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x" |
137 assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x" |
196 assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x" |
138 assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x" |
197 shows "g -- a --> 0" |
139 shows "g -- a --> 0" |
198 proof (rule LIM_imp_LIM [OF f]) |
140 proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *) |
199 fix x assume x: "x \<noteq> a" |
141 fix x assume x: "x \<noteq> a" |
200 have "norm (g x - 0) = g x" by (simp add: 1 x) |
142 have "norm (g x - 0) = g x" by (simp add: 1 x) |
201 also have "g x \<le> f x" by (rule 2 [OF x]) |
143 also have "g x \<le> f x" by (rule 2 [OF x]) |
202 also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self) |
144 also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self) |
203 also have "\<bar>f x\<bar> = norm (f x - 0)" by simp |
145 also have "\<bar>f x\<bar> = norm (f x - 0)" by simp |
215 lemma isCont_iff: |
157 lemma isCont_iff: |
216 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space" |
158 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space" |
217 shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x" |
159 shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x" |
218 by (simp add: isCont_def LIM_isCont_iff) |
160 by (simp add: isCont_def LIM_isCont_iff) |
219 |
161 |
220 lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a" |
|
221 unfolding isCont_def by (rule tendsto_ident_at) |
|
222 |
|
223 lemma isCont_const [simp]: "isCont (\<lambda>x. k) a" |
|
224 unfolding isCont_def by (rule tendsto_const) |
|
225 |
|
226 lemma isCont_norm [simp]: |
162 lemma isCont_norm [simp]: |
227 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
163 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
228 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a" |
164 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a" |
229 unfolding isCont_def by (rule tendsto_norm) |
165 unfolding isCont_def by (rule tendsto_norm) |
230 |
166 |
260 |
196 |
261 lemma isCont_divide [simp]: |
197 lemma isCont_divide [simp]: |
262 fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field" |
198 fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field" |
263 shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a" |
199 shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a" |
264 unfolding isCont_def by (rule tendsto_divide) |
200 unfolding isCont_def by (rule tendsto_divide) |
265 |
|
266 lemma isCont_tendsto_compose: |
|
267 "\<lbrakk>isCont g l; (f ---> l) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F" |
|
268 unfolding isCont_def by (rule tendsto_compose) |
|
269 |
201 |
270 lemma metric_isCont_LIM_compose2: |
202 lemma metric_isCont_LIM_compose2: |
271 assumes f [unfolded isCont_def]: "isCont f a" |
203 assumes f [unfolded isCont_def]: "isCont f a" |
272 assumes g: "g -- f a --> l" |
204 assumes g: "g -- f a --> l" |
273 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a" |
205 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a" |
279 assumes f [unfolded isCont_def]: "isCont f a" |
211 assumes f [unfolded isCont_def]: "isCont f a" |
280 assumes g: "g -- f a --> l" |
212 assumes g: "g -- f a --> l" |
281 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a" |
213 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a" |
282 shows "(\<lambda>x. g (f x)) -- a --> l" |
214 shows "(\<lambda>x. g (f x)) -- a --> l" |
283 by (rule LIM_compose2 [OF f g inj]) |
215 by (rule LIM_compose2 [OF f g inj]) |
284 |
|
285 lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a" |
|
286 unfolding isCont_def by (rule tendsto_compose) |
|
287 |
|
288 lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a" |
|
289 unfolding o_def by (rule isCont_o2) |
|
290 |
216 |
291 lemma (in bounded_linear) isCont: |
217 lemma (in bounded_linear) isCont: |
292 "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a" |
218 "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a" |
293 unfolding isCont_def by (rule tendsto) |
219 unfolding isCont_def by (rule tendsto) |
294 |
220 |
370 proof (rule ccontr) |
296 proof (rule ccontr) |
371 let ?I = "\<lambda>n. inverse (real (Suc n))" |
297 let ?I = "\<lambda>n. inverse (real (Suc n))" |
372 def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" |
298 def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" |
373 assume "\<not> eventually P (at a within s)" |
299 assume "\<not> eventually P (at a within s)" |
374 hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x" |
300 hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x" |
375 unfolding Limits.eventually_within Limits.eventually_at by fast |
301 unfolding eventually_within eventually_at by fast |
376 hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp |
302 hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp |
377 hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)" |
303 hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)" |
378 unfolding F_def by (rule someI_ex) |
304 unfolding F_def by (rule someI_ex) |
379 hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a" |
305 hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a" |
380 and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)" |
306 and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)" |