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
wenzelm@62479
     1
(*  Title:      HOL/Nonstandard_Analysis/CLim.thy
wenzelm@62479
     2
    Author:     Jacques D. Fleuriot
wenzelm@62479
     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
wenzelm@64601
     7
section \<open>Limits, Continuity and Differentiation for Complex Functions\<close>
huffman@27468
     8
huffman@27468
     9
theory CLim
wenzelm@64601
    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*)
wenzelm@64601
    17
lemma lemma_complex_mult_inverse_squared [simp]: "x \<noteq> 0 \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
wenzelm@64601
    18
  for x :: complex
wenzelm@64601
    19
  by (simp add: numeral_2_eq_2)
wenzelm@64601
    20
wenzelm@64601
    21
text \<open>Changing the quantified variable. Install earlier?\<close>
wenzelm@64601
    22
lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) \<longleftrightarrow> (\<forall>x. P (x - a))"
wenzelm@64601
    23
  apply auto
wenzelm@64601
    24
  apply (drule_tac x = "x + a" in spec)
wenzelm@64601
    25
  apply (simp add: add.assoc)
wenzelm@64601
    26
  done
huffman@27468
    27
wenzelm@64601
    28
lemma complex_add_minus_iff [simp]: "x + - a = 0 \<longleftrightarrow> x = a"
wenzelm@64601
    29
  for x a :: complex
wenzelm@64601
    30
  by (simp add: diff_eq_eq)
huffman@27468
    31
wenzelm@64601
    32
lemma complex_add_eq_0_iff [iff]: "x + y = 0 \<longleftrightarrow> y = - x"
wenzelm@64601
    33
  for x y :: complex
wenzelm@64601
    34
  apply auto
wenzelm@64601
    35
  apply (drule sym [THEN diff_eq_eq [THEN iffD2]])
wenzelm@64601
    36
  apply auto
wenzelm@64601
    37
  done
huffman@27468
    38
huffman@27468
    39
wenzelm@64601
    40
subsection \<open>Limit of Complex to Complex Function\<close>
wenzelm@64601
    41
wenzelm@64601
    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"
wenzelm@64601
    43
  by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex)
huffman@27468
    44
wenzelm@64601
    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"
wenzelm@64601
    46
  by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hIm_hcomplex_of_complex)
huffman@27468
    47
wenzelm@64601
    48
lemma LIM_Re: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. Re (f x)) \<midarrow>a\<rightarrow> Re L"
wenzelm@64601
    49
  for f :: "'a::real_normed_vector \<Rightarrow> complex"
wenzelm@64601
    50
  by (simp add: LIM_NSLIM_iff NSLIM_Re)
huffman@27468
    51
wenzelm@64601
    52
lemma LIM_Im: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. Im (f x)) \<midarrow>a\<rightarrow> Im L"
wenzelm@64601
    53
  for f :: "'a::real_normed_vector \<Rightarrow> complex"
wenzelm@64601
    54
  by (simp add: LIM_NSLIM_iff NSLIM_Im)
huffman@27468
    55
wenzelm@64601
    56
lemma LIM_cnj: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L"
wenzelm@64601
    57
  for f :: "'a::real_normed_vector \<Rightarrow> complex"
wenzelm@64601
    58
  by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
huffman@27468
    59
wenzelm@64601
    60
lemma LIM_cnj_iff: "((\<lambda>x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L) \<longleftrightarrow> f \<midarrow>a\<rightarrow> L"
wenzelm@64601
    61
  for f :: "'a::real_normed_vector \<Rightarrow> complex"
wenzelm@64601
    62
  by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
huffman@27468
    63
huffman@27468
    64
lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
wenzelm@64601
    65
  by transfer (rule refl)
huffman@27468
    66
huffman@27468
    67
lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
wenzelm@64601
    68
  by transfer (rule refl)
huffman@27468
    69
huffman@27468
    70
lemma star_of_Im [simp]: "star_of (Im x) = hIm (star_of x)"
wenzelm@64601
    71
  by transfer (rule refl)
