src/HOL/Multivariate_Analysis/Complex_Transcendental.thy

     by (simp add: scaleR_conv_of_real field_simps)
 qed
 
 theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)"
 proof -
-  have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) 
+  have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n)
         = (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))"
   proof
     fix n
     show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)"
       by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)

 lemma cos_exp_eq:  "cos z = (exp(ii * z) + exp(-(ii * z))) / 2"
   by (simp add: exp_Euler exp_minus_Euler)
 
 subsection{*Relationships between real and complex trig functions*}
 
-declare sin_of_real [simp] cos_of_real [simp]
-
 lemma real_sin_eq [simp]:
   fixes x::real
   shows "Re(sin(of_real x)) = sin x"
   by (simp add: sin_of_real)
-  
+
 lemma real_cos_eq [simp]:
   fixes x::real
   shows "Re(cos(of_real x)) = cos x"
   by (simp add: cos_of_real)
 

     by auto
   also have "... sums (exp (cnj z))"
     by (rule exp_converges)
   finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
   moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
-    by (metis exp_converges sums_cnj) 
+    by (metis exp_converges sums_cnj)
   ultimately show ?thesis
     using sums_unique2
-    by blast 
+    by blast
 qed
 
 lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
   by (simp add: sin_exp_eq exp_cnj field_simps)
 
 lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
   by (simp add: cos_exp_eq exp_cnj field_simps)
 
-lemma exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
-  by (metis Reals_cases Reals_of_real exp_of_real)
-
-lemma sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
-  by (metis Reals_cases Reals_of_real sin_of_real)
-
-lemma cos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> cos z \<in> \<real>"
-  by (metis Reals_cases Reals_of_real cos_of_real)
-
 lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
   using DERIV_sin complex_differentiable_def by blast
 
 lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)"
   by (simp add: complex_differentiable_at_sin complex_differentiable_at_within)

 lemma holomorphic_on_cos: "cos holomorphic_on s"
   by (simp add: complex_differentiable_within_cos holomorphic_on_def)
 
 subsection{* Get a nice real/imaginary separation in Euler's formula.*}
 
-lemma Euler: "exp(z) = of_real(exp(Re z)) * 
+lemma Euler: "exp(z) = of_real(exp(Re z)) *
               (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
 by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
 
 lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   by (simp add: sin_exp_eq field_simps Re_divide Im_exp)

 lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
 
 lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
   by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
-  
+
+lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
+  by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
+
+lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
+  by (simp add: Re_sin Im_sin algebra_simps)
+
+lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
+  by (simp add: Re_sin Im_sin algebra_simps)
+
 subsection{*More on the Polar Representation of Complex Numbers*}
 
 lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
-  by (simp add: exp_add exp_Euler exp_of_real)
+  by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
 
 lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
 apply auto
 apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
 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)

 qed
 
 lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
   by (auto simp: exp_eq abs_mult)
 
-lemma exp_integer_2pi: 
+lemma exp_integer_2pi:
   assumes "n \<in> Ints"
   shows "exp((2 * n * pi) * ii) = 1"
 proof -
   have "exp((2 * n * pi) * ii) = exp 0"
     using assms

   apply (auto simp: sin_add cos_add)
   apply (metis add.commute diff_add_cancel mult.commute)
   done
 qed
 
-lemma exp_i_ne_1: 
+lemma exp_i_ne_1:
   assumes "0 < x" "x < 2*pi"
   shows "exp(\<i> * of_real x) \<noteq> 1"
-proof 
+proof
   assume "exp (\<i> * of_real x) = 1"
   then have "exp (\<i> * of_real x) = exp 0"
     by simp
   then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
     by (simp only: Ints_def exp_eq) auto

     by simp
   then show False using assms
     by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
 qed
 
-lemma sin_eq_0: 
+lemma sin_eq_0:
   fixes z::complex
   shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
   by (simp add: sin_exp_eq exp_eq of_real_numeral)
 
-lemma cos_eq_0: 
+lemma cos_eq_0:
   fixes z::complex
   shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
   using sin_eq_0 [of "z - of_real pi/2"]
   by (simp add: sin_diff algebra_simps)
 
-lemma cos_eq_1: 
+lemma cos_eq_1:
   fixes z::complex
   shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
 proof -
   have "cos z = cos (2*(z/2))"
     by simp

     by (simp only: cos_double_sin)
   finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
     by simp
   show ?thesis
     by (auto simp: sin_eq_0 of_real_numeral)
-qed  
+qed
 
 lemma csin_eq_1:
   fixes z::complex
   shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)"
   using cos_eq_1 [of "z - of_real pi/2"]

     apply (rule_tac [2] x="-(x+1)" in exI)
     apply (rule_tac x="-(x+1)" in exI)
     apply (simp_all add: algebra_simps)
     done
   finally show ?thesis .
