src/HOL/Nonstandard_Analysis/CLim.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (21 months ago) changeset 67003 49850a679c2c parent 64601 37ce6ceacbb7 child 69597 ff784d5a5bfb permissions -rw-r--r--
more robust sorted_entries;
```     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
```