208 also have "g x \<le> f x" by (rule 2 [OF x]) |
208 also have "g x \<le> f x" by (rule 2 [OF x]) |
209 also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self) |
209 also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self) |
210 also have "\<bar>f x\<bar> = norm (f x - 0)" by simp |
210 also have "\<bar>f x\<bar> = norm (f x - 0)" by simp |
211 finally show "norm (g x - 0) \<le> norm (f x - 0)" . |
211 finally show "norm (g x - 0) \<le> norm (f x - 0)" . |
212 qed |
212 qed |
213 |
|
214 text {* Bounded Linear Operators *} |
|
215 |
|
216 lemma (in bounded_linear) LIM: |
|
217 "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l" |
|
218 by (rule tendsto) |
|
219 |
|
220 lemma (in bounded_linear) LIM_zero: |
|
221 "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0" |
|
222 by (rule tendsto_zero) |
|
223 |
|
224 text {* Bounded Bilinear Operators *} |
|
225 |
|
226 lemma (in bounded_bilinear) LIM: |
|
227 "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M" |
|
228 by (rule tendsto) |
|
229 |
|
230 lemma (in bounded_bilinear) LIM_prod_zero: |
|
231 fixes a :: "'d::metric_space" |
|
232 assumes f: "f -- a --> 0" |
|
233 assumes g: "g -- a --> 0" |
|
234 shows "(\<lambda>x. f x ** g x) -- a --> 0" |
|
235 using f g by (rule tendsto_zero) |
|
236 |
|
237 lemma (in bounded_bilinear) LIM_left_zero: |
|
238 "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0" |
|
239 by (rule tendsto_left_zero) |
|
240 |
|
241 lemma (in bounded_bilinear) LIM_right_zero: |
|
242 "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0" |
|
243 by (rule tendsto_right_zero) |
|
244 |
|
245 lemmas LIM_mult_zero = |
|
246 bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult] |
|
247 |
|
248 lemmas LIM_mult_left_zero = |
|
249 bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult] |
|
250 |
|
251 lemmas LIM_mult_right_zero = |
|
252 bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult] |
|
253 |
|
254 lemma LIM_inverse_fun: |
|
255 assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)" |
|
256 shows "inverse -- a --> inverse a" |
|
257 by (rule tendsto_inverse [OF tendsto_ident_at a]) |
|
258 |
213 |
259 |
214 |
260 subsection {* Continuity *} |
215 subsection {* Continuity *} |
261 |
216 |
262 lemma LIM_isCont_iff: |
217 lemma LIM_isCont_iff: |
493 lemma LIMSEQ_SEQ_conv: |
448 lemma LIMSEQ_SEQ_conv: |
494 "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = |
449 "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = |
495 (X -- a --> (L::'b::topological_space))" |
450 (X -- a --> (L::'b::topological_space))" |
496 using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 .. |
451 using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 .. |
497 |
452 |
498 subsection {* Legacy theorem names *} |
|
499 |
|
500 lemmas LIM_ident [simp] = tendsto_ident_at |
|
501 lemmas LIM_const [simp] = tendsto_const [where F="at x", standard] |
|
502 lemmas LIM_add = tendsto_add [where F="at x", standard] |
|
503 lemmas LIM_add_zero = tendsto_add_zero [where F="at x", standard] |
|
504 lemmas LIM_minus = tendsto_minus [where F="at x", standard] |
|
505 lemmas LIM_diff = tendsto_diff [where F="at x", standard] |
|
506 lemmas LIM_norm = tendsto_norm [where F="at x", standard] |
|
507 lemmas LIM_norm_zero = tendsto_norm_zero [where F="at x", standard] |
|
508 lemmas LIM_norm_zero_cancel = tendsto_norm_zero_cancel [where F="at x", standard] |
|
509 lemmas LIM_norm_zero_iff = tendsto_norm_zero_iff [where F="at x", standard] |
|
510 lemmas LIM_rabs = tendsto_rabs [where F="at x", standard] |
|
511 lemmas LIM_rabs_zero = tendsto_rabs_zero [where F="at x", standard] |
|
512 lemmas LIM_rabs_zero_cancel = tendsto_rabs_zero_cancel [where F="at x", standard] |
|
513 lemmas LIM_rabs_zero_iff = tendsto_rabs_zero_iff [where F="at x", standard] |
|
514 lemmas LIM_compose = tendsto_compose [where F="at x", standard] |
|
515 lemmas LIM_mult = tendsto_mult [where F="at x", standard] |
|
516 lemmas LIM_scaleR = tendsto_scaleR [where F="at x", standard] |
|
517 lemmas LIM_of_real = tendsto_of_real [where F="at x", standard] |
|
518 lemmas LIM_power = tendsto_power [where F="at x", standard] |
|
519 lemmas LIM_inverse = tendsto_inverse [where F="at x", standard] |
|
520 lemmas LIM_sgn = tendsto_sgn [where F="at x", standard] |
|
521 lemmas isCont_LIM_compose = isCont_tendsto_compose [where F="at x", standard] |
|
522 |
|
523 end |
453 end |