src/HOL/Analysis/Complex_Transcendental.thy
author Manuel Eberl <eberlm@in.tum.de>
Sun Aug 20 18:55:03 2017 +0200 (23 months ago)
changeset 66466 aec5d9c88d69
parent 66453 cc19f7ca2ed6
child 66480 4b8d1df8933b
permissions -rw-r--r--
More lemmas for HOL-Analysis
wenzelm@60420
     1
section \<open>Complex Transcendental Functions\<close>
lp15@59745
     2
lp15@61711
     3
text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>
lp15@61711
     4
lp15@59745
     5
theory Complex_Transcendental
lp15@62534
     6
imports
eberlm@62049
     7
  Complex_Analysis_Basics
hoelzl@63594
     8
  Summation_Tests
wenzelm@66453
     9
   "HOL-Library.Periodic_Fun"
lp15@59745
    10
begin
lp15@59745
    11
eberlm@62049
    12
(* TODO: Figure out what to do with Möbius transformations *)
eberlm@62049
    13
definition "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))"
eberlm@62049
    14
lp15@62534
    15
lemma moebius_inverse:
eberlm@62049
    16
  assumes "a * d \<noteq> b * c" "c * z + d \<noteq> 0"
eberlm@62049
    17
  shows   "moebius d (-b) (-c) a (moebius a b c d z) = z"
eberlm@62049
    18
proof -
eberlm@62049
    19
  from assms have "(-c) * moebius a b c d z + a \<noteq> 0" unfolding moebius_def
eberlm@62049
    20
    by (simp add: field_simps)
eberlm@62049
    21
  with assms show ?thesis
eberlm@62049
    22
    unfolding moebius_def by (simp add: moebius_def divide_simps) (simp add: algebra_simps)?
eberlm@62049
    23
qed
eberlm@62049
    24
lp15@62534
    25
lemma moebius_inverse':
eberlm@62049
    26
  assumes "a * d \<noteq> b * c" "c * z - a \<noteq> 0"
eberlm@62049
    27
  shows   "moebius a b c d (moebius d (-b) (-c) a z) = z"
eberlm@62049
    28
  using assms moebius_inverse[of d a "-b" "-c" z]
eberlm@62049
    29
  by (auto simp: algebra_simps)
eberlm@62049
    30
lp15@59870
    31
lemma cmod_add_real_less:
lp15@59870
    32
  assumes "Im z \<noteq> 0" "r\<noteq>0"
wenzelm@61945
    33
    shows "cmod (z + r) < cmod z + \<bar>r\<bar>"
lp15@59870
    34
proof (cases z)
lp15@59870
    35
  case (Complex x y)
lp15@59870
    36
  have "r * x / \<bar>r\<bar> < sqrt (x*x + y*y)"
lp15@59870
    37
    apply (rule real_less_rsqrt)
lp15@59870
    38
    using assms
lp15@59870
    39
    apply (simp add: Complex power2_eq_square)
lp15@59870
    40
    using not_real_square_gt_zero by blast
lp15@59870
    41
  then show ?thesis using assms Complex
lp15@59870
    42
    apply (auto simp: cmod_def)
lp15@59870
    43
    apply (rule power2_less_imp_less, auto)
lp15@59870
    44
    apply (simp add: power2_eq_square field_simps)
lp15@59870
    45
    done
lp15@59870
    46
qed
lp15@59870
    47
wenzelm@61945
    48
lemma cmod_diff_real_less: "Im z \<noteq> 0 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> cmod (z - x) < cmod z + \<bar>x\<bar>"
lp15@59870
    49
  using cmod_add_real_less [of z "-x"]
lp15@59870
    50
  by simp
lp15@59870
    51
lp15@59870
    52
lemma cmod_square_less_1_plus:
lp15@59870
    53
  assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
lp15@59870
    54
    shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
lp15@59870
    55
  using assms
lp15@59870
    56
  apply (cases "Im z = 0 \<or> Re z = 0")
lp15@59870
    57
  using abs_square_less_1
lp15@59870
    58
    apply (force simp add: Re_power2 Im_power2 cmod_def)
lp15@59870
    59
  using cmod_diff_real_less [of "1 - z\<^sup>2" "1"]
lp15@59870
    60
  apply (simp add: norm_power Im_power2)
lp15@59870
    61
  done
lp15@59870
    62
wenzelm@60420
    63
subsection\<open>The Exponential Function is Differentiable and Continuous\<close>
lp15@59745
    64
lp15@62534
    65
lemma field_differentiable_within_exp: "exp field_differentiable (at z within s)"
lp15@62534
    66
  using DERIV_exp field_differentiable_at_within field_differentiable_def by blast
lp15@59745
    67
lp15@59745
    68
lemma continuous_within_exp:
lp15@59745
    69
  fixes z::"'a::{real_normed_field,banach}"
lp15@59745
    70
  shows "continuous (at z within s) exp"
lp15@59745
    71
by (simp add: continuous_at_imp_continuous_within)
lp15@59745
    72
lp15@62381
    73
lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"
lp15@62534
    74
  by (simp add: field_differentiable_within_exp holomorphic_on_def)
lp15@59745
    75
wenzelm@60420
    76
subsection\<open>Euler and de Moivre formulas.\<close>
wenzelm@60420
    77
wenzelm@60420
    78
text\<open>The sine series times @{term i}\<close>
lp15@65064
    79
lemma sin_i_eq: "(\<lambda>n. (\<i> * sin_coeff n) * z^n) sums (\<i> * sin z)"
lp15@59745
    80
proof -
wenzelm@63589
    81
  have "(\<lambda>n. \<i> * sin_coeff n *\<^sub>R z^n) sums (\<i> * sin z)"
lp15@59745
    82
    using sin_converges sums_mult by blast
lp15@59745
    83
  then show ?thesis
lp15@59745
    84
    by (simp add: scaleR_conv_of_real field_simps)
lp15@59745
    85
qed
lp15@59745
    86
wenzelm@63589
    87
theorem exp_Euler: "exp(\<i> * z) = cos(z) + \<i> * sin(z)"
lp15@59745
    88
proof -
wenzelm@63589
    89
  have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n)
wenzelm@63589
    90
        = (\<lambda>n. (\<i> * z) ^ n /\<^sub>R (fact n))"
lp15@59745
    91
  proof
lp15@59745
    92
    fix n
wenzelm@63589
    93
    show "(cos_coeff n + \<i> * sin_coeff n) * z^n = (\<i> * z) ^ n /\<^sub>R (fact n)"
lp15@59745
    94
      by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
lp15@59745
    95
  qed
wenzelm@63589
    96
  also have "... sums (exp (\<i> * z))"
lp15@59745
    97
    by (rule exp_converges)
wenzelm@63589
    98
  finally have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (exp (\<i> * z))" .
wenzelm@63589
    99
  moreover have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (cos z + \<i> * sin z)"
lp15@65064
   100
    using sums_add [OF cos_converges [of z] sin_i_eq [of z]]
lp15@59745
   101
    by (simp add: field_simps scaleR_conv_of_real)
lp15@59745
   102
  ultimately show ?thesis
lp15@59745
   103
    using sums_unique2 by blast
lp15@59745
   104
qed
lp15@59745
   105
wenzelm@63589
   106
corollary exp_minus_Euler: "exp(-(\<i> * z)) = cos(z) - \<i> * sin(z)"
lp15@59745
   107
  using exp_Euler [of "-z"]
lp15@59745
   108
  by simp
lp15@59745
   109
wenzelm@63589
   110
lemma sin_exp_eq: "sin z = (exp(\<i> * z) - exp(-(\<i> * z))) / (2*\<i>)"
lp15@59745
   111
  by (simp add: exp_Euler exp_minus_Euler)
lp15@59745
   112
wenzelm@63589
   113
lemma sin_exp_eq': "sin z = \<i> * (exp(-(\<i> * z)) - exp(\<i> * z)) / 2"
lp15@59745
   114
  by (simp add: exp_Euler exp_minus_Euler)
lp15@59745
   115
wenzelm@63589
   116
lemma cos_exp_eq:  "cos z = (exp(\<i> * z) + exp(-(\<i> * z))) / 2"
lp15@59745
   117
  by (simp add: exp_Euler exp_minus_Euler)
lp15@59745
   118
wenzelm@60420
   119
subsection\<open>Relationships between real and complex trig functions\<close>
lp15@59745
   120
lp15@59745
   121
lemma real_sin_eq [simp]:
lp15@59745
   122
  fixes x::real
lp15@59745
   123
  shows "Re(sin(of_real x)) = sin x"
lp15@59745
   124
  by (simp add: sin_of_real)
lp15@59862
   125
lp15@59745
   126
lemma real_cos_eq [simp]:
lp15@59745
   127
  fixes x::real
lp15@59745
   128
  shows "Re(cos(of_real x)) = cos x"
lp15@59745
   129
  by (simp add: cos_of_real)
lp15@59745
   130
wenzelm@63589
   131
lemma DeMoivre: "(cos z + \<i> * sin z) ^ n = cos(n * z) + \<i> * sin(n * z)"
lp15@59745
   132
  apply (simp add: exp_Euler [symmetric])
lp15@59745
   133
  by (metis exp_of_nat_mult mult.left_commute)
lp15@59745
   134
lp15@59745
   135
lemma exp_cnj:
lp15@59745
   136
  fixes z::complex
lp15@59745
   137
  shows "cnj (exp z) = exp (cnj z)"
lp15@59745
   138
proof -
lp15@59745
   139
  have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))"
lp15@59745
   140
    by auto
lp15@59745
   141
  also have "... sums (exp (cnj z))"
lp15@59745
   142
    by (rule exp_converges)
lp15@59745
   143
  finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
lp15@59745
   144
  moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
lp15@59862
   145
    by (metis exp_converges sums_cnj)
lp15@59745
   146
  ultimately show ?thesis
lp15@59745
   147
    using sums_unique2
lp15@59862
   148
    by blast
lp15@59745
   149
qed
lp15@59745
   150
lp15@59745
   151
lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
lp15@59745
   152
  by (simp add: sin_exp_eq exp_cnj field_simps)
lp15@59745
   153
lp15@59745
   154
lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
lp15@59745
   155
  by (simp add: cos_exp_eq exp_cnj field_simps)
lp15@59745
   156
lp15@62534
   157
lemma field_differentiable_at_sin: "sin field_differentiable at z"
lp15@62534
   158
  using DERIV_sin field_differentiable_def by blast
lp15@62534
   159
lp15@62534
   160
lemma field_differentiable_within_sin: "sin field_differentiable (at z within s)"
lp15@62534
   161
  by (simp add: field_differentiable_at_sin field_differentiable_at_within)
lp15@62534
   162
lp15@62534
   163
lemma field_differentiable_at_cos: "cos field_differentiable at z"
lp15@62534
   164
  using DERIV_cos field_differentiable_def by blast
lp15@62534
   165
lp15@62534
   166
lemma field_differentiable_within_cos: "cos field_differentiable (at z within s)"
lp15@62534
   167
  by (simp add: field_differentiable_at_cos field_differentiable_at_within)
lp15@59745
   168
lp15@59745
   169
lemma holomorphic_on_sin: "sin holomorphic_on s"
lp15@62534
   170
  by (simp add: field_differentiable_within_sin holomorphic_on_def)
lp15@59745
   171
lp15@59745
   172
lemma holomorphic_on_cos: "cos holomorphic_on s"
lp15@62534
   173
  by (simp add: field_differentiable_within_cos holomorphic_on_def)
lp15@59745
   174
wenzelm@60420
   175
subsection\<open>Get a nice real/imaginary separation in Euler's formula.\<close>
lp15@59745
   176
lp15@59862
   177
lemma Euler: "exp(z) = of_real(exp(Re z)) *
wenzelm@63589
   178
              (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
lp15@65274
   179
by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real Complex_eq)
lp15@59745
   180
lp15@59745
   181
lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
lp15@59745
   182
  by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
lp15@59745
   183
lp15@59745
   184
lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
lp15@59745
   185
  by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
lp15@59745
   186
lp15@59745
   187
lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
lp15@59745
   188
  by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
lp15@59745
   189
lp15@59745
   190
lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
lp15@59745
   191
  by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
lp15@59862
   192
lp15@59862
   193
lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
lp15@59862
   194
  by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
lp15@59862
   195
lp15@59862
   196
lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
lp15@59862
   197
  by (simp add: Re_sin Im_sin algebra_simps)
lp15@59862
   198
lp15@59862
   199
lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
lp15@59862
   200
  by (simp add: Re_sin Im_sin algebra_simps)
lp15@59862
   201
wenzelm@60420
   202
subsection\<open>More on the Polar Representation of Complex Numbers\<close>
lp15@59746
   203
lp15@59746
   204
lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
lp15@65274
   205
  by (simp add: Complex_eq exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
lp15@59746
   206
lp15@59746
   207
lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
lp15@65274
   208
                 (is "?lhs = ?rhs")
lp15@65274
   209
proof 
lp15@65274
   210
  assume "exp z = 1"
lp15@65274
   211
  then have "Re z = 0"
lp15@65274
   212
    by (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
lp15@65274
   213
  with \<open>?lhs\<close> show ?rhs
lp15@65274
   214
    by (metis Re_exp complex_Re_of_int cos_one_2pi_int exp_zero mult.commute mult_numeral_1 numeral_One of_int_mult of_int_numeral)
lp15@65274
   215
next
lp15@65274
   216
  assume ?rhs then show ?lhs
lp15@65274
   217
    using Im_exp Re_exp complex_Re_Im_cancel_iff by force
lp15@65274
   218
qed
lp15@59746
   219
wenzelm@63589
   220
lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * \<i>)"
lp15@59746
   221
                (is "?lhs = ?rhs")
lp15@59746
   222
proof -
lp15@59746
   223
  have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
lp15@59746
   224
    by (simp add: exp_diff)
lp15@59746
   225
  also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
lp15@59746
   226
    by (simp add: exp_eq_1)
lp15@59746
   227
  also have "... \<longleftrightarrow> ?rhs"
lp15@59746
   228
    by (auto simp: algebra_simps intro!: complex_eqI)
lp15@59746
   229
  finally show ?thesis .
lp15@59746
   230
qed
lp15@59746
   231
wenzelm@61945
   232
lemma exp_complex_eqI: "\<bar>Im w - Im z\<bar> < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
lp15@59746
   233
  by (auto simp: exp_eq abs_mult)
lp15@59746
   234
lp15@59862
   235
lemma exp_integer_2pi:
wenzelm@61070
   236
  assumes "n \<in> \<int>"
wenzelm@63589
   237
  shows "exp((2 * n * pi) * \<i>) = 1"
lp15@59746
   238
proof -
wenzelm@63589
   239
  have "exp((2 * n * pi) * \<i>) = exp 0"
lp15@59746
   240
    using assms
lp15@59746
   241
    by (simp only: Ints_def exp_eq) auto
lp15@59746
   242
  also have "... = 1"
lp15@59746
   243
    by simp
lp15@59746
   244
  finally show ?thesis .
lp15@59746
   245
qed
lp15@59746
   246
lp15@64287
   247
lemma exp_plus_2pin [simp]: "exp (z + \<i> * (of_int n * (of_real pi * 2))) = exp z"
lp15@64287
   248
  by (simp add: exp_eq)
lp15@64287
   249
eberlm@66466
   250
lemma exp_integer_2pi_plus1:
eberlm@66466
   251
  assumes "n \<in> \<int>"
eberlm@66466
   252
  shows "exp(((2 * n + 1) * pi) * \<i>) = - 1"
eberlm@66466
   253
proof -
eberlm@66466
   254
  from assms obtain n' where [simp]: "n = of_int n'"
eberlm@66466
   255
    by (auto simp: Ints_def)
eberlm@66466
   256
  have "exp(((2 * n + 1) * pi) * \<i>) = exp (pi * \<i>)"
eberlm@66466
   257
    using assms by (subst exp_eq) (auto intro!: exI[of _ n'] simp: algebra_simps)
eberlm@66466
   258
  also have "... = - 1"
eberlm@66466
   259
    by simp
eberlm@66466
   260
  finally show ?thesis .
eberlm@66466
   261
qed
eberlm@66466
   262
lp15@64287
   263
lemma inj_on_exp_pi:
lp15@64287
   264
  fixes z::complex shows "inj_on exp (ball z pi)"
lp15@64287
   265
proof (clarsimp simp: inj_on_def exp_eq)
lp15@64287
   266
  fix y n
lp15@64287
   267
  assume "dist z (y + 2 * of_int n * of_real pi * \<i>) < pi"
lp15@64287
   268
         "dist z y < pi"
lp15@64287
   269
  then have "dist y (y + 2 * of_int n * of_real pi * \<i>) < pi+pi"
lp15@64287
   270
    using dist_commute_lessI dist_triangle_less_add by blast
lp15@64287
   271
  then have "norm (2 * of_int n * of_real pi * \<i>) < 2*pi"
lp15@64287
   272
    by (simp add: dist_norm)
lp15@64287
   273
  then show "n = 0"
lp15@64287
   274
    by (auto simp: norm_mult)
lp15@64287
   275
qed
lp15@64287
   276
lp15@59746
   277
lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
lp15@59746
   278
proof -
lp15@59746
   279
  { assume "sin y = sin x" "cos y = cos x"
lp15@59746
   280
    then have "cos (y-x) = 1"
lp15@59746
   281
      using cos_add [of y "-x"] by simp
lp15@61609
   282
    then have "\<exists>n::int. y-x = n * 2 * pi"
lp15@59746
   283
      using cos_one_2pi_int by blast }
lp15@59746
   284
  then show ?thesis
lp15@59746
   285
  apply (auto simp: sin_add cos_add)
lp15@59746
   286
  apply (metis add.commute diff_add_cancel mult.commute)
lp15@59746
   287
  done
lp15@59746
   288
qed
lp15@59746
   289
lp15@59862
   290
lemma exp_i_ne_1:
lp15@59746
   291
  assumes "0 < x" "x < 2*pi"
lp15@59746
   292
  shows "exp(\<i> * of_real x) \<noteq> 1"
lp15@59862
   293
proof
lp15@59746
   294
  assume "exp (\<i> * of_real x) = 1"
lp15@59746
   295
  then have "exp (\<i> * of_real x) = exp 0"
lp15@59746
   296
    by simp
lp15@59746
   297
  then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
lp15@59746
   298
    by (simp only: Ints_def exp_eq) auto
lp15@59746
   299
  then have  "of_real x = (of_int (2 * n) * pi)"
lp15@59746
   300
    by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
lp15@59746
   301
  then have  "x = (of_int (2 * n) * pi)"
lp15@59746
   302
    by simp
lp15@59746
   303
  then show False using assms
lp15@59746
   304
    by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
lp15@59746
   305
qed
lp15@59746
   306
lp15@59862
   307
lemma sin_eq_0:
lp15@59746
   308
  fixes z::complex
lp15@59746
   309
  shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
lp15@59746
   310
  by (simp add: sin_exp_eq exp_eq of_real_numeral)
lp15@59746
   311
lp15@59862
   312
lemma cos_eq_0:
lp15@59746
   313
  fixes z::complex
lp15@59746
   314
  shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
lp15@59746
   315
  using sin_eq_0 [of "z - of_real pi/2"]
lp15@59746
   316
  by (simp add: sin_diff algebra_simps)
lp15@59746
   317
lp15@59862
   318
lemma cos_eq_1:
lp15@59746
   319
  fixes z::complex
lp15@59746
   320
  shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
lp15@59746
   321
proof -
lp15@59746
   322
  have "cos z = cos (2*(z/2))"
lp15@59746
   323
    by simp
lp15@59746
   324
  also have "... = 1 - 2 * sin (z/2) ^ 2"
lp15@59746
   325
    by (simp only: cos_double_sin)
lp15@59746
   326
  finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
lp15@59746
   327
    by simp
lp15@59746
   328
  show ?thesis
lp15@59746
   329
    by (auto simp: sin_eq_0 of_real_numeral)
lp15@59862
   330
qed
lp15@59746
   331
lp15@59746
   332
lemma csin_eq_1:
lp15@59746
   333
  fixes z::complex
lp15@59746
   334
  shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)"
lp15@59746
   335
  using cos_eq_1 [of "z - of_real pi/2"]
lp15@59746
   336
  by (simp add: cos_diff algebra_simps)
lp15@59746
   337
lp15@59746
   338
lemma csin_eq_minus1:
lp15@59746
   339
  fixes z::complex
lp15@59746
   340
  shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)"
lp15@59746
   341
        (is "_ = ?rhs")
lp15@59746
   342
proof -
lp15@59746
   343
  have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
lp15@59746
   344
    by (simp add: equation_minus_iff)
lp15@59746
   345
  also have "...  \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
lp15@59746
   346
    by (simp only: csin_eq_1)
lp15@59746
   347
  also have "...  \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
lp15@59746
   348
    apply (rule iff_exI)
lp15@59746
   349
    by (metis (no_types)  is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff)
lp15@59746
   350
  also have "... = ?rhs"
lp15@59746
   351
    apply (auto simp: of_real_numeral)
lp15@59746
   352
    apply (rule_tac [2] x="-(x+1)" in exI)
lp15@59746
   353
    apply (rule_tac x="-(x+1)" in exI)
lp15@59746
   354
    apply (simp_all add: algebra_simps)
lp15@59746
   355
    done
lp15@59746
   356
  finally show ?thesis .
lp15@59862
   357
qed
lp15@59746
   358
lp15@59862
   359
lemma ccos_eq_minus1:
lp15@59746
   360
  fixes z::complex
lp15@59746
   361
  shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
lp15@59746
   362
  using csin_eq_1 [of "z - of_real pi/2"]
lp15@59746
   363
  apply (simp add: sin_diff)
lp15@59746
   364
  apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
lp15@59862
   365
  done
lp15@59746
   366
lp15@59746
   367
lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
lp15@59746
   368
                (is "_ = ?rhs")
lp15@59746
   369
proof -
lp15@59746
   370
  have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
lp15@59746
   371
    by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
lp15@59746
   372
  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
lp15@59746
   373
    by (simp only: csin_eq_1)
lp15@59746
   374
  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
lp15@59746
   375
    apply (rule iff_exI)
lp15@59746
   376
    apply (auto simp: algebra_simps of_real_numeral)
lp15@59746
   377
    apply (rule injD [OF inj_of_real [where 'a = complex]])
lp15@59746
   378
    apply (auto simp: of_real_numeral)
lp15@59746
   379
    done
lp15@59746
   380
  also have "... = ?rhs"
lp15@59746
   381
    by (auto simp: algebra_simps)
lp15@59746
   382
  finally show ?thesis .
lp15@59862
   383
qed
lp15@59746
   384
lp15@59746
   385
lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
lp15@59746
   386
proof -
lp15@59746
   387
  have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
lp15@59746
   388
    by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
lp15@59746
   389
  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
lp15@59746
   390
    by (simp only: csin_eq_minus1)
lp15@59746
   391
  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
lp15@59746
   392
    apply (rule iff_exI)
lp15@59746
   393
    apply (auto simp: algebra_simps)
lp15@59746
   394
    apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
lp15@59746
   395
    done
lp15@59746
   396
  also have "... = ?rhs"
lp15@59746
   397
    by (auto simp: algebra_simps)
lp15@59746
   398
  finally show ?thesis .
lp15@59862
   399
qed
lp15@59746
   400
lp15@59746
   401
lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
lp15@59746
   402
                      (is "_ = ?rhs")
lp15@59746
   403
proof -
lp15@59746
   404
  have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
lp15@59746
   405
    by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
lp15@59746
   406
  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
lp15@59746
   407
    by (simp only: ccos_eq_minus1)
lp15@59746
   408
  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
lp15@59746
   409
    apply (rule iff_exI)
lp15@59746
   410
    apply (auto simp: algebra_simps)
lp15@59746
   411
    apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
lp15@59746
   412
    done
lp15@59746
   413
  also have "... = ?rhs"
lp15@59746
   414
    by (auto simp: algebra_simps)
lp15@59746
   415
  finally show ?thesis .
lp15@59862
   416
qed
lp15@59746
   417
lp15@65064
   418
lemma dist_exp_i_1: "norm(exp(\<i> * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
lp15@59862
   419
  apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
lp15@59746
   420
  using cos_double_sin [of "t/2"]
lp15@59746
   421
  apply (simp add: real_sqrt_mult)
lp15@59746
   422
  done
lp15@59746
   423
lp15@64773
   424
lp15@64773
   425
lemma complex_sin_eq:
lp15@64773
   426
  fixes w :: complex
lp15@64773
   427
  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))"
lp15@64773
   428
        (is "?lhs = ?rhs")
lp15@64773
   429
proof
lp15@64773
   430
  assume ?lhs
lp15@64773
   431
  then have "sin w - sin z = 0"
lp15@64773
   432
    by (auto simp: algebra_simps)
lp15@64773
   433
  then have "sin ((w - z) / 2)*cos ((w + z) / 2) = 0"
lp15@64773
   434
    by (auto simp: sin_diff_sin)
lp15@64773
   435
  then consider "sin ((w - z) / 2) = 0" | "cos ((w + z) / 2) = 0"
lp15@64773
   436
    using mult_eq_0_iff by blast
lp15@64773
   437
  then show ?rhs
lp15@64773
   438
  proof cases
lp15@64773
   439
    case 1
lp15@64773
   440
    then show ?thesis
lp15@64773
   441
      apply (auto simp: sin_eq_0 algebra_simps)
lp15@64773
   442
      by (metis Ints_of_int of_real_of_int_eq)
lp15@64773
   443
  next
lp15@64773
   444
    case 2
lp15@64773
   445
    then show ?thesis
lp15@64773
   446
      apply (auto simp: cos_eq_0 algebra_simps)
lp15@64773
   447
      by (metis Ints_of_int of_real_of_int_eq)
lp15@64773
   448
  qed
lp15@64773
   449
next
lp15@64773
   450
  assume ?rhs
lp15@64773
   451
  then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \<or>
lp15@64773
   452
                               w = -z + of_real ((2* of_int n + 1)*pi)"
lp15@64773
   453
    using Ints_cases by blast
lp15@64773
   454
  then show ?lhs
lp15@64773
   455
    using Periodic_Fun.sin.plus_of_int [of z n]
lp15@64773
   456
    apply (auto simp: algebra_simps)
lp15@64773
   457
    by (metis (no_types, hide_lams) add_diff_cancel_left add_diff_cancel_left' add_minus_cancel
lp15@64773
   458
              mult.commute sin.plus_of_int sin_minus sin_plus_pi)
lp15@64773
   459
qed
lp15@64773
   460
lp15@64773
   461
lemma complex_cos_eq:
lp15@64773
   462
  fixes w :: complex
lp15@64773
   463
  shows "cos w = cos z \<longleftrightarrow>
lp15@64773
   464
         (\<exists>n \<in> \<int>. w = z + of_real(2*n*pi) \<or> w = -z + of_real(2*n*pi))"
lp15@64773
   465
        (is "?lhs = ?rhs")
lp15@64773
   466
proof
lp15@64773
   467
  assume ?lhs
lp15@64773
   468
  then have "cos w - cos z = 0"
lp15@64773
   469
    by (auto simp: algebra_simps)
lp15@64773
   470
  then have "sin ((w + z) / 2) * sin ((z - w) / 2) = 0"
lp15@64773
   471
    by (auto simp: cos_diff_cos)
lp15@64773
   472
  then consider "sin ((w + z) / 2) = 0" | "sin ((z - w) / 2) = 0"
lp15@64773
   473
    using mult_eq_0_iff by blast
lp15@64773
   474
  then show ?rhs
lp15@64773
   475
  proof cases
lp15@64773
   476
    case 1
lp15@64773
   477
    then show ?thesis
lp15@64773
   478
      apply (auto simp: sin_eq_0 algebra_simps)
lp15@64773
   479
      by (metis Ints_of_int of_real_of_int_eq)
lp15@64773
   480
  next
lp15@64773
   481
    case 2
lp15@64773
   482
    then show ?thesis
lp15@64773
   483
      apply (auto simp: sin_eq_0 algebra_simps)
lp15@64773
   484
      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)
lp15@64773
   485
  qed
lp15@64773
   486
next
lp15@64773
   487
  assume ?rhs
lp15@64773
   488
  then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \<or>
lp15@64773
   489
                               w = -z + of_real(2*n*pi)"
lp15@64773
   490
    using Ints_cases  by (metis of_int_mult of_int_numeral)
lp15@64773
   491
  then show ?lhs
lp15@64773
   492
    using Periodic_Fun.cos.plus_of_int [of z n]
lp15@64773
   493
    apply (auto simp: algebra_simps)
lp15@64773
   494
    by (metis cos.plus_of_int cos_minus minus_add_cancel mult.commute)
lp15@64773
   495
qed
lp15@64773
   496
lp15@64773
   497
lemma sin_eq:
lp15@64773
   498
   "sin x = sin y \<longleftrightarrow> (\<exists>n \<in> \<int>. x = y + 2*n*pi \<or> x = -y + (2*n + 1)*pi)"
lp15@64773
   499
  using complex_sin_eq [of x y]
lp15@64773
   500
  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)
lp15@64773
   501
lp15@64773
   502
lemma cos_eq:
lp15@64773
   503
   "cos x = cos y \<longleftrightarrow> (\<exists>n \<in> \<int>. x = y + 2*n*pi \<or> x = -y + 2*n*pi)"
lp15@64773
   504
  using complex_cos_eq [of x y]
lp15@64773
   505
  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)
lp15@64773
   506
lp15@59746
   507
lemma sinh_complex:
lp15@59746
   508
  fixes z :: complex
wenzelm@63589
   509
  shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
lp15@65274
   510
  by (simp add: sin_exp_eq divide_simps exp_minus)
lp15@59746
   511
lp15@65064
   512
lemma sin_i_times:
lp15@59746
   513
  fixes z :: complex
wenzelm@63589
   514
  shows "sin(\<i> * z) = \<i> * ((exp z - inverse (exp z)) / 2)"
lp15@59746
   515
  using sinh_complex by auto
lp15@59746
   516
lp15@59746
   517
lemma sinh_real:
lp15@59746
   518
  fixes x :: real
wenzelm@63589
   519
  shows "of_real((exp x - inverse (exp x)) / 2) = -\<i> * sin(\<i> * of_real x)"
lp15@65274
   520
  by (simp add: exp_of_real sin_i_times)
lp15@59746
   521
lp15@59746
   522
lemma cosh_complex:
lp15@59746
   523
  fixes z :: complex
wenzelm@63589
   524
  shows "(exp z + inverse (exp z)) / 2 = cos(\<i> * z)"
lp15@65274
   525
  by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real)
lp15@59746
   526
lp15@59746
   527
lemma cosh_real:
lp15@59746
   528
  fixes x :: real
wenzelm@63589
   529
  shows "of_real((exp x + inverse (exp x)) / 2) = cos(\<i> * of_real x)"
lp15@65274
   530
  by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real)
lp15@59746
   531
lp15@65064
   532
lemmas cos_i_times = cosh_complex [symmetric]
lp15@59746
   533
lp15@59862
   534
lemma norm_cos_squared:
lp15@59746
   535
    "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
lp15@59746
   536
  apply (cases z)
lp15@65274
   537
  apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real Complex_eq)
lp15@61694
   538
  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
lp15@59746
   539
  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
lp15@59746
   540
  apply (simp add: sin_squared_eq)
lp15@59746
   541
  apply (simp add: power2_eq_square algebra_simps divide_simps)
lp15@59746
   542
  done
lp15@59746
   543
lp15@59746
   544
lemma norm_sin_squared:
lp15@59746
   545
    "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
lp15@59746
   546
  apply (cases z)
lp15@65274
   547
  apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq)
lp15@61694
   548
  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
lp15@59746
   549
  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
lp15@59746
   550
  apply (simp add: cos_squared_eq)
lp15@59746
   551
  apply (simp add: power2_eq_square algebra_simps divide_simps)
lp15@59862
   552
  done
lp15@59746
   553
lp15@59746
   554
lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
lp15@59746
   555
  using abs_Im_le_cmod linear order_trans by fastforce
lp15@59746
   556
lp15@59862
   557
lemma norm_cos_le:
lp15@59746
   558
  fixes z::complex
lp15@59746
   559
  shows "norm(cos z) \<le> exp(norm z)"
lp15@59746
   560
proof -
lp15@59746
   561
  have "Im z \<le> cmod z"
lp15@59746
   562
    using abs_Im_le_cmod abs_le_D1 by auto
lp15@59746
   563
  with exp_uminus_Im show ?thesis
lp15@59746
   564
    apply (simp add: cos_exp_eq norm_divide)
lp15@59746
   565
    apply (rule order_trans [OF norm_triangle_ineq], simp)
lp15@59746
   566
    apply (metis add_mono exp_le_cancel_iff mult_2_right)
lp15@59746
   567
    done
lp15@59746
   568
qed
lp15@59746
   569
lp15@59862
   570
lemma norm_cos_plus1_le:
lp15@59746
   571
  fixes z::complex
lp15@59746
   572
  shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
lp15@59746
   573
proof -
lp15@59746
   574
  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"
lp15@59746
   575
      by arith
lp15@59746
   576
  have *: "Im z \<le> cmod z"
lp15@59746
   577
    using abs_Im_le_cmod abs_le_D1 by auto
lp15@59746
   578
  have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)"
lp15@59746
   579
    by (simp add: norm_add_rule_thm)
lp15@59746
   580
  have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
lp15@59746
   581
    by (simp add: cos_exp_eq)
lp15@59746
   582
  also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
lp15@59746
   583
    by (simp add: field_simps)
lp15@59746
   584
  also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
lp15@59746
   585
    by (simp add: norm_divide)
lp15@59746
   586
  finally show ?thesis
lp15@59746
   587
    apply (rule ssubst, simp)
lp15@59746
   588
    apply (rule order_trans [OF triangle3], simp)
lp15@59746
   589
    using exp_uminus_Im *
lp15@59746
   590
    apply (auto intro: mono)
lp15@59746
   591
    done
lp15@59746
   592
qed
lp15@59746
   593
wenzelm@60420
   594
subsection\<open>Taylor series for complex exponential, sine and cosine.\<close>
lp15@59746
   595
lp15@59746
   596
declare power_Suc [simp del]
lp15@59746
   597
immler@66252
   598
lemma Taylor_exp_field:
immler@66252
   599
  fixes z::"'a::{banach,real_normed_field}"
immler@66252
   600
  shows "norm (exp z - (\<Sum>i\<le>n. z ^ i / fact i)) \<le> exp (norm z) * (norm z ^ Suc n) / fact n"
immler@66252
   601
proof (rule field_taylor[of _ n "\<lambda>k. exp" "exp (norm z)" 0 z, simplified])
immler@66252
   602
  show "convex (closed_segment 0 z)"
immler@66252
   603
    by (rule convex_closed_segment [of 0 z])
immler@66252
   604
next
immler@66252
   605
  fix k x
immler@66252
   606
  assume "x \<in> closed_segment 0 z" "k \<le> n"
immler@66252
   607
  show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
immler@66252
   608
    using DERIV_exp DERIV_subset by blast
immler@66252
   609
next
immler@66252
   610
  fix x
