src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
author paulson <lp15@cam.ac.uk>
Wed Mar 18 17:23:22 2015 +0000 (2015-03-18)
changeset 59746 ddae5727c5a9
parent 59745 390476a0ef13
child 59751 916c0f6c83e3
permissions -rw-r--r--
new HOL Light material about exp, sin, cos
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@59746
    11
subsection{*The Exponential Function is Differentiable and Continuous*}
lp15@59745
    12
lp15@59745
    13
lemma complex_differentiable_at_exp: "exp complex_differentiable at z"
lp15@59745
    14
  using DERIV_exp complex_differentiable_def by blast
lp15@59745
    15
lp15@59745
    16
lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
lp15@59745
    17
  by (simp add: complex_differentiable_at_exp complex_differentiable_at_within)
lp15@59745
    18
lp15@59745
    19
lemma continuous_within_exp:
lp15@59745
    20
  fixes z::"'a::{real_normed_field,banach}"
lp15@59745
    21
  shows "continuous (at z within s) exp"
lp15@59745
    22
by (simp add: continuous_at_imp_continuous_within)
lp15@59745
    23
lp15@59745
    24
lemma continuous_on_exp:
lp15@59745
    25
  fixes s::"'a::{real_normed_field,banach} set"
lp15@59745
    26
  shows "continuous_on s exp"
lp15@59745
    27
by (simp add: continuous_on_exp continuous_on_id)
lp15@59745
    28
lp15@59745
    29
lemma holomorphic_on_exp: "exp holomorphic_on s"
lp15@59745
    30
  by (simp add: complex_differentiable_within_exp holomorphic_on_def)
lp15@59745
    31
lp15@59745
    32
subsection{*Euler and de Moivre formulas.*}
lp15@59745
    33
lp15@59745
    34
text{*The sine series times @{term i}*}
lp15@59745
    35
lemma sin_ii_eq: "(\<lambda>n. (ii * sin_coeff n) * z^n) sums (ii * sin z)"
lp15@59745
    36
proof -
lp15@59745
    37
  have "(\<lambda>n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)"
lp15@59745
    38
    using sin_converges sums_mult by blast
lp15@59745
    39
  then show ?thesis
lp15@59745
    40
    by (simp add: scaleR_conv_of_real field_simps)
lp15@59745
    41
qed
lp15@59745
    42
lp15@59745
    43
theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)"
lp15@59745
    44
proof -
lp15@59745
    45
  have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) 
lp15@59745
    46
        = (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))"
lp15@59745
    47
  proof
lp15@59745
    48
    fix n
lp15@59745
    49
    show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)"
lp15@59745
    50
      by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
lp15@59745
    51
  qed
lp15@59745
    52
  also have "... sums (exp (ii * z))"
lp15@59745
    53
    by (rule exp_converges)
lp15@59745
    54
  finally have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (exp (ii * z))" .
lp15@59745
    55
  moreover have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (cos z + ii * sin z)"
lp15@59745
    56
    using sums_add [OF cos_converges [of z] sin_ii_eq [of z]]
lp15@59745
    57
    by (simp add: field_simps scaleR_conv_of_real)
lp15@59745
    58
  ultimately show ?thesis
lp15@59745
    59
    using sums_unique2 by blast
lp15@59745
    60
qed
lp15@59745
    61
lp15@59745
    62
corollary exp_minus_Euler: "exp(-(ii * z)) = cos(z) - ii * sin(z)"
lp15@59745
    63
  using exp_Euler [of "-z"]
lp15@59745
    64
  by simp
lp15@59745
    65
lp15@59745
    66
lemma sin_exp_eq: "sin z = (exp(ii * z) - exp(-(ii * z))) / (2*ii)"
lp15@59745
    67
  by (simp add: exp_Euler exp_minus_Euler)
lp15@59745
    68
lp15@59745
    69
lemma sin_exp_eq': "sin z = ii * (exp(-(ii * z)) - exp(ii * z)) / 2"
lp15@59745
    70
  by (simp add: exp_Euler exp_minus_Euler)
lp15@59745
    71
lp15@59745
    72
lemma cos_exp_eq:  "cos z = (exp(ii * z) + exp(-(ii * z))) / 2"
lp15@59745
    73
  by (simp add: exp_Euler exp_minus_Euler)
lp15@59745
    74
lp15@59745
    75
subsection{*Relationships between real and complex trig functions*}
lp15@59745
    76
lp15@59745
    77
declare sin_of_real [simp] cos_of_real [simp]
lp15@59745
    78
lp15@59745
    79
lemma real_sin_eq [simp]:
lp15@59745
    80
  fixes x::real
lp15@59745
    81
  shows "Re(sin(of_real x)) = sin x"
lp15@59745
    82
  by (simp add: sin_of_real)
lp15@59745
    83
  
lp15@59745
    84
lemma real_cos_eq [simp]:
lp15@59745
    85
  fixes x::real
lp15@59745
    86
  shows "Re(cos(of_real x)) = cos x"
lp15@59745
    87
  by (simp add: cos_of_real)
lp15@59745
    88
lp15@59745
    89
lemma DeMoivre: "(cos z + ii * sin z) ^ n = cos(n * z) + ii * sin(n * z)"
lp15@59745
    90
  apply (simp add: exp_Euler [symmetric])
lp15@59745
    91
  by (metis exp_of_nat_mult mult.left_commute)
lp15@59745
    92
lp15@59745
    93
lemma exp_cnj:
lp15@59745
    94
  fixes z::complex
lp15@59745
    95
  shows "cnj (exp z) = exp (cnj z)"
lp15@59745
    96
proof -
lp15@59745
    97
  have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))"
lp15@59745
    98
    by auto
lp15@59745
    99
  also have "... sums (exp (cnj z))"
lp15@59745
   100
    by (rule exp_converges)
lp15@59745
   101
  finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
lp15@59745
   102
  moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
lp15@59745
   103
    by (metis exp_converges sums_cnj) 
lp15@59745
   104
  ultimately show ?thesis
lp15@59745
   105
    using sums_unique2
lp15@59745
   106
    by blast 
