src/HOL/Complex/CLim.thy
 author wenzelm Fri Mar 28 19:43:54 2008 +0100 (2008-03-28) changeset 26462 dac4e2bce00d parent 23077 be166bf115d4 child 27105 5f139027c365 permissions -rw-r--r--
avoid rebinding of existing facts;
```     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
```
```     7 header{*Limits, Continuity and Differentiation for Complex Functions*}
```
```     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]:
```
```    18      "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"
```
```    19 by (simp add: numeral_2_eq_2)
```
```    20
```
```    21 text{*Changing the quantified variable. Install earlier?*}
```
```    22 lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))";
```
```    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
```
```    35
```
```    36
```
```    37 subsection{*Limit of Complex to Complex Function*}
```
```    38
```
```    39 lemma NSLIM_Re: "f -- a --NS> L ==> (%x. Re(f x)) -- a --NS> Re(L)"
```
```    40 by (simp add: NSLIM_def starfunC_approx_Re_Im_iff
```
```    41               hRe_hcomplex_of_complex)
```
```    42
```
```    43 lemma NSLIM_Im: "f -- a --NS> L ==> (%x. Im(f x)) -- a --NS> Im(L)"
```
```    44 by (simp add: NSLIM_def starfunC_approx_Re_Im_iff
```
```    45               hIm_hcomplex_of_complex)
```
```    46
```
```    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)
```
```    50
```
```    51 lemma LIM_Im: "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
```
```    52 by (simp add: LIM_NSLIM_iff NSLIM_Im)
```
```    53
```
```    54 lemma LIM_cnj: "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
```
```    55 by (simp add: LIM_def complex_cnj_diff [symmetric])
```
```    56
```
```    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])
```
```    59
```
```    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""
```
```    70 (** another equivalence result **)
```
```    71 lemma NSCLIM_NSCRLIM_iff:
```
```    72    "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
```
```    73 by (simp add: NSLIM_def starfun_norm
```
```    74     approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
```
```    75
```
```    76 (** much, much easier standard proof **)
```
```    77 lemma CLIM_CRLIM_iff: "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
```
```    78 by (simp add: LIM_def)
```
```    79
```
```    80 (* so this is nicer nonstandard proof *)
```
```    81 lemma NSCLIM_NSCRLIM_iff2:
```
```    82      "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
```
```    83 by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
```
```    84
```
```    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)
```
```    89 apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
```
```    90 apply (auto dest!: spec)
```
```    91 apply (simp add: hcomplex_approx_iff)
```
```    92 done
```
```    93
```
```    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)
```
```    98
```
```    99
```
```   100 subsection{*Continuity*}
```
```   101
```
```   102 lemma NSLIM_isContc_iff:
```
```   103      "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
```
```   104 by (rule NSLIM_h_iff)
```
```   105
```
```   106 subsection{*Functions from Complex to Reals*}
```
```   107
```
```   108 lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)"
```
```   109 by (auto intro: approx_hnorm
```
```   110          simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric]
```
```   111                     isNSCont_def)
```
```   112
```
```   113 lemma isContCR_cmod [simp]: "isCont cmod (a)"
```
```   114 by (simp add: isNSCont_isCont_iff [symmetric])
```
```   115
```
```   116 lemma isCont_Re: "isCont f a ==> isCont (%x. Re (f x)) a"
```
```   117 by (simp add: isCont_def LIM_Re)
```
```   118
```
```   119 lemma isCont_Im: "isCont f a ==> isCont (%x. Im (f x)) a"
```
```   120 by (simp add: isCont_def LIM_Im)
```
```   121
```
```   122 subsection{* Differentiation of Natural Number Powers*}
```
```   123
```
```   124 lemma CDERIV_pow [simp]:
```
```   125      "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
```
```   126 apply (induct_tac "n")
```
```   127 apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
```
```   128 apply (auto simp add: left_distrib real_of_nat_Suc)
```
```   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:
```
```   135      "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
```
```   136 by (simp add: NSDERIV_DERIV_iff)
```
```   137
```
```   138 text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
```
```   139 lemma NSCDERIV_inverse:
```
```   140      "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
```
```   141 unfolding numeral_2_eq_2
```
```   142 by (rule NSDERIV_inverse)
```
```   143
```
```   144 lemma CDERIV_inverse:
```
```   145      "(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"
```
```   146 unfolding numeral_2_eq_2
```
```   147 by (rule DERIV_inverse)
```
```   148
```
```   149
```
```   150 subsection{*Derivative of Reciprocals (Function @{term inverse})*}
```
```   151
```
```   152 lemma CDERIV_inverse_fun:
```
```   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)
```
```   157
```
```   158 lemma NSCDERIV_inverse_fun:
```
```   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)
```
```   163
```
```   164
```
```   165 subsection{* Derivative of Quotient*}
```
```   166
```
```   167 lemma CDERIV_quotient:
```
```   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)
```
```   172
```
```   173 lemma NSCDERIV_quotient:
```
```   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)
```
```   178
```
```   179
```
```   180 subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*}
```
```   181
```
```   182 lemma CARAT_CDERIVD:
```
```   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)
```
```   186
```
```   187 end
```