immler@66252
   611
  assume x: "x \<in> closed_segment 0 z"
immler@66252
   612
  have "norm (exp x) \<le> exp (norm x)"
immler@66252
   613
    by (rule norm_exp)
immler@66252
   614
  also have "norm x \<le> norm z"
immler@66252
   615
    using x by (auto simp: closed_segment_def intro!: mult_left_le_one_le)
immler@66252
   616
  finally show "norm (exp x) \<le> exp (norm z)"
immler@66252
   617
    by simp
immler@66252
   618
next
immler@66252
   619
  show "0 \<in> closed_segment 0 z"
immler@66252
   620
    by (auto simp: closed_segment_def)
immler@66252
   621
next
immler@66252
   622
  show "z \<in> closed_segment 0 z"
immler@66252
   623
    apply (simp add: closed_segment_def scaleR_conv_of_real)
immler@66252
   624
    using of_real_1 zero_le_one by blast
immler@66252
   625
qed
immler@66252
   626
lp15@59862
   627
lemma Taylor_exp:
lp15@59746
   628
  "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
lp15@59746
   629
proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
lp15@59746
   630
  show "convex (closed_segment 0 z)"
paulson@61518
   631
    by (rule convex_closed_segment [of 0 z])
lp15@59746
   632
next
lp15@59746
   633
  fix k x
lp15@59746
   634
  assume "x \<in> closed_segment 0 z" "k \<le> n"
lp15@59746
   635
  show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
lp15@59746
   636
    using DERIV_exp DERIV_subset by blast
lp15@59746
   637
next
lp15@59746
   638
  fix x
lp15@59746
   639
  assume "x \<in> closed_segment 0 z"
lp15@59746
   640
  then show "Re x \<le> \<bar>Re z\<bar>"
lp15@59746
   641
    apply (auto simp: closed_segment_def scaleR_conv_of_real)
lp15@59746
   642
    by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans)
lp15@59746
   643
next
lp15@59746
   644
  show "0 \<in> closed_segment 0 z"
lp15@59746
   645
    by (auto simp: closed_segment_def)
lp15@59746
   646
next
lp15@59746
   647
  show "z \<in> closed_segment 0 z"
lp15@59746
   648
    apply (simp add: closed_segment_def scaleR_conv_of_real)
lp15@59746
   649
    using of_real_1 zero_le_one by blast
lp15@59862
   650
qed
lp15@59746
   651
lp15@59862
   652
lemma
lp15@59746
   653
  assumes "0 \<le> u" "u \<le> 1"
lp15@59862
   654
  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
lp15@59746
   655
    and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
lp15@59746
   656
proof -
lp15@59746
   657
  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
lp15@59746
   658
    by arith
lp15@59746
   659
  show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
lp15@59746
   660
    apply (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
lp15@59746
   661
    apply (rule order_trans [OF norm_triangle_ineq4])
lp15@59746
   662
    apply (rule mono)
lp15@59746
   663
    apply (auto simp: abs_if mult_left_le_one_le)
lp15@59746
   664
    apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
lp15@59746
   665
    apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
lp15@59746
   666
    done
lp15@59746
   667
  show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
lp15@59746
   668
    apply (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
lp15@59746
   669
    apply (rule order_trans [OF norm_triangle_ineq])
lp15@59746
   670
    apply (rule mono)
lp15@59746
   671
    apply (auto simp: abs_if mult_left_le_one_le)
lp15@59746
   672
    apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
lp15@59746
   673
    apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
lp15@59746
   674
    done
lp15@59746
   675
qed
lp15@59862
   676
lp15@59862
   677
lemma Taylor_sin:
lp15@59862
   678
  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
lp15@59746
   679
   \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
lp15@59746
   680
proof -
lp15@59746
   681
  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
lp15@59746
   682
      by arith
lp15@59746
   683
  have *: "cmod (sin z -
lp15@59746
   684
                 (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
lp15@59862
   685
           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
lp15@61609
   686
  proof (rule complex_taylor [of "closed_segment 0 z" n
lp15@61609
   687
                                 "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)"
lp15@60162
   688
                                 "exp\<bar>Im z\<bar>" 0 z,  simplified])
lp15@59746
   689
    fix k x
lp15@59746
   690
    show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
lp15@59746
   691
            (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
lp15@59746
   692
            (at x within closed_segment 0 z)"
lp15@59746
   693
      apply (auto simp: power_Suc)
lp15@59746
   694
      apply (intro derivative_eq_intros | simp)+
lp15@59746
   695
      done
lp15@59746
   696
  next
lp15@59746
   697
    fix x
lp15@59746
   698
    assume "x \<in> closed_segment 0 z"
lp15@59746
   699
    then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
lp15@59746
   700
      by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
lp15@59862
   701
  qed
lp15@59746
   702
  have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
lp15@59746
   703
            = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
lp15@59746
   704
    by (auto simp: sin_coeff_def elim!: oddE)
lp15@59746
   705
  show ?thesis
lp15@59746
   706
    apply (rule order_trans [OF _ *])
lp15@59746
   707
    apply (simp add: **)
lp15@59746
   708
    done
lp15@59746
   709
qed
lp15@59746
   710
lp15@59862
   711
lemma Taylor_cos:
lp15@59862
   712
  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k))
lp15@59746
   713
   \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
lp15@59746
   714
proof -
lp15@59746
   715
  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
lp15@59746
   716
      by arith
lp15@59746
   717
  have *: "cmod (cos z -
lp15@59746
   718
                 (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
lp15@59862
   719
           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
lp15@59746
   720
  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,
lp15@59746
   721
simplified])
lp15@59746
   722
    fix k x
lp15@59746
   723
    assume "x \<in> closed_segment 0 z" "k \<le> n"
lp15@59746
   724
    show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
lp15@59746
   725
            (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
lp15@59746
   726
             (at x within closed_segment 0 z)"
lp15@59746
   727
      apply (auto simp: power_Suc)
lp15@59746
   728
      apply (intro derivative_eq_intros | simp)+
lp15@59746
   729
      done
lp15@59746
   730
  next
lp15@59746
   731
    fix x
lp15@59746
   732
    assume "x \<in> closed_segment 0 z"
lp15@59746
   733
    then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
lp15@59746
   734
      by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
lp15@59862
   735
  qed
lp15@59746
   736
  have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
lp15@59746
   737
            = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
lp15@59746
   738
    by (auto simp: cos_coeff_def elim!: evenE)
lp15@59746
   739
  show ?thesis
lp15@59746
   740
    apply (rule order_trans [OF _ *])
lp15@59746
   741
    apply (simp add: **)
lp15@59746
   742
    done
lp15@59746
   743
qed
lp15@59746
   744
lp15@60162
   745
declare power_Suc [simp]
lp15@59746
   746
wenzelm@60420
   747
text\<open>32-bit Approximation to e\<close>
wenzelm@61945
   748
lemma e_approx_32: "\<bar>exp(1) - 5837465777 / 2147483648\<bar> \<le> (inverse(2 ^ 32)::real)"
lp15@59751
   749
  using Taylor_exp [of 1 14] exp_le
nipkow@64267
   750
  apply (simp add: sum_distrib_right in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
lp15@59751
   751
  apply (simp only: pos_le_divide_eq [symmetric], linarith)
lp15@59751
   752
  done
lp15@59751
   753
lp15@65719
   754
lemma e_less_272: "exp 1 < (272/100::real)"
lp15@60017
   755
  using e_approx_32
nipkow@62390
   756
  by (simp add: abs_if split: if_split_asm)
lp15@60017
   757
lp15@65719
   758
lemma ln_272_gt_1: "ln (272/100) > (1::real)"
lp15@65719
   759
  by (metis e_less_272 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
lp15@65719
   760
lp15@65719
   761
text\<open>Apparently redundant. But many arguments involve integers.\<close>
lp15@60017
   762
lemma ln3_gt_1: "ln 3 > (1::real)"
lp15@65719
   763
  by (simp add: less_trans [OF ln_272_gt_1])
lp15@60017
   764
wenzelm@60420
   765
subsection\<open>The argument of a complex number\<close>
lp15@59746
   766
lp15@59746
   767
definition Arg :: "complex \<Rightarrow> real" where
lp15@59746
   768
 "Arg z \<equiv> if z = 0 then 0
lp15@59746
   769
           else THE t. 0 \<le> t \<and> t < 2*pi \<and>
wenzelm@63589
   770
                    z = of_real(norm z) * exp(\<i> * of_real t)"
lp15@59746
   771
lp15@59746
   772
lemma Arg_0 [simp]: "Arg(0) = 0"
lp15@59746
   773
  by (simp add: Arg_def)
lp15@59746
   774
lp15@59746
   775
lemma Arg_unique_lemma:
wenzelm@63589
   776
  assumes z:  "z = of_real(norm z) * exp(\<i> * of_real t)"
wenzelm@63589
   777
      and z': "z = of_real(norm z) * exp(\<i> * of_real t')"
lp15@59746
   778
      and t:  "0 \<le> t"  "t < 2*pi"
lp15@59746
   779
      and t': "0 \<le> t'" "t' < 2*pi"
lp15@59746
   780
      and nz: "z \<noteq> 0"
lp15@59746
   781
  shows "t' = t"
lp15@59746
   782
proof -
lp15@59746
   783
  have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
lp15@59746
   784
    by arith
lp15@59746
   785
  have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
lp15@59746
   786
    by (metis z z')
lp15@59746
   787
  then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
lp15@59746
   788
    by (metis nz mult_left_cancel mult_zero_left z)
lp15@59746
   789
  then have "sin t' = sin t \<and> cos t' = cos t"
lp15@59746
   790
    apply (simp add: exp_Euler sin_of_real cos_of_real)
lp15@59746
   791
    by (metis Complex_eq complex.sel)
lp15@61609
   792
  then obtain n::int where n: "t' = t + 2 * n * pi"
lp15@59746
   793
    by (auto simp: sin_cos_eq_iff)
lp15@59746
   794
  then have "n=0"
lp15@59746
   795
    apply (rule_tac z=n in int_cases)
lp15@59746
   796
    using t t'
lp15@59746
   797
    apply (auto simp: mult_less_0_iff algebra_simps)
lp15@59746
   798
    done
lp15@59746
   799
  then show "t' = t"
lp15@59746
   800
      by (simp add: n)
lp15@59746
   801
qed
lp15@59746
   802
wenzelm@63589
   803
lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
lp15@59746
   804
proof (cases "z=0")
lp15@59746
   805
  case True then show ?thesis
lp15@59746
   806
    by (simp add: Arg_def)
lp15@59746
   807
next
lp15@59746
   808
  case False
lp15@59746
   809
  obtain t where t: "0 \<le> t" "t < 2*pi"
lp15@59746
   810
             and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
lp15@59746
   811
    using sincos_total_2pi [OF complex_unit_circle [OF False]]
lp15@59746
   812
    by blast
wenzelm@63589
   813
  have z: "z = of_real(norm z) * exp(\<i> * of_real t)"
lp15@59746
   814
    apply (rule complex_eqI)
lp15@59746
   815
    using t False ReIm
lp15@59746
   816
    apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
lp15@59746
   817
    done
lp15@59746
   818
  show ?thesis
lp15@59746
   819
    apply (simp add: Arg_def False)
lp15@59746
   820
    apply (rule theI [where a=t])
lp15@59746
   821
    using t z False
lp15@59746
   822
    apply (auto intro: Arg_unique_lemma)
lp15@59746
   823
    done
lp15@59746
   824
qed
lp15@59746
   825
lp15@59746
   826
corollary
lp15@59746
   827
  shows Arg_ge_0: "0 \<le> Arg z"
lp15@59746
   828
    and Arg_lt_2pi: "Arg z < 2*pi"
wenzelm@63589
   829
    and Arg_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
lp15@59746
   830
  using Arg by auto
lp15@59746
   831
lp15@64394
   832
lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg z)) = z"
lp15@64394
   833
  by (metis Arg_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
lp15@59746
   834
wenzelm@63589
   835
lemma Arg_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
lp15@59746
   836
  apply (rule Arg_unique_lemma [OF _ Arg_eq])
lp15@59746
   837
  using Arg [of z]
lp15@59746
   838
  apply (auto simp: norm_mult)
lp15@59746
   839
  done
lp15@59746
   840
lp15@59746
   841
lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
lp15@59746
   842
  apply (rule Arg_unique [of "norm z"])
lp15@59746
   843
  apply (rule complex_eqI)
lp15@59746
   844
  using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] Arg_eq [of z]
lp15@59746
   845
  apply auto
lp15@59746
   846
  apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
lp15@59746
   847
  apply (metis Re_rcis Im_rcis rcis_def)+
lp15@59746
   848
  done
lp15@59746
   849
lp15@59746
   850
lemma Arg_times_of_real [simp]: "0 < r \<Longrightarrow> Arg (of_real r * z) = Arg z"
lp15@59746
   851
  apply (cases "z=0", simp)
lp15@59746
   852
  apply (rule Arg_unique [of "r * norm z"])
lp15@59746
   853
  using Arg
lp15@59746
   854
  apply auto
lp15@59746
   855
  done
lp15@59746
   856
lp15@59746
   857
lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
lp15@59746
   858
  by (metis Arg_times_of_real mult.commute)
lp15@59746
   859
lp15@59746
   860
lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
lp15@59746
   861
  by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
lp15@59746
   862
lp15@59746
   863
lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
lp15@59746
   864
proof (cases "z=0")
lp15@59746
   865
  case True then show ?thesis
lp15@59746
   866
    by simp
lp15@59746
   867
next
lp15@59746
   868
  case False
lp15@59746
   869
  have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
lp15@59746
   870
    by (metis Arg_eq)
lp15@59746
   871
  also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
lp15@59746
   872
    using False
lp15@59746
   873
    by (simp add: zero_le_mult_iff)
lp15@59746
   874
  also have "... \<longleftrightarrow> Arg z \<le> pi"
lp15@59746
   875
    by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
lp15@59746
   876
  finally show ?thesis
lp15@59746
   877
    by blast
lp15@59746
   878
qed
lp15@59746
   879
lp15@59746
   880
lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
lp15@59746
   881
proof (cases "z=0")
lp15@59746
   882
  case True then show ?thesis
lp15@59746
   883
    by simp
lp15@59746
   884
next
lp15@59746
   885
  case False
lp15@59746
   886
  have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
lp15@59746
   887
    by (metis Arg_eq)
lp15@59746
   888
  also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
lp15@59746
   889
    using False
lp15@59746
   890
    by (simp add: zero_less_mult_iff)
lp15@59746
   891
  also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
lp15@59746
   892
    using Arg_ge_0  Arg_lt_2pi sin_le_zero sin_gt_zero
lp15@59746
   893
    apply (auto simp: Im_exp)
lp15@59746
   894
    using le_less apply fastforce
lp15@59746
   895
    using not_le by blast
lp15@59746
   896
  finally show ?thesis
lp15@59746
   897
    by blast
lp15@59746
   898
qed
lp15@59746
   899
wenzelm@61070
   900
lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
lp15@59746
   901
proof (cases "z=0")
lp15@59746
   902
  case True then show ?thesis
lp15@59746
   903
    by simp
lp15@59746
   904
next
lp15@59746
   905
  case False
wenzelm@61070
   906
  have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
lp15@59746
   907
    by (metis Arg_eq)
wenzelm@61070
   908
  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
lp15@59746
   909
    using False
lp15@59746
   910
    by (simp add: zero_le_mult_iff)
lp15@59746
   911
  also have "... \<longleftrightarrow> Arg z = 0"
lp15@59746
   912
    apply (auto simp: Re_exp)
lp15@59746
   913
    apply (metis Arg_lt_pi Arg_ge_0 Arg_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
lp15@59746
   914
    using Arg_eq [of z]
lp15@59746
   915
    apply (auto simp: Reals_def)
lp15@59746
   916
    done
lp15@59746
   917
  finally show ?thesis
lp15@59746
   918
    by blast
lp15@59746
   919
qed
lp15@59746
   920
lp15@61609
   921
corollary Arg_gt_0:
lp15@60150
   922
  assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
lp15@60150
   923
    shows "Arg z > 0"
lp15@60150
   924
  using Arg_eq_0 Arg_ge_0 assms dual_order.strict_iff_order by fastforce
lp15@60150
   925
lp15@59746
   926
lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
lp15@59746
   927
  by (simp add: Arg_eq_0)
lp15@59746
   928
lp15@59746
   929
lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
lp15@59746
   930
  apply  (cases "z=0", simp)
lp15@59746
   931
  using Arg_eq_0 [of "-z"]
lp15@59746
   932
  apply (auto simp: complex_is_Real_iff Arg_minus)
lp15@59746
   933
  apply (simp add: complex_Re_Im_cancel_iff)
lp15@59746
   934
  apply (metis Arg_minus pi_gt_zero add.left_neutral minus_minus minus_zero)
lp15@59746
   935
  done
lp15@59746
   936
lp15@59746
   937
lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
lp15@59746
   938
  using Arg_eq_0 Arg_eq_pi not_le by auto
lp15@59746
   939
lp15@59746
   940
lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
lp15@59746
   941
  apply (cases "z=0", simp)
lp15@59746
   942
  apply (rule Arg_unique [of "inverse (norm z)"])
lp15@61762
   943
  using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] exp_two_pi_i
lp15@59746
   944
  apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
lp15@59746
   945
  done
lp15@59746
   946
lp15@59746
   947
lemma Arg_eq_iff:
lp15@59746
   948
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59746
   949
     shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
lp15@59746
   950
  using assms Arg_eq [of z] Arg_eq [of w]
lp15@59746
   951
  apply auto
lp15@59746
   952
  apply (rule_tac x="norm w / norm z" in exI)
lp15@59746
   953
  apply (simp add: divide_simps)
lp15@59746
   954
  by (metis mult.commute mult.left_commute)
lp15@59746
   955
lp15@59746
   956
lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
lp15@59746
   957
  using complex_is_Real_iff
lp15@59746
   958
  apply (simp add: Arg_eq_0)
lp15@59746
   959
  apply (auto simp: divide_simps not_sum_power2_lt_zero)
lp15@59746
   960
  done
lp15@59746
   961
lp15@59746
   962
lemma Arg_divide:
lp15@59746
   963
  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
lp15@59746
   964
    shows "Arg(z / w) = Arg z - Arg w"
lp15@59746
   965
  apply (rule Arg_unique [of "norm(z / w)"])
lp15@59746
   966
  using assms Arg_eq [of z] Arg_eq [of w] Arg_ge_0 [of w] Arg_lt_2pi [of z]
lp15@59746
   967
  apply (auto simp: exp_diff norm_divide algebra_simps divide_simps)
lp15@59746
   968
  done
lp15@59746
   969
lp15@59746
   970
lemma Arg_le_div_sum:
lp15@59746
   971
  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
lp15@59746
   972
    shows "Arg z = Arg w + Arg(z / w)"
lp15@59746
   973
  by (simp add: Arg_divide assms)
lp15@59746
   974
lp15@59746
   975
lemma Arg_le_div_sum_eq:
lp15@59746
   976
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59746
   977
    shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
lp15@59746
   978
  using assms
lp15@59746
   979
  by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
lp15@59746
   980
lp15@59746
   981
lemma Arg_diff:
lp15@59746
   982
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59746
   983
    shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
lp15@59746
   984
  using assms
lp15@59746
   985
  apply (auto simp: Arg_ge_0 Arg_divide not_le)
lp15@59746
   986
  using Arg_divide [of w z] Arg_inverse [of "w/z"]
lp15@59746
   987
  apply auto
lp15@59746
   988
  by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
lp15@59746
   989
lp15@59746
   990
lemma Arg_add:
lp15@59746
   991
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59746
   992
    shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
lp15@59746
   993
  using assms
lp15@59746
   994
  using Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
lp15@59746
   995
  apply (auto simp: Arg_ge_0 Arg_divide not_le)
lp15@59746
   996
  apply (metis Arg_lt_2pi add.commute)
lp15@59746
   997
  apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
lp15@59746
   998
  done
lp15@59746
   999
lp15@59746
  1000
lemma Arg_times:
lp15@59746
  1001
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59746
  1002
    shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
lp15@59746
  1003
                            else (Arg w + Arg z) - 2*pi)"
lp15@59746
  1004
  using Arg_add [OF assms]
lp15@59746
  1005
  by auto
lp15@59746
  1006
lp15@59746
  1007
lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
lp15@59746
  1008
  apply (cases "z=0", simp)
lp15@59746
  1009
  apply (rule trans [of _ "Arg(inverse z)"])
lp15@59746
  1010
  apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
lp15@59746
  1011
  apply (metis norm_eq_zero of_real_power zero_less_power2)
lp15@59746
  1012
  apply (auto simp: of_real_numeral Arg_inverse)
lp15@59746
  1013
  done
lp15@59746
  1014
lp15@59746
  1015
lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
lp15@59746
  1016
  using Arg_eq_0 Arg_eq_0_pi
lp15@59746
  1017
  by auto
lp15@59746
  1018
lp15@59746
  1019
lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
lp15@61762
  1020
  by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: exp_eq_polar)