lp15@59745
   107
qed
lp15@59745
   108
lp15@59745
   109
lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
lp15@59745
   110
  by (simp add: sin_exp_eq exp_cnj field_simps)
lp15@59745
   111
lp15@59745
   112
lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
lp15@59745
   113
  by (simp add: cos_exp_eq exp_cnj field_simps)
lp15@59745
   114
lp15@59745
   115
lemma exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
lp15@59745
   116
  by (metis Reals_cases Reals_of_real exp_of_real)
lp15@59745
   117
lp15@59745
   118
lemma sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
lp15@59745
   119
  by (metis Reals_cases Reals_of_real sin_of_real)
lp15@59745
   120
lp15@59745
   121
lemma cos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> cos z \<in> \<real>"
lp15@59745
   122
  by (metis Reals_cases Reals_of_real cos_of_real)
lp15@59745
   123
lp15@59745
   124
lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
lp15@59745
   125
  using DERIV_sin complex_differentiable_def by blast
lp15@59745
   126
lp15@59745
   127
lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)"
lp15@59745
   128
  by (simp add: complex_differentiable_at_sin complex_differentiable_at_within)
lp15@59745
   129
lp15@59745
   130
lemma complex_differentiable_at_cos: "cos complex_differentiable at z"
lp15@59745
   131
  using DERIV_cos complex_differentiable_def by blast
lp15@59745
   132
lp15@59745
   133
lemma complex_differentiable_within_cos: "cos complex_differentiable (at z within s)"
lp15@59745
   134
  by (simp add: complex_differentiable_at_cos complex_differentiable_at_within)
lp15@59745
   135
lp15@59745
   136
lemma holomorphic_on_sin: "sin holomorphic_on s"
lp15@59745
   137
  by (simp add: complex_differentiable_within_sin holomorphic_on_def)
lp15@59745
   138
lp15@59745
   139
lemma holomorphic_on_cos: "cos holomorphic_on s"
lp15@59745
   140
  by (simp add: complex_differentiable_within_cos holomorphic_on_def)
lp15@59745
   141
lp15@59745
   142
subsection{* Get a nice real/imaginary separation in Euler's formula.*}
lp15@59745
   143
lp15@59745
   144
lemma Euler: "exp(z) = of_real(exp(Re z)) * 
lp15@59745
   145
              (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
lp15@59745
   146
by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
lp15@59745
   147
lp15@59745
   148
lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
lp15@59745
   149
  by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
lp15@59745
   150
lp15@59745
   151
lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
lp15@59745
   152
  by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
lp15@59745
   153
lp15@59745
   154
lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
lp15@59745
   155
  by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
lp15@59745
   156
lp15@59745
   157
lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
lp15@59745
   158
  by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
lp15@59745
   159
lp15@59746
   160
lp15@59746
   161
subsection {* More Corollaries about Sine and Cosine *}
lp15@59745
   162
lp15@59745
   163
lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
lp15@59745
   164
  by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
lp15@59745
   165
lp15@59745
   166
lemma cos_one_2pi: 
lp15@59745
   167
    "cos(x) = 1 \<longleftrightarrow> (\<exists>n::nat. x = n * 2*pi) | (\<exists>n::nat. x = -(n * 2*pi))"
lp15@59745
   168
    (is "?lhs = ?rhs")
lp15@59745
   169
proof
lp15@59745
   170
  assume "cos(x) = 1"
lp15@59745
   171
  then have "sin x = 0"
lp15@59745
   172
    by (simp add: cos_one_sin_zero)
lp15@59745
   173
  then show ?rhs
lp15@59745
   174
  proof (simp only: sin_zero_iff, elim exE disjE conjE)
lp15@59745
   175
    fix n::nat
lp15@59745
   176
    assume n: "even n" "x = real n * (pi/2)"
lp15@59745
   177
    then obtain m where m: "n = 2 * m"
lp15@59745
   178
      using dvdE by blast
lp15@59745
   179
    then have me: "even m" using `?lhs` n
lp15@59745
   180
      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
lp15@59745
   181
    show ?rhs
lp15@59745
   182
      using m me n
lp15@59745
   183
      by (auto simp: field_simps elim!: evenE)
lp15@59745
   184
  next    
lp15@59745
   185
    fix n::nat
lp15@59745
   186
    assume n: "even n" "x = - (real n * (pi/2))"
lp15@59745
   187
    then obtain m where m: "n = 2 * m"
lp15@59745
   188
      using dvdE by blast
lp15@59745
   189
    then have me: "even m" using `?lhs` n
lp15@59745
   190
      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
lp15@59745
   191
    show ?rhs
lp15@59745
   192
      using m me n
lp15@59745
   193
      by (auto simp: field_simps elim!: evenE)
lp15@59745
   194
  qed
lp15@59745
   195
next
lp15@59745
   196
  assume "?rhs"
lp15@59745
   197
  then show "cos x = 1"
lp15@59745
   198
    by (metis cos_2npi cos_minus mult.assoc mult.left_commute)
lp15@59745
   199
qed
lp15@59745
   200
lp15@59745
   201
lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
lp15@59745
   202
  apply auto  --{*FIXME simproc bug*}
lp15@59745
   203
  apply (auto simp: cos_one_2pi)
lp15@59745
   204
  apply (metis real_of_int_of_nat_eq)
lp15@59745
   205
  apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq)
lp15@59745
   206
  by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def)
lp15@59745
   207
lp15@59745
   208
lemma sin_cos_sqrt: "0 \<le> sin(x) \<Longrightarrow> (sin(x) = sqrt(1 - (cos(x) ^ 2)))"
lp15@59745
   209
  using sin_squared_eq real_sqrt_unique by fastforce
lp15@59745
   210
lp15@59745
   211
lemma sin_eq_0_pi: "-pi < x \<Longrightarrow> x < pi \<Longrightarrow> sin(x) = 0 \<Longrightarrow> x = 0"
lp15@59745
   212
  by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq)
lp15@59745
   213
lp15@59745
   214
lemma cos_treble_cos: 
lp15@59745
   215
  fixes x :: "'a::{real_normed_field,banach}"
