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