-qed  
-
-lemma ccos_eq_minus1: 
+qed
+
+lemma ccos_eq_minus1:
   fixes z::complex
   shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
   using csin_eq_1 [of "z - of_real pi/2"]
   apply (simp add: sin_diff)
   apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
-  done       
+  done
 
 lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
                 (is "_ = ?rhs")
 proof -
   have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"

     apply (auto simp: of_real_numeral)
     done
   also have "... = ?rhs"
     by (auto simp: algebra_simps)
   finally show ?thesis .
-qed  
+qed
 
 lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
 proof -
   have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
     by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)

     apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
     done
   also have "... = ?rhs"
     by (auto simp: algebra_simps)
   finally show ?thesis .
-qed  
+qed
 
 lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
                       (is "_ = ?rhs")
 proof -
   have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"

     apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
     done
   also have "... = ?rhs"
     by (auto simp: algebra_simps)
   finally show ?thesis .
-qed  
+qed
 
 lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
-  apply (simp add: exp_Euler cmod_def power2_diff algebra_simps)
+  apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
   using cos_double_sin [of "t/2"]
   apply (simp add: real_sqrt_mult)
   done
 
 lemma sinh_complex:

   shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)"
   by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
 
 lemmas cos_ii_times = cosh_complex [symmetric]
 
-lemma norm_cos_squared: 
+lemma norm_cos_squared:
     "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
   apply (cases z)
   apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)

   apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   apply (simp add: cos_squared_eq)
   apply (simp add: power2_eq_square algebra_simps divide_simps)
-  done 
+  done
 
 lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
   using abs_Im_le_cmod linear order_trans by fastforce
 
-lemma norm_cos_le: 
+lemma norm_cos_le:
   fixes z::complex
   shows "norm(cos z) \<le> exp(norm z)"
 proof -
   have "Im z \<le> cmod z"
     using abs_Im_le_cmod abs_le_D1 by auto

     apply (rule order_trans [OF norm_triangle_ineq], simp)
     apply (metis add_mono exp_le_cancel_iff mult_2_right)
     done
 qed
 
-lemma norm_cos_plus1_le: 
+lemma norm_cos_plus1_le:
   fixes z::complex
   shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
 proof -
   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"
       by arith

     done
 qed
 
 subsection{* Taylor series for complex exponential, sine and cosine.*}
 
-context 
+context
 begin
 
 declare power_Suc [simp del]
 
-lemma Taylor_exp: 
+lemma Taylor_exp:
   "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
 proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
   show "convex (closed_segment 0 z)"
     by (rule convex_segment [of 0 z])
 next

     by (auto simp: closed_segment_def)
 next
   show "z \<in> closed_segment 0 z"
     apply (simp add: closed_segment_def scaleR_conv_of_real)
     using of_real_1 zero_le_one by blast
-qed 
-
-lemma 
+qed
+
+lemma
   assumes "0 \<le> u" "u \<le> 1"