lp15@59745
   216
  shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x"
lp15@59745
   217
proof -
lp15@59745
   218
  have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))"
lp15@59745
   219
    by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square])
lp15@59745
   220
  have "cos(3 * x) = cos(2*x + x)"
lp15@59745
   221
    by simp
lp15@59745
   222
  also have "... = 4 * cos(x) ^ 3 - 3 * cos x"
lp15@59745
   223
    apply (simp only: cos_add cos_double sin_double)
lp15@59745
   224
    apply (simp add: * field_simps power2_eq_square power3_eq_cube)
lp15@59745
   225
    done
lp15@59745
   226
  finally show ?thesis .
lp15@59745
   227
qed
lp15@59745
   228
lp15@59746
   229
  
lp15@59746
   230
subsection{*More on the Polar Representation of Complex Numbers*}
lp15@59746
   231
lp15@59746
   232
lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
lp15@59746
   233
  by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
lp15@59746
   234
lp15@59746
   235
lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
lp15@59746
   236
  by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
lp15@59746
   237
lp15@59746
   238
lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"
lp15@59746
   239
  by (simp add: cos_one_2pi_int)
lp15@59746
   240
lp15@59746
   241
lemma sin_int_2npi [simp]: "sin (2 * real (n::int) * pi) = 0"
lp15@59746
   242
  by (metis Ints_real_of_int mult.assoc mult.commute sin_integer_2pi)
lp15@59746
   243
lp15@59746
   244
lemma sincos_principal_value: "\<exists>y. (-pi < y \<and> y \<le> pi) \<and> (sin(y) = sin(x) \<and> cos(y) = cos(x))"
lp15@59746
   245
  apply (rule exI [where x="pi - (2*pi) * frac((pi - x) / (2*pi))"])
lp15@59746
   246
  apply (auto simp: field_simps frac_lt_1)
lp15@59746
   247
  apply (simp_all add: frac_def divide_simps)
lp15@59746
   248
  apply (simp_all add: add_divide_distrib diff_divide_distrib)
lp15@59746
   249
  apply (simp_all add: sin_diff cos_diff mult.assoc [symmetric] cos_integer_2pi sin_integer_2pi)
lp15@59746
   250
  done
lp15@59746
   251
lp15@59746
   252
lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
lp15@59746
   253
  by (simp add: exp_add exp_Euler exp_of_real)
lp15@59746
   254
lp15@59746
   255
lp15@59746
   256
lp15@59746
   257
lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
lp15@59746
   258
apply auto
lp15@59746
   259
apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
lp15@59746
   260
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
   261
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
   262
lp15@59746
   263
lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * ii)"
lp15@59746
   264
                (is "?lhs = ?rhs")
lp15@59746
   265
proof -
lp15@59746
   266
  have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
lp15@59746
   267
    by (simp add: exp_diff)
lp15@59746
   268
  also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
lp15@59746
   269
    by (simp add: exp_eq_1)
lp15@59746
   270
  also have "... \<longleftrightarrow> ?rhs"
lp15@59746
   271
    by (auto simp: algebra_simps intro!: complex_eqI)
lp15@59746
   272
  finally show ?thesis .
lp15@59746
   273
qed
lp15@59746
   274
lp15@59746
   275
lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
lp15@59746
   276
  by (auto simp: exp_eq abs_mult)
lp15@59746
   277
lp15@59746
   278
lemma exp_integer_2pi: 
lp15@59746
   279
  assumes "n \<in> Ints"
lp15@59746
   280
  shows "exp((2 * n * pi) * ii) = 1"
lp15@59746
   281
proof -
lp15@59746
   282
  have "exp((2 * n * pi) * ii) = exp 0"
lp15@59746
   283
    using assms
lp15@59746
   284
    by (simp only: Ints_def exp_eq) auto
lp15@59746
   285
  also have "... = 1"
lp15@59746
   286
    by simp
lp15@59746
   287
  finally show ?thesis .
lp15@59746
   288
qed
lp15@59746
   289
lp15@59746
   290
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
   291
proof -
lp15@59746
   292
  { assume "sin y = sin x" "cos y = cos x"
lp15@59746
   293
    then have "cos (y-x) = 1"
lp15@59746
   294
      using cos_add [of y "-x"] by simp
lp15@59746
   295
    then have "\<exists>n::int. y-x = real n * 2 * pi"
lp15@59746
   296
      using cos_one_2pi_int by blast }
lp15@59746
   297
  then show ?thesis
lp15@59746
   298
  apply (auto simp: sin_add cos_add)
lp15@59746
   299
  apply (metis add.commute diff_add_cancel mult.commute)
lp15@59746
   300
  done
lp15@59746
   301
qed
lp15@59746
   302
lp15@59746
   303
lemma exp_i_ne_1: 
lp15@59746
   304
  assumes "0 < x" "x < 2*pi"
lp15@59746
   305
  shows "exp(\<i> * of_real x) \<noteq> 1"
lp15@59746
   306
proof 
lp15@59746
   307
  assume "exp (\<i> * of_real x) = 1"
lp15@59746
   308
  then have "exp (\<i> * of_real x) = exp 0"
lp15@59746
   309
    by simp
lp15@59746
   310
  then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
lp15@59746
   311
    by (simp only: Ints_def exp_eq) auto
lp15@59746
   312
  then have  "of_real x = (of_int (2 * n) * pi)"
lp15@59746
   313
    by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
lp15@59746
   314
  then have  "x = (of_int (2 * n) * pi)"
lp15@59746
   315
    by simp
lp15@59746
   316
  then show False using assms
lp15@59746
   317
    by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
lp15@59746
   318
qed
lp15@59746
   319
lp15@59746
   320
lemma sin_eq_0: 
lp15@59746
   321
  fixes z::complex
lp15@59746
   322
  shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
lp15@59746
   323
  by (simp add: sin_exp_eq exp_eq of_real_numeral)
lp15@59746
   324
lp15@59746
   325
lemma cos_eq_0: 
lp15@59746
   326
  fixes z::complex
