src/HOL/Nonstandard_Analysis/CLim.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64601 37ce6ceacbb7
child 69597 ff784d5a5bfb
permissions -rw-r--r--
executable domain membership checks
     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 
     7 section \<open>Limits, Continuity and Differentiation for Complex Functions\<close>
     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]: "x \<noteq> 0 \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
    18   for x :: complex
    19   by (simp add: numeral_2_eq_2)
    20 
    21 text \<open>Changing the quantified variable. Install earlier?\<close>
    22 lemma 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 
    28 lemma complex_add_minus_iff [simp]: "x + - a = 0 \<longleftrightarrow> x = a"
    29   for x a :: complex
    30   by (simp add: diff_eq_eq)
    31 
    32 lemma 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 
    40 subsection \<open>Limit of Complex to Complex Function\<close>
    41 
    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"
    43   by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex)
    44 
    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"
    46   by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hIm_hcomplex_of_complex)
    47 
    48 lemma 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 
    52 lemma 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 
    56 lemma 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 
    60 lemma 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 
    64 lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
    65   by transfer (rule refl)
    66 
    67 lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
    68   by transfer (rule refl)
    69 
    70 lemma star_of_Im [simp]: "star_of (Im x) = hIm (star_of x)"
    71   by transfer (rule refl)
    72 
    73 text \<open>Another equivalence result.\<close>
    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"
    75   by (simp add: NSLIM_def starfun_norm
    76       approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
    77 
    78 text \<open>Much, much easier standard proof.\<close>
    79 lemma 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 
    83 text \<open>So this is nicer nonstandard proof.\<close>
    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"
    85   by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
    86 
    87 lemma 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 
    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"
    96   for f :: "'a::real_normed_vector \<Rightarrow> complex"
    97   by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
    98 
    99 
   100 subsection \<open>Continuity\<close>
   101 
   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"
   103   by (rule NSLIM_h_iff)
   104 
   105 
   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>
   149 
   150 lemma 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 
   155 lemma 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 
   161 subsection \<open>Derivative of Quotient\<close>
   162 
   163 lemma 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 
   169 lemma 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 
   175 subsection \<open>Caratheodory Formulation of Derivative at a Point: Standard Proof\<close>
   176 
   177 lemma 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 
   181 end