lp15@61762
  1021
lp15@61762
  1022
lemma complex_split_polar:
lp15@61762
  1023
  obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
lp15@65274
  1024
  using Arg cis.ctr cis_conv_exp unfolding Complex_eq by fastforce
lp15@59751
  1025
lp15@61806
  1026
lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
lp15@61806
  1027
proof (cases w rule: complex_split_polar)
lp15@61806
  1028
  case (1 r a) with sin_cos_le1 [of a \<phi>] show ?thesis
lp15@61806
  1029
    apply (simp add: norm_mult cmod_unit_one)
lp15@61806
  1030
    by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
lp15@61806
  1031
qed
lp15@61806
  1032
wenzelm@60420
  1033
subsection\<open>Analytic properties of tangent function\<close>
lp15@59751
  1034
lp15@59751
  1035
lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
lp15@59751
  1036
  by (simp add: cnj_cos cnj_sin tan_def)
lp15@59751
  1037
lp15@62534
  1038
lemma field_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan field_differentiable at z"
lp15@62534
  1039
  unfolding field_differentiable_def
lp15@59751
  1040
  using DERIV_tan by blast
lp15@59751
  1041
lp15@62534
  1042
lemma field_differentiable_within_tan: "~(cos z = 0)
lp15@62534
  1043
         \<Longrightarrow> tan field_differentiable (at z within s)"
lp15@62534
  1044
  using field_differentiable_at_tan field_differentiable_at_within by blast
lp15@59751
  1045
lp15@59751
  1046
lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
lp15@59751
  1047
  using continuous_at_imp_continuous_within isCont_tan by blast
lp15@59751
  1048
lp15@59751
  1049
lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan"
lp15@59751
  1050
  by (simp add: continuous_at_imp_continuous_on)
lp15@59751
  1051
lp15@59751
  1052
lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
lp15@62534
  1053
  by (simp add: field_differentiable_within_tan holomorphic_on_def)
lp15@59751
  1054
lp15@59751
  1055
wenzelm@60420
  1056
subsection\<open>Complex logarithms (the conventional principal value)\<close>
lp15@59751
  1057
lp15@60020
  1058
instantiation complex :: ln
lp15@60020
  1059
begin
lp15@60017
  1060
lp15@60020
  1061
definition ln_complex :: "complex \<Rightarrow> complex"
lp15@60020
  1062
  where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
lp15@59751
  1063
lp15@65585
  1064
text\<open>NOTE: within this scope, the constant Ln is not yet available!\<close>
lp15@59751
  1065
lemma
lp15@59751
  1066
  assumes "z \<noteq> 0"
lp15@60020
  1067
    shows exp_Ln [simp]:  "exp(ln z) = z"
lp15@60020
  1068
      and mpi_less_Im_Ln: "-pi < Im(ln z)"
lp15@60020
  1069
      and Im_Ln_le_pi:    "Im(ln z) \<le> pi"
lp15@59751
  1070
proof -
lp15@59751
  1071
  obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
lp15@59751
  1072
    using complex_unimodular_polar [of "z / (norm z)"] assms
lp15@59751
  1073
    by (auto simp: norm_divide divide_simps)
lp15@59751
  1074
  obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
lp15@59751
  1075
    using sincos_principal_value [of "\<psi>"] assms
lp15@59751
  1076
    by (auto simp: norm_divide divide_simps)
lp15@60020
  1077
  have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \<le> pi" unfolding ln_complex_def
lp15@59751
  1078
    apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
lp15@59751
  1079
    using z assms \<phi>
lp15@61762
  1080
    apply (auto simp: field_simps exp_complex_eqI exp_eq_polar cis.code)
lp15@59751
  1081
    done
lp15@60020
  1082
  then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \<le> pi"
lp15@59751
  1083
    by auto
lp15@59751
  1084
qed
lp15@59751
  1085
lp15@59751
  1086
lemma Ln_exp [simp]:
lp15@59751
  1087
  assumes "-pi < Im(z)" "Im(z) \<le> pi"
lp15@60020
  1088
    shows "ln(exp z) = z"
lp15@59751
  1089
  apply (rule exp_complex_eqI)
lp15@59751
  1090
  using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
lp15@59751
  1091
  apply auto
lp15@59751
  1092
  done
lp15@59751
  1093
wenzelm@60420
  1094
subsection\<open>Relation to Real Logarithm\<close>
lp15@60020
  1095
lp15@60020
  1096
lemma Ln_of_real:
lp15@60020
  1097
  assumes "0 < z"
lp15@60020
  1098
    shows "ln(of_real z::complex) = of_real(ln z)"
lp15@60020
  1099
proof -
lp15@60020
  1100
  have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"
lp15@60020
  1101
    by (simp add: exp_of_real)
lp15@60020
  1102
  also have "... = of_real(ln z)"
lp15@60020
  1103
    using assms
lp15@60020
  1104
    by (subst Ln_exp) auto
lp15@60020
  1105
  finally show ?thesis
lp15@60020
  1106
    using assms by simp
lp15@60020
  1107
qed
lp15@60020
  1108
lp15@60020
  1109
corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
lp15@60020
  1110
  by (auto simp: Ln_of_real elim: Reals_cases)
lp15@60020
  1111
lp15@60150
  1112
corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
lp15@60150
  1113
  by (simp add: Ln_of_real)
lp15@60150
  1114
wenzelm@61070
  1115
lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
lp15@60150
  1116
  using Ln_of_real by force
lp15@60150
  1117
lp15@65719
  1118
lemma Ln_Reals_eq: "\<lbrakk>x \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> ln x = of_real (ln (Re x))"
lp15@65719
  1119
  using Ln_of_real by force
lp15@65719
  1120
lp15@65585
  1121
lemma Ln_1 [simp]: "ln 1 = (0::complex)"
lp15@60020
  1122
proof -
lp15@60020
  1123
  have "ln (exp 0) = (0::complex)"
lp15@60020
  1124
    by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one)
lp15@60020
  1125
  then show ?thesis
lp15@65585
  1126
    by simp                              
lp15@60020
  1127
qed
lp15@60020
  1128
lp15@65585
  1129
  
lp15@65585
  1130
lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1" for x::complex
lp15@65585
  1131
  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
lp15@65585
  1132
lp15@60020
  1133
instance
lp15@60020
  1134
  by intro_classes (rule ln_complex_def Ln_1)
lp15@60020
  1135
lp15@60020
  1136
end
lp15@60020
  1137
lp15@60020
  1138
abbreviation Ln :: "complex \<Rightarrow> complex"
lp15@60020
  1139
  where "Ln \<equiv> ln"
lp15@60020
  1140
lp15@59751
  1141
lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
lp15@59751
  1142
  by (metis exp_Ln)
lp15@59751
  1143
lp15@59751
  1144
lemma Ln_unique: "exp(z) = w \<Longrightarrow> -pi < Im(z) \<Longrightarrow> Im(z) \<le> pi \<Longrightarrow> Ln w = z"
lp15@59751
  1145
  using Ln_exp by blast
lp15@59751
  1146
lp15@59751
  1147
lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
wenzelm@63092
  1148
  by (metis exp_Ln ln_exp norm_exp_eq_Re)
lp15@60150
  1149
lp15@61609
  1150
corollary ln_cmod_le:
lp15@60150
  1151
  assumes z: "z \<noteq> 0"
lp15@60150
  1152
    shows "ln (cmod z) \<le> cmod (Ln z)"
lp15@60150
  1153
  using norm_exp [of "Ln z", simplified exp_Ln [OF z]]
lp15@60150
  1154
  by (metis Re_Ln complex_Re_le_cmod z)
lp15@59751
  1155
lp15@62843
  1156
proposition exists_complex_root:
lp15@62843
  1157
  fixes z :: complex
lp15@62843
  1158
  assumes "n \<noteq> 0"  obtains w where "z = w ^ n"
lp15@62843
  1159
  apply (cases "z=0")
lp15@62843
  1160
  using assms apply (simp add: power_0_left)
lp15@62843
  1161
  apply (rule_tac w = "exp(Ln z / n)" in that)
lp15@62843
  1162
  apply (auto simp: assms exp_of_nat_mult [symmetric])
lp15@59751
  1163
  done
lp15@59751
  1164
lp15@62843
  1165
corollary exists_complex_root_nonzero:
lp15@62843
  1166
  fixes z::complex
lp15@62843
  1167
  assumes "z \<noteq> 0" "n \<noteq> 0"
lp15@62843
  1168
  obtains w where "w \<noteq> 0" "z = w ^ n"
lp15@62843
  1169
  by (metis exists_complex_root [of n z] assms power_0_left)
lp15@62843
  1170
wenzelm@60420
  1171
subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
wenzelm@60420
  1172
wenzelm@60420
  1173
text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
lp15@59862
  1174
lp15@59862
  1175
definition unwinding :: "complex \<Rightarrow> complex" where
wenzelm@63589
  1176
   "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
wenzelm@63589
  1177
wenzelm@63589
  1178
lemma unwinding_2pi: "(2*pi) * \<i> * unwinding(z) = z - Ln(exp z)"
lp15@59862
  1179
  by (simp add: unwinding_def)
lp15@59862
  1180
lp15@59862
  1181
lemma Ln_times_unwinding:
wenzelm@63589
  1182
    "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \<i> * unwinding(Ln w + Ln z)"
lp15@59862
  1183
  using unwinding_2pi by (simp add: exp_add)
lp15@59862
  1184
lp15@59862
  1185
wenzelm@60420
  1186
subsection\<open>Derivative of Ln away from the branch cut\<close>
lp15@59751
  1187
lp15@59751
  1188
lemma
paulson@62131
  1189
  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
lp15@59751
  1190
    shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
lp15@59751
  1191
      and Im_Ln_less_pi:           "Im (Ln z) < pi"
lp15@59751
  1192
proof -
lp15@59751
  1193
  have znz: "z \<noteq> 0"
lp15@59751
  1194
    using assms by auto
paulson@62131
  1195
  then have "Im (Ln z) \<noteq> pi"
paulson@62131
  1196
    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)
paulson@62131
  1197
  then show *: "Im (Ln z) < pi" using assms Im_Ln_le_pi
paulson@62131
  1198
    by (simp add: le_neq_trans znz)
lp15@62534
  1199
  have "(exp has_field_derivative z) (at (Ln z))"
lp15@62534
  1200
    by (metis znz DERIV_exp exp_Ln)
lp15@62534
  1201
  then show "(Ln has_field_derivative inverse(z)) (at z)"
lp15@59751
  1202
    apply (rule has_complex_derivative_inverse_strong_x
lp15@62534
  1203
              [where s = "{w. -pi < Im(w) \<and> Im(w) < pi}"])
lp15@59751
  1204
    using znz *
lp15@62534
  1205
    apply (auto simp: Transcendental.continuous_on_exp [OF continuous_on_id] open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt mpi_less_Im_Ln)
lp15@59751
  1206
    done
lp15@59751
  1207
qed
lp15@59751
  1208
lp15@59751
  1209
declare has_field_derivative_Ln [derivative_intros]
lp15@59751
  1210
declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
lp15@59751
  1211
lp15@62534
  1212
lemma field_differentiable_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln field_differentiable at z"
lp15@62534
  1213
  using field_differentiable_def has_field_derivative_Ln by blast
lp15@62534
  1214
lp15@62534
  1215
lemma field_differentiable_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0
lp15@62534
  1216
         \<Longrightarrow> Ln field_differentiable (at z within s)"
lp15@62534
  1217
  using field_differentiable_at_Ln field_differentiable_within_subset by blast
lp15@59751
  1218
paulson@62131
  1219
lemma continuous_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) Ln"
lp15@62534
  1220
  by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Ln)
lp15@59751
  1221
lp15@59862
  1222
lemma isCont_Ln' [simp]:
paulson@62131
  1223
   "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
lp15@59862
  1224
  by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
lp15@59862
  1225
paulson@62131
  1226
lemma continuous_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within s) Ln"
lp15@59751
  1227
  using continuous_at_Ln continuous_at_imp_continuous_within by blast
lp15@59751
  1228
paulson@62131
  1229
lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s Ln"
lp15@59751
  1230
  by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
lp15@59751
  1231
paulson@62131
  1232
lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
lp15@62534
  1233
  by (simp add: field_differentiable_within_Ln holomorphic_on_def)
lp15@59751
  1234
lp15@65719
  1235
lemma divide_ln_mono:
lp15@65719
  1236
  fixes x y::real
lp15@65719
  1237
  assumes "3 \<le> x" "x \<le> y"
lp15@65719
  1238
  shows "x / ln x \<le> y / ln y"
lp15@65719
  1239
proof (rule exE [OF complex_mvt_line [of x y "\<lambda>z. z / Ln z" "\<lambda>z. 1/(Ln z) - 1/(Ln z)^2"]];
lp15@65719
  1240
    clarsimp simp add: closed_segment_Reals closed_segment_eq_real_ivl assms)
lp15@65719
  1241
  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)"
lp15@65719
  1242
    using \<open>3 \<le> x\<close> apply -
lp15@65719
  1243
    apply (rule derivative_eq_intros | simp)+
lp15@65719
  1244
    apply (force simp: field_simps power_eq_if)
lp15@65719
  1245
    done
lp15@65719
  1246
  show "x / ln x \<le> y / ln y"
lp15@65719
  1247
    if "Re (y / Ln y) - Re (x / Ln x) = (Re (1 / Ln u) - Re (1 / (Ln u)\<^sup>2)) * (y - x)"
lp15@65719
  1248
    and x: "x \<le> u" "u \<le> y" for u
lp15@65719
  1249
  proof -
lp15@65719
  1250
    have eq: "y / ln y = (1 / ln u - 1 / (ln u)\<^sup>2) * (y - x) + x / ln x"
lp15@65719
  1251
      using that \<open>3 \<le> x\<close> by (auto simp: Ln_Reals_eq in_Reals_norm group_add_class.diff_eq_eq)
lp15@65719
  1252
    show ?thesis
lp15@65719
  1253
      using exp_le \<open>3 \<le> x\<close> x by (simp add: eq) (simp add: power_eq_if divide_simps ln_ge_iff)
lp15@65719
  1254
  qed
lp15@65719
  1255
qed
lp15@65719
  1256
    
lp15@59751
  1257
wenzelm@60420
  1258