lp15@59746
   327
  shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
lp15@59746
   328
  using sin_eq_0 [of "z - of_real pi/2"]
lp15@59746
   329
  by (simp add: sin_diff algebra_simps)
lp15@59746
   330
lp15@59746
   331
lemma cos_eq_1: 
lp15@59746
   332
  fixes z::complex
lp15@59746
   333
  shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
lp15@59746
   334
proof -
lp15@59746
   335
  have "cos z = cos (2*(z/2))"
lp15@59746
   336
    by simp
lp15@59746
   337
  also have "... = 1 - 2 * sin (z/2) ^ 2"
lp15@59746
   338
    by (simp only: cos_double_sin)
lp15@59746
   339
  finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
lp15@59746
   340
    by simp
lp15@59746
   341
  show ?thesis
lp15@59746
   342
    by (auto simp: sin_eq_0 of_real_numeral)
lp15@59746
   343
qed  
lp15@59746
   344
lp15@59746
   345
lemma csin_eq_1:
lp15@59746
   346
  fixes z::complex
lp15@59746
   347
  shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)"
lp15@59746
   348
  using cos_eq_1 [of "z - of_real pi/2"]
lp15@59746
   349
  by (simp add: cos_diff algebra_simps)
lp15@59746
   350
lp15@59746
   351
lemma csin_eq_minus1:
lp15@59746
   352
  fixes z::complex
lp15@59746
   353
  shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)"
lp15@59746
   354
        (is "_ = ?rhs")
lp15@59746
   355
proof -
lp15@59746
   356
  have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
lp15@59746
   357
    by (simp add: equation_minus_iff)
lp15@59746
   358
  also have "...  \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
lp15@59746
   359
    by (simp only: csin_eq_1)
lp15@59746
   360
  also have "...  \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
lp15@59746
   361
    apply (rule iff_exI)
lp15@59746
   362
    by (metis (no_types)  is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff)
lp15@59746
   363
  also have "... = ?rhs"
lp15@59746
   364
    apply (auto simp: of_real_numeral)
lp15@59746
   365
    apply (rule_tac [2] x="-(x+1)" in exI)
lp15@59746
   366
    apply (rule_tac x="-(x+1)" in exI)
lp15@59746
   367
    apply (simp_all add: algebra_simps)
lp15@59746
   368
    done
lp15@59746
   369
  finally show ?thesis .
lp15@59746
   370
qed  
lp15@59746
   371
lp15@59746
   372
lemma ccos_eq_minus1: 
lp15@59746
   373
  fixes z::complex
lp15@59746
   374
  shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
lp15@59746
   375
  using csin_eq_1 [of "z - of_real pi/2"]
lp15@59746
   376
  apply (simp add: sin_diff)
lp15@59746
   377
  apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
lp15@59746
   378
  done       
lp15@59746
   379
lp15@59746
   380
lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
lp15@59746
   381
                (is "_ = ?rhs")
lp15@59746
   382
proof -
lp15@59746
   383
  have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
lp15@59746
   384
    by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
lp15@59746
   385
  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
lp15@59746
   386
    by (simp only: csin_eq_1)
lp15@59746
   387
  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
lp15@59746
   388
    apply (rule iff_exI)
lp15@59746
   389
    apply (auto simp: algebra_simps of_real_numeral)
lp15@59746
   390
    apply (rule injD [OF inj_of_real [where 'a = complex]])
lp15@59746
   391
    apply (auto simp: of_real_numeral)
lp15@59746
   392
    done
lp15@59746
   393
  also have "... = ?rhs"
lp15@59746
   394
    by (auto simp: algebra_simps)
lp15@59746
   395
  finally show ?thesis .
lp15@59746
   396
qed  
lp15@59746
   397
lp15@59746
   398
lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
lp15@59746
   399
proof -
lp15@59746
   400
  have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
lp15@59746
   401
    by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
lp15@59746
   402
  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
lp15@59746
   403
    by (simp only: csin_eq_minus1)
lp15@59746
   404
  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
lp15@59746
   405
    apply (rule iff_exI)
lp15@59746
   406
    apply (auto simp: algebra_simps)
lp15@59746
   407
    apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
lp15@59746
   408
    done
lp15@59746
   409
  also have "... = ?rhs"
lp15@59746
   410
    by (auto simp: algebra_simps)
lp15@59746
   411
  finally show ?thesis .
lp15@59746
   412
qed  
lp15@59746
   413
lp15@59746
   414
lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
lp15@59746
   415
                      (is "_ = ?rhs")
lp15@59746
   416
proof -
lp15@59746
   417
  have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
lp15@59746
   418
    by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
lp15@59746
   419
  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
lp15@59746
   420
    by (simp only: ccos_eq_minus1)
lp15@59746
   421
  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
lp15@59746
   422
    apply (rule iff_exI)
lp15@59746
   423
    apply (auto simp: algebra_simps)
lp15@59746
   424
    apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
lp15@59746
   425
    done
lp15@59746
   426
  also have "... = ?rhs"
lp15@59746
   427
    by (auto simp: algebra_simps)
lp15@59746
   428
  finally show ?thesis .
lp15@59746
   429
qed  
lp15@59746
   430
lp15@59746
   431
lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
lp15@59746
   432
  apply (simp add: exp_Euler cmod_def power2_diff algebra_simps)
lp15@59746
   433
  using cos_double_sin [of "t/2"]
lp15@59746
   434
  apply (simp add: real_sqrt_mult)
lp15@59746
   435
  done
lp15@59746
   436
lp15@59746
   437
lemma sinh_complex:
lp15@59746
   438
  fixes z :: complex
lp15@59746
   439
  shows "(exp z - inverse (exp z)) / 2 = -ii * sin(ii * z)"
lp15@59746
   440
  by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
lp15@59746
   441
lp15@59746
   442
lemma sin_ii_times:
lp15@59746
   443
  fixes z :: complex
lp15@59746
   444
  shows "sin(ii * z) = ii * ((exp z - inverse (exp z)) / 2)"
lp15@59746
   445
  using sinh_complex by auto
lp15@59746
   446
lp15@59746
   447
lemma sinh_real:
lp15@59746
   448
  fixes x :: real
lp15@59746
   449
  shows "of_real((exp x - inverse (exp x)) / 2) = -ii * sin(ii * of_real x)"
lp15@59746
   450
  by (simp add: exp_of_real sin_ii_times of_real_numeral)
lp15@59746
   451
lp15@59746
   452
lemma cosh_complex:
lp15@59746
   453
  fixes z :: complex
lp15@59746
   454
  shows "(exp z + inverse (exp z)) / 2 = cos(ii * z)"
lp15@59746
   455
  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
lp15@59746
   456
lp15@59746
   457
lemma cosh_real:
lp15@59746
   458
  fixes x :: real
lp15@59746
   459
  shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)"
lp15@59746
   460
  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
lp15@59746
   461
lp15@59746
   462
lemmas cos_ii_times = cosh_complex [symmetric]
lp15@59746
   463
lp15@59746
   464
lemma norm_cos_squared: 
lp15@59746
   465
    "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
lp15@59746
   466
  apply (cases z)
lp15@59746
   467
  apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
lp15@59746
   468
  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
lp15@59746
   469
  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
lp15@59746
   470
  apply (simp add: sin_squared_eq)
lp15@59746
   471
  apply (simp add: power2_eq_square algebra_simps divide_simps)
lp15@59746
   472
  done
lp15@59746
   473
lp15@59746
   474
lemma norm_sin_squared:
lp15@59746
   475
    "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
lp15@59746
   476
  apply (cases z)
lp15@59746
   477
  apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
lp15@59746
   478
  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
lp15@59746
   479
  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
lp15@59746
   480
  apply (simp add: cos_squared_eq)
lp15@59746
   481
  apply (simp add: power2_eq_square algebra_simps divide_simps)
lp15@59746
   482
  done 
lp15@59746
   483
lp15@59746
   484
lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
lp15@59746
   485
  using abs_Im_le_cmod linear order_trans by fastforce
lp15@59746
   486
lp15@59746
   487
lemma norm_cos_le: 
lp15@59746
   488
  fixes z::complex
lp15@59746
   489
  shows "norm(cos z) \<le> exp(norm z)"
lp15@59746
   490
proof -
lp15@59746
   491
  have "Im z \<le> cmod z"
lp15@59746
   492
    using abs_Im_le_cmod abs_le_D1 by auto
lp15@59746
   493
  with exp_uminus_Im show ?thesis
lp15@59746
   494
    apply (simp add: cos_exp_eq norm_divide)
lp15@59746
   495
    apply (rule order_trans [OF norm_triangle_ineq], simp)
lp15@59746
   496
    apply (metis add_mono exp_le_cancel_iff mult_2_right)
lp15@59746
   497
    done
lp15@59746
   498
qed
lp15@59746
   499
lp15@59746
   500
lemma norm_cos_plus1_le: 
lp15@59746
   501
  fixes z::complex
lp15@59746
   502
  shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
lp15@59746
   503
proof -
lp15@59746
   504
  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
   505
      by arith
lp15@59746
   506
  have *: "Im z \<le> cmod z"
lp15@59746
   507
    using abs_Im_le_cmod abs_le_D1 by auto
lp15@59746
   508
  have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)"
lp15@59746
   509
    by (simp add: norm_add_rule_thm)
lp15@59746
   510
  have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
lp15@59746
   511
    by (simp add: cos_exp_eq)
lp15@59746
   512
  also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
lp15@59746
   513
    by (simp add: field_simps)
lp15@59746
   514
  also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
lp15@59746
   515
    by (simp add: norm_divide)
lp15@59746
   516
  finally show ?thesis
lp15@59746
   517
    apply (rule ssubst, simp)
lp15@59746
   518
    apply (rule order_trans [OF triangle3], simp)
lp15@59746
   519
    using exp_uminus_Im *
lp15@59746
   520
    apply (auto intro: mono)
lp15@59746
   521
    done
lp15@59746
   522
qed
lp15@59746
   523
lp15@59746
   524
subsection{* Taylor series for complex exponential, sine and cosine.*}
lp15@59746
   525
lp15@59746
   526
context 
lp15@59746
   527
begin
lp15@59746
   528
lp15@59746
   529
declare power_Suc [simp del]
lp15@59746
   530
lp15@59746
   531
lemma Taylor_exp: 
lp15@59746
   532
  "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
   533
proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
lp15@59746
   534
  show "convex (closed_segment 0 z)"
lp15@59746
   535
    by (rule convex_segment [of 0 z])
lp15@59746
   536
next
lp15@59746
   537
  fix k x
lp15@59746
   538
  assume "x \<in> closed_segment 0 z" "k \<le> n"
lp15@59746
   539
  show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
lp15@59746
   540
    using DERIV_exp DERIV_subset by blast
lp15@59746
   541
next
lp15@59746
   542
  fix x
lp15@59746
   543
  assume "x \<in> closed_segment 0 z"
lp15@59746
   544
  then show "Re x \<le> \<bar>Re z\<bar>"
lp15@59746
   545
    apply (auto simp: closed_segment_def scaleR_conv_of_real)
lp15@59746
   546
    by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans)
lp15@59746
   547
next
lp15@59746
   548
  show "0 \<in> closed_segment 0 z"
lp15@59746
   549
    by (auto simp: closed_segment_def)
lp15@59746
   550
next
lp15@59746
   551
  show "z \<in> closed_segment 0 z"
lp15@59746
   552
    apply (simp add: closed_segment_def scaleR_conv_of_real)
lp15@59746
   553
    using of_real_1 zero_le_one by blast
lp15@59746
   554
qed 
lp15@59746
   555
lp15@59746
   556
lemma 
lp15@59746
   557
  assumes "0 \<le> u" "u \<le> 1"
lp15@59746
   558
  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" 
lp15@59746
   559
    and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
lp15@59746
   560
proof -
lp15@59746
   561
  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
lp15@59746
   562
    by arith
lp15@59746
   563
  show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
