src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
 author paulson 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
```