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