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