src/HOL/Analysis/Complex_Transcendental.thy
 changeset 64773 223b2ebdda79 parent 64593 50c715579715 child 64790 ed38f9a834d8
```     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jan 03 23:21:09 2017 +0100
1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Jan 04 16:18:50 2017 +0000
1.3 @@ -6,6 +6,7 @@
1.4  imports
1.5    Complex_Analysis_Basics
1.6    Summation_Tests
1.7 +   "~~/src/HOL/Library/Periodic_Fun"
1.8  begin
1.9
1.10  (* TODO: Figure out what to do with MÃ¶bius transformations *)
1.11 @@ -400,6 +401,89 @@
1.13    done
1.14
1.15 +
1.16 +lemma complex_sin_eq:
1.17 +  fixes w :: complex
1.18 +  shows "sin w = sin z \<longleftrightarrow> (\<exists>n \<in> \<int>. w = z + of_real(2*n*pi) \<or> w = -z + of_real((2*n + 1)*pi))"
1.19 +        (is "?lhs = ?rhs")
1.20 +proof
1.21 +  assume ?lhs
1.22 +  then have "sin w - sin z = 0"
1.23 +    by (auto simp: algebra_simps)
1.24 +  then have "sin ((w - z) / 2)*cos ((w + z) / 2) = 0"
1.25 +    by (auto simp: sin_diff_sin)
1.26 +  then consider "sin ((w - z) / 2) = 0" | "cos ((w + z) / 2) = 0"
1.27 +    using mult_eq_0_iff by blast
1.28 +  then show ?rhs
1.29 +  proof cases
1.30 +    case 1
1.31 +    then show ?thesis
1.32 +      apply (auto simp: sin_eq_0 algebra_simps)
1.33 +      by (metis Ints_of_int of_real_of_int_eq)
1.34 +  next
1.35 +    case 2
1.36 +    then show ?thesis
1.37 +      apply (auto simp: cos_eq_0 algebra_simps)
1.38 +      by (metis Ints_of_int of_real_of_int_eq)
1.39 +  qed
1.40 +next
1.41 +  assume ?rhs
1.42 +  then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \<or>
1.43 +                               w = -z + of_real ((2* of_int n + 1)*pi)"
1.44 +    using Ints_cases by blast
1.45 +  then show ?lhs
1.46 +    using Periodic_Fun.sin.plus_of_int [of z n]
1.47 +    apply (auto simp: algebra_simps)
1.49 +              mult.commute sin.plus_of_int sin_minus sin_plus_pi)
1.50 +qed
1.51 +
1.52 +lemma complex_cos_eq:
1.53 +  fixes w :: complex
1.54 +  shows "cos w = cos z \<longleftrightarrow>
1.55 +         (\<exists>n \<in> \<int>. w = z + of_real(2*n*pi) \<or> w = -z + of_real(2*n*pi))"
1.56 +        (is "?lhs = ?rhs")
1.57 +proof
1.58 +  assume ?lhs
1.59 +  then have "cos w - cos z = 0"
1.60 +    by (auto simp: algebra_simps)
1.61 +  then have "sin ((w + z) / 2) * sin ((z - w) / 2) = 0"
1.62 +    by (auto simp: cos_diff_cos)
1.63 +  then consider "sin ((w + z) / 2) = 0" | "sin ((z - w) / 2) = 0"
1.64 +    using mult_eq_0_iff by blast
1.65 +  then show ?rhs
1.66 +  proof cases
1.67 +    case 1
1.68 +    then show ?thesis
1.69 +      apply (auto simp: sin_eq_0 algebra_simps)
1.70 +      by (metis Ints_of_int of_real_of_int_eq)
1.71 +  next
1.72 +    case 2
1.73 +    then show ?thesis
1.74 +      apply (auto simp: sin_eq_0 algebra_simps)
1.75 +      by (metis Ints_of_int add_minus_cancel distrib_right mult_of_int_commute mult_zero_right of_int_0 of_int_add of_real_of_int_eq)
1.76 +  qed
1.77 +next
1.78 +  assume ?rhs
1.79 +  then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \<or>
1.80 +                               w = -z + of_real(2*n*pi)"
1.81 +    using Ints_cases  by (metis of_int_mult of_int_numeral)
1.82 +  then show ?lhs
1.83 +    using Periodic_Fun.cos.plus_of_int [of z n]
1.84 +    apply (auto simp: algebra_simps)
1.85 +    by (metis cos.plus_of_int cos_minus minus_add_cancel mult.commute)
1.86 +qed
1.87 +
1.88 +lemma sin_eq:
1.89 +   "sin x = sin y \<longleftrightarrow> (\<exists>n \<in> \<int>. x = y + 2*n*pi \<or> x = -y + (2*n + 1)*pi)"
1.90 +  using complex_sin_eq [of x y]
1.91 +  by (simp only: sin_of_real Re_complex_of_real of_real_add [symmetric] of_real_minus [symmetric] of_real_mult [symmetric] of_real_eq_iff)
1.92 +
1.93 +lemma cos_eq:
1.94 +   "cos x = cos y \<longleftrightarrow> (\<exists>n \<in> \<int>. x = y + 2*n*pi \<or> x = -y + 2*n*pi)"
1.95 +  using complex_cos_eq [of x y]
1.96 +  by (simp only: cos_of_real Re_complex_of_real of_real_add [symmetric] of_real_minus [symmetric] of_real_mult [symmetric] of_real_eq_iff)
1.97 +
1.98  lemma sinh_complex:
1.99    fixes z :: complex
1.100    shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
1.101 @@ -2837,6 +2921,19 @@
1.102  lemma Re_Arccos_bound: "\<bar>Re(Arccos z)\<bar> \<le> pi"
1.103    by (meson Re_Arccos_bounds abs_le_iff less_eq_real_def minus_less_iff)
1.104
1.105 +lemma Im_Arccos_bound: "\<bar>Im (Arccos w)\<bar> \<le> cmod w"
1.106 +proof -
1.107 +  have "(Im (Arccos w))\<^sup>2 \<le> (cmod (cos (Arccos w)))\<^sup>2 - (cos (Re (Arccos w)))\<^sup>2"
1.108 +    using norm_cos_squared [of "Arccos w"] real_le_abs_sinh [of "Im (Arccos w)"]
1.109 +    apply (simp only: abs_le_square_iff)
1.110 +    apply (simp add: divide_simps)
1.111 +    done
1.112 +  also have "... \<le> (cmod w)\<^sup>2"
1.113 +    by (auto simp: cmod_power2)
1.114 +  finally show ?thesis
1.115 +    using abs_le_square_iff by force
1.116 +qed
1.117 +
1.118  lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
1.119    unfolding Re_Arcsin
1.120    by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
1.121 @@ -2844,6 +2941,21 @@
1.122  lemma Re_Arcsin_bound: "\<bar>Re(Arcsin z)\<bar> \<le> pi"
1.123    by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
1.124
1.125 +lemma norm_Arccos_bounded:
1.126 +  fixes w :: complex
1.127 +  shows "norm (Arccos w) \<le> pi + norm w"
1.128 +proof -
1.129 +  have Re: "(Re (Arccos w))\<^sup>2 \<le> pi\<^sup>2" "(Im (Arccos w))\<^sup>2 \<le> (cmod w)\<^sup>2"
1.130 +    using Re_Arccos_bound [of w] Im_Arccos_bound [of w] abs_le_square_iff by force+
1.131 +  have "Arccos w \<bullet> Arccos w \<le> pi\<^sup>2 + (cmod w)\<^sup>2"
1.132 +    using Re by (simp add: dot_square_norm cmod_power2 [of "Arccos w"])
1.133 +  then have "cmod (Arccos w) \<le> pi + cmod (cos (Arccos w))"
1.134 +    apply (simp add: norm_le_square)
1.135 +    by (metis dot_square_norm norm_ge_zero norm_le_square pi_ge_zero triangle_lemma)
1.136 +  then show "cmod (Arccos w) \<le> pi + cmod w"
1.137 +    by auto
1.138 +qed
1.139 +
1.140
1.141  subsection\<open>Interrelations between Arcsin and Arccos\<close>
1.142
```