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