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.12    apply (simp add: real_sqrt_mult)
    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.48 +    by (metis (no_types, hide_lams) add_diff_cancel_left add_diff_cancel_left' add_minus_cancel
    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