author | haftmann |
Fri, 04 Jul 2014 20:18:47 +0200 | |
changeset 57512 | cc97b347b301 |
parent 56889 | 48a745e1bde7 |
child 57514 | bdc2c6b40bf2 |
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]: |
|
53077 | 18 |
"x \<noteq> (0::complex) \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x" |
27468 | 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) |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56889
diff
changeset
|
25 |
apply (simp add: add.assoc) |
27468 | 26 |
done |
27 |
||
28 |
lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)" |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53077
diff
changeset
|
29 |
by (simp add: diff_eq_eq) |
27468 | 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" |
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54230
diff
changeset
|
61 |
by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff) |
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)" |
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54230
diff
changeset
|
66 |
by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff) |
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]) |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
31338
diff
changeset
|
143 |
apply (auto simp add: distrib_right real_of_nat_Suc) |
27468 | 144 |
apply (case_tac "n") |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56889
diff
changeset
|
145 |
apply (auto simp add: mult_ac add.commute) |
27468 | 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))" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54230
diff
changeset
|
151 |
by (simp add: NSDERIV_DERIV_iff del: of_real_real_of_nat_eq) |
27468 | 152 |
|
153 |
text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*} |
|
154 |
lemma NSCDERIV_inverse: |
|
53077 | 155 |
"(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))" |
27468 | 156 |
unfolding numeral_2_eq_2 |
157 |
by (rule NSDERIV_inverse) |
|
158 |
||
159 |
lemma CDERIV_inverse: |
|
53077 | 160 |
"(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))" |
27468 | 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) |] |
|
53077 | 169 |
==> DERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))" |
27468 | 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) |] |
|
53077 | 175 |
==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))" |
27468 | 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) |] |
|
53077 | 184 |
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)" |
27468 | 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) |] |
|
53077 | 190 |
==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)" |
27468 | 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 |