src/HOL/Analysis/Complex_Transcendental.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69508 2a4c8a2a3f8e child 69566 c41954ee87cf permissions -rw-r--r--
capitalize proper names in lemma names
     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 i}\<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 Arg2pi} follows HOL Light in adopting the interval $[0,2\pi)$.

   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 $(-\pi,\pi]$.

   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: $(-\pi,\pi]$.\<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
`