src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
 author paulson Tue Mar 31 15:00:03 2015 +0100 (2015-03-31) changeset 59862 44b3f4fa33ca parent 59751 916c0f6c83e3 child 59870 68d6b6aa4450 permissions -rw-r--r--
New material and binomial fix
```     1 (*  Author: John Harrison
```
```     2     Ported from "hol_light/Multivariate/transcendentals.ml" by L C Paulson (2015)
```
```     3 *)
```
```     4
```
```     5 section {* Complex Transcendental Functions *}
```
```     6
```
```     7 theory Complex_Transcendental
```
```     8 imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
```
```     9 begin
```
```    10
```
```    11 subsection{*The Exponential Function is Differentiable and Continuous*}
```
```    12
```
```    13 lemma complex_differentiable_at_exp: "exp complex_differentiable at z"
```
```    14   using DERIV_exp complex_differentiable_def by blast
```
```    15
```
```    16 lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
```
```    17   by (simp add: complex_differentiable_at_exp complex_differentiable_at_within)
```
```    18
```
```    19 lemma continuous_within_exp:
```
```    20   fixes z::"'a::{real_normed_field,banach}"
```
```    21   shows "continuous (at z within s) exp"
```
```    22 by (simp add: continuous_at_imp_continuous_within)
```
```    23
```
```    24 lemma continuous_on_exp:
```
```    25   fixes s::"'a::{real_normed_field,banach} set"
```
```    26   shows "continuous_on s exp"
```
```    27 by (simp add: continuous_on_exp continuous_on_id)
```
```    28
```
```    29 lemma holomorphic_on_exp: "exp holomorphic_on s"
```
```    30   by (simp add: complex_differentiable_within_exp holomorphic_on_def)
```
```    31
```
```    32 subsection{*Euler and de Moivre formulas.*}
```
```    33
```
```    34 text{*The sine series times @{term i}*}
```
```    35 lemma sin_ii_eq: "(\<lambda>n. (ii * sin_coeff n) * z^n) sums (ii * sin z)"
```
```    36 proof -
```
```    37   have "(\<lambda>n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)"
```
```    38     using sin_converges sums_mult by blast
```
```    39   then show ?thesis
```
```    40     by (simp add: scaleR_conv_of_real field_simps)
```
```    41 qed
```
```    42
```
```    43 theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)"
```
```    44 proof -
```
```    45   have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n)
```
```    46         = (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))"
```
```    47   proof
```
```    48     fix n
```
```    49     show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)"
```
```    50       by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
```
```    51   qed
```
```    52   also have "... sums (exp (ii * z))"
```
```    53     by (rule exp_converges)
```
```    54   finally have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (exp (ii * z))" .
```
```    55   moreover have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (cos z + ii * sin z)"
```
```    56     using sums_add [OF cos_converges [of z] sin_ii_eq [of z]]
```
```    57     by (simp add: field_simps scaleR_conv_of_real)
```
```    58   ultimately show ?thesis
```
```    59     using sums_unique2 by blast
```
```    60 qed
```
```    61
```
```    62 corollary exp_minus_Euler: "exp(-(ii * z)) = cos(z) - ii * sin(z)"
```
```    63   using exp_Euler [of "-z"]
```
```    64   by simp
```
```    65
```
```    66 lemma sin_exp_eq: "sin z = (exp(ii * z) - exp(-(ii * z))) / (2*ii)"
```
```    67   by (simp add: exp_Euler exp_minus_Euler)
```
```    68
```
```    69 lemma sin_exp_eq': "sin z = ii * (exp(-(ii * z)) - exp(ii * z)) / 2"
```
```    70   by (simp add: exp_Euler exp_minus_Euler)
```
```    71
```
```    72 lemma cos_exp_eq:  "cos z = (exp(ii * z) + exp(-(ii * z))) / 2"
```
```    73   by (simp add: exp_Euler exp_minus_Euler)
```
```    74
```
```    75 subsection{*Relationships between real and complex trig functions*}
```
```    76
```
```    77 lemma real_sin_eq [simp]:
```
```    78   fixes x::real
```
```    79   shows "Re(sin(of_real x)) = sin x"
```
```    80   by (simp add: sin_of_real)
```
```    81
```
```    82 lemma real_cos_eq [simp]:
```
```    83   fixes x::real
```
```    84   shows "Re(cos(of_real x)) = cos x"
```
```    85   by (simp add: cos_of_real)
```
```    86
```
```    87 lemma DeMoivre: "(cos z + ii * sin z) ^ n = cos(n * z) + ii * sin(n * z)"
```
```    88   apply (simp add: exp_Euler [symmetric])
```
```    89   by (metis exp_of_nat_mult mult.left_commute)
```
```    90
```
```    91 lemma exp_cnj:
```
```    92   fixes z::complex
```
```    93   shows "cnj (exp z) = exp (cnj z)"
```
```    94 proof -
```
```    95   have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))"
```
```    96     by auto
```
```    97   also have "... sums (exp (cnj z))"
```
```    98     by (rule exp_converges)
```
```    99   finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
```
```   100   moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
```
```   101     by (metis exp_converges sums_cnj)
```
```   102   ultimately show ?thesis
```
```   103     using sums_unique2
```
```   104     by blast
```
```   105 qed
```
```   106
```
```   107 lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
```
```   108   by (simp add: sin_exp_eq exp_cnj field_simps)
```
```   109
```
```   110 lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
```
```   111   by (simp add: cos_exp_eq exp_cnj field_simps)
```
```   112
```
```   113 lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
```
```   114   using DERIV_sin complex_differentiable_def by blast
```
```   115
```
```   116 lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)"
```
```   117   by (simp add: complex_differentiable_at_sin complex_differentiable_at_within)
```
```   118
```
```   119 lemma complex_differentiable_at_cos: "cos complex_differentiable at z"
```
```   120   using DERIV_cos complex_differentiable_def by blast
```
```   121
```
```   122 lemma complex_differentiable_within_cos: "cos complex_differentiable (at z within s)"
```
```   123   by (simp add: complex_differentiable_at_cos complex_differentiable_at_within)
```
```   124
```
```   125 lemma holomorphic_on_sin: "sin holomorphic_on s"
```
```   126   by (simp add: complex_differentiable_within_sin holomorphic_on_def)
```
```   127
```
```   128 lemma holomorphic_on_cos: "cos holomorphic_on s"
```
```   129   by (simp add: complex_differentiable_within_cos holomorphic_on_def)
```
```   130
```
```   131 subsection{* Get a nice real/imaginary separation in Euler's formula.*}
```
```   132
```
```   133 lemma Euler: "exp(z) = of_real(exp(Re z)) *
```
```   134               (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
```
```   135 by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
```
```   136
```
```   137 lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
```
```   138   by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
```
```   139
```
```   140 lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
```
```   141   by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
```
```   142
```
```   143 lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
```
```   144   by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
```
```   145
```
```   146 lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
```
```   147   by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
```
```   148
```
```   149 lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
```
```   150   by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
```
```   151
```
```   152 lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
```
```   153   by (simp add: Re_sin Im_sin algebra_simps)
```
```   154
```
```   155 lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
```
```   156   by (simp add: Re_sin Im_sin algebra_simps)
```
```   157
```
```   158 subsection{*More on the Polar Representation of Complex Numbers*}
```
```   159
```
```   160 lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
```
```   161   by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
```
```   162
```
```   163 lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
```
```   164 apply auto
```
```   165 apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
```
```   166 apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1) real_of_int_def)
```
```   167 by (metis Im_exp Re_exp complex_Re_Im_cancel_iff cos_one_2pi_int sin_double Re_complex_of_real complex_Re_numeral exp_zero mult.assoc mult.left_commute mult_eq_0_iff mult_numeral_1 numeral_One of_real_0 real_of_int_def sin_zero_iff_int2)
```
```   168
```
```   169 lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * ii)"
```
```   170                 (is "?lhs = ?rhs")
```
```   171 proof -
```
```   172   have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
```
```   173     by (simp add: exp_diff)
```
```   174   also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
```
```   175     by (simp add: exp_eq_1)
```
```   176   also have "... \<longleftrightarrow> ?rhs"
```
```   177     by (auto simp: algebra_simps intro!: complex_eqI)
```
```   178   finally show ?thesis .
```
```   179 qed
```
```   180
```
```   181 lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
```
```   182   by (auto simp: exp_eq abs_mult)
```
```   183
```
```   184 lemma exp_integer_2pi:
```
```   185   assumes "n \<in> Ints"
```
```   186   shows "exp((2 * n * pi) * ii) = 1"
```
```   187 proof -
```
```   188   have "exp((2 * n * pi) * ii) = exp 0"
```
```   189     using assms
```
```   190     by (simp only: Ints_def exp_eq) auto
```
```   191   also have "... = 1"
```
```   192     by simp
```
```   193   finally show ?thesis .
```
```   194 qed
```
```   195
```
```   196 lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
```
```   197 proof -
```
```   198   { assume "sin y = sin x" "cos y = cos x"
```
```   199     then have "cos (y-x) = 1"
```
```   200       using cos_add [of y "-x"] by simp
```
```   201     then have "\<exists>n::int. y-x = real n * 2 * pi"
```
```   202       using cos_one_2pi_int by blast }
```
```   203   then show ?thesis
```
```   204   apply (auto simp: sin_add cos_add)
```
```   205   apply (metis add.commute diff_add_cancel mult.commute)
```
```   206   done
```
```   207 qed
```
```   208
```
```   209 lemma exp_i_ne_1:
```
```   210   assumes "0 < x" "x < 2*pi"
```
```   211   shows "exp(\<i> * of_real x) \<noteq> 1"
```
```   212 proof
```
```   213   assume "exp (\<i> * of_real x) = 1"
```
```   214   then have "exp (\<i> * of_real x) = exp 0"
```
```   215     by simp
```
```   216   then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
```
```   217     by (simp only: Ints_def exp_eq) auto
```
```   218   then have  "of_real x = (of_int (2 * n) * pi)"
```
```   219     by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
```
```   220   then have  "x = (of_int (2 * n) * pi)"
```
```   221     by simp
```
```   222   then show False using assms
```
```   223     by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
```
```   224 qed
```
```   225
```
```   226 lemma sin_eq_0:
```
```   227   fixes z::complex
```
```   228   shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
```
```   229   by (simp add: sin_exp_eq exp_eq of_real_numeral)
```
```   230
```
```   231 lemma cos_eq_0:
```
```   232   fixes z::complex
```
```   233   shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
```
```   234   using sin_eq_0 [of "z - of_real pi/2"]
```
```   235   by (simp add: sin_diff algebra_simps)
```
```   236
```
```   237 lemma cos_eq_1:
```
```   238   fixes z::complex
```
```   239   shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
```
```   240 proof -
```
```   241   have "cos z = cos (2*(z/2))"
```
```   242     by simp
```
```   243   also have "... = 1 - 2 * sin (z/2) ^ 2"
```
```   244     by (simp only: cos_double_sin)
```
```   245   finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
```
```   246     by simp
```
```   247   show ?thesis
```
```   248     by (auto simp: sin_eq_0 of_real_numeral)
```
```   249 qed
```
```   250
```
```   251 lemma csin_eq_1:
```
```   252   fixes z::complex
```
```   253   shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)"
```
```   254   using cos_eq_1 [of "z - of_real pi/2"]
```
```   255   by (simp add: cos_diff algebra_simps)
```
```   256
```
```   257 lemma csin_eq_minus1:
```
```   258   fixes z::complex
```
```   259   shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)"
```
```   260         (is "_ = ?rhs")
```
```   261 proof -
```
```   262   have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
```
```   263     by (simp add: equation_minus_iff)
```
```   264   also have "...  \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
```
```   265     by (simp only: csin_eq_1)
```
```   266   also have "...  \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
```
```   267     apply (rule iff_exI)
```
```   268     by (metis (no_types)  is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff)
```
```   269   also have "... = ?rhs"
```
```   270     apply (auto simp: of_real_numeral)
```
```   271     apply (rule_tac [2] x="-(x+1)" in exI)
```
```   272     apply (rule_tac x="-(x+1)" in exI)
```
```   273     apply (simp_all add: algebra_simps)
```
```   274     done
```
```   275   finally show ?thesis .
```
```   276 qed
```
```   277
```
```   278 lemma ccos_eq_minus1:
```
```   279   fixes z::complex
```
```   280   shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
```
```   281   using csin_eq_1 [of "z - of_real pi/2"]
```
```   282   apply (simp add: sin_diff)
```
```   283   apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
```
```   284   done
```
```   285
```
```   286 lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
```
```   287                 (is "_ = ?rhs")
```
```   288 proof -
```
```   289   have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
```
```   290     by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
```
```   291   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
```
```   292     by (simp only: csin_eq_1)
```
```   293   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
```
```   294     apply (rule iff_exI)
```
```   295     apply (auto simp: algebra_simps of_real_numeral)
```
```   296     apply (rule injD [OF inj_of_real [where 'a = complex]])
```
```   297     apply (auto simp: of_real_numeral)
```
```   298     done
```
```   299   also have "... = ?rhs"
```
```   300     by (auto simp: algebra_simps)
```
```   301   finally show ?thesis .
```
```   302 qed
```
```   303
```
```   304 lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
```
```   305 proof -
```
```   306   have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
```
```   307     by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
```
```   308   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
```
```   309     by (simp only: csin_eq_minus1)
```
```   310   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
```
```   311     apply (rule iff_exI)
```
```   312     apply (auto simp: algebra_simps)
```
```   313     apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
```
```   314     done
```
```   315   also have "... = ?rhs"
```
```   316     by (auto simp: algebra_simps)
```
```   317   finally show ?thesis .
```
```   318 qed
```
```   319
```
```   320 lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
```
```   321                       (is "_ = ?rhs")
```
```   322 proof -
```
```   323   have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
```
```   324     by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
```
```   325   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
```
```   326     by (simp only: ccos_eq_minus1)
```
```   327   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
```
```   328     apply (rule iff_exI)
```
```   329     apply (auto simp: algebra_simps)
```
```   330     apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
```
```   331     done
```
```   332   also have "... = ?rhs"
```
```   333     by (auto simp: algebra_simps)
```
```   334   finally show ?thesis .
```
```   335 qed
```
```   336
```
```   337 lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
```
```   338   apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
```
```   339   using cos_double_sin [of "t/2"]
```
```   340   apply (simp add: real_sqrt_mult)
```
```   341   done
```
```   342
```
```   343 lemma sinh_complex:
```
```   344   fixes z :: complex
```
```   345   shows "(exp z - inverse (exp z)) / 2 = -ii * sin(ii * z)"
```
```   346   by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
```
```   347
```
```   348 lemma sin_ii_times:
```
```   349   fixes z :: complex
```
```   350   shows "sin(ii * z) = ii * ((exp z - inverse (exp z)) / 2)"
```
```   351   using sinh_complex by auto
```
```   352
```
```   353 lemma sinh_real:
```
```   354   fixes x :: real
```
```   355   shows "of_real((exp x - inverse (exp x)) / 2) = -ii * sin(ii * of_real x)"
```
```   356   by (simp add: exp_of_real sin_ii_times of_real_numeral)
```
```   357
```
```   358 lemma cosh_complex:
```
```   359   fixes z :: complex
```
```   360   shows "(exp z + inverse (exp z)) / 2 = cos(ii * z)"
```
```   361   by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
```
```   362
```
```   363 lemma cosh_real:
```
```   364   fixes x :: real
```
```   365   shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)"
```
```   366   by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
```
```   367
```
```   368 lemmas cos_ii_times = cosh_complex [symmetric]
```
```   369
```
```   370 lemma norm_cos_squared:
```
```   371     "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
```
```   372   apply (cases z)
```
```   373   apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
```
```   374   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
```
```   375   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
```
```   376   apply (simp add: sin_squared_eq)
```
```   377   apply (simp add: power2_eq_square algebra_simps divide_simps)
```
```   378   done
```
```   379
```
```   380 lemma norm_sin_squared:
```
```   381     "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
```
```   382   apply (cases z)
```
```   383   apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
```
```   384   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
```
```   385   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
```
```   386   apply (simp add: cos_squared_eq)
```
```   387   apply (simp add: power2_eq_square algebra_simps divide_simps)
```
```   388   done
```
```   389
```
```   390 lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
```
```   391   using abs_Im_le_cmod linear order_trans by fastforce
```
```   392
```
```   393 lemma norm_cos_le:
```
```   394   fixes z::complex
```
```   395   shows "norm(cos z) \<le> exp(norm z)"
```
```   396 proof -
```
```   397   have "Im z \<le> cmod z"
```
```   398     using abs_Im_le_cmod abs_le_D1 by auto
```
```   399   with exp_uminus_Im show ?thesis
```
```   400     apply (simp add: cos_exp_eq norm_divide)
```
```   401     apply (rule order_trans [OF norm_triangle_ineq], simp)
```
```   402     apply (metis add_mono exp_le_cancel_iff mult_2_right)
```
```   403     done
```
```   404 qed
```
```   405
```
```   406 lemma norm_cos_plus1_le:
```
```   407   fixes z::complex
```
```   408   shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
```
```   409 proof -
```
```   410   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"
```
```   411       by arith
```
```   412   have *: "Im z \<le> cmod z"
```
```   413     using abs_Im_le_cmod abs_le_D1 by auto
```
```   414   have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)"
```
```   415     by (simp add: norm_add_rule_thm)
```
```   416   have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
```
```   417     by (simp add: cos_exp_eq)
```
```   418   also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
```
```   419     by (simp add: field_simps)
```
```   420   also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
```
```   421     by (simp add: norm_divide)
```
```   422   finally show ?thesis
```
```   423     apply (rule ssubst, simp)
```
```   424     apply (rule order_trans [OF triangle3], simp)
```
```   425     using exp_uminus_Im *
```
```   426     apply (auto intro: mono)
```
```   427     done
```
```   428 qed
```
```   429
```
```   430 subsection{* Taylor series for complex exponential, sine and cosine.*}
```
```   431
```
```   432 context
```
```   433 begin
```
```   434
```
```   435 declare power_Suc [simp del]
```
```   436
```
```   437 lemma Taylor_exp:
```
```   438   "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
```
```   439 proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
```
```   440   show "convex (closed_segment 0 z)"
```
```   441     by (rule convex_segment [of 0 z])
```
```   442 next
```
```   443   fix k x
```
```   444   assume "x \<in> closed_segment 0 z" "k \<le> n"
```
```   445   show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
```
```   446     using DERIV_exp DERIV_subset by blast
```
```   447 next
```
```   448   fix x
```
```   449   assume "x \<in> closed_segment 0 z"
```
```   450   then show "Re x \<le> \<bar>Re z\<bar>"
```
```   451     apply (auto simp: closed_segment_def scaleR_conv_of_real)
```
```   452     by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans)
```
```   453 next
```
```   454   show "0 \<in> closed_segment 0 z"
```
```   455     by (auto simp: closed_segment_def)
```
```   456 next
```
```   457   show "z \<in> closed_segment 0 z"
```
```   458     apply (simp add: closed_segment_def scaleR_conv_of_real)
```
```   459     using of_real_1 zero_le_one by blast
```
```   460 qed
```
```   461
```
```   462 lemma
```
```   463   assumes "0 \<le> u" "u \<le> 1"
```
```   464   shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
```
```   465     and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
```
```   466 proof -
```
```   467   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
```
```   468     by arith
```
```   469   show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
```
```   470     apply (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
```
```   471     apply (rule order_trans [OF norm_triangle_ineq4])
```
```   472     apply (rule mono)
```
```   473     apply (auto simp: abs_if mult_left_le_one_le)
```
```   474     apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
```
```   475     apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
```
```   476     done
```
```   477   show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
```
```   478     apply (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
```
```   479     apply (rule order_trans [OF norm_triangle_ineq])
```
```   480     apply (rule mono)
```
```   481     apply (auto simp: abs_if mult_left_le_one_le)
```
```   482     apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
```
```   483     apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
```
```   484     done
```
```   485 qed
```
```   486
```
```   487 lemma Taylor_sin:
```
```   488   "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
```
```   489    \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
```
```   490 proof -
```
```   491   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
```
```   492       by arith
```
```   493   have *: "cmod (sin z -
```
```   494                  (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
```
```   495            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
```
```   496   proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" "exp\<bar>Im z\<bar>" 0 z,
```
```   497 simplified])
```
```   498   show "convex (closed_segment 0 z)"
```
```   499     by (rule convex_segment [of 0 z])
```
```   500   next
```
```   501     fix k x
```
```   502     show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
```
```   503             (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
```
```   504             (at x within closed_segment 0 z)"
```
```   505       apply (auto simp: power_Suc)
```
```   506       apply (intro derivative_eq_intros | simp)+
```
```   507       done
```
```   508   next
```
```   509     fix x
```
```   510     assume "x \<in> closed_segment 0 z"
```
```   511     then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
```
```   512       by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
```
```   513   next
```
```   514     show "0 \<in> closed_segment 0 z"
```
```   515       by (auto simp: closed_segment_def)
```
```   516   next
```
```   517     show "z \<in> closed_segment 0 z"
```
```   518       apply (simp add: closed_segment_def scaleR_conv_of_real)
```
```   519       using of_real_1 zero_le_one by blast
```
```   520   qed
```
```   521   have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
```
```   522             = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
```
```   523     by (auto simp: sin_coeff_def elim!: oddE)
```
```   524   show ?thesis
```
```   525     apply (rule order_trans [OF _ *])
```
```   526     apply (simp add: **)
```
```   527     done
```
```   528 qed
```
```   529
```
```   530 lemma Taylor_cos:
```
```   531   "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k))
```
```   532    \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
```
```   533 proof -
```
```   534   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
```
```   535       by arith
```
```   536   have *: "cmod (cos z -
```
```   537                  (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
```
```   538            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
```
```   539   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,
```
```   540 simplified])
```
```   541   show "convex (closed_segment 0 z)"
```
```   542     by (rule convex_segment [of 0 z])
```
```   543   next
```
```   544     fix k x
```
```   545     assume "x \<in> closed_segment 0 z" "k \<le> n"
```
```   546     show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
```
```   547             (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
```
```   548              (at x within closed_segment 0 z)"
```
```   549       apply (auto simp: power_Suc)
```
```   550       apply (intro derivative_eq_intros | simp)+
```
```   551       done
```
```   552   next
```
```   553     fix x
```
```   554     assume "x \<in> closed_segment 0 z"
```
```   555     then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
```
```   556       by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
```
```   557   next
```
```   558     show "0 \<in> closed_segment 0 z"
```
```   559       by (auto simp: closed_segment_def)
```
```   560   next
```
```   561     show "z \<in> closed_segment 0 z"
```
```   562       apply (simp add: closed_segment_def scaleR_conv_of_real)
```
```   563       using of_real_1 zero_le_one by blast
```
```   564   qed
```
```   565   have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
```
```   566             = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
```
```   567     by (auto simp: cos_coeff_def elim!: evenE)
```
```   568   show ?thesis
```
```   569     apply (rule order_trans [OF _ *])
```
```   570     apply (simp add: **)
```
```   571     done
```
```   572 qed
```
```   573
```
```   574 end (* of context *)
```
```   575
```
```   576 text{*32-bit Approximation to e*}
```
```   577 lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
```
```   578   using Taylor_exp [of 1 14] exp_le
```
```   579   apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
```
```   580   apply (simp only: pos_le_divide_eq [symmetric], linarith)
```
```   581   done
```
```   582
```
```   583 subsection{*The argument of a complex number*}
```
```   584
```
```   585 definition Arg :: "complex \<Rightarrow> real" where
```
```   586  "Arg z \<equiv> if z = 0 then 0
```
```   587            else THE t. 0 \<le> t \<and> t < 2*pi \<and>
```
```   588                     z = of_real(norm z) * exp(ii * of_real t)"
```
```   589
```
```   590 lemma Arg_0 [simp]: "Arg(0) = 0"
```
```   591   by (simp add: Arg_def)
```
```   592
```
```   593 lemma Arg_unique_lemma:
```
```   594   assumes z:  "z = of_real(norm z) * exp(ii * of_real t)"
```
```   595       and z': "z = of_real(norm z) * exp(ii * of_real t')"
```
```   596       and t:  "0 \<le> t"  "t < 2*pi"
```
```   597       and t': "0 \<le> t'" "t' < 2*pi"
```
```   598       and nz: "z \<noteq> 0"
```
```   599   shows "t' = t"
```
```   600 proof -
```
```   601   have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
```
```   602     by arith
```
```   603   have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
```
```   604     by (metis z z')
```
```   605   then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
```
```   606     by (metis nz mult_left_cancel mult_zero_left z)
```
```   607   then have "sin t' = sin t \<and> cos t' = cos t"
```
```   608     apply (simp add: exp_Euler sin_of_real cos_of_real)
```
```   609     by (metis Complex_eq complex.sel)
```
```   610   then obtain n::int where n: "t' = t + 2 * real n * pi"
```
```   611     by (auto simp: sin_cos_eq_iff)
```
```   612   then have "n=0"
```
```   613     apply (rule_tac z=n in int_cases)
```
```   614     using t t'
```
```   615     apply (auto simp: mult_less_0_iff algebra_simps)
```
```   616     done
```
```   617   then show "t' = t"
```
```   618       by (simp add: n)
```
```   619 qed
```
```   620
```
```   621 lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(ii * of_real(Arg z))"
```
```   622 proof (cases "z=0")
```
```   623   case True then show ?thesis
```
```   624     by (simp add: Arg_def)
```
```   625 next
```
```   626   case False
```
```   627   obtain t where t: "0 \<le> t" "t < 2*pi"
```
```   628              and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
```
```   629     using sincos_total_2pi [OF complex_unit_circle [OF False]]
```
```   630     by blast
```
```   631   have z: "z = of_real(norm z) * exp(ii * of_real t)"
```
```   632     apply (rule complex_eqI)
```
```   633     using t False ReIm
```
```   634     apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
```
```   635     done
```
```   636   show ?thesis
```
```   637     apply (simp add: Arg_def False)
```
```   638     apply (rule theI [where a=t])
```
```   639     using t z False
```
```   640     apply (auto intro: Arg_unique_lemma)
```
```   641     done
```
```   642 qed
```
```   643
```
```   644
```
```   645 corollary
```
```   646   shows Arg_ge_0: "0 \<le> Arg z"
```
```   647     and Arg_lt_2pi: "Arg z < 2*pi"
```
```   648     and Arg_eq: "z = of_real(norm z) * exp(ii * of_real(Arg z))"
```
```   649   using Arg by auto
```
```   650
```
```   651 lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(ii * of_real t))"
```
```   652   using Arg [of z] by auto
```
```   653
```
```   654 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"
```
```   655   apply (rule Arg_unique_lemma [OF _ Arg_eq])
```
```   656   using Arg [of z]
```
```   657   apply (auto simp: norm_mult)
```
```   658   done
```
```   659
```
```   660 lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
```
```   661   apply (rule Arg_unique [of "norm z"])
```
```   662   apply (rule complex_eqI)
```
```   663   using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] Arg_eq [of z]
```
```   664   apply auto
```
```   665   apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
```
```   666   apply (metis Re_rcis Im_rcis rcis_def)+
```
```   667   done
```
```   668
```
```   669 lemma Arg_times_of_real [simp]: "0 < r \<Longrightarrow> Arg (of_real r * z) = Arg z"
```
```   670   apply (cases "z=0", simp)
```
```   671   apply (rule Arg_unique [of "r * norm z"])
```
```   672   using Arg
```
```   673   apply auto
```
```   674   done
```
```   675
```
```   676 lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
```
```   677   by (metis Arg_times_of_real mult.commute)
```
```   678
```
```   679 lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
```
```   680   by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
```
```   681
```
```   682 lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
```
```   683 proof (cases "z=0")
```
```   684   case True then show ?thesis
```
```   685     by simp
```
```   686 next
```
```   687   case False
```
```   688   have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
```
```   689     by (metis Arg_eq)
```
```   690   also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
```
```   691     using False
```
```   692     by (simp add: zero_le_mult_iff)
```
```   693   also have "... \<longleftrightarrow> Arg z \<le> pi"
```
```   694     by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
```
```   695   finally show ?thesis
```
```   696     by blast
```
```   697 qed
```
```   698
```
```   699 lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
```
```   700 proof (cases "z=0")
```
```   701   case True then show ?thesis
```
```   702     by simp
```
```   703 next
```
```   704   case False
```
```   705   have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
```
```   706     by (metis Arg_eq)
```
```   707   also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
```
```   708     using False
```
```   709     by (simp add: zero_less_mult_iff)
```
```   710   also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
```
```   711     using Arg_ge_0  Arg_lt_2pi sin_le_zero sin_gt_zero
```
```   712     apply (auto simp: Im_exp)
```
```   713     using le_less apply fastforce
```
```   714     using not_le by blast
```
```   715   finally show ?thesis
```
```   716     by blast
```
```   717 qed
```
```   718
```
```   719 lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
```
```   720 proof (cases "z=0")
```
```   721   case True then show ?thesis
```
```   722     by simp
```
```   723 next
```
```   724   case False
```
```   725   have "z \<in> Reals \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
```
```   726     by (metis Arg_eq)
```
```   727   also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
```
```   728     using False
```
```   729     by (simp add: zero_le_mult_iff)
```
```   730   also have "... \<longleftrightarrow> Arg z = 0"
```
```   731     apply (auto simp: Re_exp)
```
```   732     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)
```
```   733     using Arg_eq [of z]
```
```   734     apply (auto simp: Reals_def)
```
```   735     done
```
```   736   finally show ?thesis
```
```   737     by blast
```
```   738 qed
```
```   739
```
```   740 lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
```
```   741   by (simp add: Arg_eq_0)
```
```   742
```
```   743 lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
```
```   744   apply  (cases "z=0", simp)
```
```   745   using Arg_eq_0 [of "-z"]
```
```   746   apply (auto simp: complex_is_Real_iff Arg_minus)
```
```   747   apply (simp add: complex_Re_Im_cancel_iff)
```
```   748   apply (metis Arg_minus pi_gt_zero add.left_neutral minus_minus minus_zero)
```
```   749   done
```
```   750
```
```   751 lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
```
```   752   using Arg_eq_0 Arg_eq_pi not_le by auto
```
```   753
```
```   754 lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
```
```   755   apply (cases "z=0", simp)
```
```   756   apply (rule Arg_unique [of "inverse (norm z)"])
```
```   757   using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] Exp_two_pi_i
```
```   758   apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
```
```   759   done
```
```   760
```
```   761 lemma Arg_eq_iff:
```
```   762   assumes "w \<noteq> 0" "z \<noteq> 0"
```
```   763      shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
```
```   764   using assms Arg_eq [of z] Arg_eq [of w]
```
```   765   apply auto
```
```   766   apply (rule_tac x="norm w / norm z" in exI)
```
```   767   apply (simp add: divide_simps)
```
```   768   by (metis mult.commute mult.left_commute)
```
```   769
```
```   770 lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
```
```   771   using complex_is_Real_iff
```
```   772   apply (simp add: Arg_eq_0)
```
```   773   apply (auto simp: divide_simps not_sum_power2_lt_zero)
```
```   774   done
```
```   775
```
```   776 lemma Arg_divide:
```
```   777   assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
```
```   778     shows "Arg(z / w) = Arg z - Arg w"
```
```   779   apply (rule Arg_unique [of "norm(z / w)"])
```
```   780   using assms Arg_eq [of z] Arg_eq [of w] Arg_ge_0 [of w] Arg_lt_2pi [of z]
```
```   781   apply (auto simp: exp_diff norm_divide algebra_simps divide_simps)
```
```   782   done
```
```   783
```
```   784 lemma Arg_le_div_sum:
```
```   785   assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
```
```   786     shows "Arg z = Arg w + Arg(z / w)"
```
```   787   by (simp add: Arg_divide assms)
```
```   788
```
```   789 lemma Arg_le_div_sum_eq:
```
```   790   assumes "w \<noteq> 0" "z \<noteq> 0"
```
```   791     shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
```
```   792   using assms
```
```   793   by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
```
```   794
```
```   795 lemma Arg_diff:
```
```   796   assumes "w \<noteq> 0" "z \<noteq> 0"
```
```   797     shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
```
```   798   using assms
```
```   799   apply (auto simp: Arg_ge_0 Arg_divide not_le)
```
```   800   using Arg_divide [of w z] Arg_inverse [of "w/z"]
```
```   801   apply auto
```
```   802   by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
```
```   803
```
```   804 lemma Arg_add:
```
```   805   assumes "w \<noteq> 0" "z \<noteq> 0"
```
```   806     shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
```
```   807   using assms
```
```   808   using Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
```
```   809   apply (auto simp: Arg_ge_0 Arg_divide not_le)
```
```   810   apply (metis Arg_lt_2pi add.commute)
```
```   811   apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
```
```   812   done
```
```   813
```
```   814 lemma Arg_times:
```
```   815   assumes "w \<noteq> 0" "z \<noteq> 0"
```
```   816     shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
```
```   817                             else (Arg w + Arg z) - 2*pi)"
```
```   818   using Arg_add [OF assms]
```
```   819   by auto
```
```   820
```
```   821 lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
```
```   822   apply (cases "z=0", simp)
```
```   823   apply (rule trans [of _ "Arg(inverse z)"])
```
```   824   apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
```
```   825   apply (metis norm_eq_zero of_real_power zero_less_power2)
```
```   826   apply (auto simp: of_real_numeral Arg_inverse)
```
```   827   done
```
```   828
```
```   829 lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
```
```   830   using Arg_eq_0 Arg_eq_0_pi
```
```   831   by auto
```
```   832
```
```   833 lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
```
```   834   by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
```
```   835
```
```   836
```
```   837 subsection{*Analytic properties of tangent function*}
```
```   838
```
```   839 lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
```
```   840   by (simp add: cnj_cos cnj_sin tan_def)
```
```   841
```
```   842 lemma complex_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan complex_differentiable at z"
```
```   843   unfolding complex_differentiable_def
```
```   844   using DERIV_tan by blast
```
```   845
```
```   846 lemma complex_differentiable_within_tan: "~(cos z = 0)
```
```   847          \<Longrightarrow> tan complex_differentiable (at z within s)"
```
```   848   using complex_differentiable_at_tan complex_differentiable_at_within by blast
```
```   849
```
```   850 lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
```
```   851   using continuous_at_imp_continuous_within isCont_tan by blast
```
```   852
```
```   853 lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan"
```
```   854   by (simp add: continuous_at_imp_continuous_on)
```
```   855
```
```   856 lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
```
```   857   by (simp add: complex_differentiable_within_tan holomorphic_on_def)
```
```   858
```
```   859
```
```   860 subsection{*Complex logarithms (the conventional principal value)*}
```
```   861
```
```   862 definition Ln where
```
```   863    "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
```
```   864
```
```   865 lemma
```
```   866   assumes "z \<noteq> 0"
```
```   867     shows exp_Ln [simp]: "exp(Ln z) = z"
```
```   868       and mpi_less_Im_Ln: "-pi < Im(Ln z)"
```
```   869       and Im_Ln_le_pi:    "Im(Ln z) \<le> pi"
```
```   870 proof -
```
```   871   obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
```
```   872     using complex_unimodular_polar [of "z / (norm z)"] assms
```
```   873     by (auto simp: norm_divide divide_simps)
```
```   874   obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
```
```   875     using sincos_principal_value [of "\<psi>"] assms
```
```   876     by (auto simp: norm_divide divide_simps)
```
```   877   have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def
```
```   878     apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
```
```   879     using z assms \<phi>
```
```   880     apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
```
```   881     done
```
```   882   then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi"
```
```   883     by auto
```
```   884 qed
```
```   885
```
```   886 lemma Ln_exp [simp]:
```
```   887   assumes "-pi < Im(z)" "Im(z) \<le> pi"
```
```   888     shows "Ln(exp z) = z"
```
```   889   apply (rule exp_complex_eqI)
```
```   890   using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
```
```   891   apply auto
```
```   892   done
```
```   893
```
```   894 lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
```
```   895   by (metis exp_Ln)
```
```   896
```
```   897 lemma Ln_unique: "exp(z) = w \<Longrightarrow> -pi < Im(z) \<Longrightarrow> Im(z) \<le> pi \<Longrightarrow> Ln w = z"
```
```   898   using Ln_exp by blast
```
```   899
```
```   900 lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
```
```   901 by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
```
```   902
```
```   903 lemma exists_complex_root:
```
```   904   fixes a :: complex
```
```   905   shows "n \<noteq> 0 \<Longrightarrow> \<exists>z. z ^ n = a"
```
```   906   apply (cases "a=0", simp)
```
```   907   apply (rule_tac x= "exp(Ln(a) / n)" in exI)
```
```   908   apply (auto simp: exp_of_nat_mult [symmetric])
```
```   909   done
```
```   910
```
```   911 subsection{*The Unwinding Number and the Ln-product Formula*}
```
```   912
```
```   913 text{*Note that in this special case the unwinding number is -1, 0 or 1.*}
```
```   914
```
```   915 definition unwinding :: "complex \<Rightarrow> complex" where
```
```   916    "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * ii)"
```
```   917
```
```   918 lemma unwinding_2pi: "(2*pi) * ii * unwinding(z) = z - Ln(exp z)"
```
```   919   by (simp add: unwinding_def)
```
```   920
```
```   921 lemma Ln_times_unwinding:
```
```   922     "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * ii * unwinding(Ln w + Ln z)"
```
```   923   using unwinding_2pi by (simp add: exp_add)
```
```   924
```
```   925
```
```   926 subsection{*Derivative of Ln away from the branch cut*}
```
```   927
```
```   928 lemma
```
```   929   assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)"
```
```   930     shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
```
```   931       and Im_Ln_less_pi:           "Im (Ln z) < pi"
```
```   932 proof -
```
```   933   have znz: "z \<noteq> 0"
```
```   934     using assms by auto
```
```   935   then show *: "Im (Ln z) < pi" using assms
```
```   936     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)
```
```   937   show "(Ln has_field_derivative inverse(z)) (at z)"
```
```   938     apply (rule has_complex_derivative_inverse_strong_x
```
```   939               [where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"])
```
```   940     using znz *
```
```   941     apply (auto simp: continuous_on_exp open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
```
```   942     apply (metis DERIV_exp exp_Ln)
```
```   943     apply (metis mpi_less_Im_Ln)
```
```   944     done
```
```   945 qed
```
```   946
```
```   947 declare has_field_derivative_Ln [derivative_intros]
```
```   948 declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
```
```   949
```
```   950 lemma complex_differentiable_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln complex_differentiable at z"
```
```   951   using complex_differentiable_def has_field_derivative_Ln by blast
```
```   952
```
```   953 lemma complex_differentiable_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z))
```
```   954          \<Longrightarrow> Ln complex_differentiable (at z within s)"
```
```   955   using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
```
```   956
```
```   957 lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
```
```   958   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
```
```   959
```
```   960 lemma isCont_Ln' [simp]:
```
```   961    "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
```
```   962   by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
```
```   963
```
```   964 lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
```
```   965   using continuous_at_Ln continuous_at_imp_continuous_within by blast
```
```   966
```
```   967 lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s Ln"
```
```   968   by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
```
```   969
```
```   970 lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln holomorphic_on s"
```
```   971   by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
```
```   972
```
```   973
```
```   974 subsection{*Relation to Real Logarithm*}
```
```   975
```
```   976 lemma Ln_of_real:
```
```   977   assumes "0 < z"
```
```   978     shows "Ln(of_real z) = of_real(ln z)"
```
```   979 proof -
```
```   980   have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
```
```   981     by (simp add: exp_of_real)
```
```   982   also have "... = of_real(ln z)"
```
```   983     using assms
```
```   984     by (subst Ln_exp) auto
```
```   985   finally show ?thesis
```
```   986     using assms by simp
```
```   987 qed
```
```   988
```
```   989 corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> Ln z \<in> \<real>"
```
```   990   by (auto simp: Ln_of_real elim: Reals_cases)
```
```   991
```
```   992
```
```   993 subsection{*Quadrant-type results for Ln*}
```
```   994
```
```   995 lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
```
```   996   using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
```
```   997   by simp
```
```   998
```
```   999 lemma Re_Ln_pos_lt:
```
```  1000   assumes "z \<noteq> 0"
```
```  1001     shows "abs(Im(Ln z)) < pi/2 \<longleftrightarrow> 0 < Re(z)"
```
```  1002 proof -
```
```  1003   { fix w
```
```  1004     assume "w = Ln z"
```
```  1005     then have w: "Im w \<le> pi" "- pi < Im w"
```
```  1006       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
```
```  1007       by auto
```
```  1008     then have "abs(Im w) < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
```
```  1009       apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
```
```  1010       using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
```
```  1011       apply (simp add: abs_if split: split_if_asm)
```
```  1012       apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4)
```
```  1013                less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right
```
```  1014                mult_numeral_1_right)
```
```  1015       done
```
```  1016   }
```
```  1017   then show ?thesis using assms
```
```  1018     by auto
```
```  1019 qed
```
```  1020
```
```  1021 lemma Re_Ln_pos_le:
```
```  1022   assumes "z \<noteq> 0"
```
```  1023     shows "abs(Im(Ln z)) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
```
```  1024 proof -
```
```  1025   { fix w
```
```  1026     assume "w = Ln z"
```
```  1027     then have w: "Im w \<le> pi" "- pi < Im w"
```
```  1028       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
```
```  1029       by auto
```
```  1030     then have "abs(Im w) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
```
```  1031       apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
```
```  1032       using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
```
```  1033       apply (auto simp: abs_if split: split_if_asm)
```
```  1034       done
```
```  1035   }
```
```  1036   then show ?thesis using assms
```
```  1037     by auto
```
```  1038 qed
```
```  1039
```
```  1040 lemma Im_Ln_pos_lt:
```
```  1041   assumes "z \<noteq> 0"
```
```  1042     shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
```
```  1043 proof -
```
```  1044   { fix w
```
```  1045     assume "w = Ln z"
```
```  1046     then have w: "Im w \<le> pi" "- pi < Im w"
```
```  1047       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
```
```  1048       by auto
```
```  1049     then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)"
```
```  1050       using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"]
```
```  1051       apply (auto simp: Im_exp zero_less_mult_iff)
```
```  1052       using less_linear apply fastforce
```
```  1053       using less_linear apply fastforce
```
```  1054       done
```
```  1055   }
```
```  1056   then show ?thesis using assms
```
```  1057     by auto
```
```  1058 qed
```
```  1059
```
```  1060 lemma Im_Ln_pos_le:
```
```  1061   assumes "z \<noteq> 0"
```
```  1062     shows "0 \<le> Im(Ln z) \<and> Im(Ln z) \<le> pi \<longleftrightarrow> 0 \<le> Im(z)"
```
```  1063 proof -
```
```  1064   { fix w
```
```  1065     assume "w = Ln z"
```
```  1066     then have w: "Im w \<le> pi" "- pi < Im w"
```
```  1067       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
```
```  1068       by auto
```
```  1069     then have "0 \<le> Im w \<and> Im w \<le> pi \<longleftrightarrow> 0 \<le> Im(exp w)"
```
```  1070       using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"]
```
```  1071       apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero)
```
```  1072       apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi)
```
```  1073       done }
```
```  1074   then show ?thesis using assms
```
```  1075     by auto
```
```  1076 qed
```
```  1077
```
```  1078 lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> abs(Im(Ln z)) < pi/2"
```
```  1079   by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
```
```  1080
```
```  1081 lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
```
```  1082   by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))
```
```  1083
```
```  1084 lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
```
```  1085   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
```
```  1086        complex_eq exp_of_real le_less mult_zero_right norm_exp_eq_Re norm_le_zero_iff not_le of_real_0)
```
```  1087
```
```  1088 lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
```
```  1089   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)
```
```  1090
```
```  1091
```
```  1092 subsection{*More Properties of Ln*}
```
```  1093
```
```  1094 lemma cnj_Ln: "(Im z = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
```
```  1095   apply (cases "z=0", auto)
```
```  1096   apply (rule exp_complex_eqI)
```
```  1097   apply (auto simp: abs_if split: split_if_asm)
```
```  1098   apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps(1) cnj.simps(2) mult_2 neg_equal_0_iff_equal)
```
```  1099   apply (metis add_mono_thms_linordered_field(5) complex_cnj_zero_iff diff_0_right diff_minus_eq_add minus_diff_eq mpi_less_Im_Ln mult.commute mult_2_right neg_less_iff_less)
```
```  1100   by (metis exp_Ln exp_cnj)
```
```  1101
```
```  1102 lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
```
```  1103   apply (cases "z=0", auto)
```
```  1104   apply (rule exp_complex_eqI)
```
```  1105   using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
```
```  1106   apply (auto simp: abs_if exp_minus split: split_if_asm)
```
```  1107   apply (metis Im_Ln_less_pi Im_Ln_pos_le add_less_cancel_left add_strict_mono
```
```  1108                inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
```
```  1109   done
```
```  1110
```
```  1111 lemma Ln_1 [simp]: "Ln(1) = 0"
```
```  1112 proof -
```
```  1113   have "Ln (exp 0) = 0"
```
```  1114     by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
```
```  1115   then show ?thesis
```
```  1116     by simp
```
```  1117 qed
```
```  1118
```
```  1119 lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
```
```  1120   apply (rule exp_complex_eqI)
```
```  1121   using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
```
```  1122   apply (auto simp: abs_if)
```
```  1123   done
```
```  1124
```
```  1125 lemma Ln_ii [simp]: "Ln ii = ii * of_real pi/2"
```
```  1126   using Ln_exp [of "ii * (of_real pi/2)"]
```
```  1127   unfolding exp_Euler
```
```  1128   by simp
```
```  1129
```
```  1130 lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)"
```
```  1131 proof -
```
```  1132   have  "Ln(-ii) = Ln(1/ii)"
```
```  1133     by simp
```
```  1134   also have "... = - (Ln ii)"
```
```  1135     by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one)
```
```  1136   also have "... = - (ii * pi/2)"
```
```  1137     by (simp add: Ln_ii)
```
```  1138   finally show ?thesis .
```
```  1139 qed
```
```  1140
```
```  1141 lemma Ln_times:
```
```  1142   assumes "w \<noteq> 0" "z \<noteq> 0"
```
```  1143     shows "Ln(w * z) =
```
```  1144                 (if Im(Ln w + Ln z) \<le> -pi then
```
```  1145                   (Ln(w) + Ln(z)) + ii * of_real(2*pi)
```
```  1146                 else if Im(Ln w + Ln z) > pi then
```
```  1147                   (Ln(w) + Ln(z)) - ii * of_real(2*pi)
```
```  1148                 else Ln(w) + Ln(z))"
```
```  1149   using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
```
```  1150   using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
```
```  1151   by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
```
```  1152
```
```  1153 lemma Ln_times_simple:
```
```  1154     "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
```
```  1155          \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
```
```  1156   by (simp add: Ln_times)
```
```  1157
```
```  1158 lemma Ln_minus:
```
```  1159   assumes "z \<noteq> 0"
```
```  1160     shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
```
```  1161                      then Ln(z) + ii * pi
```
```  1162                      else Ln(z) - ii * pi)" (is "_ = ?rhs")
```
```  1163   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
```
```  1164         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
```
```  1165     by (auto simp: of_real_numeral exp_add exp_diff exp_Euler intro!: Ln_unique)
```
```  1166
```
```  1167 lemma Ln_inverse_if:
```
```  1168   assumes "z \<noteq> 0"
```
```  1169     shows "Ln (inverse z) =
```
```  1170             (if (Im(z) = 0 \<longrightarrow> 0 < Re z)
```
```  1171              then -(Ln z)
```
```  1172              else -(Ln z) + \<i> * 2 * complex_of_real pi)"
```
```  1173 proof (cases "(Im(z) = 0 \<longrightarrow> 0 < Re z)")
```
```  1174   case True then show ?thesis
```
```  1175     by (simp add: Ln_inverse)
```
```  1176 next
```
```  1177   case False
```
```  1178   then have z: "Im z = 0" "Re z < 0"
```
```  1179     using assms
```
```  1180     apply auto
```
```  1181     by (metis cnj.code complex_cnj_cnj not_less_iff_gr_or_eq zero_complex.simps(1) zero_complex.simps(2))
```
```  1182   have "Ln(inverse z) = Ln(- (inverse (-z)))"
```
```  1183     by simp
```
```  1184   also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
```
```  1185     using assms z
```
```  1186     apply (simp add: Ln_minus)
```
```  1187     apply (simp add: field_simps)
```
```  1188     done
```
```  1189   also have "... = - Ln (- z) + \<i> * complex_of_real pi"
```
```  1190     apply (subst Ln_inverse)
```
```  1191     using z assms by auto
```
```  1192   also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
```
```  1193     apply (subst Ln_minus [OF assms])
```
```  1194     using assms z
```
```  1195     apply simp
```
```  1196     done
```
```  1197   finally show ?thesis
```
```  1198     using assms z
```
```  1199     by simp
```
```  1200 qed
```
```  1201
```
```  1202 lemma Ln_times_ii:
```
```  1203   assumes "z \<noteq> 0"
```
```  1204     shows  "Ln(ii * z) = (if 0 \<le> Re(z) | Im(z) < 0
```
```  1205                           then Ln(z) + ii * of_real pi/2
```
```  1206                           else Ln(z) - ii * of_real(3 * pi/2))"
```
```  1207   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
```
```  1208         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
```
```  1209   by (auto simp: of_real_numeral Ln_times)
```
```  1210
```
```  1211
```
```  1212 subsection{*Relation between Square Root and exp/ln, hence its derivative*}
```
```  1213
```
```  1214 lemma csqrt_exp_Ln:
```
```  1215   assumes "z \<noteq> 0"
```
```  1216     shows "csqrt z = exp(Ln(z) / 2)"
```
```  1217 proof -
```
```  1218   have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
```
```  1219     by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
```
```  1220   also have "... = z"
```
```  1221     using assms exp_Ln by blast
```
```  1222   finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
```
```  1223     by simp
```
```  1224   also have "... = exp (Ln z / 2)"
```
```  1225     apply (subst csqrt_square)
```
```  1226     using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
```
```  1227     apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+)
```
```  1228     done
```
```  1229   finally show ?thesis using assms csqrt_square
```
```  1230     by simp
```
```  1231 qed
```
```  1232
```
```  1233 lemma csqrt_inverse:
```
```  1234   assumes "Im(z) = 0 \<Longrightarrow> 0 < Re z"
```
```  1235     shows "csqrt (inverse z) = inverse (csqrt z)"
```
```  1236 proof (cases "z=0", simp)
```
```  1237   assume "z \<noteq> 0 "
```
```  1238   then show ?thesis
```
```  1239     using assms
```
```  1240     by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
```
```  1241 qed
```
```  1242
```
```  1243 lemma cnj_csqrt:
```
```  1244   assumes "Im z = 0 \<Longrightarrow> 0 \<le> Re(z)"
```
```  1245     shows "cnj(csqrt z) = csqrt(cnj z)"
```
```  1246 proof (cases "z=0", simp)
```
```  1247   assume z: "z \<noteq> 0"
```
```  1248   then have "Im z = 0 \<Longrightarrow> 0 < Re(z)"
```
```  1249     using assms cnj.code complex_cnj_zero_iff by fastforce
```
```  1250   then show ?thesis
```
```  1251    using z by (simp add: csqrt_exp_Ln cnj_Ln exp_cnj)
```
```  1252 qed
```
```  1253
```
```  1254 lemma has_field_derivative_csqrt:
```
```  1255   assumes "Im z = 0 \<Longrightarrow> 0 < Re(z)"
```
```  1256     shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)"
```
```  1257 proof -
```
```  1258   have z: "z \<noteq> 0"
```
```  1259     using assms by auto
```
```  1260   then have *: "inverse z = inverse (2*z) * 2"
```
```  1261     by (simp add: divide_simps)
```
```  1262   show ?thesis
```
```  1263     apply (rule DERIV_transform_at [where f = "\<lambda>z. exp(Ln(z) / 2)" and d = "norm z"])
```
```  1264     apply (intro derivative_eq_intros | simp add: assms)+
```
```  1265     apply (rule *)
```
```  1266     using z
```
```  1267     apply (auto simp: field_simps csqrt_exp_Ln [symmetric])
```
```  1268     apply (metis power2_csqrt power2_eq_square)
```
```  1269     apply (metis csqrt_exp_Ln dist_0_norm less_irrefl)
```
```  1270     done
```
```  1271 qed
```
```  1272
```
```  1273 lemma complex_differentiable_at_csqrt:
```
```  1274     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable at z"
```
```  1275   using complex_differentiable_def has_field_derivative_csqrt by blast
```
```  1276
```
```  1277 lemma complex_differentiable_within_csqrt:
```
```  1278     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable (at z within s)"
```
```  1279   using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast
```
```  1280
```
```  1281 lemma continuous_at_csqrt:
```
```  1282     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
```
```  1283   by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
```
```  1284
```
```  1285 corollary isCont_csqrt' [simp]:
```
```  1286    "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
```
```  1287   by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
```
```  1288
```
```  1289 lemma continuous_within_csqrt:
```
```  1290     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
```
```  1291   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
```
```  1292
```
```  1293 lemma continuous_on_csqrt [continuous_intros]:
```
```  1294     "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s csqrt"
```
```  1295   by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
```
```  1296
```
```  1297 lemma holomorphic_on_csqrt:
```
```  1298     "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt holomorphic_on s"
```
```  1299   by (simp add: complex_differentiable_within_csqrt holomorphic_on_def)
```
```  1300
```
```  1301 lemma continuous_within_closed_nontrivial:
```
```  1302     "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
```
```  1303   using open_Compl
```
```  1304   by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
```
```  1305
```
```  1306 lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
```
```  1307   using closed_halfspace_Re_ge
```
```  1308   by (simp add: closed_Int closed_complex_Reals)
```
```  1309
```
```  1310 lemma continuous_within_csqrt_posreal:
```
```  1311     "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
```
```  1312 proof (cases "Im z = 0 --> 0 < Re(z)")
```
```  1313   case True then show ?thesis
```
```  1314     by (blast intro: continuous_within_csqrt)
```
```  1315 next
```
```  1316   case False
```
```  1317   then have "Im z = 0" "Re z < 0 \<or> z = 0"
```
```  1318     using False cnj.code complex_cnj_zero_iff by auto force
```
```  1319   then show ?thesis
```
```  1320     apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
```
```  1321     apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
```
```  1322     apply (rule_tac x="e^2" in exI)
```
```  1323     apply (auto simp: Reals_def)
```
```  1324 by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
```
```  1325 qed
```
```  1326
```
```  1327
```
```  1328 end
```