author | huffman |
Fri, 29 May 2009 09:22:56 -0700 | |
changeset 31338 | d41a8ba25b67 |
parent 31336 | e17f13cd1280 |
child 31349 | 2261c8781f73 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : Lim.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
14477 | 4 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
10751 | 5 |
*) |
6 |
||
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
7 |
header{* Limits and Continuity *} |
10751 | 8 |
|
15131 | 9 |
theory Lim |
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
28952
diff
changeset
|
10 |
imports SEQ |
15131 | 11 |
begin |
14477 | 12 |
|
22641
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset
|
13 |
text{*Standard Definitions*} |
10751 | 14 |
|
19765 | 15 |
definition |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
16 |
LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset
|
17 |
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where |
28562 | 18 |
[code del]: "f -- a --> L = |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
19 |
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
20 |
--> dist (f x) L < r)" |
10751 | 21 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset
|
22 |
definition |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
23 |
isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where |
19765 | 24 |
"isCont f a = (f -- a --> (f a))" |
10751 | 25 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset
|
26 |
definition |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
27 |
isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
28 |
[code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)" |
10751 | 29 |
|
30 |
||
20755 | 31 |
subsection {* Limits of Functions *} |
14477 | 32 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
33 |
lemma metric_LIM_I: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
34 |
"(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
35 |
\<Longrightarrow> f -- a --> L" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
36 |
by (simp add: LIM_def) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
37 |
|
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
38 |
lemma metric_LIM_D: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
39 |
"\<lbrakk>f -- a --> L; 0 < r\<rbrakk> |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
40 |
\<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
41 |
by (simp add: LIM_def) |
14477 | 42 |
|
43 |
lemma LIM_eq: |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
44 |
fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
45 |
shows "f -- a --> L = |
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
46 |
(\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
47 |
by (simp add: LIM_def dist_norm) |
14477 | 48 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
49 |
lemma LIM_I: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
50 |
fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
51 |
shows "(!!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
|
52 |
==> f -- a --> L" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
53 |
by (simp add: LIM_eq) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
54 |
|
14477 | 55 |
lemma LIM_D: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
56 |
fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
57 |
shows "[| 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
|
58 |
==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r" |
14477 | 59 |
by (simp add: LIM_eq) |
60 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
61 |
lemma LIM_offset: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
62 |
fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
63 |
shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
64 |
unfolding LIM_def dist_norm |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
65 |
apply clarify |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
66 |
apply (drule_tac x="r" in spec, safe) |
20756 | 67 |
apply (rule_tac x="s" in exI, safe) |
68 |
apply (drule_tac x="x + k" in spec) |
|
29667 | 69 |
apply (simp add: algebra_simps) |
20756 | 70 |
done |
71 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
72 |
lemma LIM_offset_zero: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
73 |
fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
74 |
shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L" |
21239 | 75 |
by (drule_tac k="a" in LIM_offset, simp add: add_commute) |
76 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
77 |
lemma LIM_offset_zero_cancel: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
78 |
fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
79 |
shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L" |
21239 | 80 |
by (drule_tac k="- a" in LIM_offset, simp) |
81 |
||
15228 | 82 |
lemma LIM_const [simp]: "(%x. k) -- x --> k" |
14477 | 83 |
by (simp add: LIM_def) |
84 |
||
85 |
lemma LIM_add: |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
86 |
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
14477 | 87 |
assumes f: "f -- a --> L" and g: "g -- a --> M" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
88 |
shows "(\<lambda>x. f x + g x) -- a --> (L + M)" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
89 |
proof (rule metric_LIM_I) |
14477 | 90 |
fix r :: real |
20409 | 91 |
assume r: "0 < r" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
92 |
from metric_LIM_D [OF f half_gt_zero [OF r]] |
14477 | 93 |
obtain fs |
94 |
where fs: "0 < fs" |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
95 |
and fs_lt: "\<forall>x. x \<noteq> a \<and> dist x a < fs \<longrightarrow> dist (f x) L < r/2" |
14477 | 96 |
by blast |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
97 |
from metric_LIM_D [OF g half_gt_zero [OF r]] |
14477 | 98 |
obtain gs |
99 |
where gs: "0 < gs" |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
100 |
and gs_lt: "\<forall>x. x \<noteq> a \<and> dist x a < gs \<longrightarrow> dist (g x) M < r/2" |
14477 | 101 |
by blast |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
102 |
show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x + g x) (L + M) < r" |
14477 | 103 |
proof (intro exI conjI strip) |
104 |
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
|
105 |
fix x :: 'a |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
106 |
assume "x \<noteq> a \<and> dist x a < min fs gs" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
107 |
hence "x \<noteq> a \<and> dist x a < fs \<and> dist x a < gs" by simp |
14477 | 108 |
with fs_lt gs_lt |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
109 |
have "dist (f x) L < r/2" and "dist (g x) M < r/2" by blast+ |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
110 |
hence "dist (f x) L + dist (g x) M < r" by arith |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
111 |
thus "dist (f x + g x) (L + M) < r" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
112 |
unfolding dist_norm |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
113 |
by (blast intro: norm_diff_triangle_ineq order_le_less_trans) |
14477 | 114 |
qed |
115 |
qed |
|
116 |
||
21257 | 117 |
lemma LIM_add_zero: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
118 |
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
119 |
shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0" |
21257 | 120 |
by (drule (1) LIM_add, simp) |
121 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
122 |
lemma minus_diff_minus: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
123 |
fixes a b :: "'a::ab_group_add" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
124 |
shows "(- a) - (- b) = - (a - b)" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
125 |
by simp |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
126 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
127 |
lemma LIM_minus: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
128 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
129 |
shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
130 |
by (simp only: LIM_def dist_norm minus_diff_minus norm_minus_cancel) |
14477 | 131 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
132 |
(* TODO: delete *) |
14477 | 133 |
lemma LIM_add_minus: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
134 |
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
135 |
shows "[| 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
|
136 |
by (intro LIM_add LIM_minus) |
14477 | 137 |
|
138 |
lemma LIM_diff: |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
139 |
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
140 |
shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>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
|
141 |
by (simp only: diff_minus LIM_add LIM_minus) |
14477 | 142 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
143 |
lemma LIM_zero: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
144 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
145 |
shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
146 |
by (simp add: LIM_def dist_norm) |
21239 | 147 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
148 |
lemma LIM_zero_cancel: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
149 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
150 |
shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
151 |
by (simp add: LIM_def dist_norm) |
21239 | 152 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
153 |
lemma LIM_zero_iff: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
154 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
155 |
shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
156 |
by (simp add: LIM_def dist_norm) |
21399 | 157 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
158 |
lemma metric_LIM_imp_LIM: |
21257 | 159 |
assumes f: "f -- a --> l" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
160 |
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l" |
21257 | 161 |
shows "g -- a --> m" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
162 |
apply (rule metric_LIM_I, drule metric_LIM_D [OF f], safe) |
21257 | 163 |
apply (rule_tac x="s" in exI, safe) |
164 |
apply (drule_tac x="x" in spec, safe) |
|
165 |
apply (erule (1) order_le_less_trans [OF le]) |
|
166 |
done |
|
167 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
168 |
lemma LIM_imp_LIM: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
169 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
170 |
fixes g :: "'a::metric_space \<Rightarrow> 'c::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
171 |
assumes f: "f -- a --> l" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
172 |
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
173 |
shows "g -- a --> m" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
174 |
apply (rule metric_LIM_imp_LIM [OF f]) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
175 |
apply (simp add: dist_norm le) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
176 |
done |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
177 |
|
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
178 |
lemma LIM_norm: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
179 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
180 |
shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l" |
21257 | 181 |
by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3) |
182 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
183 |
lemma LIM_norm_zero: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
184 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
185 |
shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0" |
21257 | 186 |
by (drule LIM_norm, simp) |
187 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
188 |
lemma LIM_norm_zero_cancel: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
189 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
190 |
shows "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0" |
21257 | 191 |
by (erule LIM_imp_LIM, simp) |
192 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
193 |
lemma LIM_norm_zero_iff: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
194 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
195 |
shows "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0" |
21399 | 196 |
by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero]) |
197 |
||
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
198 |
lemma LIM_rabs: "f -- a --> (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> \<bar>l\<bar>" |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
199 |
by (fold real_norm_def, rule LIM_norm) |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
200 |
|
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
201 |
lemma LIM_rabs_zero: "f -- a --> (0::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> 0" |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
202 |
by (fold real_norm_def, rule LIM_norm_zero) |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
203 |
|
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
204 |
lemma LIM_rabs_zero_cancel: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) \<Longrightarrow> f -- a --> 0" |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
205 |
by (fold real_norm_def, rule LIM_norm_zero_cancel) |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
206 |
|
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
207 |
lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0" |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
208 |
by (fold real_norm_def, rule LIM_norm_zero_iff) |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
209 |
|
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
210 |
lemma LIM_const_not_eq: |
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset
|
211 |
fixes a :: "'a::real_normed_algebra_1" |
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset
|
212 |
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
213 |
apply (simp add: LIM_def) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
214 |
apply (rule_tac x="dist k L" in exI, simp add: zero_less_dist_iff, safe) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
215 |
apply (rule_tac x="a + of_real (s/2)" in exI, simp add: dist_norm) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
216 |
done |
14477 | 217 |
|
21786 | 218 |
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0] |
219 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
220 |
lemma LIM_const_eq: |
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset
|
221 |
fixes a :: "'a::real_normed_algebra_1" |
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset
|
222 |
shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L" |
14477 | 223 |
apply (rule ccontr) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
224 |
apply (blast dest: LIM_const_not_eq) |
14477 | 225 |
done |
226 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
227 |
lemma LIM_unique: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
228 |
fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *} |
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset
|
229 |
shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
230 |
apply (rule ccontr) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
231 |
apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
232 |
apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
233 |
apply (clarify, rename_tac r s) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
234 |
apply (subgoal_tac "min r s \<noteq> 0") |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
235 |
apply (subgoal_tac "dist L M < dist L M / 2 + dist L M / 2", simp) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
236 |
apply (subgoal_tac "dist L M \<le> dist (f (a + of_real (min r s / 2))) L + |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
237 |
dist (f (a + of_real (min r s / 2))) M") |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
238 |
apply (erule le_less_trans, rule add_strict_mono) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
239 |
apply (drule spec, erule mp, simp add: dist_norm) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
240 |
apply (drule spec, erule mp, simp add: dist_norm) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
241 |
apply (subst dist_commute, rule dist_triangle) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
242 |
apply simp |
14477 | 243 |
done |
244 |
||
23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset
|
245 |
lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a" |
14477 | 246 |
by (auto simp add: LIM_def) |
247 |
||
248 |
text{*Limits are equal for functions equal except at limit point*} |
|
249 |
lemma LIM_equal: |
|
250 |
"[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)" |
|
251 |
by (simp add: LIM_def) |
|
252 |
||
20796 | 253 |
lemma LIM_cong: |
254 |
"\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk> |
|
21399 | 255 |
\<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)" |
20796 | 256 |
by (simp add: LIM_def) |
257 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
258 |
lemma metric_LIM_equal2: |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
259 |
assumes 1: "0 < R" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
260 |
assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x" |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
261 |
shows "g -- a --> l \<Longrightarrow> f -- a --> l" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
262 |
apply (unfold LIM_def, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
263 |
apply (drule_tac x="r" in spec, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
264 |
apply (rule_tac x="min s R" in exI, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
265 |
apply (simp add: 1) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
266 |
apply (simp add: 2) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
267 |
done |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
268 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
269 |
lemma LIM_equal2: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
270 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
271 |
assumes 1: "0 < R" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
272 |
assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
273 |
shows "g -- a --> l \<Longrightarrow> f -- a --> l" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
274 |
apply (unfold LIM_def dist_norm, safe) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
275 |
apply (drule_tac x="r" in spec, safe) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
276 |
apply (rule_tac x="min s R" in exI, safe) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
277 |
apply (simp add: 1) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
278 |
apply (simp add: 2) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
279 |
done |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
280 |
|
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
281 |
text{*Two uses in Transcendental.ML*} |
14477 | 282 |
lemma LIM_trans: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
283 |
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
284 |
shows "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l" |
14477 | 285 |
apply (drule LIM_add, assumption) |
286 |
apply (auto simp add: add_assoc) |
|
287 |
done |
|
288 |
||
21239 | 289 |
lemma LIM_compose: |
290 |
assumes g: "g -- l --> g l" |
|
291 |
assumes f: "f -- a --> l" |
|
292 |
shows "(\<lambda>x. g (f x)) -- a --> g l" |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
293 |
proof (rule metric_LIM_I) |
21239 | 294 |
fix r::real assume r: "0 < r" |
295 |
obtain s where s: "0 < s" |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
296 |
and less_r: "\<And>y. \<lbrakk>y \<noteq> l; dist y l < s\<rbrakk> \<Longrightarrow> dist (g y) (g l) < r" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
297 |
using metric_LIM_D [OF g r] by fast |
21239 | 298 |
obtain t where t: "0 < t" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
299 |
and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) l < s" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
300 |
using metric_LIM_D [OF f s] by fast |
21239 | 301 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
302 |
show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) (g l) < r" |
21239 | 303 |
proof (rule exI, safe) |
304 |
show "0 < t" using t . |
|
305 |
next |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
306 |
fix x assume "x \<noteq> a" and "dist x a < t" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
307 |
hence "dist (f x) l < s" by (rule less_s) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
308 |
thus "dist (g (f x)) (g l) < r" |
21239 | 309 |
using r less_r by (case_tac "f x = l", simp_all) |
310 |
qed |
|
311 |
qed |
|
312 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
313 |
lemma metric_LIM_compose2: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
314 |
assumes f: "f -- a --> b" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
315 |
assumes g: "g -- b --> c" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
316 |
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
317 |
shows "(\<lambda>x. g (f x)) -- a --> c" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
318 |
proof (rule metric_LIM_I) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
319 |
fix r :: real |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
320 |
assume r: "0 < r" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
321 |
obtain s where s: "0 < s" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
322 |
and less_r: "\<And>y. \<lbrakk>y \<noteq> b; dist y b < s\<rbrakk> \<Longrightarrow> dist (g y) c < r" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
323 |
using metric_LIM_D [OF g r] by fast |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
324 |
obtain t where t: "0 < t" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
325 |
and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) b < s" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
326 |
using metric_LIM_D [OF f s] by fast |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
327 |
obtain d where d: "0 < d" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
328 |
and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < d\<rbrakk> \<Longrightarrow> f x \<noteq> b" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
329 |
using inj by fast |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
330 |
|
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
331 |
show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) c < r" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
332 |
proof (safe intro!: exI) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
333 |
show "0 < min d t" using d t by simp |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
334 |
next |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
335 |
fix x |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
336 |
assume "x \<noteq> a" and "dist x a < min d t" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
337 |
hence "f x \<noteq> b" and "dist (f x) b < s" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
338 |
using neq_b less_s by simp_all |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
339 |
thus "dist (g (f x)) c < r" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
340 |
by (rule less_r) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
341 |
qed |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
342 |
qed |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
343 |
|
23040 | 344 |
lemma LIM_compose2: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
345 |
fixes a :: "'a::real_normed_vector" |
23040 | 346 |
assumes f: "f -- a --> b" |
347 |
assumes g: "g -- b --> c" |
|
348 |
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b" |
|
349 |
shows "(\<lambda>x. g (f x)) -- a --> c" |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
350 |
by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) |
23040 | 351 |
|
21239 | 352 |
lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l" |
353 |
unfolding o_def by (rule LIM_compose) |
|
354 |
||
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
355 |
lemma real_LIM_sandwich_zero: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
356 |
fixes f g :: "'a::metric_space \<Rightarrow> real" |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
357 |
assumes f: "f -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
358 |
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
|
359 |
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
|
360 |
shows "g -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
361 |
proof (rule LIM_imp_LIM [OF f]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
362 |
fix x assume x: "x \<noteq> a" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
363 |
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
|
364 |
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
|
365 |
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
|
366 |
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
|
367 |
finally show "norm (g x - 0) \<le> norm (f x - 0)" . |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
368 |
qed |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
369 |
|
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21810
diff
changeset
|
370 |
text {* Bounded Linear Operators *} |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
371 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
372 |
lemma (in bounded_linear) cont: "f -- a --> f a" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
373 |
proof (rule LIM_I) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
374 |
fix r::real assume r: "0 < r" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
375 |
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
|
376 |
using pos_bounded by fast |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
377 |
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
|
378 |
proof (rule exI, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
379 |
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
|
380 |
next |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
381 |
fix x assume x: "norm (x - a) < r / K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
382 |
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
|
383 |
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
|
384 |
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
|
385 |
finally show "norm (f x - f a) < r" . |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
386 |
qed |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
387 |
qed |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
388 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
389 |
lemma (in bounded_linear) LIM: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
390 |
"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
|
391 |
by (rule LIM_compose [OF cont]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
392 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
393 |
lemma (in bounded_linear) LIM_zero: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
394 |
"g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
395 |
by (drule LIM, simp only: zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
396 |
|
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21810
diff
changeset
|
397 |
text {* Bounded Bilinear Operators *} |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
398 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
399 |
lemma (in bounded_bilinear) LIM_prod_zero: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
400 |
fixes a :: "'d::metric_space" |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
401 |
assumes f: "f -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
402 |
assumes g: "g -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
403 |
shows "(\<lambda>x. f x ** g x) -- a --> 0" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
404 |
proof (rule metric_LIM_I, unfold dist_norm) |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
405 |
fix r::real assume r: "0 < r" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
406 |
obtain K where K: "0 < K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
407 |
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
|
408 |
using pos_bounded by fast |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
409 |
from K have K': "0 < inverse K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
410 |
by (rule positive_imp_inverse_positive) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
411 |
obtain s where s: "0 < s" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
412 |
and norm_f: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> norm (f x) < r" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
413 |
using metric_LIM_D [OF f r, unfolded dist_norm] by auto |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
414 |
obtain t where t: "0 < t" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
415 |
and norm_g: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> norm (g x) < inverse K" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
416 |
using metric_LIM_D [OF g K', unfolded dist_norm] by auto |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
417 |
show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> norm (f x ** g x - 0) < r" |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
418 |
proof (rule exI, safe) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
419 |
from s t show "0 < min s t" by simp |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
420 |
next |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
421 |
fix x assume x: "x \<noteq> a" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
422 |
assume "dist x a < min s t" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
423 |
hence xs: "dist x a < s" and xt: "dist x a < t" by simp_all |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
424 |
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
|
425 |
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
|
426 |
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
|
427 |
also from 1 2 K have "\<dots> < r * inverse K * K" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
428 |
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
|
429 |
also from K have "r * inverse K * K = r" by simp |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
430 |
finally show "norm (f x ** g x - 0) < r" by simp |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
431 |
qed |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
432 |
qed |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
433 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
434 |
lemma (in bounded_bilinear) LIM_left_zero: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
435 |
"f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
436 |
by (rule bounded_linear.LIM_zero [OF bounded_linear_left]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
437 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
438 |
lemma (in bounded_bilinear) LIM_right_zero: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
439 |
"f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
440 |
by (rule bounded_linear.LIM_zero [OF bounded_linear_right]) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
441 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
442 |
lemma (in bounded_bilinear) LIM: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
443 |
"\<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
|
444 |
apply (drule LIM_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
445 |
apply (drule LIM_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
446 |
apply (rule LIM_zero_cancel) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
447 |
apply (subst prod_diff_prod) |
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 (rule LIM_add_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
450 |
apply (erule (1) LIM_prod_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
451 |
apply (erule LIM_left_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
452 |
apply (erule LIM_right_zero) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
453 |
done |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
454 |
|
23127 | 455 |
lemmas LIM_mult = mult.LIM |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
456 |
|
23127 | 457 |
lemmas LIM_mult_zero = mult.LIM_prod_zero |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
458 |
|
23127 | 459 |
lemmas LIM_mult_left_zero = mult.LIM_left_zero |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
460 |
|
23127 | 461 |
lemmas LIM_mult_right_zero = mult.LIM_right_zero |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
462 |
|
23127 | 463 |
lemmas LIM_scaleR = scaleR.LIM |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
464 |
|
23127 | 465 |
lemmas LIM_of_real = of_real.LIM |
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
466 |
|
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
467 |
lemma LIM_power: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
468 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}" |
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
469 |
assumes f: "f -- a --> l" |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
470 |
shows "(\<lambda>x. f x ^ n) -- a --> l ^ n" |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
29885
diff
changeset
|
471 |
by (induct n, simp, simp add: LIM_mult f) |
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
472 |
|
22641
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset
|
473 |
subsubsection {* Derived theorems about @{term LIM} *} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset
|
474 |
|
22637 | 475 |
lemma LIM_inverse_lemma: |
476 |
fixes x :: "'a::real_normed_div_algebra" |
|
477 |
assumes r: "0 < r" |
|
478 |
assumes x: "norm (x - 1) < min (1/2) (r/2)" |
|
479 |
shows "norm (inverse x - 1) < r" |
|
480 |
proof - |
|
481 |
from r have r2: "0 < r/2" by simp |
|
482 |
from x have 0: "x \<noteq> 0" by clarsimp |
|
483 |
from x have x': "norm (1 - x) < min (1/2) (r/2)" |
|
484 |
by (simp only: norm_minus_commute) |
|
485 |
hence less1: "norm (1 - x) < r/2" by simp |
|
486 |
have "norm (1::'a) - norm x \<le> norm (1 - x)" by (rule norm_triangle_ineq2) |
|
487 |
also from x' have "norm (1 - x) < 1/2" by simp |
|
488 |
finally have "1/2 < norm x" by simp |
|
489 |
hence "inverse (norm x) < inverse (1/2)" |
|
490 |
by (rule less_imp_inverse_less, simp) |
|
491 |
hence less2: "norm (inverse x) < 2" |
|
492 |
by (simp add: nonzero_norm_inverse 0) |
|
493 |
from less1 less2 r2 norm_ge_zero |
|
494 |
have "norm (1 - x) * norm (inverse x) < (r/2) * 2" |
|
495 |
by (rule mult_strict_mono) |
|
496 |
thus "norm (inverse x - 1) < r" |
|
497 |
by (simp only: norm_mult [symmetric] left_diff_distrib, simp add: 0) |
|
498 |
qed |
|
499 |
||
500 |
lemma LIM_inverse_fun: |
|
501 |
assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)" |
|
502 |
shows "inverse -- a --> inverse a" |
|
503 |
proof (rule LIM_equal2) |
|
504 |
from a show "0 < norm a" by simp |
|
505 |
next |
|
506 |
fix x assume "norm (x - a) < norm a" |
|
507 |
hence "x \<noteq> 0" by auto |
|
508 |
with a show "inverse x = inverse (inverse a * x) * inverse a" |
|
509 |
by (simp add: nonzero_inverse_mult_distrib |
|
510 |
nonzero_imp_inverse_nonzero |
|
511 |
nonzero_inverse_inverse_eq mult_assoc) |
|
512 |
next |
|
513 |
have 1: "inverse -- 1 --> inverse (1::'a)" |
|
514 |
apply (rule LIM_I) |
|
515 |
apply (rule_tac x="min (1/2) (r/2)" in exI) |
|
516 |
apply (simp add: LIM_inverse_lemma) |
|
517 |
done |
|
518 |
have "(\<lambda>x. inverse a * x) -- a --> inverse a * a" |
|
23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset
|
519 |
by (intro LIM_mult LIM_ident LIM_const) |
22637 | 520 |
hence "(\<lambda>x. inverse a * x) -- a --> 1" |
521 |
by (simp add: a) |
|
522 |
with 1 have "(\<lambda>x. inverse (inverse a * x)) -- a --> inverse 1" |
|
523 |
by (rule LIM_compose) |
|
524 |
hence "(\<lambda>x. inverse (inverse a * x)) -- a --> 1" |
|
525 |
by simp |
|
526 |
hence "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> 1 * inverse a" |
|
527 |
by (intro LIM_mult LIM_const) |
|
528 |
thus "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> inverse a" |
|
529 |
by simp |
|
530 |
qed |
|
531 |
||
532 |
lemma LIM_inverse: |
|
533 |
fixes L :: "'a::real_normed_div_algebra" |
|
534 |
shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L" |
|
535 |
by (rule LIM_inverse_fun [THEN LIM_compose]) |
|
536 |
||
29885 | 537 |
lemma LIM_sgn: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
538 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
539 |
shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l" |
29885 | 540 |
unfolding sgn_div_norm |
541 |
by (simp add: LIM_scaleR LIM_inverse LIM_norm) |
|
542 |
||
14477 | 543 |
|
20755 | 544 |
subsection {* Continuity *} |
14477 | 545 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
546 |
lemma LIM_isCont_iff: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
547 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
548 |
shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)" |
21239 | 549 |
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) |
550 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
551 |
lemma isCont_iff: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
552 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
553 |
shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x" |
21239 | 554 |
by (simp add: isCont_def LIM_isCont_iff) |
555 |
||
23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset
|
556 |
lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a" |
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset
|
557 |
unfolding isCont_def by (rule LIM_ident) |
21239 | 558 |
|
21786 | 559 |
lemma isCont_const [simp]: "isCont (\<lambda>x. k) a" |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
560 |
unfolding isCont_def by (rule LIM_const) |
21239 | 561 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
562 |
lemma isCont_norm: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
563 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
564 |
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a" |
21786 | 565 |
unfolding isCont_def by (rule LIM_norm) |
566 |
||
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
567 |
lemma isCont_rabs: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x :: real\<bar>) a" |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
568 |
unfolding isCont_def by (rule LIM_rabs) |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
569 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
570 |
lemma isCont_add: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
571 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
572 |
shows "\<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
|
573 |
unfolding isCont_def by (rule LIM_add) |
21239 | 574 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
575 |
lemma isCont_minus: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
576 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
577 |
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a" |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
578 |
unfolding isCont_def by (rule LIM_minus) |
21239 | 579 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
580 |
lemma isCont_diff: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
581 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
582 |
shows "\<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
|
583 |
unfolding isCont_def by (rule LIM_diff) |
21239 | 584 |
|
585 |
lemma isCont_mult: |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
586 |
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_algebra" |
21786 | 587 |
shows "\<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
|
588 |
unfolding isCont_def by (rule LIM_mult) |
21239 | 589 |
|
590 |
lemma isCont_inverse: |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
591 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_div_algebra" |
21786 | 592 |
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a" |
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
593 |
unfolding isCont_def by (rule LIM_inverse) |
21239 | 594 |
|
595 |
lemma isCont_LIM_compose: |
|
596 |
"\<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
|
597 |
unfolding isCont_def by (rule LIM_compose) |
21239 | 598 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
599 |
lemma metric_isCont_LIM_compose2: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
600 |
assumes f [unfolded isCont_def]: "isCont f a" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
601 |
assumes g: "g -- f a --> l" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
602 |
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
603 |
shows "(\<lambda>x. g (f x)) -- a --> l" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
604 |
by (rule metric_LIM_compose2 [OF f g inj]) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
605 |
|
23040 | 606 |
lemma isCont_LIM_compose2: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
607 |
fixes a :: "'a::real_normed_vector" |
23040 | 608 |
assumes f [unfolded isCont_def]: "isCont f a" |
609 |
assumes g: "g -- f a --> l" |
|
610 |
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a" |
|
611 |
shows "(\<lambda>x. g (f x)) -- a --> l" |
|
612 |
by (rule LIM_compose2 [OF f g inj]) |
|
613 |
||
21239 | 614 |
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
|
615 |
unfolding isCont_def by (rule LIM_compose) |
21239 | 616 |
|
617 |
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
|
618 |
unfolding o_def by (rule isCont_o2) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
619 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
620 |
lemma (in bounded_linear) isCont: "isCont f a" |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
621 |
unfolding isCont_def by (rule cont) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
622 |
|
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
623 |
lemma (in bounded_bilinear) isCont: |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
624 |
"\<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
|
625 |
unfolding isCont_def by (rule LIM) |
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset
|
626 |
|
23127 | 627 |
lemmas isCont_scaleR = scaleR.isCont |
21239 | 628 |
|
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
629 |
lemma isCont_of_real: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
630 |
"isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a" |
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
631 |
unfolding isCont_def by (rule LIM_of_real) |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
632 |
|
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
633 |
lemma isCont_power: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
634 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}" |
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
635 |
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a" |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
636 |
unfolding isCont_def by (rule LIM_power) |
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset
|
637 |
|
29885 | 638 |
lemma isCont_sgn: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
639 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
640 |
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a" |
29885 | 641 |
unfolding isCont_def by (rule LIM_sgn) |
642 |
||
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset
|
643 |
lemma isCont_abs [simp]: "isCont abs (a::real)" |
23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset
|
644 |
by (rule isCont_rabs [OF isCont_ident]) |
15228 | 645 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
646 |
lemma isCont_setsum: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
647 |
fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
648 |
fixes A :: "'a set" assumes "finite A" |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
649 |
shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
650 |
using `finite A` |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
651 |
proof induct |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
652 |
case (insert a F) show "isCont (\<lambda> x. \<Sum> i \<in> (insert a F). f i x) x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
653 |
unfolding setsum_insert[OF `finite F` `a \<notin> F`] by (rule isCont_add, auto simp add: insert) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
654 |
qed auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
655 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
656 |
lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
657 |
and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
658 |
shows "0 \<le> f x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
659 |
proof (rule ccontr) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
660 |
assume "\<not> 0 \<le> f x" hence "f x < 0" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
661 |
hence "0 < - f x / 2" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
662 |
from isCont[unfolded isCont_def, THEN LIM_D, OF this] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
663 |
obtain s where "s > 0" and s_D: "\<And>x'. \<lbrakk> x' \<noteq> x ; \<bar> x' - x \<bar> < s \<rbrakk> \<Longrightarrow> \<bar> f x' - f x \<bar> < - f x / 2" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
664 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
665 |
let ?x = "x - min (s / 2) ((x - b) / 2)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
666 |
have "?x < x" and "\<bar> ?x - x \<bar> < s" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
667 |
using `b < x` and `0 < s` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
668 |
have "b < ?x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
669 |
proof (cases "s < x - b") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
670 |
case True thus ?thesis using `0 < s` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
671 |
next |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
672 |
case False hence "s / 2 \<ge> (x - b) / 2" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
673 |
from inf_absorb2[OF this, unfolded inf_real_def] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
674 |
have "?x = (x + b) / 2" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
675 |
thus ?thesis using `b < x` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
676 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
677 |
hence "0 \<le> f ?x" using all_le `?x < x` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
678 |
moreover have "\<bar>f ?x - f x\<bar> < - f x / 2" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
679 |
using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
680 |
hence "f ?x - f x < - f x / 2" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
681 |
hence "f ?x < f x / 2" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
682 |
hence "f ?x < 0" using `f x < 0` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
683 |
thus False using `0 \<le> f ?x` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset
|
684 |
qed |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
685 |
|
14477 | 686 |
|
20755 | 687 |
subsection {* Uniform Continuity *} |
688 |
||
14477 | 689 |
lemma isUCont_isCont: "isUCont f ==> isCont f x" |
23012 | 690 |
by (simp add: isUCont_def isCont_def LIM_def, force) |
14477 | 691 |
|
23118 | 692 |
lemma isUCont_Cauchy: |
693 |
"\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))" |
|
694 |
unfolding isUCont_def |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
695 |
apply (rule metric_CauchyI) |
23118 | 696 |
apply (drule_tac x=e in spec, safe) |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
697 |
apply (drule_tac e=s in metric_CauchyD, safe) |
23118 | 698 |
apply (rule_tac x=M in exI, simp) |
699 |
done |
|
700 |
||
701 |
lemma (in bounded_linear) isUCont: "isUCont f" |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
702 |
unfolding isUCont_def dist_norm |
23118 | 703 |
proof (intro allI impI) |
704 |
fix r::real assume r: "0 < r" |
|
705 |
obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K" |
|
706 |
using pos_bounded by fast |
|
707 |
show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r" |
|
708 |
proof (rule exI, safe) |
|
709 |
from r K show "0 < r / K" by (rule divide_pos_pos) |
|
710 |
next |
|
711 |
fix x y :: 'a |
|
712 |
assume xy: "norm (x - y) < r / K" |
|
713 |
have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff) |
|
714 |
also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le) |
|
715 |
also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq) |
|
716 |
finally show "norm (f x - f y) < r" . |
|
717 |
qed |
|
718 |
qed |
|
719 |
||
720 |
lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))" |
|
721 |
by (rule isUCont [THEN isUCont_Cauchy]) |
|
722 |
||
14477 | 723 |
|
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
724 |
subsection {* Relation of LIM and LIMSEQ *} |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
725 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
726 |
lemma LIMSEQ_SEQ_conv1: |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
727 |
fixes a :: "'a::metric_space" |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
728 |
assumes X: "X -- a --> L" |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
729 |
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
730 |
proof (safe intro!: metric_LIMSEQ_I) |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
731 |
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
|
732 |
fix r :: real |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
733 |
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
|
734 |
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
|
735 |
assume S: "S ----> a" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
736 |
from metric_LIM_D [OF X rgz] obtain s |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
737 |
where sgz: "0 < s" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
738 |
and aux: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> dist (X x) L < r" |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
739 |
by fast |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
740 |
from metric_LIMSEQ_D [OF S sgz] |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
741 |
obtain no where "\<forall>n\<ge>no. dist (S n) a < s" by blast |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
742 |
hence "\<forall>n\<ge>no. dist (X (S n)) L < r" by (simp add: aux as) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
743 |
thus "\<exists>no. \<forall>n\<ge>no. dist (X (S n)) L < r" .. |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
744 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
745 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
746 |
|
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
747 |
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
|
748 |
fixes a :: real |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
749 |
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
|
750 |
shows "X -- a --> L" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
751 |
proof (rule ccontr) |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
752 |
assume "\<not> (X -- a --> L)" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
753 |
hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> dist (X x) L < r)" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
754 |
unfolding LIM_def dist_norm . |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
755 |
hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> dist (X x) L < r)" by simp |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
756 |
hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r)" by (simp add: not_less) |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
757 |
then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r))" by auto |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
758 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
759 |
let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
760 |
have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (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
|
761 |
using rdef by simp |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
762 |
hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (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
|
763 |
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
|
764 |
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
|
765 |
and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
766 |
and F3: "\<And>n. dist (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
|
767 |
by fast+ |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
768 |
|
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
769 |
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
|
770 |
proof (rule LIMSEQ_I, unfold real_norm_def) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
771 |
fix e::real |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
772 |
assume "0 < e" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
773 |
(* choose no such that inverse (real (Suc n)) < e *) |
23441 | 774 |
then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
775 |
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
|
776 |
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
|
777 |
proof (intro exI allI impI) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
778 |
fix n |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
779 |
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
|
780 |
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
|
781 |
by (rule F2) |
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
782 |
also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))" |
23441 | 783 |
using mlen by auto |
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset
|
784 |
also from nodef have |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
785 |
"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
|
786 |
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
|
787 |
qed |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
788 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
789 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
790 |
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
|
791 |
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
|
792 |
|
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
793 |
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
|
794 |
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
|
795 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
796 |
moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)" |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
797 |
proof - |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
798 |
{ |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
799 |
fix no::nat |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
800 |
obtain n where "n = no + 1" by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
801 |
then have nolen: "no \<le> n" by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
802 |
(* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *) |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
803 |
have "dist (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
|
804 |
by (rule F3) |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
805 |
with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
806 |
} |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
807 |
then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
808 |
with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset
|
809 |
thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
810 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
811 |
ultimately show False by simp |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
812 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
813 |
|
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
814 |
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
|
815 |
"(\<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
|
816 |
(X -- a --> L)" |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
817 |
proof |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
818 |
assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" |
23441 | 819 |
thus "X -- a --> L" by (rule LIMSEQ_SEQ_conv2) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
820 |
next |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
821 |
assume "(X -- a --> L)" |
23441 | 822 |
thus "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1) |
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
823 |
qed |
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset
|
824 |
|
10751 | 825 |
end |