-  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" 
+  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
     and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
 proof -
   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
     by arith
   show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms

     apply (auto simp: abs_if mult_left_le_one_le)
     apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
     apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
     done
 qed
-    
-lemma Taylor_sin: 
-  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) 
+
+lemma Taylor_sin:
+  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
    \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
 proof -
   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
       by arith
   have *: "cmod (sin z -
                  (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
-           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
+           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   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,
 simplified])
   show "convex (closed_segment 0 z)"
     by (rule convex_segment [of 0 z])
   next

       by (auto simp: closed_segment_def)
   next
     show "z \<in> closed_segment 0 z"
       apply (simp add: closed_segment_def scaleR_conv_of_real)
       using of_real_1 zero_le_one by blast
-  qed 
+  qed
   have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
             = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
     by (auto simp: sin_coeff_def elim!: oddE)
   show ?thesis
     apply (rule order_trans [OF _ *])
     apply (simp add: **)
     done
 qed
 
-lemma Taylor_cos: 
-  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k)) 
+lemma Taylor_cos:
+  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k))
    \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
 proof -
   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
       by arith
   have *: "cmod (cos z -
                  (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
-           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
+           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   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,
 simplified])
   show "convex (closed_segment 0 z)"
     by (rule convex_segment [of 0 z])
   next

       by (auto simp: closed_segment_def)
   next
     show "z \<in> closed_segment 0 z"
       apply (simp add: closed_segment_def scaleR_conv_of_real)
       using of_real_1 zero_le_one by blast
-  qed 
+  qed
   have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
             = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
     by (auto simp: cos_coeff_def elim!: evenE)
   show ?thesis
     apply (rule order_trans [OF _ *])

   apply (cases "a=0", simp)
   apply (rule_tac x= "exp(Ln(a) / n)" in exI)
   apply (auto simp: exp_of_nat_mult [symmetric])
   done
 
+subsection{*The Unwinding Number and the Ln-product Formula*}
+
+text{*Note that in this special case the unwinding number is -1, 0 or 1.*}
+
+definition unwinding :: "complex \<Rightarrow> complex" where
+   "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * ii)"
+
+lemma unwinding_2pi: "(2*pi) * ii * unwinding(z) = z - Ln(exp z)"
+  by (simp add: unwinding_def)
+
+lemma Ln_times_unwinding:
+    "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * ii * unwinding(Ln w + Ln z)"
+  using unwinding_2pi by (simp add: exp_add)
+
+
 subsection{*Derivative of Ln away from the branch cut*}
 
 lemma
   assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)"
     shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"

   using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
 
 lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
 
+lemma isCont_Ln' [simp]:
+   "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
+  by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
+
 lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
   using continuous_at_Ln continuous_at_imp_continuous_within by blast
 
 lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s Ln"
   by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)

   by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
 
 
 subsection{*Relation to Real Logarithm*}
 
-lemma ln_of_real:
+lemma Ln_of_real:
   assumes "0 < z"
     shows "Ln(of_real z) = of_real(ln z)"
 proof -
   have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
     by (simp add: exp_of_real)

     using assms
     by (subst Ln_exp) auto
   finally show ?thesis
     using assms by simp
 qed
+
+corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> Ln z \<in> \<real>"
+  by (auto simp: Ln_of_real elim: Reals_cases)
 
 
 subsection{*Quadrant-type results for Ln*}
 
 lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"

   done
 
 lemma Ln_1 [simp]: "Ln(1) = 0"
 proof -
   have "Ln (exp 0) = 0"
-    by (metis exp_zero ln_exp ln_of_real of_real_0 of_real_1 zero_less_one)
+    by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
   then show ?thesis
     by simp
 qed
 
 lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"

 
 lemma continuous_at_csqrt:
     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
   by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
 
+corollary isCont_csqrt' [simp]:
+   "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
+  by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
+
 lemma continuous_within_csqrt:
     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
 
 lemma continuous_on_csqrt [continuous_intros]: