src/HOL/Analysis/Complex_Transcendental.thy
changeset 63627 6ddb43c6b711
parent 63594 bd218a9320b5
child 63721 492bb53c3420
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Aug 08 14:13:14 2016 +0200
     1.3 @@ -0,0 +1,3231 @@
     1.4 +section \<open>Complex Transcendental Functions\<close>
     1.5 +
     1.6 +text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>
     1.7 +
     1.8 +theory Complex_Transcendental
     1.9 +imports
    1.10 +  Complex_Analysis_Basics
    1.11 +  Summation_Tests
    1.12 +begin
    1.13 +
    1.14 +(* TODO: Figure out what to do with Möbius transformations *)
    1.15 +definition "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))"
    1.16 +
    1.17 +lemma moebius_inverse:
    1.18 +  assumes "a * d \<noteq> b * c" "c * z + d \<noteq> 0"
    1.19 +  shows   "moebius d (-b) (-c) a (moebius a b c d z) = z"
    1.20 +proof -
    1.21 +  from assms have "(-c) * moebius a b c d z + a \<noteq> 0" unfolding moebius_def
    1.22 +    by (simp add: field_simps)
    1.23 +  with assms show ?thesis
    1.24 +    unfolding moebius_def by (simp add: moebius_def divide_simps) (simp add: algebra_simps)?
    1.25 +qed
    1.26 +
    1.27 +lemma moebius_inverse':
    1.28 +  assumes "a * d \<noteq> b * c" "c * z - a \<noteq> 0"
    1.29 +  shows   "moebius a b c d (moebius d (-b) (-c) a z) = z"
    1.30 +  using assms moebius_inverse[of d a "-b" "-c" z]
    1.31 +  by (auto simp: algebra_simps)
    1.32 +
    1.33 +lemma cmod_add_real_less:
    1.34 +  assumes "Im z \<noteq> 0" "r\<noteq>0"
    1.35 +    shows "cmod (z + r) < cmod z + \<bar>r\<bar>"
    1.36 +proof (cases z)
    1.37 +  case (Complex x y)
    1.38 +  have "r * x / \<bar>r\<bar> < sqrt (x*x + y*y)"
    1.39 +    apply (rule real_less_rsqrt)
    1.40 +    using assms
    1.41 +    apply (simp add: Complex power2_eq_square)
    1.42 +    using not_real_square_gt_zero by blast
    1.43 +  then show ?thesis using assms Complex
    1.44 +    apply (auto simp: cmod_def)
    1.45 +    apply (rule power2_less_imp_less, auto)
    1.46 +    apply (simp add: power2_eq_square field_simps)
    1.47 +    done
    1.48 +qed
    1.49 +
    1.50 +lemma cmod_diff_real_less: "Im z \<noteq> 0 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> cmod (z - x) < cmod z + \<bar>x\<bar>"
    1.51 +  using cmod_add_real_less [of z "-x"]
    1.52 +  by simp
    1.53 +
    1.54 +lemma cmod_square_less_1_plus:
    1.55 +  assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
    1.56 +    shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
    1.57 +  using assms
    1.58 +  apply (cases "Im z = 0 \<or> Re z = 0")
    1.59 +  using abs_square_less_1
    1.60 +    apply (force simp add: Re_power2 Im_power2 cmod_def)
    1.61 +  using cmod_diff_real_less [of "1 - z\<^sup>2" "1"]
    1.62 +  apply (simp add: norm_power Im_power2)
    1.63 +  done
    1.64 +
    1.65 +subsection\<open>The Exponential Function is Differentiable and Continuous\<close>
    1.66 +
    1.67 +lemma field_differentiable_within_exp: "exp field_differentiable (at z within s)"
    1.68 +  using DERIV_exp field_differentiable_at_within field_differentiable_def by blast
    1.69 +
    1.70 +lemma continuous_within_exp:
    1.71 +  fixes z::"'a::{real_normed_field,banach}"
    1.72 +  shows "continuous (at z within s) exp"
    1.73 +by (simp add: continuous_at_imp_continuous_within)
    1.74 +
    1.75 +lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"
    1.76 +  by (simp add: field_differentiable_within_exp holomorphic_on_def)
    1.77 +
    1.78 +subsection\<open>Euler and de Moivre formulas.\<close>
    1.79 +
    1.80 +text\<open>The sine series times @{term i}\<close>
    1.81 +lemma sin_ii_eq: "(\<lambda>n. (\<i> * sin_coeff n) * z^n) sums (\<i> * sin z)"
    1.82 +proof -
    1.83 +  have "(\<lambda>n. \<i> * sin_coeff n *\<^sub>R z^n) sums (\<i> * sin z)"
    1.84 +    using sin_converges sums_mult by blast
    1.85 +  then show ?thesis
    1.86 +    by (simp add: scaleR_conv_of_real field_simps)
    1.87 +qed
    1.88 +
    1.89 +theorem exp_Euler: "exp(\<i> * z) = cos(z) + \<i> * sin(z)"
    1.90 +proof -
    1.91 +  have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n)
    1.92 +        = (\<lambda>n. (\<i> * z) ^ n /\<^sub>R (fact n))"
    1.93 +  proof
    1.94 +    fix n
    1.95 +    show "(cos_coeff n + \<i> * sin_coeff n) * z^n = (\<i> * z) ^ n /\<^sub>R (fact n)"
    1.96 +      by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
    1.97 +  qed
    1.98 +  also have "... sums (exp (\<i> * z))"
    1.99 +    by (rule exp_converges)
   1.100 +  finally have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (exp (\<i> * z))" .
   1.101 +  moreover have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (cos z + \<i> * sin z)"
   1.102 +    using sums_add [OF cos_converges [of z] sin_ii_eq [of z]]
   1.103 +    by (simp add: field_simps scaleR_conv_of_real)
   1.104 +  ultimately show ?thesis
   1.105 +    using sums_unique2 by blast
   1.106 +qed
   1.107 +
   1.108 +corollary exp_minus_Euler: "exp(-(\<i> * z)) = cos(z) - \<i> * sin(z)"
   1.109 +  using exp_Euler [of "-z"]
   1.110 +  by simp
   1.111 +
   1.112 +lemma sin_exp_eq: "sin z = (exp(\<i> * z) - exp(-(\<i> * z))) / (2*\<i>)"
   1.113 +  by (simp add: exp_Euler exp_minus_Euler)
   1.114 +
   1.115 +lemma sin_exp_eq': "sin z = \<i> * (exp(-(\<i> * z)) - exp(\<i> * z)) / 2"
   1.116 +  by (simp add: exp_Euler exp_minus_Euler)
   1.117 +
   1.118 +lemma cos_exp_eq:  "cos z = (exp(\<i> * z) + exp(-(\<i> * z))) / 2"
   1.119 +  by (simp add: exp_Euler exp_minus_Euler)
   1.120 +
   1.121 +subsection\<open>Relationships between real and complex trig functions\<close>
   1.122 +
   1.123 +lemma real_sin_eq [simp]:
   1.124 +  fixes x::real
   1.125 +  shows "Re(sin(of_real x)) = sin x"
   1.126 +  by (simp add: sin_of_real)
   1.127 +
   1.128 +lemma real_cos_eq [simp]:
   1.129 +  fixes x::real
   1.130 +  shows "Re(cos(of_real x)) = cos x"
   1.131 +  by (simp add: cos_of_real)
   1.132 +
   1.133 +lemma DeMoivre: "(cos z + \<i> * sin z) ^ n = cos(n * z) + \<i> * sin(n * z)"
   1.134 +  apply (simp add: exp_Euler [symmetric])
   1.135 +  by (metis exp_of_nat_mult mult.left_commute)
   1.136 +
   1.137 +lemma exp_cnj:
   1.138 +  fixes z::complex
   1.139 +  shows "cnj (exp z) = exp (cnj z)"
   1.140 +proof -
   1.141 +  have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))"
   1.142 +    by auto
   1.143 +  also have "... sums (exp (cnj z))"
   1.144 +    by (rule exp_converges)
   1.145 +  finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
   1.146 +  moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
   1.147 +    by (metis exp_converges sums_cnj)
   1.148 +  ultimately show ?thesis
   1.149 +    using sums_unique2
   1.150 +    by blast
   1.151 +qed
   1.152 +
   1.153 +lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
   1.154 +  by (simp add: sin_exp_eq exp_cnj field_simps)
   1.155 +
   1.156 +lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
   1.157 +  by (simp add: cos_exp_eq exp_cnj field_simps)
   1.158 +
   1.159 +lemma field_differentiable_at_sin: "sin field_differentiable at z"
   1.160 +  using DERIV_sin field_differentiable_def by blast
   1.161 +
   1.162 +lemma field_differentiable_within_sin: "sin field_differentiable (at z within s)"
   1.163 +  by (simp add: field_differentiable_at_sin field_differentiable_at_within)
   1.164 +
   1.165 +lemma field_differentiable_at_cos: "cos field_differentiable at z"
   1.166 +  using DERIV_cos field_differentiable_def by blast
   1.167 +
   1.168 +lemma field_differentiable_within_cos: "cos field_differentiable (at z within s)"
   1.169 +  by (simp add: field_differentiable_at_cos field_differentiable_at_within)
   1.170 +
   1.171 +lemma holomorphic_on_sin: "sin holomorphic_on s"
   1.172 +  by (simp add: field_differentiable_within_sin holomorphic_on_def)
   1.173 +
   1.174 +lemma holomorphic_on_cos: "cos holomorphic_on s"
   1.175 +  by (simp add: field_differentiable_within_cos holomorphic_on_def)
   1.176 +
   1.177 +subsection\<open>Get a nice real/imaginary separation in Euler's formula.\<close>
   1.178 +
   1.179 +lemma Euler: "exp(z) = of_real(exp(Re z)) *
   1.180 +              (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
   1.181 +by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
   1.182 +
   1.183 +lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   1.184 +  by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
   1.185 +
   1.186 +lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
   1.187 +  by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
   1.188 +
   1.189 +lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   1.190 +  by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
   1.191 +
   1.192 +lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
   1.193 +  by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
   1.194 +
   1.195 +lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
   1.196 +  by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
   1.197 +
   1.198 +lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
   1.199 +  by (simp add: Re_sin Im_sin algebra_simps)
   1.200 +
   1.201 +lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
   1.202 +  by (simp add: Re_sin Im_sin algebra_simps)
   1.203 +
   1.204 +subsection\<open>More on the Polar Representation of Complex Numbers\<close>
   1.205 +
   1.206 +lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
   1.207 +  by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
   1.208 +
   1.209 +lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
   1.210 +apply auto
   1.211 +apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
   1.212 +apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1))
   1.213 +by (metis Im_exp Re_exp complex_Re_Im_cancel_iff cos_one_2pi_int sin_double Re_complex_of_real complex_Re_numeral exp_zero mult.assoc mult.left_commute mult_eq_0_iff mult_numeral_1 numeral_One of_real_0 sin_zero_iff_int2)
   1.214 +
   1.215 +lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * \<i>)"
   1.216 +                (is "?lhs = ?rhs")
   1.217 +proof -
   1.218 +  have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
   1.219 +    by (simp add: exp_diff)
   1.220 +  also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
   1.221 +    by (simp add: exp_eq_1)
   1.222 +  also have "... \<longleftrightarrow> ?rhs"
   1.223 +    by (auto simp: algebra_simps intro!: complex_eqI)
   1.224 +  finally show ?thesis .
   1.225 +qed
   1.226 +
   1.227 +lemma exp_complex_eqI: "\<bar>Im w - Im z\<bar> < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
   1.228 +  by (auto simp: exp_eq abs_mult)
   1.229 +
   1.230 +lemma exp_integer_2pi:
   1.231 +  assumes "n \<in> \<int>"
   1.232 +  shows "exp((2 * n * pi) * \<i>) = 1"
   1.233 +proof -
   1.234 +  have "exp((2 * n * pi) * \<i>) = exp 0"
   1.235 +    using assms
   1.236 +    by (simp only: Ints_def exp_eq) auto
   1.237 +  also have "... = 1"
   1.238 +    by simp
   1.239 +  finally show ?thesis .
   1.240 +qed
   1.241 +
   1.242 +lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
   1.243 +proof -
   1.244 +  { assume "sin y = sin x" "cos y = cos x"
   1.245 +    then have "cos (y-x) = 1"
   1.246 +      using cos_add [of y "-x"] by simp
   1.247 +    then have "\<exists>n::int. y-x = n * 2 * pi"
   1.248 +      using cos_one_2pi_int by blast }
   1.249 +  then show ?thesis
   1.250 +  apply (auto simp: sin_add cos_add)
   1.251 +  apply (metis add.commute diff_add_cancel mult.commute)
   1.252 +  done
   1.253 +qed
   1.254 +
   1.255 +lemma exp_i_ne_1:
   1.256 +  assumes "0 < x" "x < 2*pi"
   1.257 +  shows "exp(\<i> * of_real x) \<noteq> 1"
   1.258 +proof
   1.259 +  assume "exp (\<i> * of_real x) = 1"
   1.260 +  then have "exp (\<i> * of_real x) = exp 0"
   1.261 +    by simp
   1.262 +  then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
   1.263 +    by (simp only: Ints_def exp_eq) auto
   1.264 +  then have  "of_real x = (of_int (2 * n) * pi)"
   1.265 +    by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
   1.266 +  then have  "x = (of_int (2 * n) * pi)"
   1.267 +    by simp
   1.268 +  then show False using assms
   1.269 +    by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
   1.270 +qed
   1.271 +
   1.272 +lemma sin_eq_0:
   1.273 +  fixes z::complex
   1.274 +  shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
   1.275 +  by (simp add: sin_exp_eq exp_eq of_real_numeral)
   1.276 +
   1.277 +lemma cos_eq_0:
   1.278 +  fixes z::complex
   1.279 +  shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
   1.280 +  using sin_eq_0 [of "z - of_real pi/2"]
   1.281 +  by (simp add: sin_diff algebra_simps)
   1.282 +
   1.283 +lemma cos_eq_1:
   1.284 +  fixes z::complex
   1.285 +  shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
   1.286 +proof -
   1.287 +  have "cos z = cos (2*(z/2))"
   1.288 +    by simp
   1.289 +  also have "... = 1 - 2 * sin (z/2) ^ 2"
   1.290 +    by (simp only: cos_double_sin)
   1.291 +  finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
   1.292 +    by simp
   1.293 +  show ?thesis
   1.294 +    by (auto simp: sin_eq_0 of_real_numeral)
   1.295 +qed
   1.296 +
   1.297 +lemma csin_eq_1:
   1.298 +  fixes z::complex
   1.299 +  shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)"
   1.300 +  using cos_eq_1 [of "z - of_real pi/2"]
   1.301 +  by (simp add: cos_diff algebra_simps)
   1.302 +
   1.303 +lemma csin_eq_minus1:
   1.304 +  fixes z::complex
   1.305 +  shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)"
   1.306 +        (is "_ = ?rhs")
   1.307 +proof -
   1.308 +  have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
   1.309 +    by (simp add: equation_minus_iff)
   1.310 +  also have "...  \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
   1.311 +    by (simp only: csin_eq_1)
   1.312 +  also have "...  \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
   1.313 +    apply (rule iff_exI)
   1.314 +    by (metis (no_types)  is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff)
   1.315 +  also have "... = ?rhs"
   1.316 +    apply (auto simp: of_real_numeral)
   1.317 +    apply (rule_tac [2] x="-(x+1)" in exI)
   1.318 +    apply (rule_tac x="-(x+1)" in exI)
   1.319 +    apply (simp_all add: algebra_simps)
   1.320 +    done
   1.321 +  finally show ?thesis .
   1.322 +qed
   1.323 +
   1.324 +lemma ccos_eq_minus1:
   1.325 +  fixes z::complex
   1.326 +  shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
   1.327 +  using csin_eq_1 [of "z - of_real pi/2"]
   1.328 +  apply (simp add: sin_diff)
   1.329 +  apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
   1.330 +  done
   1.331 +
   1.332 +lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
   1.333 +                (is "_ = ?rhs")
   1.334 +proof -
   1.335 +  have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
   1.336 +    by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
   1.337 +  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
   1.338 +    by (simp only: csin_eq_1)
   1.339 +  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
   1.340 +    apply (rule iff_exI)
   1.341 +    apply (auto simp: algebra_simps of_real_numeral)
   1.342 +    apply (rule injD [OF inj_of_real [where 'a = complex]])
   1.343 +    apply (auto simp: of_real_numeral)
   1.344 +    done
   1.345 +  also have "... = ?rhs"
   1.346 +    by (auto simp: algebra_simps)
   1.347 +  finally show ?thesis .
   1.348 +qed
   1.349 +
   1.350 +lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
   1.351 +proof -
   1.352 +  have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
   1.353 +    by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
   1.354 +  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
   1.355 +    by (simp only: csin_eq_minus1)
   1.356 +  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
   1.357 +    apply (rule iff_exI)
   1.358 +    apply (auto simp: algebra_simps)
   1.359 +    apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
   1.360 +    done
   1.361 +  also have "... = ?rhs"
   1.362 +    by (auto simp: algebra_simps)
   1.363 +  finally show ?thesis .
   1.364 +qed
   1.365 +
   1.366 +lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
   1.367 +                      (is "_ = ?rhs")
   1.368 +proof -
   1.369 +  have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
   1.370 +    by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
   1.371 +  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
   1.372 +    by (simp only: ccos_eq_minus1)
   1.373 +  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
   1.374 +    apply (rule iff_exI)
   1.375 +    apply (auto simp: algebra_simps)
   1.376 +    apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
   1.377 +    done
   1.378 +  also have "... = ?rhs"
   1.379 +    by (auto simp: algebra_simps)
   1.380 +  finally show ?thesis .
   1.381 +qed
   1.382 +
   1.383 +lemma dist_exp_ii_1: "norm(exp(\<i> * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
   1.384 +  apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
   1.385 +  using cos_double_sin [of "t/2"]
   1.386 +  apply (simp add: real_sqrt_mult)
   1.387 +  done
   1.388 +
   1.389 +lemma sinh_complex:
   1.390 +  fixes z :: complex
   1.391 +  shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
   1.392 +  by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
   1.393 +
   1.394 +lemma sin_ii_times:
   1.395 +  fixes z :: complex
   1.396 +  shows "sin(\<i> * z) = \<i> * ((exp z - inverse (exp z)) / 2)"
   1.397 +  using sinh_complex by auto
   1.398 +
   1.399 +lemma sinh_real:
   1.400 +  fixes x :: real
   1.401 +  shows "of_real((exp x - inverse (exp x)) / 2) = -\<i> * sin(\<i> * of_real x)"
   1.402 +  by (simp add: exp_of_real sin_ii_times of_real_numeral)
   1.403 +
   1.404 +lemma cosh_complex:
   1.405 +  fixes z :: complex
   1.406 +  shows "(exp z + inverse (exp z)) / 2 = cos(\<i> * z)"
   1.407 +  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
   1.408 +
   1.409 +lemma cosh_real:
   1.410 +  fixes x :: real
   1.411 +  shows "of_real((exp x + inverse (exp x)) / 2) = cos(\<i> * of_real x)"
   1.412 +  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
   1.413 +
   1.414 +lemmas cos_ii_times = cosh_complex [symmetric]
   1.415 +
   1.416 +lemma norm_cos_squared:
   1.417 +    "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
   1.418 +  apply (cases z)
   1.419 +  apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
   1.420 +  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
   1.421 +  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   1.422 +  apply (simp add: sin_squared_eq)
   1.423 +  apply (simp add: power2_eq_square algebra_simps divide_simps)
   1.424 +  done
   1.425 +
   1.426 +lemma norm_sin_squared:
   1.427 +    "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
   1.428 +  apply (cases z)
   1.429 +  apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
   1.430 +  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
   1.431 +  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   1.432 +  apply (simp add: cos_squared_eq)
   1.433 +  apply (simp add: power2_eq_square algebra_simps divide_simps)
   1.434 +  done
   1.435 +
   1.436 +lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
   1.437 +  using abs_Im_le_cmod linear order_trans by fastforce
   1.438 +
   1.439 +lemma norm_cos_le:
   1.440 +  fixes z::complex
   1.441 +  shows "norm(cos z) \<le> exp(norm z)"
   1.442 +proof -
   1.443 +  have "Im z \<le> cmod z"
   1.444 +    using abs_Im_le_cmod abs_le_D1 by auto
   1.445 +  with exp_uminus_Im show ?thesis
   1.446 +    apply (simp add: cos_exp_eq norm_divide)
   1.447 +    apply (rule order_trans [OF norm_triangle_ineq], simp)
   1.448 +    apply (metis add_mono exp_le_cancel_iff mult_2_right)
   1.449 +    done
   1.450 +qed
   1.451 +
   1.452 +lemma norm_cos_plus1_le:
   1.453 +  fixes z::complex
   1.454 +  shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
   1.455 +proof -
   1.456 +  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"
   1.457 +      by arith
   1.458 +  have *: "Im z \<le> cmod z"
   1.459 +    using abs_Im_le_cmod abs_le_D1 by auto
   1.460 +  have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)"
   1.461 +    by (simp add: norm_add_rule_thm)
   1.462 +  have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
   1.463 +    by (simp add: cos_exp_eq)
   1.464 +  also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
   1.465 +    by (simp add: field_simps)
   1.466 +  also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
   1.467 +    by (simp add: norm_divide)
   1.468 +  finally show ?thesis
   1.469 +    apply (rule ssubst, simp)
   1.470 +    apply (rule order_trans [OF triangle3], simp)
   1.471 +    using exp_uminus_Im *
   1.472 +    apply (auto intro: mono)
   1.473 +    done
   1.474 +qed
   1.475 +
   1.476 +subsection\<open>Taylor series for complex exponential, sine and cosine.\<close>
   1.477 +
   1.478 +declare power_Suc [simp del]
   1.479 +
   1.480 +lemma Taylor_exp:
   1.481 +  "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   1.482 +proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
   1.483 +  show "convex (closed_segment 0 z)"
   1.484 +    by (rule convex_closed_segment [of 0 z])
   1.485 +next
   1.486 +  fix k x
   1.487 +  assume "x \<in> closed_segment 0 z" "k \<le> n"
   1.488 +  show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
   1.489 +    using DERIV_exp DERIV_subset by blast
   1.490 +next
   1.491 +  fix x
   1.492 +  assume "x \<in> closed_segment 0 z"
   1.493 +  then show "Re x \<le> \<bar>Re z\<bar>"
   1.494 +    apply (auto simp: closed_segment_def scaleR_conv_of_real)
   1.495 +    by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans)
   1.496 +next
   1.497 +  show "0 \<in> closed_segment 0 z"
   1.498 +    by (auto simp: closed_segment_def)
   1.499 +next
   1.500 +  show "z \<in> closed_segment 0 z"
   1.501 +    apply (simp add: closed_segment_def scaleR_conv_of_real)
   1.502 +    using of_real_1 zero_le_one by blast
   1.503 +qed
   1.504 +
   1.505 +lemma
   1.506 +  assumes "0 \<le> u" "u \<le> 1"
   1.507 +  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   1.508 +    and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   1.509 +proof -
   1.510 +  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   1.511 +    by arith
   1.512 +  show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
   1.513 +    apply (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
   1.514 +    apply (rule order_trans [OF norm_triangle_ineq4])
   1.515 +    apply (rule mono)
   1.516 +    apply (auto simp: abs_if mult_left_le_one_le)
   1.517 +    apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
   1.518 +    apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   1.519 +    done
   1.520 +  show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
   1.521 +    apply (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
   1.522 +    apply (rule order_trans [OF norm_triangle_ineq])
   1.523 +    apply (rule mono)
   1.524 +    apply (auto simp: abs_if mult_left_le_one_le)
   1.525 +    apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
   1.526 +    apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   1.527 +    done
   1.528 +qed
   1.529 +
   1.530 +lemma Taylor_sin:
   1.531 +  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
   1.532 +   \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   1.533 +proof -
   1.534 +  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   1.535 +      by arith
   1.536 +  have *: "cmod (sin z -
   1.537 +                 (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
   1.538 +           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   1.539 +  proof (rule complex_taylor [of "closed_segment 0 z" n
   1.540 +                                 "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)"
   1.541 +                                 "exp\<bar>Im z\<bar>" 0 z,  simplified])
   1.542 +    fix k x
   1.543 +    show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
   1.544 +            (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
   1.545 +            (at x within closed_segment 0 z)"
   1.546 +      apply (auto simp: power_Suc)
   1.547 +      apply (intro derivative_eq_intros | simp)+
   1.548 +      done
   1.549 +  next
   1.550 +    fix x
   1.551 +    assume "x \<in> closed_segment 0 z"
   1.552 +    then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
   1.553 +      by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
   1.554 +  qed
   1.555 +  have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
   1.556 +            = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
   1.557 +    by (auto simp: sin_coeff_def elim!: oddE)
   1.558 +  show ?thesis
   1.559 +    apply (rule order_trans [OF _ *])
   1.560 +    apply (simp add: **)
   1.561 +    done
   1.562 +qed
   1.563 +
   1.564 +lemma Taylor_cos:
   1.565 +  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k))
   1.566 +   \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
   1.567 +proof -
   1.568 +  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   1.569 +      by arith
   1.570 +  have *: "cmod (cos z -
   1.571 +                 (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
   1.572 +           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   1.573 +  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,
   1.574 +simplified])
   1.575 +    fix k x
   1.576 +    assume "x \<in> closed_segment 0 z" "k \<le> n"
   1.577 +    show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
   1.578 +            (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
   1.579 +             (at x within closed_segment 0 z)"
   1.580 +      apply (auto simp: power_Suc)
   1.581 +      apply (intro derivative_eq_intros | simp)+
   1.582 +      done
   1.583 +  next
   1.584 +    fix x
   1.585 +    assume "x \<in> closed_segment 0 z"
   1.586 +    then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
   1.587 +      by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
   1.588 +  qed
   1.589 +  have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
   1.590 +            = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
   1.591 +    by (auto simp: cos_coeff_def elim!: evenE)
   1.592 +  show ?thesis
   1.593 +    apply (rule order_trans [OF _ *])
   1.594 +    apply (simp add: **)
   1.595 +    done
   1.596 +qed
   1.597 +
   1.598 +declare power_Suc [simp]
   1.599 +
   1.600 +text\<open>32-bit Approximation to e\<close>
   1.601 +lemma e_approx_32: "\<bar>exp(1) - 5837465777 / 2147483648\<bar> \<le> (inverse(2 ^ 32)::real)"
   1.602 +  using Taylor_exp [of 1 14] exp_le
   1.603 +  apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
   1.604 +  apply (simp only: pos_le_divide_eq [symmetric], linarith)
   1.605 +  done
   1.606 +
   1.607 +lemma e_less_3: "exp 1 < (3::real)"
   1.608 +  using e_approx_32
   1.609 +  by (simp add: abs_if split: if_split_asm)
   1.610 +
   1.611 +lemma ln3_gt_1: "ln 3 > (1::real)"
   1.612 +  by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
   1.613 +
   1.614 +
   1.615 +subsection\<open>The argument of a complex number\<close>
   1.616 +
   1.617 +definition Arg :: "complex \<Rightarrow> real" where
   1.618 + "Arg z \<equiv> if z = 0 then 0
   1.619 +           else THE t. 0 \<le> t \<and> t < 2*pi \<and>
   1.620 +                    z = of_real(norm z) * exp(\<i> * of_real t)"
   1.621 +
   1.622 +lemma Arg_0 [simp]: "Arg(0) = 0"
   1.623 +  by (simp add: Arg_def)
   1.624 +
   1.625 +lemma Arg_unique_lemma:
   1.626 +  assumes z:  "z = of_real(norm z) * exp(\<i> * of_real t)"
   1.627 +      and z': "z = of_real(norm z) * exp(\<i> * of_real t')"
   1.628 +      and t:  "0 \<le> t"  "t < 2*pi"
   1.629 +      and t': "0 \<le> t'" "t' < 2*pi"
   1.630 +      and nz: "z \<noteq> 0"
   1.631 +  shows "t' = t"
   1.632 +proof -
   1.633 +  have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
   1.634 +    by arith
   1.635 +  have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
   1.636 +    by (metis z z')
   1.637 +  then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
   1.638 +    by (metis nz mult_left_cancel mult_zero_left z)
   1.639 +  then have "sin t' = sin t \<and> cos t' = cos t"
   1.640 +    apply (simp add: exp_Euler sin_of_real cos_of_real)
   1.641 +    by (metis Complex_eq complex.sel)
   1.642 +  then obtain n::int where n: "t' = t + 2 * n * pi"
   1.643 +    by (auto simp: sin_cos_eq_iff)
   1.644 +  then have "n=0"
   1.645 +    apply (rule_tac z=n in int_cases)
   1.646 +    using t t'
   1.647 +    apply (auto simp: mult_less_0_iff algebra_simps)
   1.648 +    done
   1.649 +  then show "t' = t"
   1.650 +      by (simp add: n)
   1.651 +qed
   1.652 +
   1.653 +lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
   1.654 +proof (cases "z=0")
   1.655 +  case True then show ?thesis
   1.656 +    by (simp add: Arg_def)
   1.657 +next
   1.658 +  case False
   1.659 +  obtain t where t: "0 \<le> t" "t < 2*pi"
   1.660 +             and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
   1.661 +    using sincos_total_2pi [OF complex_unit_circle [OF False]]
   1.662 +    by blast
   1.663 +  have z: "z = of_real(norm z) * exp(\<i> * of_real t)"
   1.664 +    apply (rule complex_eqI)
   1.665 +    using t False ReIm
   1.666 +    apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
   1.667 +    done
   1.668 +  show ?thesis
   1.669 +    apply (simp add: Arg_def False)
   1.670 +    apply (rule theI [where a=t])
   1.671 +    using t z False
   1.672 +    apply (auto intro: Arg_unique_lemma)
   1.673 +    done
   1.674 +qed
   1.675 +
   1.676 +corollary
   1.677 +  shows Arg_ge_0: "0 \<le> Arg z"
   1.678 +    and Arg_lt_2pi: "Arg z < 2*pi"
   1.679 +    and Arg_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
   1.680 +  using Arg by auto
   1.681 +
   1.682 +lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(\<i> * of_real t))"
   1.683 +  using Arg [of z] by auto
   1.684 +
   1.685 +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"
   1.686 +  apply (rule Arg_unique_lemma [OF _ Arg_eq])
   1.687 +  using Arg [of z]
   1.688 +  apply (auto simp: norm_mult)
   1.689 +  done
   1.690 +
   1.691 +lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
   1.692 +  apply (rule Arg_unique [of "norm z"])
   1.693 +  apply (rule complex_eqI)
   1.694 +  using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] Arg_eq [of z]
   1.695 +  apply auto
   1.696 +  apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
   1.697 +  apply (metis Re_rcis Im_rcis rcis_def)+
   1.698 +  done
   1.699 +
   1.700 +lemma Arg_times_of_real [simp]: "0 < r \<Longrightarrow> Arg (of_real r * z) = Arg z"
   1.701 +  apply (cases "z=0", simp)
   1.702 +  apply (rule Arg_unique [of "r * norm z"])
   1.703 +  using Arg
   1.704 +  apply auto
   1.705 +  done
   1.706 +
   1.707 +lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
   1.708 +  by (metis Arg_times_of_real mult.commute)
   1.709 +
   1.710 +lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
   1.711 +  by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
   1.712 +
   1.713 +lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
   1.714 +proof (cases "z=0")
   1.715 +  case True then show ?thesis
   1.716 +    by simp
   1.717 +next
   1.718 +  case False
   1.719 +  have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   1.720 +    by (metis Arg_eq)
   1.721 +  also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
   1.722 +    using False
   1.723 +    by (simp add: zero_le_mult_iff)
   1.724 +  also have "... \<longleftrightarrow> Arg z \<le> pi"
   1.725 +    by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
   1.726 +  finally show ?thesis
   1.727 +    by blast
   1.728 +qed
   1.729 +
   1.730 +lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
   1.731 +proof (cases "z=0")
   1.732 +  case True then show ?thesis
   1.733 +    by simp
   1.734 +next
   1.735 +  case False
   1.736 +  have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   1.737 +    by (metis Arg_eq)
   1.738 +  also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
   1.739 +    using False
   1.740 +    by (simp add: zero_less_mult_iff)
   1.741 +  also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
   1.742 +    using Arg_ge_0  Arg_lt_2pi sin_le_zero sin_gt_zero
   1.743 +    apply (auto simp: Im_exp)
   1.744 +    using le_less apply fastforce
   1.745 +    using not_le by blast
   1.746 +  finally show ?thesis
   1.747 +    by blast
   1.748 +qed
   1.749 +
   1.750 +lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
   1.751 +proof (cases "z=0")
   1.752 +  case True then show ?thesis
   1.753 +    by simp
   1.754 +next
   1.755 +  case False
   1.756 +  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)))"
   1.757 +    by (metis Arg_eq)
   1.758 +  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
   1.759 +    using False
   1.760 +    by (simp add: zero_le_mult_iff)
   1.761 +  also have "... \<longleftrightarrow> Arg z = 0"
   1.762 +    apply (auto simp: Re_exp)
   1.763 +    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)
   1.764 +    using Arg_eq [of z]
   1.765 +    apply (auto simp: Reals_def)
   1.766 +    done
   1.767 +  finally show ?thesis
   1.768 +    by blast
   1.769 +qed
   1.770 +
   1.771 +corollary Arg_gt_0:
   1.772 +  assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
   1.773 +    shows "Arg z > 0"
   1.774 +  using Arg_eq_0 Arg_ge_0 assms dual_order.strict_iff_order by fastforce
   1.775 +
   1.776 +lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
   1.777 +  by (simp add: Arg_eq_0)
   1.778 +
   1.779 +lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
   1.780 +  apply  (cases "z=0", simp)
   1.781 +  using Arg_eq_0 [of "-z"]
   1.782 +  apply (auto simp: complex_is_Real_iff Arg_minus)
   1.783 +  apply (simp add: complex_Re_Im_cancel_iff)
   1.784 +  apply (metis Arg_minus pi_gt_zero add.left_neutral minus_minus minus_zero)
   1.785 +  done
   1.786 +
   1.787 +lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
   1.788 +  using Arg_eq_0 Arg_eq_pi not_le by auto
   1.789 +
   1.790 +lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   1.791 +  apply (cases "z=0", simp)
   1.792 +  apply (rule Arg_unique [of "inverse (norm z)"])
   1.793 +  using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] exp_two_pi_i
   1.794 +  apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
   1.795 +  done
   1.796 +
   1.797 +lemma Arg_eq_iff:
   1.798 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   1.799 +     shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
   1.800 +  using assms Arg_eq [of z] Arg_eq [of w]
   1.801 +  apply auto
   1.802 +  apply (rule_tac x="norm w / norm z" in exI)
   1.803 +  apply (simp add: divide_simps)
   1.804 +  by (metis mult.commute mult.left_commute)
   1.805 +
   1.806 +lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
   1.807 +  using complex_is_Real_iff
   1.808 +  apply (simp add: Arg_eq_0)
   1.809 +  apply (auto simp: divide_simps not_sum_power2_lt_zero)
   1.810 +  done
   1.811 +
   1.812 +lemma Arg_divide:
   1.813 +  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
   1.814 +    shows "Arg(z / w) = Arg z - Arg w"
   1.815 +  apply (rule Arg_unique [of "norm(z / w)"])
   1.816 +  using assms Arg_eq [of z] Arg_eq [of w] Arg_ge_0 [of w] Arg_lt_2pi [of z]
   1.817 +  apply (auto simp: exp_diff norm_divide algebra_simps divide_simps)
   1.818 +  done
   1.819 +
   1.820 +lemma Arg_le_div_sum:
   1.821 +  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
   1.822 +    shows "Arg z = Arg w + Arg(z / w)"
   1.823 +  by (simp add: Arg_divide assms)
   1.824 +
   1.825 +lemma Arg_le_div_sum_eq:
   1.826 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   1.827 +    shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
   1.828 +  using assms
   1.829 +  by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
   1.830 +
   1.831 +lemma Arg_diff:
   1.832 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   1.833 +    shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
   1.834 +  using assms
   1.835 +  apply (auto simp: Arg_ge_0 Arg_divide not_le)
   1.836 +  using Arg_divide [of w z] Arg_inverse [of "w/z"]
   1.837 +  apply auto
   1.838 +  by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
   1.839 +
   1.840 +lemma Arg_add:
   1.841 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   1.842 +    shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
   1.843 +  using assms
   1.844 +  using Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
   1.845 +  apply (auto simp: Arg_ge_0 Arg_divide not_le)
   1.846 +  apply (metis Arg_lt_2pi add.commute)
   1.847 +  apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
   1.848 +  done
   1.849 +
   1.850 +lemma Arg_times:
   1.851 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   1.852 +    shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
   1.853 +                            else (Arg w + Arg z) - 2*pi)"
   1.854 +  using Arg_add [OF assms]
   1.855 +  by auto
   1.856 +
   1.857 +lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   1.858 +  apply (cases "z=0", simp)
   1.859 +  apply (rule trans [of _ "Arg(inverse z)"])
   1.860 +  apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
   1.861 +  apply (metis norm_eq_zero of_real_power zero_less_power2)
   1.862 +  apply (auto simp: of_real_numeral Arg_inverse)
   1.863 +  done
   1.864 +
   1.865 +lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
   1.866 +  using Arg_eq_0 Arg_eq_0_pi
   1.867 +  by auto
   1.868 +
   1.869 +lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
   1.870 +  by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: exp_eq_polar)
   1.871 +
   1.872 +lemma complex_split_polar:
   1.873 +  obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
   1.874 +  using Arg cis.ctr cis_conv_exp by fastforce
   1.875 +
   1.876 +lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
   1.877 +proof (cases w rule: complex_split_polar)
   1.878 +  case (1 r a) with sin_cos_le1 [of a \<phi>] show ?thesis
   1.879 +    apply (simp add: norm_mult cmod_unit_one)
   1.880 +    by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
   1.881 +qed
   1.882 +
   1.883 +subsection\<open>Analytic properties of tangent function\<close>
   1.884 +
   1.885 +lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
   1.886 +  by (simp add: cnj_cos cnj_sin tan_def)
   1.887 +
   1.888 +lemma field_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan field_differentiable at z"
   1.889 +  unfolding field_differentiable_def
   1.890 +  using DERIV_tan by blast
   1.891 +
   1.892 +lemma field_differentiable_within_tan: "~(cos z = 0)
   1.893 +         \<Longrightarrow> tan field_differentiable (at z within s)"
   1.894 +  using field_differentiable_at_tan field_differentiable_at_within by blast
   1.895 +
   1.896 +lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
   1.897 +  using continuous_at_imp_continuous_within isCont_tan by blast
   1.898 +
   1.899 +lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan"
   1.900 +  by (simp add: continuous_at_imp_continuous_on)
   1.901 +
   1.902 +lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
   1.903 +  by (simp add: field_differentiable_within_tan holomorphic_on_def)
   1.904 +
   1.905 +
   1.906 +subsection\<open>Complex logarithms (the conventional principal value)\<close>
   1.907 +
   1.908 +instantiation complex :: ln
   1.909 +begin
   1.910 +
   1.911 +definition ln_complex :: "complex \<Rightarrow> complex"
   1.912 +  where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
   1.913 +
   1.914 +lemma
   1.915 +  assumes "z \<noteq> 0"
   1.916 +    shows exp_Ln [simp]:  "exp(ln z) = z"
   1.917 +      and mpi_less_Im_Ln: "-pi < Im(ln z)"
   1.918 +      and Im_Ln_le_pi:    "Im(ln z) \<le> pi"
   1.919 +proof -
   1.920 +  obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
   1.921 +    using complex_unimodular_polar [of "z / (norm z)"] assms
   1.922 +    by (auto simp: norm_divide divide_simps)
   1.923 +  obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
   1.924 +    using sincos_principal_value [of "\<psi>"] assms
   1.925 +    by (auto simp: norm_divide divide_simps)
   1.926 +  have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \<le> pi" unfolding ln_complex_def
   1.927 +    apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
   1.928 +    using z assms \<phi>
   1.929 +    apply (auto simp: field_simps exp_complex_eqI exp_eq_polar cis.code)
   1.930 +    done
   1.931 +  then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \<le> pi"
   1.932 +    by auto
   1.933 +qed
   1.934 +
   1.935 +lemma Ln_exp [simp]:
   1.936 +  assumes "-pi < Im(z)" "Im(z) \<le> pi"
   1.937 +    shows "ln(exp z) = z"
   1.938 +  apply (rule exp_complex_eqI)
   1.939 +  using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
   1.940 +  apply auto
   1.941 +  done
   1.942 +
   1.943 +subsection\<open>Relation to Real Logarithm\<close>
   1.944 +
   1.945 +lemma Ln_of_real:
   1.946 +  assumes "0 < z"
   1.947 +    shows "ln(of_real z::complex) = of_real(ln z)"
   1.948 +proof -
   1.949 +  have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"
   1.950 +    by (simp add: exp_of_real)
   1.951 +  also have "... = of_real(ln z)"
   1.952 +    using assms
   1.953 +    by (subst Ln_exp) auto
   1.954 +  finally show ?thesis
   1.955 +    using assms by simp
   1.956 +qed
   1.957 +
   1.958 +corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
   1.959 +  by (auto simp: Ln_of_real elim: Reals_cases)
   1.960 +
   1.961 +corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
   1.962 +  by (simp add: Ln_of_real)
   1.963 +
   1.964 +lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
   1.965 +  using Ln_of_real by force
   1.966 +
   1.967 +lemma Ln_1: "ln 1 = (0::complex)"
   1.968 +proof -
   1.969 +  have "ln (exp 0) = (0::complex)"
   1.970 +    by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one)
   1.971 +  then show ?thesis
   1.972 +    by simp
   1.973 +qed
   1.974 +
   1.975 +instance
   1.976 +  by intro_classes (rule ln_complex_def Ln_1)
   1.977 +
   1.978 +end
   1.979 +
   1.980 +abbreviation Ln :: "complex \<Rightarrow> complex"
   1.981 +  where "Ln \<equiv> ln"
   1.982 +
   1.983 +lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
   1.984 +  by (metis exp_Ln)
   1.985 +
   1.986 +lemma Ln_unique: "exp(z) = w \<Longrightarrow> -pi < Im(z) \<Longrightarrow> Im(z) \<le> pi \<Longrightarrow> Ln w = z"
   1.987 +  using Ln_exp by blast
   1.988 +
   1.989 +lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
   1.990 +  by (metis exp_Ln ln_exp norm_exp_eq_Re)
   1.991 +
   1.992 +corollary ln_cmod_le:
   1.993 +  assumes z: "z \<noteq> 0"
   1.994 +    shows "ln (cmod z) \<le> cmod (Ln z)"
   1.995 +  using norm_exp [of "Ln z", simplified exp_Ln [OF z]]
   1.996 +  by (metis Re_Ln complex_Re_le_cmod z)
   1.997 +
   1.998 +proposition exists_complex_root:
   1.999 +  fixes z :: complex
  1.1000 +  assumes "n \<noteq> 0"  obtains w where "z = w ^ n"
  1.1001 +  apply (cases "z=0")
  1.1002 +  using assms apply (simp add: power_0_left)
  1.1003 +  apply (rule_tac w = "exp(Ln z / n)" in that)
  1.1004 +  apply (auto simp: assms exp_of_nat_mult [symmetric])
  1.1005 +  done
  1.1006 +
  1.1007 +corollary exists_complex_root_nonzero:
  1.1008 +  fixes z::complex
  1.1009 +  assumes "z \<noteq> 0" "n \<noteq> 0"
  1.1010 +  obtains w where "w \<noteq> 0" "z = w ^ n"
  1.1011 +  by (metis exists_complex_root [of n z] assms power_0_left)
  1.1012 +
  1.1013 +subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
  1.1014 +
  1.1015 +text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
  1.1016 +
  1.1017 +definition unwinding :: "complex \<Rightarrow> complex" where
  1.1018 +   "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
  1.1019 +
  1.1020 +lemma unwinding_2pi: "(2*pi) * \<i> * unwinding(z) = z - Ln(exp z)"
  1.1021 +  by (simp add: unwinding_def)
  1.1022 +
  1.1023 +lemma Ln_times_unwinding:
  1.1024 +    "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \<i> * unwinding(Ln w + Ln z)"
  1.1025 +  using unwinding_2pi by (simp add: exp_add)
  1.1026 +
  1.1027 +
  1.1028 +subsection\<open>Derivative of Ln away from the branch cut\<close>
  1.1029 +
  1.1030 +lemma
  1.1031 +  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
  1.1032 +    shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
  1.1033 +      and Im_Ln_less_pi:           "Im (Ln z) < pi"
  1.1034 +proof -
  1.1035 +  have znz: "z \<noteq> 0"
  1.1036 +    using assms by auto
  1.1037 +  then have "Im (Ln z) \<noteq> pi"
  1.1038 +    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)
  1.1039 +  then show *: "Im (Ln z) < pi" using assms Im_Ln_le_pi
  1.1040 +    by (simp add: le_neq_trans znz)
  1.1041 +  have "(exp has_field_derivative z) (at (Ln z))"
  1.1042 +    by (metis znz DERIV_exp exp_Ln)
  1.1043 +  then show "(Ln has_field_derivative inverse(z)) (at z)"
  1.1044 +    apply (rule has_complex_derivative_inverse_strong_x
  1.1045 +              [where s = "{w. -pi < Im(w) \<and> Im(w) < pi}"])
  1.1046 +    using znz *
  1.1047 +    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)
  1.1048 +    done
  1.1049 +qed
  1.1050 +
  1.1051 +declare has_field_derivative_Ln [derivative_intros]
  1.1052 +declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
  1.1053 +
  1.1054 +lemma field_differentiable_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln field_differentiable at z"
  1.1055 +  using field_differentiable_def has_field_derivative_Ln by blast
  1.1056 +
  1.1057 +lemma field_differentiable_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0
  1.1058 +         \<Longrightarrow> Ln field_differentiable (at z within s)"
  1.1059 +  using field_differentiable_at_Ln field_differentiable_within_subset by blast
  1.1060 +
  1.1061 +lemma continuous_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) Ln"
  1.1062 +  by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Ln)
  1.1063 +
  1.1064 +lemma isCont_Ln' [simp]:
  1.1065 +   "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
  1.1066 +  by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
  1.1067 +
  1.1068 +lemma continuous_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within s) Ln"
  1.1069 +  using continuous_at_Ln continuous_at_imp_continuous_within by blast
  1.1070 +
  1.1071 +lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s Ln"
  1.1072 +  by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
  1.1073 +
  1.1074 +lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
  1.1075 +  by (simp add: field_differentiable_within_Ln holomorphic_on_def)
  1.1076 +
  1.1077 +
  1.1078 +subsection\<open>Quadrant-type results for Ln\<close>
  1.1079 +
  1.1080 +lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
  1.1081 +  using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
  1.1082 +  by simp
  1.1083 +
  1.1084 +lemma Re_Ln_pos_lt:
  1.1085 +  assumes "z \<noteq> 0"
  1.1086 +    shows "\<bar>Im(Ln z)\<bar> < pi/2 \<longleftrightarrow> 0 < Re(z)"
  1.1087 +proof -
  1.1088 +  { fix w
  1.1089 +    assume "w = Ln z"
  1.1090 +    then have w: "Im w \<le> pi" "- pi < Im w"
  1.1091 +      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1.1092 +      by auto
  1.1093 +    then have "\<bar>Im w\<bar> < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
  1.1094 +      apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
  1.1095 +      using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
  1.1096 +      apply (simp add: abs_if split: if_split_asm)
  1.1097 +      apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4)
  1.1098 +               less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right
  1.1099 +               mult_numeral_1_right)
  1.1100 +      done
  1.1101 +  }
  1.1102 +  then show ?thesis using assms
  1.1103 +    by auto
  1.1104 +qed
  1.1105 +
  1.1106 +lemma Re_Ln_pos_le:
  1.1107 +  assumes "z \<noteq> 0"
  1.1108 +    shows "\<bar>Im(Ln z)\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
  1.1109 +proof -
  1.1110 +  { fix w
  1.1111 +    assume "w = Ln z"
  1.1112 +    then have w: "Im w \<le> pi" "- pi < Im w"
  1.1113 +      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1.1114 +      by auto
  1.1115 +    then have "\<bar>Im w\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
  1.1116 +      apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
  1.1117 +      using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
  1.1118 +      apply (auto simp: abs_if split: if_split_asm)
  1.1119 +      done
  1.1120 +  }
  1.1121 +  then show ?thesis using assms
  1.1122 +    by auto
  1.1123 +qed
  1.1124 +
  1.1125 +lemma Im_Ln_pos_lt:
  1.1126 +  assumes "z \<noteq> 0"
  1.1127 +    shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
  1.1128 +proof -
  1.1129 +  { fix w
  1.1130 +    assume "w = Ln z"
  1.1131 +    then have w: "Im w \<le> pi" "- pi < Im w"
  1.1132 +      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1.1133 +      by auto
  1.1134 +    then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)"
  1.1135 +      using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"]
  1.1136 +      apply (auto simp: Im_exp zero_less_mult_iff)
  1.1137 +      using less_linear apply fastforce
  1.1138 +      using less_linear apply fastforce
  1.1139 +      done
  1.1140 +  }
  1.1141 +  then show ?thesis using assms
  1.1142 +    by auto
  1.1143 +qed
  1.1144 +
  1.1145 +lemma Im_Ln_pos_le:
  1.1146 +  assumes "z \<noteq> 0"
  1.1147 +    shows "0 \<le> Im(Ln z) \<and> Im(Ln z) \<le> pi \<longleftrightarrow> 0 \<le> Im(z)"
  1.1148 +proof -
  1.1149 +  { fix w
  1.1150 +    assume "w = Ln z"
  1.1151 +    then have w: "Im w \<le> pi" "- pi < Im w"
  1.1152 +      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1.1153 +      by auto
  1.1154 +    then have "0 \<le> Im w \<and> Im w \<le> pi \<longleftrightarrow> 0 \<le> Im(exp w)"
  1.1155 +      using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"]
  1.1156 +      apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero)
  1.1157 +      apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi)
  1.1158 +      done }
  1.1159 +  then show ?thesis using assms
  1.1160 +    by auto
  1.1161 +qed
  1.1162 +
  1.1163 +lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> \<bar>Im(Ln z)\<bar> < pi/2"
  1.1164 +  by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
  1.1165 +
  1.1166 +lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
  1.1167 +  by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))
  1.1168 +
  1.1169 +text\<open>A reference to the set of positive real numbers\<close>
  1.1170 +lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
  1.1171 +by (metis Im_complex_of_real Im_exp Ln_in_Reals Re_Ln_pos_lt Re_Ln_pos_lt_imp
  1.1172 +          Re_complex_of_real complex_is_Real_iff exp_Ln exp_of_real pi_gt_zero)
  1.1173 +
  1.1174 +lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
  1.1175 +by (metis Im_Ln_eq_0 Im_Ln_pos_le Im_Ln_pos_lt add.left_neutral complex_eq less_eq_real_def
  1.1176 +    mult_zero_right not_less_iff_gr_or_eq pi_ge_zero pi_neq_zero rcis_zero_arg rcis_zero_mod)
  1.1177 +
  1.1178 +
  1.1179 +subsection\<open>More Properties of Ln\<close>
  1.1180 +
  1.1181 +lemma cnj_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
  1.1182 +  apply (cases "z=0", auto)
  1.1183 +  apply (rule exp_complex_eqI)
  1.1184 +  apply (auto simp: abs_if split: if_split_asm)
  1.1185 +  using Im_Ln_less_pi Im_Ln_le_pi apply force
  1.1186 +  apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff
  1.1187 +          mpi_less_Im_Ln mult.commute mult_2_right)
  1.1188 +  by (metis exp_Ln exp_cnj)
  1.1189 +
  1.1190 +lemma Ln_inverse: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln(inverse z) = -(Ln z)"
  1.1191 +  apply (cases "z=0", auto)
  1.1192 +  apply (rule exp_complex_eqI)
  1.1193 +  using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
  1.1194 +  apply (auto simp: abs_if exp_minus split: if_split_asm)
  1.1195 +  apply (metis Im_Ln_less_pi Im_Ln_le_pi add.commute add_mono_thms_linordered_field(3) inverse_nonzero_iff_nonzero mult_2)
  1.1196 +  done
  1.1197 +
  1.1198 +lemma Ln_minus1 [simp]: "Ln(-1) = \<i> * pi"
  1.1199 +  apply (rule exp_complex_eqI)
  1.1200 +  using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
  1.1201 +  apply (auto simp: abs_if)
  1.1202 +  done
  1.1203 +
  1.1204 +lemma Ln_ii [simp]: "Ln \<i> = \<i> * of_real pi/2"
  1.1205 +  using Ln_exp [of "\<i> * (of_real pi/2)"]
  1.1206 +  unfolding exp_Euler
  1.1207 +  by simp
  1.1208 +
  1.1209 +lemma Ln_minus_ii [simp]: "Ln(-\<i>) = - (\<i> * pi/2)"
  1.1210 +proof -
  1.1211 +  have  "Ln(-\<i>) = Ln(inverse \<i>)"    by simp
  1.1212 +  also have "... = - (Ln \<i>)"         using Ln_inverse by blast
  1.1213 +  also have "... = - (\<i> * pi/2)"     by simp
  1.1214 +  finally show ?thesis .
  1.1215 +qed
  1.1216 +
  1.1217 +lemma Ln_times:
  1.1218 +  assumes "w \<noteq> 0" "z \<noteq> 0"
  1.1219 +    shows "Ln(w * z) =
  1.1220 +                (if Im(Ln w + Ln z) \<le> -pi then
  1.1221 +                  (Ln(w) + Ln(z)) + \<i> * of_real(2*pi)
  1.1222 +                else if Im(Ln w + Ln z) > pi then
  1.1223 +                  (Ln(w) + Ln(z)) - \<i> * of_real(2*pi)
  1.1224 +                else Ln(w) + Ln(z))"
  1.1225 +  using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
  1.1226 +  using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
  1.1227 +  by (auto simp: exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
  1.1228 +
  1.1229 +corollary Ln_times_simple:
  1.1230 +    "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
  1.1231 +         \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
  1.1232 +  by (simp add: Ln_times)
  1.1233 +
  1.1234 +corollary Ln_times_of_real:
  1.1235 +    "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(of_real r * z) = ln r + Ln(z)"
  1.1236 +  using mpi_less_Im_Ln Im_Ln_le_pi
  1.1237 +  by (force simp: Ln_times)
  1.1238 +
  1.1239 +corollary Ln_divide_of_real:
  1.1240 +    "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
  1.1241 +using Ln_times_of_real [of "inverse r" z]
  1.1242 +by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric]
  1.1243 +         del: of_real_inverse)
  1.1244 +
  1.1245 +lemma Ln_minus:
  1.1246 +  assumes "z \<noteq> 0"
  1.1247 +    shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
  1.1248 +                     then Ln(z) + \<i> * pi
  1.1249 +                     else Ln(z) - \<i> * pi)" (is "_ = ?rhs")
  1.1250 +  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
  1.1251 +        Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
  1.1252 +    by (fastforce simp: exp_add exp_diff exp_Euler intro!: Ln_unique)
  1.1253 +
  1.1254 +lemma Ln_inverse_if:
  1.1255 +  assumes "z \<noteq> 0"
  1.1256 +    shows "Ln (inverse z) = (if z \<in> \<real>\<^sub>\<le>\<^sub>0 then -(Ln z) + \<i> * 2 * complex_of_real pi else -(Ln z))"
  1.1257 +proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
  1.1258 +  case False then show ?thesis
  1.1259 +    by (simp add: Ln_inverse)
  1.1260 +next
  1.1261 +  case True
  1.1262 +  then have z: "Im z = 0" "Re z < 0"
  1.1263 +    using assms
  1.1264 +    apply (auto simp: complex_nonpos_Reals_iff)
  1.1265 +    by (metis complex_is_Real_iff le_imp_less_or_eq of_real_0 of_real_Re)
  1.1266 +  have "Ln(inverse z) = Ln(- (inverse (-z)))"
  1.1267 +    by simp
  1.1268 +  also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
  1.1269 +    using assms z
  1.1270 +    apply (simp add: Ln_minus)
  1.1271 +    apply (simp add: field_simps)
  1.1272 +    done
  1.1273 +  also have "... = - Ln (- z) + \<i> * complex_of_real pi"
  1.1274 +    apply (subst Ln_inverse)
  1.1275 +    using z by (auto simp add: complex_nonneg_Reals_iff)
  1.1276 +  also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
  1.1277 +    apply (subst Ln_minus [OF assms])
  1.1278 +    using assms z
  1.1279 +    apply simp
  1.1280 +    done
  1.1281 +  finally show ?thesis by (simp add: True)
  1.1282 +qed
  1.1283 +
  1.1284 +lemma Ln_times_ii:
  1.1285 +  assumes "z \<noteq> 0"
  1.1286 +    shows  "Ln(\<i> * z) = (if 0 \<le> Re(z) | Im(z) < 0
  1.1287 +                          then Ln(z) + \<i> * of_real pi/2
  1.1288 +                          else Ln(z) - \<i> * of_real(3 * pi/2))"
  1.1289 +  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
  1.1290 +        Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
  1.1291 +  by (auto simp: Ln_times)
  1.1292 +
  1.1293 +lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
  1.1294 +  by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
  1.1295 +
  1.1296 +lemma Ln_of_nat_over_of_nat:
  1.1297 +  assumes "m > 0" "n > 0"
  1.1298 +  shows   "Ln (of_nat m / of_nat n) = of_real (ln (of_nat m) - ln (of_nat n))"
  1.1299 +proof -
  1.1300 +  have "of_nat m / of_nat n = (of_real (of_nat m / of_nat n) :: complex)" by simp
  1.1301 +  also from assms have "Ln ... = of_real (ln (of_nat m / of_nat n))"
  1.1302 +    by (simp add: Ln_of_real[symmetric])
  1.1303 +  also from assms have "... = of_real (ln (of_nat m) - ln (of_nat n))"
  1.1304 +    by (simp add: ln_div)
  1.1305 +  finally show ?thesis .
  1.1306 +qed
  1.1307 +
  1.1308 +
  1.1309 +subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
  1.1310 +
  1.1311 +lemma Arg_Ln:
  1.1312 +  assumes "0 < Arg z" shows "Arg z = Im(Ln(-z)) + pi"
  1.1313 +proof (cases "z = 0")
  1.1314 +  case True
  1.1315 +  with assms show ?thesis
  1.1316 +    by simp
  1.1317 +next
  1.1318 +  case False
  1.1319 +  then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
  1.1320 +    using Arg [of z]
  1.1321 +    by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff)
  1.1322 +  then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
  1.1323 +    using cis_conv_exp cis_pi
  1.1324 +    by (auto simp: exp_diff algebra_simps)
  1.1325 +  then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg z) - pi)))"
  1.1326 +    by simp
  1.1327 +  also have "... = \<i> * (of_real(Arg z) - pi)"
  1.1328 +    using Arg [of z] assms pi_not_less_zero
  1.1329 +    by auto
  1.1330 +  finally have "Arg z =  Im (Ln (- z / of_real (cmod z))) + pi"
  1.1331 +    by simp
  1.1332 +  also have "... = Im (Ln (-z) - ln (cmod z)) + pi"
  1.1333 +    by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)
  1.1334 +  also have "... = Im (Ln (-z)) + pi"
  1.1335 +    by simp
  1.1336 +  finally show ?thesis .
  1.1337 +qed
  1.1338 +
  1.1339 +lemma continuous_at_Arg:
  1.1340 +  assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
  1.1341 +    shows "continuous (at z) Arg"
  1.1342 +proof -
  1.1343 +  have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
  1.1344 +    by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
  1.1345 +  have [simp]: "\<And>x. \<lbrakk>Im x \<noteq> 0\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg x"
  1.1346 +      using Arg_Ln Arg_gt_0 complex_is_Real_iff by auto
  1.1347 +  consider "Re z < 0" | "Im z \<noteq> 0" using assms
  1.1348 +    using complex_nonneg_Reals_iff not_le by blast
  1.1349 +  then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg z"
  1.1350 +      using "*"  by (simp add: isCont_def) (metis Arg_Ln Arg_gt_0 complex_is_Real_iff)
  1.1351 +  show ?thesis
  1.1352 +      apply (simp add: continuous_at)
  1.1353 +      apply (rule Lim_transform_within_open [where s= "-\<real>\<^sub>\<ge>\<^sub>0" and f = "\<lambda>z. Im(Ln(-z)) + pi"])
  1.1354 +      apply (auto simp add: not_le Arg_Ln [OF Arg_gt_0] complex_nonneg_Reals_iff closed_def [symmetric])
  1.1355 +      using assms apply (force simp add: complex_nonneg_Reals_iff)
  1.1356 +      done
  1.1357 +qed
  1.1358 +
  1.1359 +lemma Ln_series:
  1.1360 +  fixes z :: complex
  1.1361 +  assumes "norm z < 1"
  1.1362 +  shows   "(\<lambda>n. (-1)^Suc n / of_nat n * z^n) sums ln (1 + z)" (is "(\<lambda>n. ?f n * z^n) sums _")
  1.1363 +proof -
  1.1364 +  let ?F = "\<lambda>z. \<Sum>n. ?f n * z^n" and ?F' = "\<lambda>z. \<Sum>n. diffs ?f n * z^n"
  1.1365 +  have r: "conv_radius ?f = 1"
  1.1366 +    by (intro conv_radius_ratio_limit_nonzero[of _ 1])
  1.1367 +       (simp_all add: norm_divide LIMSEQ_Suc_n_over_n del: of_nat_Suc)
  1.1368 +
  1.1369 +  have "\<exists>c. \<forall>z\<in>ball 0 1. ln (1 + z) - ?F z = c"
  1.1370 +  proof (rule has_field_derivative_zero_constant)
  1.1371 +    fix z :: complex assume z': "z \<in> ball 0 1"
  1.1372 +    hence z: "norm z < 1" by (simp add: dist_0_norm)
  1.1373 +    define t :: complex where "t = of_real (1 + norm z) / 2"
  1.1374 +    from z have t: "norm z < norm t" "norm t < 1" unfolding t_def
  1.1375 +      by (simp_all add: field_simps norm_divide del: of_real_add)
  1.1376 +
  1.1377 +    have "Re (-z) \<le> norm (-z)" by (rule complex_Re_le_cmod)
  1.1378 +    also from z have "... < 1" by simp
  1.1379 +    finally have "((\<lambda>z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)"
  1.1380 +      by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
  1.1381 +    moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
  1.1382 +      by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all
  1.1383 +    ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))
  1.1384 +                       (at z within ball 0 1)"
  1.1385 +      by (intro derivative_intros) (simp_all add: at_within_open[OF z'])
  1.1386 +    also have "(\<lambda>n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r
  1.1387 +      by (intro diffs_equiv termdiff_converges[OF t(1)] summable_in_conv_radius) simp_all
  1.1388 +    from sums_split_initial_segment[OF this, of 1]
  1.1389 +      have "(\<lambda>i. (-z) ^ i) sums ?F' z" by (simp add: power_minus[of z] del: of_nat_Suc)
  1.1390 +    hence "?F' z = inverse (1 + z)" using z by (simp add: sums_iff suminf_geometric divide_inverse)
  1.1391 +    also have "inverse (1 + z) - inverse (1 + z) = 0" by simp
  1.1392 +    finally show "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative 0) (at z within ball 0 1)" .
  1.1393 +  qed simp_all
  1.1394 +  then obtain c where c: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> ln (1 + z) - ?F z = c" by blast
  1.1395 +  from c[of 0] have "c = 0" by (simp only: powser_zero) simp
  1.1396 +  with c[of z] assms have "ln (1 + z) = ?F z" by (simp add: dist_0_norm)
  1.1397 +  moreover have "summable (\<lambda>n. ?f n * z^n)" using assms r
  1.1398 +    by (intro summable_in_conv_radius) simp_all
  1.1399 +  ultimately show ?thesis by (simp add: sums_iff)
  1.1400 +qed
  1.1401 +
  1.1402 +lemma Ln_approx_linear:
  1.1403 +  fixes z :: complex
  1.1404 +  assumes "norm z < 1"
  1.1405 +  shows   "norm (ln (1 + z) - z) \<le> norm z^2 / (1 - norm z)"
  1.1406 +proof -
  1.1407 +  let ?f = "\<lambda>n. (-1)^Suc n / of_nat n"
  1.1408 +  from assms have "(\<lambda>n. ?f n * z^n) sums ln (1 + z)" using Ln_series by simp
  1.1409 +  moreover have "(\<lambda>n. (if n = 1 then 1 else 0) * z^n) sums z" using powser_sums_if[of 1] by simp
  1.1410 +  ultimately have "(\<lambda>n. (?f n - (if n = 1 then 1 else 0)) * z^n) sums (ln (1 + z) - z)"
  1.1411 +    by (subst left_diff_distrib, intro sums_diff) simp_all
  1.1412 +  from sums_split_initial_segment[OF this, of "Suc 1"]
  1.1413 +    have "(\<lambda>i. (-(z^2)) * inverse (2 + of_nat i) * (- z)^i) sums (Ln (1 + z) - z)"
  1.1414 +    by (simp add: power2_eq_square mult_ac power_minus[of z] divide_inverse)
  1.1415 +  hence "(Ln (1 + z) - z) = (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)"
  1.1416 +    by (simp add: sums_iff)
  1.1417 +  also have A: "summable (\<lambda>n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"
  1.1418 +    by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])
  1.1419 +       (auto simp: assms field_simps intro!: always_eventually)
  1.1420 +  hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le>
  1.1421 +             (\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"
  1.1422 +    by (intro summable_norm)
  1.1423 +       (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)
  1.1424 +  also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \<le> norm ((-z)^2 * (-z)^i) * 1" for i
  1.1425 +    by (intro mult_left_mono) (simp_all add: divide_simps)
  1.1426 +  hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i)) \<le>
  1.1427 +           (\<Sum>i. norm (-(z^2) * (-z)^i))" using A assms
  1.1428 +    apply (simp_all only: norm_power norm_inverse norm_divide norm_mult)
  1.1429 +    apply (intro suminf_le summable_mult summable_geometric)
  1.1430 +    apply (auto simp: norm_power field_simps simp del: of_nat_add of_nat_Suc)
  1.1431 +    done
  1.1432 +  also have "... = norm z^2 * (\<Sum>i. norm z^i)" using assms
  1.1433 +    by (subst suminf_mult [symmetric]) (auto intro!: summable_geometric simp: norm_mult norm_power)
  1.1434 +  also have "(\<Sum>i. norm z^i) = inverse (1 - norm z)" using assms
  1.1435 +    by (subst suminf_geometric) (simp_all add: divide_inverse)
  1.1436 +  also have "norm z^2 * ... = norm z^2 / (1 - norm z)" by (simp add: divide_inverse)
  1.1437 +  finally show ?thesis .
  1.1438 +qed
  1.1439 +
  1.1440 +
  1.1441 +text\<open>Relation between Arg and arctangent in upper halfplane\<close>
  1.1442 +lemma Arg_arctan_upperhalf:
  1.1443 +  assumes "0 < Im z"
  1.1444 +    shows "Arg z = pi/2 - arctan(Re z / Im z)"
  1.1445 +proof (cases "z = 0")
  1.1446 +  case True with assms show ?thesis
  1.1447 +    by simp
  1.1448 +next
  1.1449 +  case False
  1.1450 +  show ?thesis
  1.1451 +    apply (rule Arg_unique [of "norm z"])
  1.1452 +    using False assms arctan [of "Re z / Im z"] pi_ge_two pi_half_less_two
  1.1453 +    apply (auto simp: exp_Euler cos_diff sin_diff)
  1.1454 +    using norm_complex_def [of z, symmetric]
  1.1455 +    apply (simp add: sin_of_real cos_of_real sin_arctan cos_arctan field_simps real_sqrt_divide)
  1.1456 +    apply (metis complex_eq mult.assoc ring_class.ring_distribs(2))
  1.1457 +    done
  1.1458 +qed
  1.1459 +
  1.1460 +lemma Arg_eq_Im_Ln:
  1.1461 +  assumes "0 \<le> Im z" "0 < Re z"
  1.1462 +    shows "Arg z = Im (Ln z)"
  1.1463 +proof (cases "z = 0 \<or> Im z = 0")
  1.1464 +  case True then show ?thesis
  1.1465 +    using assms Arg_eq_0 complex_is_Real_iff
  1.1466 +    apply auto
  1.1467 +    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))
  1.1468 +next
  1.1469 +  case False
  1.1470 +  then have "Arg z > 0"
  1.1471 +    using Arg_gt_0 complex_is_Real_iff by blast
  1.1472 +  then show ?thesis
  1.1473 +    using assms False
  1.1474 +    by (subst Arg_Ln) (auto simp: Ln_minus)
  1.1475 +qed
  1.1476 +
  1.1477 +lemma continuous_within_upperhalf_Arg:
  1.1478 +  assumes "z \<noteq> 0"
  1.1479 +    shows "continuous (at z within {z. 0 \<le> Im z}) Arg"
  1.1480 +proof (cases "z \<in> \<real>\<^sub>\<ge>\<^sub>0")
  1.1481 +  case False then show ?thesis
  1.1482 +    using continuous_at_Arg continuous_at_imp_continuous_within by auto
  1.1483 +next
  1.1484 +  case True
  1.1485 +  then have z: "z \<in> \<real>" "0 < Re z"
  1.1486 +    using assms  by (auto simp: complex_nonneg_Reals_iff complex_is_Real_iff complex_neq_0)
  1.1487 +  then have [simp]: "Arg z = 0" "Im (Ln z) = 0"
  1.1488 +    by (auto simp: Arg_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
  1.1489 +  show ?thesis
  1.1490 +  proof (clarsimp simp add: continuous_within Lim_within dist_norm)
  1.1491 +    fix e::real
  1.1492 +    assume "0 < e"
  1.1493 +    moreover have "continuous (at z) (\<lambda>x. Im (Ln x))"
  1.1494 +      using z by (simp add: continuous_at_Ln complex_nonpos_Reals_iff)
  1.1495 +    ultimately
  1.1496 +    obtain d where d: "d>0" "\<And>x. x \<noteq> z \<Longrightarrow> cmod (x - z) < d \<Longrightarrow> \<bar>Im (Ln x)\<bar> < e"
  1.1497 +      by (auto simp: continuous_within Lim_within dist_norm)
  1.1498 +    { fix x
  1.1499 +      assume "cmod (x - z) < Re z / 2"
  1.1500 +      then have "\<bar>Re x - Re z\<bar> < Re z / 2"
  1.1501 +        by (metis le_less_trans abs_Re_le_cmod minus_complex.simps(1))
  1.1502 +      then have "0 < Re x"
  1.1503 +        using z by linarith
  1.1504 +    }
  1.1505 +    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"
  1.1506 +      apply (rule_tac x="min d (Re z / 2)" in exI)
  1.1507 +      using z d
  1.1508 +      apply (auto simp: Arg_eq_Im_Ln)
  1.1509 +      done
  1.1510 +  qed
  1.1511 +qed
  1.1512 +
  1.1513 +lemma continuous_on_upperhalf_Arg: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg"
  1.1514 +  apply (auto simp: continuous_on_eq_continuous_within)
  1.1515 +  by (metis Diff_subset continuous_within_subset continuous_within_upperhalf_Arg)
  1.1516 +
  1.1517 +lemma open_Arg_less_Int:
  1.1518 +  assumes "0 \<le> s" "t \<le> 2*pi"
  1.1519 +    shows "open ({y. s < Arg y} \<inter> {y. Arg y < t})"
  1.1520 +proof -
  1.1521 +  have 1: "continuous_on (UNIV - \<real>\<^sub>\<ge>\<^sub>0) Arg"
  1.1522 +    using continuous_at_Arg continuous_at_imp_continuous_within
  1.1523 +    by (auto simp: continuous_on_eq_continuous_within)
  1.1524 +  have 2: "open (UNIV - \<real>\<^sub>\<ge>\<^sub>0 :: complex set)"  by (simp add: open_Diff)
  1.1525 +  have "open ({z. s < z} \<inter> {z. z < t})"
  1.1526 +    using open_lessThan [of t] open_greaterThan [of s]
  1.1527 +    by (metis greaterThan_def lessThan_def open_Int)
  1.1528 +  moreover have "{y. s < Arg y} \<inter> {y. Arg y < t} \<subseteq> - \<real>\<^sub>\<ge>\<^sub>0"
  1.1529 +    using assms by (auto simp: Arg_real complex_nonneg_Reals_iff complex_is_Real_iff)
  1.1530 +  ultimately show ?thesis
  1.1531 +    using continuous_imp_open_vimage [OF 1 2, of  "{z. Re z > s} \<inter> {z. Re z < t}"]
  1.1532 +    by auto
  1.1533 +qed
  1.1534 +
  1.1535 +lemma open_Arg_gt: "open {z. t < Arg z}"
  1.1536 +proof (cases "t < 0")
  1.1537 +  case True then have "{z. t < Arg z} = UNIV"
  1.1538 +    using Arg_ge_0 less_le_trans by auto
  1.1539 +  then show ?thesis
  1.1540 +    by simp
  1.1541 +next
  1.1542 +  case False then show ?thesis
  1.1543 +    using open_Arg_less_Int [of t "2*pi"] Arg_lt_2pi
  1.1544 +    by auto
  1.1545 +qed
  1.1546 +
  1.1547 +lemma closed_Arg_le: "closed {z. Arg z \<le> t}"
  1.1548 +  using open_Arg_gt [of t]
  1.1549 +  by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)
  1.1550 +
  1.1551 +subsection\<open>Complex Powers\<close>
  1.1552 +
  1.1553 +lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
  1.1554 +  by (simp add: powr_def)
  1.1555 +
  1.1556 +lemma powr_nat:
  1.1557 +  fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
  1.1558 +  by (simp add: exp_of_nat_mult powr_def)
  1.1559 +
  1.1560 +lemma powr_add_complex:
  1.1561 +  fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
  1.1562 +  by (simp add: powr_def algebra_simps exp_add)
  1.1563 +
  1.1564 +lemma powr_minus_complex:
  1.1565 +  fixes w::complex shows  "w powr (-z) = inverse(w powr z)"
  1.1566 +  by (simp add: powr_def exp_minus)
  1.1567 +
  1.1568 +lemma powr_diff_complex:
  1.1569 +  fixes w::complex shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
  1.1570 +  by (simp add: powr_def algebra_simps exp_diff)
  1.1571 +
  1.1572 +lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
  1.1573 +  apply (simp add: powr_def)
  1.1574 +  using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
  1.1575 +  by auto
  1.1576 +
  1.1577 +lemma cnj_powr:
  1.1578 +  assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"
  1.1579 +  shows   "cnj (a powr b) = cnj a powr cnj b"
  1.1580 +proof (cases "a = 0")
  1.1581 +  case False
  1.1582 +  with assms have "a \<notin> \<real>\<^sub>\<le>\<^sub>0" by (auto simp: complex_eq_iff complex_nonpos_Reals_iff)
  1.1583 +  with False show ?thesis by (simp add: powr_def exp_cnj cnj_Ln)
  1.1584 +qed simp
  1.1585 +
  1.1586 +lemma powr_real_real:
  1.1587 +    "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
  1.1588 +  apply (simp add: powr_def)
  1.1589 +  by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
  1.1590 +       exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
  1.1591 +
  1.1592 +lemma powr_of_real:
  1.1593 +  fixes x::real and y::real
  1.1594 +  shows "0 \<le> x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
  1.1595 +  by (simp_all add: powr_def exp_eq_polar)
  1.1596 +
  1.1597 +lemma norm_powr_real_mono:
  1.1598 +    "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
  1.1599 +     \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
  1.1600 +  by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
  1.1601 +
  1.1602 +lemma powr_times_real:
  1.1603 +    "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
  1.1604 +           \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
  1.1605 +  by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
  1.1606 +
  1.1607 +lemma powr_neg_real_complex:
  1.1608 +  shows   "(- of_real x) powr a = (-1) powr (of_real (sgn x) * a) * of_real x powr (a :: complex)"
  1.1609 +proof (cases "x = 0")
  1.1610 +  assume x: "x \<noteq> 0"
  1.1611 +  hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)
  1.1612 +  also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \<i>"
  1.1613 +    by (simp add: Ln_minus Ln_of_real)
  1.1614 +  also from x have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
  1.1615 +    by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)
  1.1616 +  also note cis_pi
  1.1617 +  finally show ?thesis by simp
  1.1618 +qed simp_all
  1.1619 +
  1.1620 +lemma has_field_derivative_powr:
  1.1621 +  fixes z :: complex
  1.1622 +  shows "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
  1.1623 +  apply (cases "z=0", auto)
  1.1624 +  apply (simp add: powr_def)
  1.1625 +  apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
  1.1626 +  apply (auto simp: dist_complex_def)
  1.1627 +  apply (intro derivative_eq_intros | simp)+
  1.1628 +  apply (simp add: field_simps exp_diff)
  1.1629 +  done
  1.1630 +
  1.1631 +declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
  1.1632 +
  1.1633 +
  1.1634 +lemma has_field_derivative_powr_right:
  1.1635 +    "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
  1.1636 +  apply (simp add: powr_def)
  1.1637 +  apply (intro derivative_eq_intros | simp)+
  1.1638 +  done
  1.1639 +
  1.1640 +lemma field_differentiable_powr_right:
  1.1641 +  fixes w::complex
  1.1642 +  shows
  1.1643 +    "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
  1.1644 +using field_differentiable_def has_field_derivative_powr_right by blast
  1.1645 +
  1.1646 +lemma holomorphic_on_powr_right:
  1.1647 +    "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
  1.1648 +    unfolding holomorphic_on_def field_differentiable_def
  1.1649 +by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
  1.1650 +
  1.1651 +lemma norm_powr_real_powr:
  1.1652 +  "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
  1.1653 +  by (cases "w = 0") (auto simp add: norm_powr_real powr_def Im_Ln_eq_0
  1.1654 +                                     complex_is_Real_iff in_Reals_norm complex_eq_iff)
  1.1655 +
  1.1656 +lemma tendsto_ln_complex [tendsto_intros]:
  1.1657 +  assumes "(f \<longlongrightarrow> a) F" "a \<notin> \<real>\<^sub>\<le>\<^sub>0"
  1.1658 +  shows   "((\<lambda>z. ln (f z :: complex)) \<longlongrightarrow> ln a) F"
  1.1659 +  using tendsto_compose[OF continuous_at_Ln[of a, unfolded isCont_def] assms(1)] assms(2) by simp
  1.1660 +
  1.1661 +lemma tendsto_powr_complex:
  1.1662 +  fixes f g :: "_ \<Rightarrow> complex"
  1.1663 +  assumes a: "a \<notin> \<real>\<^sub>\<le>\<^sub>0"
  1.1664 +  assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F"
  1.1665 +  shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
  1.1666 +proof -
  1.1667 +  from a have [simp]: "a \<noteq> 0" by auto
  1.1668 +  from f g a have "((\<lambda>z. exp (g z * ln (f z))) \<longlongrightarrow> a powr b) F" (is ?P)
  1.1669 +    by (auto intro!: tendsto_intros simp: powr_def)
  1.1670 +  also {
  1.1671 +    have "eventually (\<lambda>z. z \<noteq> 0) (nhds a)"
  1.1672 +      by (intro t1_space_nhds) simp_all
  1.1673 +    with f have "eventually (\<lambda>z. f z \<noteq> 0) F" using filterlim_iff by blast
  1.1674 +  }
  1.1675 +  hence "?P \<longleftrightarrow> ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
  1.1676 +    by (intro tendsto_cong refl) (simp_all add: powr_def mult_ac)
  1.1677 +  finally show ?thesis .
  1.1678 +qed
  1.1679 +
  1.1680 +lemma tendsto_powr_complex_0:
  1.1681 +  fixes f g :: "'a \<Rightarrow> complex"
  1.1682 +  assumes f: "(f \<longlongrightarrow> 0) F" and g: "(g \<longlongrightarrow> b) F" and b: "Re b > 0"
  1.1683 +  shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> 0) F"
  1.1684 +proof (rule tendsto_norm_zero_cancel)
  1.1685 +  define h where
  1.1686 +    "h = (\<lambda>z. if f z = 0 then 0 else exp (Re (g z) * ln (cmod (f z)) + abs (Im (g z)) * pi))"
  1.1687 +  {
  1.1688 +    fix z :: 'a assume z: "f z \<noteq> 0"
  1.1689 +    define c where "c = abs (Im (g z)) * pi"
  1.1690 +    from mpi_less_Im_Ln[OF z] Im_Ln_le_pi[OF z]
  1.1691 +      have "abs (Im (Ln (f z))) \<le> pi" by simp
  1.1692 +    from mult_left_mono[OF this, of "abs (Im (g z))"]
  1.1693 +      have "abs (Im (g z) * Im (ln (f z))) \<le> c" by (simp add: abs_mult c_def)
  1.1694 +    hence "-Im (g z) * Im (ln (f z)) \<le> c" by simp
  1.1695 +    hence "norm (f z powr g z) \<le> h z" by (simp add: powr_def field_simps h_def c_def)
  1.1696 +  }
  1.1697 +  hence le: "norm (f z powr g z) \<le> h z" for z by (cases "f x = 0") (simp_all add: h_def)
  1.1698 +
  1.1699 +  have g': "(g \<longlongrightarrow> b) (inf F (principal {z. f z \<noteq> 0}))"
  1.1700 +    by (rule tendsto_mono[OF _ g]) simp_all
  1.1701 +  have "((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) (inf F (principal {z. f z \<noteq> 0}))"
  1.1702 +    by (subst tendsto_norm_zero_iff, rule tendsto_mono[OF _ f]) simp_all
  1.1703 +  moreover {
  1.1704 +    have "filterlim (\<lambda>x. norm (f x)) (principal {0<..}) (principal {z. f z \<noteq> 0})"
  1.1705 +      by (auto simp: filterlim_def)
  1.1706 +    hence "filterlim (\<lambda>x. norm (f x)) (principal {0<..})
  1.1707 +             (inf F (principal {z. f z \<noteq> 0}))"
  1.1708 +      by (rule filterlim_mono) simp_all
  1.1709 +  }
  1.1710 +  ultimately have norm: "filterlim (\<lambda>x. norm (f x)) (at_right 0) (inf F (principal {z. f z \<noteq> 0}))"
  1.1711 +    by (simp add: filterlim_inf at_within_def)
  1.1712 +
  1.1713 +  have A: "LIM x inf F (principal {z. f z \<noteq> 0}). Re (g x) * -ln (cmod (f x)) :> at_top"
  1.1714 +    by (rule filterlim_tendsto_pos_mult_at_top tendsto_intros g' b
  1.1715 +          filterlim_compose[OF filterlim_uminus_at_top_at_bot] filterlim_compose[OF ln_at_0] norm)+
  1.1716 +  have B: "LIM x inf F (principal {z. f z \<noteq> 0}).
  1.1717 +          -\<bar>Im (g x)\<bar> * pi + -(Re (g x) * ln (cmod (f x))) :> at_top"
  1.1718 +    by (rule filterlim_tendsto_add_at_top tendsto_intros g')+ (insert A, simp_all)
  1.1719 +  have C: "(h \<longlongrightarrow> 0) F" unfolding h_def
  1.1720 +    by (intro filterlim_If tendsto_const filterlim_compose[OF exp_at_bot])
  1.1721 +       (insert B, auto simp: filterlim_uminus_at_bot algebra_simps)
  1.1722 +  show "((\<lambda>x. norm (f x powr g x)) \<longlongrightarrow> 0) F"
  1.1723 +    by (rule Lim_null_comparison[OF always_eventually C]) (insert le, auto)
  1.1724 +qed
  1.1725 +
  1.1726 +lemma tendsto_powr_complex' [tendsto_intros]:
  1.1727 +  fixes f g :: "_ \<Rightarrow> complex"
  1.1728 +  assumes fz: "a \<notin> \<real>\<^sub>\<le>\<^sub>0 \<or> (a = 0 \<and> Re b > 0)"
  1.1729 +  assumes fg: "(f \<longlongrightarrow> a) F" "(g \<longlongrightarrow> b) F"
  1.1730 +  shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
  1.1731 +proof (cases "a = 0")
  1.1732 +  case True
  1.1733 +  with assms show ?thesis by (auto intro!: tendsto_powr_complex_0)
  1.1734 +next
  1.1735 +  case False
  1.1736 +  with assms show ?thesis by (auto intro!: tendsto_powr_complex elim!: nonpos_Reals_cases)
  1.1737 +qed
  1.1738 +
  1.1739 +lemma continuous_powr_complex:
  1.1740 +  assumes "f (netlimit F) \<notin> \<real>\<^sub>\<le>\<^sub>0" "continuous F f" "continuous F g"
  1.1741 +  shows   "continuous F (\<lambda>z. f z powr g z :: complex)"
  1.1742 +  using assms unfolding continuous_def by (intro tendsto_powr_complex) simp_all
  1.1743 +
  1.1744 +lemma isCont_powr_complex [continuous_intros]:
  1.1745 +  assumes "f z \<notin> \<real>\<^sub>\<le>\<^sub>0" "isCont f z" "isCont g z"
  1.1746 +  shows   "isCont (\<lambda>z. f z powr g z :: complex) z"
  1.1747 +  using assms unfolding isCont_def by (intro tendsto_powr_complex) simp_all
  1.1748 +
  1.1749 +lemma continuous_on_powr_complex [continuous_intros]:
  1.1750 +  assumes "A \<subseteq> {z. Re (f z) \<ge> 0 \<or> Im (f z) \<noteq> 0}"
  1.1751 +  assumes "\<And>z. z \<in> A \<Longrightarrow> f z = 0 \<Longrightarrow> Re (g z) > 0"
  1.1752 +  assumes "continuous_on A f" "continuous_on A g"
  1.1753 +  shows   "continuous_on A (\<lambda>z. f z powr g z)"
  1.1754 +  unfolding continuous_on_def
  1.1755 +proof
  1.1756 +  fix z assume z: "z \<in> A"
  1.1757 +  show "((\<lambda>z. f z powr g z) \<longlongrightarrow> f z powr g z) (at z within A)"
  1.1758 +  proof (cases "f z = 0")
  1.1759 +    case False
  1.1760 +    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
  1.1761 +    with assms(3,4) z show ?thesis
  1.1762 +      by (intro tendsto_powr_complex')
  1.1763 +         (auto elim!: nonpos_Reals_cases simp: complex_eq_iff continuous_on_def)
  1.1764 +  next
  1.1765 +    case True
  1.1766 +    with assms z show ?thesis
  1.1767 +      by (auto intro!: tendsto_powr_complex_0 simp: continuous_on_def)
  1.1768 +  qed
  1.1769 +qed
  1.1770 +
  1.1771 +
  1.1772 +subsection\<open>Some Limits involving Logarithms\<close>
  1.1773 +
  1.1774 +lemma lim_Ln_over_power:
  1.1775 +  fixes s::complex
  1.1776 +  assumes "0 < Re s"
  1.1777 +    shows "((\<lambda>n. Ln n / (n powr s)) \<longlongrightarrow> 0) sequentially"
  1.1778 +proof (simp add: lim_sequentially dist_norm, clarify)
  1.1779 +  fix e::real
  1.1780 +  assume e: "0 < e"
  1.1781 +  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"
  1.1782 +  proof (rule_tac x="2/(e * (Re s)\<^sup>2)" in exI, safe)
  1.1783 +    show "0 < 2 / (e * (Re s)\<^sup>2)"
  1.1784 +      using e assms by (simp add: field_simps)
  1.1785 +  next
  1.1786 +    fix x::real
  1.1787 +    assume x: "2 / (e * (Re s)\<^sup>2) \<le> x"
  1.1788 +    then have "x>0"
  1.1789 +    using e assms
  1.1790 +      by (metis less_le_trans mult_eq_0_iff mult_pos_pos pos_less_divide_eq power2_eq_square
  1.1791 +                zero_less_numeral)
  1.1792 +    then show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
  1.1793 +      using e assms x
  1.1794 +      apply (auto simp: field_simps)
  1.1795 +      apply (rule_tac y = "e * (x\<^sup>2 * (Re s)\<^sup>2)" in le_less_trans)
  1.1796 +      apply (auto simp: power2_eq_square field_simps add_pos_pos)
  1.1797 +      done
  1.1798 +  qed
  1.1799 +  then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < 1 + (Re s * x) + (1/2) * (Re s * x)^2"
  1.1800 +    using e  by (simp add: field_simps)
  1.1801 +  then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < exp (Re s * x)"
  1.1802 +    using assms
  1.1803 +    by (force intro: less_le_trans [OF _ exp_lower_taylor_quadratic])
  1.1804 +  then have "\<exists>xo>0. \<forall>x\<ge>xo. x < e * exp (Re s * x)"
  1.1805 +    using e   by (auto simp: field_simps)
  1.1806 +  with e show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
  1.1807 +    apply (auto simp: norm_divide norm_powr_real divide_simps)
  1.1808 +    apply (rule_tac x="nat \<lceil>exp xo\<rceil>" in exI)
  1.1809 +    apply clarify
  1.1810 +    apply (drule_tac x="ln n" in spec)
  1.1811 +    apply (auto simp: exp_less_mono nat_ceiling_le_eq not_le)
  1.1812 +    apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff)
  1.1813 +    done
  1.1814 +qed
  1.1815 +
  1.1816 +lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
  1.1817 +  using lim_Ln_over_power [of 1]
  1.1818 +  by simp
  1.1819 +
  1.1820 +lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
  1.1821 +  using Ln_of_real by force
  1.1822 +
  1.1823 +lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
  1.1824 +  by (simp add: powr_of_real)
  1.1825 +
  1.1826 +lemma lim_ln_over_power:
  1.1827 +  fixes s :: real
  1.1828 +  assumes "0 < s"
  1.1829 +    shows "((\<lambda>n. ln n / (n powr s)) \<longlongrightarrow> 0) sequentially"
  1.1830 +  using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
  1.1831 +  apply (subst filterlim_sequentially_Suc [symmetric])
  1.1832 +  apply (simp add: lim_sequentially dist_norm
  1.1833 +          Ln_Reals_eq norm_powr_real_powr norm_divide)
  1.1834 +  done
  1.1835 +
  1.1836 +lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
  1.1837 +  using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]]
  1.1838 +  apply (subst filterlim_sequentially_Suc [symmetric])
  1.1839 +  apply (simp add: lim_sequentially dist_norm)
  1.1840 +  done
  1.1841 +
  1.1842 +lemma lim_1_over_complex_power:
  1.1843 +  assumes "0 < Re s"
  1.1844 +    shows "((\<lambda>n. 1 / (of_nat n powr s)) \<longlongrightarrow> 0) sequentially"
  1.1845 +proof -
  1.1846 +  have "\<forall>n>0. 3 \<le> n \<longrightarrow> 1 \<le> ln (real_of_nat n)"
  1.1847 +    using ln3_gt_1
  1.1848 +    by (force intro: order_trans [of _ "ln 3"] ln3_gt_1)
  1.1849 +  moreover have "(\<lambda>n. cmod (Ln (of_nat n) / of_nat n powr s)) \<longlonglongrightarrow> 0"
  1.1850 +    using lim_Ln_over_power [OF assms]
  1.1851 +    by (metis tendsto_norm_zero_iff)
  1.1852 +  ultimately show ?thesis
  1.1853 +    apply (auto intro!: Lim_null_comparison [where g = "\<lambda>n. norm (Ln(of_nat n) / of_nat n powr s)"])
  1.1854 +    apply (auto simp: norm_divide divide_simps eventually_sequentially)
  1.1855 +    done
  1.1856 +qed
  1.1857 +
  1.1858 +lemma lim_1_over_real_power:
  1.1859 +  fixes s :: real
  1.1860 +  assumes "0 < s"
  1.1861 +    shows "((\<lambda>n. 1 / (of_nat n powr s)) \<longlongrightarrow> 0) sequentially"
  1.1862 +  using lim_1_over_complex_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
  1.1863 +  apply (subst filterlim_sequentially_Suc [symmetric])
  1.1864 +  apply (simp add: lim_sequentially dist_norm)
  1.1865 +  apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide)
  1.1866 +  done
  1.1867 +
  1.1868 +lemma lim_1_over_Ln: "((\<lambda>n. 1 / Ln(of_nat n)) \<longlongrightarrow> 0) sequentially"
  1.1869 +proof (clarsimp simp add: lim_sequentially dist_norm norm_divide divide_simps)
  1.1870 +  fix r::real
  1.1871 +  assume "0 < r"
  1.1872 +  have ir: "inverse (exp (inverse r)) > 0"
  1.1873 +    by simp
  1.1874 +  obtain n where n: "1 < of_nat n * inverse (exp (inverse r))"
  1.1875 +    using ex_less_of_nat_mult [of _ 1, OF ir]
  1.1876 +    by auto
  1.1877 +  then have "exp (inverse r) < of_nat n"
  1.1878 +    by (simp add: divide_simps)
  1.1879 +  then have "ln (exp (inverse r)) < ln (of_nat n)"
  1.1880 +    by (metis exp_gt_zero less_trans ln_exp ln_less_cancel_iff)
  1.1881 +  with \<open>0 < r\<close> have "1 < r * ln (real_of_nat n)"
  1.1882 +    by (simp add: field_simps)
  1.1883 +  moreover have "n > 0" using n
  1.1884 +    using neq0_conv by fastforce
  1.1885 +  ultimately show "\<exists>no. \<forall>n. Ln (of_nat n) \<noteq> 0 \<longrightarrow> no \<le> n \<longrightarrow> 1 < r * cmod (Ln (of_nat n))"
  1.1886 +    using n \<open>0 < r\<close>
  1.1887 +    apply (rule_tac x=n in exI)
  1.1888 +    apply (auto simp: divide_simps)
  1.1889 +    apply (erule less_le_trans, auto)
  1.1890 +    done
  1.1891 +qed
  1.1892 +
  1.1893 +lemma lim_1_over_ln: "((\<lambda>n. 1 / ln(real_of_nat n)) \<longlongrightarrow> 0) sequentially"
  1.1894 +  using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]]
  1.1895 +  apply (subst filterlim_sequentially_Suc [symmetric])
  1.1896 +  apply (simp add: lim_sequentially dist_norm)
  1.1897 +  apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide)
  1.1898 +  done
  1.1899 +
  1.1900 +
  1.1901 +subsection\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
  1.1902 +
  1.1903 +lemma csqrt_exp_Ln:
  1.1904 +  assumes "z \<noteq> 0"
  1.1905 +    shows "csqrt z = exp(Ln(z) / 2)"
  1.1906 +proof -
  1.1907 +  have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
  1.1908 +    by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
  1.1909 +  also have "... = z"
  1.1910 +    using assms exp_Ln by blast
  1.1911 +  finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
  1.1912 +    by simp
  1.1913 +  also have "... = exp (Ln z / 2)"
  1.1914 +    apply (subst csqrt_square)
  1.1915 +    using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
  1.1916 +    apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+)
  1.1917 +    done
  1.1918 +  finally show ?thesis using assms csqrt_square
  1.1919 +    by simp
  1.1920 +qed
  1.1921 +
  1.1922 +lemma csqrt_inverse:
  1.1923 +  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
  1.1924 +    shows "csqrt (inverse z) = inverse (csqrt z)"
  1.1925 +proof (cases "z=0", simp)
  1.1926 +  assume "z \<noteq> 0"
  1.1927 +  then show ?thesis
  1.1928 +    using assms csqrt_exp_Ln Ln_inverse exp_minus
  1.1929 +    by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
  1.1930 +qed
  1.1931 +
  1.1932 +lemma cnj_csqrt:
  1.1933 +  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
  1.1934 +    shows "cnj(csqrt z) = csqrt(cnj z)"
  1.1935 +proof (cases "z=0", simp)
  1.1936 +  assume "z \<noteq> 0"
  1.1937 +  then show ?thesis
  1.1938 +     by (simp add: assms cnj_Ln csqrt_exp_Ln exp_cnj)
  1.1939 +qed
  1.1940 +
  1.1941 +lemma has_field_derivative_csqrt:
  1.1942 +  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
  1.1943 +    shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)"
  1.1944 +proof -
  1.1945 +  have z: "z \<noteq> 0"
  1.1946 +    using assms by auto
  1.1947 +  then have *: "inverse z = inverse (2*z) * 2"
  1.1948 +    by (simp add: divide_simps)
  1.1949 +  have [simp]: "exp (Ln z / 2) * inverse z = inverse (csqrt z)"
  1.1950 +    by (simp add: z field_simps csqrt_exp_Ln [symmetric]) (metis power2_csqrt power2_eq_square)
  1.1951 +  have "Im z = 0 \<Longrightarrow> 0 < Re z"
  1.1952 +    using assms complex_nonpos_Reals_iff not_less by blast
  1.1953 +  with z have "((\<lambda>z. exp (Ln z / 2)) has_field_derivative inverse (2 * csqrt z)) (at z)"
  1.1954 +    by (force intro: derivative_eq_intros * simp add: assms)
  1.1955 +  then show ?thesis
  1.1956 +    apply (rule DERIV_transform_at[where d = "norm z"])
  1.1957 +    apply (intro z derivative_eq_intros | simp add: assms)+
  1.1958 +    using z
  1.1959 +    apply (metis csqrt_exp_Ln dist_0_norm less_irrefl)
  1.1960 +    done
  1.1961 +qed
  1.1962 +
  1.1963 +lemma field_differentiable_at_csqrt:
  1.1964 +    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt field_differentiable at z"
  1.1965 +  using field_differentiable_def has_field_derivative_csqrt by blast
  1.1966 +
  1.1967 +lemma field_differentiable_within_csqrt:
  1.1968 +    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt field_differentiable (at z within s)"
  1.1969 +  using field_differentiable_at_csqrt field_differentiable_within_subset by blast
  1.1970 +
  1.1971 +lemma continuous_at_csqrt:
  1.1972 +    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) csqrt"
  1.1973 +  by (simp add: field_differentiable_within_csqrt field_differentiable_imp_continuous_at)
  1.1974 +
  1.1975 +corollary isCont_csqrt' [simp]:
  1.1976 +   "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
  1.1977 +  by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
  1.1978 +
  1.1979 +lemma continuous_within_csqrt:
  1.1980 +    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within s) csqrt"
  1.1981 +  by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_csqrt)
  1.1982 +
  1.1983 +lemma continuous_on_csqrt [continuous_intros]:
  1.1984 +    "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s csqrt"
  1.1985 +  by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
  1.1986 +
  1.1987 +lemma holomorphic_on_csqrt:
  1.1988 +    "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> csqrt holomorphic_on s"
  1.1989 +  by (simp add: field_differentiable_within_csqrt holomorphic_on_def)
  1.1990 +
  1.1991 +lemma continuous_within_closed_nontrivial:
  1.1992 +    "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
  1.1993 +  using open_Compl
  1.1994 +  by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
  1.1995 +
  1.1996 +lemma continuous_within_csqrt_posreal:
  1.1997 +    "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
  1.1998 +proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
  1.1999 +  case True
  1.2000 +  then have "Im z = 0" "Re z < 0 \<or> z = 0"
  1.2001 +    using cnj.code complex_cnj_zero_iff  by (auto simp: complex_nonpos_Reals_iff) fastforce
  1.2002 +  then show ?thesis
  1.2003 +    apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
  1.2004 +    apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
  1.2005 +    apply (rule_tac x="e^2" in exI)
  1.2006 +    apply (auto simp: Reals_def)
  1.2007 +    by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
  1.2008 +next
  1.2009 +  case False
  1.2010 +    then show ?thesis   by (blast intro: continuous_within_csqrt)
  1.2011 +qed
  1.2012 +
  1.2013 +subsection\<open>Complex arctangent\<close>
  1.2014 +
  1.2015 +text\<open>The branch cut gives standard bounds in the real case.\<close>
  1.2016 +
  1.2017 +definition Arctan :: "complex \<Rightarrow> complex" where
  1.2018 +    "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))"
  1.2019 +
  1.2020 +lemma Arctan_def_moebius: "Arctan z = \<i>/2 * Ln (moebius (-\<i>) 1 \<i> 1 z)"
  1.2021 +  by (simp add: Arctan_def moebius_def add_ac)
  1.2022 +
  1.2023 +lemma Ln_conv_Arctan:
  1.2024 +  assumes "z \<noteq> -1"
  1.2025 +  shows   "Ln z = -2*\<i> * Arctan (moebius 1 (- 1) (- \<i>) (- \<i>) z)"
  1.2026 +proof -
  1.2027 +  have "Arctan (moebius 1 (- 1) (- \<i>) (- \<i>) z) =
  1.2028 +             \<i>/2 * Ln (moebius (- \<i>) 1 \<i> 1 (moebius 1 (- 1) (- \<i>) (- \<i>) z))"
  1.2029 +    by (simp add: Arctan_def_moebius)
  1.2030 +  also from assms have "\<i> * z \<noteq> \<i> * (-1)" by (subst mult_left_cancel) simp
  1.2031 +  hence "\<i> * z - -\<i> \<noteq> 0" by (simp add: eq_neg_iff_add_eq_0)
  1.2032 +  from moebius_inverse'[OF _ this, of 1 1]
  1.2033 +    have "moebius (- \<i>) 1 \<i> 1 (moebius 1 (- 1) (- \<i>) (- \<i>) z) = z" by simp
  1.2034 +  finally show ?thesis by (simp add: field_simps)
  1.2035 +qed
  1.2036 +
  1.2037 +lemma Arctan_0 [simp]: "Arctan 0 = 0"
  1.2038 +  by (simp add: Arctan_def)
  1.2039 +
  1.2040 +lemma Im_complex_div_lemma: "Im((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<longleftrightarrow> Re z = 0"
  1.2041 +  by (auto simp: Im_complex_div_eq_0 algebra_simps)
  1.2042 +
  1.2043 +lemma Re_complex_div_lemma: "0 < Re((1 - \<i>*z) / (1 + \<i>*z)) \<longleftrightarrow> norm z < 1"
  1.2044 +  by (simp add: Re_complex_div_gt_0 algebra_simps cmod_def power2_eq_square)
  1.2045 +
  1.2046 +lemma tan_Arctan:
  1.2047 +  assumes "z\<^sup>2 \<noteq> -1"
  1.2048 +    shows [simp]:"tan(Arctan z) = z"
  1.2049 +proof -
  1.2050 +  have "1 + \<i>*z \<noteq> 0"
  1.2051 +    by (metis assms complex_i_mult_minus i_squared minus_unique power2_eq_square power2_minus)
  1.2052 +  moreover
  1.2053 +  have "1 - \<i>*z \<noteq> 0"
  1.2054 +    by (metis assms complex_i_mult_minus i_squared power2_eq_square power2_minus right_minus_eq)
  1.2055 +  ultimately
  1.2056 +  show ?thesis
  1.2057 +    by (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus csqrt_exp_Ln [symmetric]
  1.2058 +                  divide_simps power2_eq_square [symmetric])
  1.2059 +qed
  1.2060 +
  1.2061 +lemma Arctan_tan [simp]:
  1.2062 +  assumes "\<bar>Re z\<bar> < pi/2"
  1.2063 +    shows "Arctan(tan z) = z"
  1.2064 +proof -
  1.2065 +  have ge_pi2: "\<And>n::int. \<bar>of_int (2*n + 1) * pi/2\<bar> \<ge> pi/2"
  1.2066 +    by (case_tac n rule: int_cases) (auto simp: abs_mult)
  1.2067 +  have "exp (\<i>*z)*exp (\<i>*z) = -1 \<longleftrightarrow> exp (2*\<i>*z) = -1"
  1.2068 +    by (metis distrib_right exp_add mult_2)
  1.2069 +  also have "... \<longleftrightarrow> exp (2*\<i>*z) = exp (\<i>*pi)"
  1.2070 +    using cis_conv_exp cis_pi by auto
  1.2071 +  also have "... \<longleftrightarrow> exp (2*\<i>*z - \<i>*pi) = 1"
  1.2072 +    by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute)
  1.2073 +  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)"
  1.2074 +    by (simp add: exp_eq_1)
  1.2075 +  also have "... \<longleftrightarrow> Im z = 0 \<and> (\<exists>n::int. 2 * Re z = of_int (2*n + 1) * pi)"
  1.2076 +    by (simp add: algebra_simps)
  1.2077 +  also have "... \<longleftrightarrow> False"
  1.2078 +    using assms ge_pi2
  1.2079 +    apply (auto simp: algebra_simps)
  1.2080 +    by (metis abs_mult_pos not_less of_nat_less_0_iff of_nat_numeral)
  1.2081 +  finally have *: "exp (\<i>*z)*exp (\<i>*z) + 1 \<noteq> 0"
  1.2082 +    by (auto simp: add.commute minus_unique)
  1.2083 +  show ?thesis
  1.2084 +    using assms *
  1.2085 +    apply (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps
  1.2086 +                     ii_times_eq_iff power2_eq_square [symmetric])
  1.2087 +    apply (rule Ln_unique)
  1.2088 +    apply (auto simp: divide_simps exp_minus)
  1.2089 +    apply (simp add: algebra_simps exp_double [symmetric])
  1.2090 +    done
  1.2091 +qed
  1.2092 +
  1.2093 +lemma
  1.2094 +  assumes "Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1"
  1.2095 +  shows Re_Arctan_bounds: "\<bar>Re(Arctan z)\<bar> < pi/2"
  1.2096 +    and has_field_derivative_Arctan: "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
  1.2097 +proof -
  1.2098 +  have nz0: "1 + \<i>*z \<noteq> 0"
  1.2099 +    using assms
  1.2100 +    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2)
  1.2101 +              less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
  1.2102 +  have "z \<noteq> -\<i>" using assms
  1.2103 +    by auto
  1.2104 +  then have zz: "1 + z * z \<noteq> 0"
  1.2105 +    by (metis abs_one assms i_squared ii.simps less_irrefl minus_unique square_eq_iff)
  1.2106 +  have nz1: "1 - \<i>*z \<noteq> 0"
  1.2107 +    using assms by (force simp add: ii_times_eq_iff)
  1.2108 +  have nz2: "inverse (1 + \<i>*z) \<noteq> 0"
  1.2109 +    using assms
  1.2110 +    by (metis Im_complex_div_lemma Re_complex_div_lemma cmod_eq_Im divide_complex_def
  1.2111 +              less_irrefl mult_zero_right zero_complex.simps(1) zero_complex.simps(2))
  1.2112 +  have nzi: "((1 - \<i>*z) * inverse (1 + \<i>*z)) \<noteq> 0"
  1.2113 +    using nz1 nz2 by auto
  1.2114 +  have "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))"
  1.2115 +    apply (simp add: divide_complex_def)
  1.2116 +    apply (simp add: divide_simps split: if_split_asm)
  1.2117 +    using assms
  1.2118 +    apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square])
  1.2119 +    done
  1.2120 +  then have *: "((1 - \<i>*z) / (1 + \<i>*z)) \<notin> \<real>\<^sub>\<le>\<^sub>0"
  1.2121 +    by (auto simp add: complex_nonpos_Reals_iff)
  1.2122 +  show "\<bar>Re(Arctan z)\<bar> < pi/2"
  1.2123 +    unfolding Arctan_def divide_complex_def
  1.2124 +    using mpi_less_Im_Ln [OF nzi]
  1.2125 +    apply (auto simp: abs_if intro!: Im_Ln_less_pi * [unfolded divide_complex_def])
  1.2126 +    done
  1.2127 +  show "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
  1.2128 +    unfolding Arctan_def scaleR_conv_of_real
  1.2129 +    apply (rule DERIV_cong)
  1.2130 +    apply (intro derivative_eq_intros | simp add: nz0 *)+
  1.2131 +    using nz0 nz1 zz
  1.2132 +    apply (simp add: divide_simps power2_eq_square)
  1.2133 +    apply (auto simp: algebra_simps)
  1.2134 +    done
  1.2135 +qed
  1.2136 +
  1.2137 +lemma field_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan field_differentiable at z"
  1.2138 +  using has_field_derivative_Arctan
  1.2139 +  by (auto simp: field_differentiable_def)
  1.2140 +
  1.2141 +lemma field_differentiable_within_Arctan:
  1.2142 +    "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan field_differentiable (at z within s)"
  1.2143 +  using field_differentiable_at_Arctan field_differentiable_at_within by blast
  1.2144 +
  1.2145 +declare has_field_derivative_Arctan [derivative_intros]
  1.2146 +declare has_field_derivative_Arctan [THEN DERIV_chain2, derivative_intros]
  1.2147 +
  1.2148 +lemma continuous_at_Arctan:
  1.2149 +    "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous (at z) Arctan"
  1.2150 +  by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Arctan)
  1.2151 +
  1.2152 +lemma continuous_within_Arctan:
  1.2153 +    "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arctan"
  1.2154 +  using continuous_at_Arctan continuous_at_imp_continuous_within by blast
  1.2155 +
  1.2156 +lemma continuous_on_Arctan [continuous_intros]:
  1.2157 +    "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous_on s Arctan"
  1.2158 +  by (auto simp: continuous_at_imp_continuous_on continuous_within_Arctan)
  1.2159 +
  1.2160 +lemma holomorphic_on_Arctan:
  1.2161 +    "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
  1.2162 +  by (simp add: field_differentiable_within_Arctan holomorphic_on_def)
  1.2163 +
  1.2164 +lemma Arctan_series:
  1.2165 +  assumes z: "norm (z :: complex) < 1"
  1.2166 +  defines "g \<equiv> \<lambda>n. if odd n then -\<i>*\<i>^n / n else 0"
  1.2167 +  defines "h \<equiv> \<lambda>z n. (-1)^n / of_nat (2*n+1) * (z::complex)^(2*n+1)"
  1.2168 +  shows   "(\<lambda>n. g n * z^n) sums Arctan z"
  1.2169 +  and     "h z sums Arctan z"
  1.2170 +proof -
  1.2171 +  define G where [abs_def]: "G z = (\<Sum>n. g n * z^n)" for z
  1.2172 +  have summable: "summable (\<lambda>n. g n * u^n)" if "norm u < 1" for u
  1.2173 +  proof (cases "u = 0")
  1.2174 +    assume u: "u \<noteq> 0"
  1.2175 +    have "(\<lambda>n. ereal (norm (h u n) / norm (h u (Suc n)))) = (\<lambda>n. ereal (inverse (norm u)^2) *
  1.2176 +              ereal ((2 + inverse (real (Suc n))) / (2 - inverse (real (Suc n)))))"
  1.2177 +    proof
  1.2178 +      fix n
  1.2179 +      have "ereal (norm (h u n) / norm (h u (Suc n))) =
  1.2180 +             ereal (inverse (norm u)^2) * ereal ((of_nat (2*Suc n+1) / of_nat (Suc n)) /
  1.2181 +                 (of_nat (2*Suc n-1) / of_nat (Suc n)))"
  1.2182 +      by (simp add: h_def norm_mult norm_power norm_divide divide_simps
  1.2183 +                    power2_eq_square eval_nat_numeral del: of_nat_add of_nat_Suc)
  1.2184 +      also have "of_nat (2*Suc n+1) / of_nat (Suc n) = (2::real) + inverse (real (Suc n))"
  1.2185 +        by (auto simp: divide_simps simp del: of_nat_Suc) simp_all?
  1.2186 +      also have "of_nat (2*Suc n-1) / of_nat (Suc n) = (2::real) - inverse (real (Suc n))"
  1.2187 +        by (auto simp: divide_simps simp del: of_nat_Suc) simp_all?
  1.2188 +      finally show "ereal (norm (h u n) / norm (h u (Suc n))) = ereal (inverse (norm u)^2) *
  1.2189 +              ereal ((2 + inverse (real (Suc n))) / (2 - inverse (real (Suc n))))" .
  1.2190 +    qed
  1.2191 +    also have "\<dots> \<longlonglongrightarrow> ereal (inverse (norm u)^2) * ereal ((2 + 0) / (2 - 0))"
  1.2192 +      by (intro tendsto_intros LIMSEQ_inverse_real_of_nat) simp_all
  1.2193 +    finally have "liminf (\<lambda>n. ereal (cmod (h u n) / cmod (h u (Suc n)))) = inverse (norm u)^2"
  1.2194 +      by (intro lim_imp_Liminf) simp_all
  1.2195 +    moreover from power_strict_mono[OF that, of 2] u have "inverse (norm u)^2 > 1"
  1.2196 +      by (simp add: divide_simps)
  1.2197 +    ultimately have A: "liminf (\<lambda>n. ereal (cmod (h u n) / cmod (h u (Suc n)))) > 1" by simp
  1.2198 +    from u have "summable (h u)"
  1.2199 +      by (intro summable_norm_cancel[OF ratio_test_convergence[OF _ A]])
  1.2200 +         (auto simp: h_def norm_divide norm_mult norm_power simp del: of_nat_Suc
  1.2201 +               intro!: mult_pos_pos divide_pos_pos always_eventually)
  1.2202 +    thus "summable (\<lambda>n. g n * u^n)"
  1.2203 +      by (subst summable_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
  1.2204 +         (auto simp: power_mult subseq_def g_def h_def elim!: oddE)
  1.2205 +  qed (simp add: h_def)
  1.2206 +
  1.2207 +  have "\<exists>c. \<forall>u\<in>ball 0 1. Arctan u - G u = c"
  1.2208 +  proof (rule has_field_derivative_zero_constant)
  1.2209 +    fix u :: complex assume "u \<in> ball 0 1"
  1.2210 +    hence u: "norm u < 1" by (simp add: dist_0_norm)
  1.2211 +    define K where "K = (norm u + 1) / 2"
  1.2212 +    from u and abs_Im_le_cmod[of u] have Im_u: "\<bar>Im u\<bar> < 1" by linarith
  1.2213 +    from u have K: "0 \<le> K" "norm u < K" "K < 1" by (simp_all add: K_def)
  1.2214 +    hence "(G has_field_derivative (\<Sum>n. diffs g n * u ^ n)) (at u)" unfolding G_def
  1.2215 +      by (intro termdiffs_strong[of _ "of_real K"] summable) simp_all
  1.2216 +    also have "(\<lambda>n. diffs g n * u^n) = (\<lambda>n. if even n then (\<i>*u)^n else 0)"
  1.2217 +      by (intro ext) (simp_all del: of_nat_Suc add: g_def diffs_def power_mult_distrib)
  1.2218 +    also have "suminf \<dots> = (\<Sum>n. (-(u^2))^n)"
  1.2219 +      by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric])
  1.2220 +         (auto elim!: evenE simp: subseq_def power_mult power_mult_distrib)
  1.2221 +    also from u have "norm u^2 < 1^2" by (intro power_strict_mono) simp_all
  1.2222 +    hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)"
  1.2223 +      by (subst suminf_geometric) (simp_all add: norm_power inverse_eq_divide)
  1.2224 +    finally have "(G has_field_derivative inverse (1 + u\<^sup>2)) (at u)" .
  1.2225 +    from DERIV_diff[OF has_field_derivative_Arctan this] Im_u u
  1.2226 +      show "((\<lambda>u. Arctan u - G u) has_field_derivative 0) (at u within ball 0 1)"
  1.2227 +      by (simp_all add: dist_0_norm at_within_open[OF _ open_ball])
  1.2228 +  qed simp_all
  1.2229 +  then obtain c where c: "\<And>u. norm u < 1 \<Longrightarrow> Arctan u - G u = c" by (auto simp: dist_0_norm)
  1.2230 +  from this[of 0] have "c = 0" by (simp add: G_def g_def powser_zero)
  1.2231 +  with c z have "Arctan z = G z" by simp
  1.2232 +  with summable[OF z] show "(\<lambda>n. g n * z^n) sums Arctan z" unfolding G_def by (simp add: sums_iff)
  1.2233 +  thus "h z sums Arctan z" by (subst (asm) sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
  1.2234 +                              (auto elim!: oddE simp: subseq_def power_mult g_def h_def)
  1.2235 +qed
  1.2236 +
  1.2237 +text \<open>A quickly-converging series for the logarithm, based on the arctangent.\<close>
  1.2238 +lemma ln_series_quadratic:
  1.2239 +  assumes x: "x > (0::real)"
  1.2240 +  shows "(\<lambda>n. (2*((x - 1) / (x + 1)) ^ (2*n+1) / of_nat (2*n+1))) sums ln x"
  1.2241 +proof -
  1.2242 +  define y :: complex where "y = of_real ((x-1)/(x+1))"
  1.2243 +  from x have x': "complex_of_real x \<noteq> of_real (-1)"  by (subst of_real_eq_iff) auto
  1.2244 +  from x have "\<bar>x - 1\<bar> < \<bar>x + 1\<bar>" by linarith
  1.2245 +  hence "norm (complex_of_real (x - 1) / complex_of_real (x + 1)) < 1"
  1.2246 +    by (simp add: norm_divide del: of_real_add of_real_diff)
  1.2247 +  hence "norm (\<i> * y) < 1" unfolding y_def by (subst norm_mult) simp
  1.2248 +  hence "(\<lambda>n. (-2*\<i>) * ((-1)^n / of_nat (2*n+1) * (\<i>*y)^(2*n+1))) sums ((-2*\<i>) * Arctan (\<i>*y))"
  1.2249 +    by (intro Arctan_series sums_mult) simp_all
  1.2250 +  also have "(\<lambda>n. (-2*\<i>) * ((-1)^n / of_nat (2*n+1) * (\<i>*y)^(2*n+1))) =
  1.2251 +                 (\<lambda>n. (-2*\<i>) * ((-1)^n * (\<i>*y*(-y\<^sup>2)^n)/of_nat (2*n+1)))"
  1.2252 +    by (intro ext) (simp_all add: power_mult power_mult_distrib)
  1.2253 +  also have "\<dots> = (\<lambda>n. 2*y* ((-1) * (-y\<^sup>2))^n/of_nat (2*n+1))"
  1.2254 +    by (intro ext, subst power_mult_distrib) (simp add: algebra_simps power_mult)
  1.2255 +  also have "\<dots> = (\<lambda>n. 2*y^(2*n+1) / of_nat (2*n+1))"
  1.2256 +    by (subst power_add, subst power_mult) (simp add: mult_ac)
  1.2257 +  also have "\<dots> = (\<lambda>n. of_real (2*((x-1)/(x+1))^(2*n+1) / of_nat (2*n+1)))"
  1.2258 +    by (intro ext) (simp add: y_def)
  1.2259 +  also have "\<i> * y = (of_real x - 1) / (-\<i> * (of_real x + 1))"
  1.2260 +    by (subst divide_divide_eq_left [symmetric]) (simp add: y_def)
  1.2261 +  also have "\<dots> = moebius 1 (-1) (-\<i>) (-\<i>) (of_real x)" by (simp add: moebius_def algebra_simps)
  1.2262 +  also from x' have "-2*\<i>*Arctan \<dots> = Ln (of_real x)" by (intro Ln_conv_Arctan [symmetric]) simp_all
  1.2263 +  also from x have "\<dots> = ln x" by (rule Ln_of_real)
  1.2264 +  finally show ?thesis by (subst (asm) sums_of_real_iff)
  1.2265 +qed
  1.2266 +
  1.2267 +subsection \<open>Real arctangent\<close>
  1.2268 +
  1.2269 +lemma norm_exp_ii_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
  1.2270 +  by simp
  1.2271 +
  1.2272 +lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
  1.2273 +  by (simp add: complex_norm_eq_1_exp)
  1.2274 +
  1.2275 +lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
  1.2276 +  unfolding Arctan_def divide_complex_def
  1.2277 +  apply (simp add: complex_eq_iff)
  1.2278 +  apply (rule norm_exp_imaginary)
  1.2279 +  apply (subst exp_Ln, auto)
  1.2280 +  apply (simp_all add: cmod_def complex_eq_iff)
  1.2281 +  apply (auto simp: divide_simps)
  1.2282 +  apply (metis power_one sum_power2_eq_zero_iff zero_neq_one, algebra)
  1.2283 +  done
  1.2284 +
  1.2285 +lemma arctan_eq_Re_Arctan: "arctan x = Re (Arctan (of_real x))"
  1.2286 +proof (rule arctan_unique)
  1.2287 +  show "- (pi / 2) < Re (Arctan (complex_of_real x))"
  1.2288 +    apply (simp add: Arctan_def)
  1.2289 +    apply (rule Im_Ln_less_pi)
  1.2290 +    apply (auto simp: Im_complex_div_lemma complex_nonpos_Reals_iff)
  1.2291 +    done
  1.2292 +next
  1.2293 +  have *: " (1 - \<i>*x) / (1 + \<i>*x) \<noteq> 0"
  1.2294 +    by (simp add: divide_simps) ( simp add: complex_eq_iff)
  1.2295 +  show "Re (Arctan (complex_of_real x)) < pi / 2"
  1.2296 +    using mpi_less_Im_Ln [OF *]
  1.2297 +    by (simp add: Arctan_def)
  1.2298 +next
  1.2299 +  have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))"
  1.2300 +    apply (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos)
  1.2301 +    apply (simp add: field_simps)
  1.2302 +    by (simp add: power2_eq_square)
  1.2303 +  also have "... = x"
  1.2304 +    apply (subst tan_Arctan, auto)
  1.2305 +    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)
  1.2306 +  finally show "tan (Re (Arctan (complex_of_real x))) = x" .
  1.2307 +qed
  1.2308 +
  1.2309 +lemma Arctan_of_real: "Arctan (of_real x) = of_real (arctan x)"
  1.2310 +  unfolding arctan_eq_Re_Arctan divide_complex_def
  1.2311 +  by (simp add: complex_eq_iff)
  1.2312 +
  1.2313 +lemma Arctan_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Arctan z \<in> \<real>"
  1.2314 +  by (metis Reals_cases Reals_of_real Arctan_of_real)
  1.2315 +
  1.2316 +declare arctan_one [simp]
  1.2317 +
  1.2318 +lemma arctan_less_pi4_pos: "x < 1 \<Longrightarrow> arctan x < pi/4"
  1.2319 +  by (metis arctan_less_iff arctan_one)
  1.2320 +
  1.2321 +lemma arctan_less_pi4_neg: "-1 < x \<Longrightarrow> -(pi/4) < arctan x"
  1.2322 +  by (metis arctan_less_iff arctan_minus arctan_one)
  1.2323 +
  1.2324 +lemma arctan_less_pi4: "\<bar>x\<bar> < 1 \<Longrightarrow> \<bar>arctan x\<bar> < pi/4"
  1.2325 +  by (metis abs_less_iff arctan_less_pi4_pos arctan_minus)
  1.2326 +
  1.2327 +lemma arctan_le_pi4: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>arctan x\<bar> \<le> pi/4"
  1.2328 +  by (metis abs_le_iff arctan_le_iff arctan_minus arctan_one)
  1.2329 +
  1.2330 +lemma abs_arctan: "\<bar>arctan x\<bar> = arctan \<bar>x\<bar>"
  1.2331 +  by (simp add: abs_if arctan_minus)
  1.2332 +
  1.2333 +lemma arctan_add_raw:
  1.2334 +  assumes "\<bar>arctan x + arctan y\<bar> < pi/2"
  1.2335 +    shows "arctan x + arctan y = arctan((x + y) / (1 - x * y))"
  1.2336 +proof (rule arctan_unique [symmetric])
  1.2337 +  show 12: "- (pi / 2) < arctan x + arctan y" "arctan x + arctan y < pi / 2"
  1.2338 +    using assms by linarith+
  1.2339 +  show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
  1.2340 +    using cos_gt_zero_pi [OF 12]
  1.2341 +    by (simp add: arctan tan_add)
  1.2342 +qed
  1.2343 +
  1.2344 +lemma arctan_inverse:
  1.2345 +  assumes "0 < x"
  1.2346 +    shows "arctan(inverse x) = pi/2 - arctan x"
  1.2347 +proof -
  1.2348 +  have "arctan(inverse x) = arctan(inverse(tan(arctan x)))"
  1.2349 +    by (simp add: arctan)
  1.2350 +  also have "... = arctan (tan (pi / 2 - arctan x))"
  1.2351 +    by (simp add: tan_cot)
  1.2352 +  also have "... = pi/2 - arctan x"
  1.2353 +  proof -
  1.2354 +    have "0 < pi - arctan x"
  1.2355 +    using arctan_ubound [of x] pi_gt_zero by linarith
  1.2356 +    with assms show ?thesis
  1.2357 +      by (simp add: Transcendental.arctan_tan)
  1.2358 +  qed
  1.2359 +  finally show ?thesis .
  1.2360 +qed
  1.2361 +
  1.2362 +lemma arctan_add_small:
  1.2363 +  assumes "\<bar>x * y\<bar> < 1"
  1.2364 +    shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))"
  1.2365 +proof (cases "x = 0 \<or> y = 0")
  1.2366 +  case True then show ?thesis
  1.2367 +    by auto
  1.2368 +next
  1.2369 +  case False
  1.2370 +  then have *: "\<bar>arctan x\<bar> < pi / 2 - \<bar>arctan y\<bar>" using assms
  1.2371 +    apply (auto simp add: abs_arctan arctan_inverse [symmetric] arctan_less_iff)
  1.2372 +    apply (simp add: divide_simps abs_mult)
  1.2373 +    done
  1.2374 +  show ?thesis
  1.2375 +    apply (rule arctan_add_raw)
  1.2376 +    using * by linarith
  1.2377 +qed
  1.2378 +
  1.2379 +lemma abs_arctan_le:
  1.2380 +  fixes x::real shows "\<bar>arctan x\<bar> \<le> \<bar>x\<bar>"
  1.2381 +proof -
  1.2382 +  { fix w::complex and z::complex
  1.2383 +    assume *: "w \<in> \<real>" "z \<in> \<real>"
  1.2384 +    have "cmod (Arctan w - Arctan z) \<le> 1 * cmod (w-z)"
  1.2385 +      apply (rule field_differentiable_bound [OF convex_Reals, of Arctan _ 1])
  1.2386 +      apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan])
  1.2387 +      apply (force simp add: Reals_def)
  1.2388 +      apply (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square)
  1.2389 +      using * by auto
  1.2390 +  }
  1.2391 +  then have "cmod (Arctan (of_real x) - Arctan 0) \<le> 1 * cmod (of_real x -0)"
  1.2392 +    using Reals_0 Reals_of_real by blast
  1.2393 +  then show ?thesis
  1.2394 +    by (simp add: Arctan_of_real)
  1.2395 +qed
  1.2396 +
  1.2397 +lemma arctan_le_self: "0 \<le> x \<Longrightarrow> arctan x \<le> x"
  1.2398 +  by (metis abs_arctan_le abs_of_nonneg zero_le_arctan_iff)
  1.2399 +
  1.2400 +lemma abs_tan_ge: "\<bar>x\<bar> < pi/2 \<Longrightarrow> \<bar>x\<bar> \<le> \<bar>tan x\<bar>"
  1.2401 +  by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
  1.2402 +
  1.2403 +lemma arctan_bounds:
  1.2404 +  assumes "0 \<le> x" "x < 1"
  1.2405 +  shows arctan_lower_bound:
  1.2406 +    "(\<Sum>k<2 * n. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1))) \<le> arctan x"
  1.2407 +    (is "(\<Sum>k<_. (- 1)^ k * ?a k) \<le> _")
  1.2408 +    and arctan_upper_bound:
  1.2409 +    "arctan x \<le> (\<Sum>k<2 * n + 1. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1)))"
  1.2410 +proof -
  1.2411 +  have tendsto_zero: "?a \<longlonglongrightarrow> 0"
  1.2412 +    using assms
  1.2413 +    apply -
  1.2414 +    apply (rule tendsto_eq_rhs[where x="0 * 0"])
  1.2415 +    subgoal by (intro tendsto_mult real_tendsto_divide_at_top)
  1.2416 +        (auto simp: filterlim_real_sequentially filterlim_sequentially_iff_filterlim_real
  1.2417 +          intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially
  1.2418 +           tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top)
  1.2419 +    subgoal by simp
  1.2420 +    done
  1.2421 +  have nonneg: "0 \<le> ?a n" for n
  1.2422 +    by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms)
  1.2423 +  have le: "?a (Suc n) \<le> ?a n" for n
  1.2424 +    by (rule mult_mono[OF _ power_decreasing]) (auto simp: divide_simps assms less_imp_le)
  1.2425 +  from summable_Leibniz'(4)[of ?a, OF tendsto_zero nonneg le, of n]
  1.2426 +    summable_Leibniz'(2)[of ?a, OF tendsto_zero nonneg le, of n]
  1.2427 +    assms
  1.2428 +  show "(\<Sum>k<2*n. (- 1)^ k * ?a k) \<le> arctan x" "arctan x \<le> (\<Sum>k<2 * n + 1. (- 1)^ k * ?a k)"
  1.2429 +    by (auto simp: arctan_series)
  1.2430 +qed
  1.2431 +
  1.2432 +subsection \<open>Bounds on pi using real arctangent\<close>
  1.2433 +
  1.2434 +lemma pi_machin: "pi = 16 * arctan (1 / 5) - 4 * arctan (1 / 239)"
  1.2435 +  using machin
  1.2436 +  by simp
  1.2437 +
  1.2438 +lemma pi_approx: "3.141592653588 \<le> pi" "pi \<le> 3.1415926535899"
  1.2439 +  unfolding pi_machin
  1.2440 +  using arctan_bounds[of "1/5"   4]
  1.2441 +        arctan_bounds[of "1/239" 4]
  1.2442 +  by (simp_all add: eval_nat_numeral)
  1.2443 +
  1.2444 +
  1.2445 +subsection\<open>Inverse Sine\<close>
  1.2446 +
  1.2447 +definition Arcsin :: "complex \<Rightarrow> complex" where
  1.2448 +   "Arcsin \<equiv> \<lambda>z. -\<i> * Ln(\<i> * z + csqrt(1 - z\<^sup>2))"
  1.2449 +
  1.2450 +lemma Arcsin_body_lemma: "\<i> * z + csqrt(1 - z\<^sup>2) \<noteq> 0"
  1.2451 +  using power2_csqrt [of "1 - z\<^sup>2"]
  1.2452 +  apply auto
  1.2453 +  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)
  1.2454 +
  1.2455 +lemma Arcsin_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Re(\<i> * z + csqrt(1 - z\<^sup>2))"
  1.2456 +  using Complex.cmod_power2 [of z, symmetric]
  1.2457 +  by (simp add: real_less_rsqrt algebra_simps Re_power2 cmod_square_less_1_plus)
  1.2458 +
  1.2459 +lemma Re_Arcsin: "Re(Arcsin z) = Im (Ln (\<i> * z + csqrt(1 - z\<^sup>2)))"
  1.2460 +  by (simp add: Arcsin_def)
  1.2461 +
  1.2462 +lemma Im_Arcsin: "Im(Arcsin z) = - ln (cmod (\<i> * z + csqrt (1 - z\<^sup>2)))"
  1.2463 +  by (simp add: Arcsin_def Arcsin_body_lemma)
  1.2464 +
  1.2465 +lemma one_minus_z2_notin_nonpos_Reals:
  1.2466 +  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1.2467 +  shows "1 - z\<^sup>2 \<notin> \<real>\<^sub>\<le>\<^sub>0"
  1.2468 +    using assms
  1.2469 +    apply (auto simp: complex_nonpos_Reals_iff Re_power2 Im_power2)
  1.2470 +    using power2_less_0 [of "Im z"] apply force
  1.2471 +    using abs_square_less_1 not_le by blast
  1.2472 +
  1.2473 +lemma isCont_Arcsin_lemma:
  1.2474 +  assumes le0: "Re (\<i> * z + csqrt (1 - z\<^sup>2)) \<le> 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1.2475 +    shows False
  1.2476 +proof (cases "Im z = 0")
  1.2477 +  case True
  1.2478 +  then show ?thesis
  1.2479 +    using assms by (fastforce simp: cmod_def abs_square_less_1 [symmetric])
  1.2480 +next
  1.2481 +  case False
  1.2482 +  have neq: "(cmod z)\<^sup>2 \<noteq> 1 + cmod (1 - z\<^sup>2)"
  1.2483 +  proof (clarsimp simp add: cmod_def)
  1.2484 +    assume "(Re z)\<^sup>2 + (Im z)\<^sup>2 = 1 + sqrt ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
  1.2485 +    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)"
  1.2486 +      by simp
  1.2487 +    then show False using False
  1.2488 +      by (simp add: power2_eq_square algebra_simps)
  1.2489 +  qed
  1.2490 +  moreover have 2: "(Im z)\<^sup>2 = (1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2"
  1.2491 +    using le0
  1.2492 +    apply simp
  1.2493 +    apply (drule sqrt_le_D)
  1.2494 +    using cmod_power2 [of z] norm_triangle_ineq2 [of "z^2" 1]
  1.2495 +    apply (simp add: norm_power Re_power2 norm_minus_commute [of 1])
  1.2496 +    done
  1.2497 +  ultimately show False
  1.2498 +    by (simp add: Re_power2 Im_power2 cmod_power2)
  1.2499 +qed
  1.2500 +
  1.2501 +lemma isCont_Arcsin:
  1.2502 +  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1.2503 +    shows "isCont Arcsin z"
  1.2504 +proof -
  1.2505 +  have *: "\<i> * z + csqrt (1 - z\<^sup>2) \<notin> \<real>\<^sub>\<le>\<^sub>0"
  1.2506 +    by (metis isCont_Arcsin_lemma assms complex_nonpos_Reals_iff)
  1.2507 +  show ?thesis
  1.2508 +    using assms
  1.2509 +    apply (simp add: Arcsin_def)
  1.2510 +    apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
  1.2511 +    apply (simp add: one_minus_z2_notin_nonpos_Reals assms)
  1.2512 +    apply (rule *)
  1.2513 +    done
  1.2514 +qed
  1.2515 +
  1.2516 +lemma isCont_Arcsin' [simp]:
  1.2517 +  shows "isCont f z \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>x. Arcsin (f x)) z"
  1.2518 +  by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
  1.2519 +
  1.2520 +lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
  1.2521 +proof -
  1.2522 +  have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
  1.2523 +    by (simp add: algebra_simps)  \<comment>\<open>Cancelling a factor of 2\<close>
  1.2524 +  moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
  1.2525 +    by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral)
  1.2526 +  ultimately show ?thesis
  1.2527 +    apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps)
  1.2528 +    apply (simp add: algebra_simps)
  1.2529 +    apply (simp add: power2_eq_square [symmetric] algebra_simps)
  1.2530 +    done
  1.2531 +qed
  1.2532 +
  1.2533 +lemma Re_eq_pihalf_lemma:
  1.2534 +    "\<bar>Re z\<bar> = pi/2 \<Longrightarrow> Im z = 0 \<Longrightarrow>
  1.2535 +      Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2) = 0 \<and> 0 \<le> Im ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2)"
  1.2536 +  apply (simp add: cos_ii_times [symmetric] Re_cos Im_cos abs_if del: eq_divide_eq_numeral1)
  1.2537 +  by (metis cos_minus cos_pi_half)
  1.2538 +
  1.2539 +lemma Re_less_pihalf_lemma:
  1.2540 +  assumes "\<bar>Re z\<bar> < pi / 2"
  1.2541 +    shows "0 < Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2)"
  1.2542 +proof -
  1.2543 +  have "0 < cos (Re z)" using assms
  1.2544 +    using cos_gt_zero_pi by auto
  1.2545 +  then show ?thesis
  1.2546 +    by (simp add: cos_ii_times [symmetric] Re_cos Im_cos add_pos_pos)
  1.2547 +qed
  1.2548 +
  1.2549 +lemma Arcsin_sin:
  1.2550 +    assumes "\<bar>Re z\<bar> < pi/2 \<or> (\<bar>Re z\<bar> = pi/2 \<and> Im z = 0)"
  1.2551 +      shows "Arcsin(sin z) = z"
  1.2552 +proof -
  1.2553 +  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))"
  1.2554 +    by (simp add: sin_exp_eq Arcsin_def exp_minus power_divide)
  1.2555 +  also have "... = - (\<i> * Ln (csqrt (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2)\<^sup>2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
  1.2556 +    by (simp add: field_simps power2_eq_square)
  1.2557 +  also have "... = - (\<i> * Ln (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
  1.2558 +    apply (subst csqrt_square)
  1.2559 +    using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma
  1.2560 +    apply auto
  1.2561 +    done
  1.2562 +  also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
  1.2563 +    by (simp add: field_simps power2_eq_square)
  1.2564 +  also have "... = z"
  1.2565 +    apply (subst Complex_Transcendental.Ln_exp)
  1.2566 +    using assms
  1.2567 +    apply (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: if_split_asm)
  1.2568 +    done
  1.2569 +  finally show ?thesis .
  1.2570 +qed
  1.2571 +
  1.2572 +lemma Arcsin_unique:
  1.2573 +    "\<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"
  1.2574 +  by (metis Arcsin_sin)
  1.2575 +
  1.2576 +lemma Arcsin_0 [simp]: "Arcsin 0 = 0"
  1.2577 +  by (metis Arcsin_sin norm_zero pi_half_gt_zero real_norm_def sin_zero zero_complex.simps(1))
  1.2578 +
  1.2579 +lemma Arcsin_1 [simp]: "Arcsin 1 = pi/2"
  1.2580 +  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)
  1.2581 +
  1.2582 +lemma Arcsin_minus_1 [simp]: "Arcsin(-1) = - (pi/2)"
  1.2583 +  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)
  1.2584 +
  1.2585 +lemma has_field_derivative_Arcsin:
  1.2586 +  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1.2587 +    shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)"
  1.2588 +proof -
  1.2589 +  have "(sin (Arcsin z))\<^sup>2 \<noteq> 1"
  1.2590 +    using assms
  1.2591 +    apply atomize
  1.2592 +    apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
  1.2593 +    apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
  1.2594 +    by (metis abs_minus_cancel abs_one abs_power2 one_neq_neg_one)
  1.2595 +  then have "cos (Arcsin z) \<noteq> 0"
  1.2596 +    by (metis diff_0_right power_zero_numeral sin_squared_eq)
  1.2597 +  then show ?thesis
  1.2598 +    apply (rule has_complex_derivative_inverse_basic [OF DERIV_sin _ _ open_ball [of z 1]])
  1.2599 +    apply (auto intro: isCont_Arcsin assms)
  1.2600 +    done
  1.2601 +qed
  1.2602 +
  1.2603 +declare has_field_derivative_Arcsin [derivative_intros]
  1.2604 +declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
  1.2605 +
  1.2606 +lemma field_differentiable_at_Arcsin:
  1.2607 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin field_differentiable at z"
  1.2608 +  using field_differentiable_def has_field_derivative_Arcsin by blast
  1.2609 +
  1.2610 +lemma field_differentiable_within_Arcsin:
  1.2611 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin field_differentiable (at z within s)"
  1.2612 +  using field_differentiable_at_Arcsin field_differentiable_within_subset by blast
  1.2613 +
  1.2614 +lemma continuous_within_Arcsin:
  1.2615 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arcsin"
  1.2616 +  using continuous_at_imp_continuous_within isCont_Arcsin by blast
  1.2617 +
  1.2618 +lemma continuous_on_Arcsin [continuous_intros]:
  1.2619 +    "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous_on s Arcsin"
  1.2620 +  by (simp add: continuous_at_imp_continuous_on)
  1.2621 +
  1.2622 +lemma holomorphic_on_Arcsin: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin holomorphic_on s"
  1.2623 +  by (simp add: field_differentiable_within_Arcsin holomorphic_on_def)
  1.2624 +
  1.2625 +
  1.2626 +subsection\<open>Inverse Cosine\<close>
  1.2627 +
  1.2628 +definition Arccos :: "complex \<Rightarrow> complex" where
  1.2629 +   "Arccos \<equiv> \<lambda>z. -\<i> * Ln(z + \<i> * csqrt(1 - z\<^sup>2))"
  1.2630 +
  1.2631 +lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))"
  1.2632 +  using Arcsin_range_lemma [of "-z"]
  1.2633 +  by simp
  1.2634 +
  1.2635 +lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 0"
  1.2636 +  using Arcsin_body_lemma [of z]
  1.2637 +  by (metis complex_i_mult_minus diff_add_cancel minus_diff_eq minus_unique mult.assoc mult.left_commute
  1.2638 +           power2_csqrt power2_eq_square zero_neq_one)
  1.2639 +
  1.2640 +lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \<i> * csqrt(1 - z\<^sup>2)))"
  1.2641 +  by (simp add: Arccos_def)
  1.2642 +
  1.2643 +lemma Im_Arccos: "Im(Arccos z) = - ln (cmod (z + \<i> * csqrt (1 - z\<^sup>2)))"
  1.2644 +  by (simp add: Arccos_def Arccos_body_lemma)
  1.2645 +
  1.2646 +text\<open>A very tricky argument to find!\<close>
  1.2647 +lemma isCont_Arccos_lemma:
  1.2648 +  assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1.2649 +    shows False
  1.2650 +proof (cases "Im z = 0")
  1.2651 +  case True
  1.2652 +  then show ?thesis
  1.2653 +    using assms by (fastforce simp add: cmod_def abs_square_less_1 [symmetric])
  1.2654 +next
  1.2655 +  case False
  1.2656 +  have Imz: "Im z = - sqrt ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
  1.2657 +    using eq0 abs_Re_le_cmod [of "1-z\<^sup>2"]
  1.2658 +    by (simp add: Re_power2 algebra_simps)
  1.2659 +  have "(cmod z)\<^sup>2 - 1 \<noteq> cmod (1 - z\<^sup>2)"
  1.2660 +  proof (clarsimp simp add: cmod_def)
  1.2661 +    assume "(Re z)\<^sup>2 + (Im z)\<^sup>2 - 1 = sqrt ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
  1.2662 +    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)"
  1.2663 +      by simp
  1.2664 +    then show False using False
  1.2665 +      by (simp add: power2_eq_square algebra_simps)
  1.2666 +  qed
  1.2667 +  moreover have "(Im z)\<^sup>2 = ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
  1.2668 +    apply (subst Imz)
  1.2669 +    using abs_Re_le_cmod [of "1-z\<^sup>2"]
  1.2670 +    apply (simp add: Re_power2)
  1.2671 +    done
  1.2672 +  ultimately show False
  1.2673 +    by (simp add: cmod_power2)
  1.2674 +qed
  1.2675 +
  1.2676 +lemma isCont_Arccos:
  1.2677 +  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1.2678 +    shows "isCont Arccos z"
  1.2679 +proof -
  1.2680 +  have "z + \<i> * csqrt (1 - z\<^sup>2) \<notin> \<real>\<^sub>\<le>\<^sub>0"
  1.2681 +    by (metis complex_nonpos_Reals_iff isCont_Arccos_lemma assms)
  1.2682 +  with assms show ?thesis
  1.2683 +    apply (simp add: Arccos_def)
  1.2684 +    apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
  1.2685 +    apply (simp_all add: one_minus_z2_notin_nonpos_Reals assms)
  1.2686 +    done
  1.2687 +qed
  1.2688 +
  1.2689 +lemma isCont_Arccos' [simp]:
  1.2690 +  shows "isCont f z \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>x. Arccos (f x)) z"
  1.2691 +  by (blast intro: isCont_o2 [OF _ isCont_Arccos])
  1.2692 +
  1.2693 +lemma cos_Arccos [simp]: "cos(Arccos z) = z"
  1.2694 +proof -
  1.2695 +  have "z*2 + \<i> * (2 * csqrt (1 - z\<^sup>2)) = 0 \<longleftrightarrow> z*2 + \<i> * csqrt (1 - z\<^sup>2)*2 = 0"
  1.2696 +    by (simp add: algebra_simps)  \<comment>\<open>Cancelling a factor of 2\<close>
  1.2697 +  moreover have "... \<longleftrightarrow> z + \<i> * csqrt (1 - z\<^sup>2) = 0"
  1.2698 +    by (metis distrib_right mult_eq_0_iff zero_neq_numeral)
  1.2699 +  ultimately show ?thesis
  1.2700 +    apply (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps)
  1.2701 +    apply (simp add: power2_eq_square [symmetric])
  1.2702 +    done
  1.2703 +qed
  1.2704 +
  1.2705 +lemma Arccos_cos:
  1.2706 +    assumes "0 < Re z & Re z < pi \<or>
  1.2707 +             Re z = 0 & 0 \<le> Im z \<or>
  1.2708 +             Re z = pi & Im z \<le> 0"
  1.2709 +      shows "Arccos(cos z) = z"
  1.2710 +proof -
  1.2711 +  have *: "((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z))) = sin z"
  1.2712 +    by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square)
  1.2713 +  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"
  1.2714 +    by (simp add: field_simps power2_eq_square)
  1.2715 +  then have "Arccos(cos z) = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
  1.2716 +                           \<i> * csqrt (((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2)))"
  1.2717 +    by (simp add: cos_exp_eq Arccos_def exp_minus power_divide)
  1.2718 +  also have "... = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
  1.2719 +                              \<i> * ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))))"
  1.2720 +    apply (subst csqrt_square)
  1.2721 +    using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z]
  1.2722 +    apply (auto simp: * Re_sin Im_sin)
  1.2723 +    done
  1.2724 +  also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
  1.2725 +    by (simp add: field_simps power2_eq_square)
  1.2726 +  also have "... = z"
  1.2727 +    using assms
  1.2728 +    apply (subst Complex_Transcendental.Ln_exp, auto)
  1.2729 +    done
  1.2730 +  finally show ?thesis .
  1.2731 +qed
  1.2732 +
  1.2733 +lemma Arccos_unique:
  1.2734 +    "\<lbrakk>cos z = w;
  1.2735 +      0 < Re z \<and> Re z < pi \<or>
  1.2736 +      Re z = 0 \<and> 0 \<le> Im z \<or>
  1.2737 +      Re z = pi \<and> Im z \<le> 0\<rbrakk> \<Longrightarrow> Arccos w = z"
  1.2738 +  using Arccos_cos by blast
  1.2739 +
  1.2740 +lemma Arccos_0 [simp]: "Arccos 0 = pi/2"
  1.2741 +  by (rule Arccos_unique) (auto simp: of_real_numeral)
  1.2742 +
  1.2743 +lemma Arccos_1 [simp]: "Arccos 1 = 0"
  1.2744 +  by (rule Arccos_unique) auto
  1.2745 +
  1.2746 +lemma Arccos_minus1: "Arccos(-1) = pi"
  1.2747 +  by (rule Arccos_unique) auto
  1.2748 +
  1.2749 +lemma has_field_derivative_Arccos:
  1.2750 +  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1.2751 +    shows "(Arccos has_field_derivative - inverse(sin(Arccos z))) (at z)"
  1.2752 +proof -
  1.2753 +  have "(cos (Arccos z))\<^sup>2 \<noteq> 1"
  1.2754 +    using assms
  1.2755 +    apply atomize
  1.2756 +    apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
  1.2757 +    apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
  1.2758 +    apply (metis left_minus less_irrefl power_one sum_power2_gt_zero_iff zero_neq_neg_one)
  1.2759 +    done
  1.2760 +  then have "- sin (Arccos z) \<noteq> 0"
  1.2761 +    by (metis cos_squared_eq diff_0_right mult_zero_left neg_0_equal_iff_equal power2_eq_square)
  1.2762 +  then have "(Arccos has_field_derivative inverse(- sin(Arccos z))) (at z)"
  1.2763 +    apply (rule has_complex_derivative_inverse_basic [OF DERIV_cos _ _ open_ball [of z 1]])
  1.2764 +    apply (auto intro: isCont_Arccos assms)
  1.2765 +    done
  1.2766 +  then show ?thesis
  1.2767 +    by simp
  1.2768 +qed
  1.2769 +
  1.2770 +declare has_field_derivative_Arcsin [derivative_intros]
  1.2771 +declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
  1.2772 +
  1.2773 +lemma field_differentiable_at_Arccos:
  1.2774 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos field_differentiable at z"
  1.2775 +  using field_differentiable_def has_field_derivative_Arccos by blast
  1.2776 +
  1.2777 +lemma field_differentiable_within_Arccos:
  1.2778 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos field_differentiable (at z within s)"
  1.2779 +  using field_differentiable_at_Arccos field_differentiable_within_subset by blast
  1.2780 +
  1.2781 +lemma continuous_within_Arccos:
  1.2782 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arccos"
  1.2783 +  using continuous_at_imp_continuous_within isCont_Arccos by blast
  1.2784 +
  1.2785 +lemma continuous_on_Arccos [continuous_intros]:
  1.2786 +    "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous_on s Arccos"
  1.2787 +  by (simp add: continuous_at_imp_continuous_on)
  1.2788 +
  1.2789 +lemma holomorphic_on_Arccos: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos holomorphic_on s"
  1.2790 +  by (simp add: field_differentiable_within_Arccos holomorphic_on_def)
  1.2791 +
  1.2792 +
  1.2793 +subsection\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
  1.2794 +
  1.2795 +lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> \<bar>Re(Arcsin z)\<bar> < pi/2"
  1.2796 +  unfolding Re_Arcsin
  1.2797 +  by (blast intro: Re_Ln_pos_lt_imp Arcsin_range_lemma)
  1.2798 +
  1.2799 +lemma Arccos_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Re(Arccos z) \<and> Re(Arccos z) < pi"
  1.2800 +  unfolding Re_Arccos
  1.2801 +  by (blast intro!: Im_Ln_pos_lt_imp Arccos_range_lemma)
  1.2802 +
  1.2803 +lemma Re_Arccos_bounds: "-pi < Re(Arccos z) \<and> Re(Arccos z) \<le> pi"
  1.2804 +  unfolding Re_Arccos
  1.2805 +  by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arccos_body_lemma)
  1.2806 +
  1.2807 +lemma Re_Arccos_bound: "\<bar>Re(Arccos z)\<bar> \<le> pi"
  1.2808 +  by (meson Re_Arccos_bounds abs_le_iff less_eq_real_def minus_less_iff)
  1.2809 +
  1.2810 +lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
  1.2811 +  unfolding Re_Arcsin
  1.2812 +  by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
  1.2813 +
  1.2814 +lemma Re_Arcsin_bound: "\<bar>Re(Arcsin z)\<bar> \<le> pi"
  1.2815 +  by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
  1.2816 +
  1.2817 +
  1.2818 +subsection\<open>Interrelations between Arcsin and Arccos\<close>
  1.2819 +
  1.2820 +lemma cos_Arcsin_nonzero:
  1.2821 +  assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
  1.2822 +proof -
  1.2823 +  have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)"
  1.2824 +    by (simp add: power_mult_distrib algebra_simps)
  1.2825 +  have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> z\<^sup>2 - 1"
  1.2826 +  proof
  1.2827 +    assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1"
  1.2828 +    then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (z\<^sup>2 - 1)\<^sup>2"
  1.2829 +      by simp
  1.2830 +    then have "z\<^sup>2 * (z\<^sup>2 - 1) = (z\<^sup>2 - 1)*(z\<^sup>2 - 1)"
  1.2831 +      using eq power2_eq_square by auto
  1.2832 +    then show False
  1.2833 +      using assms by simp
  1.2834 +  qed
  1.2835 +  then have "1 + \<i> * z * (csqrt (1 - z * z)) \<noteq> z\<^sup>2"
  1.2836 +    by (metis add_minus_cancel power2_eq_square uminus_add_conv_diff)
  1.2837 +  then have "2*(1 + \<i> * z * (csqrt (1 - z * z))) \<noteq> 2*z\<^sup>2"  (*FIXME cancel_numeral_factor*)
  1.2838 +    by (metis mult_cancel_left zero_neq_numeral)
  1.2839 +  then have "(\<i> * z + csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> -1"
  1.2840 +    using assms
  1.2841 +    apply (auto simp: power2_sum)
  1.2842 +    apply (simp add: power2_eq_square algebra_simps)
  1.2843 +    done
  1.2844 +  then show ?thesis
  1.2845 +    apply (simp add: cos_exp_eq Arcsin_def exp_minus)
  1.2846 +    apply (simp add: divide_simps Arcsin_body_lemma)
  1.2847 +    apply (metis add.commute minus_unique power2_eq_square)
  1.2848 +    done
  1.2849 +qed
  1.2850 +
  1.2851 +lemma sin_Arccos_nonzero:
  1.2852 +  assumes "z\<^sup>2 \<noteq> 1" shows "sin(Arccos z) \<noteq> 0"
  1.2853 +proof -
  1.2854 +  have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)"
  1.2855 +    by (simp add: power_mult_distrib algebra_simps)
  1.2856 +  have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1 - z\<^sup>2"
  1.2857 +  proof
  1.2858 +    assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2"
  1.2859 +    then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (1 - z\<^sup>2)\<^sup>2"
  1.2860 +      by simp
  1.2861 +    then have "-(z\<^sup>2) * (1 - z\<^sup>2) = (1 - z\<^sup>2)*(1 - z\<^sup>2)"
  1.2862 +      using eq power2_eq_square by auto
  1.2863 +    then have "-(z\<^sup>2) = (1 - z\<^sup>2)"
  1.2864 +      using assms
  1.2865 +      by (metis add.commute add.right_neutral diff_add_cancel mult_right_cancel)
  1.2866 +    then show False
  1.2867 +      using assms by simp
  1.2868 +  qed
  1.2869 +  then have "z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1"
  1.2870 +    by (simp add: algebra_simps)
  1.2871 +  then have "2*(z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2))) \<noteq> 2*1"
  1.2872 +    by (metis mult_cancel_left2 zero_neq_numeral)  (*FIXME cancel_numeral_factor*)
  1.2873 +  then have "(z + \<i> * csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> 1"
  1.2874 +    using assms
  1.2875 +    apply (auto simp: Power.comm_semiring_1_class.power2_sum power_mult_distrib)
  1.2876 +    apply (simp add: power2_eq_square algebra_simps)
  1.2877 +    done
  1.2878 +  then show ?thesis
  1.2879 +    apply (simp add: sin_exp_eq Arccos_def exp_minus)
  1.2880 +    apply (simp add: divide_simps Arccos_body_lemma)
  1.2881 +    apply (simp add: power2_eq_square)
  1.2882 +    done
  1.2883 +qed
  1.2884 +
  1.2885 +lemma cos_sin_csqrt:
  1.2886 +  assumes "0 < cos(Re z)  \<or>  cos(Re z) = 0 \<and> Im z * sin(Re z) \<le> 0"
  1.2887 +    shows "cos z = csqrt(1 - (sin z)\<^sup>2)"
  1.2888 +  apply (rule csqrt_unique [THEN sym])
  1.2889 +  apply (simp add: cos_squared_eq)
  1.2890 +  using assms
  1.2891 +  apply (auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff)
  1.2892 +  done
  1.2893 +
  1.2894 +lemma sin_cos_csqrt:
  1.2895 +  assumes "0 < sin(Re z)  \<or>  sin(Re z) = 0 \<and> 0 \<le> Im z * cos(Re z)"
  1.2896 +    shows "sin z = csqrt(1 - (cos z)\<^sup>2)"
  1.2897 +  apply (rule csqrt_unique [THEN sym])
  1.2898 +  apply (simp add: sin_squared_eq)
  1.2899 +  using assms
  1.2900 +  apply (auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff)
  1.2901 +  done
  1.2902 +
  1.2903 +lemma Arcsin_Arccos_csqrt_pos:
  1.2904 +    "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arcsin z = Arccos(csqrt(1 - z\<^sup>2))"
  1.2905 +  by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
  1.2906 +
  1.2907 +lemma Arccos_Arcsin_csqrt_pos:
  1.2908 +    "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arccos z = Arcsin(csqrt(1 - z\<^sup>2))"
  1.2909 +  by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
  1.2910 +
  1.2911 +lemma sin_Arccos:
  1.2912 +    "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> sin(Arccos z) = csqrt(1 - z\<^sup>2)"
  1.2913 +  by (simp add: Arccos_Arcsin_csqrt_pos)
  1.2914 +
  1.2915 +lemma cos_Arcsin:
  1.2916 +    "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> cos(Arcsin z) = csqrt(1 - z\<^sup>2)"
  1.2917 +  by (simp add: Arcsin_Arccos_csqrt_pos)
  1.2918 +
  1.2919 +
  1.2920 +subsection\<open>Relationship with Arcsin on the Real Numbers\<close>
  1.2921 +
  1.2922 +lemma Im_Arcsin_of_real:
  1.2923 +  assumes "\<bar>x\<bar> \<le> 1"
  1.2924 +    shows "Im (Arcsin (of_real x)) = 0"
  1.2925 +proof -
  1.2926 +  have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
  1.2927 +    by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
  1.2928 +  then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
  1.2929 +    using assms abs_square_le_1
  1.2930 +    by (force simp add: Complex.cmod_power2)
  1.2931 +  then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2)) = 1"
  1.2932 +    by (simp add: norm_complex_def)
  1.2933 +  then show ?thesis
  1.2934 +    by (simp add: Im_Arcsin exp_minus)
  1.2935 +qed
  1.2936 +
  1.2937 +corollary Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
  1.2938 +  by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
  1.2939 +
  1.2940 +lemma arcsin_eq_Re_Arcsin:
  1.2941 +  assumes "\<bar>x\<bar> \<le> 1"
  1.2942 +    shows "arcsin x = Re (Arcsin (of_real x))"
  1.2943 +unfolding arcsin_def
  1.2944 +proof (rule the_equality, safe)
  1.2945 +  show "- (pi / 2) \<le> Re (Arcsin (complex_of_real x))"
  1.2946 +    using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
  1.2947 +    by (auto simp: Complex.in_Reals_norm Re_Arcsin)
  1.2948 +next
  1.2949 +  show "Re (Arcsin (complex_of_real x)) \<le> pi / 2"
  1.2950 +    using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
  1.2951 +    by (auto simp: Complex.in_Reals_norm Re_Arcsin)
  1.2952 +next
  1.2953 +  show "sin (Re (Arcsin (complex_of_real x))) = x"
  1.2954 +    using Re_sin [of "Arcsin (of_real x)"] Arcsin_body_lemma [of "of_real x"]
  1.2955 +    by (simp add: Im_Arcsin_of_real assms)
  1.2956 +next
  1.2957 +  fix x'
  1.2958 +  assume "- (pi / 2) \<le> x'" "x' \<le> pi / 2" "x = sin x'"
  1.2959 +  then show "x' = Re (Arcsin (complex_of_real (sin x')))"
  1.2960 +    apply (simp add: sin_of_real [symmetric])
  1.2961 +    apply (subst Arcsin_sin)
  1.2962 +    apply (auto simp: )
  1.2963 +    done
  1.2964 +qed
  1.2965 +
  1.2966 +lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
  1.2967 +  by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
  1.2968 +
  1.2969 +
  1.2970 +subsection\<open>Relationship with Arccos on the Real Numbers\<close>
  1.2971 +
  1.2972 +lemma Im_Arccos_of_real:
  1.2973 +  assumes "\<bar>x\<bar> \<le> 1"
  1.2974 +    shows "Im (Arccos (of_real x)) = 0"
  1.2975 +proof -
  1.2976 +  have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
  1.2977 +    by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
  1.2978 +  then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
  1.2979 +    using assms abs_square_le_1
  1.2980 +    by (force simp add: Complex.cmod_power2)
  1.2981 +  then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2)) = 1"
  1.2982 +    by (simp add: norm_complex_def)
  1.2983 +  then show ?thesis
  1.2984 +    by (simp add: Im_Arccos exp_minus)
  1.2985 +qed
  1.2986 +
  1.2987 +corollary Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
  1.2988 +  by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
  1.2989 +
  1.2990 +lemma arccos_eq_Re_Arccos:
  1.2991 +  assumes "\<bar>x\<bar> \<le> 1"
  1.2992 +    shows "arccos x = Re (Arccos (of_real x))"
  1.2993 +unfolding arccos_def
  1.2994 +proof (rule the_equality, safe)
  1.2995 +  show "0 \<le> Re (Arccos (complex_of_real x))"
  1.2996 +    using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
  1.2997 +    by (auto simp: Complex.in_Reals_norm Re_Arccos)
  1.2998 +next
  1.2999 +  show "Re (Arccos (complex_of_real x)) \<le> pi"
  1.3000 +    using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
  1.3001 +    by (auto simp: Complex.in_Reals_norm Re_Arccos)
  1.3002 +next
  1.3003 +  show "cos (Re (Arccos (complex_of_real x))) = x"
  1.3004 +    using Re_cos [of "Arccos (of_real x)"] Arccos_body_lemma [of "of_real x"]
  1.3005 +    by (simp add: Im_Arccos_of_real assms)
  1.3006 +next
  1.3007 +  fix x'
  1.3008 +  assume "0 \<le> x'" "x' \<le> pi" "x = cos x'"
  1.3009 +  then show "x' = Re (Arccos (complex_of_real (cos x')))"
  1.3010 +    apply (simp add: cos_of_real [symmetric])
  1.3011 +    apply (subst Arccos_cos)
  1.3012 +    apply (auto simp: )
  1.3013 +    done
  1.3014 +qed
  1.3015 +
  1.3016 +lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
  1.3017 +  by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
  1.3018 +
  1.3019 +subsection\<open>Some interrelationships among the real inverse trig functions.\<close>
  1.3020 +
  1.3021 +lemma arccos_arctan:
  1.3022 +  assumes "-1 < x" "x < 1"
  1.3023 +    shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))"
  1.3024 +proof -
  1.3025 +  have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0"
  1.3026 +  proof (rule sin_eq_0_pi)
  1.3027 +    show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)"
  1.3028 +      using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"]  arccos_bounded [of x] assms
  1.3029 +      by (simp add: algebra_simps)
  1.3030 +  next
  1.3031 +    show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi"
  1.3032 +      using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"]  arccos_bounded [of x] assms
  1.3033 +      by (simp add: algebra_simps)
  1.3034 +  next
  1.3035 +    show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0"
  1.3036 +      using assms
  1.3037 +      by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
  1.3038 +                    power2_eq_square square_eq_1_iff)
  1.3039 +  qed
  1.3040 +  then show ?thesis
  1.3041 +    by simp
  1.3042 +qed
  1.3043 +
  1.3044 +lemma arcsin_plus_arccos:
  1.3045 +  assumes "-1 \<le> x" "x \<le> 1"
  1.3046 +    shows "arcsin x + arccos x = pi/2"
  1.3047 +proof -
  1.3048 +  have "arcsin x = pi/2 - arccos x"
  1.3049 +    apply (rule sin_inj_pi)
  1.3050 +    using assms arcsin [OF assms] arccos [OF assms]
  1.3051 +    apply (auto simp: algebra_simps sin_diff)
  1.3052 +    done
  1.3053 +  then show ?thesis
  1.3054 +    by (simp add: algebra_simps)
  1.3055 +qed
  1.3056 +
  1.3057 +lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x"
  1.3058 +  using arcsin_plus_arccos by force
  1.3059 +
  1.3060 +lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x"
  1.3061 +  using arcsin_plus_arccos by force
  1.3062 +
  1.3063 +lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
  1.3064 +  by (simp add: arccos_arctan arcsin_arccos_eq)
  1.3065 +
  1.3066 +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))"
  1.3067 +  by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
  1.3068 +
  1.3069 +lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
  1.3070 +  apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
  1.3071 +  apply (subst Arcsin_Arccos_csqrt_pos)
  1.3072 +  apply (auto simp: power_le_one csqrt_1_diff_eq)
  1.3073 +  done
  1.3074 +
  1.3075 +lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
  1.3076 +  using arcsin_arccos_sqrt_pos [of "-x"]
  1.3077 +  by (simp add: arcsin_minus)
  1.3078 +
  1.3079 +lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
  1.3080 +  apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
  1.3081 +  apply (subst Arccos_Arcsin_csqrt_pos)
  1.3082 +  apply (auto simp: power_le_one csqrt_1_diff_eq)
  1.3083 +  done
  1.3084 +
  1.3085 +lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
  1.3086 +  using arccos_arcsin_sqrt_pos [of "-x"]
  1.3087 +  by (simp add: arccos_minus)
  1.3088 +
  1.3089 +subsection\<open>continuity results for arcsin and arccos.\<close>
  1.3090 +
  1.3091 +lemma continuous_on_Arcsin_real [continuous_intros]:
  1.3092 +    "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
  1.3093 +proof -
  1.3094 +  have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arcsin (Re x))) =
  1.3095 +        continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arcsin (of_real (Re x)))))"
  1.3096 +    by (rule continuous_on_cong [OF refl]) (simp add: arcsin_eq_Re_Arcsin)
  1.3097 +  also have "... = ?thesis"
  1.3098 +    by (rule continuous_on_cong [OF refl]) simp
  1.3099 +  finally show ?thesis
  1.3100 +    using continuous_on_arcsin [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
  1.3101 +          continuous_on_of_real
  1.3102 +    by fastforce
  1.3103 +qed
  1.3104 +
  1.3105 +lemma continuous_within_Arcsin_real:
  1.3106 +    "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arcsin"
  1.3107 +proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
  1.3108 +  case True then show ?thesis
  1.3109 +    using continuous_on_Arcsin_real continuous_on_eq_continuous_within
  1.3110 +    by blast
  1.3111 +next
  1.3112 +  case False
  1.3113 +  with closed_real_abs_le [of 1] show ?thesis
  1.3114 +    by (rule continuous_within_closed_nontrivial)
  1.3115 +qed
  1.3116 +
  1.3117 +lemma continuous_on_Arccos_real:
  1.3118 +    "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arccos"
  1.3119 +proof -
  1.3120 +  have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arccos (Re x))) =
  1.3121 +        continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arccos (of_real (Re x)))))"
  1.3122 +    by (rule continuous_on_cong [OF refl]) (simp add: arccos_eq_Re_Arccos)
  1.3123 +  also have "... = ?thesis"
  1.3124 +    by (rule continuous_on_cong [OF refl]) simp
  1.3125 +  finally show ?thesis
  1.3126 +    using continuous_on_arccos [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
  1.3127 +          continuous_on_of_real
  1.3128 +    by fastforce
  1.3129 +qed
  1.3130 +
  1.3131 +lemma continuous_within_Arccos_real:
  1.3132 +    "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arccos"
  1.3133 +proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
  1.3134 +  case True then show ?thesis
  1.3135 +    using continuous_on_Arccos_real continuous_on_eq_continuous_within
  1.3136 +    by blast
  1.3137 +next
  1.3138 +  case False
  1.3139 +  with closed_real_abs_le [of 1] show ?thesis
  1.3140 +    by (rule continuous_within_closed_nontrivial)
  1.3141 +qed
  1.3142 +
  1.3143 +
  1.3144 +subsection\<open>Roots of unity\<close>
  1.3145 +
  1.3146 +lemma complex_root_unity:
  1.3147 +  fixes j::nat
  1.3148 +  assumes "n \<noteq> 0"
  1.3149 +    shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
  1.3150 +proof -
  1.3151 +  have *: "of_nat j * (complex_of_real pi * 2) = complex_of_real (2 * real j * pi)"
  1.3152 +    by (simp add: of_real_numeral)
  1.3153 +  then show ?thesis
  1.3154 +    apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler)
  1.3155 +    apply (simp only: * cos_of_real sin_of_real)
  1.3156 +    apply (simp add: )
  1.3157 +    done
  1.3158 +qed
  1.3159 +
  1.3160 +lemma complex_root_unity_eq:
  1.3161 +  fixes j::nat and k::nat
  1.3162 +  assumes "1 \<le> n"
  1.3163 +    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)
  1.3164 +           \<longleftrightarrow> j mod n = k mod n)"
  1.3165 +proof -
  1.3166 +    have "(\<exists>z::int. \<i> * (of_nat j * (of_real pi * 2)) =
  1.3167 +               \<i> * (of_nat k * (of_real pi * 2)) + \<i> * (of_int z * (of_nat n * (of_real pi * 2)))) \<longleftrightarrow>
  1.3168 +          (\<exists>z::int. of_nat j * (\<i> * (of_real pi * 2)) =
  1.3169 +              (of_nat k + of_nat n * of_int z) * (\<i> * (of_real pi * 2)))"
  1.3170 +      by (simp add: algebra_simps)
  1.3171 +    also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))"
  1.3172 +      by simp
  1.3173 +    also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * z)"
  1.3174 +      apply (rule HOL.iff_exI)
  1.3175 +      apply (auto simp: )
  1.3176 +      using of_int_eq_iff apply fastforce
  1.3177 +      by (metis of_int_add of_int_mult of_int_of_nat_eq)
  1.3178 +    also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
  1.3179 +      by (auto simp: zmod_eq_dvd_iff dvd_def algebra_simps)
  1.3180 +    also have "... \<longleftrightarrow> j mod n = k mod n"
  1.3181 +      by (metis of_nat_eq_iff zmod_int)
  1.3182 +    finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =
  1.3183 +             \<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" .
  1.3184 +   note * = this
  1.3185 +  show ?thesis
  1.3186 +    using assms
  1.3187 +    by (simp add: exp_eq divide_simps mult_ac of_real_numeral *)
  1.3188 +qed
  1.3189 +
  1.3190 +corollary bij_betw_roots_unity:
  1.3191 +    "bij_betw (\<lambda>j. exp(2 * of_real pi * \<i> * of_nat j / of_nat n))
  1.3192 +              {..<n}  {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j. j < n}"
  1.3193 +  by (auto simp: bij_betw_def inj_on_def complex_root_unity_eq)
  1.3194 +
  1.3195 +lemma complex_root_unity_eq_1:
  1.3196 +  fixes j::nat and k::nat
  1.3197 +  assumes "1 \<le> n"
  1.3198 +    shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n) = 1 \<longleftrightarrow> n dvd j"
  1.3199 +proof -
  1.3200 +  have "1 = exp(2 * of_real pi * \<i> * (of_nat n / of_nat n))"
  1.3201 +    using assms by simp
  1.3202 +  then have "exp(2 * of_real pi * \<i> * (of_nat j / of_nat n)) = 1 \<longleftrightarrow> j mod n = n mod n"
  1.3203 +     using complex_root_unity_eq [of n j n] assms
  1.3204 +     by simp
  1.3205 +  then show ?thesis
  1.3206 +    by auto
  1.3207 +qed
  1.3208 +
  1.3209 +lemma finite_complex_roots_unity_explicit:
  1.3210 +     "finite {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
  1.3211 +by simp
  1.3212 +
  1.3213 +lemma card_complex_roots_unity_explicit:
  1.3214 +     "card {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n} = n"
  1.3215 +  by (simp add:  Finite_Set.bij_betw_same_card [OF bij_betw_roots_unity, symmetric])
  1.3216 +
  1.3217 +lemma complex_roots_unity:
  1.3218 +  assumes "1 \<le> n"
  1.3219 +    shows "{z::complex. z^n = 1} = {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
  1.3220 +  apply (rule Finite_Set.card_seteq [symmetric])
  1.3221 +  using assms
  1.3222 +  apply (auto simp: card_complex_roots_unity_explicit finite_roots_unity complex_root_unity card_roots_unity)
  1.3223 +  done
  1.3224 +
  1.3225 +lemma card_complex_roots_unity: "1 \<le> n \<Longrightarrow> card {z::complex. z^n = 1} = n"
  1.3226 +  by (simp add: card_complex_roots_unity_explicit complex_roots_unity)
  1.3227 +
  1.3228 +lemma complex_not_root_unity:
  1.3229 +    "1 \<le> n \<Longrightarrow> \<exists>u::complex. norm u = 1 \<and> u^n \<noteq> 1"
  1.3230 +  apply (rule_tac x="exp (of_real pi * \<i> * of_real (1 / n))" in exI)
  1.3231 +  apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
  1.3232 +  done
  1.3233 +
  1.3234 +end