huffman@27468
    72
wenzelm@64601
    73
text \<open>Another equivalence result.\<close>
wenzelm@64601
    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"
wenzelm@64601
    75
  by (simp add: NSLIM_def starfun_norm
wenzelm@64601
    76
      approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
huffman@27468
    77
wenzelm@64601
    78
text \<open>Much, much easier standard proof.\<close>
wenzelm@64601
    79
lemma CLIM_CRLIM_iff: "f \<midarrow>x\<rightarrow> L \<longleftrightarrow> (\<lambda>y. cmod (f y - L)) \<midarrow>x\<rightarrow> 0"
wenzelm@64601
    80
  for f :: "'a::real_normed_vector \<Rightarrow> complex"
wenzelm@64601
    81
  by (simp add: LIM_eq)
huffman@27468
    82
wenzelm@64601
    83
text \<open>So this is nicer nonstandard proof.\<close>
wenzelm@64601
    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"
wenzelm@64601
    85
  by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
huffman@27468
    86
huffman@27468
    87
lemma NSLIM_NSCRLIM_Re_Im_iff:
wenzelm@64601
    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"
wenzelm@64601
    89
  apply (auto intro: NSLIM_Re NSLIM_Im)
wenzelm@64601
    90
  apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
wenzelm@64601
    91
  apply (auto dest!: spec)
wenzelm@64601
    92
  apply (simp add: hcomplex_approx_iff)
wenzelm@64601
    93
  done
wenzelm@64601
    94
wenzelm@64601
    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"
wenzelm@64601
    96
  for f :: "'a::real_normed_vector \<Rightarrow> complex"
wenzelm@64601
    97
  by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
wenzelm@64601
    98
wenzelm@64601
    99
wenzelm@64601
   100
subsection \<open>Continuity\<close>
wenzelm@64601
   101
wenzelm@64601
   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"
wenzelm@64601
   103
  by (rule NSLIM_h_iff)
huffman@27468
   104
wenzelm@64601
   105
wenzelm@64601
   106
subsection \<open>Functions from Complex to Reals\<close>
wenzelm@64601
   107
wenzelm@64601
   108
lemma isNSContCR_cmod [simp]: "isNSCont cmod a"
wenzelm@64601
   109
  by (auto intro: approx_hnorm
wenzelm@64601
   110
      simp: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] isNSCont_def)
wenzelm@64601
   111
wenzelm@64601
   112
lemma isContCR_cmod [simp]: "isCont cmod a"
wenzelm@64601
   113
  by (simp add: isNSCont_isCont_iff [symmetric])
wenzelm@64601
   114
wenzelm@64601
   115
lemma isCont_Re: "isCont f a \<Longrightarrow> isCont (\<lambda>x. Re (f x)) a"
wenzelm@64601
   116
  for f :: "'a::real_normed_vector \<Rightarrow> complex"
wenzelm@64601
   117
  by (simp add: isCont_def LIM_Re)
wenzelm@64601
   118
wenzelm@64601
   119
lemma isCont_Im: "isCont f a \<Longrightarrow> isCont (\<lambda>x. Im (f x)) a"
wenzelm@64601
   120
  for f :: "'a::real_normed_vector \<Rightarrow> complex"
wenzelm@64601
   121
  by (simp add: isCont_def LIM_Im)
huffman@27468
   122
huffman@27468
   123
wenzelm@64601
   124
subsection \<open>Differentiation of Natural Number Powers\<close>
huffman@27468
   125
wenzelm@64601
   126
lemma CDERIV_pow [simp]: "DERIV (\<lambda>x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - Suc 0))"
wenzelm@64601
   127
  apply (induct n)
wenzelm@64601
   128
   apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
wenzelm@64601
   129
   apply (auto simp add: distrib_right of_nat_Suc)
wenzelm@64601
   130
  apply (case_tac "n")
wenzelm@64601
   131
   apply (auto simp add: ac_simps)
wenzelm@64601
   132
  done
