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