subsection\<open>Quadrant-type results for Ln\<close>
lp15@59751
  1259
lp15@59751
  1260
lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
lp15@59751
  1261
  using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
lp15@59751
  1262
  by simp
lp15@59751
  1263
lp15@59751
  1264
lemma Re_Ln_pos_lt:
lp15@59751
  1265
  assumes "z \<noteq> 0"
wenzelm@61945
  1266
    shows "\<bar>Im(Ln z)\<bar> < pi/2 \<longleftrightarrow> 0 < Re(z)"
lp15@59751
  1267
proof -
lp15@59751
  1268
  { fix w
lp15@59751
  1269
    assume "w = Ln z"
lp15@59751
  1270
    then have w: "Im w \<le> pi" "- pi < Im w"
lp15@59751
  1271
      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
lp15@59751
  1272
      by auto
wenzelm@61945
  1273
    then have "\<bar>Im w\<bar> < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
lp15@59751
  1274
      apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
lp15@59751
  1275
      using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
nipkow@62390
  1276
      apply (simp add: abs_if split: if_split_asm)
lp15@59751
  1277
      apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4)
lp15@59751
  1278
               less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right
lp15@59751
  1279
               mult_numeral_1_right)
lp15@59751
  1280
      done
lp15@59751
  1281
  }
lp15@59751
  1282
  then show ?thesis using assms
lp15@59751
  1283
    by auto
lp15@59751
  1284
qed
lp15@59751
  1285
lp15@59751
  1286
lemma Re_Ln_pos_le:
lp15@59751
  1287
  assumes "z \<noteq> 0"
wenzelm@61945
  1288
    shows "\<bar>Im(Ln z)\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
lp15@59751
  1289
proof -
lp15@59751
  1290
  { fix w
lp15@59751
  1291
    assume "w = Ln z"
lp15@59751
  1292
    then have w: "Im w \<le> pi" "- pi < Im w"
lp15@59751
  1293
      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
lp15@59751
  1294
      by auto
wenzelm@61945
  1295
    then have "\<bar>Im w\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
lp15@59751
  1296
      apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
lp15@59751
  1297
      using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
nipkow@62390
  1298
      apply (auto simp: abs_if split: if_split_asm)
lp15@59751
  1299
      done
lp15@59751
  1300
  }
lp15@59751
  1301
  then show ?thesis using assms
lp15@59751
  1302
    by auto
lp15@59751
  1303
qed
lp15@59751
  1304
lp15@59751
  1305
lemma Im_Ln_pos_lt:
lp15@59751
  1306
  assumes "z \<noteq> 0"
lp15@59751
  1307
    shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
lp15@59751
  1308
proof -
lp15@59751
  1309
  { fix w
lp15@59751
  1310
    assume "w = Ln z"
lp15@59751
  1311
    then have w: "Im w \<le> pi" "- pi < Im w"
lp15@59751
  1312
      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
lp15@59751
  1313
      by auto
lp15@59751
  1314
    then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)"
lp15@59751
  1315
      using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"]
lp15@59751
  1316
      apply (auto simp: Im_exp zero_less_mult_iff)
lp15@59751
  1317
      using less_linear apply fastforce
lp15@59751
  1318
      using less_linear apply fastforce
lp15@59751
  1319
      done
lp15@59751
  1320
  }
lp15@59751
  1321
  then show ?thesis using assms
lp15@59751
  1322
    by auto
lp15@59751
  1323
qed
lp15@59751
  1324
lp15@59751
  1325
lemma Im_Ln_pos_le:
lp15@59751
  1326
  assumes "z \<noteq> 0"
lp15@59751
  1327
    shows "0 \<le> Im(Ln z) \<and> Im(Ln z) \<le> pi \<longleftrightarrow> 0 \<le> Im(z)"
lp15@59751
  1328
proof -
lp15@59751
  1329
  { fix w
lp15@59751
  1330
    assume "w = Ln z"
lp15@59751
  1331
    then have w: "Im w \<le> pi" "- pi < Im w"
lp15@59751
  1332
      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
lp15@59751
  1333
      by auto
lp15@59751
  1334
    then have "0 \<le> Im w \<and> Im w \<le> pi \<longleftrightarrow> 0 \<le> Im(exp w)"
lp15@59751
  1335
      using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"]
lp15@59751
  1336
      apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero)
lp15@59751
  1337
      apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi)
lp15@59751
  1338
      done }
lp15@59751
  1339
  then show ?thesis using assms
lp15@59751
  1340
    by auto
lp15@59751
  1341
qed
lp15@59751
  1342
wenzelm@61945
  1343
lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> \<bar>Im(Ln z)\<bar> < pi/2"
lp15@59751
  1344
  by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
lp15@59751
  1345
lp15@59751
  1346
lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
lp15@59751
  1347
  by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))
lp15@59751
  1348
paulson@62131
  1349
text\<open>A reference to the set of positive real numbers\<close>
lp15@59751
  1350
lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
lp15@62534
  1351
by (metis Im_complex_of_real Im_exp Ln_in_Reals Re_Ln_pos_lt Re_Ln_pos_lt_imp
paulson@62131
  1352
          Re_complex_of_real complex_is_Real_iff exp_Ln exp_of_real pi_gt_zero)
lp15@59751
  1353
lp15@59751
  1354
lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
lp15@62534
  1355
by (metis Im_Ln_eq_0 Im_Ln_pos_le Im_Ln_pos_lt add.left_neutral complex_eq less_eq_real_def
paulson@62131
  1356
    mult_zero_right not_less_iff_gr_or_eq pi_ge_zero pi_neq_zero rcis_zero_arg rcis_zero_mod)
lp15@59751
  1357
lp15@59751
  1358
wenzelm@60420
  1359
subsection\<open>More Properties of Ln\<close>
lp15@59751
  1360
paulson@62131
  1361
lemma cnj_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
lp15@59751
  1362
  apply (cases "z=0", auto)
lp15@59751
  1363
  apply (rule exp_complex_eqI)
nipkow@62390
  1364
  apply (auto simp: abs_if split: if_split_asm)
paulson@62131
  1365
  using Im_Ln_less_pi Im_Ln_le_pi apply force
lp15@62534
  1366
  apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff
paulson@62131
  1367
          mpi_less_Im_Ln mult.commute mult_2_right)
lp15@59751
  1368
  by (metis exp_Ln exp_cnj)
lp15@59751
  1369
paulson@62131
  1370
lemma Ln_inverse: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln(inverse z) = -(Ln z)"
lp15@59751
  1371
  apply (cases "z=0", auto)
lp15@59751
  1372
  apply (rule exp_complex_eqI)
lp15@59751
  1373
  using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
nipkow@62390
  1374
  apply (auto simp: abs_if exp_minus split: if_split_asm)
paulson@62131
  1375
  apply (metis Im_Ln_less_pi Im_Ln_le_pi add.commute add_mono_thms_linordered_field(3) inverse_nonzero_iff_nonzero mult_2)
lp15@59751
  1376
  done
lp15@59751
  1377
wenzelm@63589
  1378
lemma Ln_minus1 [simp]: "Ln(-1) = \<i> * pi"
lp15@59751
  1379
  apply (rule exp_complex_eqI)
lp15@59751
  1380
  using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
lp15@59751
  1381
  apply (auto simp: abs_if)
lp15@59751
  1382
  done
lp15@59751
  1383
wenzelm@63589
  1384
lemma Ln_ii [simp]: "Ln \<i> = \<i> * of_real pi/2"
wenzelm@63589
  1385
  using Ln_exp [of "\<i> * (of_real pi/2)"]
lp15@59751
  1386
  unfolding exp_Euler
lp15@59751
  1387
  by simp
lp15@59751
  1388
wenzelm@63589
  1389
lemma Ln_minus_ii [simp]: "Ln(-\<i>) = - (\<i> * pi/2)"
lp15@59751
  1390
proof -
wenzelm@63589
  1391
  have  "Ln(-\<i>) = Ln(inverse \<i>)"    by simp
wenzelm@63589
  1392
  also have "... = - (Ln \<i>)"         using Ln_inverse by blast
wenzelm@63589
  1393
  also have "... = - (\<i> * pi/2)"     by simp
lp15@59751
  1394
  finally show ?thesis .
lp15@59751
  1395
qed
lp15@59751
  1396
lp15@59751
  1397
lemma Ln_times:
lp15@59751
  1398
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59751
  1399
    shows "Ln(w * z) =
lp15@59751
  1400
                (if Im(Ln w + Ln z) \<le> -pi then
wenzelm@63589
  1401
                  (Ln(w) + Ln(z)) + \<i> * of_real(2*pi)
lp15@59751
  1402
                else if Im(Ln w + Ln z) > pi then
wenzelm@63589
  1403
                  (Ln(w) + Ln(z)) - \<i> * of_real(2*pi)
lp15@59751
  1404
                else Ln(w) + Ln(z))"
lp15@59751
  1405
  using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
lp15@59751
  1406
  using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
paulson@62131
  1407
  by (auto simp: exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
lp15@59751
  1408
lp15@60150
  1409
corollary Ln_times_simple:
lp15@59751
  1410
    "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
lp15@59751
  1411
         \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
lp15@59751
  1412
  by (simp add: Ln_times)
lp15@59751
  1413
lp15@60150
  1414
corollary Ln_times_of_real:
lp15@60150
  1415
    "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(of_real r * z) = ln r + Ln(z)"
lp15@60150
  1416
  using mpi_less_Im_Ln Im_Ln_le_pi
lp15@60150
  1417
  by (force simp: Ln_times)
lp15@60150
  1418
lp15@60150
  1419
corollary Ln_divide_of_real:
lp15@60150
  1420
    "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
lp15@60150
  1421
using Ln_times_of_real [of "inverse r" z]
lp15@61609
  1422
by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric]
lp15@60150
  1423
         del: of_real_inverse)
lp15@60150
  1424
lp15@59751
  1425
lemma Ln_minus:
lp15@59751
  1426
  assumes "z \<noteq> 0"
lp15@59751
  1427
    shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
wenzelm@63589
  1428
                     then Ln(z) + \<i> * pi
wenzelm@63589
  1429
                     else Ln(z) - \<i> * pi)" (is "_ = ?rhs")
lp15@59751
  1430
  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
lp15@59751
  1431
        Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
paulson@62131
  1432
    by (fastforce simp: exp_add exp_diff exp_Euler intro!: Ln_unique)
lp15@59751
  1433
lp15@59751
  1434
lemma Ln_inverse_if:
lp15@59751
  1435
  assumes "z \<noteq> 0"
paulson@62131
  1436
    shows "Ln (inverse z) = (if z \<in> \<real>\<^sub>\<le>\<^sub>0 then -(Ln z) + \<i> * 2 * complex_of_real pi else -(Ln z))"
paulson@62131
  1437
proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
paulson@62131
  1438
  case False then show ?thesis
lp15@59751
  1439
    by (simp add: Ln_inverse)
lp15@59751
  1440
next
paulson@62131
  1441
  case True
lp15@59751
  1442
  then have z: "Im z = 0" "Re z < 0"
lp15@59751
  1443
    using assms
paulson@62131
  1444
    apply (auto simp: complex_nonpos_Reals_iff)
paulson@62131
  1445
    by (metis complex_is_Real_iff le_imp_less_or_eq of_real_0 of_real_Re)
lp15@59751
  1446
  have "Ln(inverse z) = Ln(- (inverse (-z)))"
lp15@59751
  1447
    by simp
lp15@59751
  1448
  also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
lp15@59751
  1449
    using assms z
lp15@59751
  1450
    apply (simp add: Ln_minus)
lp15@59751
  1451
    apply (simp add: field_simps)
lp15@59751
  1452
    done
lp15@59751
  1453
  also have "... = - Ln (- z) + \<i> * complex_of_real pi"
lp15@59751
  1454
    apply (subst Ln_inverse)
lp15@62534
  1455
    using z by (auto simp add: complex_nonneg_Reals_iff)
lp15@59751
  1456
  also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
lp15@59751
  1457
    apply (subst Ln_minus [OF assms])
lp15@59751
  1458
    using assms z
lp15@59751
  1459
    apply simp
lp15@59751
  1460
    done
paulson@62131
  1461
  finally show ?thesis by (simp add: True)
lp15@59751
  1462
qed
lp15@59751
  1463
lp15@59751
  1464
lemma Ln_times_ii:
lp15@59751
  1465
  assumes "z \<noteq> 0"
wenzelm@63589
  1466
    shows  "Ln(\<i> * z) = (if 0 \<le> Re(z) | Im(z) < 0
wenzelm@63589
  1467
                          then Ln(z) + \<i> * of_real pi/2
wenzelm@63589
  1468
                          else Ln(z) - \<i> * of_real(3 * pi/2))"
lp15@59751
  1469
  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
lp15@59751
  1470
        Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
lp15@65064
  1471
  by (simp add: Ln_times) auto
lp15@59751
  1472
lp15@65587
  1473
lemma Ln_of_nat [simp]: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
eberlm@61524
  1474
  by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
eberlm@61524
  1475
lp15@61609
  1476
lemma Ln_of_nat_over_of_nat:
eberlm@61524
  1477
  assumes "m > 0" "n > 0"
eberlm@61524
  1478
  shows   "Ln (of_nat m / of_nat n) = of_real (ln (of_nat m) - ln (of_nat n))"
eberlm@61524
  1479
proof -
eberlm@61524
  1480
  have "of_nat m / of_nat n = (of_real (of_nat m / of_nat n) :: complex)" by simp
eberlm@61524
  1481
  also from assms have "Ln ... = of_real (ln (of_nat m / of_nat n))"
eberlm@61524
  1482
    by (simp add: Ln_of_real[symmetric])
eberlm@61524
  1483
  also from assms have "... = of_real (ln (of_nat m) - ln (of_nat n))"
eberlm@61524
  1484
    by (simp add: ln_div)
eberlm@61524
  1485
  finally show ?thesis .
eberlm@61524
  1486
qed
eberlm@61524
  1487
lp15@59751
  1488
wenzelm@60420
  1489
subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
lp15@60150
  1490
lp15@61609
  1491
lemma Arg_Ln:
lp15@60150
  1492
  assumes "0 < Arg z" shows "Arg z = Im(Ln(-z)) + pi"
lp15@60150
  1493
proof (cases "z = 0")
lp15@60150
  1494
  case True
lp15@60150
  1495
  with assms show ?thesis
lp15@60150
  1496
    by simp
lp15@60150
  1497
next
lp15@60150
  1498
  case False
wenzelm@63589
  1499
  then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
lp15@60150
  1500
    using Arg [of z]
haftmann@64240
  1501
    by (metis abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
lp15@60150
  1502
  then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
lp15@60150
  1503
    using cis_conv_exp cis_pi
lp15@60150
  1504
    by (auto simp: exp_diff algebra_simps)
lp15@60150
  1505
  then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg z) - pi)))"
lp15@60150
  1506
    by simp
lp15@60150
  1507
  also have "... = \<i> * (of_real(Arg z) - pi)"
lp15@60150
  1508
    using Arg [of z] assms pi_not_less_zero
lp15@60150
  1509
    by auto
lp15@60150
  1510
  finally have "Arg z =  Im (Ln (- z / of_real (cmod z))) + pi"
lp15@60150
  1511
    by simp
lp15@60150
  1512
  also have "... = Im (Ln (-z) - ln (cmod z)) + pi"
lp15@60150
  1513
    by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)
lp15@60150
  1514
  also have "... = Im (Ln (-z)) + pi"
lp15@60150
  1515
    by simp
lp15@60150
  1516
  finally show ?thesis .
lp15@60150
  1517
qed
lp15@60150
  1518
lp15@61609
  1519
lemma continuous_at_Arg:
paulson@62131
  1520
  assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
lp15@60150
  1521
    shows "continuous (at z) Arg"
lp15@60150
  1522
proof -
lp15@60150
  1523
  have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
lp15@60150
  1524
    by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
paulson@62131
  1525
  have [simp]: "\<And>x. \<lbrakk>Im x \<noteq> 0\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg x"
paulson@62131
  1526
      using Arg_Ln Arg_gt_0 complex_is_Real_iff by auto
paulson@62131
  1527
  consider "Re z < 0" | "Im z \<noteq> 0" using assms
lp15@62534
  1528
    using complex_nonneg_Reals_iff not_le by blast
paulson@62131
  1529
  then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg z"
paulson@62131
  1530
      using "*"  by (simp add: isCont_def) (metis Arg_Ln Arg_gt_0 complex_is_Real_iff)
paulson@62131
  1531
  show ?thesis
paulson@62131
  1532
      apply (simp add: continuous_at)
paulson@62131
  1533
      apply (rule Lim_transform_within_open [where s= "-\<real>\<^sub>\<ge>\<^sub>0" and f = "\<lambda>z. Im(Ln(-z)) + pi"])
paulson@62131
  1534
      apply (auto simp add: not_le Arg_Ln [OF Arg_gt_0] complex_nonneg_Reals_iff closed_def [symmetric])
paulson@62131
  1535
      using assms apply (force simp add: complex_nonneg_Reals_iff)
paulson@62131
  1536
      done
lp15@60150
  1537
qed
lp15@60150
  1538
eberlm@62049
  1539
lemma Ln_series:
eberlm@62049
  1540
  fixes z :: complex
eberlm@62049
  1541
  assumes "norm z < 1"
eberlm@62049
  1542
  shows   "(\<lambda>n. (-1)^Suc n / of_nat n * z^n) sums ln (1 + z)" (is "(\<lambda>n. ?f n * z^n) sums _")
eberlm@62049
  1543
proof -
eberlm@62049
  1544
  let ?F = "\<lambda>z. \<Sum>n. ?f n * z^n" and ?F' = "\<lambda>z. \<Sum>n. diffs ?f n * z^n"
