src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
author paulson <lp15@cam.ac.uk>
Thu Mar 19 14:24:51 2015 +0000 (2015-03-19)
changeset 59751 916c0f6c83e3
parent 59746 ddae5727c5a9
child 59862 44b3f4fa33ca
permissions -rw-r--r--
New material for complex sin, cos, tan, Ln, also some reorganisation
     1 (*  Author: John Harrison
     2     Ported from "hol_light/Multivariate/transcendentals.ml" by L C Paulson (2015)
     3 *)
     4 
     5 section {* Complex Transcendental Functions *}
     6 
     7 theory Complex_Transcendental
     8 imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
     9 begin
    10 
    11 subsection{*The Exponential Function is Differentiable and Continuous*}
    12 
    13 lemma complex_differentiable_at_exp: "exp complex_differentiable at z"
    14   using DERIV_exp complex_differentiable_def by blast
    15 
    16 lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
    17   by (simp add: complex_differentiable_at_exp complex_differentiable_at_within)
    18 
    19 lemma continuous_within_exp:
    20   fixes z::"'a::{real_normed_field,banach}"
    21   shows "continuous (at z within s) exp"
    22 by (simp add: continuous_at_imp_continuous_within)
    23 
    24 lemma continuous_on_exp:
    25   fixes s::"'a::{real_normed_field,banach} set"
    26   shows "continuous_on s exp"
    27 by (simp add: continuous_on_exp continuous_on_id)
    28 
    29 lemma holomorphic_on_exp: "exp holomorphic_on s"
    30   by (simp add: complex_differentiable_within_exp holomorphic_on_def)
    31 
    32 subsection{*Euler and de Moivre formulas.*}
    33 
    34 text{*The sine series times @{term i}*}
    35 lemma sin_ii_eq: "(\<lambda>n. (ii * sin_coeff n) * z^n) sums (ii * sin z)"
    36 proof -
    37   have "(\<lambda>n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)"
    38     using sin_converges sums_mult by blast
    39   then show ?thesis
    40     by (simp add: scaleR_conv_of_real field_simps)
    41 qed
    42 
    43 theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)"
    44 proof -
    45   have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) 
    46         = (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))"
    47   proof
    48     fix n
    49     show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)"
    50       by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
    51   qed
    52   also have "... sums (exp (ii * z))"
    53     by (rule exp_converges)
    54   finally have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (exp (ii * z))" .
    55   moreover have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (cos z + ii * sin z)"
    56     using sums_add [OF cos_converges [of z] sin_ii_eq [of z]]
    57     by (simp add: field_simps scaleR_conv_of_real)
    58   ultimately show ?thesis
    59     using sums_unique2 by blast
    60 qed
    61 
    62 corollary exp_minus_Euler: "exp(-(ii * z)) = cos(z) - ii * sin(z)"
    63   using exp_Euler [of "-z"]
    64   by simp
    65 
    66 lemma sin_exp_eq: "sin z = (exp(ii * z) - exp(-(ii * z))) / (2*ii)"
    67   by (simp add: exp_Euler exp_minus_Euler)
    68 
    69 lemma sin_exp_eq': "sin z = ii * (exp(-(ii * z)) - exp(ii * z)) / 2"
    70   by (simp add: exp_Euler exp_minus_Euler)
    71 
    72 lemma cos_exp_eq:  "cos z = (exp(ii * z) + exp(-(ii * z))) / 2"
    73   by (simp add: exp_Euler exp_minus_Euler)
    74 
    75 subsection{*Relationships between real and complex trig functions*}
    76 
    77 declare sin_of_real [simp] cos_of_real [simp]
    78 
    79 lemma real_sin_eq [simp]:
    80   fixes x::real
    81   shows "Re(sin(of_real x)) = sin x"
    82   by (simp add: sin_of_real)
    83   
    84 lemma real_cos_eq [simp]:
    85   fixes x::real
    86   shows "Re(cos(of_real x)) = cos x"
    87   by (simp add: cos_of_real)
    88 
    89 lemma DeMoivre: "(cos z + ii * sin z) ^ n = cos(n * z) + ii * sin(n * z)"
    90   apply (simp add: exp_Euler [symmetric])
    91   by (metis exp_of_nat_mult mult.left_commute)
    92 
    93 lemma exp_cnj:
    94   fixes z::complex
    95   shows "cnj (exp z) = exp (cnj z)"
    96 proof -
    97   have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))"
    98     by auto
    99   also have "... sums (exp (cnj z))"
   100     by (rule exp_converges)
   101   finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
   102   moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
   103     by (metis exp_converges sums_cnj) 
   104   ultimately show ?thesis
   105     using sums_unique2
   106     by blast 
   107 qed
   108 
   109 lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
   110   by (simp add: sin_exp_eq exp_cnj field_simps)
   111 
   112 lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
   113   by (simp add: cos_exp_eq exp_cnj field_simps)
   114 
   115 lemma exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
   116   by (metis Reals_cases Reals_of_real exp_of_real)
   117 
   118 lemma sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
   119   by (metis Reals_cases Reals_of_real sin_of_real)
   120 
   121 lemma cos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> cos z \<in> \<real>"
   122   by (metis Reals_cases Reals_of_real cos_of_real)
   123 
   124 lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
   125   using DERIV_sin complex_differentiable_def by blast
   126 
   127 lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)"
   128   by (simp add: complex_differentiable_at_sin complex_differentiable_at_within)
   129 
   130 lemma complex_differentiable_at_cos: "cos complex_differentiable at z"
   131   using DERIV_cos complex_differentiable_def by blast
   132 
   133 lemma complex_differentiable_within_cos: "cos complex_differentiable (at z within s)"
   134   by (simp add: complex_differentiable_at_cos complex_differentiable_at_within)
   135 
   136 lemma holomorphic_on_sin: "sin holomorphic_on s"
   137   by (simp add: complex_differentiable_within_sin holomorphic_on_def)
   138 
   139 lemma holomorphic_on_cos: "cos holomorphic_on s"
   140   by (simp add: complex_differentiable_within_cos holomorphic_on_def)
   141 
   142 subsection{* Get a nice real/imaginary separation in Euler's formula.*}
   143 
   144 lemma Euler: "exp(z) = of_real(exp(Re z)) * 
   145               (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
   146 by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
   147 
   148 lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   149   by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
   150 
   151 lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
   152   by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
   153 
   154 lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   155   by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
   156 
   157 lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
   158   by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
   159   
   160 subsection{*More on the Polar Representation of Complex Numbers*}
   161 
   162 lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
   163   by (simp add: exp_add exp_Euler exp_of_real)
   164 
   165 lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
   166 apply auto
   167 apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
   168 apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1) real_of_int_def)
   169 by (metis Im_exp Re_exp complex_Re_Im_cancel_iff cos_one_2pi_int sin_double Re_complex_of_real complex_Re_numeral exp_zero mult.assoc mult.left_commute mult_eq_0_iff mult_numeral_1 numeral_One of_real_0 real_of_int_def sin_zero_iff_int2)
   170 
   171 lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * ii)"
   172                 (is "?lhs = ?rhs")
   173 proof -
   174   have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
   175     by (simp add: exp_diff)
   176   also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
   177     by (simp add: exp_eq_1)
   178   also have "... \<longleftrightarrow> ?rhs"
   179     by (auto simp: algebra_simps intro!: complex_eqI)
   180   finally show ?thesis .
   181 qed
   182 
   183 lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
   184   by (auto simp: exp_eq abs_mult)
   185 
   186 lemma exp_integer_2pi: 
   187   assumes "n \<in> Ints"
   188   shows "exp((2 * n * pi) * ii) = 1"
   189 proof -
   190   have "exp((2 * n * pi) * ii) = exp 0"
   191     using assms
   192     by (simp only: Ints_def exp_eq) auto
   193   also have "... = 1"
   194     by simp
   195   finally show ?thesis .
   196 qed
   197 
   198 lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
   199 proof -
   200   { assume "sin y = sin x" "cos y = cos x"
   201     then have "cos (y-x) = 1"
   202       using cos_add [of y "-x"] by simp
   203     then have "\<exists>n::int. y-x = real n * 2 * pi"
   204       using cos_one_2pi_int by blast }
   205   then show ?thesis
   206   apply (auto simp: sin_add cos_add)
   207   apply (metis add.commute diff_add_cancel mult.commute)
   208   done
   209 qed
   210 
   211 lemma exp_i_ne_1: 
   212   assumes "0 < x" "x < 2*pi"
   213   shows "exp(\<i> * of_real x) \<noteq> 1"
   214 proof 
   215   assume "exp (\<i> * of_real x) = 1"
   216   then have "exp (\<i> * of_real x) = exp 0"
   217     by simp
   218   then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
   219     by (simp only: Ints_def exp_eq) auto
   220   then have  "of_real x = (of_int (2 * n) * pi)"
   221     by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
   222   then have  "x = (of_int (2 * n) * pi)"
   223     by simp
   224   then show False using assms
   225     by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
   226 qed
   227 
   228 lemma sin_eq_0: 
   229   fixes z::complex
   230   shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
   231   by (simp add: sin_exp_eq exp_eq of_real_numeral)
   232 
   233 lemma cos_eq_0: 
   234   fixes z::complex
   235   shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
   236   using sin_eq_0 [of "z - of_real pi/2"]
   237   by (simp add: sin_diff algebra_simps)
   238 
   239 lemma cos_eq_1: 
   240   fixes z::complex
   241   shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
   242 proof -
   243   have "cos z = cos (2*(z/2))"
   244     by simp
   245   also have "... = 1 - 2 * sin (z/2) ^ 2"
   246     by (simp only: cos_double_sin)
   247   finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
   248     by simp
   249   show ?thesis
   250     by (auto simp: sin_eq_0 of_real_numeral)
   251 qed  
   252 
   253 lemma csin_eq_1:
   254   fixes z::complex
   255   shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)"
   256   using cos_eq_1 [of "z - of_real pi/2"]
   257   by (simp add: cos_diff algebra_simps)
   258 
   259 lemma csin_eq_minus1:
   260   fixes z::complex
   261   shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)"
   262         (is "_ = ?rhs")
   263 proof -
   264   have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
   265     by (simp add: equation_minus_iff)
   266   also have "...  \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
   267     by (simp only: csin_eq_1)
   268   also have "...  \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
   269     apply (rule iff_exI)
   270     by (metis (no_types)  is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff)
   271   also have "... = ?rhs"
   272     apply (auto simp: of_real_numeral)
   273     apply (rule_tac [2] x="-(x+1)" in exI)
   274     apply (rule_tac x="-(x+1)" in exI)
   275     apply (simp_all add: algebra_simps)
   276     done
   277   finally show ?thesis .
   278 qed  
   279 
   280 lemma ccos_eq_minus1: 
   281   fixes z::complex
   282   shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
   283   using csin_eq_1 [of "z - of_real pi/2"]
   284   apply (simp add: sin_diff)
   285   apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
   286   done       
   287 
   288 lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
   289                 (is "_ = ?rhs")
   290 proof -
   291   have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
   292     by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
   293   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
   294     by (simp only: csin_eq_1)
   295   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
   296     apply (rule iff_exI)
   297     apply (auto simp: algebra_simps of_real_numeral)
   298     apply (rule injD [OF inj_of_real [where 'a = complex]])
   299     apply (auto simp: of_real_numeral)
   300     done
   301   also have "... = ?rhs"
   302     by (auto simp: algebra_simps)
   303   finally show ?thesis .
   304 qed  
   305 
   306 lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
   307 proof -
   308   have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
   309     by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
   310   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
   311     by (simp only: csin_eq_minus1)
   312   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
   313     apply (rule iff_exI)
   314     apply (auto simp: algebra_simps)
   315     apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
   316     done
   317   also have "... = ?rhs"
   318     by (auto simp: algebra_simps)
   319   finally show ?thesis .
   320 qed  
   321 
   322 lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
   323                       (is "_ = ?rhs")
   324 proof -
   325   have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
   326     by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
   327   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
   328     by (simp only: ccos_eq_minus1)
   329   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
   330     apply (rule iff_exI)
   331     apply (auto simp: algebra_simps)
   332     apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
   333     done
   334   also have "... = ?rhs"
   335     by (auto simp: algebra_simps)
   336   finally show ?thesis .
   337 qed  
   338 
   339 lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
   340   apply (simp add: exp_Euler cmod_def power2_diff algebra_simps)
   341   using cos_double_sin [of "t/2"]
   342   apply (simp add: real_sqrt_mult)
   343   done
   344 
   345 lemma sinh_complex:
   346   fixes z :: complex
   347   shows "(exp z - inverse (exp z)) / 2 = -ii * sin(ii * z)"
   348   by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
   349 
   350 lemma sin_ii_times:
   351   fixes z :: complex
   352   shows "sin(ii * z) = ii * ((exp z - inverse (exp z)) / 2)"
   353   using sinh_complex by auto
   354 
   355 lemma sinh_real:
   356   fixes x :: real
   357   shows "of_real((exp x - inverse (exp x)) / 2) = -ii * sin(ii * of_real x)"
   358   by (simp add: exp_of_real sin_ii_times of_real_numeral)
   359 
   360 lemma cosh_complex:
   361   fixes z :: complex
   362   shows "(exp z + inverse (exp z)) / 2 = cos(ii * z)"
   363   by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
   364 
   365 lemma cosh_real:
   366   fixes x :: real
   367   shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)"
   368   by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
   369 
   370 lemmas cos_ii_times = cosh_complex [symmetric]
   371 
   372 lemma norm_cos_squared: 
   373     "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
   374   apply (cases z)
   375   apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
   376   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
   377   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   378   apply (simp add: sin_squared_eq)
   379   apply (simp add: power2_eq_square algebra_simps divide_simps)
   380   done
   381 
   382 lemma norm_sin_squared:
   383     "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
   384   apply (cases z)
   385   apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
   386   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
   387   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   388   apply (simp add: cos_squared_eq)
   389   apply (simp add: power2_eq_square algebra_simps divide_simps)
   390   done 
   391 
   392 lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
   393   using abs_Im_le_cmod linear order_trans by fastforce
   394 
   395 lemma norm_cos_le: 
   396   fixes z::complex
   397   shows "norm(cos z) \<le> exp(norm z)"
   398 proof -
   399   have "Im z \<le> cmod z"
   400     using abs_Im_le_cmod abs_le_D1 by auto
   401   with exp_uminus_Im show ?thesis
   402     apply (simp add: cos_exp_eq norm_divide)
   403     apply (rule order_trans [OF norm_triangle_ineq], simp)
   404     apply (metis add_mono exp_le_cancel_iff mult_2_right)
   405     done
   406 qed
   407 
   408 lemma norm_cos_plus1_le: 
   409   fixes z::complex
   410   shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
   411 proof -
   412   have mono: "\<And>u w z::real. (1 \<le> w | 1 \<le> z) \<Longrightarrow> (w \<le> u & z \<le> u) \<Longrightarrow> 2 + w + z \<le> 4 * u"
   413       by arith
   414   have *: "Im z \<le> cmod z"
   415     using abs_Im_le_cmod abs_le_D1 by auto
   416   have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)"
   417     by (simp add: norm_add_rule_thm)
   418   have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
   419     by (simp add: cos_exp_eq)
   420   also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
   421     by (simp add: field_simps)
   422   also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
   423     by (simp add: norm_divide)
   424   finally show ?thesis
   425     apply (rule ssubst, simp)
   426     apply (rule order_trans [OF triangle3], simp)
   427     using exp_uminus_Im *
   428     apply (auto intro: mono)
   429     done
   430 qed
   431 
   432 subsection{* Taylor series for complex exponential, sine and cosine.*}
   433 
   434 context 
   435 begin
   436 
   437 declare power_Suc [simp del]
   438 
   439 lemma Taylor_exp: 
   440   "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   441 proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
   442   show "convex (closed_segment 0 z)"
   443     by (rule convex_segment [of 0 z])
   444 next
   445   fix k x
   446   assume "x \<in> closed_segment 0 z" "k \<le> n"
   447   show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
   448     using DERIV_exp DERIV_subset by blast
   449 next
   450   fix x
   451   assume "x \<in> closed_segment 0 z"
   452   then show "Re x \<le> \<bar>Re z\<bar>"
   453     apply (auto simp: closed_segment_def scaleR_conv_of_real)
   454     by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans)
   455 next
   456   show "0 \<in> closed_segment 0 z"
   457     by (auto simp: closed_segment_def)
   458 next
   459   show "z \<in> closed_segment 0 z"
   460     apply (simp add: closed_segment_def scaleR_conv_of_real)
   461     using of_real_1 zero_le_one by blast
   462 qed 
   463 
   464 lemma 
   465   assumes "0 \<le> u" "u \<le> 1"
   466   shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" 
   467     and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   468 proof -
   469   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   470     by arith
   471   show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
   472     apply (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
   473     apply (rule order_trans [OF norm_triangle_ineq4])
   474     apply (rule mono)
   475     apply (auto simp: abs_if mult_left_le_one_le)
   476     apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
   477     apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   478     done
   479   show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
   480     apply (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
   481     apply (rule order_trans [OF norm_triangle_ineq])
   482     apply (rule mono)
   483     apply (auto simp: abs_if mult_left_le_one_le)
   484     apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
   485     apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   486     done
   487 qed
   488     
   489 lemma Taylor_sin: 
   490   "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) 
   491    \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   492 proof -
   493   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   494       by arith
   495   have *: "cmod (sin z -
   496                  (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
   497            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
   498   proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" "exp\<bar>Im z\<bar>" 0 z,
   499 simplified])
   500   show "convex (closed_segment 0 z)"
   501     by (rule convex_segment [of 0 z])
   502   next
   503     fix k x
   504     show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
   505             (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
   506             (at x within closed_segment 0 z)"
   507       apply (auto simp: power_Suc)
   508       apply (intro derivative_eq_intros | simp)+
   509       done
   510   next
   511     fix x
   512     assume "x \<in> closed_segment 0 z"
   513     then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
   514       by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
   515   next
   516     show "0 \<in> closed_segment 0 z"
   517       by (auto simp: closed_segment_def)
   518   next
   519     show "z \<in> closed_segment 0 z"
   520       apply (simp add: closed_segment_def scaleR_conv_of_real)
   521       using of_real_1 zero_le_one by blast
   522   qed 
   523   have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
   524             = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
   525     by (auto simp: sin_coeff_def elim!: oddE)
   526   show ?thesis
   527     apply (rule order_trans [OF _ *])
   528     apply (simp add: **)
   529     done
   530 qed
   531 
   532 lemma Taylor_cos: 
   533   "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k)) 
   534    \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
   535 proof -
   536   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   537       by arith
   538   have *: "cmod (cos z -
   539                  (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
   540            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
   541   proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
   542 simplified])
   543   show "convex (closed_segment 0 z)"
   544     by (rule convex_segment [of 0 z])
   545   next
   546     fix k x
   547     assume "x \<in> closed_segment 0 z" "k \<le> n"
   548     show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
   549             (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
   550              (at x within closed_segment 0 z)"
   551       apply (auto simp: power_Suc)
   552       apply (intro derivative_eq_intros | simp)+
   553       done
   554   next
   555     fix x
   556     assume "x \<in> closed_segment 0 z"
   557     then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
   558       by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
   559   next
   560     show "0 \<in> closed_segment 0 z"
   561       by (auto simp: closed_segment_def)
   562   next
   563     show "z \<in> closed_segment 0 z"
   564       apply (simp add: closed_segment_def scaleR_conv_of_real)
   565       using of_real_1 zero_le_one by blast
   566   qed 
   567   have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
   568             = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
   569     by (auto simp: cos_coeff_def elim!: evenE)
   570   show ?thesis
   571     apply (rule order_trans [OF _ *])
   572     apply (simp add: **)
   573     done
   574 qed
   575 
   576 end (* of context *)
   577 
   578 text{*32-bit Approximation to e*}
   579 lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
   580   using Taylor_exp [of 1 14] exp_le
   581   apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
   582   apply (simp only: pos_le_divide_eq [symmetric], linarith)
   583   done
   584 
   585 subsection{*The argument of a complex number*}
   586 
   587 definition Arg :: "complex \<Rightarrow> real" where
   588  "Arg z \<equiv> if z = 0 then 0
   589            else THE t. 0 \<le> t \<and> t < 2*pi \<and>
   590                     z = of_real(norm z) * exp(ii * of_real t)"
   591 
   592 lemma Arg_0 [simp]: "Arg(0) = 0"
   593   by (simp add: Arg_def)
   594 
   595 lemma Arg_unique_lemma:
   596   assumes z:  "z = of_real(norm z) * exp(ii * of_real t)"
   597       and z': "z = of_real(norm z) * exp(ii * of_real t')"
   598       and t:  "0 \<le> t"  "t < 2*pi"
   599       and t': "0 \<le> t'" "t' < 2*pi"
   600       and nz: "z \<noteq> 0"
   601   shows "t' = t"
   602 proof -
   603   have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
   604     by arith
   605   have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
   606     by (metis z z')
   607   then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
   608     by (metis nz mult_left_cancel mult_zero_left z)
   609   then have "sin t' = sin t \<and> cos t' = cos t"
   610     apply (simp add: exp_Euler sin_of_real cos_of_real)
   611     by (metis Complex_eq complex.sel)
   612   then obtain n::int where n: "t' = t + 2 * real n * pi"
   613     by (auto simp: sin_cos_eq_iff)
   614   then have "n=0"
   615     apply (rule_tac z=n in int_cases)
   616     using t t'
   617     apply (auto simp: mult_less_0_iff algebra_simps)
   618     done
   619   then show "t' = t"
   620       by (simp add: n)
   621 qed
   622 
   623 lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(ii * of_real(Arg z))"
   624 proof (cases "z=0")
   625   case True then show ?thesis
   626     by (simp add: Arg_def)
   627 next
   628   case False
   629   obtain t where t: "0 \<le> t" "t < 2*pi"
   630              and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
   631     using sincos_total_2pi [OF complex_unit_circle [OF False]]
   632     by blast
   633   have z: "z = of_real(norm z) * exp(ii * of_real t)"
   634     apply (rule complex_eqI)
   635     using t False ReIm
   636     apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
   637     done
   638   show ?thesis
   639     apply (simp add: Arg_def False)
   640     apply (rule theI [where a=t])
   641     using t z False
   642     apply (auto intro: Arg_unique_lemma)
   643     done
   644 qed
   645 
   646 
   647 corollary
   648   shows Arg_ge_0: "0 \<le> Arg z"
   649     and Arg_lt_2pi: "Arg z < 2*pi"
   650     and Arg_eq: "z = of_real(norm z) * exp(ii * of_real(Arg z))"
   651   using Arg by auto
   652 
   653 lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(ii * of_real t))"
   654   using Arg [of z] by auto
   655 
   656 lemma Arg_unique: "\<lbrakk>of_real r * exp(ii * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
   657   apply (rule Arg_unique_lemma [OF _ Arg_eq])
   658   using Arg [of z]
   659   apply (auto simp: norm_mult)
   660   done
   661 
   662 lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
   663   apply (rule Arg_unique [of "norm z"])
   664   apply (rule complex_eqI)
   665   using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] Arg_eq [of z]
   666   apply auto
   667   apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
   668   apply (metis Re_rcis Im_rcis rcis_def)+
   669   done
   670 
   671 lemma Arg_times_of_real [simp]: "0 < r \<Longrightarrow> Arg (of_real r * z) = Arg z"
   672   apply (cases "z=0", simp)
   673   apply (rule Arg_unique [of "r * norm z"])
   674   using Arg
   675   apply auto
   676   done
   677 
   678 lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
   679   by (metis Arg_times_of_real mult.commute)
   680 
   681 lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
   682   by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
   683 
   684 lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
   685 proof (cases "z=0")
   686   case True then show ?thesis
   687     by simp
   688 next
   689   case False
   690   have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   691     by (metis Arg_eq)
   692   also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
   693     using False
   694     by (simp add: zero_le_mult_iff)
   695   also have "... \<longleftrightarrow> Arg z \<le> pi"
   696     by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
   697   finally show ?thesis
   698     by blast
   699 qed
   700 
   701 lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
   702 proof (cases "z=0")
   703   case True then show ?thesis
   704     by simp
   705 next
   706   case False
   707   have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   708     by (metis Arg_eq)
   709   also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
   710     using False
   711     by (simp add: zero_less_mult_iff)
   712   also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
   713     using Arg_ge_0  Arg_lt_2pi sin_le_zero sin_gt_zero
   714     apply (auto simp: Im_exp)
   715     using le_less apply fastforce
   716     using not_le by blast
   717   finally show ?thesis
   718     by blast
   719 qed
   720 
   721 lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
   722 proof (cases "z=0")
   723   case True then show ?thesis
   724     by simp
   725 next
   726   case False
   727   have "z \<in> Reals \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   728     by (metis Arg_eq)
   729   also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
   730     using False
   731     by (simp add: zero_le_mult_iff)
   732   also have "... \<longleftrightarrow> Arg z = 0"
   733     apply (auto simp: Re_exp)
   734     apply (metis Arg_lt_pi Arg_ge_0 Arg_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
   735     using Arg_eq [of z]
   736     apply (auto simp: Reals_def)
   737     done
   738   finally show ?thesis
   739     by blast
   740 qed
   741 
   742 lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
   743   by (simp add: Arg_eq_0)
   744 
   745 lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
   746   apply  (cases "z=0", simp)
   747   using Arg_eq_0 [of "-z"]
   748   apply (auto simp: complex_is_Real_iff Arg_minus)
   749   apply (simp add: complex_Re_Im_cancel_iff)
   750   apply (metis Arg_minus pi_gt_zero add.left_neutral minus_minus minus_zero)
   751   done
   752 
   753 lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
   754   using Arg_eq_0 Arg_eq_pi not_le by auto
   755 
   756 lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   757   apply (cases "z=0", simp)
   758   apply (rule Arg_unique [of "inverse (norm z)"])
   759   using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] Exp_two_pi_i
   760   apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
   761   done
   762 
   763 lemma Arg_eq_iff:
   764   assumes "w \<noteq> 0" "z \<noteq> 0"
   765      shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
   766   using assms Arg_eq [of z] Arg_eq [of w]
   767   apply auto
   768   apply (rule_tac x="norm w / norm z" in exI)
   769   apply (simp add: divide_simps)
   770   by (metis mult.commute mult.left_commute)
   771 
   772 lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
   773   using complex_is_Real_iff
   774   apply (simp add: Arg_eq_0)
   775   apply (auto simp: divide_simps not_sum_power2_lt_zero)
   776   done
   777 
   778 lemma Arg_divide:
   779   assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
   780     shows "Arg(z / w) = Arg z - Arg w"
   781   apply (rule Arg_unique [of "norm(z / w)"])
   782   using assms Arg_eq [of z] Arg_eq [of w] Arg_ge_0 [of w] Arg_lt_2pi [of z]
   783   apply (auto simp: exp_diff norm_divide algebra_simps divide_simps)
   784   done
   785 
   786 lemma Arg_le_div_sum:
   787   assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
   788     shows "Arg z = Arg w + Arg(z / w)"
   789   by (simp add: Arg_divide assms)
   790 
   791 lemma Arg_le_div_sum_eq:
   792   assumes "w \<noteq> 0" "z \<noteq> 0"
   793     shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
   794   using assms
   795   by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
   796 
   797 lemma Arg_diff:
   798   assumes "w \<noteq> 0" "z \<noteq> 0"
   799     shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
   800   using assms
   801   apply (auto simp: Arg_ge_0 Arg_divide not_le)
   802   using Arg_divide [of w z] Arg_inverse [of "w/z"]
   803   apply auto
   804   by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
   805 
   806 lemma Arg_add:
   807   assumes "w \<noteq> 0" "z \<noteq> 0"
   808     shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
   809   using assms
   810   using Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
   811   apply (auto simp: Arg_ge_0 Arg_divide not_le)
   812   apply (metis Arg_lt_2pi add.commute)
   813   apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
   814   done
   815 
   816 lemma Arg_times:
   817   assumes "w \<noteq> 0" "z \<noteq> 0"
   818     shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
   819                             else (Arg w + Arg z) - 2*pi)"
   820   using Arg_add [OF assms]
   821   by auto
   822 
   823 lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   824   apply (cases "z=0", simp)
   825   apply (rule trans [of _ "Arg(inverse z)"])
   826   apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
   827   apply (metis norm_eq_zero of_real_power zero_less_power2)
   828   apply (auto simp: of_real_numeral Arg_inverse)
   829   done
   830 
   831 lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
   832   using Arg_eq_0 Arg_eq_0_pi
   833   by auto
   834 
   835 lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
   836   by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
   837 
   838 
   839 subsection{*Analytic properties of tangent function*}
   840 
   841 lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
   842   by (simp add: cnj_cos cnj_sin tan_def)
   843 
   844 lemma complex_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan complex_differentiable at z"
   845   unfolding complex_differentiable_def
   846   using DERIV_tan by blast
   847 
   848 lemma complex_differentiable_within_tan: "~(cos z = 0)
   849          \<Longrightarrow> tan complex_differentiable (at z within s)"
   850   using complex_differentiable_at_tan complex_differentiable_at_within by blast
   851 
   852 lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
   853   using continuous_at_imp_continuous_within isCont_tan by blast
   854 
   855 lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan"
   856   by (simp add: continuous_at_imp_continuous_on)
   857 
   858 lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
   859   by (simp add: complex_differentiable_within_tan holomorphic_on_def)
   860 
   861 
   862 subsection{*Complex logarithms (the conventional principal value)*}
   863 
   864 definition Ln where
   865    "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
   866 
   867 lemma
   868   assumes "z \<noteq> 0"
   869     shows exp_Ln [simp]: "exp(Ln z) = z"
   870       and mpi_less_Im_Ln: "-pi < Im(Ln z)"
   871       and Im_Ln_le_pi:    "Im(Ln z) \<le> pi"
   872 proof -
   873   obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
   874     using complex_unimodular_polar [of "z / (norm z)"] assms
   875     by (auto simp: norm_divide divide_simps)
   876   obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
   877     using sincos_principal_value [of "\<psi>"] assms
   878     by (auto simp: norm_divide divide_simps)
   879   have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def
   880     apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
   881     using z assms \<phi>
   882     apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
   883     done
   884   then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi"
   885     by auto
   886 qed
   887 
   888 lemma Ln_exp [simp]:
   889   assumes "-pi < Im(z)" "Im(z) \<le> pi"
   890     shows "Ln(exp z) = z"
   891   apply (rule exp_complex_eqI)
   892   using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
   893   apply auto
   894   done
   895 
   896 lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
   897   by (metis exp_Ln)
   898 
   899 lemma Ln_unique: "exp(z) = w \<Longrightarrow> -pi < Im(z) \<Longrightarrow> Im(z) \<le> pi \<Longrightarrow> Ln w = z"
   900   using Ln_exp by blast
   901 
   902 lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
   903 by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
   904 
   905 lemma exists_complex_root:
   906   fixes a :: complex
   907   shows "n \<noteq> 0 \<Longrightarrow> \<exists>z. z ^ n = a"
   908   apply (cases "a=0", simp)
   909   apply (rule_tac x= "exp(Ln(a) / n)" in exI)
   910   apply (auto simp: exp_of_nat_mult [symmetric])
   911   done
   912 
   913 subsection{*Derivative of Ln away from the branch cut*}
   914 
   915 lemma
   916   assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)"
   917     shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
   918       and Im_Ln_less_pi:           "Im (Ln z) < pi"
   919 proof -
   920   have znz: "z \<noteq> 0"
   921     using assms by auto
   922   then show *: "Im (Ln z) < pi" using assms
   923     by (metis exp_Ln Im_Ln_le_pi Im_exp Re_exp abs_of_nonneg cmod_eq_Re cos_pi mult.right_neutral mult_minus_right mult_zero_right neg_less_0_iff_less norm_exp_eq_Re not_less not_less_iff_gr_or_eq sin_pi)
   924   show "(Ln has_field_derivative inverse(z)) (at z)"
   925     apply (rule has_complex_derivative_inverse_strong_x
   926               [where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"])
   927     using znz *
   928     apply (auto simp: continuous_on_exp open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
   929     apply (metis DERIV_exp exp_Ln)
   930     apply (metis mpi_less_Im_Ln)
   931     done
   932 qed
   933 
   934 declare has_field_derivative_Ln [derivative_intros]
   935 declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
   936 
   937 lemma complex_differentiable_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln complex_differentiable at z"
   938   using complex_differentiable_def has_field_derivative_Ln by blast
   939 
   940 lemma complex_differentiable_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z))
   941          \<Longrightarrow> Ln complex_differentiable (at z within s)"
   942   using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
   943 
   944 lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
   945   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
   946 
   947 lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
   948   using continuous_at_Ln continuous_at_imp_continuous_within by blast
   949 
   950 lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s Ln"
   951   by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
   952 
   953 lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln holomorphic_on s"
   954   by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
   955 
   956 
   957 subsection{*Relation to Real Logarithm*}
   958 
   959 lemma ln_of_real:
   960   assumes "0 < z"
   961     shows "Ln(of_real z) = of_real(ln z)"
   962 proof -
   963   have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
   964     by (simp add: exp_of_real)
   965   also have "... = of_real(ln z)"
   966     using assms
   967     by (subst Ln_exp) auto
   968   finally show ?thesis
   969     using assms by simp
   970 qed
   971 
   972 
   973 subsection{*Quadrant-type results for Ln*}
   974 
   975 lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
   976   using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
   977   by simp
   978 
   979 lemma Re_Ln_pos_lt:
   980   assumes "z \<noteq> 0"
   981     shows "abs(Im(Ln z)) < pi/2 \<longleftrightarrow> 0 < Re(z)"
   982 proof -
   983   { fix w
   984     assume "w = Ln z"
   985     then have w: "Im w \<le> pi" "- pi < Im w"
   986       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
   987       by auto
   988     then have "abs(Im w) < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
   989       apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
   990       using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
   991       apply (simp add: abs_if split: split_if_asm)
   992       apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4)
   993                less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right
   994                mult_numeral_1_right)
   995       done
   996   }
   997   then show ?thesis using assms
   998     by auto
   999 qed
  1000 
  1001 lemma Re_Ln_pos_le:
  1002   assumes "z \<noteq> 0"
  1003     shows "abs(Im(Ln z)) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
  1004 proof -
  1005   { fix w
  1006     assume "w = Ln z"
  1007     then have w: "Im w \<le> pi" "- pi < Im w"
  1008       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1009       by auto
  1010     then have "abs(Im w) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
  1011       apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
  1012       using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
  1013       apply (auto simp: abs_if split: split_if_asm)
  1014       done
  1015   }
  1016   then show ?thesis using assms
  1017     by auto
  1018 qed
  1019 
  1020 lemma Im_Ln_pos_lt:
  1021   assumes "z \<noteq> 0"
  1022     shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
  1023 proof -
  1024   { fix w
  1025     assume "w = Ln z"
  1026     then have w: "Im w \<le> pi" "- pi < Im w"
  1027       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1028       by auto
  1029     then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)"
  1030       using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"]
  1031       apply (auto simp: Im_exp zero_less_mult_iff)
  1032       using less_linear apply fastforce
  1033       using less_linear apply fastforce
  1034       done
  1035   }
  1036   then show ?thesis using assms
  1037     by auto
  1038 qed
  1039 
  1040 lemma Im_Ln_pos_le:
  1041   assumes "z \<noteq> 0"
  1042     shows "0 \<le> Im(Ln z) \<and> Im(Ln z) \<le> pi \<longleftrightarrow> 0 \<le> Im(z)"
  1043 proof -
  1044   { fix w
  1045     assume "w = Ln z"
  1046     then have w: "Im w \<le> pi" "- pi < Im w"
  1047       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1048       by auto
  1049     then have "0 \<le> Im w \<and> Im w \<le> pi \<longleftrightarrow> 0 \<le> Im(exp w)"
  1050       using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"]
  1051       apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero)
  1052       apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi)
  1053       done }
  1054   then show ?thesis using assms
  1055     by auto
  1056 qed
  1057 
  1058 lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> abs(Im(Ln z)) < pi/2"
  1059   by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
  1060 
  1061 lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
  1062   by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))
  1063 
  1064 lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
  1065   by (metis exp_Ln Im_Ln_less_pi Im_Ln_pos_le Im_Ln_pos_lt Re_complex_of_real add.commute add.left_neutral
  1066        complex_eq exp_of_real le_less mult_zero_right norm_exp_eq_Re norm_le_zero_iff not_le of_real_0)
  1067 
  1068 lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
  1069   by (metis Im_Ln_eq_0 Im_Ln_less_pi Im_Ln_pos_le Im_Ln_pos_lt add.right_neutral complex_eq mult_zero_right not_less not_less_iff_gr_or_eq of_real_0)
  1070 
  1071 
  1072 subsection{*More Properties of Ln*}
  1073 
  1074 lemma cnj_Ln: "(Im z = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
  1075   apply (cases "z=0", auto)
  1076   apply (rule exp_complex_eqI)
  1077   apply (auto simp: abs_if split: split_if_asm)
  1078   apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps(1) cnj.simps(2) mult_2 neg_equal_0_iff_equal)
  1079   apply (metis add_mono_thms_linordered_field(5) complex_cnj_zero_iff diff_0_right diff_minus_eq_add minus_diff_eq mpi_less_Im_Ln mult.commute mult_2_right neg_less_iff_less)
  1080   by (metis exp_Ln exp_cnj)
  1081 
  1082 lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
  1083   apply (cases "z=0", auto)
  1084   apply (rule exp_complex_eqI)
  1085   using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
  1086   apply (auto simp: abs_if exp_minus split: split_if_asm)
  1087   apply (metis Im_Ln_less_pi Im_Ln_pos_le add_less_cancel_left add_strict_mono
  1088                inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
  1089   done
  1090 
  1091 lemma Ln_1 [simp]: "Ln(1) = 0"
  1092 proof -
  1093   have "Ln (exp 0) = 0"
  1094     by (metis exp_zero ln_exp ln_of_real of_real_0 of_real_1 zero_less_one)
  1095   then show ?thesis
  1096     by simp
  1097 qed
  1098 
  1099 lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
  1100   apply (rule exp_complex_eqI)
  1101   using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
  1102   apply (auto simp: abs_if)
  1103   done
  1104 
  1105 lemma Ln_ii [simp]: "Ln ii = ii * of_real pi/2"
  1106   using Ln_exp [of "ii * (of_real pi/2)"]
  1107   unfolding exp_Euler
  1108   by simp
  1109 
  1110 lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)"
  1111 proof -
  1112   have  "Ln(-ii) = Ln(1/ii)"
  1113     by simp
  1114   also have "... = - (Ln ii)"
  1115     by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one)
  1116   also have "... = - (ii * pi/2)"
  1117     by (simp add: Ln_ii)
  1118   finally show ?thesis .
  1119 qed
  1120 
  1121 lemma Ln_times:
  1122   assumes "w \<noteq> 0" "z \<noteq> 0"
  1123     shows "Ln(w * z) =
  1124                 (if Im(Ln w + Ln z) \<le> -pi then
  1125                   (Ln(w) + Ln(z)) + ii * of_real(2*pi)
  1126                 else if Im(Ln w + Ln z) > pi then
  1127                   (Ln(w) + Ln(z)) - ii * of_real(2*pi)
  1128                 else Ln(w) + Ln(z))"
  1129   using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
  1130   using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
  1131   by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
  1132 
  1133 lemma Ln_times_simple:
  1134     "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
  1135          \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
  1136   by (simp add: Ln_times)
  1137 
  1138 lemma Ln_minus:
  1139   assumes "z \<noteq> 0"
  1140     shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
  1141                      then Ln(z) + ii * pi
  1142                      else Ln(z) - ii * pi)" (is "_ = ?rhs")
  1143   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
  1144         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
  1145     by (auto simp: of_real_numeral exp_add exp_diff exp_Euler intro!: Ln_unique)
  1146 
  1147 lemma Ln_inverse_if:
  1148   assumes "z \<noteq> 0"
  1149     shows "Ln (inverse z) =
  1150             (if (Im(z) = 0 \<longrightarrow> 0 < Re z)
  1151              then -(Ln z)
  1152              else -(Ln z) + \<i> * 2 * complex_of_real pi)"
  1153 proof (cases "(Im(z) = 0 \<longrightarrow> 0 < Re z)")
  1154   case True then show ?thesis
  1155     by (simp add: Ln_inverse)
  1156 next
  1157   case False
  1158   then have z: "Im z = 0" "Re z < 0"
  1159     using assms
  1160     apply auto
  1161     by (metis cnj.code complex_cnj_cnj not_less_iff_gr_or_eq zero_complex.simps(1) zero_complex.simps(2))
  1162   have "Ln(inverse z) = Ln(- (inverse (-z)))"
  1163     by simp
  1164   also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
  1165     using assms z
  1166     apply (simp add: Ln_minus)
  1167     apply (simp add: field_simps)
  1168     done
  1169   also have "... = - Ln (- z) + \<i> * complex_of_real pi"
  1170     apply (subst Ln_inverse)
  1171     using z assms by auto
  1172   also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
  1173     apply (subst Ln_minus [OF assms])
  1174     using assms z
  1175     apply simp
  1176     done
  1177   finally show ?thesis
  1178     using assms z
  1179     by simp
  1180 qed
  1181 
  1182 lemma Ln_times_ii:
  1183   assumes "z \<noteq> 0"
  1184     shows  "Ln(ii * z) = (if 0 \<le> Re(z) | Im(z) < 0
  1185                           then Ln(z) + ii * of_real pi/2
  1186                           else Ln(z) - ii * of_real(3 * pi/2))"
  1187   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
  1188         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
  1189   by (auto simp: of_real_numeral Ln_times)
  1190 
  1191 
  1192 subsection{*Relation between Square Root and exp/ln, hence its derivative*}
  1193 
  1194 lemma csqrt_exp_Ln:
  1195   assumes "z \<noteq> 0"
  1196     shows "csqrt z = exp(Ln(z) / 2)"
  1197 proof -
  1198   have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
  1199     by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
  1200   also have "... = z"
  1201     using assms exp_Ln by blast
  1202   finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
  1203     by simp
  1204   also have "... = exp (Ln z / 2)"
  1205     apply (subst csqrt_square)
  1206     using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
  1207     apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+)
  1208     done
  1209   finally show ?thesis using assms csqrt_square
  1210     by simp
  1211 qed
  1212 
  1213 lemma csqrt_inverse:
  1214   assumes "Im(z) = 0 \<Longrightarrow> 0 < Re z"
  1215     shows "csqrt (inverse z) = inverse (csqrt z)"
  1216 proof (cases "z=0", simp)
  1217   assume "z \<noteq> 0 "
  1218   then show ?thesis
  1219     using assms
  1220     by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
  1221 qed
  1222 
  1223 lemma cnj_csqrt:
  1224   assumes "Im z = 0 \<Longrightarrow> 0 \<le> Re(z)"
  1225     shows "cnj(csqrt z) = csqrt(cnj z)"
  1226 proof (cases "z=0", simp)
  1227   assume z: "z \<noteq> 0"
  1228   then have "Im z = 0 \<Longrightarrow> 0 < Re(z)"
  1229     using assms cnj.code complex_cnj_zero_iff by fastforce
  1230   then show ?thesis
  1231    using z by (simp add: csqrt_exp_Ln cnj_Ln exp_cnj)
  1232 qed
  1233 
  1234 lemma has_field_derivative_csqrt:
  1235   assumes "Im z = 0 \<Longrightarrow> 0 < Re(z)"
  1236     shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)"
  1237 proof -
  1238   have z: "z \<noteq> 0"
  1239     using assms by auto
  1240   then have *: "inverse z = inverse (2*z) * 2"
  1241     by (simp add: divide_simps)
  1242   show ?thesis
  1243     apply (rule DERIV_transform_at [where f = "\<lambda>z. exp(Ln(z) / 2)" and d = "norm z"])
  1244     apply (intro derivative_eq_intros | simp add: assms)+
  1245     apply (rule *)
  1246     using z
  1247     apply (auto simp: field_simps csqrt_exp_Ln [symmetric])
  1248     apply (metis power2_csqrt power2_eq_square)
  1249     apply (metis csqrt_exp_Ln dist_0_norm less_irrefl)
  1250     done
  1251 qed
  1252 
  1253 lemma complex_differentiable_at_csqrt:
  1254     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable at z"
  1255   using complex_differentiable_def has_field_derivative_csqrt by blast
  1256 
  1257 lemma complex_differentiable_within_csqrt:
  1258     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable (at z within s)"
  1259   using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast
  1260 
  1261 lemma continuous_at_csqrt:
  1262     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
  1263   by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
  1264 
  1265 lemma continuous_within_csqrt:
  1266     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
  1267   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
  1268 
  1269 lemma continuous_on_csqrt [continuous_intros]:
  1270     "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s csqrt"
  1271   by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
  1272 
  1273 lemma holomorphic_on_csqrt:
  1274     "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt holomorphic_on s"
  1275   by (simp add: complex_differentiable_within_csqrt holomorphic_on_def)
  1276 
  1277 lemma continuous_within_closed_nontrivial:
  1278     "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
  1279   using open_Compl
  1280   by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
  1281 
  1282 lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
  1283   using closed_halfspace_Re_ge
  1284   by (simp add: closed_Int closed_complex_Reals)
  1285 
  1286 lemma continuous_within_csqrt_posreal:
  1287     "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
  1288 proof (cases "Im z = 0 --> 0 < Re(z)")
  1289   case True then show ?thesis
  1290     by (blast intro: continuous_within_csqrt)
  1291 next
  1292   case False
  1293   then have "Im z = 0" "Re z < 0 \<or> z = 0"
  1294     using False cnj.code complex_cnj_zero_iff by auto force
  1295   then show ?thesis
  1296     apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
  1297     apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
  1298     apply (rule_tac x="e^2" in exI)
  1299     apply (auto simp: Reals_def)
  1300 by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
  1301 qed
  1302 
  1303 
  1304 end