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