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