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 **)
|
|
48 |
lemma LIM_Re: "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)"
|
|
49 |
by (simp add: LIM_NSLIM_iff NSLIM_Re)
|
|
50 |
|
|
51 |
lemma LIM_Im: "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
|
|
52 |
by (simp add: LIM_NSLIM_iff NSLIM_Im)
|
|
53 |
|
|
54 |
lemma LIM_cnj: "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
|
|
55 |
by (simp add: LIM_def complex_cnj_diff [symmetric])
|
|
56 |
|
|
57 |
lemma LIM_cnj_iff: "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
|
|
58 |
by (simp add: LIM_def complex_cnj_diff [symmetric])
|
|
59 |
|
|
60 |
lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
|
|
61 |
by transfer (rule refl)
|
|
62 |
|
|
63 |
lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
|
|
64 |
by transfer (rule refl)
|
|
65 |
|
|
66 |
lemma star_of_Im [simp]: "star_of (Im x) = hIm (star_of x)"
|
|
67 |
by transfer (rule refl)
|
|
68 |
|
|
69 |
text""
|
|
70 |
(** another equivalence result **)
|
|
71 |
lemma NSCLIM_NSCRLIM_iff:
|
|
72 |
"(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
|
|
73 |
by (simp add: NSLIM_def starfun_norm
|
|
74 |
approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
|
|
75 |
|
|
76 |
(** much, much easier standard proof **)
|
|
77 |
lemma CLIM_CRLIM_iff: "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
|
|
78 |
by (simp add: LIM_def)
|
|
79 |
|
|
80 |
(* so this is nicer nonstandard proof *)
|
|
81 |
lemma NSCLIM_NSCRLIM_iff2:
|
|
82 |
"(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
|
|
83 |
by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
|
|
84 |
|
|
85 |
lemma NSLIM_NSCRLIM_Re_Im_iff:
|
|
86 |
"(f -- a --NS> L) = ((%x. Re(f x)) -- a --NS> Re(L) &
|
|
87 |
(%x. Im(f x)) -- a --NS> Im(L))"
|
|
88 |
apply (auto intro: NSLIM_Re NSLIM_Im)
|
|
89 |
apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
|
|
90 |
apply (auto dest!: spec)
|
|
91 |
apply (simp add: hcomplex_approx_iff)
|
|
92 |
done
|
|
93 |
|
|
94 |
lemma LIM_CRLIM_Re_Im_iff:
|
|
95 |
"(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) &
|
|
96 |
(%x. Im(f x)) -- a --> Im(L))"
|
|
97 |
by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
|
|
98 |
|
|
99 |
|
|
100 |
subsection{*Continuity*}
|
|
101 |
|
|
102 |
lemma NSLIM_isContc_iff:
|
|
103 |
"(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
|
|
104 |
by (rule NSLIM_h_iff)
|
|
105 |
|
|
106 |
subsection{*Functions from Complex to Reals*}
|
|
107 |
|
|
108 |
lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)"
|
|
109 |
by (auto intro: approx_hnorm
|
|
110 |
simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric]
|
|
111 |
isNSCont_def)
|
|
112 |
|
|
113 |
lemma isContCR_cmod [simp]: "isCont cmod (a)"
|
|
114 |
by (simp add: isNSCont_isCont_iff [symmetric])
|
|
115 |
|
|
116 |
lemma isCont_Re: "isCont f a ==> isCont (%x. Re (f x)) a"
|
|
117 |
by (simp add: isCont_def LIM_Re)
|
|
118 |
|
|
119 |
lemma isCont_Im: "isCont f a ==> isCont (%x. Im (f x)) a"
|
|
120 |
by (simp add: isCont_def LIM_Im)
|
|
121 |
|
|
122 |
subsection{* Differentiation of Natural Number Powers*}
|
|
123 |
|
|
124 |
lemma CDERIV_pow [simp]:
|
|
125 |
"DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
|
|
126 |
apply (induct n)
|
|
127 |
apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
|
|
128 |
apply (auto simp add: left_distrib real_of_nat_Suc)
|
|
129 |
apply (case_tac "n")
|
|
130 |
apply (auto simp add: mult_ac add_commute)
|
|
131 |
done
|
|
132 |
|
|
133 |
text{*Nonstandard version*}
|
|
134 |
lemma NSCDERIV_pow:
|
|
135 |
"NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
|
|
136 |
by (simp add: NSDERIV_DERIV_iff)
|
|
137 |
|
|
138 |
text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
|
|
139 |
lemma NSCDERIV_inverse:
|
|
140 |
"(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
|
|
141 |
unfolding numeral_2_eq_2
|
|
142 |
by (rule NSDERIV_inverse)
|
|
143 |
|
|
144 |
lemma CDERIV_inverse:
|
|
145 |
"(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"
|
|
146 |
unfolding numeral_2_eq_2
|
|
147 |
by (rule DERIV_inverse)
|
|
148 |
|
|
149 |
|
|
150 |
subsection{*Derivative of Reciprocals (Function @{term inverse})*}
|
|
151 |
|
|
152 |
lemma CDERIV_inverse_fun:
|
|
153 |
"[| DERIV f x :> d; f(x) \<noteq> (0::complex) |]
|
|
154 |
==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
|
|
155 |
unfolding numeral_2_eq_2
|
|
156 |
by (rule DERIV_inverse_fun)
|
|
157 |
|
|
158 |
lemma NSCDERIV_inverse_fun:
|
|
159 |
"[| NSDERIV f x :> d; f(x) \<noteq> (0::complex) |]
|
|
160 |
==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
|
|
161 |
unfolding numeral_2_eq_2
|
|
162 |
by (rule NSDERIV_inverse_fun)
|
|
163 |
|
|
164 |
|
|
165 |
subsection{* Derivative of Quotient*}
|
|
166 |
|
|
167 |
lemma CDERIV_quotient:
|
|
168 |
"[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |]
|
|
169 |
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
|
|
170 |
unfolding numeral_2_eq_2
|
|
171 |
by (rule DERIV_quotient)
|
|
172 |
|
|
173 |
lemma NSCDERIV_quotient:
|
|
174 |
"[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> (0::complex) |]
|
|
175 |
==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
|
|
176 |
unfolding numeral_2_eq_2
|
|
177 |
by (rule NSDERIV_quotient)
|
|
178 |
|
|
179 |
|
|
180 |
subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*}
|
|
181 |
|
|
182 |
lemma CARAT_CDERIVD:
|
|
183 |
"(\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l
|
|
184 |
==> NSDERIV f x :> l"
|
|
185 |
by clarify (rule CARAT_DERIVD)
|
|
186 |
|
|
187 |
end
|