1(*  Title:      HOL/Nonstandard_Analysis/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
7section \<open>Limits, Continuity and Differentiation for Complex Functions\<close>
8
9theory CLim
10  imports CStar
11begin
12
13(*not in simpset?*)
14declare epsilon_not_zero [simp]
15
16(*??generalize*)
17lemma lemma_complex_mult_inverse_squared [simp]: "x \<noteq> 0 \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
18  for x :: complex
19  by (simp add: numeral_2_eq_2)
20
21text \<open>Changing the quantified variable. Install earlier?\<close>
22lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) \<longleftrightarrow> (\<forall>x. P (x - a))"
23  apply auto
24  apply (drule_tac x = "x + a" in spec)
25  apply (simp add: add.assoc)
26  done
27
28lemma complex_add_minus_iff [simp]: "x + - a = 0 \<longleftrightarrow> x = a"
29  for x a :: complex
30  by (simp add: diff_eq_eq)
31
32lemma complex_add_eq_0_iff [iff]: "x + y = 0 \<longleftrightarrow> y = - x"
33  for x y :: complex
34  apply auto
35  apply (drule sym [THEN diff_eq_eq [THEN iffD2]])
36  apply auto
37  done
38
39
40subsection \<open>Limit of Complex to Complex Function\<close>
41
42lemma 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"
43  by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex)
44
45lemma 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"
46  by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hIm_hcomplex_of_complex)
47
48lemma LIM_Re: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. Re (f x)) \<midarrow>a\<rightarrow> Re L"
49  for f :: "'a::real_normed_vector \<Rightarrow> complex"
50  by (simp add: LIM_NSLIM_iff NSLIM_Re)
51
52lemma LIM_Im: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. Im (f x)) \<midarrow>a\<rightarrow> Im L"
53  for f :: "'a::real_normed_vector \<Rightarrow> complex"
54  by (simp add: LIM_NSLIM_iff NSLIM_Im)
55
56lemma LIM_cnj: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L"
57  for f :: "'a::real_normed_vector \<Rightarrow> complex"
58  by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
59
60lemma LIM_cnj_iff: "((\<lambda>x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L) \<longleftrightarrow> f \<midarrow>a\<rightarrow> L"
61  for f :: "'a::real_normed_vector \<Rightarrow> complex"
62  by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
63
64lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
65  by transfer (rule refl)
66
67lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
68  by transfer (rule refl)
69
70lemma star_of_Im [simp]: "star_of (Im x) = hIm (star_of x)"
71  by transfer (rule refl)
72
73text \<open>Another equivalence result.\<close>
74lemma 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"
75  by (simp add: NSLIM_def starfun_norm
76      approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
77
78text \<open>Much, much easier standard proof.\<close>
79lemma CLIM_CRLIM_iff: "f \<midarrow>x\<rightarrow> L \<longleftrightarrow> (\<lambda>y. cmod (f y - L)) \<midarrow>x\<rightarrow> 0"
80  for f :: "'a::real_normed_vector \<Rightarrow> complex"
81  by (simp add: LIM_eq)
82
83text \<open>So this is nicer nonstandard proof.\<close>
84lemma 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"
85  by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
86
87lemma NSLIM_NSCRLIM_Re_Im_iff:
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"
89  apply (auto intro: NSLIM_Re NSLIM_Im)
90  apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
91  apply (auto dest!: spec)
92  apply (simp add: hcomplex_approx_iff)
93  done
94
95lemma 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"
96  for f :: "'a::real_normed_vector \<Rightarrow> complex"
97  by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
98
99
100subsection \<open>Continuity\<close>
101
102lemma 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"
103  by (rule NSLIM_at0_iff)
104
105
106subsection \<open>Functions from Complex to Reals\<close>
107
108lemma isNSContCR_cmod [simp]: "isNSCont cmod a"
109  by (auto intro: approx_hnorm
110      simp: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] isNSCont_def)
111
112lemma isContCR_cmod [simp]: "isCont cmod a"
113  by (simp add: isNSCont_isCont_iff [symmetric])
114
115lemma 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
119lemma 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
124subsection \<open>Differentiation of Natural Number Powers\<close>
125
126lemma 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
134text \<open>Nonstandard version.\<close>
135lemma 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
138text \<open>Can't relax the premise \<^term>\<open>x \<noteq> 0\<close>: it isn't continuous at zero.\<close>
139lemma 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
143lemma 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
148subsection \<open>Derivative of Reciprocals (Function \<^term>\<open>inverse\<close>)\<close>
149
150lemma CDERIV_inverse_fun:
151  "DERIV f x :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse (f x)) x :> - (d * inverse ((f x)\<^sup>2))"
152  for x :: complex
153  unfolding numeral_2_eq_2 by (rule DERIV_inverse_fun)
154
155lemma NSCDERIV_inverse_fun:
156  "NSDERIV f x :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> NSDERIV (\<lambda>x. inverse (f x)) x :> - (d * inverse ((f x)\<^sup>2))"
157  for x :: complex
158  unfolding numeral_2_eq_2 by (rule NSDERIV_inverse_fun)
159
160
161subsection \<open>Derivative of Quotient\<close>
162
163lemma CDERIV_quotient:
164  "DERIV f x :> d \<Longrightarrow> DERIV g x :> e \<Longrightarrow> g(x) \<noteq> 0 \<Longrightarrow>
165    DERIV (\<lambda>y. f y / g y) x :> (d * g x - (e * f x)) / (g x)\<^sup>2"
166  for x :: complex
167  unfolding numeral_2_eq_2 by (rule DERIV_quotient)
168
169lemma NSCDERIV_quotient:
170  "NSDERIV f x :> d \<Longrightarrow> NSDERIV g x :> e \<Longrightarrow> g x \<noteq> (0::complex) \<Longrightarrow>
171    NSDERIV (\<lambda>y. f y / g y) x :> (d * g x - (e * f x)) / (g x)\<^sup>2"
172  unfolding numeral_2_eq_2 by (rule NSDERIV_quotient)
173
174
175subsection \<open>Caratheodory Formulation of Derivative at a Point: Standard Proof\<close>
176
177lemma CARAT_CDERIVD:
178  "(\<forall>z. f z - f x = g z * (z - x)) \<and> isNSCont g x \<and> g x = l \<Longrightarrow> NSDERIV f x :> l"
179  by clarify (rule CARAT_DERIVD)
180
181end
182