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