author | huffman |
Fri, 10 Nov 2006 00:46:00 +0100 | |
changeset 21282 | dd647b4d7952 |
parent 21257 | b7f090c5057d |
child 21399 | 700ae58d2273 |
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 |
||
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
222 |
lemma LIM_equal2: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
223 |
assumes 1: "0 < R" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
224 |
assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
225 |
shows "g -- a --> l \<Longrightarrow> f -- a --> l" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
226 |
apply (unfold LIM_def, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
227 |
apply (drule_tac x="r" in spec, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
228 |
apply (rule_tac x="min s R" in exI, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
229 |
apply (simp add: 1) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
230 |
apply (simp add: 2) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
231 |
done |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
232 |
|
14477 | 233 |
text{*Two uses in Hyperreal/Transcendental.ML*} |
234 |
lemma LIM_trans: |
|
235 |
"[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l" |
|
236 |
apply (drule LIM_add, assumption) |
|
237 |
apply (auto simp add: add_assoc) |
|
238 |
done |
|
239 |
||
21239 | 240 |
lemma LIM_compose: |
241 |
assumes g: "g -- l --> g l" |
|
242 |
assumes f: "f -- a --> l" |
|
243 |
shows "(\<lambda>x. g (f x)) -- a --> g l" |
|
244 |
proof (rule LIM_I) |
|
245 |
fix r::real assume r: "0 < r" |
|
246 |
obtain s where s: "0 < s" |
|
247 |
and less_r: "\<And>y. \<lbrakk>y \<noteq> l; norm (y - l) < s\<rbrakk> \<Longrightarrow> norm (g y - g l) < r" |
|
248 |
using LIM_D [OF g r] by fast |
|
249 |
obtain t where t: "0 < t" |
|
250 |
and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (f x - l) < s" |
|
251 |
using LIM_D [OF f s] by fast |
|
252 |
||
253 |
show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < t \<longrightarrow> norm (g (f x) - g l) < r" |
|
254 |
proof (rule exI, safe) |
|
255 |
show "0 < t" using t . |
|
256 |
next |
|
257 |
fix x assume "x \<noteq> a" and "norm (x - a) < t" |
|
258 |
hence "norm (f x - l) < s" by (rule less_s) |
|
259 |
thus "norm (g (f x) - g l) < r" |
|
260 |
using r less_r by (case_tac "f x = l", simp_all) |
|
261 |
qed |
|
262 |
qed |
|
263 |
||
264 |
lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l" |
|
265 |
unfolding o_def by (rule LIM_compose) |
|
266 |
||
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
267 |
lemma real_LIM_sandwich_zero: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
268 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> real" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
269 |
assumes f: "f -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
270 |
assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
271 |
assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
272 |
shows "g -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
273 |
proof (rule LIM_imp_LIM [OF f]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
274 |
fix x assume x: "x \<noteq> a" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
275 |
have "norm (g x - 0) = g x" by (simp add: 1 x) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
276 |
also have "g x \<le> f x" by (rule 2 [OF x]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
277 |
also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
278 |
also have "\<bar>f x\<bar> = norm (f x - 0)" by simp |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
279 |
finally show "norm (g x - 0) \<le> norm (f x - 0)" . |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
280 |
qed |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
281 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
282 |
subsubsection {* Bounded Linear Operators *} |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
283 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
284 |
locale bounded_linear = additive + |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
285 |
constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
286 |
assumes scaleR: "f (scaleR r x) = scaleR r (f x)" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
287 |
assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
288 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
289 |
lemma (in bounded_linear) pos_bounded: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
290 |
"\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
291 |
apply (cut_tac bounded, erule exE) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
292 |
apply (rule_tac x="max 1 K" in exI, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
293 |
apply (rule order_less_le_trans [OF zero_less_one le_maxI1]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
294 |
apply (drule spec, erule order_trans) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
295 |
apply (rule mult_left_mono [OF le_maxI2 norm_ge_zero]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
296 |
done |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
297 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
298 |
lemma (in bounded_linear) pos_boundedE: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
299 |
obtains K where "0 < K" and "\<forall>x. norm (f x) \<le> norm x * K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
300 |
using pos_bounded by fast |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
301 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
302 |
lemma (in bounded_linear) cont: "f -- a --> f a" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
303 |
proof (rule LIM_I) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
304 |
fix r::real assume r: "0 < r" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
305 |
obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
306 |
using pos_bounded by fast |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
307 |
show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - f a) < r" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
308 |
proof (rule exI, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
309 |
from r K show "0 < r / K" by (rule divide_pos_pos) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
310 |
next |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
311 |
fix x assume x: "norm (x - a) < r / K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
312 |
have "norm (f x - f a) = norm (f (x - a))" by (simp only: diff) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
313 |
also have "\<dots> \<le> norm (x - a) * K" by (rule norm_le) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
314 |
also from K x have "\<dots> < r" by (simp only: pos_less_divide_eq) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
315 |
finally show "norm (f x - f a) < r" . |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
316 |
qed |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
317 |
qed |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
318 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
319 |
lemma (in bounded_linear) LIM: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
320 |
"g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
321 |
by (rule LIM_compose [OF cont]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
322 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
323 |
lemma (in bounded_linear) LIM_zero: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
324 |
"g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
325 |
by (drule LIM, simp only: zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
326 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
327 |
subsubsection {* Bounded Bilinear Operators *} |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
328 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
329 |
locale bounded_bilinear = |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
330 |
fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector] |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
331 |
\<Rightarrow> 'c::real_normed_vector" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
332 |
(infixl "**" 70) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
333 |
assumes add_left: "prod (a + a') b = prod a b + prod a' b" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
334 |
assumes add_right: "prod a (b + b') = prod a b + prod a b'" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
335 |
assumes scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
336 |
assumes scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
337 |
assumes bounded: "\<exists>K. \<forall>a b. norm (prod a b) \<le> norm a * norm b * K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
338 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
339 |
lemma (in bounded_bilinear) pos_bounded: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
340 |
"\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
341 |
apply (cut_tac bounded, erule exE) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
342 |
apply (rule_tac x="max 1 K" in exI, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
343 |
apply (rule order_less_le_trans [OF zero_less_one le_maxI1]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
344 |
apply (drule spec, drule spec, erule order_trans) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
345 |
apply (rule mult_left_mono [OF le_maxI2]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
346 |
apply (intro mult_nonneg_nonneg norm_ge_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
347 |
done |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
348 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
349 |
lemma (in bounded_bilinear) additive_right: "additive (\<lambda>b. prod a b)" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
350 |
by (rule additive.intro, rule add_right) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
351 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
352 |
lemma (in bounded_bilinear) additive_left: "additive (\<lambda>a. prod a b)" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
353 |
by (rule additive.intro, rule add_left) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
354 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
355 |
lemma (in bounded_bilinear) zero_left: "prod 0 b = 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
356 |
by (rule additive.zero [OF additive_left]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
357 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
358 |
lemma (in bounded_bilinear) zero_right: "prod a 0 = 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
359 |
by (rule additive.zero [OF additive_right]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
360 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
361 |
lemma (in bounded_bilinear) minus_left: "prod (- a) b = - prod a b" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
362 |
by (rule additive.minus [OF additive_left]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
363 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
364 |
lemma (in bounded_bilinear) minus_right: "prod a (- b) = - prod a b" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
365 |
by (rule additive.minus [OF additive_right]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
366 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
367 |
lemma (in bounded_bilinear) diff_left: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
368 |
"prod (a - a') b = prod a b - prod a' b" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
369 |
by (rule additive.diff [OF additive_left]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
370 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
371 |
lemma (in bounded_bilinear) diff_right: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
372 |
"prod a (b - b') = prod a b - prod a b'" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
373 |
by (rule additive.diff [OF additive_right]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
374 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
375 |
lemma (in bounded_bilinear) LIM_prod_zero: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
376 |
assumes f: "f -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
377 |
assumes g: "g -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
378 |
shows "(\<lambda>x. f x ** g x) -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
379 |
proof (rule LIM_I) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
380 |
fix r::real assume r: "0 < r" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
381 |
obtain K where K: "0 < K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
382 |
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
383 |
using pos_bounded by fast |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
384 |
from K have K': "0 < inverse K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
385 |
by (rule positive_imp_inverse_positive) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
386 |
obtain s where s: "0 < s" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
387 |
and norm_f: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x) < r" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
388 |
using LIM_D [OF f r] by auto |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
389 |
obtain t where t: "0 < t" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
390 |
and norm_g: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (g x) < inverse K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
391 |
using LIM_D [OF g K'] by auto |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
392 |
show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x ** g x - 0) < r" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
393 |
proof (rule exI, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
394 |
from s t show "0 < min s t" by simp |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
395 |
next |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
396 |
fix x assume x: "x \<noteq> a" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
397 |
assume "norm (x - a) < min s t" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
398 |
hence xs: "norm (x - a) < s" and xt: "norm (x - a) < t" by simp_all |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
399 |
from x xs have 1: "norm (f x) < r" by (rule norm_f) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
400 |
from x xt have 2: "norm (g x) < inverse K" by (rule norm_g) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
401 |
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" by (rule norm_le) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
402 |
also from 1 2 K have "\<dots> < r * inverse K * K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
403 |
by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
404 |
also from K have "r * inverse K * K = r" by simp |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
405 |
finally show "norm (f x ** g x - 0) < r" by simp |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
406 |
qed |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
407 |
qed |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
408 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
409 |
lemma (in bounded_bilinear) bounded_linear_left: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
410 |
"bounded_linear (\<lambda>a. a ** b)" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
411 |
apply (unfold_locales) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
412 |
apply (rule add_left) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
413 |
apply (rule scaleR_left) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
414 |
apply (cut_tac bounded, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
415 |
apply (rule_tac x="norm b * K" in exI) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
416 |
apply (simp add: mult_ac) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
417 |
done |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
418 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
419 |
lemma (in bounded_bilinear) bounded_linear_right: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
420 |
"bounded_linear (\<lambda>b. a ** b)" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
421 |
apply (unfold_locales) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
422 |
apply (rule add_right) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
423 |
apply (rule scaleR_right) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
424 |
apply (cut_tac bounded, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
425 |
apply (rule_tac x="norm a * K" in exI) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
426 |
apply (simp add: mult_ac) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
427 |
done |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
428 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
429 |
lemma (in bounded_bilinear) LIM_left_zero: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
430 |
"f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
431 |
by (rule bounded_linear.LIM_zero [OF bounded_linear_left]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
432 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
433 |
lemma (in bounded_bilinear) LIM_right_zero: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
434 |
"f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
435 |
by (rule bounded_linear.LIM_zero [OF bounded_linear_right]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
436 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
437 |
lemma (in bounded_bilinear) prod_diff_prod: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
438 |
"(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
439 |
by (simp add: diff_left diff_right) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
440 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
441 |
lemma (in bounded_bilinear) LIM: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
442 |
"\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
443 |
apply (drule LIM_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
444 |
apply (drule LIM_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
445 |
apply (rule LIM_zero_cancel) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
446 |
apply (subst prod_diff_prod) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
447 |
apply (rule LIM_add_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
448 |
apply (rule LIM_add_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
449 |
apply (erule (1) LIM_prod_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
450 |
apply (erule LIM_left_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
451 |
apply (erule LIM_right_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
452 |
done |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
453 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
454 |
interpretation bounded_bilinear_mult: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
455 |
bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"] |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
456 |
apply (rule bounded_bilinear.intro) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
457 |
apply (rule left_distrib) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
458 |
apply (rule right_distrib) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
459 |
apply (rule mult_scaleR_left) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
460 |
apply (rule mult_scaleR_right) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
461 |
apply (rule_tac x="1" in exI) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
462 |
apply (simp add: norm_mult_ineq) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
463 |
done |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
464 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
465 |
interpretation bounded_bilinear_scaleR: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
466 |
bounded_bilinear ["scaleR"] |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
467 |
apply (rule bounded_bilinear.intro) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
468 |
apply (rule scaleR_left_distrib) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
469 |
apply (rule scaleR_right_distrib) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
470 |
apply (simp add: real_scaleR_def) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
471 |
apply (rule scaleR_left_commute) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
472 |
apply (rule_tac x="1" in exI) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
473 |
apply (simp add: norm_scaleR) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
474 |
done |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
475 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
476 |
lemmas LIM_mult = bounded_bilinear_mult.LIM |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
477 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
478 |
lemmas LIM_mult_zero = bounded_bilinear_mult.LIM_prod_zero |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
479 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
480 |
lemmas LIM_mult_left_zero = bounded_bilinear_mult.LIM_left_zero |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
481 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
482 |
lemmas LIM_mult_right_zero = bounded_bilinear_mult.LIM_right_zero |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
483 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
484 |
lemmas LIM_scaleR = bounded_bilinear_scaleR.LIM |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
485 |
|
20755 | 486 |
subsubsection {* Purely nonstandard proofs *} |
14477 | 487 |
|
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
488 |
lemma NSLIM_I: |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
489 |
"(\<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
|
490 |
\<Longrightarrow> f -- a --NS> L" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
491 |
by (simp add: NSLIM_def) |
14477 | 492 |
|
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
493 |
lemma NSLIM_D: |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
494 |
"\<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
|
495 |
\<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
|
496 |
by (simp add: NSLIM_def) |
14477 | 497 |
|
20755 | 498 |
text{*Proving properties of limits using nonstandard definition. |
499 |
The properties hold for standard limits as well!*} |
|
500 |
||
501 |
lemma NSLIM_mult: |
|
502 |
fixes l m :: "'a::real_normed_algebra" |
|
503 |
shows "[| f -- x --NS> l; g -- x --NS> m |] |
|
504 |
==> (%x. f(x) * g(x)) -- x --NS> (l * m)" |
|
505 |
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite) |
|
506 |
||
20794 | 507 |
lemma starfun_scaleR [simp]: |
508 |
"starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))" |
|
509 |
by transfer (rule refl) |
|
510 |
||
511 |
lemma NSLIM_scaleR: |
|
512 |
"[| f -- x --NS> l; g -- x --NS> m |] |
|
513 |
==> (%x. f(x) *# g(x)) -- x --NS> (l *# m)" |
|
514 |
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite) |
|
515 |
||
20755 | 516 |
lemma NSLIM_add: |
517 |
"[| f -- x --NS> l; g -- x --NS> m |] |
|
518 |
==> (%x. f(x) + g(x)) -- x --NS> (l + m)" |
|
519 |
by (auto simp add: NSLIM_def intro!: approx_add) |
|
520 |
||
521 |
lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k" |
|
522 |
by (simp add: NSLIM_def) |
|
523 |
||
524 |
lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L" |
|
525 |
by (simp add: NSLIM_def) |
|
526 |
||
527 |
lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)" |
|
528 |
by (simp only: NSLIM_add NSLIM_minus) |
|
529 |
||
530 |
lemma NSLIM_inverse: |
|
531 |
fixes L :: "'a::real_normed_div_algebra" |
|
532 |
shows "[| f -- a --NS> L; L \<noteq> 0 |] |
|
533 |
==> (%x. inverse(f(x))) -- a --NS> (inverse L)" |
|
534 |
apply (simp add: NSLIM_def, clarify) |
|
535 |
apply (drule spec) |
|
536 |
apply (auto simp add: star_of_approx_inverse) |
|
537 |
done |
|
538 |
||
539 |
lemma NSLIM_zero: |
|
540 |
assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0" |
|
541 |
proof - |
|
542 |
have "(\<lambda>x. f x + - l) -- a --NS> l + -l" |
|
543 |
by (rule NSLIM_add_minus [OF f NSLIM_const]) |
|
544 |
thus ?thesis by simp |
|
545 |
qed |
|
546 |
||
547 |
lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l" |
|
548 |
apply (drule_tac g = "%x. l" and m = l in NSLIM_add) |
|
549 |
apply (auto simp add: diff_minus add_assoc) |
|
550 |
done |
|
551 |
||
552 |
lemma NSLIM_const_not_eq: |
|
553 |
fixes a :: real (* TODO: generalize to real_normed_div_algebra *) |
|
554 |
shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)" |
|
555 |
apply (simp add: NSLIM_def) |
|
556 |
apply (rule_tac x="star_of a + epsilon" in exI) |
|
557 |
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] |
|
558 |
simp add: hypreal_epsilon_not_zero) |
|
559 |
done |
|
560 |
||
561 |
lemma NSLIM_not_zero: |
|
562 |
fixes a :: real |
|
563 |
shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)" |
|
564 |
by (rule NSLIM_const_not_eq) |
|
565 |
||
566 |
lemma NSLIM_const_eq: |
|
567 |
fixes a :: real |
|
568 |
shows "(%x. k) -- a --NS> L ==> k = L" |
|
569 |
apply (rule ccontr) |
|
570 |
apply (blast dest: NSLIM_const_not_eq) |
|
571 |
done |
|
572 |
||
573 |
text{* can actually be proved more easily by unfolding the definition!*} |
|
574 |
lemma NSLIM_unique: |
|
575 |
fixes a :: real |
|
576 |
shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M" |
|
577 |
apply (drule NSLIM_minus) |
|
578 |
apply (drule NSLIM_add, assumption) |
|
579 |
apply (auto dest!: NSLIM_const_eq [symmetric]) |
|
580 |
apply (simp add: diff_def [symmetric]) |
|
581 |
done |
|
582 |
||
583 |
lemma NSLIM_mult_zero: |
|
584 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
|
585 |
shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0" |
|
586 |
by (drule NSLIM_mult, auto) |
|
587 |
||
588 |
lemma NSLIM_self: "(%x. x) -- a --NS> a" |
|
589 |
by (simp add: NSLIM_def) |
|
590 |
||
591 |
subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *} |
|
592 |
||
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
593 |
lemma LIM_NSLIM: |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
594 |
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
|
595 |
proof (rule NSLIM_I) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
596 |
fix x |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
597 |
assume neq: "x \<noteq> star_of a" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
598 |
assume approx: "x \<approx> star_of a" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
599 |
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
|
600 |
proof (rule InfinitesimalI2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
601 |
fix r::real assume r: "0 < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
602 |
from LIM_D [OF f r] |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
603 |
obtain s where s: "0 < s" and |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
604 |
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
|
605 |
by fast |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
606 |
from less_r have less_r': |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
607 |
"\<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
|
608 |
\<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
|
609 |
by transfer |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
610 |
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
|
611 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
612 |
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
|
613 |
using s by (rule InfinitesimalD2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
614 |
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
|
615 |
by (rule less_r') |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
616 |
qed |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
617 |
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
|
618 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
619 |
qed |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
620 |
|
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
621 |
lemma NSLIM_LIM: |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
622 |
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
|
623 |
proof (rule LIM_I) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
624 |
fix r::real assume r: "0 < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
625 |
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
|
626 |
\<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
|
627 |
proof (rule exI, safe) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
628 |
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
|
629 |
next |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
630 |
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
|
631 |
assume "hnorm (x - star_of a) < epsilon" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
632 |
with Infinitesimal_epsilon |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
633 |
have "x - star_of a \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
634 |
by (rule hnorm_less_Infinitesimal) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
635 |
hence "x \<approx> star_of a" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
636 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
637 |
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
|
638 |
by (rule NSLIM_D) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
639 |
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
|
640 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
641 |
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
|
642 |
using r by (rule InfinitesimalD2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
643 |
qed |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
644 |
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
|
645 |
by transfer |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
646 |
qed |
14477 | 647 |
|
15228 | 648 |
theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)" |
14477 | 649 |
by (blast intro: LIM_NSLIM NSLIM_LIM) |
650 |
||
20755 | 651 |
subsubsection {* Derived theorems about @{term LIM} *} |
14477 | 652 |
|
15228 | 653 |
lemma LIM_mult2: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
654 |
fixes l m :: "'a::real_normed_algebra" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
655 |
shows "[| f -- x --> l; g -- x --> m |] |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
656 |
==> (%x. f(x) * g(x)) -- x --> (l * m)" |
14477 | 657 |
by (simp add: LIM_NSLIM_iff NSLIM_mult) |
658 |
||
20794 | 659 |
lemma LIM_scaleR: |
660 |
"[| f -- x --> l; g -- x --> m |] |
|
661 |
==> (%x. f(x) *# g(x)) -- x --> (l *# m)" |
|
662 |
by (simp add: LIM_NSLIM_iff NSLIM_scaleR) |
|
663 |
||
15228 | 664 |
lemma LIM_add2: |
665 |
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)" |
|
14477 | 666 |
by (simp add: LIM_NSLIM_iff NSLIM_add) |
667 |
||
668 |
lemma LIM_const2: "(%x. k) -- x --> k" |
|
669 |
by (simp add: LIM_NSLIM_iff) |
|
670 |
||
671 |
lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L" |
|
672 |
by (simp add: LIM_NSLIM_iff NSLIM_minus) |
|
673 |
||
674 |
lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)" |
|
675 |
by (simp add: LIM_NSLIM_iff NSLIM_add_minus) |
|
676 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
677 |
lemma LIM_inverse: |
20653
24cda2c5fd40
removed division_by_zero class requirements from several lemmas
huffman
parents:
20635
diff
changeset
|
678 |
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
|
679 |
shows "[| f -- a --> L; L \<noteq> 0 |] |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
680 |
==> (%x. inverse(f(x))) -- a --> (inverse L)" |
14477 | 681 |
by (simp add: LIM_NSLIM_iff NSLIM_inverse) |
682 |
||
683 |
lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0" |
|
684 |
by (simp add: LIM_NSLIM_iff NSLIM_zero) |
|
685 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
686 |
lemma LIM_unique2: |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
687 |
fixes a :: real |
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
688 |
shows "[| f -- a --> L; f -- a --> M |] ==> L = M" |
14477 | 689 |
by (simp add: LIM_NSLIM_iff NSLIM_unique) |
690 |
||
691 |
(* we can use the corresponding thm LIM_mult2 *) |
|
692 |
(* for standard definition of limit *) |
|
693 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
694 |
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
|
695 |
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
|
696 |
shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0" |
14477 | 697 |
by (drule LIM_mult2, auto) |
698 |
||
699 |
||
20755 | 700 |
subsection {* Continuity *} |
14477 | 701 |
|
21239 | 702 |
subsubsection {* Purely standard proofs *} |
703 |
||
704 |
lemma LIM_isCont_iff: "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)" |
|
705 |
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) |
|
706 |
||
707 |
lemma isCont_iff: "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x" |
|
708 |
by (simp add: isCont_def LIM_isCont_iff) |
|
709 |
||
710 |
lemma isCont_Id: "isCont (\<lambda>x. x) a" |
|
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
711 |
unfolding isCont_def by (rule LIM_self) |
21239 | 712 |
|
713 |
lemma isCont_const [simp]: "isCont (%x. k) a" |
|
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
714 |
unfolding isCont_def by (rule LIM_const) |
21239 | 715 |
|
716 |
lemma isCont_add: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a" |
|
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
717 |
unfolding isCont_def by (rule LIM_add) |
21239 | 718 |
|
719 |
lemma isCont_minus: "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a" |
|
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
720 |
unfolding isCont_def by (rule LIM_minus) |
21239 | 721 |
|
722 |
lemma isCont_diff: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a" |
|
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
723 |
unfolding isCont_def by (rule LIM_diff) |
21239 | 724 |
|
725 |
lemma isCont_mult: |
|
726 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
|
727 |
shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a" |
|
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
728 |
unfolding isCont_def by (rule LIM_mult) |
21239 | 729 |
|
730 |
lemma isCont_inverse: |
|
731 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra" |
|
732 |
shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x" |
|
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
733 |
unfolding isCont_def by (rule LIM_inverse) |
21239 | 734 |
|
735 |
lemma isCont_LIM_compose: |
|
736 |
"\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l" |
|
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
737 |
unfolding isCont_def by (rule LIM_compose) |
21239 | 738 |
|
739 |
lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a" |
|
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
740 |
unfolding isCont_def by (rule LIM_compose) |
21239 | 741 |
|
742 |
lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a" |
|
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
743 |
unfolding o_def by (rule isCont_o2) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
744 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
745 |
lemma (in bounded_linear) isCont: "isCont f a" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
746 |
unfolding isCont_def by (rule cont) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
747 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
748 |
lemma (in bounded_bilinear) isCont: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
749 |
"\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
750 |
unfolding isCont_def by (rule LIM) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
751 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
752 |
lemmas isCont_scaleR = bounded_bilinear_scaleR.isCont |
21239 | 753 |
|
754 |
subsubsection {* Nonstandard proofs *} |
|
755 |
||
14477 | 756 |
lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)" |
757 |
by (simp add: isNSCont_def) |
|
758 |
||
759 |
lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) " |
|
760 |
by (simp add: isNSCont_def NSLIM_def) |
|
761 |
||
762 |
lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a" |
|
763 |
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
|
764 |
apply (case_tac "y = star_of a", auto) |
14477 | 765 |
done |
766 |
||
15228 | 767 |
text{*NS continuity can be defined using NS Limit in |
768 |
similar fashion to standard def of continuity*} |
|
14477 | 769 |
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))" |
770 |
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont) |
|
771 |
||
15228 | 772 |
text{*Hence, NS continuity can be given |
773 |
in terms of standard limit*} |
|
14477 | 774 |
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))" |
775 |
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff) |
|
776 |
||
15228 | 777 |
text{*Moreover, it's trivial now that NS continuity |
778 |
is equivalent to standard continuity*} |
|
14477 | 779 |
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)" |
780 |
apply (simp add: isCont_def) |
|
781 |
apply (rule isNSCont_LIM_iff) |
|
782 |
done |
|
783 |
||
15228 | 784 |
text{*Standard continuity ==> NS continuity*} |
14477 | 785 |
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a" |
786 |
by (erule isNSCont_isCont_iff [THEN iffD2]) |
|
787 |
||
15228 | 788 |
text{*NS continuity ==> Standard continuity*} |
14477 | 789 |
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a" |
790 |
by (erule isNSCont_isCont_iff [THEN iffD1]) |
|
791 |
||
792 |
text{*Alternative definition of continuity*} |
|
793 |
(* Prove equivalence between NS limits - *) |
|
794 |
(* seems easier than using standard def *) |
|
795 |
lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)" |
|
796 |
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
|
797 |
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
|
798 |
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
|
799 |
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
|
800 |
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
|
801 |
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
|
802 |
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
|
803 |
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
|
804 |
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) |
14477 | 805 |
done |
806 |
||
807 |
lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)" |
|
808 |
by (rule NSLIM_h_iff) |
|
809 |
||
810 |
lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a" |
|
811 |
by (simp add: isNSCont_def) |
|
812 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
813 |
lemma isNSCont_inverse: |
20653
24cda2c5fd40
removed division_by_zero class requirements from several lemmas
huffman
parents:
20635
diff
changeset
|
814 |
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
|
815 |
shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x" |
14477 | 816 |
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff) |
817 |
||
15228 | 818 |
lemma isNSCont_const [simp]: "isNSCont (%x. k) a" |
14477 | 819 |
by (simp add: isNSCont_def) |
820 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
821 |
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" |
14477 | 822 |
apply (simp add: isNSCont_def) |
823 |
apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs) |
|
824 |
done |
|
825 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
826 |
lemma isCont_abs [simp]: "isCont abs (a::real)" |
14477 | 827 |
by (auto simp add: isNSCont_isCont_iff [symmetric]) |
15228 | 828 |
|
14477 | 829 |
|
830 |
(**************************************************************** |
|
831 |
(%* Leave as commented until I add topology theory or remove? *%) |
|
832 |
(%*------------------------------------------------------------ |
|
833 |
Elementary topology proof for a characterisation of |
|
834 |
continuity now: a function f is continuous if and only |
|
835 |
if the inverse image, {x. f(x) \<in> A}, of any open set A |
|
836 |
is always an open set |
|
837 |
------------------------------------------------------------*%) |
|
838 |
Goal "[| isNSopen A; \<forall>x. isNSCont f x |] |
|
839 |
==> isNSopen {x. f x \<in> A}" |
|
840 |
by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); |
|
841 |
by (dtac (mem_monad_approx RS approx_sym); |
|
842 |
by (dres_inst_tac [("x","a")] spec 1); |
|
843 |
by (dtac isNSContD 1 THEN assume_tac 1) |
|
844 |
by (dtac bspec 1 THEN assume_tac 1) |
|
845 |
by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1); |
|
846 |
by (blast_tac (claset() addIs [starfun_mem_starset]); |
|
847 |
qed "isNSCont_isNSopen"; |
|
848 |
||
849 |
Goalw [isNSCont_def] |
|
850 |
"\<forall>A. isNSopen A --> isNSopen {x. f x \<in> A} \ |
|
851 |
\ ==> isNSCont f x"; |
|
852 |
by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS |
|
853 |
(approx_minus_iff RS iffD2)],simpset() addsimps |
|
854 |
[Infinitesimal_def,SReal_iff])); |
|
855 |
by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1); |
|
856 |
by (etac (isNSopen_open_interval RSN (2,impE)); |
|
857 |
by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def])); |
|
858 |
by (dres_inst_tac [("x","x")] spec 1); |
|
859 |
by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad], |
|
860 |
simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus])); |
|
861 |
qed "isNSopen_isNSCont"; |
|
862 |
||
863 |
Goal "(\<forall>x. isNSCont f x) = \ |
|
864 |
\ (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})"; |
|
865 |
by (blast_tac (claset() addIs [isNSCont_isNSopen, |
|
866 |
isNSopen_isNSCont]); |
|
867 |
qed "isNSCont_isNSopen_iff"; |
|
868 |
||
869 |
(%*------- Standard version of same theorem --------*%) |
|
870 |
Goal "(\<forall>x. isCont f x) = \ |
|
871 |
\ (\<forall>A. isopen A --> isopen {x. f(x) \<in> A})"; |
|
872 |
by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff], |
|
873 |
simpset() addsimps [isNSopen_isopen_iff RS sym, |
|
874 |
isNSCont_isCont_iff RS sym])); |
|
875 |
qed "isCont_isopen_iff"; |
|
876 |
*******************************************************************) |
|
877 |
||
20755 | 878 |
subsection {* Uniform Continuity *} |
879 |
||
14477 | 880 |
lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y" |
881 |
by (simp add: isNSUCont_def) |
|
882 |
||
883 |
lemma isUCont_isCont: "isUCont f ==> isCont f x" |
|
884 |
by (simp add: isUCont_def isCont_def LIM_def, meson) |
|
885 |
||
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
886 |
lemma isUCont_isNSUCont: |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
887 |
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
|
888 |
assumes f: "isUCont f" shows "isNSUCont f" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
889 |
proof (unfold isNSUCont_def, safe) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
890 |
fix x y :: "'a star" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
891 |
assume approx: "x \<approx> y" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
892 |
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
|
893 |
proof (rule InfinitesimalI2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
894 |
fix r::real assume r: "0 < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
895 |
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
|
896 |
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
|
897 |
by (auto simp add: isUCont_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
898 |
from less_r have less_r': |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
899 |
"\<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
|
900 |
\<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
|
901 |
by transfer |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
902 |
from approx have "x - y \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
903 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
904 |
hence "hnorm (x - y) < star_of s" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
905 |
using s by (rule InfinitesimalD2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
906 |
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
|
907 |
by (rule less_r') |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
908 |
qed |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
909 |
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
|
910 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
911 |
qed |
14477 | 912 |
|
913 |
lemma isNSUCont_isUCont: |
|
20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
914 |
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
|
915 |
assumes f: "isNSUCont f" shows "isUCont f" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
916 |
proof (unfold isUCont_def, safe) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
917 |
fix r::real assume r: "0 < r" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
918 |
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
|
919 |
\<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
|
920 |
proof (rule exI, safe) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
921 |
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
|
922 |
next |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
923 |
fix x y :: "'a star" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
924 |
assume "hnorm (x - y) < epsilon" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
925 |
with Infinitesimal_epsilon |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
926 |
have "x - y \<in> Infinitesimal" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
927 |
by (rule hnorm_less_Infinitesimal) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
928 |
hence "x \<approx> y" |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
929 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
930 |
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
|
931 |
by (simp add: isNSUCont_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
932 |
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
|
933 |
by (unfold approx_def) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
934 |
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
|
935 |
using r by (rule InfinitesimalD2) |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
936 |
qed |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
937 |
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
|
938 |
by transfer |
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset
|
939 |
qed |
14477 | 940 |
|
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
941 |
subsection {* Relation of LIM and LIMSEQ *} |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
942 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
943 |
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
|
944 |
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
|
945 |
assumes X: "X -- a --> L" |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
946 |
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
|
947 |
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
|
948 |
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
|
949 |
fix r :: real |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
950 |
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
|
951 |
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
|
952 |
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
|
953 |
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
|
954 |
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
|
955 |
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
|
956 |
by fast |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
957 |
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
|
958 |
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
|
959 |
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
|
960 |
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
|
961 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
962 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
963 |
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
|
964 |
fixes a :: real |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
965 |
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
|
966 |
shows "X -- a --> L" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
967 |
proof (rule ccontr) |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
968 |
assume "\<not> (X -- a --> L)" |
20563 | 969 |
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) |
970 |
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 |
|
971 |
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) |
|
972 |
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
|
973 |
|
20563 | 974 |
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
|
975 |
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
|
976 |
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
|
977 |
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
|
978 |
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
|
979 |
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
|
980 |
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
|
981 |
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
|
982 |
by fast+ |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
983 |
|
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
984 |
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
|
985 |
proof (rule LIMSEQ_I, unfold real_norm_def) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
986 |
fix e::real |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
987 |
assume "0 < e" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
988 |
(* choose no such that inverse (real (Suc n)) < e *) |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
989 |
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
|
990 |
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
|
991 |
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
|
992 |
proof (intro exI allI impI) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
993 |
fix n |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
994 |
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
|
995 |
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
|
996 |
by (rule F2) |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
997 |
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
|
998 |
by auto |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
999 |
also from nodef have |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1000 |
"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
|
1001 |
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
|
1002 |
qed |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1003 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1004 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1005 |
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
|
1006 |
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
|
1007 |
|
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1008 |
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
|
1009 |
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
|
1010 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1011 |
moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1012 |
proof - |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1013 |
{ |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1014 |
fix no::nat |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1015 |
obtain n where "n = no + 1" by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1016 |
then have nolen: "no \<le> n" by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1017 |
(* 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
|
1018 |
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
|
1019 |
by (rule F3) |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
1020 |
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
|
1021 |
} |
20563 | 1022 |
then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp |
1023 |
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
|
1024 |
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
|
1025 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1026 |
ultimately show False by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1027 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1028 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1029 |
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
|
1030 |
"(\<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
|
1031 |
(X -- a --> L)" |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1032 |
proof |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1033 |
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
|
1034 |
show "X -- a --> L" by (rule LIMSEQ_SEQ_conv2) |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1035 |
next |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1036 |
assume "(X -- a --> L)" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1037 |
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
|
1038 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
1039 |
|
10751 | 1040 |
end |