author | wenzelm |
Mon, 15 Feb 2016 14:55:44 +0100 | |
changeset 62337 | d3996d5873dd |
parent 61976 | 3a27957ac658 |
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 |
||
61975 | 7 |
section\<open>Limits, Continuity and Differentiation for Complex Functions\<close> |
27468 | 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 |
||
61975 | 21 |
text\<open>Changing the quantified variable. Install earlier?\<close> |
58860 | 22 |
lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))" |
27468 | 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 |
||
61975 | 37 |
subsection\<open>Limit of Complex to Complex Function\<close> |
27468 | 38 |
|
61971 | 39 |
lemma NSLIM_Re: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L)" |
27468 | 40 |
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff |
41 |
hRe_hcomplex_of_complex) |
|
42 |
||
61971 | 43 |
lemma NSLIM_Im: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Im(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im(L)" |
27468 | 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" |
61976 | 50 |
shows "f \<midarrow>a\<rightarrow> L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow> 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" |
61976 | 55 |
shows "f \<midarrow>a\<rightarrow> L ==> (%x. Im(f x)) \<midarrow>a\<rightarrow> 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" |
61976 | 60 |
shows "f \<midarrow>a\<rightarrow> L ==> (%x. cnj (f x)) \<midarrow>a\<rightarrow> 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" |
61976 | 65 |
shows "((%x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L) = (f \<midarrow>a\<rightarrow> 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: |
|
61971 | 80 |
"(f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0)" |
27468 | 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" |
61976 | 87 |
shows "(f \<midarrow>x\<rightarrow> L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow> 0)" |
31338
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: |
|
61971 | 92 |
"(f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0)" |
27468 | 93 |
by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff) |
94 |
||
95 |
lemma NSLIM_NSCRLIM_Re_Im_iff: |
|
61971 | 96 |
"(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L) = ((%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L) & |
97 |
(%x. Im(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im(L))" |
|
27468 | 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" |
61976 | 106 |
shows "(f \<midarrow>a\<rightarrow> L) = ((%x. Re(f x)) \<midarrow>a\<rightarrow> Re(L) & |
107 |
(%x. Im(f x)) \<midarrow>a\<rightarrow> Im(L))" |
|
27468 | 108 |
by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff) |
109 |
||
110 |
||
61975 | 111 |
subsection\<open>Continuity\<close> |
27468 | 112 |
|
113 |
lemma NSLIM_isContc_iff: |
|
61971 | 114 |
"(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)" |
27468 | 115 |
by (rule NSLIM_h_iff) |
116 |
||
61975 | 117 |
subsection\<open>Functions from Complex to Reals\<close> |
27468 | 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 |
||
61975 | 137 |
subsection\<open>Differentiation of Natural Number Powers\<close> |
27468 | 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]) |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
58878
diff
changeset
|
143 |
apply (auto simp add: distrib_right of_nat_Suc) |
27468 | 144 |
apply (case_tac "n") |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
58878
diff
changeset
|
145 |
apply (auto simp add: ac_simps) |
27468 | 146 |
done |
147 |
||
61975 | 148 |
text\<open>Nonstandard version\<close> |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
58878
diff
changeset
|
149 |
lemma NSCDERIV_pow: "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
58878
diff
changeset
|
150 |
by (metis CDERIV_pow NSDERIV_DERIV_iff One_nat_def) |
27468 | 151 |
|
61975 | 152 |
text\<open>Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero\<close> |
27468 | 153 |
lemma NSCDERIV_inverse: |
53077 | 154 |
"(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))" |
27468 | 155 |
unfolding numeral_2_eq_2 |
156 |
by (rule NSDERIV_inverse) |
|
157 |
||
158 |
lemma CDERIV_inverse: |
|
53077 | 159 |
"(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))" |
27468 | 160 |
unfolding numeral_2_eq_2 |
161 |
by (rule DERIV_inverse) |
|
162 |
||
163 |
||
61975 | 164 |
subsection\<open>Derivative of Reciprocals (Function @{term inverse})\<close> |
27468 | 165 |
|
166 |
lemma CDERIV_inverse_fun: |
|
167 |
"[| DERIV f x :> d; f(x) \<noteq> (0::complex) |] |
|
53077 | 168 |
==> DERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))" |
27468 | 169 |
unfolding numeral_2_eq_2 |
170 |
by (rule DERIV_inverse_fun) |
|
171 |
||
172 |
lemma NSCDERIV_inverse_fun: |
|
173 |
"[| NSDERIV f x :> d; f(x) \<noteq> (0::complex) |] |
|
53077 | 174 |
==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse ((f x)\<^sup>2)))" |
27468 | 175 |
unfolding numeral_2_eq_2 |
176 |
by (rule NSDERIV_inverse_fun) |
|
177 |
||
178 |
||
61975 | 179 |
subsection\<open>Derivative of Quotient\<close> |
27468 | 180 |
|
181 |
lemma CDERIV_quotient: |
|
182 |
"[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |] |
|
53077 | 183 |
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)" |
27468 | 184 |
unfolding numeral_2_eq_2 |
185 |
by (rule DERIV_quotient) |
|
186 |
||
187 |
lemma NSCDERIV_quotient: |
|
188 |
"[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> (0::complex) |] |
|
53077 | 189 |
==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / ((g x)\<^sup>2)" |
27468 | 190 |
unfolding numeral_2_eq_2 |
191 |
by (rule NSDERIV_quotient) |
|
192 |
||
193 |
||
61975 | 194 |
subsection\<open>Caratheodory Formulation of Derivative at a Point: Standard Proof\<close> |
27468 | 195 |
|
196 |
lemma CARAT_CDERIVD: |
|
197 |
"(\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l |
|
198 |
==> NSDERIV f x :> l" |
|
199 |
by clarify (rule CARAT_DERIVD) |
|
200 |
||
201 |
end |