105 thus "norm (f x + g x - (L + M)) < r" |
105 thus "norm (f x + g x - (L + M)) < r" |
106 by (blast intro: norm_diff_triangle_ineq order_le_less_trans) |
106 by (blast intro: norm_diff_triangle_ineq order_le_less_trans) |
107 qed |
107 qed |
108 qed |
108 qed |
109 |
109 |
|
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 |
110 lemma minus_diff_minus: |
114 lemma minus_diff_minus: |
111 fixes a b :: "'a::ab_group_add" |
115 fixes a b :: "'a::ab_group_add" |
112 shows "(- a) - (- b) = - (a - b)" |
116 shows "(- a) - (- b) = - (a - b)" |
113 by simp |
117 by simp |
114 |
118 |
126 lemma LIM_zero: "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0" |
130 lemma LIM_zero: "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0" |
127 by (simp add: LIM_def) |
131 by (simp add: LIM_def) |
128 |
132 |
129 lemma LIM_zero_cancel: "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l" |
133 lemma LIM_zero_cancel: "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l" |
130 by (simp add: LIM_def) |
134 by (simp add: LIM_def) |
|
135 |
|
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) |
131 |
154 |
132 lemma LIM_const_not_eq: |
155 lemma LIM_const_not_eq: |
133 fixes a :: "'a::real_normed_div_algebra" |
156 fixes a :: "'a::real_normed_div_algebra" |
134 shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)" |
157 shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)" |
135 apply (simp add: LIM_eq) |
158 apply (simp add: LIM_eq) |