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