79 lemma LIM_offset_zero_cancel: |
79 lemma LIM_offset_zero_cancel: |
80 fixes a :: "'a::real_normed_vector" |
80 fixes a :: "'a::real_normed_vector" |
81 shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L" |
81 shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L" |
82 by (drule_tac k="- a" in LIM_offset, simp) |
82 by (drule_tac k="- a" in LIM_offset, simp) |
83 |
83 |
84 lemma LIM_const [simp]: "(%x. k) -- x --> k" |
|
85 by (rule tendsto_const) |
|
86 |
|
87 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp |
84 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp |
88 |
|
89 lemma LIM_add: |
|
90 fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
|
91 assumes f: "f -- a --> L" and g: "g -- a --> M" |
|
92 shows "(\<lambda>x. f x + g x) -- a --> (L + M)" |
|
93 using assms by (rule tendsto_add) |
|
94 |
|
95 lemma LIM_add_zero: |
|
96 fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
|
97 shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0" |
|
98 by (rule tendsto_add_zero) |
|
99 |
|
100 lemma LIM_minus: |
|
101 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
|
102 shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L" |
|
103 by (rule tendsto_minus) |
|
104 |
|
105 lemma LIM_diff: |
|
106 fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
|
107 shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m" |
|
108 by (rule tendsto_diff) |
|
109 |
85 |
110 lemma LIM_zero: |
86 lemma LIM_zero: |
111 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
87 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
112 shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0" |
88 shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0" |
113 unfolding tendsto_iff dist_norm by simp |
89 unfolding tendsto_iff dist_norm by simp |
136 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)" |
112 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)" |
137 shows "g -- a --> m" |
113 shows "g -- a --> m" |
138 by (rule metric_LIM_imp_LIM [OF f], |
114 by (rule metric_LIM_imp_LIM [OF f], |
139 simp add: dist_norm le) |
115 simp add: dist_norm le) |
140 |
116 |
141 lemma LIM_norm: |
|
142 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
|
143 shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l" |
|
144 by (rule tendsto_norm) |
|
145 |
|
146 lemma LIM_norm_zero: |
|
147 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
|
148 shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0" |
|
149 by (rule tendsto_norm_zero) |
|
150 |
|
151 lemma LIM_norm_zero_cancel: |
|
152 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
|
153 shows "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0" |
|
154 by (rule tendsto_norm_zero_cancel) |
|
155 |
|
156 lemma LIM_norm_zero_iff: |
|
157 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
|
158 shows "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0" |
|
159 by (rule tendsto_norm_zero_iff) |
|
160 |
|
161 lemma LIM_rabs: "f -- a --> (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> \<bar>l\<bar>" |
|
162 by (rule tendsto_rabs) |
|
163 |
|
164 lemma LIM_rabs_zero: "f -- a --> (0::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> 0" |
|
165 by (rule tendsto_rabs_zero) |
|
166 |
|
167 lemma LIM_rabs_zero_cancel: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) \<Longrightarrow> f -- a --> 0" |
|
168 by (rule tendsto_rabs_zero_cancel) |
|
169 |
|
170 lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0" |
|
171 by (rule tendsto_rabs_zero_iff) |
|
172 |
|
173 lemma trivial_limit_at: |
117 lemma trivial_limit_at: |
174 fixes a :: "'a::real_normed_algebra_1" |
118 fixes a :: "'a::real_normed_algebra_1" |
175 shows "\<not> trivial_limit (at a)" -- {* TODO: find a more appropriate class *} |
119 shows "\<not> trivial_limit (at a)" -- {* TODO: find a more appropriate class *} |
176 unfolding trivial_limit_def |
120 unfolding trivial_limit_def |
177 unfolding eventually_at dist_norm |
121 unfolding eventually_at dist_norm |
227 assumes 1: "0 < R" |
168 assumes 1: "0 < R" |
228 assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x" |
169 assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x" |
229 shows "g -- a --> l \<Longrightarrow> f -- a --> l" |
170 shows "g -- a --> l \<Longrightarrow> f -- a --> l" |
230 by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm) |
171 by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm) |
231 |
172 |
232 lemma LIM_compose: |
|
233 assumes g: "g -- l --> g l" |
|
234 assumes f: "f -- a --> l" |
|
235 shows "(\<lambda>x. g (f x)) -- a --> g l" |
|
236 using assms by (rule tendsto_compose) |
|
237 |
|
238 lemma LIM_compose_eventually: |
173 lemma LIM_compose_eventually: |
239 assumes f: "f -- a --> b" |
174 assumes f: "f -- a --> b" |
240 assumes g: "g -- b --> c" |
175 assumes g: "g -- b --> c" |
241 assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)" |
176 assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)" |
242 shows "(\<lambda>x. g (f x)) -- a --> c" |
177 shows "(\<lambda>x. g (f x)) -- a --> c" |
245 lemma metric_LIM_compose2: |
180 lemma metric_LIM_compose2: |
246 assumes f: "f -- a --> b" |
181 assumes f: "f -- a --> b" |
247 assumes g: "g -- b --> c" |
182 assumes g: "g -- b --> c" |
248 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b" |
183 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b" |
249 shows "(\<lambda>x. g (f x)) -- a --> c" |
184 shows "(\<lambda>x. g (f x)) -- a --> c" |
250 using f g inj [folded eventually_at] |
185 using g f inj [folded eventually_at] |
251 by (rule LIM_compose_eventually) |
186 by (rule tendsto_compose_eventually) |
252 |
187 |
253 lemma LIM_compose2: |
188 lemma LIM_compose2: |
254 fixes a :: "'a::real_normed_vector" |
189 fixes a :: "'a::real_normed_vector" |
255 assumes f: "f -- a --> b" |
190 assumes f: "f -- a --> b" |
256 assumes g: "g -- b --> c" |
191 assumes g: "g -- b --> c" |
257 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b" |
192 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b" |
258 shows "(\<lambda>x. g (f x)) -- a --> c" |
193 shows "(\<lambda>x. g (f x)) -- a --> c" |
259 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) |
194 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) |
260 |
195 |
261 lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l" |
196 lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l" |
262 unfolding o_def by (rule LIM_compose) |
197 unfolding o_def by (rule tendsto_compose) |
263 |
198 |
264 lemma real_LIM_sandwich_zero: |
199 lemma real_LIM_sandwich_zero: |
265 fixes f g :: "'a::topological_space \<Rightarrow> real" |
200 fixes f g :: "'a::topological_space \<Rightarrow> real" |
266 assumes f: "f -- a --> 0" |
201 assumes f: "f -- a --> 0" |
267 assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x" |
202 assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x" |
305 |
240 |
306 lemma (in bounded_bilinear) LIM_right_zero: |
241 lemma (in bounded_bilinear) LIM_right_zero: |
307 "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0" |
242 "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0" |
308 by (rule tendsto_right_zero) |
243 by (rule tendsto_right_zero) |
309 |
244 |
310 lemmas LIM_mult = |
|
311 bounded_bilinear.LIM [OF bounded_bilinear_mult] |
|
312 |
|
313 lemmas LIM_mult_zero = |
245 lemmas LIM_mult_zero = |
314 bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult] |
246 bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult] |
315 |
247 |
316 lemmas LIM_mult_left_zero = |
248 lemmas LIM_mult_left_zero = |
317 bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult] |
249 bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult] |
318 |
250 |
319 lemmas LIM_mult_right_zero = |
251 lemmas LIM_mult_right_zero = |
320 bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult] |
252 bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult] |
321 |
|
322 lemmas LIM_scaleR = |
|
323 bounded_bilinear.LIM [OF bounded_bilinear_scaleR] |
|
324 |
|
325 lemmas LIM_of_real = |
|
326 bounded_linear.LIM [OF bounded_linear_of_real] |
|
327 |
|
328 lemma LIM_power: |
|
329 fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}" |
|
330 assumes f: "f -- a --> l" |
|
331 shows "(\<lambda>x. f x ^ n) -- a --> l ^ n" |
|
332 using assms by (rule tendsto_power) |
|
333 |
|
334 lemma LIM_inverse: |
|
335 fixes L :: "'a::real_normed_div_algebra" |
|
336 shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L" |
|
337 by (rule tendsto_inverse) |
|
338 |
253 |
339 lemma LIM_inverse_fun: |
254 lemma LIM_inverse_fun: |
340 assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)" |
255 assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)" |
341 shows "inverse -- a --> inverse a" |
256 shows "inverse -- a --> inverse a" |
342 by (rule LIM_inverse [OF LIM_ident a]) |
257 by (rule tendsto_inverse [OF tendsto_ident_at a]) |
343 |
|
344 lemma LIM_sgn: |
|
345 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
|
346 shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l" |
|
347 by (rule tendsto_sgn) |
|
348 |
258 |
349 |
259 |
350 subsection {* Continuity *} |
260 subsection {* Continuity *} |
351 |
261 |
352 lemma LIM_isCont_iff: |
262 lemma LIM_isCont_iff: |
358 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space" |
268 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space" |
359 shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x" |
269 shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x" |
360 by (simp add: isCont_def LIM_isCont_iff) |
270 by (simp add: isCont_def LIM_isCont_iff) |
361 |
271 |
362 lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a" |
272 lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a" |
363 unfolding isCont_def by (rule LIM_ident) |
273 unfolding isCont_def by (rule tendsto_ident_at) |
364 |
274 |
365 lemma isCont_const [simp]: "isCont (\<lambda>x. k) a" |
275 lemma isCont_const [simp]: "isCont (\<lambda>x. k) a" |
366 unfolding isCont_def by (rule LIM_const) |
276 unfolding isCont_def by (rule tendsto_const) |
367 |
277 |
368 lemma isCont_norm [simp]: |
278 lemma isCont_norm [simp]: |
369 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
279 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
370 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a" |
280 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a" |
371 unfolding isCont_def by (rule LIM_norm) |
281 unfolding isCont_def by (rule tendsto_norm) |
372 |
282 |
373 lemma isCont_rabs [simp]: |
283 lemma isCont_rabs [simp]: |
374 fixes f :: "'a::topological_space \<Rightarrow> real" |
284 fixes f :: "'a::topological_space \<Rightarrow> real" |
375 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a" |
285 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a" |
376 unfolding isCont_def by (rule LIM_rabs) |
286 unfolding isCont_def by (rule tendsto_rabs) |
377 |
287 |
378 lemma isCont_add [simp]: |
288 lemma isCont_add [simp]: |
379 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
289 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
380 shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a" |
290 shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a" |
381 unfolding isCont_def by (rule LIM_add) |
291 unfolding isCont_def by (rule tendsto_add) |
382 |
292 |
383 lemma isCont_minus [simp]: |
293 lemma isCont_minus [simp]: |
384 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
294 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
385 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a" |
295 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a" |
386 unfolding isCont_def by (rule LIM_minus) |
296 unfolding isCont_def by (rule tendsto_minus) |
387 |
297 |
388 lemma isCont_diff [simp]: |
298 lemma isCont_diff [simp]: |
389 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
299 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
390 shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a" |
300 shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a" |
391 unfolding isCont_def by (rule LIM_diff) |
301 unfolding isCont_def by (rule tendsto_diff) |
392 |
302 |
393 lemma isCont_mult [simp]: |
303 lemma isCont_mult [simp]: |
394 fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra" |
304 fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra" |
395 shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a" |
305 shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a" |
396 unfolding isCont_def by (rule LIM_mult) |
306 unfolding isCont_def by (rule tendsto_mult) |
397 |
307 |
398 lemma isCont_inverse [simp]: |
308 lemma isCont_inverse [simp]: |
399 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra" |
309 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra" |
400 shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a" |
310 shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a" |
401 unfolding isCont_def by (rule LIM_inverse) |
311 unfolding isCont_def by (rule tendsto_inverse) |
402 |
312 |
403 lemma isCont_divide [simp]: |
313 lemma isCont_divide [simp]: |
404 fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field" |
314 fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field" |
405 shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a" |
315 shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a" |
406 unfolding isCont_def by (rule tendsto_divide) |
316 unfolding isCont_def by (rule tendsto_divide) |
407 |
317 |
408 lemma isCont_tendsto_compose: |
318 lemma isCont_tendsto_compose: |
409 "\<lbrakk>isCont g l; (f ---> l) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F" |
319 "\<lbrakk>isCont g l; (f ---> l) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F" |
410 unfolding isCont_def by (rule tendsto_compose) |
320 unfolding isCont_def by (rule tendsto_compose) |
411 |
|
412 lemma isCont_LIM_compose: |
|
413 "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l" |
|
414 by (rule isCont_tendsto_compose) (* TODO: delete? *) |
|
415 |
321 |
416 lemma metric_isCont_LIM_compose2: |
322 lemma metric_isCont_LIM_compose2: |
417 assumes f [unfolded isCont_def]: "isCont f a" |
323 assumes f [unfolded isCont_def]: "isCont f a" |
418 assumes g: "g -- f a --> l" |
324 assumes g: "g -- f a --> l" |
419 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a" |
325 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a" |
427 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a" |
333 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a" |
428 shows "(\<lambda>x. g (f x)) -- a --> l" |
334 shows "(\<lambda>x. g (f x)) -- a --> l" |
429 by (rule LIM_compose2 [OF f g inj]) |
335 by (rule LIM_compose2 [OF f g inj]) |
430 |
336 |
431 lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a" |
337 lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a" |
432 unfolding isCont_def by (rule LIM_compose) |
338 unfolding isCont_def by (rule tendsto_compose) |
433 |
339 |
434 lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a" |
340 lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a" |
435 unfolding o_def by (rule isCont_o2) |
341 unfolding o_def by (rule isCont_o2) |
436 |
342 |
437 lemma (in bounded_linear) isCont: |
343 lemma (in bounded_linear) isCont: |
438 "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a" |
344 "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a" |
439 unfolding isCont_def by (rule LIM) |
345 unfolding isCont_def by (rule tendsto) |
440 |
346 |
441 lemma (in bounded_bilinear) isCont: |
347 lemma (in bounded_bilinear) isCont: |
442 "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a" |
348 "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a" |
443 unfolding isCont_def by (rule LIM) |
349 unfolding isCont_def by (rule tendsto) |
444 |
350 |
445 lemmas isCont_scaleR [simp] = |
351 lemmas isCont_scaleR [simp] = |
446 bounded_bilinear.isCont [OF bounded_bilinear_scaleR] |
352 bounded_bilinear.isCont [OF bounded_bilinear_scaleR] |
447 |
353 |
448 lemmas isCont_of_real [simp] = |
354 lemmas isCont_of_real [simp] = |
449 bounded_linear.isCont [OF bounded_linear_of_real] |
355 bounded_linear.isCont [OF bounded_linear_of_real] |
450 |
356 |
451 lemma isCont_power [simp]: |
357 lemma isCont_power [simp]: |
452 fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}" |
358 fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}" |
453 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a" |
359 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a" |
454 unfolding isCont_def by (rule LIM_power) |
360 unfolding isCont_def by (rule tendsto_power) |
455 |
361 |
456 lemma isCont_sgn [simp]: |
362 lemma isCont_sgn [simp]: |
457 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
363 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
458 shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a" |
364 shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a" |
459 unfolding isCont_def by (rule LIM_sgn) |
365 unfolding isCont_def by (rule tendsto_sgn) |
460 |
366 |
461 lemma isCont_setsum [simp]: |
367 lemma isCont_setsum [simp]: |
462 fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector" |
368 fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector" |
463 fixes A :: "'a set" |
369 fixes A :: "'a set" |
464 shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a" |
370 shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a" |
582 lemma LIMSEQ_SEQ_conv: |
488 lemma LIMSEQ_SEQ_conv: |
583 "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = |
489 "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = |
584 (X -- a --> (L::'b::topological_space))" |
490 (X -- a --> (L::'b::topological_space))" |
585 using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 .. |
491 using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 .. |
586 |
492 |
|
493 subsection {* Legacy theorem names *} |
|
494 |
|
495 lemmas LIM_ident [simp] = tendsto_ident_at |
|
496 lemmas LIM_const [simp] = tendsto_const [where F="at x", standard] |
|
497 lemmas LIM_add = tendsto_add [where F="at x", standard] |
|
498 lemmas LIM_add_zero = tendsto_add_zero [where F="at x", standard] |
|
499 lemmas LIM_minus = tendsto_minus [where F="at x", standard] |
|
500 lemmas LIM_diff = tendsto_diff [where F="at x", standard] |
|
501 lemmas LIM_norm = tendsto_norm [where F="at x", standard] |
|
502 lemmas LIM_norm_zero = tendsto_norm_zero [where F="at x", standard] |
|
503 lemmas LIM_norm_zero_cancel = tendsto_norm_zero_cancel [where F="at x", standard] |
|
504 lemmas LIM_norm_zero_iff = tendsto_norm_zero_iff [where F="at x", standard] |
|
505 lemmas LIM_rabs = tendsto_rabs [where F="at x", standard] |
|
506 lemmas LIM_rabs_zero = tendsto_rabs_zero [where F="at x", standard] |
|
507 lemmas LIM_rabs_zero_cancel = tendsto_rabs_zero_cancel [where F="at x", standard] |
|
508 lemmas LIM_rabs_zero_iff = tendsto_rabs_zero_iff [where F="at x", standard] |
|
509 lemmas LIM_compose = tendsto_compose [where F="at x", standard] |
|
510 lemmas LIM_mult = tendsto_mult [where F="at x", standard] |
|
511 lemmas LIM_scaleR = tendsto_scaleR [where F="at x", standard] |
|
512 lemmas LIM_of_real = tendsto_of_real [where F="at x", standard] |
|
513 lemmas LIM_power = tendsto_power [where F="at x", standard] |
|
514 lemmas LIM_inverse = tendsto_inverse [where F="at x", standard] |
|
515 lemmas LIM_sgn = tendsto_sgn [where F="at x", standard] |
|
516 lemmas isCont_LIM_compose = isCont_tendsto_compose [where F="at x", standard] |
|
517 |
587 end |
518 end |