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