src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
changeset 59862 44b3f4fa33ca
parent 59751 916c0f6c83e3
child 59870 68d6b6aa4450
     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Mar 31 00:21:07 2015 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Mar 31 15:00:03 2015 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5  theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)"
     1.6  proof -
     1.7 -  have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) 
     1.8 +  have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n)
     1.9          = (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))"
    1.10    proof
    1.11      fix n
    1.12 @@ -74,13 +74,11 @@
    1.13  
    1.14  subsection{*Relationships between real and complex trig functions*}
    1.15  
    1.16 -declare sin_of_real [simp] cos_of_real [simp]
    1.17 -
    1.18  lemma real_sin_eq [simp]:
    1.19    fixes x::real
    1.20    shows "Re(sin(of_real x)) = sin x"
    1.21    by (simp add: sin_of_real)
    1.22 -  
    1.23 +
    1.24  lemma real_cos_eq [simp]:
    1.25    fixes x::real
    1.26    shows "Re(cos(of_real x)) = cos x"
    1.27 @@ -100,10 +98,10 @@
    1.28      by (rule exp_converges)
    1.29    finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
    1.30    moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
    1.31 -    by (metis exp_converges sums_cnj) 
    1.32 +    by (metis exp_converges sums_cnj)
    1.33    ultimately show ?thesis
    1.34      using sums_unique2
    1.35 -    by blast 
    1.36 +    by blast
    1.37  qed
    1.38  
    1.39  lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
    1.40 @@ -112,15 +110,6 @@
    1.41  lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
    1.42    by (simp add: cos_exp_eq exp_cnj field_simps)
    1.43  
    1.44 -lemma exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
    1.45 -  by (metis Reals_cases Reals_of_real exp_of_real)
    1.46 -
    1.47 -lemma sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
    1.48 -  by (metis Reals_cases Reals_of_real sin_of_real)
    1.49 -
    1.50 -lemma cos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> cos z \<in> \<real>"
    1.51 -  by (metis Reals_cases Reals_of_real cos_of_real)
    1.52 -
    1.53  lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
    1.54    using DERIV_sin complex_differentiable_def by blast
    1.55  
    1.56 @@ -141,7 +130,7 @@
    1.57  
    1.58  subsection{* Get a nice real/imaginary separation in Euler's formula.*}
    1.59  
    1.60 -lemma Euler: "exp(z) = of_real(exp(Re z)) * 
    1.61 +lemma Euler: "exp(z) = of_real(exp(Re z)) *
    1.62                (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
    1.63  by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
    1.64  
    1.65 @@ -156,11 +145,20 @@
    1.66  
    1.67  lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
    1.68    by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
    1.69 -  
    1.70 +
    1.71 +lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
    1.72 +  by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
    1.73 +
    1.74 +lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
    1.75 +  by (simp add: Re_sin Im_sin algebra_simps)
    1.76 +
    1.77 +lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
    1.78 +  by (simp add: Re_sin Im_sin algebra_simps)
    1.79 +
    1.80  subsection{*More on the Polar Representation of Complex Numbers*}
    1.81  
    1.82  lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
    1.83 -  by (simp add: exp_add exp_Euler exp_of_real)
    1.84 +  by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
    1.85  
    1.86  lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
    1.87  apply auto
    1.88 @@ -183,7 +181,7 @@
    1.89  lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
    1.90    by (auto simp: exp_eq abs_mult)
    1.91  
    1.92 -lemma exp_integer_2pi: 
    1.93 +lemma exp_integer_2pi:
    1.94    assumes "n \<in> Ints"
    1.95    shows "exp((2 * n * pi) * ii) = 1"
    1.96  proof -
    1.97 @@ -208,10 +206,10 @@
    1.98    done
    1.99  qed
   1.100  
   1.101 -lemma exp_i_ne_1: 
   1.102 +lemma exp_i_ne_1:
   1.103    assumes "0 < x" "x < 2*pi"
   1.104    shows "exp(\<i> * of_real x) \<noteq> 1"
   1.105 -proof 
   1.106 +proof
   1.107    assume "exp (\<i> * of_real x) = 1"
   1.108    then have "exp (\<i> * of_real x) = exp 0"
   1.109      by simp
   1.110 @@ -225,18 +223,18 @@
   1.111      by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
   1.112  qed
   1.113  
   1.114 -lemma sin_eq_0: 
   1.115 +lemma sin_eq_0:
   1.116    fixes z::complex
   1.117    shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
   1.118    by (simp add: sin_exp_eq exp_eq of_real_numeral)
   1.119  
   1.120 -lemma cos_eq_0: 
   1.121 +lemma cos_eq_0:
   1.122    fixes z::complex
   1.123    shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
   1.124    using sin_eq_0 [of "z - of_real pi/2"]
   1.125    by (simp add: sin_diff algebra_simps)
   1.126  
   1.127 -lemma cos_eq_1: 
   1.128 +lemma cos_eq_1:
   1.129    fixes z::complex
   1.130    shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
   1.131  proof -
   1.132 @@ -248,7 +246,7 @@
   1.133      by simp
   1.134    show ?thesis
   1.135      by (auto simp: sin_eq_0 of_real_numeral)
   1.136 -qed  
   1.137 +qed
   1.138  
   1.139  lemma csin_eq_1:
   1.140    fixes z::complex
   1.141 @@ -275,15 +273,15 @@
   1.142      apply (simp_all add: algebra_simps)
   1.143      done
   1.144    finally show ?thesis .
   1.145 -qed  
   1.146 +qed
   1.147  
   1.148 -lemma ccos_eq_minus1: 
   1.149 +lemma ccos_eq_minus1:
   1.150    fixes z::complex
   1.151    shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
   1.152    using csin_eq_1 [of "z - of_real pi/2"]
   1.153    apply (simp add: sin_diff)
   1.154    apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
   1.155 -  done       
   1.156 +  done
   1.157  
   1.158  lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
   1.159                  (is "_ = ?rhs")
   1.160 @@ -301,7 +299,7 @@
   1.161    also have "... = ?rhs"
   1.162      by (auto simp: algebra_simps)
   1.163    finally show ?thesis .
   1.164 -qed  
   1.165 +qed
   1.166  
   1.167  lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
   1.168  proof -
   1.169 @@ -317,7 +315,7 @@
   1.170    also have "... = ?rhs"
   1.171      by (auto simp: algebra_simps)
   1.172    finally show ?thesis .
   1.173 -qed  
   1.174 +qed
   1.175  
   1.176  lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
   1.177                        (is "_ = ?rhs")
   1.178 @@ -334,10 +332,10 @@
   1.179    also have "... = ?rhs"
   1.180      by (auto simp: algebra_simps)
   1.181    finally show ?thesis .
   1.182 -qed  
   1.183 +qed
   1.184  
   1.185  lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
   1.186 -  apply (simp add: exp_Euler cmod_def power2_diff algebra_simps)
   1.187 +  apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
   1.188    using cos_double_sin [of "t/2"]
   1.189    apply (simp add: real_sqrt_mult)
   1.190    done
   1.191 @@ -369,7 +367,7 @@
   1.192  
   1.193  lemmas cos_ii_times = cosh_complex [symmetric]
   1.194  
   1.195 -lemma norm_cos_squared: 
   1.196 +lemma norm_cos_squared:
   1.197      "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
   1.198    apply (cases z)
   1.199    apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
   1.200 @@ -387,12 +385,12 @@
   1.201    apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   1.202    apply (simp add: cos_squared_eq)
   1.203    apply (simp add: power2_eq_square algebra_simps divide_simps)
   1.204 -  done 
   1.205 +  done
   1.206  
   1.207  lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
   1.208    using abs_Im_le_cmod linear order_trans by fastforce
   1.209  
   1.210 -lemma norm_cos_le: 
   1.211 +lemma norm_cos_le:
   1.212    fixes z::complex
   1.213    shows "norm(cos z) \<le> exp(norm z)"
   1.214  proof -
   1.215 @@ -405,7 +403,7 @@
   1.216      done
   1.217  qed
   1.218  
   1.219 -lemma norm_cos_plus1_le: 
   1.220 +lemma norm_cos_plus1_le:
   1.221    fixes z::complex
   1.222    shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
   1.223  proof -
   1.224 @@ -431,12 +429,12 @@
   1.225  
   1.226  subsection{* Taylor series for complex exponential, sine and cosine.*}
   1.227  
   1.228 -context 
   1.229 +context
   1.230  begin
   1.231  
   1.232  declare power_Suc [simp del]
   1.233  
   1.234 -lemma Taylor_exp: 
   1.235 +lemma Taylor_exp:
   1.236    "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   1.237  proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
   1.238    show "convex (closed_segment 0 z)"
   1.239 @@ -459,11 +457,11 @@
   1.240    show "z \<in> closed_segment 0 z"
   1.241      apply (simp add: closed_segment_def scaleR_conv_of_real)
   1.242      using of_real_1 zero_le_one by blast
   1.243 -qed 
   1.244 +qed
   1.245  
   1.246 -lemma 
   1.247 +lemma
   1.248    assumes "0 \<le> u" "u \<le> 1"
   1.249 -  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" 
   1.250 +  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   1.251      and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   1.252  proof -
   1.253    have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   1.254 @@ -485,16 +483,16 @@
   1.255      apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   1.256      done
   1.257  qed
   1.258 -    
   1.259 -lemma Taylor_sin: 
   1.260 -  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) 
   1.261 +
   1.262 +lemma Taylor_sin:
   1.263 +  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
   1.264     \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   1.265  proof -
   1.266    have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   1.267        by arith
   1.268    have *: "cmod (sin z -
   1.269                   (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
   1.270 -           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
   1.271 +           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   1.272    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,
   1.273  simplified])
   1.274    show "convex (closed_segment 0 z)"
   1.275 @@ -519,7 +517,7 @@
   1.276      show "z \<in> closed_segment 0 z"
   1.277        apply (simp add: closed_segment_def scaleR_conv_of_real)
   1.278        using of_real_1 zero_le_one by blast
   1.279 -  qed 
   1.280 +  qed
   1.281    have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
   1.282              = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
   1.283      by (auto simp: sin_coeff_def elim!: oddE)
   1.284 @@ -529,15 +527,15 @@
   1.285      done
   1.286  qed
   1.287  
   1.288 -lemma Taylor_cos: 
   1.289 -  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k)) 
   1.290 +lemma Taylor_cos:
   1.291 +  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k))
   1.292     \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
   1.293  proof -
   1.294    have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   1.295        by arith
   1.296    have *: "cmod (cos z -
   1.297                   (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
   1.298 -           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
   1.299 +           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   1.300    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,
   1.301  simplified])
   1.302    show "convex (closed_segment 0 z)"
   1.303 @@ -563,7 +561,7 @@
   1.304      show "z \<in> closed_segment 0 z"
   1.305        apply (simp add: closed_segment_def scaleR_conv_of_real)
   1.306        using of_real_1 zero_le_one by blast
   1.307 -  qed 
   1.308 +  qed
   1.309    have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
   1.310              = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
   1.311      by (auto simp: cos_coeff_def elim!: evenE)
   1.312 @@ -910,6 +908,21 @@
   1.313    apply (auto simp: exp_of_nat_mult [symmetric])
   1.314    done
   1.315  
   1.316 +subsection{*The Unwinding Number and the Ln-product Formula*}
   1.317 +
   1.318 +text{*Note that in this special case the unwinding number is -1, 0 or 1.*}
   1.319 +
   1.320 +definition unwinding :: "complex \<Rightarrow> complex" where
   1.321 +   "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * ii)"
   1.322 +
   1.323 +lemma unwinding_2pi: "(2*pi) * ii * unwinding(z) = z - Ln(exp z)"
   1.324 +  by (simp add: unwinding_def)
   1.325 +
   1.326 +lemma Ln_times_unwinding:
   1.327 +    "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * ii * unwinding(Ln w + Ln z)"
   1.328 +  using unwinding_2pi by (simp add: exp_add)
   1.329 +
   1.330 +
   1.331  subsection{*Derivative of Ln away from the branch cut*}
   1.332  
   1.333  lemma
   1.334 @@ -944,6 +957,10 @@
   1.335  lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
   1.336    by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
   1.337  
   1.338 +lemma isCont_Ln' [simp]:
   1.339 +   "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
   1.340 +  by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
   1.341 +
   1.342  lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
   1.343    using continuous_at_Ln continuous_at_imp_continuous_within by blast
   1.344  
   1.345 @@ -956,7 +973,7 @@
   1.346  
   1.347  subsection{*Relation to Real Logarithm*}
   1.348  
   1.349 -lemma ln_of_real:
   1.350 +lemma Ln_of_real:
   1.351    assumes "0 < z"
   1.352      shows "Ln(of_real z) = of_real(ln z)"
   1.353  proof -
   1.354 @@ -969,6 +986,9 @@
   1.355      using assms by simp
   1.356  qed
   1.357  
   1.358 +corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> Ln z \<in> \<real>"
   1.359 +  by (auto simp: Ln_of_real elim: Reals_cases)
   1.360 +
   1.361  
   1.362  subsection{*Quadrant-type results for Ln*}
   1.363  
   1.364 @@ -1091,7 +1111,7 @@
   1.365  lemma Ln_1 [simp]: "Ln(1) = 0"
   1.366  proof -
   1.367    have "Ln (exp 0) = 0"
   1.368 -    by (metis exp_zero ln_exp ln_of_real of_real_0 of_real_1 zero_less_one)
   1.369 +    by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
   1.370    then show ?thesis
   1.371      by simp
   1.372  qed
   1.373 @@ -1262,6 +1282,10 @@
   1.374      "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
   1.375    by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
   1.376  
   1.377 +corollary isCont_csqrt' [simp]:
   1.378 +   "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
   1.379 +  by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
   1.380 +
   1.381  lemma continuous_within_csqrt:
   1.382      "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
   1.383    by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)