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