lp15@59746
   564
    apply (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
lp15@59746
   565
    apply (rule order_trans [OF norm_triangle_ineq4])
lp15@59746
   566
    apply (rule mono)
lp15@59746
   567
    apply (auto simp: abs_if mult_left_le_one_le)
lp15@59746
   568
    apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
lp15@59746
   569
    apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
lp15@59746
   570
    done
lp15@59746
   571
  show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
lp15@59746
   572
    apply (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
lp15@59746
   573
    apply (rule order_trans [OF norm_triangle_ineq])
lp15@59746
   574
    apply (rule mono)
lp15@59746
   575
    apply (auto simp: abs_if mult_left_le_one_le)
lp15@59746
   576
    apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
lp15@59746
   577
    apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
lp15@59746
   578
    done
lp15@59746
   579
qed
lp15@59746
   580
    
lp15@59746
   581
lemma Taylor_sin: 
lp15@59746
   582
  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) 
lp15@59746
   583
   \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
lp15@59746
   584
proof -
lp15@59746
   585
  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
lp15@59746
   586
      by arith
lp15@59746
   587
  have *: "cmod (sin z -
lp15@59746
   588
                 (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
lp15@59746
   589
           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
lp15@59746
   590
  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
   591
simplified])
lp15@59746
   592
  show "convex (closed_segment 0 z)"
lp15@59746
   593
    by (rule convex_segment [of 0 z])
lp15@59746
   594
  next
lp15@59746
   595
    fix k x
lp15@59746
   596
    show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
lp15@59746
   597
            (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
lp15@59746
   598
            (at x within closed_segment 0 z)"
lp15@59746
   599
      apply (auto simp: power_Suc)
lp15@59746
   600
      apply (intro derivative_eq_intros | simp)+
lp15@59746
   601
      done
lp15@59746
   602
  next
lp15@59746
   603
    fix x
lp15@59746
   604
    assume "x \<in> closed_segment 0 z"
lp15@59746
   605
    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
   606
      by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
lp15@59746
   607
  next
lp15@59746
   608
    show "0 \<in> closed_segment 0 z"
lp15@59746
   609
      by (auto simp: closed_segment_def)
lp15@59746
   610
  next
lp15@59746
   611
    show "z \<in> closed_segment 0 z"
lp15@59746
   612
      apply (simp add: closed_segment_def scaleR_conv_of_real)
lp15@59746
   613
      using of_real_1 zero_le_one by blast
lp15@59746
   614
  qed 
lp15@59746
   615
  have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
lp15@59746
   616
            = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
lp15@59746
   617
    by (auto simp: sin_coeff_def elim!: oddE)
lp15@59746
   618
  show ?thesis
lp15@59746
   619
    apply (rule order_trans [OF _ *])
lp15@59746
   620
    apply (simp add: **)
lp15@59746
   621
    done
lp15@59746
   622
qed
lp15@59746
   623
lp15@59746
   624
lemma Taylor_cos: 
lp15@59746
   625
  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k)) 
lp15@59746
   626
   \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
lp15@59746
   627
proof -
lp15@59746
   628
  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
lp15@59746
   629
      by arith
lp15@59746
   630
  have *: "cmod (cos z -
lp15@59746
   631
                 (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
lp15@59746
   632
           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
lp15@59746
   633
  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
   634
simplified])
lp15@59746
   635
  show "convex (closed_segment 0 z)"
lp15@59746
   636
    by (rule convex_segment [of 0 z])
lp15@59746
   637
  next
lp15@59746
   638
    fix k x
lp15@59746
   639
    assume "x \<in> closed_segment 0 z" "k \<le> n"
lp15@59746
   640
    show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
lp15@59746
   641
            (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
lp15@59746
   642
             (at x within closed_segment 0 z)"
lp15@59746
   643
      apply (auto simp: power_Suc)
lp15@59746
   644
      apply (intro derivative_eq_intros | simp)+
lp15@59746
   645
      done
lp15@59746
   646
  next
lp15@59746
   647
    fix x
lp15@59746
   648
    assume "x \<in> closed_segment 0 z"
lp15@59746
   649
    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
   650
      by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
lp15@59746
   651
  next
lp15@59746
   652
    show "0 \<in> closed_segment 0 z"
lp15@59746
   653
      by (auto simp: closed_segment_def)
lp15@59746
   654
  next
lp15@59746
   655
    show "z \<in> closed_segment 0 z"
lp15@59746
   656
      apply (simp add: closed_segment_def scaleR_conv_of_real)
lp15@59746
   657
      using of_real_1 zero_le_one by blast
lp15@59746
   658
  qed 
lp15@59746
   659
  have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
lp15@59746
   660
            = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
lp15@59746
   661
    by (auto simp: cos_coeff_def elim!: evenE)
lp15@59746
   662
  show ?thesis
lp15@59746
   663
    apply (rule order_trans [OF _ *])
lp15@59746
   664
    apply (simp add: **)
lp15@59746
   665
    done
lp15@59746
   666
qed
lp15@59746
   667
lp15@59746
   668
end (* of context *)
lp15@59746
   669
lp15@59746
   670
subsection{*The argument of a complex number*}
lp15@59746
   671
lp15@59746
   672
definition Arg :: "complex \<Rightarrow> real" where
lp15@59746
   673
 "Arg z \<equiv> if z = 0 then 0
lp15@59746
   674
           else THE t. 0 \<le> t \<and> t < 2*pi \<and>
lp15@59746
   675
                    z = of_real(norm z) * exp(ii * of_real t)"
lp15@59746
   676
lp15@59746
   677
lemma Arg_0 [simp]: "Arg(0) = 0"
lp15@59746
   678
  by (simp add: Arg_def)
lp15@59746
   679
lp15@59746
   680
lemma Arg_unique_lemma:
lp15@59746
   681
  assumes z:  "z = of_real(norm z) * exp(ii * of_real t)"
lp15@59746
   682
      and z': "z = of_real(norm z) * exp(ii * of_real t')"
lp15@59746
   683
      and t:  "0 \<le> t"  "t < 2*pi"