eberlm@62049
  1545
  have r: "conv_radius ?f = 1"
eberlm@62049
  1546
    by (intro conv_radius_ratio_limit_nonzero[of _ 1])
eberlm@62049
  1547
       (simp_all add: norm_divide LIMSEQ_Suc_n_over_n del: of_nat_Suc)
eberlm@62049
  1548
eberlm@62049
  1549
  have "\<exists>c. \<forall>z\<in>ball 0 1. ln (1 + z) - ?F z = c"
eberlm@62049
  1550
  proof (rule has_field_derivative_zero_constant)
eberlm@62049
  1551
    fix z :: complex assume z': "z \<in> ball 0 1"
eberlm@62049
  1552
    hence z: "norm z < 1" by (simp add: dist_0_norm)
wenzelm@63040
  1553
    define t :: complex where "t = of_real (1 + norm z) / 2"
eberlm@62049
  1554
    from z have t: "norm z < norm t" "norm t < 1" unfolding t_def
eberlm@62049
  1555
      by (simp_all add: field_simps norm_divide del: of_real_add)
eberlm@62049
  1556
eberlm@62049
  1557
    have "Re (-z) \<le> norm (-z)" by (rule complex_Re_le_cmod)
eberlm@62049
  1558
    also from z have "... < 1" by simp
eberlm@62049
  1559
    finally have "((\<lambda>z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)"
paulson@62131
  1560
      by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
eberlm@62049
  1561
    moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
eberlm@62049
  1562
      by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all
lp15@62534
  1563
    ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))
eberlm@62049
  1564
                       (at z within ball 0 1)"
eberlm@62049
  1565
      by (intro derivative_intros) (simp_all add: at_within_open[OF z'])
eberlm@62049
  1566
    also have "(\<lambda>n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r
eberlm@62049
  1567
      by (intro diffs_equiv termdiff_converges[OF t(1)] summable_in_conv_radius) simp_all
eberlm@62049
  1568
    from sums_split_initial_segment[OF this, of 1]
eberlm@62049
  1569
      have "(\<lambda>i. (-z) ^ i) sums ?F' z" by (simp add: power_minus[of z] del: of_nat_Suc)
eberlm@62049
  1570
    hence "?F' z = inverse (1 + z)" using z by (simp add: sums_iff suminf_geometric divide_inverse)
eberlm@62049
  1571
    also have "inverse (1 + z) - inverse (1 + z) = 0" by simp
eberlm@62049
  1572
    finally show "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative 0) (at z within ball 0 1)" .
eberlm@62049
  1573
  qed simp_all
eberlm@62049
  1574
  then obtain c where c: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> ln (1 + z) - ?F z = c" by blast
eberlm@62049
  1575
  from c[of 0] have "c = 0" by (simp only: powser_zero) simp
eberlm@62049
  1576
  with c[of z] assms have "ln (1 + z) = ?F z" by (simp add: dist_0_norm)
eberlm@62049
  1577
  moreover have "summable (\<lambda>n. ?f n * z^n)" using assms r
eberlm@62049
  1578
    by (intro summable_in_conv_radius) simp_all
eberlm@62049
  1579
  ultimately show ?thesis by (simp add: sums_iff)
eberlm@62049
  1580
qed
eberlm@62049
  1581
eberlm@63721
  1582
lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
eberlm@63721
  1583
  by (drule Ln_series) (simp add: power_minus')
eberlm@63721
  1584
lp15@65064
  1585
lemma ln_series':
eberlm@63721
  1586
  assumes "abs (x::real) < 1"
eberlm@63721
  1587
  shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
eberlm@63721
  1588
proof -
eberlm@63721
  1589
  from assms have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
eberlm@63721
  1590
    by (intro Ln_series') simp_all
eberlm@63721
  1591
  also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
eberlm@63721
  1592
    by (rule ext) simp
lp15@65064
  1593
  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"
eberlm@63721
  1594
    by (subst Ln_of_real [symmetric]) simp_all
eberlm@63721
  1595
  finally show ?thesis by (subst (asm) sums_of_real_iff)
eberlm@63721
  1596
qed
eberlm@63721
  1597
eberlm@62049
  1598
lemma Ln_approx_linear:
eberlm@62049
  1599
  fixes z :: complex
eberlm@62049
  1600
  assumes "norm z < 1"
eberlm@62049
  1601
  shows   "norm (ln (1 + z) - z) \<le> norm z^2 / (1 - norm z)"
eberlm@62049
  1602
proof -
eberlm@62049
  1603
  let ?f = "\<lambda>n. (-1)^Suc n / of_nat n"
eberlm@62049
  1604
  from assms have "(\<lambda>n. ?f n * z^n) sums ln (1 + z)" using Ln_series by simp
eberlm@62049
  1605
  moreover have "(\<lambda>n. (if n = 1 then 1 else 0) * z^n) sums z" using powser_sums_if[of 1] by simp
eberlm@62049
  1606
  ultimately have "(\<lambda>n. (?f n - (if n = 1 then 1 else 0)) * z^n) sums (ln (1 + z) - z)"
eberlm@62049
  1607
    by (subst left_diff_distrib, intro sums_diff) simp_all
eberlm@62049
  1608
  from sums_split_initial_segment[OF this, of "Suc 1"]
eberlm@62049
  1609
    have "(\<lambda>i. (-(z^2)) * inverse (2 + of_nat i) * (- z)^i) sums (Ln (1 + z) - z)"
eberlm@62049
  1610
    by (simp add: power2_eq_square mult_ac power_minus[of z] divide_inverse)
eberlm@62049
  1611
  hence "(Ln (1 + z) - z) = (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)"
eberlm@62049
  1612
    by (simp add: sums_iff)
eberlm@62049
  1613
  also have A: "summable (\<lambda>n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"
eberlm@62049
  1614
    by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])
eberlm@62049
  1615
       (auto simp: assms field_simps intro!: always_eventually)
lp15@62534
  1616
  hence "norm (\<Sum>i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \<le>
eberlm@62049
  1617
             (\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"
eberlm@62049
  1618
    by (intro summable_norm)
eberlm@62049
  1619
       (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)
eberlm@62049
  1620
  also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \<le> norm ((-z)^2 * (-z)^i) * 1" for i
eberlm@62049
  1621
    by (intro mult_left_mono) (simp_all add: divide_simps)
lp15@62534
  1622
  hence "(\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i)) \<le>
eberlm@62049
  1623
           (\<Sum>i. norm (-(z^2) * (-z)^i))" using A assms
eberlm@62049
  1624
    apply (simp_all only: norm_power norm_inverse norm_divide norm_mult)
eberlm@62049
  1625
    apply (intro suminf_le summable_mult summable_geometric)
eberlm@62049
  1626
    apply (auto simp: norm_power field_simps simp del: of_nat_add of_nat_Suc)
eberlm@62049
  1627
    done
eberlm@62049
  1628
  also have "... = norm z^2 * (\<Sum>i. norm z^i)" using assms
eberlm@62049
  1629
    by (subst suminf_mult [symmetric]) (auto intro!: summable_geometric simp: norm_mult norm_power)
eberlm@62049
  1630
  also have "(\<Sum>i. norm z^i) = inverse (1 - norm z)" using assms
eberlm@62049
  1631
    by (subst suminf_geometric) (simp_all add: divide_inverse)
eberlm@62049
  1632
  also have "norm z^2 * ... = norm z^2 / (1 - norm z)" by (simp add: divide_inverse)
eberlm@62049
  1633
  finally show ?thesis .
eberlm@62049
  1634
qed
eberlm@62049
  1635
eberlm@62049
  1636
wenzelm@60420
  1637
text\<open>Relation between Arg and arctangent in upper halfplane\<close>
lp15@61609
  1638
lemma Arg_arctan_upperhalf:
lp15@60150
  1639
  assumes "0 < Im z"
lp15@60150
  1640
    shows "Arg z = pi/2 - arctan(Re z / Im z)"
lp15@60150
  1641
proof (cases "z = 0")
lp15@60150
  1642
  case True with assms show ?thesis
lp15@60150
  1643
    by simp
lp15@60150
  1644
next
lp15@60150
  1645
  case False
lp15@60150
  1646
  show ?thesis
lp15@60150
  1647
    apply (rule Arg_unique [of "norm z"])
lp15@60150
  1648
    using False assms arctan [of "Re z / Im z"] pi_ge_two pi_half_less_two
lp15@60150
  1649
    apply (auto simp: exp_Euler cos_diff sin_diff)
lp15@60150
  1650
    using norm_complex_def [of z, symmetric]
paulson@62131
  1651
    apply (simp add: sin_of_real cos_of_real sin_arctan cos_arctan field_simps real_sqrt_divide)
lp15@60150
  1652
    apply (metis complex_eq mult.assoc ring_class.ring_distribs(2))
lp15@60150
  1653
    done
lp15@60150
  1654
qed
lp15@60150
  1655
lp15@61609
  1656
lemma Arg_eq_Im_Ln:
lp15@61609
  1657
  assumes "0 \<le> Im z" "0 < Re z"
lp15@60150
  1658
    shows "Arg z = Im (Ln z)"
lp15@60150
  1659
proof (cases "z = 0 \<or> Im z = 0")
lp15@60150
  1660
  case True then show ?thesis
lp15@61609
  1661
    using assms Arg_eq_0 complex_is_Real_iff
lp15@60150
  1662
    apply auto
lp15@60150
  1663
    by (metis Arg_eq_0_pi Arg_eq_pi Im_Ln_eq_0 Im_Ln_eq_pi less_numeral_extra(3) zero_complex.simps(1))
lp15@60150
  1664
next
lp15@61609
  1665
  case False
lp15@60150
  1666
  then have "Arg z > 0"
lp15@60150
  1667
    using Arg_gt_0 complex_is_Real_iff by blast
lp15@60150
  1668
  then show ?thesis
lp15@61609
  1669
    using assms False
lp15@60150
  1670
    by (subst Arg_Ln) (auto simp: Ln_minus)
lp15@60150
  1671
qed
lp15@60150
  1672
lp15@61609
  1673
lemma continuous_within_upperhalf_Arg:
lp15@60150
  1674
  assumes "z \<noteq> 0"
lp15@60150
  1675
    shows "continuous (at z within {z. 0 \<le> Im z}) Arg"
paulson@62131
  1676
proof (cases "z \<in> \<real>\<^sub>\<ge>\<^sub>0")
lp15@60150
  1677
  case False then show ?thesis
lp15@60150
  1678
    using continuous_at_Arg continuous_at_imp_continuous_within by auto
lp15@60150
  1679
next
lp15@60150
  1680
  case True
lp15@60150
  1681
  then have z: "z \<in> \<real>" "0 < Re z"
paulson@62131
  1682
    using assms  by (auto simp: complex_nonneg_Reals_iff complex_is_Real_iff complex_neq_0)
lp15@60150
  1683
  then have [simp]: "Arg z = 0" "Im (Ln z) = 0"
lp15@60150
  1684
    by (auto simp: Arg_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
lp15@61609
  1685
  show ?thesis
lp15@60150
  1686
  proof (clarsimp simp add: continuous_within Lim_within dist_norm)
lp15@60150
  1687
    fix e::real
lp15@60150
  1688
    assume "0 < e"
lp15@60150
  1689
    moreover have "continuous (at z) (\<lambda>x. Im (Ln x))"
paulson@62131
  1690
      using z by (simp add: continuous_at_Ln complex_nonpos_Reals_iff)
lp15@60150
  1691
    ultimately
lp15@60150
  1692
    obtain d where d: "d>0" "\<And>x. x \<noteq> z \<Longrightarrow> cmod (x - z) < d \<Longrightarrow> \<bar>Im (Ln x)\<bar> < e"
lp15@60150
  1693
      by (auto simp: continuous_within Lim_within dist_norm)
lp15@60150
  1694
    { fix x
lp15@60150
  1695
      assume "cmod (x - z) < Re z / 2"
lp15@60150
  1696
      then have "\<bar>Re x - Re z\<bar> < Re z / 2"
lp15@60150
  1697
        by (metis le_less_trans abs_Re_le_cmod minus_complex.simps(1))
lp15@60150
  1698
      then have "0 < Re x"
lp15@60150
  1699
        using z by linarith
lp15@60150
  1700
    }
lp15@60150
  1701
    then show "\<exists>d>0. \<forall>x. 0 \<le> Im x \<longrightarrow> x \<noteq> z \<and> cmod (x - z) < d \<longrightarrow> \<bar>Arg x\<bar> < e"
lp15@60150
  1702
      apply (rule_tac x="min d (Re z / 2)" in exI)
lp15@60150
  1703
      using z d
lp15@60150
  1704
      apply (auto simp: Arg_eq_Im_Ln)
lp15@60150
  1705
      done
lp15@60150
  1706
  qed
lp15@60150
  1707
qed
lp15@60150
  1708
lp15@60150
  1709
lemma continuous_on_upperhalf_Arg: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg"
lp15@60150
  1710
  apply (auto simp: continuous_on_eq_continuous_within)
lp15@60150
  1711
  by (metis Diff_subset continuous_within_subset continuous_within_upperhalf_Arg)
lp15@60150
  1712
lp15@61609
  1713
lemma open_Arg_less_Int:
lp15@60150
  1714
  assumes "0 \<le> s" "t \<le> 2*pi"
lp15@60150
  1715
    shows "open ({y. s < Arg y} \<inter> {y. Arg y < t})"
lp15@60150
  1716
proof -
paulson@62131
  1717
  have 1: "continuous_on (UNIV - \<real>\<^sub>\<ge>\<^sub>0) Arg"
lp15@61609
  1718
    using continuous_at_Arg continuous_at_imp_continuous_within
paulson@62131
  1719
    by (auto simp: continuous_on_eq_continuous_within)
paulson@62131
  1720
  have 2: "open (UNIV - \<real>\<^sub>\<ge>\<^sub>0 :: complex set)"  by (simp add: open_Diff)
lp15@60150
  1721
  have "open ({z. s < z} \<inter> {z. z < t})"
lp15@60150
  1722
    using open_lessThan [of t] open_greaterThan [of s]
lp15@60150
  1723
    by (metis greaterThan_def lessThan_def open_Int)
paulson@62131
  1724
  moreover have "{y. s < Arg y} \<inter> {y. Arg y < t} \<subseteq> - \<real>\<^sub>\<ge>\<^sub>0"
paulson@62131
  1725
    using assms by (auto simp: Arg_real complex_nonneg_Reals_iff complex_is_Real_iff)
lp15@60150
  1726
  ultimately show ?thesis
lp15@61609
  1727
    using continuous_imp_open_vimage [OF 1 2, of  "{z. Re z > s} \<inter> {z. Re z < t}"]
lp15@60150
  1728
    by auto
lp15@60150
  1729
qed
lp15@60150
  1730
lp15@60150
  1731
lemma open_Arg_gt: "open {z. t < Arg z}"
lp15@60150
  1732
proof (cases "t < 0")
lp15@60150
  1733
  case True then have "{z. t < Arg z} = UNIV"
lp15@60150
  1734
    using Arg_ge_0 less_le_trans by auto
lp15@60150
  1735
  then show ?thesis
lp15@60150
  1736
    by simp
lp15@60150
  1737
next
lp15@60150
  1738
  case False then show ?thesis
lp15@60150
  1739
    using open_Arg_less_Int [of t "2*pi"] Arg_lt_2pi
lp15@60150
  1740
    by auto
lp15@60150
  1741
qed
lp15@60150
  1742
lp15@60150
  1743
lemma closed_Arg_le: "closed {z. Arg z \<le> t}"
lp15@60150
  1744
  using open_Arg_gt [of t]
lp15@60150
  1745
  by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)
lp15@60017
  1746
wenzelm@60420
  1747
subsection\<open>Complex Powers\<close>
lp15@60017
  1748
lp15@60017
  1749
lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
lp15@60020
  1750
  by (simp add: powr_def)
lp15@60017
  1751
lp15@60017
  1752
lemma powr_nat:
lp15@60017
  1753
  fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
lp15@60020
  1754
  by (simp add: exp_of_nat_mult powr_def)
lp15@60017
  1755
lp15@60017
  1756
lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
lp15@60020
  1757
  apply (simp add: powr_def)
lp15@60017
  1758
  using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
lp15@60017
  1759
  by auto
lp15@60017
  1760
lp15@65583
  1761
lemma powr_complexpow [simp]:
lp15@65583
  1762
  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (of_nat n) = x^n"
lp15@65583
  1763
  by (induct n) (auto simp: ac_simps powr_add)
lp15@65583
  1764
lp15@65583
  1765
lemma powr_complexnumeral [simp]:
lp15@65583
  1766
  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (numeral n) = x ^ (numeral n)"
lp15@65583
  1767
  by (metis of_nat_numeral powr_complexpow)
lp15@65583
  1768
eberlm@61524
  1769
lemma cnj_powr:
eberlm@61524
  1770
  assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"
eberlm@61524
  1771
  shows   "cnj (a powr b) = cnj a powr cnj b"
eberlm@61524
  1772
proof (cases "a = 0")
eberlm@61524
  1773
  case False
paulson@62131
  1774
  with assms have "a \<notin> \<real>\<^sub>\<le>\<^sub>0" by (auto simp: complex_eq_iff complex_nonpos_Reals_iff)
eberlm@61524
  1775
  with False show ?thesis by (simp add: powr_def exp_cnj cnj_Ln)
eberlm@61524
  1776
qed simp
eberlm@61524
  1777
lp15@60017
  1778
lemma powr_real_real:
lp15@60017
  1779
    "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
lp15@60020
  1780
  apply (simp add: powr_def)
lp15@60017
  1781
  by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
lp15@60017
  1782
       exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
lp15@60017
  1783
lp15@60017
  1784
lemma powr_of_real:
lp15@60020
  1785
  fixes x::real and y::real
eberlm@63296
  1786
  shows "0 \<le> x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
eberlm@63296
  1787
  by (simp_all add: powr_def exp_eq_polar)
lp15@60017
  1788
lp15@65719
  1789
lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
lp15@65719
  1790
  by (metis linear not_le of_real_Re powr_of_real)
lp15@65719
  1791
lp15@60017
  1792
lemma norm_powr_real_mono:
lp15@60020
  1793
    "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
lp15@60020
  1794
     \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
lp15@60020
  1795
  by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
lp15@60017
  1796
lp15@60017
  1797
lemma powr_times_real:
lp15@60017
  1798
    "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
lp15@60017
  1799
           \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
lp15@60020
  1800
  by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
lp15@60017
  1801
lp15@65719
  1802
lemma Re_powr_le: "r \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> Re (r powr z) \<le> Re r powr Re z"
lp15@65719
  1803
  by (auto simp: powr_def nonneg_Reals_def order_trans [OF complex_Re_le_cmod])
lp15@65719
  1804
lp15@65719
  1805
lemma
lp15@65719
  1806
  fixes w::complex
lp15@65719
  1807
  shows Reals_powr [simp]: "\<lbrakk>w \<in> \<real>\<^sub>\<ge>\<^sub>0; z \<in> \<real>\<rbrakk> \<Longrightarrow> w powr z \<in> \<real>"
lp15@65719
  1808
  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"
lp15@65719
  1809
  by (auto simp: nonneg_Reals_def Reals_def powr_of_real)
lp15@65719
  1810
eberlm@61524
  1811
lemma powr_neg_real_complex:
eberlm@61524
  1812
  shows   "(- of_real x) powr a = (-1) powr (of_real (sgn x) * a) * of_real x powr (a :: complex)"
eberlm@61524
  1813
proof (cases "x = 0")
eberlm@61524
  1814
  assume x: "x \<noteq> 0"
eberlm@61524
  1815
  hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)
eberlm@61524
  1816
  also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \<i>"
eberlm@61524
  1817
    by (simp add: Ln_minus Ln_of_real)
wenzelm@63092
  1818
  also from x have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
eberlm@61524
  1819
    by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)
eberlm@61524
  1820
  also note cis_pi
eberlm@61524
  1821
  finally show ?thesis by simp
eberlm@61524
  1822
qed simp_all
eberlm@61524
  1823
lp15@60017
  1824
lemma has_field_derivative_powr:
paulson@62131
  1825
  fixes z :: complex
paulson@62131
  1826
  shows "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
lp15@60017
  1827
  apply (cases "z=0", auto)
lp15@60020
  1828
  apply (simp add: powr_def)
lp15@60017
  1829
  apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
lp15@60020
  1830
  apply (auto simp: dist_complex_def)
wenzelm@63092
  1831
  apply (intro derivative_eq_intros | simp)+
lp15@60017
  1832
  apply (simp add: field_simps exp_diff)
lp15@60017
  1833
  done
lp15@60017
  1834
paulson@62131
  1835
declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
eberlm@61524
  1836
eberlm@61524
  1837
lp15@65578
  1838
lemma has_field_derivative_powr_right [derivative_intros]:
lp15@60017
  1839
    "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
lp15@60020
  1840
  apply (simp add: powr_def)
wenzelm@63092
  1841
  apply (intro derivative_eq_intros | simp)+
lp15@60017
  1842
  done
lp15@60017
  1843
lp15@65583
  1844
lemma field_differentiable_powr_right [derivative_intros]:
lp15@62533
  1845
  fixes w::complex
lp15@65583
  1846
  shows "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
lp15@62534
  1847
using field_differentiable_def has_field_derivative_powr_right by blast
lp15@60017
  1848
lp15@65583
  1849
lemma holomorphic_on_powr_right [holomorphic_intros]:
lp15@60017
  1850
    "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
lp15@65583
  1851
  unfolding holomorphic_on_def field_differentiable_def
lp15@65583
  1852
  by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
lp15@60017
  1853
lp15@60017
  1854
lemma norm_powr_real_powr:
eberlm@63295
  1855
  "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
hoelzl@63594
  1856
  by (cases "w = 0") (auto simp add: norm_powr_real powr_def Im_Ln_eq_0
eberlm@63295
  1857
                                     complex_is_Real_iff in_Reals_norm complex_eq_iff)
eberlm@63295
  1858
eberlm@63295
  1859
lemma tendsto_ln_complex [tendsto_intros]:
eberlm@63295
  1860
  assumes "(f \<longlongrightarrow> a) F" "a \<notin> \<real>\<^sub>\<le>\<^sub>0"
eberlm@63295
  1861
  shows   "((\<lambda>z. ln (f z :: complex)) \<longlongrightarrow> ln a) F"
eberlm@63295
  1862
  using tendsto_compose[OF continuous_at_Ln[of a, unfolded isCont_def] assms(1)] assms(2) by simp
eberlm@63295
  1863
eberlm@63295
  1864
lemma tendsto_powr_complex:
eberlm@63295
  1865
  fixes f g :: "_ \<Rightarrow> complex"
eberlm@63295
  1866
  assumes a: "a \<notin> \<real>\<^sub>\<le>\<^sub>0"
eberlm@63295
  1867
  assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F"
eberlm@63295
  1868
  shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
eberlm@63295
  1869
proof -
eberlm@63295
  1870
  from a have [simp]: "a \<noteq> 0" by auto
eberlm@63295
  1871
  from f g a have "((\<lambda>z. exp (g z * ln (f z))) \<longlongrightarrow> a powr b) F" (is ?P)
eberlm@63295
  1872
    by (auto intro!: tendsto_intros simp: powr_def)
eberlm@63295
  1873
  also {
eberlm@63295
  1874
    have "eventually (\<lambda>z. z \<noteq> 0) (nhds a)"
eberlm@63295
  1875
      by (intro t1_space_nhds) simp_all
eberlm@63295
  1876
    with f have "eventually (\<lambda>z. f z \<noteq> 0) F" using filterlim_iff by blast
eberlm@63295
  1877
  }
eberlm@63295
  1878
  hence "?P \<longleftrightarrow> ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
eberlm@63295
  1879
    by (intro tendsto_cong refl) (simp_all add: powr_def mult_ac)
eberlm@63295
  1880
  finally show ?thesis .
eberlm@63295
  1881
qed
eberlm@63295
  1882
eberlm@63295
  1883
lemma tendsto_powr_complex_0:
eberlm@63295
  1884
  fixes f g :: "'a \<Rightarrow> complex"
eberlm@63295
  1885
  assumes f: "(f \<longlongrightarrow> 0) F" and g: "(g \<longlongrightarrow> b) F" and b: "Re b > 0"
eberlm@63295
  1886
  shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> 0) F"
