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