author | wenzelm |
Sun, 18 May 2008 15:04:09 +0200 | |
changeset 26939 | 1035c89b4c02 |
parent 23077 | be166bf115d4 |
child 27105 | 5f139027c365 |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title : CLim.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 2001 University of Edinburgh |
|
14469 | 4 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
13957 | 5 |
*) |
6 |
||
14469 | 7 |
header{*Limits, Continuity and Differentiation for Complex Functions*} |
8 |
||
15131 | 9 |
theory CLim |
22979 | 10 |
imports CStar |
15131 | 11 |
begin |
14405 | 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" |
|
14469 | 19 |
by (simp add: numeral_2_eq_2) |
14405 | 20 |
|
21 |
text{*Changing the quantified variable. Install earlier?*} |
|
14738 | 22 |
lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))"; |
14405 | 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 |
|
13957 | 35 |
|
14405 | 36 |
|
37 |
subsection{*Limit of Complex to Complex Function*} |
|
38 |
||
21792 | 39 |
lemma NSLIM_Re: "f -- a --NS> L ==> (%x. Re(f x)) -- a --NS> Re(L)" |
20659
66b8455090b8
changed constants into abbreviations; shortened proofs
huffman
parents:
20563
diff
changeset
|
40 |
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff |
14469 | 41 |
hRe_hcomplex_of_complex) |
42 |
||
21792 | 43 |
lemma NSLIM_Im: "f -- a --NS> L ==> (%x. Im(f x)) -- a --NS> Im(L)" |
20659
66b8455090b8
changed constants into abbreviations; shortened proofs
huffman
parents:
20563
diff
changeset
|
44 |
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff |
14469 | 45 |
hIm_hcomplex_of_complex) |
14405 | 46 |
|
21792 | 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) |
|
14405 | 50 |
|
21792 | 51 |
lemma LIM_Im: "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)" |
52 |
by (simp add: LIM_NSLIM_iff NSLIM_Im) |
|
14405 | 53 |
|
21792 | 54 |
lemma LIM_cnj: "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L" |
55 |
by (simp add: LIM_def complex_cnj_diff [symmetric]) |
|
14405 | 56 |
|
21792 | 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]) |
|
14405 | 59 |
|
21831 | 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"" |
|
14405 | 70 |
(** another equivalence result **) |
71 |
lemma NSCLIM_NSCRLIM_iff: |
|
21792 | 72 |
"(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)" |
21831 | 73 |
by (simp add: NSLIM_def starfun_norm |
74 |
approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric]) |
|
14405 | 75 |
|
76 |
(** much, much easier standard proof **) |
|
21792 | 77 |
lemma CLIM_CRLIM_iff: "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)" |
78 |
by (simp add: LIM_def) |
|
14405 | 79 |
|
80 |
(* so this is nicer nonstandard proof *) |
|
81 |
lemma NSCLIM_NSCRLIM_iff2: |
|
21792 | 82 |
"(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)" |
83 |
by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff) |
|
14405 | 84 |
|
21792 | 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) |
|
21831 | 89 |
apply (auto simp add: NSLIM_def starfun_Re starfun_Im) |
90 |
apply (auto dest!: spec) |
|
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21831
diff
changeset
|
91 |
apply (simp add: hcomplex_approx_iff) |
14405 | 92 |
done |
93 |
||
21792 | 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) |
|
14405 | 98 |
|
99 |
||
100 |
subsection{*Continuity*} |
|
101 |
||
21792 | 102 |
lemma NSLIM_isContc_iff: |
103 |
"(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)" |
|
20659
66b8455090b8
changed constants into abbreviations; shortened proofs
huffman
parents:
20563
diff
changeset
|
104 |
by (rule NSLIM_h_iff) |
14405 | 105 |
|
106 |
subsection{*Functions from Complex to Reals*} |
|
107 |
||
21792 | 108 |
lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
21839
diff
changeset
|
109 |
by (auto intro: approx_hnorm |
14405 | 110 |
simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] |
21792 | 111 |
isNSCont_def) |
14405 | 112 |
|
21792 | 113 |
lemma isContCR_cmod [simp]: "isCont cmod (a)" |
114 |
by (simp add: isNSCont_isCont_iff [symmetric]) |
|
14405 | 115 |
|
21792 | 116 |
lemma isCont_Re: "isCont f a ==> isCont (%x. Re (f x)) a" |
117 |
by (simp add: isCont_def LIM_Re) |
|
14405 | 118 |
|
21792 | 119 |
lemma isCont_Im: "isCont f a ==> isCont (%x. Im (f x)) a" |
120 |
by (simp add: isCont_def LIM_Im) |
|
14405 | 121 |
|
122 |
subsection{* Differentiation of Natural Number Powers*} |
|
123 |
||
124 |
lemma CDERIV_pow [simp]: |
|
21792 | 125 |
"DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" |
14405 | 126 |
apply (induct_tac "n") |
23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
22979
diff
changeset
|
127 |
apply (drule_tac [2] DERIV_ident [THEN DERIV_mult]) |
15013 | 128 |
apply (auto simp add: left_distrib real_of_nat_Suc) |
14405 | 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: |
|
21792 | 135 |
"NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))" |
136 |
by (simp add: NSDERIV_DERIV_iff) |
|
14405 | 137 |
|
138 |
text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*} |
|
139 |
lemma NSCDERIV_inverse: |
|
21792 | 140 |
"(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))" |
141 |
unfolding numeral_2_eq_2 |
|
142 |
by (rule NSDERIV_inverse) |
|
14405 | 143 |
|
144 |
lemma CDERIV_inverse: |
|
21792 | 145 |
"(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))" |
146 |
unfolding numeral_2_eq_2 |
|
147 |
by (rule DERIV_inverse) |
|
14405 | 148 |
|
149 |
||
150 |
subsection{*Derivative of Reciprocals (Function @{term inverse})*} |
|
151 |
||
152 |
lemma CDERIV_inverse_fun: |
|
21792 | 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) |
|
14405 | 157 |
|
158 |
lemma NSCDERIV_inverse_fun: |
|
21792 | 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) |
|
14405 | 163 |
|
164 |
||
165 |
subsection{* Derivative of Quotient*} |
|
166 |
||
167 |
lemma CDERIV_quotient: |
|
21792 | 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) |
|
14405 | 172 |
|
173 |
lemma NSCDERIV_quotient: |
|
21792 | 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) |
|
14405 | 178 |
|
179 |
||
180 |
subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*} |
|
181 |
||
182 |
lemma CARAT_CDERIVD: |
|
21792 | 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) |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset
|
186 |
|
14405 | 187 |
end |