eberlm@63295
  1887
proof (rule tendsto_norm_zero_cancel)
eberlm@63295
  1888
  define h where
eberlm@63295
  1889
    "h = (\<lambda>z. if f z = 0 then 0 else exp (Re (g z) * ln (cmod (f z)) + abs (Im (g z)) * pi))"
eberlm@63295
  1890
  {
eberlm@63295
  1891
    fix z :: 'a assume z: "f z \<noteq> 0"
eberlm@63295
  1892
    define c where "c = abs (Im (g z)) * pi"
eberlm@63295
  1893
    from mpi_less_Im_Ln[OF z] Im_Ln_le_pi[OF z]
eberlm@63295
  1894
      have "abs (Im (Ln (f z))) \<le> pi" by simp
eberlm@63295
  1895
    from mult_left_mono[OF this, of "abs (Im (g z))"]
eberlm@63295
  1896
      have "abs (Im (g z) * Im (ln (f z))) \<le> c" by (simp add: abs_mult c_def)
eberlm@63295
  1897
    hence "-Im (g z) * Im (ln (f z)) \<le> c" by simp
eberlm@63295
  1898
    hence "norm (f z powr g z) \<le> h z" by (simp add: powr_def field_simps h_def c_def)
eberlm@63295
  1899
  }
eberlm@63295
  1900
  hence le: "norm (f z powr g z) \<le> h z" for z by (cases "f x = 0") (simp_all add: h_def)
eberlm@63295
  1901
eberlm@63295
  1902
  have g': "(g \<longlongrightarrow> b) (inf F (principal {z. f z \<noteq> 0}))"
eberlm@63295
  1903
    by (rule tendsto_mono[OF _ g]) simp_all
eberlm@63295
  1904
  have "((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) (inf F (principal {z. f z \<noteq> 0}))"
eberlm@63295
  1905
    by (subst tendsto_norm_zero_iff, rule tendsto_mono[OF _ f]) simp_all
eberlm@63295
  1906
  moreover {
eberlm@63295
  1907
    have "filterlim (\<lambda>x. norm (f x)) (principal {0<..}) (principal {z. f z \<noteq> 0})"
eberlm@63295
  1908
      by (auto simp: filterlim_def)
eberlm@63295
  1909
    hence "filterlim (\<lambda>x. norm (f x)) (principal {0<..})
eberlm@63295
  1910
             (inf F (principal {z. f z \<noteq> 0}))"
eberlm@63295
  1911
      by (rule filterlim_mono) simp_all
eberlm@63295
  1912
  }
eberlm@63295
  1913
  ultimately have norm: "filterlim (\<lambda>x. norm (f x)) (at_right 0) (inf F (principal {z. f z \<noteq> 0}))"
eberlm@63295
  1914
    by (simp add: filterlim_inf at_within_def)
eberlm@63295
  1915
eberlm@63295
  1916
  have A: "LIM x inf F (principal {z. f z \<noteq> 0}). Re (g x) * -ln (cmod (f x)) :> at_top"
eberlm@63295
  1917
    by (rule filterlim_tendsto_pos_mult_at_top tendsto_intros g' b
eberlm@63295
  1918
          filterlim_compose[OF filterlim_uminus_at_top_at_bot] filterlim_compose[OF ln_at_0] norm)+
eberlm@63295
  1919
  have B: "LIM x inf F (principal {z. f z \<noteq> 0}).
eberlm@63295
  1920
          -\<bar>Im (g x)\<bar> * pi + -(Re (g x) * ln (cmod (f x))) :> at_top"
eberlm@63295
  1921
    by (rule filterlim_tendsto_add_at_top tendsto_intros g')+ (insert A, simp_all)
eberlm@63295
  1922
  have C: "(h \<longlongrightarrow> 0) F" unfolding h_def
eberlm@63295
  1923
    by (intro filterlim_If tendsto_const filterlim_compose[OF exp_at_bot])
eberlm@63295
  1924
       (insert B, auto simp: filterlim_uminus_at_bot algebra_simps)
eberlm@63295
  1925
  show "((\<lambda>x. norm (f x powr g x)) \<longlongrightarrow> 0) F"
eberlm@63295
  1926
    by (rule Lim_null_comparison[OF always_eventually C]) (insert le, auto)
eberlm@63295
  1927
qed
eberlm@63295
  1928
eberlm@63295
  1929
lemma tendsto_powr_complex' [tendsto_intros]:
eberlm@63295
  1930
  fixes f g :: "_ \<Rightarrow> complex"
eberlm@63295
  1931
  assumes fz: "a \<notin> \<real>\<^sub>\<le>\<^sub>0 \<or> (a = 0 \<and> Re b > 0)"
eberlm@63295
  1932
  assumes fg: "(f \<longlongrightarrow> a) F" "(g \<longlongrightarrow> b) F"
eberlm@63295
  1933
  shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
eberlm@63295
  1934
proof (cases "a = 0")
eberlm@63295
  1935
  case True
eberlm@63295
  1936
  with assms show ?thesis by (auto intro!: tendsto_powr_complex_0)
eberlm@63295
  1937
next
eberlm@63295
  1938
  case False
eberlm@63295
  1939
  with assms show ?thesis by (auto intro!: tendsto_powr_complex elim!: nonpos_Reals_cases)
eberlm@63295
  1940
qed
eberlm@63295
  1941
eberlm@63295
  1942
lemma continuous_powr_complex:
eberlm@63295
  1943
  assumes "f (netlimit F) \<notin> \<real>\<^sub>\<le>\<^sub>0" "continuous F f" "continuous F g"
eberlm@63295
  1944
  shows   "continuous F (\<lambda>z. f z powr g z :: complex)"
eberlm@63295
  1945
  using assms unfolding continuous_def by (intro tendsto_powr_complex) simp_all
eberlm@63295
  1946
eberlm@63295
  1947
lemma isCont_powr_complex [continuous_intros]:
eberlm@63295
  1948
  assumes "f z \<notin> \<real>\<^sub>\<le>\<^sub>0" "isCont f z" "isCont g z"
eberlm@63295
  1949
  shows   "isCont (\<lambda>z. f z powr g z :: complex) z"
eberlm@63295
  1950
  using assms unfolding isCont_def by (intro tendsto_powr_complex) simp_all
eberlm@63295
  1951
eberlm@63295
  1952
lemma continuous_on_powr_complex [continuous_intros]:
eberlm@63295
  1953
  assumes "A \<subseteq> {z. Re (f z) \<ge> 0 \<or> Im (f z) \<noteq> 0}"
eberlm@63295
  1954
  assumes "\<And>z. z \<in> A \<Longrightarrow> f z = 0 \<Longrightarrow> Re (g z) > 0"
eberlm@63295
  1955
  assumes "continuous_on A f" "continuous_on A g"
eberlm@63295
  1956
  shows   "continuous_on A (\<lambda>z. f z powr g z)"
eberlm@63295
  1957
  unfolding continuous_on_def
eberlm@63295
  1958
proof
eberlm@63295
  1959
  fix z assume z: "z \<in> A"
eberlm@63295
  1960
  show "((\<lambda>z. f z powr g z) \<longlongrightarrow> f z powr g z) (at z within A)"
eberlm@63295
  1961
  proof (cases "f z = 0")
eberlm@63295
  1962
    case False
eberlm@63295
  1963
    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
eberlm@63295
  1964
    with assms(3,4) z show ?thesis
eberlm@63295
  1965
      by (intro tendsto_powr_complex')
eberlm@63295
  1966
         (auto elim!: nonpos_Reals_cases simp: complex_eq_iff continuous_on_def)
eberlm@63295
  1967
  next
eberlm@63295
  1968
    case True
eberlm@63295
  1969
    with assms z show ?thesis
eberlm@63295
  1970
      by (auto intro!: tendsto_powr_complex_0 simp: continuous_on_def)
eberlm@63295
  1971
  qed
eberlm@63295
  1972
qed
lp15@60017
  1973
lp15@60150
  1974
wenzelm@60420
  1975
subsection\<open>Some Limits involving Logarithms\<close>
lp15@61609
  1976
lp15@60150
  1977
lemma lim_Ln_over_power:
lp15@60150
  1978
  fixes s::complex
lp15@60150
  1979
  assumes "0 < Re s"
wenzelm@61973
  1980
    shows "((\<lambda>n. Ln n / (n powr s)) \<longlongrightarrow> 0) sequentially"
lp15@60150
  1981
proof (simp add: lim_sequentially dist_norm, clarify)
lp15@61609
  1982
  fix e::real
lp15@60150
  1983
  assume e: "0 < e"
lp15@60150
  1984
  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"
lp15@60150
  1985
  proof (rule_tac x="2/(e * (Re s)\<^sup>2)" in exI, safe)
lp15@60150
  1986
    show "0 < 2 / (e * (Re s)\<^sup>2)"
lp15@60150
  1987
      using e assms by (simp add: field_simps)
lp15@60150
  1988
  next
lp15@60150
  1989
    fix x::real
lp15@60150
  1990
    assume x: "2 / (e * (Re s)\<^sup>2) \<le> x"
lp15@60150
  1991
    then have "x>0"
lp15@60150
  1992
    using e assms
lp15@60150
  1993
      by (metis less_le_trans mult_eq_0_iff mult_pos_pos pos_less_divide_eq power2_eq_square
lp15@60150
  1994
                zero_less_numeral)
lp15@60150
  1995
    then show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
lp15@60150
  1996
      using e assms x
lp15@60150
  1997
      apply (auto simp: field_simps)
lp15@60150
  1998
      apply (rule_tac y = "e * (x\<^sup>2 * (Re s)\<^sup>2)" in le_less_trans)
lp15@60150
  1999
      apply (auto simp: power2_eq_square field_simps add_pos_pos)
lp15@60150
  2000
      done
lp15@60150
  2001
  qed
lp15@60150
  2002
  then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < 1 + (Re s * x) + (1/2) * (Re s * x)^2"
lp15@60150
  2003
    using e  by (simp add: field_simps)
lp15@60150
  2004
  then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < exp (Re s * x)"
lp15@60150
  2005
    using assms
lp15@60150
  2006
    by (force intro: less_le_trans [OF _ exp_lower_taylor_quadratic])
lp15@60150
  2007
  then have "\<exists>xo>0. \<forall>x\<ge>xo. x < e * exp (Re s * x)"
lp15@60150
  2008
    using e   by (auto simp: field_simps)
lp15@60150
  2009
  with e show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
lp15@60150
  2010
    apply (auto simp: norm_divide norm_powr_real divide_simps)
wenzelm@61942
  2011
    apply (rule_tac x="nat \<lceil>exp xo\<rceil>" in exI)
lp15@60150
  2012
    apply clarify
lp15@60150
  2013
    apply (drule_tac x="ln n" in spec)
lp15@61609
  2014
    apply (auto simp: exp_less_mono nat_ceiling_le_eq not_le)
lp15@60150
  2015
    apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff)
lp15@60150
  2016
    done
lp15@60150
  2017
qed
lp15@60150
  2018
wenzelm@61973
  2019
lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
lp15@65587
  2020
  using lim_Ln_over_power [of 1] by simp
lp15@65587
  2021
lp15@60150
  2022
lemma lim_ln_over_power:
lp15@60150
  2023
  fixes s :: real
lp15@60150
  2024
  assumes "0 < s"
wenzelm@61973
  2025
    shows "((\<lambda>n. ln n / (n powr s)) \<longlongrightarrow> 0) sequentially"
lp15@60150
  2026
  using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
lp15@60150
  2027
  apply (subst filterlim_sequentially_Suc [symmetric])
lp15@60150
  2028
  apply (simp add: lim_sequentially dist_norm
lp15@61609
  2029
          Ln_Reals_eq norm_powr_real_powr norm_divide)
lp15@60150
  2030
  done
lp15@60150
  2031
wenzelm@61973
  2032
lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
lp15@60150
  2033
  using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]]
