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