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