src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
author paulson
Mon Oct 26 23:41:27 2015 +0000 (2015-10-26)
changeset 61518 ff12606337e9
parent 61426 d53db136e8fd
child 61524 f2e51e704a96
permissions -rw-r--r--
new lemmas about topology, etc., for Cauchy integral formula
     1 (*  Author: John Harrison
     2     Ported from "hol_light/Multivariate/transcendentals.ml" by L C Paulson (2015)
     3 *)
     4 
     5 section \<open>Complex Transcendental Functions\<close>
     6 
     7 theory Complex_Transcendental
     8 imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
     9 begin
    10 
    11 lemma cmod_add_real_less:
    12   assumes "Im z \<noteq> 0" "r\<noteq>0"
    13     shows "cmod (z + r) < cmod z + abs r"
    14 proof (cases z)
    15   case (Complex x y)
    16   have "r * x / \<bar>r\<bar> < sqrt (x*x + y*y)"
    17     apply (rule real_less_rsqrt)
    18     using assms
    19     apply (simp add: Complex power2_eq_square)
    20     using not_real_square_gt_zero by blast
    21   then show ?thesis using assms Complex
    22     apply (auto simp: cmod_def)
    23     apply (rule power2_less_imp_less, auto)
    24     apply (simp add: power2_eq_square field_simps)
    25     done
    26 qed
    27 
    28 lemma cmod_diff_real_less: "Im z \<noteq> 0 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> cmod (z - x) < cmod z + abs x"
    29   using cmod_add_real_less [of z "-x"]
    30   by simp
    31 
    32 lemma cmod_square_less_1_plus:
    33   assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
    34     shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
    35   using assms
    36   apply (cases "Im z = 0 \<or> Re z = 0")
    37   using abs_square_less_1
    38     apply (force simp add: Re_power2 Im_power2 cmod_def)
    39   using cmod_diff_real_less [of "1 - z\<^sup>2" "1"]
    40   apply (simp add: norm_power Im_power2)
    41   done
    42 
    43 subsection\<open>The Exponential Function is Differentiable and Continuous\<close>
    44 
    45 lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
    46   using DERIV_exp complex_differentiable_at_within complex_differentiable_def by blast
    47 
    48 lemma continuous_within_exp:
    49   fixes z::"'a::{real_normed_field,banach}"
    50   shows "continuous (at z within s) exp"
    51 by (simp add: continuous_at_imp_continuous_within)
    52 
    53 lemma continuous_on_exp:
    54   fixes s::"'a::{real_normed_field,banach} set"
    55   shows "continuous_on s exp"
    56 by (simp add: continuous_on_exp continuous_on_id)
    57 
    58 lemma holomorphic_on_exp: "exp holomorphic_on s"
    59   by (simp add: complex_differentiable_within_exp holomorphic_on_def)
    60 
    61 subsection\<open>Euler and de Moivre formulas.\<close>
    62 
    63 text\<open>The sine series times @{term i}\<close>
    64 lemma sin_ii_eq: "(\<lambda>n. (ii * sin_coeff n) * z^n) sums (ii * sin z)"
    65 proof -
    66   have "(\<lambda>n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)"
    67     using sin_converges sums_mult by blast
    68   then show ?thesis
    69     by (simp add: scaleR_conv_of_real field_simps)
    70 qed
    71 
    72 theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)"
    73 proof -
    74   have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n)
    75         = (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))"
    76   proof
    77     fix n
    78     show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)"
    79       by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
    80   qed
    81   also have "... sums (exp (ii * z))"
    82     by (rule exp_converges)
    83   finally have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (exp (ii * z))" .
    84   moreover have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (cos z + ii * sin z)"
    85     using sums_add [OF cos_converges [of z] sin_ii_eq [of z]]
    86     by (simp add: field_simps scaleR_conv_of_real)
    87   ultimately show ?thesis
    88     using sums_unique2 by blast
    89 qed
    90 
    91 corollary exp_minus_Euler: "exp(-(ii * z)) = cos(z) - ii * sin(z)"
    92   using exp_Euler [of "-z"]
    93   by simp
    94 
    95 lemma sin_exp_eq: "sin z = (exp(ii * z) - exp(-(ii * z))) / (2*ii)"
    96   by (simp add: exp_Euler exp_minus_Euler)
    97 
    98 lemma sin_exp_eq': "sin z = ii * (exp(-(ii * z)) - exp(ii * z)) / 2"
    99   by (simp add: exp_Euler exp_minus_Euler)
   100 
   101 lemma cos_exp_eq:  "cos z = (exp(ii * z) + exp(-(ii * z))) / 2"
   102   by (simp add: exp_Euler exp_minus_Euler)
   103 
   104 subsection\<open>Relationships between real and complex trig functions\<close>
   105 
   106 lemma real_sin_eq [simp]:
   107   fixes x::real
   108   shows "Re(sin(of_real x)) = sin x"
   109   by (simp add: sin_of_real)
   110 
   111 lemma real_cos_eq [simp]:
   112   fixes x::real
   113   shows "Re(cos(of_real x)) = cos x"
   114   by (simp add: cos_of_real)
   115 
   116 lemma DeMoivre: "(cos z + ii * sin z) ^ n = cos(n * z) + ii * sin(n * z)"
   117   apply (simp add: exp_Euler [symmetric])
   118   by (metis exp_of_nat_mult mult.left_commute)
   119 
   120 lemma exp_cnj:
   121   fixes z::complex
   122   shows "cnj (exp z) = exp (cnj z)"
   123 proof -
   124   have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))"
   125     by auto
   126   also have "... sums (exp (cnj z))"
   127     by (rule exp_converges)
   128   finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
   129   moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
   130     by (metis exp_converges sums_cnj)
   131   ultimately show ?thesis
   132     using sums_unique2
   133     by blast
   134 qed
   135 
   136 lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
   137   by (simp add: sin_exp_eq exp_cnj field_simps)
   138 
   139 lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
   140   by (simp add: cos_exp_eq exp_cnj field_simps)
   141 
   142 lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
   143   using DERIV_sin complex_differentiable_def by blast
   144 
   145 lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)"
   146   by (simp add: complex_differentiable_at_sin complex_differentiable_at_within)
   147 
   148 lemma complex_differentiable_at_cos: "cos complex_differentiable at z"
   149   using DERIV_cos complex_differentiable_def by blast
   150 
   151 lemma complex_differentiable_within_cos: "cos complex_differentiable (at z within s)"
   152   by (simp add: complex_differentiable_at_cos complex_differentiable_at_within)
   153 
   154 lemma holomorphic_on_sin: "sin holomorphic_on s"
   155   by (simp add: complex_differentiable_within_sin holomorphic_on_def)
   156 
   157 lemma holomorphic_on_cos: "cos holomorphic_on s"
   158   by (simp add: complex_differentiable_within_cos holomorphic_on_def)
   159 
   160 subsection\<open>Get a nice real/imaginary separation in Euler's formula.\<close>
   161 
   162 lemma Euler: "exp(z) = of_real(exp(Re z)) *
   163               (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
   164 by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
   165 
   166 lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   167   by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
   168 
   169 lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
   170   by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
   171 
   172 lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   173   by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
   174 
   175 lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
   176   by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
   177 
   178 lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
   179   by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
   180 
   181 lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
   182   by (simp add: Re_sin Im_sin algebra_simps)
   183 
   184 lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
   185   by (simp add: Re_sin Im_sin algebra_simps)
   186 
   187 subsection\<open>More on the Polar Representation of Complex Numbers\<close>
   188 
   189 lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
   190   by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
   191 
   192 lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
   193 apply auto
   194 apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
   195 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)
   196 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)
   197 
   198 lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * ii)"
   199                 (is "?lhs = ?rhs")
   200 proof -
   201   have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
   202     by (simp add: exp_diff)
   203   also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
   204     by (simp add: exp_eq_1)
   205   also have "... \<longleftrightarrow> ?rhs"
   206     by (auto simp: algebra_simps intro!: complex_eqI)
   207   finally show ?thesis .
   208 qed
   209 
   210 lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
   211   by (auto simp: exp_eq abs_mult)
   212 
   213 lemma exp_integer_2pi:
   214   assumes "n \<in> \<int>"
   215   shows "exp((2 * n * pi) * ii) = 1"
   216 proof -
   217   have "exp((2 * n * pi) * ii) = exp 0"
   218     using assms
   219     by (simp only: Ints_def exp_eq) auto
   220   also have "... = 1"
   221     by simp
   222   finally show ?thesis .
   223 qed
   224 
   225 lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
   226 proof -
   227   { assume "sin y = sin x" "cos y = cos x"
   228     then have "cos (y-x) = 1"
   229       using cos_add [of y "-x"] by simp
   230     then have "\<exists>n::int. y-x = real n * 2 * pi"
   231       using cos_one_2pi_int by blast }
   232   then show ?thesis
   233   apply (auto simp: sin_add cos_add)
   234   apply (metis add.commute diff_add_cancel mult.commute)
   235   done
   236 qed
   237 
   238 lemma exp_i_ne_1:
   239   assumes "0 < x" "x < 2*pi"
   240   shows "exp(\<i> * of_real x) \<noteq> 1"
   241 proof
   242   assume "exp (\<i> * of_real x) = 1"
   243   then have "exp (\<i> * of_real x) = exp 0"
   244     by simp
   245   then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
   246     by (simp only: Ints_def exp_eq) auto
   247   then have  "of_real x = (of_int (2 * n) * pi)"
   248     by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
   249   then have  "x = (of_int (2 * n) * pi)"
   250     by simp
   251   then show False using assms
   252     by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
   253 qed
   254 
   255 lemma sin_eq_0:
   256   fixes z::complex
   257   shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
   258   by (simp add: sin_exp_eq exp_eq of_real_numeral)
   259 
   260 lemma cos_eq_0:
   261   fixes z::complex
   262   shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
   263   using sin_eq_0 [of "z - of_real pi/2"]
   264   by (simp add: sin_diff algebra_simps)
   265 
   266 lemma cos_eq_1:
   267   fixes z::complex
   268   shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
   269 proof -
   270   have "cos z = cos (2*(z/2))"
   271     by simp
   272   also have "... = 1 - 2 * sin (z/2) ^ 2"
   273     by (simp only: cos_double_sin)
   274   finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
   275     by simp
   276   show ?thesis
   277     by (auto simp: sin_eq_0 of_real_numeral)
   278 qed
   279 
   280 lemma csin_eq_1:
   281   fixes z::complex
   282   shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)"
   283   using cos_eq_1 [of "z - of_real pi/2"]
   284   by (simp add: cos_diff algebra_simps)
   285 
   286 lemma csin_eq_minus1:
   287   fixes z::complex
   288   shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)"
   289         (is "_ = ?rhs")
   290 proof -
   291   have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
   292     by (simp add: equation_minus_iff)
   293   also have "...  \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
   294     by (simp only: csin_eq_1)
   295   also have "...  \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
   296     apply (rule iff_exI)
   297     by (metis (no_types)  is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff)
   298   also have "... = ?rhs"
   299     apply (auto simp: of_real_numeral)
   300     apply (rule_tac [2] x="-(x+1)" in exI)
   301     apply (rule_tac x="-(x+1)" in exI)
   302     apply (simp_all add: algebra_simps)
   303     done
   304   finally show ?thesis .
   305 qed
   306 
   307 lemma ccos_eq_minus1:
   308   fixes z::complex
   309   shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
   310   using csin_eq_1 [of "z - of_real pi/2"]
   311   apply (simp add: sin_diff)
   312   apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
   313   done
   314 
   315 lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
   316                 (is "_ = ?rhs")
   317 proof -
   318   have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
   319     by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
   320   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
   321     by (simp only: csin_eq_1)
   322   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
   323     apply (rule iff_exI)
   324     apply (auto simp: algebra_simps of_real_numeral)
   325     apply (rule injD [OF inj_of_real [where 'a = complex]])
   326     apply (auto simp: of_real_numeral)
   327     done
   328   also have "... = ?rhs"
   329     by (auto simp: algebra_simps)
   330   finally show ?thesis .
   331 qed
   332 
   333 lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
   334 proof -
   335   have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
   336     by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
   337   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
   338     by (simp only: csin_eq_minus1)
   339   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
   340     apply (rule iff_exI)
   341     apply (auto simp: algebra_simps)
   342     apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
   343     done
   344   also have "... = ?rhs"
   345     by (auto simp: algebra_simps)
   346   finally show ?thesis .
   347 qed
   348 
   349 lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
   350                       (is "_ = ?rhs")
   351 proof -
   352   have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
   353     by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
   354   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
   355     by (simp only: ccos_eq_minus1)
   356   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
   357     apply (rule iff_exI)
   358     apply (auto simp: algebra_simps)
   359     apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
   360     done
   361   also have "... = ?rhs"
   362     by (auto simp: algebra_simps)
   363   finally show ?thesis .
   364 qed
   365 
   366 lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
   367   apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
   368   using cos_double_sin [of "t/2"]
   369   apply (simp add: real_sqrt_mult)
   370   done
   371 
   372 lemma sinh_complex:
   373   fixes z :: complex
   374   shows "(exp z - inverse (exp z)) / 2 = -ii * sin(ii * z)"
   375   by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
   376 
   377 lemma sin_ii_times:
   378   fixes z :: complex
   379   shows "sin(ii * z) = ii * ((exp z - inverse (exp z)) / 2)"
   380   using sinh_complex by auto
   381 
   382 lemma sinh_real:
   383   fixes x :: real
   384   shows "of_real((exp x - inverse (exp x)) / 2) = -ii * sin(ii * of_real x)"
   385   by (simp add: exp_of_real sin_ii_times of_real_numeral)
   386 
   387 lemma cosh_complex:
   388   fixes z :: complex
   389   shows "(exp z + inverse (exp z)) / 2 = cos(ii * z)"
   390   by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
   391 
   392 lemma cosh_real:
   393   fixes x :: real
   394   shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)"
   395   by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
   396 
   397 lemmas cos_ii_times = cosh_complex [symmetric]
   398 
   399 lemma norm_cos_squared:
   400     "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
   401   apply (cases z)
   402   apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
   403   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
   404   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   405   apply (simp add: sin_squared_eq)
   406   apply (simp add: power2_eq_square algebra_simps divide_simps)
   407   done
   408 
   409 lemma norm_sin_squared:
   410     "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
   411   apply (cases z)
   412   apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
   413   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
   414   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   415   apply (simp add: cos_squared_eq)
   416   apply (simp add: power2_eq_square algebra_simps divide_simps)
   417   done
   418 
   419 lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
   420   using abs_Im_le_cmod linear order_trans by fastforce
   421 
   422 lemma norm_cos_le:
   423   fixes z::complex
   424   shows "norm(cos z) \<le> exp(norm z)"
   425 proof -
   426   have "Im z \<le> cmod z"
   427     using abs_Im_le_cmod abs_le_D1 by auto
   428   with exp_uminus_Im show ?thesis
   429     apply (simp add: cos_exp_eq norm_divide)
   430     apply (rule order_trans [OF norm_triangle_ineq], simp)
   431     apply (metis add_mono exp_le_cancel_iff mult_2_right)
   432     done
   433 qed
   434 
   435 lemma norm_cos_plus1_le:
   436   fixes z::complex
   437   shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
   438 proof -
   439   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"
   440       by arith
   441   have *: "Im z \<le> cmod z"
   442     using abs_Im_le_cmod abs_le_D1 by auto
   443   have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)"
   444     by (simp add: norm_add_rule_thm)
   445   have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
   446     by (simp add: cos_exp_eq)
   447   also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
   448     by (simp add: field_simps)
   449   also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
   450     by (simp add: norm_divide)
   451   finally show ?thesis
   452     apply (rule ssubst, simp)
   453     apply (rule order_trans [OF triangle3], simp)
   454     using exp_uminus_Im *
   455     apply (auto intro: mono)
   456     done
   457 qed
   458 
   459 subsection\<open>Taylor series for complex exponential, sine and cosine.\<close>
   460 
   461 declare power_Suc [simp del]
   462 
   463 lemma Taylor_exp:
   464   "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   465 proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
   466   show "convex (closed_segment 0 z)"
   467     by (rule convex_closed_segment [of 0 z])
   468 next
   469   fix k x
   470   assume "x \<in> closed_segment 0 z" "k \<le> n"
   471   show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
   472     using DERIV_exp DERIV_subset by blast
   473 next
   474   fix x
   475   assume "x \<in> closed_segment 0 z"
   476   then show "Re x \<le> \<bar>Re z\<bar>"
   477     apply (auto simp: closed_segment_def scaleR_conv_of_real)
   478     by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans)
   479 next
   480   show "0 \<in> closed_segment 0 z"
   481     by (auto simp: closed_segment_def)
   482 next
   483   show "z \<in> closed_segment 0 z"
   484     apply (simp add: closed_segment_def scaleR_conv_of_real)
   485     using of_real_1 zero_le_one by blast
   486 qed
   487 
   488 lemma
   489   assumes "0 \<le> u" "u \<le> 1"
   490   shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   491     and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   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   show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
   496     apply (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
   497     apply (rule order_trans [OF norm_triangle_ineq4])
   498     apply (rule mono)
   499     apply (auto simp: abs_if mult_left_le_one_le)
   500     apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
   501     apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   502     done
   503   show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
   504     apply (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
   505     apply (rule order_trans [OF norm_triangle_ineq])
   506     apply (rule mono)
   507     apply (auto simp: abs_if mult_left_le_one_le)
   508     apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
   509     apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   510     done
   511 qed
   512 
   513 lemma Taylor_sin:
   514   "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
   515    \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   516 proof -
   517   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   518       by arith
   519   have *: "cmod (sin z -
   520                  (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
   521            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   522   proof (rule complex_taylor [of "closed_segment 0 z" n 
   523                                  "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" 
   524                                  "exp\<bar>Im z\<bar>" 0 z,  simplified])
   525     fix k x
   526     show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
   527             (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
   528             (at x within closed_segment 0 z)"
   529       apply (auto simp: power_Suc)
   530       apply (intro derivative_eq_intros | simp)+
   531       done
   532   next
   533     fix x
   534     assume "x \<in> closed_segment 0 z"
   535     then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
   536       by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
   537   qed
   538   have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
   539             = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
   540     by (auto simp: sin_coeff_def elim!: oddE)
   541   show ?thesis
   542     apply (rule order_trans [OF _ *])
   543     apply (simp add: **)
   544     done
   545 qed
   546 
   547 lemma Taylor_cos:
   548   "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k))
   549    \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
   550 proof -
   551   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   552       by arith
   553   have *: "cmod (cos z -
   554                  (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
   555            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   556   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,
   557 simplified])
   558     fix k x
   559     assume "x \<in> closed_segment 0 z" "k \<le> n"
   560     show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
   561             (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
   562              (at x within closed_segment 0 z)"
   563       apply (auto simp: power_Suc)
   564       apply (intro derivative_eq_intros | simp)+
   565       done
   566   next
   567     fix x
   568     assume "x \<in> closed_segment 0 z"
   569     then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
   570       by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
   571   qed
   572   have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
   573             = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
   574     by (auto simp: cos_coeff_def elim!: evenE)
   575   show ?thesis
   576     apply (rule order_trans [OF _ *])
   577     apply (simp add: **)
   578     done
   579 qed
   580 
   581 declare power_Suc [simp]
   582 
   583 text\<open>32-bit Approximation to e\<close>
   584 lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
   585   using Taylor_exp [of 1 14] exp_le
   586   apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
   587   apply (simp only: pos_le_divide_eq [symmetric], linarith)
   588   done
   589 
   590 lemma e_less_3: "exp 1 < (3::real)"
   591   using e_approx_32
   592   by (simp add: abs_if split: split_if_asm)
   593 
   594 lemma ln3_gt_1: "ln 3 > (1::real)"
   595   by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
   596 
   597 
   598 subsection\<open>The argument of a complex number\<close>
   599 
   600 definition Arg :: "complex \<Rightarrow> real" where
   601  "Arg z \<equiv> if z = 0 then 0
   602            else THE t. 0 \<le> t \<and> t < 2*pi \<and>
   603                     z = of_real(norm z) * exp(ii * of_real t)"
   604 
   605 lemma Arg_0 [simp]: "Arg(0) = 0"
   606   by (simp add: Arg_def)
   607 
   608 lemma Arg_unique_lemma:
   609   assumes z:  "z = of_real(norm z) * exp(ii * of_real t)"
   610       and z': "z = of_real(norm z) * exp(ii * of_real t')"
   611       and t:  "0 \<le> t"  "t < 2*pi"
   612       and t': "0 \<le> t'" "t' < 2*pi"
   613       and nz: "z \<noteq> 0"
   614   shows "t' = t"
   615 proof -
   616   have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
   617     by arith
   618   have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
   619     by (metis z z')
   620   then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
   621     by (metis nz mult_left_cancel mult_zero_left z)
   622   then have "sin t' = sin t \<and> cos t' = cos t"
   623     apply (simp add: exp_Euler sin_of_real cos_of_real)
   624     by (metis Complex_eq complex.sel)
   625   then obtain n::int where n: "t' = t + 2 * real n * pi"
   626     by (auto simp: sin_cos_eq_iff)
   627   then have "n=0"
   628     apply (rule_tac z=n in int_cases)
   629     using t t'
   630     apply (auto simp: mult_less_0_iff algebra_simps)
   631     done
   632   then show "t' = t"
   633       by (simp add: n)
   634 qed
   635 
   636 lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(ii * of_real(Arg z))"
   637 proof (cases "z=0")
   638   case True then show ?thesis
   639     by (simp add: Arg_def)
   640 next
   641   case False
   642   obtain t where t: "0 \<le> t" "t < 2*pi"
   643              and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
   644     using sincos_total_2pi [OF complex_unit_circle [OF False]]
   645     by blast
   646   have z: "z = of_real(norm z) * exp(ii * of_real t)"
   647     apply (rule complex_eqI)
   648     using t False ReIm
   649     apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
   650     done
   651   show ?thesis
   652     apply (simp add: Arg_def False)
   653     apply (rule theI [where a=t])
   654     using t z False
   655     apply (auto intro: Arg_unique_lemma)
   656     done
   657 qed
   658 
   659 
   660 corollary
   661   shows Arg_ge_0: "0 \<le> Arg z"
   662     and Arg_lt_2pi: "Arg z < 2*pi"
   663     and Arg_eq: "z = of_real(norm z) * exp(ii * of_real(Arg z))"
   664   using Arg by auto
   665 
   666 lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(ii * of_real t))"
   667   using Arg [of z] by auto
   668 
   669 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"
   670   apply (rule Arg_unique_lemma [OF _ Arg_eq])
   671   using Arg [of z]
   672   apply (auto simp: norm_mult)
   673   done
   674 
   675 lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
   676   apply (rule Arg_unique [of "norm z"])
   677   apply (rule complex_eqI)
   678   using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] Arg_eq [of z]
   679   apply auto
   680   apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
   681   apply (metis Re_rcis Im_rcis rcis_def)+
   682   done
   683 
   684 lemma Arg_times_of_real [simp]: "0 < r \<Longrightarrow> Arg (of_real r * z) = Arg z"
   685   apply (cases "z=0", simp)
   686   apply (rule Arg_unique [of "r * norm z"])
   687   using Arg
   688   apply auto
   689   done
   690 
   691 lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
   692   by (metis Arg_times_of_real mult.commute)
   693 
   694 lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
   695   by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
   696 
   697 lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
   698 proof (cases "z=0")
   699   case True then show ?thesis
   700     by simp
   701 next
   702   case False
   703   have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   704     by (metis Arg_eq)
   705   also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
   706     using False
   707     by (simp add: zero_le_mult_iff)
   708   also have "... \<longleftrightarrow> Arg z \<le> pi"
   709     by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
   710   finally show ?thesis
   711     by blast
   712 qed
   713 
   714 lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
   715 proof (cases "z=0")
   716   case True then show ?thesis
   717     by simp
   718 next
   719   case False
   720   have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   721     by (metis Arg_eq)
   722   also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
   723     using False
   724     by (simp add: zero_less_mult_iff)
   725   also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
   726     using Arg_ge_0  Arg_lt_2pi sin_le_zero sin_gt_zero
   727     apply (auto simp: Im_exp)
   728     using le_less apply fastforce
   729     using not_le by blast
   730   finally show ?thesis
   731     by blast
   732 qed
   733 
   734 lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
   735 proof (cases "z=0")
   736   case True then show ?thesis
   737     by simp
   738 next
   739   case False
   740   have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   741     by (metis Arg_eq)
   742   also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
   743     using False
   744     by (simp add: zero_le_mult_iff)
   745   also have "... \<longleftrightarrow> Arg z = 0"
   746     apply (auto simp: Re_exp)
   747     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)
   748     using Arg_eq [of z]
   749     apply (auto simp: Reals_def)
   750     done
   751   finally show ?thesis
   752     by blast
   753 qed
   754 
   755 corollary Arg_gt_0: 
   756   assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
   757     shows "Arg z > 0"
   758   using Arg_eq_0 Arg_ge_0 assms dual_order.strict_iff_order by fastforce
   759 
   760 lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
   761   by (simp add: Arg_eq_0)
   762 
   763 lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
   764   apply  (cases "z=0", simp)
   765   using Arg_eq_0 [of "-z"]
   766   apply (auto simp: complex_is_Real_iff Arg_minus)
   767   apply (simp add: complex_Re_Im_cancel_iff)
   768   apply (metis Arg_minus pi_gt_zero add.left_neutral minus_minus minus_zero)
   769   done
   770 
   771 lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
   772   using Arg_eq_0 Arg_eq_pi not_le by auto
   773 
   774 lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   775   apply (cases "z=0", simp)
   776   apply (rule Arg_unique [of "inverse (norm z)"])
   777   using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] Exp_two_pi_i
   778   apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
   779   done
   780 
   781 lemma Arg_eq_iff:
   782   assumes "w \<noteq> 0" "z \<noteq> 0"
   783      shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
   784   using assms Arg_eq [of z] Arg_eq [of w]
   785   apply auto
   786   apply (rule_tac x="norm w / norm z" in exI)
   787   apply (simp add: divide_simps)
   788   by (metis mult.commute mult.left_commute)
   789 
   790 lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
   791   using complex_is_Real_iff
   792   apply (simp add: Arg_eq_0)
   793   apply (auto simp: divide_simps not_sum_power2_lt_zero)
   794   done
   795 
   796 lemma Arg_divide:
   797   assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
   798     shows "Arg(z / w) = Arg z - Arg w"
   799   apply (rule Arg_unique [of "norm(z / w)"])
   800   using assms Arg_eq [of z] Arg_eq [of w] Arg_ge_0 [of w] Arg_lt_2pi [of z]
   801   apply (auto simp: exp_diff norm_divide algebra_simps divide_simps)
   802   done
   803 
   804 lemma Arg_le_div_sum:
   805   assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
   806     shows "Arg z = Arg w + Arg(z / w)"
   807   by (simp add: Arg_divide assms)
   808 
   809 lemma Arg_le_div_sum_eq:
   810   assumes "w \<noteq> 0" "z \<noteq> 0"
   811     shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
   812   using assms
   813   by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
   814 
   815 lemma Arg_diff:
   816   assumes "w \<noteq> 0" "z \<noteq> 0"
   817     shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
   818   using assms
   819   apply (auto simp: Arg_ge_0 Arg_divide not_le)
   820   using Arg_divide [of w z] Arg_inverse [of "w/z"]
   821   apply auto
   822   by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
   823 
   824 lemma Arg_add:
   825   assumes "w \<noteq> 0" "z \<noteq> 0"
   826     shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
   827   using assms
   828   using Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
   829   apply (auto simp: Arg_ge_0 Arg_divide not_le)
   830   apply (metis Arg_lt_2pi add.commute)
   831   apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
   832   done
   833 
   834 lemma Arg_times:
   835   assumes "w \<noteq> 0" "z \<noteq> 0"
   836     shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
   837                             else (Arg w + Arg z) - 2*pi)"
   838   using Arg_add [OF assms]
   839   by auto
   840 
   841 lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   842   apply (cases "z=0", simp)
   843   apply (rule trans [of _ "Arg(inverse z)"])
   844   apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
   845   apply (metis norm_eq_zero of_real_power zero_less_power2)
   846   apply (auto simp: of_real_numeral Arg_inverse)
   847   done
   848 
   849 lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
   850   using Arg_eq_0 Arg_eq_0_pi
   851   by auto
   852 
   853 lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
   854   by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
   855 
   856 
   857 subsection\<open>Analytic properties of tangent function\<close>
   858 
   859 lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
   860   by (simp add: cnj_cos cnj_sin tan_def)
   861 
   862 lemma complex_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan complex_differentiable at z"
   863   unfolding complex_differentiable_def
   864   using DERIV_tan by blast
   865 
   866 lemma complex_differentiable_within_tan: "~(cos z = 0)
   867          \<Longrightarrow> tan complex_differentiable (at z within s)"
   868   using complex_differentiable_at_tan complex_differentiable_at_within by blast
   869 
   870 lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
   871   using continuous_at_imp_continuous_within isCont_tan by blast
   872 
   873 lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan"
   874   by (simp add: continuous_at_imp_continuous_on)
   875 
   876 lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
   877   by (simp add: complex_differentiable_within_tan holomorphic_on_def)
   878 
   879 
   880 subsection\<open>Complex logarithms (the conventional principal value)\<close>
   881 
   882 instantiation complex :: ln
   883 begin
   884 
   885 definition ln_complex :: "complex \<Rightarrow> complex"
   886   where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
   887 
   888 lemma
   889   assumes "z \<noteq> 0"
   890     shows exp_Ln [simp]:  "exp(ln z) = z"
   891       and mpi_less_Im_Ln: "-pi < Im(ln z)"
   892       and Im_Ln_le_pi:    "Im(ln z) \<le> pi"
   893 proof -
   894   obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
   895     using complex_unimodular_polar [of "z / (norm z)"] assms
   896     by (auto simp: norm_divide divide_simps)
   897   obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
   898     using sincos_principal_value [of "\<psi>"] assms
   899     by (auto simp: norm_divide divide_simps)
   900   have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \<le> pi" unfolding ln_complex_def
   901     apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
   902     using z assms \<phi>
   903     apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
   904     done
   905   then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \<le> pi"
   906     by auto
   907 qed
   908 
   909 lemma Ln_exp [simp]:
   910   assumes "-pi < Im(z)" "Im(z) \<le> pi"
   911     shows "ln(exp z) = z"
   912   apply (rule exp_complex_eqI)
   913   using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
   914   apply auto
   915   done
   916 
   917 subsection\<open>Relation to Real Logarithm\<close>
   918 
   919 lemma Ln_of_real:
   920   assumes "0 < z"
   921     shows "ln(of_real z::complex) = of_real(ln z)"
   922 proof -
   923   have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"
   924     by (simp add: exp_of_real)
   925   also have "... = of_real(ln z)"
   926     using assms
   927     by (subst Ln_exp) auto
   928   finally show ?thesis
   929     using assms by simp
   930 qed
   931 
   932 corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
   933   by (auto simp: Ln_of_real elim: Reals_cases)
   934 
   935 corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
   936   by (simp add: Ln_of_real)
   937 
   938 lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
   939   using Ln_of_real by force
   940 
   941 lemma Ln_1: "ln 1 = (0::complex)"
   942 proof -
   943   have "ln (exp 0) = (0::complex)"
   944     by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one)
   945   then show ?thesis
   946     by simp
   947 qed
   948 
   949 instance
   950   by intro_classes (rule ln_complex_def Ln_1)
   951 
   952 end
   953 
   954 abbreviation Ln :: "complex \<Rightarrow> complex"
   955   where "Ln \<equiv> ln"
   956 
   957 lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
   958   by (metis exp_Ln)
   959 
   960 lemma Ln_unique: "exp(z) = w \<Longrightarrow> -pi < Im(z) \<Longrightarrow> Im(z) \<le> pi \<Longrightarrow> Ln w = z"
   961   using Ln_exp by blast
   962 
   963 lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
   964   by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
   965 
   966 corollary ln_cmod_le: 
   967   assumes z: "z \<noteq> 0"
   968     shows "ln (cmod z) \<le> cmod (Ln z)"
   969   using norm_exp [of "Ln z", simplified exp_Ln [OF z]]
   970   by (metis Re_Ln complex_Re_le_cmod z)
   971 
   972 lemma exists_complex_root:
   973   fixes a :: complex
   974   shows "n \<noteq> 0 \<Longrightarrow> \<exists>z. z ^ n = a"
   975   apply (cases "a=0", simp)
   976   apply (rule_tac x= "exp(Ln(a) / n)" in exI)
   977   apply (auto simp: exp_of_nat_mult [symmetric])
   978   done
   979 
   980 
   981 subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
   982 
   983 text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
   984 
   985 definition unwinding :: "complex \<Rightarrow> complex" where
   986    "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * ii)"
   987 
   988 lemma unwinding_2pi: "(2*pi) * ii * unwinding(z) = z - Ln(exp z)"
   989   by (simp add: unwinding_def)
   990 
   991 lemma Ln_times_unwinding:
   992     "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * ii * unwinding(Ln w + Ln z)"
   993   using unwinding_2pi by (simp add: exp_add)
   994 
   995 
   996 subsection\<open>Derivative of Ln away from the branch cut\<close>
   997 
   998 lemma
   999   assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)"
  1000     shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
  1001       and Im_Ln_less_pi:           "Im (Ln z) < pi"
  1002 proof -
  1003   have znz: "z \<noteq> 0"
  1004     using assms by auto
  1005   then show *: "Im (Ln z) < pi" using assms
  1006     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)
  1007   show "(Ln has_field_derivative inverse(z)) (at z)"
  1008     apply (rule has_complex_derivative_inverse_strong_x
  1009               [where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"])
  1010     using znz *
  1011     apply (auto simp: continuous_on_exp open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
  1012     apply (metis DERIV_exp exp_Ln)
  1013     apply (metis mpi_less_Im_Ln)
  1014     done
  1015 qed
  1016 
  1017 declare has_field_derivative_Ln [derivative_intros]
  1018 declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
  1019 
  1020 lemma complex_differentiable_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln complex_differentiable at z"
  1021   using complex_differentiable_def has_field_derivative_Ln by blast
  1022 
  1023 lemma complex_differentiable_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z))
  1024          \<Longrightarrow> Ln complex_differentiable (at z within s)"
  1025   using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
  1026 
  1027 lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
  1028   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
  1029 
  1030 lemma isCont_Ln' [simp]:
  1031    "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
  1032   by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
  1033 
  1034 lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
  1035   using continuous_at_Ln continuous_at_imp_continuous_within by blast
  1036 
  1037 lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s Ln"
  1038   by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
  1039 
  1040 lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln holomorphic_on s"
  1041   by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
  1042 
  1043 
  1044 subsection\<open>Quadrant-type results for Ln\<close>
  1045 
  1046 lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
  1047   using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
  1048   by simp
  1049 
  1050 lemma Re_Ln_pos_lt:
  1051   assumes "z \<noteq> 0"
  1052     shows "abs(Im(Ln z)) < pi/2 \<longleftrightarrow> 0 < Re(z)"
  1053 proof -
  1054   { fix w
  1055     assume "w = Ln z"
  1056     then have w: "Im w \<le> pi" "- pi < Im w"
  1057       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1058       by auto
  1059     then have "abs(Im w) < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
  1060       apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
  1061       using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
  1062       apply (simp add: abs_if split: split_if_asm)
  1063       apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4)
  1064                less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right
  1065                mult_numeral_1_right)
  1066       done
  1067   }
  1068   then show ?thesis using assms
  1069     by auto
  1070 qed
  1071 
  1072 lemma Re_Ln_pos_le:
  1073   assumes "z \<noteq> 0"
  1074     shows "abs(Im(Ln z)) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
  1075 proof -
  1076   { fix w
  1077     assume "w = Ln z"
  1078     then have w: "Im w \<le> pi" "- pi < Im w"
  1079       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1080       by auto
  1081     then have "abs(Im w) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
  1082       apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
  1083       using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
  1084       apply (auto simp: abs_if split: split_if_asm)
  1085       done
  1086   }
  1087   then show ?thesis using assms
  1088     by auto
  1089 qed
  1090 
  1091 lemma Im_Ln_pos_lt:
  1092   assumes "z \<noteq> 0"
  1093     shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
  1094 proof -
  1095   { fix w
  1096     assume "w = Ln z"
  1097     then have w: "Im w \<le> pi" "- pi < Im w"
  1098       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1099       by auto
  1100     then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)"
  1101       using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"]
  1102       apply (auto simp: Im_exp zero_less_mult_iff)
  1103       using less_linear apply fastforce
  1104       using less_linear apply fastforce
  1105       done
  1106   }
  1107   then show ?thesis using assms
  1108     by auto
  1109 qed
  1110 
  1111 lemma Im_Ln_pos_le:
  1112   assumes "z \<noteq> 0"
  1113     shows "0 \<le> Im(Ln z) \<and> Im(Ln z) \<le> pi \<longleftrightarrow> 0 \<le> Im(z)"
  1114 proof -
  1115   { fix w
  1116     assume "w = Ln z"
  1117     then have w: "Im w \<le> pi" "- pi < Im w"
  1118       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1119       by auto
  1120     then have "0 \<le> Im w \<and> Im w \<le> pi \<longleftrightarrow> 0 \<le> Im(exp w)"
  1121       using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"]
  1122       apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero)
  1123       apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi)
  1124       done }
  1125   then show ?thesis using assms
  1126     by auto
  1127 qed
  1128 
  1129 lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> abs(Im(Ln z)) < pi/2"
  1130   by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
  1131 
  1132 lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
  1133   by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))
  1134 
  1135 lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
  1136   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
  1137        complex_eq exp_of_real le_less mult_zero_right norm_exp_eq_Re norm_le_zero_iff not_le of_real_0)
  1138 
  1139 lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
  1140   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)
  1141 
  1142 
  1143 subsection\<open>More Properties of Ln\<close>
  1144 
  1145 lemma cnj_Ln: "(Im z = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
  1146   apply (cases "z=0", auto)
  1147   apply (rule exp_complex_eqI)
  1148   apply (auto simp: abs_if split: split_if_asm)
  1149   apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps mult_2 neg_equal_0_iff_equal)
  1150   apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff mpi_less_Im_Ln mult.commute mult_2_right)
  1151   by (metis exp_Ln exp_cnj)
  1152 
  1153 lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
  1154   apply (cases "z=0", auto)
  1155   apply (rule exp_complex_eqI)
  1156   using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
  1157   apply (auto simp: abs_if exp_minus split: split_if_asm)
  1158   apply (metis Im_Ln_less_pi Im_Ln_pos_le add_less_cancel_left add_strict_mono
  1159                inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
  1160   done
  1161 
  1162 lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
  1163   apply (rule exp_complex_eqI)
  1164   using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
  1165   apply (auto simp: abs_if)
  1166   done
  1167 
  1168 lemma Ln_ii [simp]: "Ln ii = ii * of_real pi/2"
  1169   using Ln_exp [of "ii * (of_real pi/2)"]
  1170   unfolding exp_Euler
  1171   by simp
  1172 
  1173 lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)"
  1174 proof -
  1175   have  "Ln(-ii) = Ln(1/ii)"
  1176     by simp
  1177   also have "... = - (Ln ii)"
  1178     by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one)
  1179   also have "... = - (ii * pi/2)"
  1180     by simp
  1181   finally show ?thesis .
  1182 qed
  1183 
  1184 lemma Ln_times:
  1185   assumes "w \<noteq> 0" "z \<noteq> 0"
  1186     shows "Ln(w * z) =
  1187                 (if Im(Ln w + Ln z) \<le> -pi then
  1188                   (Ln(w) + Ln(z)) + ii * of_real(2*pi)
  1189                 else if Im(Ln w + Ln z) > pi then
  1190                   (Ln(w) + Ln(z)) - ii * of_real(2*pi)
  1191                 else Ln(w) + Ln(z))"
  1192   using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
  1193   using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
  1194   by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
  1195 
  1196 corollary Ln_times_simple:
  1197     "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
  1198          \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
  1199   by (simp add: Ln_times)
  1200 
  1201 corollary Ln_times_of_real:
  1202     "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(of_real r * z) = ln r + Ln(z)"
  1203   using mpi_less_Im_Ln Im_Ln_le_pi
  1204   by (force simp: Ln_times)
  1205 
  1206 corollary Ln_divide_of_real:
  1207     "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
  1208 using Ln_times_of_real [of "inverse r" z]
  1209 by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric] 
  1210          del: of_real_inverse)
  1211 
  1212 lemma Ln_minus:
  1213   assumes "z \<noteq> 0"
  1214     shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
  1215                      then Ln(z) + ii * pi
  1216                      else Ln(z) - ii * pi)" (is "_ = ?rhs")
  1217   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
  1218         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
  1219     by (auto simp: of_real_numeral exp_add exp_diff exp_Euler intro!: Ln_unique)
  1220 
  1221 lemma Ln_inverse_if:
  1222   assumes "z \<noteq> 0"
  1223     shows "Ln (inverse z) =
  1224             (if (Im(z) = 0 \<longrightarrow> 0 < Re z)
  1225              then -(Ln z)
  1226              else -(Ln z) + \<i> * 2 * complex_of_real pi)"
  1227 proof (cases "(Im(z) = 0 \<longrightarrow> 0 < Re z)")
  1228   case True then show ?thesis
  1229     by (simp add: Ln_inverse)
  1230 next
  1231   case False
  1232   then have z: "Im z = 0" "Re z < 0"
  1233     using assms
  1234     apply auto
  1235     by (metis cnj.code complex_cnj_cnj not_less_iff_gr_or_eq zero_complex.simps(1) zero_complex.simps(2))
  1236   have "Ln(inverse z) = Ln(- (inverse (-z)))"
  1237     by simp
  1238   also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
  1239     using assms z
  1240     apply (simp add: Ln_minus)
  1241     apply (simp add: field_simps)
  1242     done
  1243   also have "... = - Ln (- z) + \<i> * complex_of_real pi"
  1244     apply (subst Ln_inverse)
  1245     using z assms by auto
  1246   also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
  1247     apply (subst Ln_minus [OF assms])
  1248     using assms z
  1249     apply simp
  1250     done
  1251   finally show ?thesis
  1252     using assms z
  1253     by simp
  1254 qed
  1255 
  1256 lemma Ln_times_ii:
  1257   assumes "z \<noteq> 0"
  1258     shows  "Ln(ii * z) = (if 0 \<le> Re(z) | Im(z) < 0
  1259                           then Ln(z) + ii * of_real pi/2
  1260                           else Ln(z) - ii * of_real(3 * pi/2))"
  1261   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
  1262         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
  1263   by (auto simp: of_real_numeral Ln_times)
  1264 
  1265 
  1266 subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
  1267 
  1268 lemma Arg_Ln: 
  1269   assumes "0 < Arg z" shows "Arg z = Im(Ln(-z)) + pi"
  1270 proof (cases "z = 0")
  1271   case True
  1272   with assms show ?thesis
  1273     by simp
  1274 next
  1275   case False
  1276   then have "z / of_real(norm z) = exp(ii * of_real(Arg z))"
  1277     using Arg [of z]
  1278     by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff)
  1279   then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
  1280     using cis_conv_exp cis_pi
  1281     by (auto simp: exp_diff algebra_simps)
  1282   then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg z) - pi)))"
  1283     by simp
  1284   also have "... = \<i> * (of_real(Arg z) - pi)"
  1285     using Arg [of z] assms pi_not_less_zero
  1286     by auto
  1287   finally have "Arg z =  Im (Ln (- z / of_real (cmod z))) + pi"
  1288     by simp
  1289   also have "... = Im (Ln (-z) - ln (cmod z)) + pi"
  1290     by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)
  1291   also have "... = Im (Ln (-z)) + pi"
  1292     by simp
  1293   finally show ?thesis .
  1294 qed
  1295 
  1296 lemma continuous_at_Arg: 
  1297   assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
  1298     shows "continuous (at z) Arg"
  1299 proof -
  1300   have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
  1301     by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
  1302   then show ?thesis
  1303     apply (simp add: continuous_at)
  1304     apply (rule Lim_transform_within_open [of "-{z. z \<in> \<real> & 0 \<le> Re z}" _ "\<lambda>z. Im(Ln(-z)) + pi"])
  1305     apply (simp add: closed_def [symmetric] closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge)
  1306     apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0])
  1307     done
  1308 qed
  1309 
  1310 text\<open>Relation between Arg and arctangent in upper halfplane\<close>
  1311 lemma Arg_arctan_upperhalf: 
  1312   assumes "0 < Im z"
  1313     shows "Arg z = pi/2 - arctan(Re z / Im z)"
  1314 proof (cases "z = 0")
  1315   case True with assms show ?thesis
  1316     by simp
  1317 next
  1318   case False
  1319   show ?thesis
  1320     apply (rule Arg_unique [of "norm z"])
  1321     using False assms arctan [of "Re z / Im z"] pi_ge_two pi_half_less_two
  1322     apply (auto simp: exp_Euler cos_diff sin_diff)
  1323     using norm_complex_def [of z, symmetric]
  1324     apply (simp add: of_real_numeral sin_of_real cos_of_real sin_arctan cos_arctan field_simps real_sqrt_divide)
  1325     apply (metis complex_eq mult.assoc ring_class.ring_distribs(2))
  1326     done
  1327 qed
  1328 
  1329 lemma Arg_eq_Im_Ln: 
  1330   assumes "0 \<le> Im z" "0 < Re z" 
  1331     shows "Arg z = Im (Ln z)"
  1332 proof (cases "z = 0 \<or> Im z = 0")
  1333   case True then show ?thesis
  1334     using assms Arg_eq_0 complex_is_Real_iff  
  1335     apply auto
  1336     by (metis Arg_eq_0_pi Arg_eq_pi Im_Ln_eq_0 Im_Ln_eq_pi less_numeral_extra(3) zero_complex.simps(1))
  1337 next
  1338   case False 
  1339   then have "Arg z > 0"
  1340     using Arg_gt_0 complex_is_Real_iff by blast
  1341   then show ?thesis
  1342     using assms False 
  1343     by (subst Arg_Ln) (auto simp: Ln_minus)
  1344 qed
  1345 
  1346 lemma continuous_within_upperhalf_Arg: 
  1347   assumes "z \<noteq> 0"
  1348     shows "continuous (at z within {z. 0 \<le> Im z}) Arg"
  1349 proof (cases "z \<in> \<real> & 0 \<le> Re z")
  1350   case False then show ?thesis
  1351     using continuous_at_Arg continuous_at_imp_continuous_within by auto
  1352 next
  1353   case True
  1354   then have z: "z \<in> \<real>" "0 < Re z"
  1355     using assms  by (auto simp: complex_is_Real_iff complex_neq_0)
  1356   then have [simp]: "Arg z = 0" "Im (Ln z) = 0"
  1357     by (auto simp: Arg_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
  1358   show ?thesis  
  1359   proof (clarsimp simp add: continuous_within Lim_within dist_norm)
  1360     fix e::real
  1361     assume "0 < e"
  1362     moreover have "continuous (at z) (\<lambda>x. Im (Ln x))"
  1363       using z  by (rule continuous_intros | simp)
  1364     ultimately
  1365     obtain d where d: "d>0" "\<And>x. x \<noteq> z \<Longrightarrow> cmod (x - z) < d \<Longrightarrow> \<bar>Im (Ln x)\<bar> < e"
  1366       by (auto simp: continuous_within Lim_within dist_norm)
  1367     { fix x
  1368       assume "cmod (x - z) < Re z / 2"
  1369       then have "\<bar>Re x - Re z\<bar> < Re z / 2"
  1370         by (metis le_less_trans abs_Re_le_cmod minus_complex.simps(1))
  1371       then have "0 < Re x"
  1372         using z by linarith
  1373     }
  1374     then show "\<exists>d>0. \<forall>x. 0 \<le> Im x \<longrightarrow> x \<noteq> z \<and> cmod (x - z) < d \<longrightarrow> \<bar>Arg x\<bar> < e"
  1375       apply (rule_tac x="min d (Re z / 2)" in exI)
  1376       using z d
  1377       apply (auto simp: Arg_eq_Im_Ln)
  1378       done
  1379   qed
  1380 qed
  1381 
  1382 lemma continuous_on_upperhalf_Arg: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg"
  1383   apply (auto simp: continuous_on_eq_continuous_within)
  1384   by (metis Diff_subset continuous_within_subset continuous_within_upperhalf_Arg)
  1385 
  1386 lemma open_Arg_less_Int: 
  1387   assumes "0 \<le> s" "t \<le> 2*pi"
  1388     shows "open ({y. s < Arg y} \<inter> {y. Arg y < t})"
  1389 proof -
  1390   have 1: "continuous_on (UNIV - {z \<in> \<real>. 0 \<le> Re z}) Arg"
  1391     using continuous_at_Arg continuous_at_imp_continuous_within 
  1392     by (auto simp: continuous_on_eq_continuous_within set_diff_eq)
  1393   have 2: "open (UNIV - {z \<in> \<real>. 0 \<le> Re z})"
  1394     by (simp add: closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge open_Diff)
  1395   have "open ({z. s < z} \<inter> {z. z < t})"
  1396     using open_lessThan [of t] open_greaterThan [of s]
  1397     by (metis greaterThan_def lessThan_def open_Int)
  1398   moreover have "{y. s < Arg y} \<inter> {y. Arg y < t} \<subseteq> - {z \<in> \<real>. 0 \<le> Re z}"
  1399     using assms
  1400     by (auto simp: Arg_real)
  1401   ultimately show ?thesis
  1402     using continuous_imp_open_vimage [OF 1 2, of  "{z. Re z > s} \<inter> {z. Re z < t}"] 
  1403     by auto
  1404 qed
  1405 
  1406 lemma open_Arg_gt: "open {z. t < Arg z}"
  1407 proof (cases "t < 0")
  1408   case True then have "{z. t < Arg z} = UNIV"
  1409     using Arg_ge_0 less_le_trans by auto
  1410   then show ?thesis
  1411     by simp
  1412 next
  1413   case False then show ?thesis
  1414     using open_Arg_less_Int [of t "2*pi"] Arg_lt_2pi
  1415     by auto
  1416 qed
  1417 
  1418 lemma closed_Arg_le: "closed {z. Arg z \<le> t}"
  1419   using open_Arg_gt [of t]
  1420   by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)
  1421 
  1422 subsection\<open>Complex Powers\<close>
  1423 
  1424 lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
  1425   by (simp add: powr_def)
  1426 
  1427 lemma powr_nat:
  1428   fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
  1429   by (simp add: exp_of_nat_mult powr_def)
  1430 
  1431 lemma powr_add_complex:
  1432   fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
  1433   by (simp add: powr_def algebra_simps exp_add)
  1434 
  1435 lemma powr_minus_complex:
  1436   fixes w::complex shows  "w powr (-z) = inverse(w powr z)"
  1437   by (simp add: powr_def exp_minus)
  1438 
  1439 lemma powr_diff_complex:
  1440   fixes w::complex shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
  1441   by (simp add: powr_def algebra_simps exp_diff)
  1442 
  1443 lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
  1444   apply (simp add: powr_def)
  1445   using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
  1446   by auto
  1447 
  1448 lemma powr_real_real:
  1449     "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
  1450   apply (simp add: powr_def)
  1451   by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
  1452        exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
  1453 
  1454 lemma powr_of_real:
  1455   fixes x::real and y::real
  1456   shows "0 < x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
  1457   by (simp add: powr_def) (metis exp_of_real of_real_mult Ln_of_real)
  1458 
  1459 lemma norm_powr_real_mono:
  1460     "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
  1461      \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
  1462   by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
  1463 
  1464 lemma powr_times_real:
  1465     "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
  1466            \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
  1467   by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
  1468 
  1469 lemma has_field_derivative_powr:
  1470     "(Im z = 0 \<Longrightarrow> 0 < Re z)
  1471      \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
  1472   apply (cases "z=0", auto)
  1473   apply (simp add: powr_def)
  1474   apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
  1475   apply (auto simp: dist_complex_def)
  1476   apply (intro derivative_eq_intros | simp add: assms)+
  1477   apply (simp add: field_simps exp_diff)
  1478   done
  1479 
  1480 lemma has_field_derivative_powr_right:
  1481     "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
  1482   apply (simp add: powr_def)
  1483   apply (intro derivative_eq_intros | simp add: assms)+
  1484   done
  1485 
  1486 lemma complex_differentiable_powr_right:
  1487     "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
  1488 using complex_differentiable_def has_field_derivative_powr_right by blast
  1489 
  1490 lemma holomorphic_on_powr_right:
  1491     "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
  1492     unfolding holomorphic_on_def
  1493     using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
  1494 
  1495 lemma norm_powr_real_powr:
  1496   "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
  1497   by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm)
  1498 
  1499 
  1500 subsection\<open>Some Limits involving Logarithms\<close>
  1501         
  1502 lemma lim_Ln_over_power:
  1503   fixes s::complex
  1504   assumes "0 < Re s"
  1505     shows "((\<lambda>n. Ln n / (n powr s)) ---> 0) sequentially"
  1506 proof (simp add: lim_sequentially dist_norm, clarify)
  1507   fix e::real 
  1508   assume e: "0 < e"
  1509   have "\<exists>xo>0. \<forall>x\<ge>xo. 0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
  1510   proof (rule_tac x="2/(e * (Re s)\<^sup>2)" in exI, safe)
  1511     show "0 < 2 / (e * (Re s)\<^sup>2)"
  1512       using e assms by (simp add: field_simps)
  1513   next
  1514     fix x::real
  1515     assume x: "2 / (e * (Re s)\<^sup>2) \<le> x"
  1516     then have "x>0"
  1517     using e assms
  1518       by (metis less_le_trans mult_eq_0_iff mult_pos_pos pos_less_divide_eq power2_eq_square
  1519                 zero_less_numeral)
  1520     then show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
  1521       using e assms x
  1522       apply (auto simp: field_simps)
  1523       apply (rule_tac y = "e * (x\<^sup>2 * (Re s)\<^sup>2)" in le_less_trans)
  1524       apply (auto simp: power2_eq_square field_simps add_pos_pos)
  1525       done
  1526   qed
  1527   then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < 1 + (Re s * x) + (1/2) * (Re s * x)^2"
  1528     using e  by (simp add: field_simps)
  1529   then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < exp (Re s * x)"
  1530     using assms
  1531     by (force intro: less_le_trans [OF _ exp_lower_taylor_quadratic])
  1532   then have "\<exists>xo>0. \<forall>x\<ge>xo. x < e * exp (Re s * x)"
  1533     using e   by (auto simp: field_simps)
  1534   with e show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
  1535     apply (auto simp: norm_divide norm_powr_real divide_simps)
  1536     apply (rule_tac x="nat (ceiling (exp xo))" in exI)
  1537     apply clarify
  1538     apply (drule_tac x="ln n" in spec)
  1539     apply (auto simp: real_of_nat_def exp_less_mono nat_ceiling_le_eq not_le)
  1540     apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff)
  1541     done
  1542 qed
  1543 
  1544 lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) ---> 0) sequentially"
  1545   using lim_Ln_over_power [of 1]
  1546   by simp
  1547 
  1548 lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
  1549   using Ln_of_real by force
  1550 
  1551 lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
  1552   by (simp add: powr_of_real)
  1553 
  1554 lemma lim_ln_over_power:
  1555   fixes s :: real
  1556   assumes "0 < s"
  1557     shows "((\<lambda>n. ln n / (n powr s)) ---> 0) sequentially"
  1558   using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
  1559   apply (subst filterlim_sequentially_Suc [symmetric])
  1560   apply (simp add: lim_sequentially dist_norm
  1561           Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def)
  1562   done
  1563 
  1564 lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) ---> 0) sequentially"
  1565   using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]]
  1566   apply (subst filterlim_sequentially_Suc [symmetric])
  1567   apply (simp add: lim_sequentially dist_norm real_of_nat_def)
  1568   done
  1569 
  1570 lemma lim_1_over_complex_power:
  1571   assumes "0 < Re s"
  1572     shows "((\<lambda>n. 1 / (of_nat n powr s)) ---> 0) sequentially"
  1573 proof -
  1574   have "\<forall>n>0. 3 \<le> n \<longrightarrow> 1 \<le> ln (real_of_nat n)"
  1575     using ln3_gt_1
  1576     by (force intro: order_trans [of _ "ln 3"] ln3_gt_1)
  1577   moreover have "(\<lambda>n. cmod (Ln (of_nat n) / of_nat n powr s)) ----> 0"
  1578     using lim_Ln_over_power [OF assms]
  1579     by (metis tendsto_norm_zero_iff)
  1580   ultimately show ?thesis
  1581     apply (auto intro!: Lim_null_comparison [where g = "\<lambda>n. norm (Ln(of_nat n) / of_nat n powr s)"])
  1582     apply (auto simp: norm_divide divide_simps eventually_sequentially)
  1583     done
  1584 qed
  1585 
  1586 lemma lim_1_over_real_power:
  1587   fixes s :: real
  1588   assumes "0 < s"
  1589     shows "((\<lambda>n. 1 / (of_nat n powr s)) ---> 0) sequentially"
  1590   using lim_1_over_complex_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
  1591   apply (subst filterlim_sequentially_Suc [symmetric])
  1592   apply (simp add: lim_sequentially dist_norm)
  1593   apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def)
  1594   done
  1595 
  1596 lemma lim_1_over_Ln: "((\<lambda>n. 1 / Ln(of_nat n)) ---> 0) sequentially"
  1597 proof (clarsimp simp add: lim_sequentially dist_norm norm_divide divide_simps)
  1598   fix r::real
  1599   assume "0 < r"
  1600   have ir: "inverse (exp (inverse r)) > 0"
  1601     by simp
  1602   obtain n where n: "1 < of_nat n * inverse (exp (inverse r))"
  1603     using ex_less_of_nat_mult [of _ 1, OF ir]
  1604     by auto
  1605   then have "exp (inverse r) < of_nat n"
  1606     by (simp add: divide_simps)
  1607   then have "ln (exp (inverse r)) < ln (of_nat n)"
  1608     by (metis exp_gt_zero less_trans ln_exp ln_less_cancel_iff)
  1609   with \<open>0 < r\<close> have "1 < r * ln (real_of_nat n)"
  1610     by (simp add: field_simps)
  1611   moreover have "n > 0" using n
  1612     using neq0_conv by fastforce
  1613   ultimately show "\<exists>no. \<forall>n. Ln (of_nat n) \<noteq> 0 \<longrightarrow> no \<le> n \<longrightarrow> 1 < r * cmod (Ln (of_nat n))"
  1614     using n \<open>0 < r\<close>
  1615     apply (rule_tac x=n in exI)
  1616     apply (auto simp: divide_simps)
  1617     apply (erule less_le_trans, auto)
  1618     done
  1619 qed
  1620 
  1621 lemma lim_1_over_ln: "((\<lambda>n. 1 / ln(real_of_nat n)) ---> 0) sequentially"
  1622   using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]] assms
  1623   apply (subst filterlim_sequentially_Suc [symmetric])
  1624   apply (simp add: lim_sequentially dist_norm)
  1625   apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def)
  1626   done
  1627 
  1628 
  1629 subsection\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
  1630 
  1631 lemma csqrt_exp_Ln:
  1632   assumes "z \<noteq> 0"
  1633     shows "csqrt z = exp(Ln(z) / 2)"
  1634 proof -
  1635   have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
  1636     by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
  1637   also have "... = z"
  1638     using assms exp_Ln by blast
  1639   finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
  1640     by simp
  1641   also have "... = exp (Ln z / 2)"
  1642     apply (subst csqrt_square)
  1643     using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
  1644     apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+)
  1645     done
  1646   finally show ?thesis using assms csqrt_square
  1647     by simp
  1648 qed
  1649 
  1650 lemma csqrt_inverse:
  1651   assumes "Im(z) = 0 \<Longrightarrow> 0 < Re z"
  1652     shows "csqrt (inverse z) = inverse (csqrt z)"
  1653 proof (cases "z=0", simp)
  1654   assume "z \<noteq> 0 "
  1655   then show ?thesis
  1656     using assms
  1657     by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
  1658 qed
  1659 
  1660 lemma cnj_csqrt:
  1661   assumes "Im z = 0 \<Longrightarrow> 0 \<le> Re(z)"
  1662     shows "cnj(csqrt z) = csqrt(cnj z)"
  1663 proof (cases "z=0", simp)
  1664   assume z: "z \<noteq> 0"
  1665   then have "Im z = 0 \<Longrightarrow> 0 < Re(z)"
  1666     using assms cnj.code complex_cnj_zero_iff by fastforce
  1667   then show ?thesis
  1668    using z by (simp add: csqrt_exp_Ln cnj_Ln exp_cnj)
  1669 qed
  1670 
  1671 lemma has_field_derivative_csqrt:
  1672   assumes "Im z = 0 \<Longrightarrow> 0 < Re(z)"
  1673     shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)"
  1674 proof -
  1675   have z: "z \<noteq> 0"
  1676     using assms by auto
  1677   then have *: "inverse z = inverse (2*z) * 2"
  1678     by (simp add: divide_simps)
  1679   show ?thesis
  1680     apply (rule DERIV_transform_at [where f = "\<lambda>z. exp(Ln(z) / 2)" and d = "norm z"])
  1681     apply (intro derivative_eq_intros | simp add: assms)+
  1682     apply (rule *)
  1683     using z
  1684     apply (auto simp: field_simps csqrt_exp_Ln [symmetric])
  1685     apply (metis power2_csqrt power2_eq_square)
  1686     apply (metis csqrt_exp_Ln dist_0_norm less_irrefl)
  1687     done
  1688 qed
  1689 
  1690 lemma complex_differentiable_at_csqrt:
  1691     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable at z"
  1692   using complex_differentiable_def has_field_derivative_csqrt by blast
  1693 
  1694 lemma complex_differentiable_within_csqrt:
  1695     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable (at z within s)"
  1696   using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast
  1697 
  1698 lemma continuous_at_csqrt:
  1699     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
  1700   by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
  1701 
  1702 corollary isCont_csqrt' [simp]:
  1703    "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
  1704   by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
  1705 
  1706 lemma continuous_within_csqrt:
  1707     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
  1708   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
  1709 
  1710 lemma continuous_on_csqrt [continuous_intros]:
  1711     "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s csqrt"
  1712   by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
  1713 
  1714 lemma holomorphic_on_csqrt:
  1715     "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt holomorphic_on s"
  1716   by (simp add: complex_differentiable_within_csqrt holomorphic_on_def)
  1717 
  1718 lemma continuous_within_closed_nontrivial:
  1719     "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
  1720   using open_Compl
  1721   by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
  1722 
  1723 lemma continuous_within_csqrt_posreal:
  1724     "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
  1725 proof (cases "Im z = 0 --> 0 < Re(z)")
  1726   case True then show ?thesis
  1727     by (blast intro: continuous_within_csqrt)
  1728 next
  1729   case False
  1730   then have "Im z = 0" "Re z < 0 \<or> z = 0"
  1731     using False cnj.code complex_cnj_zero_iff by auto force
  1732   then show ?thesis
  1733     apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
  1734     apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
  1735     apply (rule_tac x="e^2" in exI)
  1736     apply (auto simp: Reals_def)
  1737 by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
  1738 qed
  1739 
  1740 subsection\<open>Complex arctangent\<close>
  1741 
  1742 text\<open>branch cut gives standard bounds in real case.\<close>
  1743 
  1744 definition Arctan :: "complex \<Rightarrow> complex" where
  1745     "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))"
  1746 
  1747 lemma Arctan_0 [simp]: "Arctan 0 = 0"
  1748   by (simp add: Arctan_def)
  1749 
  1750 lemma Im_complex_div_lemma: "Im((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<longleftrightarrow> Re z = 0"
  1751   by (auto simp: Im_complex_div_eq_0 algebra_simps)
  1752 
  1753 lemma Re_complex_div_lemma: "0 < Re((1 - \<i>*z) / (1 + \<i>*z)) \<longleftrightarrow> norm z < 1"
  1754   by (simp add: Re_complex_div_gt_0 algebra_simps cmod_def power2_eq_square)
  1755 
  1756 lemma tan_Arctan:
  1757   assumes "z\<^sup>2 \<noteq> -1"
  1758     shows [simp]:"tan(Arctan z) = z"
  1759 proof -
  1760   have "1 + \<i>*z \<noteq> 0"
  1761     by (metis assms complex_i_mult_minus i_squared minus_unique power2_eq_square power2_minus)
  1762   moreover
  1763   have "1 - \<i>*z \<noteq> 0"
  1764     by (metis assms complex_i_mult_minus i_squared power2_eq_square power2_minus right_minus_eq)
  1765   ultimately
  1766   show ?thesis
  1767     by (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus csqrt_exp_Ln [symmetric]
  1768                   divide_simps power2_eq_square [symmetric])
  1769 qed
  1770 
  1771 lemma Arctan_tan [simp]:
  1772   assumes "\<bar>Re z\<bar> < pi/2"
  1773     shows "Arctan(tan z) = z"
  1774 proof -
  1775   have ge_pi2: "\<And>n::int. abs (of_int (2*n + 1) * pi/2) \<ge> pi/2"
  1776     by (case_tac n rule: int_cases) (auto simp: abs_mult)
  1777   have "exp (\<i>*z)*exp (\<i>*z) = -1 \<longleftrightarrow> exp (2*\<i>*z) = -1"
  1778     by (metis distrib_right exp_add mult_2)
  1779   also have "... \<longleftrightarrow> exp (2*\<i>*z) = exp (\<i>*pi)"
  1780     using cis_conv_exp cis_pi by auto
  1781   also have "... \<longleftrightarrow> exp (2*\<i>*z - \<i>*pi) = 1"
  1782     by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute)
  1783   also have "... \<longleftrightarrow> Re(\<i>*2*z - \<i>*pi) = 0 \<and> (\<exists>n::int. Im(\<i>*2*z - \<i>*pi) = of_int (2 * n) * pi)"
  1784     by (simp add: exp_eq_1)
  1785   also have "... \<longleftrightarrow> Im z = 0 \<and> (\<exists>n::int. 2 * Re z = of_int (2*n + 1) * pi)"
  1786     by (simp add: algebra_simps)
  1787   also have "... \<longleftrightarrow> False"
  1788     using assms ge_pi2
  1789     apply (auto simp: algebra_simps)
  1790     by (metis abs_mult_pos not_less not_real_of_nat_less_zero real_of_nat_numeral)
  1791   finally have *: "exp (\<i>*z)*exp (\<i>*z) + 1 \<noteq> 0"
  1792     by (auto simp: add.commute minus_unique)
  1793   show ?thesis
  1794     using assms *
  1795     apply (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps
  1796                      ii_times_eq_iff power2_eq_square [symmetric])
  1797     apply (rule Ln_unique)
  1798     apply (auto simp: divide_simps exp_minus)
  1799     apply (simp add: algebra_simps exp_double [symmetric])
  1800     done
  1801 qed
  1802 
  1803 lemma
  1804   assumes "Re z = 0 \<Longrightarrow> abs(Im z) < 1"
  1805   shows Re_Arctan_bounds: "abs(Re(Arctan z)) < pi/2"
  1806     and has_field_derivative_Arctan: "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
  1807 proof -
  1808   have nz0: "1 + \<i>*z \<noteq> 0"
  1809     using assms
  1810     by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2)
  1811               less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
  1812   have "z \<noteq> -\<i>" using assms
  1813     by auto
  1814   then have zz: "1 + z * z \<noteq> 0"
  1815     by (metis abs_one assms i_squared ii.simps less_irrefl minus_unique square_eq_iff)
  1816   have nz1: "1 - \<i>*z \<noteq> 0"
  1817     using assms by (force simp add: ii_times_eq_iff)
  1818   have nz2: "inverse (1 + \<i>*z) \<noteq> 0"
  1819     using assms
  1820     by (metis Im_complex_div_lemma Re_complex_div_lemma cmod_eq_Im divide_complex_def
  1821               less_irrefl mult_zero_right zero_complex.simps(1) zero_complex.simps(2))
  1822   have nzi: "((1 - \<i>*z) * inverse (1 + \<i>*z)) \<noteq> 0"
  1823     using nz1 nz2 by auto
  1824   have *: "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))"
  1825     apply (simp add: divide_complex_def)
  1826     apply (simp add: divide_simps split: split_if_asm)
  1827     using assms
  1828     apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square])
  1829     done
  1830   show "abs(Re(Arctan z)) < pi/2"
  1831     unfolding Arctan_def divide_complex_def
  1832     using mpi_less_Im_Ln [OF nzi]
  1833     by (auto simp: abs_if intro: Im_Ln_less_pi * [unfolded divide_complex_def])
  1834   show "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
  1835     unfolding Arctan_def scaleR_conv_of_real
  1836     apply (rule DERIV_cong)
  1837     apply (intro derivative_eq_intros | simp add: nz0 *)+
  1838     using nz0 nz1 zz
  1839     apply (simp add: divide_simps power2_eq_square)
  1840     apply (auto simp: algebra_simps)
  1841     done
  1842 qed
  1843 
  1844 lemma complex_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable at z"
  1845   using has_field_derivative_Arctan
  1846   by (auto simp: complex_differentiable_def)
  1847 
  1848 lemma complex_differentiable_within_Arctan:
  1849     "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable (at z within s)"
  1850   using complex_differentiable_at_Arctan complex_differentiable_at_within by blast
  1851 
  1852 declare has_field_derivative_Arctan [derivative_intros]
  1853 declare has_field_derivative_Arctan [THEN DERIV_chain2, derivative_intros]
  1854 
  1855 lemma continuous_at_Arctan:
  1856     "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z) Arctan"
  1857   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Arctan)
  1858 
  1859 lemma continuous_within_Arctan:
  1860     "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z within s) Arctan"
  1861   using continuous_at_Arctan continuous_at_imp_continuous_within by blast
  1862 
  1863 lemma continuous_on_Arctan [continuous_intros]:
  1864     "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous_on s Arctan"
  1865   by (auto simp: continuous_at_imp_continuous_on continuous_within_Arctan)
  1866 
  1867 lemma holomorphic_on_Arctan:
  1868     "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
  1869   by (simp add: complex_differentiable_within_Arctan holomorphic_on_def)
  1870 
  1871 
  1872 subsection \<open>Real arctangent\<close>
  1873 
  1874 lemma norm_exp_ii_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
  1875   by simp
  1876 
  1877 lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
  1878   by (simp add: complex_norm_eq_1_exp)
  1879 
  1880 lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
  1881   unfolding Arctan_def divide_complex_def
  1882   apply (simp add: complex_eq_iff)
  1883   apply (rule norm_exp_imaginary)
  1884   apply (subst exp_Ln, auto)
  1885   apply (simp_all add: cmod_def complex_eq_iff)
  1886   apply (auto simp: divide_simps)
  1887   apply (metis power_one realpow_two_sum_zero_iff zero_neq_one, algebra)
  1888   done
  1889 
  1890 lemma arctan_eq_Re_Arctan: "arctan x = Re (Arctan (of_real x))"
  1891 proof (rule arctan_unique)
  1892   show "- (pi / 2) < Re (Arctan (complex_of_real x))"
  1893     apply (simp add: Arctan_def)
  1894     apply (rule Im_Ln_less_pi)
  1895     apply (auto simp: Im_complex_div_lemma)
  1896     done
  1897 next
  1898   have *: " (1 - \<i>*x) / (1 + \<i>*x) \<noteq> 0"
  1899     by (simp add: divide_simps) ( simp add: complex_eq_iff)
  1900   show "Re (Arctan (complex_of_real x)) < pi / 2"
  1901     using mpi_less_Im_Ln [OF *]
  1902     by (simp add: Arctan_def)
  1903 next
  1904   have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))"
  1905     apply (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos)
  1906     apply (simp add: field_simps)
  1907     by (simp add: power2_eq_square)
  1908   also have "... = x"
  1909     apply (subst tan_Arctan, auto)
  1910     by (metis diff_0_right minus_diff_eq mult_zero_left not_le of_real_1 of_real_eq_iff of_real_minus of_real_power power2_eq_square real_minus_mult_self_le zero_less_one)
  1911   finally show "tan (Re (Arctan (complex_of_real x))) = x" .
  1912 qed
  1913 
  1914 lemma Arctan_of_real: "Arctan (of_real x) = of_real (arctan x)"
  1915   unfolding arctan_eq_Re_Arctan divide_complex_def
  1916   by (simp add: complex_eq_iff)
  1917 
  1918 lemma Arctan_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Arctan z \<in> \<real>"
  1919   by (metis Reals_cases Reals_of_real Arctan_of_real)
  1920 
  1921 declare arctan_one [simp]
  1922 
  1923 lemma arctan_less_pi4_pos: "x < 1 \<Longrightarrow> arctan x < pi/4"
  1924   by (metis arctan_less_iff arctan_one)
  1925 
  1926 lemma arctan_less_pi4_neg: "-1 < x \<Longrightarrow> -(pi/4) < arctan x"
  1927   by (metis arctan_less_iff arctan_minus arctan_one)
  1928 
  1929 lemma arctan_less_pi4: "abs x < 1 \<Longrightarrow> abs(arctan x) < pi/4"
  1930   by (metis abs_less_iff arctan_less_pi4_pos arctan_minus)
  1931 
  1932 lemma arctan_le_pi4: "abs x \<le> 1 \<Longrightarrow> abs(arctan x) \<le> pi/4"
  1933   by (metis abs_le_iff arctan_le_iff arctan_minus arctan_one)
  1934 
  1935 lemma abs_arctan: "abs(arctan x) = arctan(abs x)"
  1936   by (simp add: abs_if arctan_minus)
  1937 
  1938 lemma arctan_add_raw:
  1939   assumes "abs(arctan x + arctan y) < pi/2"
  1940     shows "arctan x + arctan y = arctan((x + y) / (1 - x * y))"
  1941 proof (rule arctan_unique [symmetric])
  1942   show 12: "- (pi / 2) < arctan x + arctan y" "arctan x + arctan y < pi / 2"
  1943     using assms by linarith+
  1944   show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
  1945     using cos_gt_zero_pi [OF 12]
  1946     by (simp add: arctan tan_add)
  1947 qed
  1948 
  1949 lemma arctan_inverse:
  1950   assumes "0 < x"
  1951     shows "arctan(inverse x) = pi/2 - arctan x"
  1952 proof -
  1953   have "arctan(inverse x) = arctan(inverse(tan(arctan x)))"
  1954     by (simp add: arctan)
  1955   also have "... = arctan (tan (pi / 2 - arctan x))"
  1956     by (simp add: tan_cot)
  1957   also have "... = pi/2 - arctan x"
  1958   proof -
  1959     have "0 < pi - arctan x"
  1960     using arctan_ubound [of x] pi_gt_zero by linarith
  1961     with assms show ?thesis
  1962       by (simp add: Transcendental.arctan_tan)
  1963   qed
  1964   finally show ?thesis .
  1965 qed
  1966 
  1967 lemma arctan_add_small:
  1968   assumes "abs(x * y) < 1"
  1969     shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))"
  1970 proof (cases "x = 0 \<or> y = 0")
  1971   case True then show ?thesis
  1972     by auto
  1973 next
  1974   case False
  1975   then have *: "\<bar>arctan x\<bar> < pi / 2 - \<bar>arctan y\<bar>" using assms
  1976     apply (auto simp add: abs_arctan arctan_inverse [symmetric] arctan_less_iff)
  1977     apply (simp add: divide_simps abs_mult)
  1978     done
  1979   show ?thesis
  1980     apply (rule arctan_add_raw)
  1981     using * by linarith
  1982 qed
  1983 
  1984 lemma abs_arctan_le:
  1985   fixes x::real shows "abs(arctan x) \<le> abs x"
  1986 proof -
  1987   { fix w::complex and z::complex
  1988     assume *: "w \<in> \<real>" "z \<in> \<real>"
  1989     have "cmod (Arctan w - Arctan z) \<le> 1 * cmod (w-z)"
  1990       apply (rule complex_differentiable_bound [OF convex_Reals, of Arctan _ 1])
  1991       apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan])
  1992       apply (force simp add: Reals_def)
  1993       apply (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square)
  1994       using * by auto
  1995   }
  1996   then have "cmod (Arctan (of_real x) - Arctan 0) \<le> 1 * cmod (of_real x -0)"
  1997     using Reals_0 Reals_of_real by blast
  1998   then show ?thesis
  1999     by (simp add: Arctan_of_real)
  2000 qed
  2001 
  2002 lemma arctan_le_self: "0 \<le> x \<Longrightarrow> arctan x \<le> x"
  2003   by (metis abs_arctan_le abs_of_nonneg zero_le_arctan_iff)
  2004 
  2005 lemma abs_tan_ge: "abs x < pi/2 \<Longrightarrow> abs x \<le> abs(tan x)"
  2006   by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
  2007 
  2008 
  2009 subsection\<open>Inverse Sine\<close>
  2010 
  2011 definition Arcsin :: "complex \<Rightarrow> complex" where
  2012    "Arcsin \<equiv> \<lambda>z. -\<i> * Ln(\<i> * z + csqrt(1 - z\<^sup>2))"
  2013 
  2014 lemma Arcsin_body_lemma: "\<i> * z + csqrt(1 - z\<^sup>2) \<noteq> 0"
  2015   using power2_csqrt [of "1 - z\<^sup>2"]
  2016   apply auto
  2017   by (metis complex_i_mult_minus diff_add_cancel diff_minus_eq_add diff_self mult.assoc mult.left_commute numeral_One power2_csqrt power2_eq_square zero_neq_numeral)
  2018 
  2019 lemma Arcsin_range_lemma: "abs (Re z) < 1 \<Longrightarrow> 0 < Re(\<i> * z + csqrt(1 - z\<^sup>2))"
  2020   using Complex.cmod_power2 [of z, symmetric]
  2021   by (simp add: real_less_rsqrt algebra_simps Re_power2 cmod_square_less_1_plus)
  2022 
  2023 lemma Re_Arcsin: "Re(Arcsin z) = Im (Ln (\<i> * z + csqrt(1 - z\<^sup>2)))"
  2024   by (simp add: Arcsin_def)
  2025 
  2026 lemma Im_Arcsin: "Im(Arcsin z) = - ln (cmod (\<i> * z + csqrt (1 - z\<^sup>2)))"
  2027   by (simp add: Arcsin_def Arcsin_body_lemma)
  2028 
  2029 lemma isCont_Arcsin:
  2030   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  2031     shows "isCont Arcsin z"
  2032 proof -
  2033   have rez: "Im (1 - z\<^sup>2) = 0 \<Longrightarrow> 0 < Re (1 - z\<^sup>2)"
  2034     using assms
  2035     by (auto simp: Re_power2 Im_power2 abs_square_less_1 add_pos_nonneg algebra_simps)
  2036   have cmz: "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
  2037     by (blast intro: assms cmod_square_less_1_plus)
  2038   show ?thesis
  2039     using assms
  2040     apply (simp add: Arcsin_def)
  2041     apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
  2042     apply (erule rez)
  2043     apply (auto simp: Re_power2 Im_power2 abs_square_less_1 [symmetric] real_less_rsqrt algebra_simps split: split_if_asm)
  2044     apply (simp add: norm_complex_def)
  2045     using cmod_power2 [of z, symmetric] cmz
  2046     apply (simp add: real_less_rsqrt)
  2047     done
  2048 qed
  2049 
  2050 lemma isCont_Arcsin' [simp]:
  2051   shows "isCont f z \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>x. Arcsin (f x)) z"
  2052   by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
  2053 
  2054 lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
  2055 proof -
  2056   have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
  2057     by (simp add: algebra_simps)  --\<open>Cancelling a factor of 2\<close>
  2058   moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
  2059     by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral)
  2060   ultimately show ?thesis
  2061     apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps)
  2062     apply (simp add: algebra_simps)
  2063     apply (simp add: power2_eq_square [symmetric] algebra_simps)
  2064     done
  2065 qed
  2066 
  2067 lemma Re_eq_pihalf_lemma:
  2068     "\<bar>Re z\<bar> = pi/2 \<Longrightarrow> Im z = 0 \<Longrightarrow>
  2069       Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2) = 0 \<and> 0 \<le> Im ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2)"
  2070   apply (simp add: cos_ii_times [symmetric] Re_cos Im_cos abs_if del: eq_divide_eq_numeral1)
  2071   by (metis cos_minus cos_pi_half)
  2072 
  2073 lemma Re_less_pihalf_lemma:
  2074   assumes "\<bar>Re z\<bar> < pi / 2"
  2075     shows "0 < Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2)"
  2076 proof -
  2077   have "0 < cos (Re z)" using assms
  2078     using cos_gt_zero_pi by auto
  2079   then show ?thesis
  2080     by (simp add: cos_ii_times [symmetric] Re_cos Im_cos add_pos_pos)
  2081 qed
  2082 
  2083 lemma Arcsin_sin:
  2084     assumes "\<bar>Re z\<bar> < pi/2 \<or> (\<bar>Re z\<bar> = pi/2 \<and> Im z = 0)"
  2085       shows "Arcsin(sin z) = z"
  2086 proof -
  2087   have "Arcsin(sin z) = - (\<i> * Ln (csqrt (1 - (\<i> * (exp (\<i>*z) - inverse (exp (\<i>*z))))\<^sup>2 / 4) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
  2088     by (simp add: sin_exp_eq Arcsin_def exp_minus)
  2089   also have "... = - (\<i> * Ln (csqrt (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2)\<^sup>2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
  2090     by (simp add: field_simps power2_eq_square)
  2091   also have "... = - (\<i> * Ln (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
  2092     apply (subst csqrt_square)
  2093     using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma
  2094     apply auto
  2095     done
  2096   also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
  2097     by (simp add: field_simps power2_eq_square)
  2098   also have "... = z"
  2099     apply (subst Complex_Transcendental.Ln_exp)
  2100     using assms
  2101     apply (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: split_if_asm)
  2102     done
  2103   finally show ?thesis .
  2104 qed
  2105 
  2106 lemma Arcsin_unique:
  2107     "\<lbrakk>sin z = w; \<bar>Re z\<bar> < pi/2 \<or> (\<bar>Re z\<bar> = pi/2 \<and> Im z = 0)\<rbrakk> \<Longrightarrow> Arcsin w = z"
  2108   by (metis Arcsin_sin)
  2109 
  2110 lemma Arcsin_0 [simp]: "Arcsin 0 = 0"
  2111   by (metis Arcsin_sin norm_zero pi_half_gt_zero real_norm_def sin_zero zero_complex.simps(1))
  2112 
  2113 lemma Arcsin_1 [simp]: "Arcsin 1 = pi/2"
  2114   by (metis Arcsin_sin Im_complex_of_real Re_complex_of_real numeral_One of_real_numeral pi_half_ge_zero real_sqrt_abs real_sqrt_pow2 real_sqrt_power sin_of_real sin_pi_half)
  2115 
  2116 lemma Arcsin_minus_1 [simp]: "Arcsin(-1) = - (pi/2)"
  2117   by (metis Arcsin_1 Arcsin_sin Im_complex_of_real Re_complex_of_real abs_of_nonneg of_real_minus pi_half_ge_zero power2_minus real_sqrt_abs sin_Arcsin sin_minus)
  2118 
  2119 lemma has_field_derivative_Arcsin:
  2120   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  2121     shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)"
  2122 proof -
  2123   have "(sin (Arcsin z))\<^sup>2 \<noteq> 1"
  2124     using assms
  2125     apply atomize
  2126     apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
  2127     apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
  2128     by (metis abs_minus_cancel abs_one abs_power2 one_neq_neg_one)
  2129   then have "cos (Arcsin z) \<noteq> 0"
  2130     by (metis diff_0_right power_zero_numeral sin_squared_eq)
  2131   then show ?thesis
  2132     apply (rule has_complex_derivative_inverse_basic [OF DERIV_sin])
  2133     apply (auto intro: isCont_Arcsin open_ball [of z 1] assms)
  2134     done
  2135 qed
  2136 
  2137 declare has_field_derivative_Arcsin [derivative_intros]
  2138 declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
  2139 
  2140 lemma complex_differentiable_at_Arcsin:
  2141     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable at z"
  2142   using complex_differentiable_def has_field_derivative_Arcsin by blast
  2143 
  2144 lemma complex_differentiable_within_Arcsin:
  2145     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable (at z within s)"
  2146   using complex_differentiable_at_Arcsin complex_differentiable_within_subset by blast
  2147 
  2148 lemma continuous_within_Arcsin:
  2149     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arcsin"
  2150   using continuous_at_imp_continuous_within isCont_Arcsin by blast
  2151 
  2152 lemma continuous_on_Arcsin [continuous_intros]:
  2153     "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous_on s Arcsin"
  2154   by (simp add: continuous_at_imp_continuous_on)
  2155 
  2156 lemma holomorphic_on_Arcsin: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin holomorphic_on s"
  2157   by (simp add: complex_differentiable_within_Arcsin holomorphic_on_def)
  2158 
  2159 
  2160 subsection\<open>Inverse Cosine\<close>
  2161 
  2162 definition Arccos :: "complex \<Rightarrow> complex" where
  2163    "Arccos \<equiv> \<lambda>z. -\<i> * Ln(z + \<i> * csqrt(1 - z\<^sup>2))"
  2164 
  2165 lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))"
  2166   using Arcsin_range_lemma [of "-z"]
  2167   by simp
  2168 
  2169 lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 0"
  2170   using Arcsin_body_lemma [of z]
  2171   by (metis complex_i_mult_minus diff_add_cancel minus_diff_eq minus_unique mult.assoc mult.left_commute
  2172            power2_csqrt power2_eq_square zero_neq_one)
  2173 
  2174 lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \<i> * csqrt(1 - z\<^sup>2)))"
  2175   by (simp add: Arccos_def)
  2176 
  2177 lemma Im_Arccos: "Im(Arccos z) = - ln (cmod (z + \<i> * csqrt (1 - z\<^sup>2)))"
  2178   by (simp add: Arccos_def Arccos_body_lemma)
  2179 
  2180 text\<open>A very tricky argument to find!\<close>
  2181 lemma abs_Re_less_1_preserve:
  2182   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"  "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0"
  2183     shows "0 < Re (z + \<i> * csqrt (1 - z\<^sup>2))"
  2184 proof (cases "Im z = 0")
  2185   case True
  2186   then show ?thesis
  2187     using assms
  2188     by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric])
  2189 next
  2190   case False
  2191   have Imz: "Im z = - sqrt ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
  2192     using assms abs_Re_le_cmod [of "1-z\<^sup>2"]
  2193     by (simp add: Re_power2 algebra_simps)
  2194   have "(cmod z)\<^sup>2 - 1 \<noteq> cmod (1 - z\<^sup>2)"
  2195   proof (clarsimp simp add: cmod_def)
  2196     assume "(Re z)\<^sup>2 + (Im z)\<^sup>2 - 1 = sqrt ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
  2197     then have "((Re z)\<^sup>2 + (Im z)\<^sup>2 - 1)\<^sup>2 = ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
  2198       by simp
  2199     then show False using False
  2200       by (simp add: power2_eq_square algebra_simps)
  2201   qed
  2202   moreover have "(Im z)\<^sup>2 = ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
  2203     apply (subst Imz, simp)
  2204     apply (subst real_sqrt_pow2)
  2205     using abs_Re_le_cmod [of "1-z\<^sup>2"]
  2206     apply (auto simp: Re_power2 field_simps)
  2207     done
  2208   ultimately show ?thesis
  2209     by (simp add: Re_power2 Im_power2 cmod_power2)
  2210 qed
  2211 
  2212 lemma isCont_Arccos:
  2213   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  2214     shows "isCont Arccos z"
  2215 proof -
  2216   have rez: "Im (1 - z\<^sup>2) = 0 \<Longrightarrow> 0 < Re (1 - z\<^sup>2)"
  2217     using assms
  2218     by (auto simp: Re_power2 Im_power2 abs_square_less_1 add_pos_nonneg algebra_simps)
  2219   show ?thesis
  2220     using assms
  2221     apply (simp add: Arccos_def)
  2222     apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
  2223     apply (erule rez)
  2224     apply (blast intro: abs_Re_less_1_preserve)
  2225     done
  2226 qed
  2227 
  2228 lemma isCont_Arccos' [simp]:
  2229   shows "isCont f z \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>x. Arccos (f x)) z"
  2230   by (blast intro: isCont_o2 [OF _ isCont_Arccos])
  2231 
  2232 lemma cos_Arccos [simp]: "cos(Arccos z) = z"
  2233 proof -
  2234   have "z*2 + \<i> * (2 * csqrt (1 - z\<^sup>2)) = 0 \<longleftrightarrow> z*2 + \<i> * csqrt (1 - z\<^sup>2)*2 = 0"
  2235     by (simp add: algebra_simps)  --\<open>Cancelling a factor of 2\<close>
  2236   moreover have "... \<longleftrightarrow> z + \<i> * csqrt (1 - z\<^sup>2) = 0"
  2237     by (metis distrib_right mult_eq_0_iff zero_neq_numeral)
  2238   ultimately show ?thesis
  2239     apply (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps)
  2240     apply (simp add: power2_eq_square [symmetric])
  2241     done
  2242 qed
  2243 
  2244 lemma Arccos_cos:
  2245     assumes "0 < Re z & Re z < pi \<or>
  2246              Re z = 0 & 0 \<le> Im z \<or>
  2247              Re z = pi & Im z \<le> 0"
  2248       shows "Arccos(cos z) = z"
  2249 proof -
  2250   have *: "((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z))) = sin z"
  2251     by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square)
  2252   have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2"
  2253     by (simp add: field_simps power2_eq_square)
  2254   then have "Arccos(cos z) = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
  2255                            \<i> * csqrt (((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2)))"
  2256     by (simp add: cos_exp_eq Arccos_def exp_minus)
  2257   also have "... = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
  2258                               \<i> * ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))))"
  2259     apply (subst csqrt_square)
  2260     using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z]
  2261     apply (auto simp: * Re_sin Im_sin)
  2262     done
  2263   also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
  2264     by (simp add: field_simps power2_eq_square)
  2265   also have "... = z"
  2266     using assms
  2267     apply (subst Complex_Transcendental.Ln_exp, auto)
  2268     done
  2269   finally show ?thesis .
  2270 qed
  2271 
  2272 lemma Arccos_unique:
  2273     "\<lbrakk>cos z = w;
  2274       0 < Re z \<and> Re z < pi \<or>
  2275       Re z = 0 \<and> 0 \<le> Im z \<or>
  2276       Re z = pi \<and> Im z \<le> 0\<rbrakk> \<Longrightarrow> Arccos w = z"
  2277   using Arccos_cos by blast
  2278 
  2279 lemma Arccos_0 [simp]: "Arccos 0 = pi/2"
  2280   by (rule Arccos_unique) (auto simp: of_real_numeral)
  2281 
  2282 lemma Arccos_1 [simp]: "Arccos 1 = 0"
  2283   by (rule Arccos_unique) auto
  2284 
  2285 lemma Arccos_minus1: "Arccos(-1) = pi"
  2286   by (rule Arccos_unique) auto
  2287 
  2288 lemma has_field_derivative_Arccos:
  2289   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  2290     shows "(Arccos has_field_derivative - inverse(sin(Arccos z))) (at z)"
  2291 proof -
  2292   have "(cos (Arccos z))\<^sup>2 \<noteq> 1"
  2293     using assms
  2294     apply atomize
  2295     apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
  2296     apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
  2297     apply (metis left_minus less_irrefl power_one sum_power2_gt_zero_iff zero_neq_neg_one)
  2298     done
  2299   then have "- sin (Arccos z) \<noteq> 0"
  2300     by (metis cos_squared_eq diff_0_right mult_zero_left neg_0_equal_iff_equal power2_eq_square)
  2301   then have "(Arccos has_field_derivative inverse(- sin(Arccos z))) (at z)"
  2302     apply (rule has_complex_derivative_inverse_basic [OF DERIV_cos])
  2303     apply (auto intro: isCont_Arccos open_ball [of z 1] assms)
  2304     done
  2305   then show ?thesis
  2306     by simp
  2307 qed
  2308 
  2309 declare has_field_derivative_Arcsin [derivative_intros]
  2310 declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
  2311 
  2312 lemma complex_differentiable_at_Arccos:
  2313     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable at z"
  2314   using complex_differentiable_def has_field_derivative_Arccos by blast
  2315 
  2316 lemma complex_differentiable_within_Arccos:
  2317     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable (at z within s)"
  2318   using complex_differentiable_at_Arccos complex_differentiable_within_subset by blast
  2319 
  2320 lemma continuous_within_Arccos:
  2321     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arccos"
  2322   using continuous_at_imp_continuous_within isCont_Arccos by blast
  2323 
  2324 lemma continuous_on_Arccos [continuous_intros]:
  2325     "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous_on s Arccos"
  2326   by (simp add: continuous_at_imp_continuous_on)
  2327 
  2328 lemma holomorphic_on_Arccos: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos holomorphic_on s"
  2329   by (simp add: complex_differentiable_within_Arccos holomorphic_on_def)
  2330 
  2331 
  2332 subsection\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
  2333 
  2334 lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> abs(Re(Arcsin z)) < pi/2"
  2335   unfolding Re_Arcsin
  2336   by (blast intro: Re_Ln_pos_lt_imp Arcsin_range_lemma)
  2337 
  2338 lemma Arccos_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Re(Arccos z) \<and> Re(Arccos z) < pi"
  2339   unfolding Re_Arccos
  2340   by (blast intro!: Im_Ln_pos_lt_imp Arccos_range_lemma)
  2341 
  2342 lemma Re_Arccos_bounds: "-pi < Re(Arccos z) \<and> Re(Arccos z) \<le> pi"
  2343   unfolding Re_Arccos
  2344   by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arccos_body_lemma)
  2345 
  2346 lemma Re_Arccos_bound: "abs(Re(Arccos z)) \<le> pi"
  2347   using Re_Arccos_bounds abs_le_interval_iff less_eq_real_def by blast
  2348 
  2349 lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
  2350   unfolding Re_Arcsin
  2351   by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
  2352 
  2353 lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \<le> pi"
  2354   using Re_Arcsin_bounds abs_le_interval_iff less_eq_real_def by blast
  2355 
  2356 
  2357 subsection\<open>Interrelations between Arcsin and Arccos\<close>
  2358 
  2359 lemma cos_Arcsin_nonzero:
  2360   assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
  2361 proof -
  2362   have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)"
  2363     by (simp add: power_mult_distrib algebra_simps)
  2364   have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> z\<^sup>2 - 1"
  2365   proof
  2366     assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1"
  2367     then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (z\<^sup>2 - 1)\<^sup>2"
  2368       by simp
  2369     then have "z\<^sup>2 * (z\<^sup>2 - 1) = (z\<^sup>2 - 1)*(z\<^sup>2 - 1)"
  2370       using eq power2_eq_square by auto
  2371     then show False
  2372       using assms by simp
  2373   qed
  2374   then have "1 + \<i> * z * (csqrt (1 - z * z)) \<noteq> z\<^sup>2"
  2375     by (metis add_minus_cancel power2_eq_square uminus_add_conv_diff)
  2376   then have "2*(1 + \<i> * z * (csqrt (1 - z * z))) \<noteq> 2*z\<^sup>2"  (*FIXME cancel_numeral_factor*)
  2377     by (metis mult_cancel_left zero_neq_numeral)
  2378   then have "(\<i> * z + csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> -1"
  2379     using assms
  2380     apply (auto simp: power2_sum)
  2381     apply (simp add: power2_eq_square algebra_simps)
  2382     done
  2383   then show ?thesis
  2384     apply (simp add: cos_exp_eq Arcsin_def exp_minus)
  2385     apply (simp add: divide_simps Arcsin_body_lemma)
  2386     apply (metis add.commute minus_unique power2_eq_square)
  2387     done
  2388 qed
  2389 
  2390 lemma sin_Arccos_nonzero:
  2391   assumes "z\<^sup>2 \<noteq> 1" shows "sin(Arccos z) \<noteq> 0"
  2392 proof -
  2393   have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)"
  2394     by (simp add: power_mult_distrib algebra_simps)
  2395   have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1 - z\<^sup>2"
  2396   proof
  2397     assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2"
  2398     then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (1 - z\<^sup>2)\<^sup>2"
  2399       by simp
  2400     then have "-(z\<^sup>2) * (1 - z\<^sup>2) = (1 - z\<^sup>2)*(1 - z\<^sup>2)"
  2401       using eq power2_eq_square by auto
  2402     then have "-(z\<^sup>2) = (1 - z\<^sup>2)"
  2403       using assms
  2404       by (metis add.commute add.right_neutral diff_add_cancel mult_right_cancel)
  2405     then show False
  2406       using assms by simp
  2407   qed
  2408   then have "z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1"
  2409     by (simp add: algebra_simps)
  2410   then have "2*(z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2))) \<noteq> 2*1"
  2411     by (metis mult_cancel_left2 zero_neq_numeral)  (*FIXME cancel_numeral_factor*)
  2412   then have "(z + \<i> * csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> 1"
  2413     using assms
  2414     apply (auto simp: Power.comm_semiring_1_class.power2_sum power_mult_distrib)
  2415     apply (simp add: power2_eq_square algebra_simps)
  2416     done
  2417   then show ?thesis
  2418     apply (simp add: sin_exp_eq Arccos_def exp_minus)
  2419     apply (simp add: divide_simps Arccos_body_lemma)
  2420     apply (simp add: power2_eq_square)
  2421     done
  2422 qed
  2423 
  2424 lemma cos_sin_csqrt:
  2425   assumes "0 < cos(Re z)  \<or>  cos(Re z) = 0 \<and> Im z * sin(Re z) \<le> 0"
  2426     shows "cos z = csqrt(1 - (sin z)\<^sup>2)"
  2427   apply (rule csqrt_unique [THEN sym])
  2428   apply (simp add: cos_squared_eq)
  2429   using assms
  2430   apply (auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff)
  2431   apply (auto simp: algebra_simps)
  2432   done
  2433 
  2434 lemma sin_cos_csqrt:
  2435   assumes "0 < sin(Re z)  \<or>  sin(Re z) = 0 \<and> 0 \<le> Im z * cos(Re z)"
  2436     shows "sin z = csqrt(1 - (cos z)\<^sup>2)"
  2437   apply (rule csqrt_unique [THEN sym])
  2438   apply (simp add: sin_squared_eq)
  2439   using assms
  2440   apply (auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff)
  2441   apply (auto simp: algebra_simps)
  2442   done
  2443 
  2444 lemma Arcsin_Arccos_csqrt_pos:
  2445     "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arcsin z = Arccos(csqrt(1 - z\<^sup>2))"
  2446   by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
  2447 
  2448 lemma Arccos_Arcsin_csqrt_pos:
  2449     "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arccos z = Arcsin(csqrt(1 - z\<^sup>2))"
  2450   by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
  2451 
  2452 lemma sin_Arccos:
  2453     "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> sin(Arccos z) = csqrt(1 - z\<^sup>2)"
  2454   by (simp add: Arccos_Arcsin_csqrt_pos)
  2455 
  2456 lemma cos_Arcsin:
  2457     "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> cos(Arcsin z) = csqrt(1 - z\<^sup>2)"
  2458   by (simp add: Arcsin_Arccos_csqrt_pos)
  2459 
  2460 
  2461 subsection\<open>Relationship with Arcsin on the Real Numbers\<close>
  2462 
  2463 lemma Im_Arcsin_of_real:
  2464   assumes "abs x \<le> 1"
  2465     shows "Im (Arcsin (of_real x)) = 0"
  2466 proof -
  2467   have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
  2468     by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
  2469   then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
  2470     using assms abs_square_le_1
  2471     by (force simp add: Complex.cmod_power2)
  2472   then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2)) = 1"
  2473     by (simp add: norm_complex_def)
  2474   then show ?thesis
  2475     by (simp add: Im_Arcsin exp_minus)
  2476 qed
  2477 
  2478 corollary Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
  2479   by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
  2480 
  2481 lemma arcsin_eq_Re_Arcsin:
  2482   assumes "abs x \<le> 1"
  2483     shows "arcsin x = Re (Arcsin (of_real x))"
  2484 unfolding arcsin_def
  2485 proof (rule the_equality, safe)
  2486   show "- (pi / 2) \<le> Re (Arcsin (complex_of_real x))"
  2487     using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
  2488     by (auto simp: Complex.in_Reals_norm Re_Arcsin)
  2489 next
  2490   show "Re (Arcsin (complex_of_real x)) \<le> pi / 2"
  2491     using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
  2492     by (auto simp: Complex.in_Reals_norm Re_Arcsin)
  2493 next
  2494   show "sin (Re (Arcsin (complex_of_real x))) = x"
  2495     using Re_sin [of "Arcsin (of_real x)"] Arcsin_body_lemma [of "of_real x"]
  2496     by (simp add: Im_Arcsin_of_real assms)
  2497 next
  2498   fix x'
  2499   assume "- (pi / 2) \<le> x'" "x' \<le> pi / 2" "x = sin x'"
  2500   then show "x' = Re (Arcsin (complex_of_real (sin x')))"
  2501     apply (simp add: sin_of_real [symmetric])
  2502     apply (subst Arcsin_sin)
  2503     apply (auto simp: )
  2504     done
  2505 qed
  2506 
  2507 lemma of_real_arcsin: "abs x \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
  2508   by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
  2509 
  2510 
  2511 subsection\<open>Relationship with Arccos on the Real Numbers\<close>
  2512 
  2513 lemma Im_Arccos_of_real:
  2514   assumes "abs x \<le> 1"
  2515     shows "Im (Arccos (of_real x)) = 0"
  2516 proof -
  2517   have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
  2518     by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
  2519   then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
  2520     using assms abs_square_le_1
  2521     by (force simp add: Complex.cmod_power2)
  2522   then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2)) = 1"
  2523     by (simp add: norm_complex_def)
  2524   then show ?thesis
  2525     by (simp add: Im_Arccos exp_minus)
  2526 qed
  2527 
  2528 corollary Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
  2529   by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
  2530 
  2531 lemma arccos_eq_Re_Arccos:
  2532   assumes "abs x \<le> 1"
  2533     shows "arccos x = Re (Arccos (of_real x))"
  2534 unfolding arccos_def
  2535 proof (rule the_equality, safe)
  2536   show "0 \<le> Re (Arccos (complex_of_real x))"
  2537     using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
  2538     by (auto simp: Complex.in_Reals_norm Re_Arccos)
  2539 next
  2540   show "Re (Arccos (complex_of_real x)) \<le> pi"
  2541     using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
  2542     by (auto simp: Complex.in_Reals_norm Re_Arccos)
  2543 next
  2544   show "cos (Re (Arccos (complex_of_real x))) = x"
  2545     using Re_cos [of "Arccos (of_real x)"] Arccos_body_lemma [of "of_real x"]
  2546     by (simp add: Im_Arccos_of_real assms)
  2547 next
  2548   fix x'
  2549   assume "0 \<le> x'" "x' \<le> pi" "x = cos x'"
  2550   then show "x' = Re (Arccos (complex_of_real (cos x')))"
  2551     apply (simp add: cos_of_real [symmetric])
  2552     apply (subst Arccos_cos)
  2553     apply (auto simp: )
  2554     done
  2555 qed
  2556 
  2557 lemma of_real_arccos: "abs x \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
  2558   by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
  2559 
  2560 subsection\<open>Some interrelationships among the real inverse trig functions.\<close>
  2561 
  2562 lemma arccos_arctan:
  2563   assumes "-1 < x" "x < 1"
  2564     shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))"
  2565 proof -
  2566   have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0"
  2567   proof (rule sin_eq_0_pi)
  2568     show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)"
  2569       using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"]  arccos_bounded [of x] assms
  2570       by (simp add: algebra_simps)
  2571   next
  2572     show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi"
  2573       using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"]  arccos_bounded [of x] assms
  2574       by (simp add: algebra_simps)
  2575   next
  2576     show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0"
  2577       using assms
  2578       by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
  2579                     power2_eq_square square_eq_1_iff)
  2580   qed
  2581   then show ?thesis
  2582     by simp
  2583 qed
  2584 
  2585 lemma arcsin_plus_arccos:
  2586   assumes "-1 \<le> x" "x \<le> 1"
  2587     shows "arcsin x + arccos x = pi/2"
  2588 proof -
  2589   have "arcsin x = pi/2 - arccos x"
  2590     apply (rule sin_inj_pi)
  2591     using assms arcsin [OF assms] arccos [OF assms]
  2592     apply (auto simp: algebra_simps sin_diff)
  2593     done
  2594   then show ?thesis
  2595     by (simp add: algebra_simps)
  2596 qed
  2597 
  2598 lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x"
  2599   using arcsin_plus_arccos by force
  2600 
  2601 lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x"
  2602   using arcsin_plus_arccos by force
  2603 
  2604 lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
  2605   by (simp add: arccos_arctan arcsin_arccos_eq)
  2606 
  2607 lemma csqrt_1_diff_eq: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
  2608   by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
  2609 
  2610 lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
  2611   apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
  2612   apply (subst Arcsin_Arccos_csqrt_pos)
  2613   apply (auto simp: power_le_one csqrt_1_diff_eq)
  2614   done
  2615 
  2616 lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
  2617   using arcsin_arccos_sqrt_pos [of "-x"]
  2618   by (simp add: arcsin_minus)
  2619 
  2620 lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
  2621   apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
  2622   apply (subst Arccos_Arcsin_csqrt_pos)
  2623   apply (auto simp: power_le_one csqrt_1_diff_eq)
  2624   done
  2625 
  2626 lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
  2627   using arccos_arcsin_sqrt_pos [of "-x"]
  2628   by (simp add: arccos_minus)
  2629 
  2630 subsection\<open>continuity results for arcsin and arccos.\<close>
  2631 
  2632 lemma continuous_on_Arcsin_real [continuous_intros]:
  2633     "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
  2634 proof -
  2635   have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arcsin (Re x))) =
  2636         continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arcsin (of_real (Re x)))))"
  2637     by (rule continuous_on_cong [OF refl]) (simp add: arcsin_eq_Re_Arcsin)
  2638   also have "... = ?thesis"
  2639     by (rule continuous_on_cong [OF refl]) simp
  2640   finally show ?thesis
  2641     using continuous_on_arcsin [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
  2642           continuous_on_of_real
  2643     by fastforce
  2644 qed
  2645 
  2646 lemma continuous_within_Arcsin_real:
  2647     "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arcsin"
  2648 proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
  2649   case True then show ?thesis
  2650     using continuous_on_Arcsin_real continuous_on_eq_continuous_within
  2651     by blast
  2652 next
  2653   case False
  2654   with closed_real_abs_le [of 1] show ?thesis
  2655     by (rule continuous_within_closed_nontrivial)
  2656 qed
  2657 
  2658 lemma continuous_on_Arccos_real:
  2659     "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arccos"
  2660 proof -
  2661   have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arccos (Re x))) =
  2662         continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arccos (of_real (Re x)))))"
  2663     by (rule continuous_on_cong [OF refl]) (simp add: arccos_eq_Re_Arccos)
  2664   also have "... = ?thesis"
  2665     by (rule continuous_on_cong [OF refl]) simp
  2666   finally show ?thesis
  2667     using continuous_on_arccos [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
  2668           continuous_on_of_real
  2669     by fastforce
  2670 qed
  2671 
  2672 lemma continuous_within_Arccos_real:
  2673     "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arccos"
  2674 proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
  2675   case True then show ?thesis
  2676     using continuous_on_Arccos_real continuous_on_eq_continuous_within
  2677     by blast
  2678 next
  2679   case False
  2680   with closed_real_abs_le [of 1] show ?thesis
  2681     by (rule continuous_within_closed_nontrivial)
  2682 qed
  2683 
  2684 
  2685 subsection\<open>Roots of unity\<close>
  2686 
  2687 lemma complex_root_unity:
  2688   fixes j::nat
  2689   assumes "n \<noteq> 0"
  2690     shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
  2691 proof -
  2692   have *: "of_nat j * (complex_of_real pi * 2) = complex_of_real (2 * real j * pi)"
  2693     by (simp add: of_real_numeral)
  2694   then show ?thesis
  2695     apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler)
  2696     apply (simp only: * cos_of_real sin_of_real)
  2697     apply (simp add: )
  2698     done
  2699 qed
  2700 
  2701 lemma complex_root_unity_eq:
  2702   fixes j::nat and k::nat
  2703   assumes "1 \<le> n"
  2704     shows "(exp(2 * of_real pi * \<i> * of_nat j / of_nat n) = exp(2 * of_real pi * \<i> * of_nat k / of_nat n)
  2705            \<longleftrightarrow> j mod n = k mod n)"
  2706 proof -
  2707     have "(\<exists>z::int. \<i> * (of_nat j * (of_real pi * 2)) =
  2708                \<i> * (of_nat k * (of_real pi * 2)) + \<i> * (of_int z * (of_nat n * (of_real pi * 2)))) \<longleftrightarrow>
  2709           (\<exists>z::int. of_nat j * (\<i> * (of_real pi * 2)) =
  2710               (of_nat k + of_nat n * of_int z) * (\<i> * (of_real pi * 2)))"
  2711       by (simp add: algebra_simps)
  2712     also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))"
  2713       by simp
  2714     also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * z)"
  2715       apply (rule HOL.iff_exI)
  2716       apply (auto simp: )
  2717       using of_int_eq_iff apply fastforce
  2718       by (metis of_int_add of_int_mult of_int_of_nat_eq)
  2719     also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
  2720       by (auto simp: zmod_eq_dvd_iff dvd_def algebra_simps)
  2721     also have "... \<longleftrightarrow> j mod n = k mod n"
  2722       by (metis of_nat_eq_iff zmod_int)
  2723     finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =
  2724              \<i> * (of_nat k * (of_real pi * 2)) + \<i> * (of_int z * (of_nat n * (of_real pi * 2)))) \<longleftrightarrow> j mod n = k mod n" .
  2725    note * = this
  2726   show ?thesis
  2727     using assms
  2728     by (simp add: exp_eq divide_simps mult_ac of_real_numeral *)
  2729 qed
  2730 
  2731 corollary bij_betw_roots_unity:
  2732     "bij_betw (\<lambda>j. exp(2 * of_real pi * \<i> * of_nat j / of_nat n))
  2733               {..<n}  {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j. j < n}"
  2734   by (auto simp: bij_betw_def inj_on_def complex_root_unity_eq)
  2735 
  2736 lemma complex_root_unity_eq_1:
  2737   fixes j::nat and k::nat
  2738   assumes "1 \<le> n"
  2739     shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n) = 1 \<longleftrightarrow> n dvd j"
  2740 proof -
  2741   have "1 = exp(2 * of_real pi * \<i> * (of_nat n / of_nat n))"
  2742     using assms by simp
  2743   then have "exp(2 * of_real pi * \<i> * (of_nat j / of_nat n)) = 1 \<longleftrightarrow> j mod n = n mod n"
  2744      using complex_root_unity_eq [of n j n] assms
  2745      by simp
  2746   then show ?thesis
  2747     by auto
  2748 qed
  2749 
  2750 lemma finite_complex_roots_unity_explicit:
  2751      "finite {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
  2752 by simp
  2753 
  2754 lemma card_complex_roots_unity_explicit:
  2755      "card {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n} = n"
  2756   by (simp add:  Finite_Set.bij_betw_same_card [OF bij_betw_roots_unity, symmetric])
  2757 
  2758 lemma complex_roots_unity:
  2759   assumes "1 \<le> n"
  2760     shows "{z::complex. z^n = 1} = {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
  2761   apply (rule Finite_Set.card_seteq [symmetric])
  2762   using assms
  2763   apply (auto simp: card_complex_roots_unity_explicit finite_roots_unity complex_root_unity card_roots_unity)
  2764   done
  2765 
  2766 lemma card_complex_roots_unity: "1 \<le> n \<Longrightarrow> card {z::complex. z^n = 1} = n"
  2767   by (simp add: card_complex_roots_unity_explicit complex_roots_unity)
  2768 
  2769 lemma complex_not_root_unity:
  2770     "1 \<le> n \<Longrightarrow> \<exists>u::complex. norm u = 1 \<and> u^n \<noteq> 1"
  2771   apply (rule_tac x="exp (of_real pi * \<i> * of_real (1 / n))" in exI)
  2772   apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
  2773   done
  2774 
  2775 end