lp15@60150
  2034
  apply (subst filterlim_sequentially_Suc [symmetric])
lp15@61609
  2035
  apply (simp add: lim_sequentially dist_norm)
lp15@60150
  2036
  done
lp15@60150
  2037
lp15@60150
  2038
lemma lim_1_over_complex_power:
lp15@60150
  2039
  assumes "0 < Re s"
wenzelm@61973
  2040
    shows "((\<lambda>n. 1 / (of_nat n powr s)) \<longlongrightarrow> 0) sequentially"
lp15@60150
  2041
proof -
lp15@60150
  2042
  have "\<forall>n>0. 3 \<le> n \<longrightarrow> 1 \<le> ln (real_of_nat n)"
lp15@65719
  2043
    using ln_272_gt_1
lp15@65719
  2044
    by (force intro: order_trans [of _ "ln (272/100)"])
wenzelm@61969
  2045
  moreover have "(\<lambda>n. cmod (Ln (of_nat n) / of_nat n powr s)) \<longlonglongrightarrow> 0"
lp15@60150
  2046
    using lim_Ln_over_power [OF assms]
lp15@60150
  2047
    by (metis tendsto_norm_zero_iff)
lp15@60150
  2048
  ultimately show ?thesis
lp15@60150
  2049
    apply (auto intro!: Lim_null_comparison [where g = "\<lambda>n. norm (Ln(of_nat n) / of_nat n powr s)"])
lp15@60150
  2050
    apply (auto simp: norm_divide divide_simps eventually_sequentially)
lp15@60150
  2051
    done
lp15@60150
  2052
qed
lp15@60150
  2053
lp15@60150
  2054
lemma lim_1_over_real_power:
lp15@60150
  2055
  fixes s :: real
lp15@60150
  2056
  assumes "0 < s"
wenzelm@61973
  2057
    shows "((\<lambda>n. 1 / (of_nat n powr s)) \<longlongrightarrow> 0) sequentially"
lp15@60150
  2058
  using lim_1_over_complex_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
lp15@60150
  2059
  apply (subst filterlim_sequentially_Suc [symmetric])
lp15@60150
  2060
  apply (simp add: lim_sequentially dist_norm)
lp15@61609
  2061
  apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide)
lp15@60150
  2062
  done
lp15@60150
  2063
wenzelm@61973
  2064
lemma lim_1_over_Ln: "((\<lambda>n. 1 / Ln(of_nat n)) \<longlongrightarrow> 0) sequentially"
lp15@60150
  2065
proof (clarsimp simp add: lim_sequentially dist_norm norm_divide divide_simps)
lp15@60150
  2066
  fix r::real
lp15@60150
  2067
  assume "0 < r"
lp15@60150
  2068
  have ir: "inverse (exp (inverse r)) > 0"
lp15@60150
  2069
    by simp
lp15@60150
  2070
  obtain n where n: "1 < of_nat n * inverse (exp (inverse r))"
lp15@60150
  2071
    using ex_less_of_nat_mult [of _ 1, OF ir]
lp15@60150
  2072
    by auto
lp15@60150
  2073
  then have "exp (inverse r) < of_nat n"
lp15@60150
  2074
    by (simp add: divide_simps)
lp15@60150
  2075
  then have "ln (exp (inverse r)) < ln (of_nat n)"
lp15@60150
  2076
    by (metis exp_gt_zero less_trans ln_exp ln_less_cancel_iff)
wenzelm@60420
  2077
  with \<open>0 < r\<close> have "1 < r * ln (real_of_nat n)"
lp15@60150
  2078
    by (simp add: field_simps)
lp15@60150
  2079
  moreover have "n > 0" using n
lp15@60150
  2080
    using neq0_conv by fastforce
lp15@60150
  2081
  ultimately show "\<exists>no. \<forall>n. Ln (of_nat n) \<noteq> 0 \<longrightarrow> no \<le> n \<longrightarrow> 1 < r * cmod (Ln (of_nat n))"
wenzelm@60420
  2082
    using n \<open>0 < r\<close>
lp15@60150
  2083
    apply (rule_tac x=n in exI)
lp15@60150
  2084
    apply (auto simp: divide_simps)
lp15@60150
  2085
    apply (erule less_le_trans, auto)
lp15@60150
  2086
    done
lp15@60150
  2087
qed
lp15@60150
  2088
wenzelm@61973
  2089
lemma lim_1_over_ln: "((\<lambda>n. 1 / ln(real_of_nat n)) \<longlongrightarrow> 0) sequentially"
wenzelm@63092
  2090
  using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]]
lp15@60150
  2091
  apply (subst filterlim_sequentially_Suc [symmetric])
lp15@60150
  2092
  apply (simp add: lim_sequentially dist_norm)
lp15@61609
  2093
  apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide)
lp15@60150
  2094
  done
lp15@60150
  2095
lp15@65719
  2096
lemma lim_ln1_over_ln: "(\<lambda>n. ln(Suc n) / ln n) \<longlonglongrightarrow> 1"
lp15@65719
  2097
proof (rule Lim_transform_eventually)
lp15@65719
  2098
  have "(\<lambda>n. ln(1 + 1/n) / ln n) \<longlonglongrightarrow> 0"
lp15@65719
  2099
  proof (rule Lim_transform_bound)
lp15@65719
  2100
    show "(inverse o real) \<longlonglongrightarrow> 0"
lp15@65719
  2101
      by (metis comp_def seq_harmonic tendsto_explicit)
lp15@65719
  2102
    show "\<forall>\<^sub>F n in sequentially. norm (ln (1 + 1 / n) / ln n) \<le> norm ((inverse \<circ> real) n)"
lp15@65719
  2103
    proof
lp15@65719
  2104
      fix n::nat
lp15@65719
  2105
      assume n: "3 \<le> n"
lp15@65719
  2106
      then have "ln 3 \<le> ln n" and ln0: "0 \<le> ln n"
lp15@65719
  2107
        by auto
lp15@65719
  2108
      with ln3_gt_1 have "1/ ln n \<le> 1"
lp15@65719
  2109
        by (simp add: divide_simps)
lp15@65719
  2110
      moreover have "ln (1 + 1 / real n) \<le> 1/n"
lp15@65719
  2111
        by (simp add: ln_add_one_self_le_self)
lp15@65719
  2112
      ultimately have "ln (1 + 1 / real n) * (1 / ln n) \<le> (1/n) * 1"
lp15@65719
  2113
        by (intro mult_mono) (use n in auto)
lp15@65719
  2114
      then show "norm (ln (1 + 1 / n) / ln n) \<le> norm ((inverse \<circ> real) n)"
lp15@65719
  2115
        by (simp add: field_simps ln0)
lp15@65719
  2116
      qed
lp15@65719
  2117
  qed
lp15@65719
  2118
  then show "(\<lambda>n. 1 + ln(1 + 1/n) / ln n) \<longlonglongrightarrow> 1"
lp15@65719
  2119
    by (metis (full_types) add.right_neutral tendsto_add_const_iff)
lp15@65719
  2120
  show "\<forall>\<^sub>F k in sequentially. 1 + ln (1 + 1 / k) / ln k = ln(Suc k) / ln k"
lp15@65719
  2121
    by (simp add: divide_simps ln_div eventually_sequentiallyI [of 2])
lp15@65719
  2122
qed
lp15@65719
  2123
lp15@65719
  2124
lemma lim_ln_over_ln1: "(\<lambda>n. ln n / ln(Suc n)) \<longlonglongrightarrow> 1"
lp15@65719
  2125
proof -
lp15@65719
  2126
  have "(\<lambda>n. inverse (ln(Suc n) / ln n)) \<longlonglongrightarrow> inverse 1"
lp15@65719
  2127
    by (rule tendsto_inverse [OF lim_ln1_over_ln]) auto
lp15@65719
  2128
  then show ?thesis
lp15@65719
  2129
    by simp
lp15@65719
  2130
qed
lp15@65719
  2131
lp15@60017
  2132
wenzelm@60420
  2133
subsection\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
lp15@59751
  2134
lp15@59751
  2135
lemma csqrt_exp_Ln:
lp15@59751
  2136
  assumes "z \<noteq> 0"
lp15@59751
  2137
    shows "csqrt z = exp(Ln(z) / 2)"
lp15@59751
  2138
proof -
lp15@59751
  2139
  have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
haftmann@64240
  2140
    by (metis exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
lp15@59751
  2141
  also have "... = z"
lp15@59751
  2142
    using assms exp_Ln by blast
lp15@59751
  2143
  finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
lp15@59751
  2144
    by simp
lp15@59751
  2145
  also have "... = exp (Ln z / 2)"
lp15@59751
  2146
    apply (subst csqrt_square)
lp15@59751
  2147
    using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
lp15@59751
  2148
    apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+)
lp15@59751
  2149
    done
lp15@59751
  2150
  finally show ?thesis using assms csqrt_square
lp15@59751
  2151
    by simp
lp15@59751
  2152
qed
lp15@59751
  2153
lp15@59751
  2154
lemma csqrt_inverse:
paulson@62131
  2155
  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
lp15@59751
  2156
    shows "csqrt (inverse z) = inverse (csqrt z)"
lp15@59751
  2157
proof (cases "z=0", simp)
paulson@62131
  2158
  assume "z \<noteq> 0"
lp15@59751
  2159
  then show ?thesis
paulson@62131
  2160
    using assms csqrt_exp_Ln Ln_inverse exp_minus
lp15@59751
  2161
    by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
lp15@59751
  2162
qed
lp15@59751
  2163
lp15@59751
  2164
lemma cnj_csqrt:
paulson@62131
  2165
  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
lp15@59751
  2166
    shows "cnj(csqrt z) = csqrt(cnj z)"
lp15@59751
  2167
proof (cases "z=0", simp)
paulson@62131
  2168
  assume "z \<noteq> 0"
lp15@59751
  2169
  then show ?thesis
lp15@62534
  2170
     by (simp add: assms cnj_Ln csqrt_exp_Ln exp_cnj)
lp15@59751
  2171
qed
lp15@59751
  2172
lp15@59751
  2173
lemma has_field_derivative_csqrt:
paulson@62131
  2174
  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
lp15@59751
  2175
    shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)"
lp15@59751
  2176
proof -
lp15@59751
  2177
  have z: "z \<noteq> 0"
lp15@59751
  2178
    using assms by auto
lp15@59751
  2179
  then have *: "inverse z = inverse (2*z) * 2"
lp15@59751
  2180
    by (simp add: divide_simps)
paulson@62131
  2181
  have [simp]: "exp (Ln z / 2) * inverse z = inverse (csqrt z)"
paulson@62131
  2182
    by (simp add: z field_simps csqrt_exp_Ln [symmetric]) (metis power2_csqrt power2_eq_square)
paulson@62131
  2183
  have "Im z = 0 \<Longrightarrow> 0 < Re z"
paulson@62131
  2184
    using assms complex_nonpos_Reals_iff not_less by blast
paulson@62131
  2185
  with z have "((\<lambda>z. exp (Ln z / 2)) has_field_derivative inverse (2 * csqrt z)) (at z)"
paulson@62131
  2186
    by (force intro: derivative_eq_intros * simp add: assms)
paulson@62131
  2187
  then show ?thesis
paulson@62131
  2188
    apply (rule DERIV_transform_at[where d = "norm z"])
paulson@62131
  2189
    apply (intro z derivative_eq_intros | simp add: assms)+
lp15@59751
  2190
    using z
lp15@59751
  2191
    apply (metis csqrt_exp_Ln dist_0_norm less_irrefl)
lp15@59751
  2192
    done
lp15@59751
  2193
qed
lp15@59751
  2194
lp15@62534
  2195
lemma field_differentiable_at_csqrt:
lp15@62534
  2196
    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt field_differentiable at z"
lp15@62534
  2197
  using field_differentiable_def has_field_derivative_csqrt by blast
lp15@62534
  2198
lp15@62534
  2199
lemma field_differentiable_within_csqrt:
lp15@62534
  2200
    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt field_differentiable (at z within s)"
lp15@62534
  2201
  using field_differentiable_at_csqrt field_differentiable_within_subset by blast
lp15@59751
  2202
lp15@59751
  2203
lemma continuous_at_csqrt:
paulson@62131
  2204
    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) csqrt"
lp15@62534
  2205
  by (simp add: field_differentiable_within_csqrt field_differentiable_imp_continuous_at)
lp15@59751
  2206
lp15@59862
  2207
corollary isCont_csqrt' [simp]:
paulson@62131
  2208
   "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
lp15@59862
  2209
  by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
lp15@59862
  2210
lp15@59751
  2211
lemma continuous_within_csqrt:
paulson@62131
  2212
    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within s) csqrt"
lp15@62534
  2213
  by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_csqrt)
lp15@59751
  2214
lp15@59751
  2215
lemma continuous_on_csqrt [continuous_intros]:
paulson@62131
  2216
    "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s csqrt"
lp15@59751
  2217
  by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
lp15@59751
  2218
lp15@59751
  2219
lemma holomorphic_on_csqrt:
paulson@62131
  2220
    "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> csqrt holomorphic_on s"
lp15@62534
  2221
  by (simp add: field_differentiable_within_csqrt holomorphic_on_def)
lp15@59751
  2222
lp15@59751
  2223
lemma continuous_within_closed_nontrivial:
lp15@59751
  2224
    "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
lp15@59751
  2225
  using open_Compl
lp15@59751
  2226
  by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
lp15@59751
  2227
lp15@59751
  2228
lemma continuous_within_csqrt_posreal:
lp15@59751
  2229
    "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
paulson@62131
  2230
proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
lp15@62534
  2231
  case True
lp15@59751
  2232
  then have "Im z = 0" "Re z < 0 \<or> z = 0"
lp15@65274
  2233
    using cnj.code complex_cnj_zero_iff  by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce
lp15@59751
  2234
  then show ?thesis
lp15@59751
  2235
    apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
lp15@59751
  2236
    apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
lp15@59751
  2237
    apply (rule_tac x="e^2" in exI)
lp15@59751
  2238
    apply (auto simp: Reals_def)
paulson@62131
  2239
    by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
paulson@62131
  2240
next
paulson@62131
  2241
  case False
paulson@62131
  2242
    then show ?thesis   by (blast intro: continuous_within_csqrt)
lp15@59751
  2243
qed
lp15@59751
  2244
wenzelm@60420
  2245
subsection\<open>Complex arctangent\<close>
wenzelm@60420
  2246
paulson@62131
  2247
text\<open>The branch cut gives standard bounds in the real case.\<close>
lp15@59870
  2248
lp15@59870
  2249
definition Arctan :: "complex \<Rightarrow> complex" where
lp15@59870
  2250
    "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))"
lp15@59870
  2251
eberlm@62049
  2252
lemma Arctan_def_moebius: "Arctan z = \<i>/2 * Ln (moebius (-\<i>) 1 \<i> 1 z)"
eberlm@62049
  2253
  by (simp add: Arctan_def moebius_def add_ac)
eberlm@62049
  2254
eberlm@62049
  2255
lemma Ln_conv_Arctan:
eberlm@62049
  2256
  assumes "z \<noteq> -1"
eberlm@62049
  2257
  shows   "Ln z = -2*\<i> * Arctan (moebius 1 (- 1) (- \<i>) (- \<i>) z)"
eberlm@62049
  2258
proof -
eberlm@62049
  2259
  have "Arctan (moebius 1 (- 1) (- \<i>) (- \<i>) z) =
eberlm@62049
  2260
             \<i>/2 * Ln (moebius (- \<i>) 1 \<i> 1 (moebius 1 (- 1) (- \<i>) (- \<i>) z))"
eberlm@62049
  2261
    by (simp add: Arctan_def_moebius)
eberlm@62049
  2262
  also from assms have "\<i> * z \<noteq> \<i> * (-1)" by (subst mult_left_cancel) simp
eberlm@62049
  2263
  hence "\<i> * z - -\<i> \<noteq> 0" by (simp add: eq_neg_iff_add_eq_0)
eberlm@62049
  2264
  from moebius_inverse'[OF _ this, of 1 1]
eberlm@62049
  2265
    have "moebius (- \<i>) 1 \<i> 1 (moebius 1 (- 1) (- \<i>) (- \<i>) z) = z" by simp
eberlm@62049
  2266
  finally show ?thesis by (simp add: field_simps)
eberlm@62049
  2267
qed
eberlm@62049
  2268
lp15@59870
  2269
lemma Arctan_0 [simp]: "Arctan 0 = 0"
lp15@59870
  2270
  by (simp add: Arctan_def)
lp15@59870
  2271
lp15@59870
  2272
lemma Im_complex_div_lemma: "Im((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<longleftrightarrow> Re z = 0"
lp15@59870
  2273
  by (auto simp: Im_complex_div_eq_0 algebra_simps)