huffman@27468
   133
wenzelm@64601
   134
text \<open>Nonstandard version.\<close>
wenzelm@64601
   135
lemma NSCDERIV_pow: "NSDERIV (\<lambda>x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
wenzelm@64601
   136
  by (metis CDERIV_pow NSDERIV_DERIV_iff One_nat_def)
huffman@27468
   137
wenzelm@64601
   138
text \<open>Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero.\<close>
wenzelm@64601
   139
lemma NSCDERIV_inverse: "x \<noteq> 0 \<Longrightarrow> NSDERIV (\<lambda>x. inverse x) x :> - (inverse x)\<^sup>2"
wenzelm@64601
   140
  for x :: complex
wenzelm@64601
   141
  unfolding numeral_2_eq_2 by (rule NSDERIV_inverse)
huffman@27468
   142
wenzelm@64601
   143
lemma CDERIV_inverse: "x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse x) x :> - (inverse x)\<^sup>2"
wenzelm@64601
   144
  for x :: complex
wenzelm@64601
   145
  unfolding numeral_2_eq_2 by (rule DERIV_inverse)
huffman@27468
   146
huffman@27468
   147
wenzelm@64601
   148
subsection \<open>Derivative of Reciprocals (Function @{term inverse})\<close>
huffman@27468
   149
huffman@27468
   150
lemma CDERIV_inverse_fun:
wenzelm@64601
   151
  "DERIV f x :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse (f x)) x :> - (d * inverse ((f x)\<^sup>2))"
wenzelm@64601
   152
  for x :: complex
wenzelm@64601
   153
  unfolding numeral_2_eq_2 by (rule DERIV_inverse_fun)
huffman@27468
   154
huffman@27468
   155
lemma NSCDERIV_inverse_fun:
wenzelm@64601
   156
  "NSDERIV f x :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> NSDERIV (\<lambda>x. inverse (f x)) x :> - (d * inverse ((f x)\<^sup>2))"
wenzelm@64601
   157
  for x :: complex
wenzelm@64601
   158
  unfolding numeral_2_eq_2 by (rule NSDERIV_inverse_fun)
huffman@27468
   159
huffman@27468
   160
wenzelm@64601
   161
subsection \<open>Derivative of Quotient\<close>
huffman@27468
   162
huffman@27468
   163
lemma CDERIV_quotient:
wenzelm@64601
   164
  "DERIV f x :> d \<Longrightarrow> DERIV g x :> e \<Longrightarrow> g(x) \<noteq> 0 \<Longrightarrow>
wenzelm@64601
   165
    DERIV (\<lambda>y. f y / g y) x :> (d * g x - (e * f x)) / (g x)\<^sup>2"
wenzelm@64601
   166
  for x :: complex
wenzelm@64601
   167
  unfolding numeral_2_eq_2 by (rule DERIV_quotient)
huffman@27468
   168
huffman@27468
   169
lemma NSCDERIV_quotient:
wenzelm@64601
   170
  "NSDERIV f x :> d \<Longrightarrow> NSDERIV g x :> e \<Longrightarrow> g x \<noteq> (0::complex) \<Longrightarrow>
wenzelm@64601
   171
    NSDERIV (\<lambda>y. f y / g y) x :> (d * g x - (e * f x)) / (g x)\<^sup>2"
wenzelm@64601
   172
  unfolding numeral_2_eq_2 by (rule NSDERIV_quotient)
huffman@27468
   173
huffman@27468
   174
wenzelm@64601
   175
subsection \<open>Caratheodory Formulation of Derivative at a Point: Standard Proof\<close>
huffman@27468
   176
huffman@27468
   177
lemma CARAT_CDERIVD:
wenzelm@64601
   178
  "(\<forall>z. f z - f x = g z * (z - x)) \<and> isNSCont g x \<and> g x = l \<Longrightarrow> NSDERIV f x :> l"
wenzelm@64601
   179
  by clarify (rule CARAT_DERIVD)
huffman@27468
   180
huffman@27468
   181
end