lp15@59746
   684
      and t': "0 \<le> t'" "t' < 2*pi"
lp15@59746
   685
      and nz: "z \<noteq> 0"
lp15@59746
   686
  shows "t' = t"
lp15@59746
   687
proof -
lp15@59746
   688
  have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
lp15@59746
   689
    by arith
lp15@59746
   690
  have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
lp15@59746
   691
    by (metis z z')
lp15@59746
   692
  then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
lp15@59746
   693
    by (metis nz mult_left_cancel mult_zero_left z)
lp15@59746
   694
  then have "sin t' = sin t \<and> cos t' = cos t"
lp15@59746
   695
    apply (simp add: exp_Euler sin_of_real cos_of_real)
lp15@59746
   696
    by (metis Complex_eq complex.sel)
lp15@59746
   697
  then obtain n::int where n: "t' = t + 2 * real n * pi"
lp15@59746
   698
    by (auto simp: sin_cos_eq_iff)
lp15@59746
   699
  then have "n=0"
lp15@59746
   700
    apply (rule_tac z=n in int_cases)
lp15@59746
   701
    using t t'
lp15@59746
   702
    apply (auto simp: mult_less_0_iff algebra_simps)
lp15@59746
   703
    done
lp15@59746
   704
  then show "t' = t"
lp15@59746
   705
      by (simp add: n)
lp15@59746
   706
qed
lp15@59746
   707
lp15@59746
   708
lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(ii * of_real(Arg z))"
lp15@59746
   709
proof (cases "z=0")
lp15@59746
   710
  case True then show ?thesis
lp15@59746
   711
    by (simp add: Arg_def)
lp15@59746
   712
next
lp15@59746
   713
  case False
lp15@59746
   714
  obtain t where t: "0 \<le> t" "t < 2*pi"
lp15@59746
   715
             and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
lp15@59746
   716
    using sincos_total_2pi [OF complex_unit_circle [OF False]]
lp15@59746
   717
    by blast
lp15@59746
   718
  have z: "z = of_real(norm z) * exp(ii * of_real t)"
lp15@59746
   719
    apply (rule complex_eqI)
lp15@59746
   720
    using t False ReIm
lp15@59746
   721
    apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
lp15@59746
   722
    done
lp15@59746
   723
  show ?thesis
lp15@59746
   724
    apply (simp add: Arg_def False)
lp15@59746
   725
    apply (rule theI [where a=t])
lp15@59746
   726
    using t z False
lp15@59746
   727
    apply (auto intro: Arg_unique_lemma)
lp15@59746
   728
    done
lp15@59746
   729
qed
lp15@59746
   730
lp15@59746
   731
lp15@59746
   732
corollary
lp15@59746
   733
  shows Arg_ge_0: "0 \<le> Arg z"
lp15@59746
   734
    and Arg_lt_2pi: "Arg z < 2*pi"
lp15@59746
   735
    and Arg_eq: "z = of_real(norm z) * exp(ii * of_real(Arg z))"
lp15@59746
   736
  using Arg by auto
lp15@59746
   737
lp15@59746
   738
lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(ii * of_real t))"
lp15@59746
   739
  using Arg [of z] by auto
lp15@59746
   740
lp15@59746
   741
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
   742
  apply (rule Arg_unique_lemma [OF _ Arg_eq])
lp15@59746
   743
  using Arg [of z]
lp15@59746
   744
  apply (auto simp: norm_mult)
lp15@59746
   745
  done
lp15@59746
   746
lp15@59746
   747
lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
lp15@59746
   748
  apply (rule Arg_unique [of "norm z"])
lp15@59746
   749
  apply (rule complex_eqI)
lp15@59746
   750
  using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] Arg_eq [of z]
lp15@59746
   751
  apply auto
lp15@59746
   752
  apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
lp15@59746
   753
  apply (metis Re_rcis Im_rcis rcis_def)+
lp15@59746
   754
  done
lp15@59746
   755
lp15@59746
   756
lemma Arg_times_of_real [simp]: "0 < r \<Longrightarrow> Arg (of_real r * z) = Arg z"
lp15@59746
   757
  apply (cases "z=0", simp)
lp15@59746
   758
  apply (rule Arg_unique [of "r * norm z"])
lp15@59746
   759
  using Arg
lp15@59746
   760
  apply auto
lp15@59746
   761
  done
lp15@59746
   762
lp15@59746
   763
lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
lp15@59746
   764
  by (metis Arg_times_of_real mult.commute)
lp15@59746
   765
lp15@59746
   766
lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
lp15@59746
   767
  by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
lp15@59746
   768
lp15@59746
   769
lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
lp15@59746
   770
proof (cases "z=0")
lp15@59746
   771
  case True then show ?thesis
lp15@59746
   772
    by simp
lp15@59746
   773
next
lp15@59746
   774
  case False
lp15@59746
   775
  have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
lp15@59746
   776
    by (metis Arg_eq)
lp15@59746
   777
  also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
lp15@59746
   778
    using False
lp15@59746
   779
    by (simp add: zero_le_mult_iff)
lp15@59746
   780
  also have "... \<longleftrightarrow> Arg z \<le> pi"
lp15@59746
   781
    by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
lp15@59746
   782
  finally show ?thesis
lp15@59746
   783
    by blast
lp15@59746
   784
qed
lp15@59746
   785
lp15@59746
   786
lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
lp15@59746
   787
proof (cases "z=0")
lp15@59746
   788
  case True then show ?thesis
lp15@59746
   789
    by simp
lp15@59746
   790
next
lp15@59746
   791
  case False
lp15@59746
   792
  have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
lp15@59746
   793
    by (metis Arg_eq)
lp15@59746
   794
  also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
lp15@59746
   795
    using False
lp15@59746
   796
    by (simp add: zero_less_mult_iff)
lp15@59746
   797
  also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
lp15@59746
   798
    using Arg_ge_0  Arg_lt_2pi sin_le_zero sin_gt_zero
lp15@59746
   799
    apply (auto simp: Im_exp)
lp15@59746
   800
    using le_less apply fastforce
lp15@59746
   801
    using not_le by blast
