411 shows "(\<lambda>x. f x ^ n) -- a --> l ^ n" |
411 shows "(\<lambda>x. f x ^ n) -- a --> l ^ n" |
412 by (induct n, simp, simp add: LIM_mult f) |
412 by (induct n, simp, simp add: LIM_mult f) |
413 |
413 |
414 subsubsection {* Derived theorems about @{term LIM} *} |
414 subsubsection {* Derived theorems about @{term LIM} *} |
415 |
415 |
416 lemma LIM_inverse_lemma: |
416 lemma LIM_inverse: |
417 fixes x :: "'a::real_normed_div_algebra" |
417 fixes L :: "'a::real_normed_div_algebra" |
418 assumes r: "0 < r" |
418 shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L" |
419 assumes x: "norm (x - 1) < min (1/2) (r/2)" |
419 unfolding LIM_conv_tendsto |
420 shows "norm (inverse x - 1) < r" |
420 by (rule tendsto_inverse) |
421 proof - |
|
422 from r have r2: "0 < r/2" by simp |
|
423 from x have 0: "x \<noteq> 0" by clarsimp |
|
424 from x have x': "norm (1 - x) < min (1/2) (r/2)" |
|
425 by (simp only: norm_minus_commute) |
|
426 hence less1: "norm (1 - x) < r/2" by simp |
|
427 have "norm (1::'a) - norm x \<le> norm (1 - x)" by (rule norm_triangle_ineq2) |
|
428 also from x' have "norm (1 - x) < 1/2" by simp |
|
429 finally have "1/2 < norm x" by simp |
|
430 hence "inverse (norm x) < inverse (1/2)" |
|
431 by (rule less_imp_inverse_less, simp) |
|
432 hence less2: "norm (inverse x) < 2" |
|
433 by (simp add: nonzero_norm_inverse 0) |
|
434 from less1 less2 r2 norm_ge_zero |
|
435 have "norm (1 - x) * norm (inverse x) < (r/2) * 2" |
|
436 by (rule mult_strict_mono) |
|
437 thus "norm (inverse x - 1) < r" |
|
438 by (simp only: norm_mult [symmetric] left_diff_distrib, simp add: 0) |
|
439 qed |
|
440 |
421 |
441 lemma LIM_inverse_fun: |
422 lemma LIM_inverse_fun: |
442 assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)" |
423 assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)" |
443 shows "inverse -- a --> inverse a" |
424 shows "inverse -- a --> inverse a" |
444 proof (rule LIM_equal2) |
425 by (rule LIM_inverse [OF LIM_ident a]) |
445 from a show "0 < norm a" by simp |
|
446 next |
|
447 fix x assume "norm (x - a) < norm a" |
|
448 hence "x \<noteq> 0" by auto |
|
449 with a show "inverse x = inverse (inverse a * x) * inverse a" |
|
450 by (simp add: nonzero_inverse_mult_distrib |
|
451 nonzero_imp_inverse_nonzero |
|
452 nonzero_inverse_inverse_eq mult_assoc) |
|
453 next |
|
454 have 1: "inverse -- 1 --> inverse (1::'a)" |
|
455 apply (rule LIM_I) |
|
456 apply (rule_tac x="min (1/2) (r/2)" in exI) |
|
457 apply (simp add: LIM_inverse_lemma) |
|
458 done |
|
459 have "(\<lambda>x. inverse a * x) -- a --> inverse a * a" |
|
460 by (intro LIM_mult LIM_ident LIM_const) |
|
461 hence "(\<lambda>x. inverse a * x) -- a --> 1" |
|
462 by (simp add: a) |
|
463 with 1 have "(\<lambda>x. inverse (inverse a * x)) -- a --> inverse 1" |
|
464 by (rule LIM_compose) |
|
465 hence "(\<lambda>x. inverse (inverse a * x)) -- a --> 1" |
|
466 by simp |
|
467 hence "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> 1 * inverse a" |
|
468 by (intro LIM_mult LIM_const) |
|
469 thus "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> inverse a" |
|
470 by simp |
|
471 qed |
|
472 |
|
473 lemma LIM_inverse: |
|
474 fixes L :: "'a::real_normed_div_algebra" |
|
475 shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L" |
|
476 by (rule LIM_inverse_fun [THEN LIM_compose]) |
|
477 |
426 |
478 lemma LIM_sgn: |
427 lemma LIM_sgn: |
479 fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
428 fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
480 shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l" |
429 shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l" |
481 unfolding sgn_div_norm |
430 unfolding sgn_div_norm |