author | huffman |
Thu, 09 Nov 2006 00:19:16 +0100 | |
changeset 21257 | b7f090c5057d |
parent 21239 | d4fbe2c87ef1 |
child 21282 | dd647b4d7952 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : Lim.thy |
14477 | 2 |
ID : $Id$ |
10751 | 3 |
Author : Jacques D. Fleuriot |
4 |
Copyright : 1998 University of Cambridge |
|
14477 | 5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
10751 | 6 |
*) |
7 |
||
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
8 |
header{* Limits and Continuity *} |
10751 | 9 |
|
15131 | 10 |
theory Lim |
15360 | 11 |
imports SEQ |
15131 | 12 |
begin |
14477 | 13 |
|
14 |
text{*Standard and Nonstandard Definitions*} |
|
10751 | 15 |
|
19765 | 16 |
definition |
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
17 |
LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
18 |
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) |
19765 | 19 |
"f -- a --> L = |
20563 | 20 |
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s |
21 |
--> norm (f x - L) < r)" |
|
10751 | 22 |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
23 |
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
24 |
("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
25 |
"f -- a --NS> L = |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
26 |
(\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))" |
10751 | 27 |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
28 |
isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" |
19765 | 29 |
"isCont f a = (f -- a --> (f a))" |
10751 | 30 |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
31 |
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" |
15228 | 32 |
--{*NS definition dispenses with limit notions*} |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
33 |
"isNSCont f a = (\<forall>y. y @= star_of a --> |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
34 |
( *f* f) y @= star_of (f a))" |
10751 | 35 |
|
20752 | 36 |
isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" |
37 |
"isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)" |
|
10751 | 38 |
|
20752 | 39 |
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" |
19765 | 40 |
"isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)" |
10751 | 41 |
|
42 |
||
20755 | 43 |
subsection {* Limits of Functions *} |
14477 | 44 |
|
20755 | 45 |
subsubsection {* Purely standard proofs *} |
14477 | 46 |
|
47 |
lemma LIM_eq: |
|
48 |
"f -- a --> L = |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
49 |
(\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)" |
14477 | 50 |
by (simp add: LIM_def diff_minus) |
51 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
52 |
lemma LIM_I: |
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
53 |
"(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
54 |
==> f -- a --> L" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
55 |
by (simp add: LIM_eq) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
56 |
|
14477 | 57 |
lemma LIM_D: |
58 |
"[| f -- a --> L; 0<r |] |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
59 |
==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r" |
14477 | 60 |
by (simp add: LIM_eq) |
61 |
||
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
62 |
lemma LIM_offset: "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L" |
20756 | 63 |
apply (rule LIM_I) |
64 |
apply (drule_tac r="r" in LIM_D, safe) |
|
65 |
apply (rule_tac x="s" in exI, safe) |
|
66 |
apply (drule_tac x="x + k" in spec) |
|
67 |
apply (simp add: compare_rls) |
|
68 |
done |
|
69 |
||
21239 | 70 |
lemma LIM_offset_zero: "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L" |
71 |
by (drule_tac k="a" in LIM_offset, simp add: add_commute) |
|
72 |
||
73 |
lemma LIM_offset_zero_cancel: "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L" |
|
74 |
by (drule_tac k="- a" in LIM_offset, simp) |
|
75 |
||
15228 | 76 |
lemma LIM_const [simp]: "(%x. k) -- x --> k" |
14477 | 77 |
by (simp add: LIM_def) |
78 |
||
79 |
lemma LIM_add: |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
80 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
14477 | 81 |
assumes f: "f -- a --> L" and g: "g -- a --> M" |
82 |
shows "(%x. f x + g(x)) -- a --> (L + M)" |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
83 |
proof (rule LIM_I) |
14477 | 84 |
fix r :: real |
20409 | 85 |
assume r: "0 < r" |
14477 | 86 |
from LIM_D [OF f half_gt_zero [OF r]] |
87 |
obtain fs |
|
88 |
where fs: "0 < fs" |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
89 |
and fs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < fs --> norm (f x - L) < r/2" |
14477 | 90 |
by blast |
91 |
from LIM_D [OF g half_gt_zero [OF r]] |
|
92 |
obtain gs |
|
93 |
where gs: "0 < gs" |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
94 |
and gs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < gs --> norm (g x - M) < r/2" |
14477 | 95 |
by blast |
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
96 |
show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm (f x + g x - (L + M)) < r" |
14477 | 97 |
proof (intro exI conjI strip) |
98 |
show "0 < min fs gs" by (simp add: fs gs) |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
99 |
fix x :: 'a |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
100 |
assume "x \<noteq> a \<and> norm (x-a) < min fs gs" |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
101 |
hence "x \<noteq> a \<and> norm (x-a) < fs \<and> norm (x-a) < gs" by simp |
14477 | 102 |
with fs_lt gs_lt |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
103 |
have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+ |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
104 |
hence "norm (f x - L) + norm (g x - M) < r" by arith |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
105 |
thus "norm (f x + g x - (L + M)) < r" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
106 |
by (blast intro: norm_diff_triangle_ineq order_le_less_trans) |
14477 | 107 |
qed |
108 |
qed |
|
109 |
||
21257 | 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 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
114 |
lemma minus_diff_minus: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
115 |
fixes a b :: "'a::ab_group_add" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
116 |
shows "(- a) - (- b) = - (a - b)" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
117 |
by simp |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
118 |
|
14477 | 119 |
lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
120 |
by (simp only: LIM_eq minus_diff_minus norm_minus_cancel) |
14477 | 121 |
|
122 |
lemma LIM_add_minus: |
|
123 |
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)" |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
124 |
by (intro LIM_add LIM_minus) |
14477 | 125 |
|
126 |
lemma LIM_diff: |
|
127 |
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m" |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
128 |
by (simp only: diff_minus LIM_add LIM_minus) |
14477 | 129 |
|
21239 | 130 |
lemma LIM_zero: "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0" |
131 |
by (simp add: LIM_def) |
|
132 |
||
133 |
lemma LIM_zero_cancel: "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l" |
|
134 |
by (simp add: LIM_def) |
|
135 |
||
21257 | 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) |
|
154 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
155 |
lemma LIM_const_not_eq: |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
156 |
fixes a :: "'a::real_normed_div_algebra" |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
157 |
shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
158 |
apply (simp add: LIM_eq) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
159 |
apply (rule_tac x="norm (k - L)" in exI, simp, safe) |
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
160 |
apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
161 |
done |
14477 | 162 |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
163 |
lemma LIM_const_eq: |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
164 |
fixes a :: "'a::real_normed_div_algebra" |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
165 |
shows "(%x. k) -- a --> L ==> k = L" |
14477 | 166 |
apply (rule ccontr) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
167 |
apply (blast dest: LIM_const_not_eq) |
14477 | 168 |
done |
169 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
170 |
lemma LIM_unique: |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
171 |
fixes a :: "'a::real_normed_div_algebra" |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
172 |
shows "[| f -- a --> L; f -- a --> M |] ==> L = M" |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
173 |
apply (drule LIM_diff, assumption) |
14477 | 174 |
apply (auto dest!: LIM_const_eq) |
175 |
done |
|
176 |
||
177 |
lemma LIM_mult_zero: |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
178 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
14477 | 179 |
assumes f: "f -- a --> 0" and g: "g -- a --> 0" |
180 |
shows "(%x. f(x) * g(x)) -- a --> 0" |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
181 |
proof (rule LIM_I, simp) |
14477 | 182 |
fix r :: real |
183 |
assume r: "0<r" |
|
184 |
from LIM_D [OF f zero_less_one] |
|
185 |
obtain fs |
|
186 |
where fs: "0 < fs" |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
187 |
and fs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < fs --> norm (f x) < 1" |
14477 | 188 |
by auto |
189 |
from LIM_D [OF g r] |
|
190 |
obtain gs |
|
191 |
where gs: "0 < gs" |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
192 |
and gs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < gs --> norm (g x) < r" |
14477 | 193 |
by auto |
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
194 |
show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm (f x * g x) < r)" |
14477 | 195 |
proof (intro exI conjI strip) |
196 |
show "0 < min fs gs" by (simp add: fs gs) |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
197 |
fix x :: 'a |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
198 |
assume "x \<noteq> a \<and> norm (x-a) < min fs gs" |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
199 |
hence "x \<noteq> a \<and> norm (x-a) < fs \<and> norm (x-a) < gs" by simp |
14477 | 200 |
with fs_lt gs_lt |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
201 |
have "norm (f x) < 1" and "norm (g x) < r" by blast+ |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
202 |
hence "norm (f x) * norm (g x) < 1*r" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
203 |
by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero]) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
204 |
thus "norm (f x * g x) < r" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
205 |
by (simp add: order_le_less_trans [OF norm_mult_ineq]) |
14477 | 206 |
qed |
207 |
qed |
|
208 |
||
209 |
lemma LIM_self: "(%x. x) -- a --> a" |
|
210 |
by (auto simp add: LIM_def) |
|
211 |
||
212 |
text{*Limits are equal for functions equal except at limit point*} |
|
213 |
lemma LIM_equal: |
|
214 |
"[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)" |
|
215 |
by (simp add: LIM_def) |
|
216 |
||
20796 | 217 |
lemma LIM_cong: |
218 |
"\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk> |
|
219 |
\<Longrightarrow> (f -- a --> l) = (g -- b --> m)" |
|
220 |
by (simp add: LIM_def) |
|
221 |
||
14477 | 222 |
text{*Two uses in Hyperreal/Transcendental.ML*} |
223 |
lemma LIM_trans: |
|
224 |
"[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l" |
|
225 |
apply (drule LIM_add, assumption) |
|
226 |
apply (auto simp add: add_assoc) |
|
227 |
done |
|
228 |
||
21239 | 229 |
lemma LIM_compose: |
230 |
assumes g: "g -- l --> g l" |
|
231 |
assumes f: "f -- a --> l" |
|
232 |
shows "(\<lambda>x. g (f x)) -- a --> g l" |
|
233 |
proof (rule LIM_I) |
|
234 |
fix r::real assume r: "0 < r" |
|
235 |
obtain s where s: "0 < s" |
|
236 |
and less_r: "\<And>y. \<lbrakk>y \<noteq> l; norm (y - l) < s\<rbrakk> \<Longrightarrow> norm (g y - g l) < r" |
|
237 |
using LIM_D [OF g r] by fast |
|
238 |
obtain t where t: "0 < t" |
|
239 |
and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (f x - l) < s" |
|
240 |
using LIM_D [OF f s] by fast |
|
241 |
||
242 |
show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < t \<longrightarrow> norm (g (f x) - g l) < r" |
|
243 |
proof (rule exI, safe) |
|
244 |
show "0 < t" using t . |
|
245 |
next |
|
246 |
fix x assume "x \<noteq> a" and "norm (x - a) < t" |
|
247 |
hence "norm (f x - l) < s" by (rule less_s) |
|
248 |
thus "norm (g (f x) - g l) < r" |
|
249 |
using r less_r by (case_tac "f x = l", simp_all) |
|
250 |
qed |
|
251 |
qed |
|
252 |
||
253 |
lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l" |
|
254 |
unfolding o_def by (rule LIM_compose) |
|
255 |
||
20755 | 256 |
subsubsection {* Purely nonstandard proofs *} |
14477 | 257 |
|
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
258 |
lemma NSLIM_I: |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
259 |
"(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
260 |
\<Longrightarrow> f -- a --NS> L" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
261 |
by (simp add: NSLIM_def) |
14477 | 262 |
|
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
263 |
lemma NSLIM_D: |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
264 |
"\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
265 |
\<Longrightarrow> starfun f x \<approx> star_of L" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
266 |
by (simp add: NSLIM_def) |
14477 | 267 |
|
20755 | 268 |
text{*Proving properties of limits using nonstandard definition. |
269 |
The properties hold for standard limits as well!*} |
|
270 |
||
271 |
lemma NSLIM_mult: |
|
272 |
fixes l m :: "'a::real_normed_algebra" |
|
273 |
shows "[| f -- x --NS> l; g -- x --NS> m |] |
|
274 |
==> (%x. f(x) * g(x)) -- x --NS> (l * m)" |
|
275 |
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite) |
|
276 |
||
20794 | 277 |
lemma starfun_scaleR [simp]: |
278 |
"starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))" |
|
279 |
by transfer (rule refl) |
|
280 |
||
281 |
lemma NSLIM_scaleR: |
|
282 |
"[| f -- x --NS> l; g -- x --NS> m |] |
|
283 |
==> (%x. f(x) *# g(x)) -- x --NS> (l *# m)" |
|
284 |
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite) |
|
285 |
||
20755 | 286 |
lemma NSLIM_add: |
287 |
"[| f -- x --NS> l; g -- x --NS> m |] |
|
288 |
==> (%x. f(x) + g(x)) -- x --NS> (l + m)" |
|
289 |
by (auto simp add: NSLIM_def intro!: approx_add) |
|
290 |
||
291 |
lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k" |
|
292 |
by (simp add: NSLIM_def) |
|
293 |
||
294 |
lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L" |
|
295 |
by (simp add: NSLIM_def) |
|
296 |
||
297 |
lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)" |
|
298 |
by (simp only: NSLIM_add NSLIM_minus) |
|
299 |
||
300 |
lemma NSLIM_inverse: |
|
301 |
fixes L :: "'a::real_normed_div_algebra" |
|
302 |
shows "[| f -- a --NS> L; L \<noteq> 0 |] |
|
303 |
==> (%x. inverse(f(x))) -- a --NS> (inverse L)" |
|
304 |
apply (simp add: NSLIM_def, clarify) |
|
305 |
apply (drule spec) |
|
306 |
apply (auto simp add: star_of_approx_inverse) |
|
307 |
done |
|
308 |
||
309 |
lemma NSLIM_zero: |
|
310 |
assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0" |
|
311 |
proof - |
|
312 |
have "(\<lambda>x. f x + - l) -- a --NS> l + -l" |
|
313 |
by (rule NSLIM_add_minus [OF f NSLIM_const]) |
|
314 |
thus ?thesis by simp |
|
315 |
qed |
|
316 |
||
317 |
lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l" |
|
318 |
apply (drule_tac g = "%x. l" and m = l in NSLIM_add) |
|
319 |
apply (auto simp add: diff_minus add_assoc) |
|
320 |
done |
|
321 |
||
322 |
lemma NSLIM_const_not_eq: |
|
323 |
fixes a :: real (* TODO: generalize to real_normed_div_algebra *) |
|
324 |
shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)" |
|
325 |
apply (simp add: NSLIM_def) |
|
326 |
apply (rule_tac x="star_of a + epsilon" in exI) |
|
327 |
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] |
|
328 |
simp add: hypreal_epsilon_not_zero) |
|
329 |
done |
|
330 |
||
331 |
lemma NSLIM_not_zero: |
|
332 |
fixes a :: real |
|
333 |
shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)" |
|
334 |
by (rule NSLIM_const_not_eq) |
|
335 |
||
336 |
lemma NSLIM_const_eq: |
|
337 |
fixes a :: real |
|
338 |
shows "(%x. k) -- a --NS> L ==> k = L" |
|
339 |
apply (rule ccontr) |
|
340 |
apply (blast dest: NSLIM_const_not_eq) |
|
341 |
done |
|
342 |
||
343 |
text{* can actually be proved more easily by unfolding the definition!*} |
|
344 |
lemma NSLIM_unique: |
|
345 |
fixes a :: real |
|
346 |
shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M" |
|
347 |
apply (drule NSLIM_minus) |
|
348 |
apply (drule NSLIM_add, assumption) |
|
349 |
apply (auto dest!: NSLIM_const_eq [symmetric]) |
|
350 |
apply (simp add: diff_def [symmetric]) |
|
351 |
done |
|
352 |
||
353 |
lemma NSLIM_mult_zero: |
|
354 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
|
355 |
shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0" |
|
356 |
by (drule NSLIM_mult, auto) |
|
357 |
||
358 |
lemma NSLIM_self: "(%x. x) -- a --NS> a" |
|
359 |
by (simp add: NSLIM_def) |
|
360 |
||
361 |
subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *} |
|
362 |
||
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
363 |
lemma LIM_NSLIM: |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
364 |
assumes f: "f -- a --> L" shows "f -- a --NS> L" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
365 |
proof (rule NSLIM_I) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
366 |
fix x |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
367 |
assume neq: "x \<noteq> star_of a" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
368 |
assume approx: "x \<approx> star_of a" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
369 |
have "starfun f x - star_of L \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
370 |
proof (rule InfinitesimalI2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
371 |
fix r::real assume r: "0 < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
372 |
from LIM_D [OF f r] |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
373 |
obtain s where s: "0 < s" and |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
374 |
less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
375 |
by fast |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
376 |
from less_r have less_r': |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
377 |
"\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk> |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
378 |
\<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
379 |
by transfer |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
380 |
from approx have "x - star_of a \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
381 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
382 |
hence "hnorm (x - star_of a) < star_of s" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
383 |
using s by (rule InfinitesimalD2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
384 |
with neq show "hnorm (starfun f x - star_of L) < star_of r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
385 |
by (rule less_r') |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
386 |
qed |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
387 |
thus "starfun f x \<approx> star_of L" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
388 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
389 |
qed |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
390 |
|
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
391 |
lemma NSLIM_LIM: |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
392 |
assumes f: "f -- a --NS> L" shows "f -- a --> L" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
393 |
proof (rule LIM_I) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
394 |
fix r::real assume r: "0 < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
395 |
have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
396 |
\<longrightarrow> hnorm (starfun f x - star_of L) < star_of r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
397 |
proof (rule exI, safe) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
398 |
show "0 < epsilon" by (rule hypreal_epsilon_gt_zero) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
399 |
next |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
400 |
fix x assume neq: "x \<noteq> star_of a" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
401 |
assume "hnorm (x - star_of a) < epsilon" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
402 |
with Infinitesimal_epsilon |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
403 |
have "x - star_of a \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
404 |
by (rule hnorm_less_Infinitesimal) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
405 |
hence "x \<approx> star_of a" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
406 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
407 |
with f neq have "starfun f x \<approx> star_of L" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
408 |
by (rule NSLIM_D) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
409 |
hence "starfun f x - star_of L \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
410 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
411 |
thus "hnorm (starfun f x - star_of L) < star_of r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
412 |
using r by (rule InfinitesimalD2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
413 |
qed |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
414 |
thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
415 |
by transfer |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
416 |
qed |
14477 | 417 |
|
15228 | 418 |
theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)" |
14477 | 419 |
by (blast intro: LIM_NSLIM NSLIM_LIM) |
420 |
||
20755 | 421 |
subsubsection {* Derived theorems about @{term LIM} *} |
14477 | 422 |
|
15228 | 423 |
lemma LIM_mult2: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
424 |
fixes l m :: "'a::real_normed_algebra" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
425 |
shows "[| f -- x --> l; g -- x --> m |] |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
426 |
==> (%x. f(x) * g(x)) -- x --> (l * m)" |
14477 | 427 |
by (simp add: LIM_NSLIM_iff NSLIM_mult) |
428 |
||
20794 | 429 |
lemma LIM_scaleR: |
430 |
"[| f -- x --> l; g -- x --> m |] |
|
431 |
==> (%x. f(x) *# g(x)) -- x --> (l *# m)" |
|
432 |
by (simp add: LIM_NSLIM_iff NSLIM_scaleR) |
|
433 |
||
15228 | 434 |
lemma LIM_add2: |
435 |
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)" |
|
14477 | 436 |
by (simp add: LIM_NSLIM_iff NSLIM_add) |
437 |
||
438 |
lemma LIM_const2: "(%x. k) -- x --> k" |
|
439 |
by (simp add: LIM_NSLIM_iff) |
|
440 |
||
441 |
lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L" |
|
442 |
by (simp add: LIM_NSLIM_iff NSLIM_minus) |
|
443 |
||
444 |
lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)" |
|
445 |
by (simp add: LIM_NSLIM_iff NSLIM_add_minus) |
|
446 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
447 |
lemma LIM_inverse: |
20653
24cda2c5fd40
removed division_by_zero class requirements from several lemmas
huffman
parents:
20635
diff
changeset
|
448 |
fixes L :: "'a::real_normed_div_algebra" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
449 |
shows "[| f -- a --> L; L \<noteq> 0 |] |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
450 |
==> (%x. inverse(f(x))) -- a --> (inverse L)" |
14477 | 451 |
by (simp add: LIM_NSLIM_iff NSLIM_inverse) |
452 |
||
453 |
lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0" |
|
454 |
by (simp add: LIM_NSLIM_iff NSLIM_zero) |
|
455 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
456 |
lemma LIM_unique2: |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
457 |
fixes a :: real |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
458 |
shows "[| f -- a --> L; f -- a --> M |] ==> L = M" |
14477 | 459 |
by (simp add: LIM_NSLIM_iff NSLIM_unique) |
460 |
||
461 |
(* we can use the corresponding thm LIM_mult2 *) |
|
462 |
(* for standard definition of limit *) |
|
463 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
464 |
lemma LIM_mult_zero2: |
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
465 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
466 |
shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0" |
14477 | 467 |
by (drule LIM_mult2, auto) |
468 |
||
469 |
||
20755 | 470 |
subsection {* Continuity *} |
14477 | 471 |
|
21239 | 472 |
subsubsection {* Purely standard proofs *} |
473 |
||
474 |
lemma LIM_isCont_iff: "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)" |
|
475 |
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) |
|
476 |
||
477 |
lemma isCont_iff: "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x" |
|
478 |
by (simp add: isCont_def LIM_isCont_iff) |
|
479 |
||
480 |
lemma isCont_Id: "isCont (\<lambda>x. x) a" |
|
481 |
unfolding isCont_def by (rule LIM_self) |
|
482 |
||
483 |
lemma isCont_const [simp]: "isCont (%x. k) a" |
|
484 |
unfolding isCont_def by (rule LIM_const) |
|
485 |
||
486 |
lemma isCont_add: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a" |
|
487 |
unfolding isCont_def by (rule LIM_add) |
|
488 |
||
489 |
lemma isCont_minus: "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a" |
|
490 |
unfolding isCont_def by (rule LIM_minus) |
|
491 |
||
492 |
lemma isCont_diff: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a" |
|
493 |
unfolding isCont_def by (rule LIM_diff) |
|
494 |
||
495 |
lemma isCont_mult: |
|
496 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
|
497 |
shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a" |
|
498 |
unfolding isCont_def by (rule LIM_mult2) |
|
499 |
||
500 |
lemma isCont_inverse: |
|
501 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra" |
|
502 |
shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x" |
|
503 |
unfolding isCont_def by (rule LIM_inverse) |
|
504 |
||
505 |
lemma isCont_LIM_compose: |
|
506 |
"\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l" |
|
507 |
unfolding isCont_def by (rule LIM_compose) |
|
508 |
||
509 |
lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a" |
|
510 |
unfolding isCont_def by (rule LIM_compose) |
|
511 |
||
512 |
lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a" |
|
513 |
unfolding o_def by (rule isCont_o2) |
|
514 |
||
515 |
subsubsection {* Nonstandard proofs *} |
|
516 |
||
14477 | 517 |
lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)" |
518 |
by (simp add: isNSCont_def) |
|
519 |
||
520 |
lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) " |
|
521 |
by (simp add: isNSCont_def NSLIM_def) |
|
522 |
||
523 |
lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a" |
|
524 |
apply (simp add: isNSCont_def NSLIM_def, auto) |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
525 |
apply (case_tac "y = star_of a", auto) |
14477 | 526 |
done |
527 |
||
15228 | 528 |
text{*NS continuity can be defined using NS Limit in |
529 |
similar fashion to standard def of continuity*} |
|
14477 | 530 |
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))" |
531 |
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont) |
|
532 |
||
15228 | 533 |
text{*Hence, NS continuity can be given |
534 |
in terms of standard limit*} |
|
14477 | 535 |
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))" |
536 |
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff) |
|
537 |
||
15228 | 538 |
text{*Moreover, it's trivial now that NS continuity |
539 |
is equivalent to standard continuity*} |
|
14477 | 540 |
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)" |
541 |
apply (simp add: isCont_def) |
|
542 |
apply (rule isNSCont_LIM_iff) |
|
543 |
done |
|
544 |
||
15228 | 545 |
text{*Standard continuity ==> NS continuity*} |
14477 | 546 |
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a" |
547 |
by (erule isNSCont_isCont_iff [THEN iffD2]) |
|
548 |
||
15228 | 549 |
text{*NS continuity ==> Standard continuity*} |
14477 | 550 |
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a" |
551 |
by (erule isNSCont_isCont_iff [THEN iffD1]) |
|
552 |
||
553 |
text{*Alternative definition of continuity*} |
|
554 |
(* Prove equivalence between NS limits - *) |
|
555 |
(* seems easier than using standard def *) |
|
556 |
lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)" |
|
557 |
apply (simp add: NSLIM_def, auto) |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
558 |
apply (drule_tac x = "star_of a + x" in spec) |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
559 |
apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp) |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
560 |
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]]) |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
561 |
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1]) |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
562 |
prefer 2 apply (simp add: add_commute diff_def [symmetric]) |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
563 |
apply (rule_tac x = x in star_cases) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
564 |
apply (rule_tac [2] x = x in star_cases) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
565 |
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) |
14477 | 566 |
done |
567 |
||
568 |
lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)" |
|
569 |
by (rule NSLIM_h_iff) |
|
570 |
||
571 |
lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a" |
|
572 |
by (simp add: isNSCont_def) |
|
573 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
574 |
lemma isNSCont_inverse: |
20653
24cda2c5fd40
removed division_by_zero class requirements from several lemmas
huffman
parents:
20635
diff
changeset
|
575 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
576 |
shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x" |
14477 | 577 |
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff) |
578 |
||
15228 | 579 |
lemma isNSCont_const [simp]: "isNSCont (%x. k) a" |
14477 | 580 |
by (simp add: isNSCont_def) |
581 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
582 |
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" |
14477 | 583 |
apply (simp add: isNSCont_def) |
584 |
apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs) |
|
585 |
done |
|
586 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
587 |
lemma isCont_abs [simp]: "isCont abs (a::real)" |
14477 | 588 |
by (auto simp add: isNSCont_isCont_iff [symmetric]) |
15228 | 589 |
|
14477 | 590 |
|
591 |
(**************************************************************** |
|
592 |
(%* Leave as commented until I add topology theory or remove? *%) |
|
593 |
(%*------------------------------------------------------------ |
|
594 |
Elementary topology proof for a characterisation of |
|
595 |
continuity now: a function f is continuous if and only |
|
596 |
if the inverse image, {x. f(x) \<in> A}, of any open set A |
|
597 |
is always an open set |
|
598 |
------------------------------------------------------------*%) |
|
599 |
Goal "[| isNSopen A; \<forall>x. isNSCont f x |] |
|
600 |
==> isNSopen {x. f x \<in> A}" |
|
601 |
by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); |
|
602 |
by (dtac (mem_monad_approx RS approx_sym); |
|
603 |
by (dres_inst_tac [("x","a")] spec 1); |
|
604 |
by (dtac isNSContD 1 THEN assume_tac 1) |
|
605 |
by (dtac bspec 1 THEN assume_tac 1) |
|
606 |
by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1); |
|
607 |
by (blast_tac (claset() addIs [starfun_mem_starset]); |
|
608 |
qed "isNSCont_isNSopen"; |
|
609 |
||
610 |
Goalw [isNSCont_def] |
|
611 |
"\<forall>A. isNSopen A --> isNSopen {x. f x \<in> A} \ |
|
612 |
\ ==> isNSCont f x"; |
|
613 |
by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS |
|
614 |
(approx_minus_iff RS iffD2)],simpset() addsimps |
|
615 |
[Infinitesimal_def,SReal_iff])); |
|
616 |
by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1); |
|
617 |
by (etac (isNSopen_open_interval RSN (2,impE)); |
|
618 |
by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def])); |
|
619 |
by (dres_inst_tac [("x","x")] spec 1); |
|
620 |
by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad], |
|
621 |
simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus])); |
|
622 |
qed "isNSopen_isNSCont"; |
|
623 |
||
624 |
Goal "(\<forall>x. isNSCont f x) = \ |
|
625 |
\ (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})"; |
|
626 |
by (blast_tac (claset() addIs [isNSCont_isNSopen, |
|
627 |
isNSopen_isNSCont]); |
|
628 |
qed "isNSCont_isNSopen_iff"; |
|
629 |
||
630 |
(%*------- Standard version of same theorem --------*%) |
|
631 |
Goal "(\<forall>x. isCont f x) = \ |
|
632 |
\ (\<forall>A. isopen A --> isopen {x. f(x) \<in> A})"; |
|
633 |
by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff], |
|
634 |
simpset() addsimps [isNSopen_isopen_iff RS sym, |
|
635 |
isNSCont_isCont_iff RS sym])); |
|
636 |
qed "isCont_isopen_iff"; |
|
637 |
*******************************************************************) |
|
638 |
||
20755 | 639 |
subsection {* Uniform Continuity *} |
640 |
||
14477 | 641 |
lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y" |
642 |
by (simp add: isNSUCont_def) |
|
643 |
||
644 |
lemma isUCont_isCont: "isUCont f ==> isCont f x" |
|
645 |
by (simp add: isUCont_def isCont_def LIM_def, meson) |
|
646 |
||
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
647 |
lemma isUCont_isNSUCont: |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
648 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
649 |
assumes f: "isUCont f" shows "isNSUCont f" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
650 |
proof (unfold isNSUCont_def, safe) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
651 |
fix x y :: "'a star" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
652 |
assume approx: "x \<approx> y" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
653 |
have "starfun f x - starfun f y \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
654 |
proof (rule InfinitesimalI2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
655 |
fix r::real assume r: "0 < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
656 |
with f obtain s where s: "0 < s" and |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
657 |
less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
658 |
by (auto simp add: isUCont_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
659 |
from less_r have less_r': |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
660 |
"\<And>x y. hnorm (x - y) < star_of s |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
661 |
\<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
662 |
by transfer |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
663 |
from approx have "x - y \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
664 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
665 |
hence "hnorm (x - y) < star_of s" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
666 |
using s by (rule InfinitesimalD2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
667 |
thus "hnorm (starfun f x - starfun f y) < star_of r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
668 |
by (rule less_r') |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
669 |
qed |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
670 |
thus "starfun f x \<approx> starfun f y" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
671 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
672 |
qed |
14477 | 673 |
|
674 |
lemma isNSUCont_isUCont: |
|
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
675 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
676 |
assumes f: "isNSUCont f" shows "isUCont f" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
677 |
proof (unfold isUCont_def, safe) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
678 |
fix r::real assume r: "0 < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
679 |
have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
680 |
\<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
681 |
proof (rule exI, safe) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
682 |
show "0 < epsilon" by (rule hypreal_epsilon_gt_zero) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
683 |
next |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
684 |
fix x y :: "'a star" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
685 |
assume "hnorm (x - y) < epsilon" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
686 |
with Infinitesimal_epsilon |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
687 |
have "x - y \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
688 |
by (rule hnorm_less_Infinitesimal) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
689 |
hence "x \<approx> y" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
690 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
691 |
with f have "starfun f x \<approx> starfun f y" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
692 |
by (simp add: isNSUCont_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
693 |
hence "starfun f x - starfun f y \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
694 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
695 |
thus "hnorm (starfun f x - starfun f y) < star_of r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
696 |
using r by (rule InfinitesimalD2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
697 |
qed |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
698 |
thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
699 |
by transfer |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
700 |
qed |
14477 | 701 |
|
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
702 |
subsection {* Relation of LIM and LIMSEQ *} |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
703 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
704 |
lemma LIMSEQ_SEQ_conv1: |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
705 |
fixes a :: "'a::real_normed_vector" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
706 |
assumes X: "X -- a --> L" |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
707 |
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
708 |
proof (safe intro!: LIMSEQ_I) |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
709 |
fix S :: "nat \<Rightarrow> 'a" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
710 |
fix r :: real |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
711 |
assume rgz: "0 < r" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
712 |
assume as: "\<forall>n. S n \<noteq> a" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
713 |
assume S: "S ----> a" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
714 |
from LIM_D [OF X rgz] obtain s |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
715 |
where sgz: "0 < s" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
716 |
and aux: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (X x - L) < r" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
717 |
by fast |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
718 |
from LIMSEQ_D [OF S sgz] |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
719 |
obtain no where "\<forall>n\<ge>no. norm (S n - a) < s" by fast |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
720 |
hence "\<forall>n\<ge>no. norm (X (S n) - L) < r" by (simp add: aux as) |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
721 |
thus "\<exists>no. \<forall>n\<ge>no. norm (X (S n) - L) < r" .. |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
722 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
723 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
724 |
lemma LIMSEQ_SEQ_conv2: |
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
725 |
fixes a :: real |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
726 |
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
727 |
shows "X -- a --> L" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
728 |
proof (rule ccontr) |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
729 |
assume "\<not> (X -- a --> L)" |
20563 | 730 |
hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> norm (X x - L) < r)" by (unfold LIM_def) |
731 |
hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> norm (X x - L) < r)" by simp |
|
732 |
hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r)" by (simp add: linorder_not_less) |
|
733 |
then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r))" by auto |
|
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
734 |
|
20563 | 735 |
let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r" |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
736 |
have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
737 |
using rdef by simp |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
738 |
hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n) - L) \<ge> r" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
739 |
by (rule someI_ex) |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
740 |
hence F1: "\<And>n. ?F n \<noteq> a" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
741 |
and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
742 |
and F3: "\<And>n. norm (X (?F n) - L) \<ge> r" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
743 |
by fast+ |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
744 |
|
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
745 |
have "?F ----> a" |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
746 |
proof (rule LIMSEQ_I, unfold real_norm_def) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
747 |
fix e::real |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
748 |
assume "0 < e" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
749 |
(* choose no such that inverse (real (Suc n)) < e *) |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
750 |
have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean) |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
751 |
then obtain m where nodef: "inverse (real (Suc m)) < e" by auto |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
752 |
show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
753 |
proof (intro exI allI impI) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
754 |
fix n |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
755 |
assume mlen: "m \<le> n" |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
756 |
have "\<bar>?F n - a\<bar> < inverse (real (Suc n))" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
757 |
by (rule F2) |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
758 |
also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))" |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
759 |
by auto |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
760 |
also from nodef have |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
761 |
"inverse (real (Suc m)) < e" . |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
762 |
finally show "\<bar>?F n - a\<bar> < e" . |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
763 |
qed |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
764 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
765 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
766 |
moreover have "\<forall>n. ?F n \<noteq> a" |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
767 |
by (rule allI) (rule F1) |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
768 |
|
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
769 |
moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
770 |
ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
771 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
772 |
moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
773 |
proof - |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
774 |
{ |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
775 |
fix no::nat |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
776 |
obtain n where "n = no + 1" by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
777 |
then have nolen: "no \<le> n" by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
778 |
(* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *) |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
779 |
have "norm (X (?F n) - L) \<ge> r" |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
780 |
by (rule F3) |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
781 |
with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r" by fast |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
782 |
} |
20563 | 783 |
then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp |
784 |
with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto |
|
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
785 |
thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less) |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
786 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
787 |
ultimately show False by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
788 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
789 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
790 |
lemma LIMSEQ_SEQ_conv: |
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
791 |
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
792 |
(X -- a --> L)" |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
793 |
proof |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
794 |
assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
795 |
show "X -- a --> L" by (rule LIMSEQ_SEQ_conv2) |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
796 |
next |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
797 |
assume "(X -- a --> L)" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
798 |
show "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1) |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
799 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
800 |
|
10751 | 801 |
end |