author | bulwahn |
Fri, 03 Dec 2010 08:40:47 +0100 | |
changeset 40905 | 647142607448 |
parent 31338 | d41a8ba25b67 |
child 49962 | a8cc904a6820 |
permissions | -rw-r--r-- |
27468 | 1 |
(* Title : CLim.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 2001 University of Edinburgh |
|
4 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
|
5 |
*) |
|
6 |
||
7 |
header{*Limits, Continuity and Differentiation for Complex Functions*} |
|
8 |
||
9 |
theory CLim |
|
10 |
imports CStar |
|
11 |
begin |
|
12 |
||
13 |
(*not in simpset?*) |
|
14 |
declare hypreal_epsilon_not_zero [simp] |
|
15 |
||
16 |
(*??generalize*) |
|
17 |
lemma lemma_complex_mult_inverse_squared [simp]: |
|
18 |
"x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x" |
|
19 |
by (simp add: numeral_2_eq_2) |
|
20 |
||
21 |
text{*Changing the quantified variable. Install earlier?*} |
|
22 |
lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))"; |
|
23 |
apply auto |
|
24 |
apply (drule_tac x="x+a" in spec) |
|
25 |
apply (simp add: diff_minus add_assoc) |
|
26 |
done |
|
27 |
||
28 |
lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)" |
|
29 |
by (simp add: diff_eq_eq diff_minus [symmetric]) |
|
30 |
||
31 |
lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)" |
|
32 |
apply auto |
|
33 |
apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto) |
|
34 |
done |
|
35 |
||
36 |
||
37 |
subsection{*Limit of Complex to Complex Function*} |
|
38 |
||
39 |
lemma NSLIM_Re: "f -- a --NS> L ==> (%x. Re(f x)) -- a --NS> Re(L)" |
|
40 |
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff |
|
41 |
hRe_hcomplex_of_complex) |
|
42 |
||
43 |
lemma NSLIM_Im: "f -- a --NS> L ==> (%x. Im(f x)) -- a --NS> Im(L)" |
|
44 |
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff |
|
45 |
hIm_hcomplex_of_complex) |
|
46 |
||
47 |
(** get this result easily now **) |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
48 |
lemma LIM_Re: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
49 |
fixes f :: "'a::real_normed_vector \<Rightarrow> complex" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
50 |
shows "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)" |
27468 | 51 |
by (simp add: LIM_NSLIM_iff NSLIM_Re) |
52 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
53 |
lemma LIM_Im: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
54 |
fixes f :: "'a::real_normed_vector \<Rightarrow> complex" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
55 |
shows "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)" |
27468 | 56 |
by (simp add: LIM_NSLIM_iff NSLIM_Im) |
57 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
58 |
lemma LIM_cnj: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
59 |
fixes f :: "'a::real_normed_vector \<Rightarrow> complex" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
60 |
shows "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
61 |
by (simp add: LIM_eq complex_cnj_diff [symmetric]) |
27468 | 62 |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
63 |
lemma LIM_cnj_iff: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
64 |
fixes f :: "'a::real_normed_vector \<Rightarrow> complex" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
65 |
shows "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
66 |
by (simp add: LIM_eq complex_cnj_diff [symmetric]) |
27468 | 67 |
|
68 |
lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))" |
|
69 |
by transfer (rule refl) |
|
70 |
||
71 |
lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)" |
|
72 |
by transfer (rule refl) |
|
73 |
||
74 |
lemma star_of_Im [simp]: "star_of (Im x) = hIm (star_of x)" |
|
75 |
by transfer (rule refl) |
|
76 |
||
77 |
text"" |
|
78 |
(** another equivalence result **) |
|
79 |
lemma NSCLIM_NSCRLIM_iff: |
|
80 |
"(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)" |
|
81 |
by (simp add: NSLIM_def starfun_norm |
|
82 |
approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric]) |
|
83 |
||
84 |
(** much, much easier standard proof **) |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
85 |
lemma CLIM_CRLIM_iff: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
86 |
fixes f :: "'a::real_normed_vector \<Rightarrow> complex" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
87 |
shows "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
88 |
by (simp add: LIM_eq) |
27468 | 89 |
|
90 |
(* so this is nicer nonstandard proof *) |
|
91 |
lemma NSCLIM_NSCRLIM_iff2: |
|
92 |
"(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)" |
|
93 |
by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff) |
|
94 |
||
95 |
lemma NSLIM_NSCRLIM_Re_Im_iff: |
|
96 |
"(f -- a --NS> L) = ((%x. Re(f x)) -- a --NS> Re(L) & |
|
97 |
(%x. Im(f x)) -- a --NS> Im(L))" |
|
98 |
apply (auto intro: NSLIM_Re NSLIM_Im) |
|
99 |
apply (auto simp add: NSLIM_def starfun_Re starfun_Im) |
|
100 |
apply (auto dest!: spec) |
|
101 |
apply (simp add: hcomplex_approx_iff) |
|
102 |
done |
|
103 |
||
104 |
lemma LIM_CRLIM_Re_Im_iff: |
|
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
105 |
fixes f :: "'a::real_normed_vector \<Rightarrow> complex" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
106 |
shows "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) & |
27468 | 107 |
(%x. Im(f x)) -- a --> Im(L))" |
108 |
by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff) |
|
109 |
||
110 |
||
111 |
subsection{*Continuity*} |
|
112 |
||
113 |
lemma NSLIM_isContc_iff: |
|
114 |
"(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)" |
|
115 |
by (rule NSLIM_h_iff) |
|
116 |
||
117 |
subsection{*Functions from Complex to Reals*} |
|
118 |
||
119 |
lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)" |
|
120 |
by (auto intro: approx_hnorm |
|
121 |
simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] |
|
122 |
isNSCont_def) |
|
123 |
||
124 |
lemma isContCR_cmod [simp]: "isCont cmod (a)" |
|
125 |
by (simp add: isNSCont_isCont_iff [symmetric]) |
|
126 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
127 |
lemma isCont_Re: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
128 |
fixes f :: "'a::real_normed_vector \<Rightarrow> complex" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
129 |
shows "isCont f a ==> isCont (%x. Re (f x)) a" |
27468 | 130 |
by (simp add: isCont_def LIM_Re) |
131 |
||
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
132 |
lemma isCont_Im: |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
133 |
fixes f :: "'a::real_normed_vector \<Rightarrow> complex" |
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
27468
diff
changeset
|
134 |
shows "isCont f a ==> isCont (%x. Im (f x)) a" |
27468 | 135 |
by (simp add: isCont_def LIM_Im) |
136 |
||
137 |
subsection{* Differentiation of Natural Number Powers*} |
|
138 |
||
139 |
lemma CDERIV_pow [simp]: |
|
140 |
"DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" |
|
141 |
apply (induct n) |
|
142 |
apply (drule_tac [2] DERIV_ident [THEN DERIV_mult]) |
|
143 |
apply (auto simp add: left_distrib real_of_nat_Suc) |
|
144 |
apply (case_tac "n") |
|
145 |
apply (auto simp add: mult_ac add_commute) |
|
146 |
done |
|
147 |
||
148 |
text{*Nonstandard version*} |
|
149 |
lemma NSCDERIV_pow: |
|
150 |
"NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))" |
|
151 |
by (simp add: NSDERIV_DERIV_iff) |
|
152 |
||
153 |
text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*} |
|
154 |
lemma NSCDERIV_inverse: |
|
155 |
"(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))" |
|
156 |
unfolding numeral_2_eq_2 |
|
157 |
by (rule NSDERIV_inverse) |
|
158 |
||
159 |
lemma CDERIV_inverse: |
|
160 |
"(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))" |
|
161 |
unfolding numeral_2_eq_2 |
|
162 |
by (rule DERIV_inverse) |
|
163 |
||
164 |
||
165 |
subsection{*Derivative of Reciprocals (Function @{term inverse})*} |
|
166 |
||
167 |
lemma CDERIV_inverse_fun: |
|
168 |
"[| DERIV f x :> d; f(x) \<noteq> (0::complex) |] |
|
169 |
==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))" |
|
170 |
unfolding numeral_2_eq_2 |
|
171 |
by (rule DERIV_inverse_fun) |
|
172 |
||
173 |
lemma NSCDERIV_inverse_fun: |
|
174 |
"[| NSDERIV f x :> d; f(x) \<noteq> (0::complex) |] |
|
175 |
==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))" |
|
176 |
unfolding numeral_2_eq_2 |
|
177 |
by (rule NSDERIV_inverse_fun) |
|
178 |
||
179 |
||
180 |
subsection{* Derivative of Quotient*} |
|
181 |
||
182 |
lemma CDERIV_quotient: |
|
183 |
"[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |] |
|
184 |
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)" |
|
185 |
unfolding numeral_2_eq_2 |
|
186 |
by (rule DERIV_quotient) |
|
187 |
||
188 |
lemma NSCDERIV_quotient: |
|
189 |
"[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> (0::complex) |] |
|
190 |
==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)" |
|
191 |
unfolding numeral_2_eq_2 |
|
192 |
by (rule NSDERIV_quotient) |
|
193 |
||
194 |
||
195 |
subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*} |
|
196 |
||
197 |
lemma CARAT_CDERIVD: |
|
198 |
"(\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l |
|
199 |
==> NSDERIV f x :> l" |
|
200 |
by clarify (rule CARAT_DERIVD) |
|
201 |
||
202 |
end |