lp15@59746
   802
  finally show ?thesis
lp15@59746
   803
    by blast
lp15@59746
   804
qed
lp15@59746
   805
lp15@59746
   806
lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
lp15@59746
   807
proof (cases "z=0")
lp15@59746
   808
  case True then show ?thesis
lp15@59746
   809
    by simp
lp15@59746
   810
next
lp15@59746
   811
  case False
lp15@59746
   812
  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
   813
    by (metis Arg_eq)
lp15@59746
   814
  also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
lp15@59746
   815
    using False
lp15@59746
   816
    by (simp add: zero_le_mult_iff)
lp15@59746
   817
  also have "... \<longleftrightarrow> Arg z = 0"
lp15@59746
   818
    apply (auto simp: Re_exp)
lp15@59746
   819
    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
   820
    using Arg_eq [of z]
lp15@59746
   821
    apply (auto simp: Reals_def)
lp15@59746
   822
    done
lp15@59746
   823
  finally show ?thesis
lp15@59746
   824
    by blast
lp15@59746
   825
qed
lp15@59746
   826
lp15@59746
   827
lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
lp15@59746
   828
  by (simp add: Arg_eq_0)
lp15@59746
   829
lp15@59746
   830
lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
lp15@59746
   831
  apply  (cases "z=0", simp)
lp15@59746
   832
  using Arg_eq_0 [of "-z"]
lp15@59746
   833
  apply (auto simp: complex_is_Real_iff Arg_minus)
lp15@59746
   834
  apply (simp add: complex_Re_Im_cancel_iff)
lp15@59746
   835
  apply (metis Arg_minus pi_gt_zero add.left_neutral minus_minus minus_zero)
lp15@59746
   836
  done
lp15@59746
   837
lp15@59746
   838
lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
lp15@59746
   839
  using Arg_eq_0 Arg_eq_pi not_le by auto
lp15@59746
   840
lp15@59746
   841
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
   842
  apply (cases "z=0", simp)
lp15@59746
   843
  apply (rule Arg_unique [of "inverse (norm z)"])
lp15@59746
   844
  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
   845
  apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
lp15@59746
   846
  done
lp15@59746
   847
lp15@59746
   848
lemma Arg_eq_iff:
lp15@59746
   849
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59746
   850
     shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
lp15@59746
   851
  using assms Arg_eq [of z] Arg_eq [of w]
lp15@59746
   852
  apply auto
lp15@59746
   853
  apply (rule_tac x="norm w / norm z" in exI)
lp15@59746
   854
  apply (simp add: divide_simps)
lp15@59746
   855
  by (metis mult.commute mult.left_commute)
lp15@59746
   856
lp15@59746
   857
lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
lp15@59746
   858
  using complex_is_Real_iff
lp15@59746
   859
  apply (simp add: Arg_eq_0)
lp15@59746
   860
  apply (auto simp: divide_simps not_sum_power2_lt_zero)
lp15@59746
   861
  done
lp15@59746
   862
lp15@59746
   863
lemma Arg_divide:
lp15@59746
   864
  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
lp15@59746
   865
    shows "Arg(z / w) = Arg z - Arg w"
lp15@59746
   866
  apply (rule Arg_unique [of "norm(z / w)"])
lp15@59746
   867
  using assms Arg_eq [of z] Arg_eq [of w] Arg_ge_0 [of w] Arg_lt_2pi [of z]
lp15@59746
   868
  apply (auto simp: exp_diff norm_divide algebra_simps divide_simps)
lp15@59746
   869
  done
lp15@59746
   870
lp15@59746
   871
lemma Arg_le_div_sum:
lp15@59746
   872
  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
lp15@59746
   873
    shows "Arg z = Arg w + Arg(z / w)"
lp15@59746
   874
  by (simp add: Arg_divide assms)
lp15@59746
   875
lp15@59746
   876
lemma Arg_le_div_sum_eq:
lp15@59746
   877
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59746
   878
    shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
lp15@59746
   879
  using assms
lp15@59746
   880
  by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
lp15@59746
   881
lp15@59746
   882
lemma Arg_diff:
lp15@59746
   883
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59746
   884
    shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
lp15@59746
   885
  using assms
lp15@59746
   886
  apply (auto simp: Arg_ge_0 Arg_divide not_le)
lp15@59746
   887
  using Arg_divide [of w z] Arg_inverse [of "w/z"]
lp15@59746
   888
  apply auto
lp15@59746
   889
  by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
lp15@59746
   890
lp15@59746
   891
lp15@59746
   892
lemma Arg_add:
lp15@59746
   893
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59746
   894
    shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
lp15@59746
   895
  using assms
lp15@59746
   896
  using Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
lp15@59746
   897
  apply (auto simp: Arg_ge_0 Arg_divide not_le)
lp15@59746
   898
  apply (metis Arg_lt_2pi add.commute)
lp15@59746
   899
  apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
lp15@59746
   900
  done
lp15@59746
   901
lp15@59746
   902
lemma Arg_times:
lp15@59746
   903
  assumes "w \<noteq> 0" "z \<noteq> 0"
lp15@59746
   904
    shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
lp15@59746
   905
                            else (Arg w + Arg z) - 2*pi)"
lp15@59746
   906
  using Arg_add [OF assms]
lp15@59746
   907
  by auto
lp15@59746
   908
lp15@59746
   909
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
   910
  apply (cases "z=0", simp)
lp15@59746
   911
  apply (rule trans [of _ "Arg(inverse z)"])
lp15@59746
   912
  apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
lp15@59746
   913
  apply (metis norm_eq_zero of_real_power zero_less_power2)
lp15@59746
   914
  apply (auto simp: of_real_numeral Arg_inverse)
lp15@59746
   915
  done
lp15@59746
   916
lp15@59746
   917
lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
lp15@59746
   918
  using Arg_eq_0 Arg_eq_0_pi
lp15@59746
   919
  by auto
lp15@59746
   920
lp15@59746
   921
lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
lp15@59746
   922
  by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
lp15@59746
   923
lp15@59745
   924
end