src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
changeset 60017 b785d6d06430
parent 59870 68d6b6aa4450
child 60020 065ecea354d0
     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
     1.5  begin
     1.6  
     1.7 -
     1.8  lemma cmod_add_real_less:
     1.9    assumes "Im z \<noteq> 0" "r\<noteq>0"
    1.10      shows "cmod (z + r) < cmod z + abs r"
    1.11 @@ -613,6 +612,14 @@
    1.12    apply (simp only: pos_le_divide_eq [symmetric], linarith)
    1.13    done
    1.14  
    1.15 +lemma e_less_3: "exp 1 < (3::real)"
    1.16 +  using e_approx_32
    1.17 +  by (simp add: abs_if split: split_if_asm)
    1.18 +
    1.19 +lemma ln3_gt_1: "ln 3 > (1::real)"
    1.20 +  by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
    1.21 +
    1.22 +
    1.23  subsection{*The argument of a complex number*}
    1.24  
    1.25  definition Arg :: "complex \<Rightarrow> real" where
    1.26 @@ -892,8 +899,9 @@
    1.27  
    1.28  subsection{*Complex logarithms (the conventional principal value)*}
    1.29  
    1.30 -definition Ln where
    1.31 -   "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
    1.32 +definition Ln :: "complex \<Rightarrow> complex"
    1.33 +  where "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
    1.34 +
    1.35  
    1.36  lemma
    1.37    assumes "z \<noteq> 0"
    1.38 @@ -941,6 +949,7 @@
    1.39    apply (auto simp: exp_of_nat_mult [symmetric])
    1.40    done
    1.41  
    1.42 +
    1.43  subsection{*The Unwinding Number and the Ln-product Formula*}
    1.44  
    1.45  text{*Note that in this special case the unwinding number is -1, 0 or 1.*}
    1.46 @@ -1128,8 +1137,8 @@
    1.47    apply (cases "z=0", auto)
    1.48    apply (rule exp_complex_eqI)
    1.49    apply (auto simp: abs_if split: split_if_asm)
    1.50 -  apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps(1) cnj.simps(2) mult_2 neg_equal_0_iff_equal)
    1.51 -  apply (metis add_mono_thms_linordered_field(5) complex_cnj_zero_iff diff_0_right diff_minus_eq_add minus_diff_eq mpi_less_Im_Ln mult.commute mult_2_right neg_less_iff_less)
    1.52 +  apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps mult_2 neg_equal_0_iff_equal)
    1.53 +  apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff mpi_less_Im_Ln mult.commute mult_2_right)
    1.54    by (metis exp_Ln exp_cnj)
    1.55  
    1.56  lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
    1.57 @@ -1141,7 +1150,7 @@
    1.58                 inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
    1.59    done
    1.60  
    1.61 -lemma Ln_1 [simp]: "Ln(1) = 0"
    1.62 +lemma Ln_1 [simp]: "Ln 1 = 0"
    1.63  proof -
    1.64    have "Ln (exp 0) = 0"
    1.65      by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
    1.66 @@ -1149,6 +1158,18 @@
    1.67      by simp
    1.68  qed
    1.69  
    1.70 +instantiation complex :: ln
    1.71 +begin
    1.72 +
    1.73 +definition ln_complex :: "complex \<Rightarrow> complex"
    1.74 +  where "ln_complex \<equiv> Ln"
    1.75 +
    1.76 +instance 
    1.77 +  by intro_classes (simp add: ln_complex_def)
    1.78 +
    1.79 +end
    1.80 +
    1.81 +
    1.82  lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
    1.83    apply (rule exp_complex_eqI)
    1.84    using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
    1.85 @@ -1242,6 +1263,93 @@
    1.86    by (auto simp: of_real_numeral Ln_times)
    1.87  
    1.88  
    1.89 +
    1.90 +subsection{*Complex Powers*}
    1.91 +
    1.92 +lemma powr_0 [simp]: "0 powr z = 0"
    1.93 +  by (simp add: powr_def)
    1.94 +
    1.95 +lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
    1.96 +  by (simp add: powr_def ln_complex_def)
    1.97 +
    1.98 +lemma powr_nat:
    1.99 +  fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
   1.100 +  by (simp add: exp_of_nat_mult powr_def ln_complex_def)
   1.101 +
   1.102 +lemma powr_add:
   1.103 +  fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
   1.104 +  by (simp add: powr_def algebra_simps exp_add)
   1.105 +
   1.106 +lemma powr_minus:
   1.107 +  fixes w::complex shows  "w powr (-z) = inverse(w powr z)"
   1.108 +  by (simp add: powr_def exp_minus)
   1.109 +
   1.110 +lemma powr_diff:
   1.111 +  fixes w::complex shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
   1.112 +  by (simp add: powr_def algebra_simps exp_diff)
   1.113 +
   1.114 +lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
   1.115 +  apply (simp add: powr_def ln_complex_def)
   1.116 +  using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
   1.117 +  by auto
   1.118 +
   1.119 +lemma powr_real_real:
   1.120 +    "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
   1.121 +  apply (simp add: powr_def ln_complex_def)
   1.122 +  by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
   1.123 +       exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
   1.124 +
   1.125 +lemma powr_of_real:
   1.126 +  fixes x::real
   1.127 +  shows "0 < x \<Longrightarrow> x powr y = x powr y"
   1.128 +  by (simp add: powr_def powr_real_real)
   1.129 +
   1.130 +lemma norm_powr_real_mono:
   1.131 +    "w \<in> \<real> \<Longrightarrow> 1 < Re w
   1.132 +             \<Longrightarrow> norm(w powr z1) \<le> norm(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
   1.133 +  by (auto simp: powr_def ln_complex_def algebra_simps Reals_def Ln_of_real)
   1.134 +
   1.135 +lemma powr_times_real:
   1.136 +    "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
   1.137 +           \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
   1.138 +  by (auto simp: Reals_def powr_def ln_complex_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
   1.139 +
   1.140 +lemma has_field_derivative_powr:
   1.141 +    "(Im z = 0 \<Longrightarrow> 0 < Re z)
   1.142 +     \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
   1.143 +  apply (cases "z=0", auto)
   1.144 +  apply (simp add: powr_def ln_complex_def)
   1.145 +  apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
   1.146 +  apply (auto simp: dist_complex_def ln_complex_def)
   1.147 +  apply (intro derivative_eq_intros | simp add: assms)+
   1.148 +  apply (simp add: field_simps exp_diff)
   1.149 +  done
   1.150 +
   1.151 +lemma has_field_derivative_powr_right:
   1.152 +    "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
   1.153 +  apply (simp add: powr_def ln_complex_def)
   1.154 +  apply (intro derivative_eq_intros | simp add: assms)+
   1.155 +  done
   1.156 +
   1.157 +lemma complex_differentiable_powr_right:
   1.158 +    "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
   1.159 +using complex_differentiable_def has_field_derivative_powr_right by blast
   1.160 +
   1.161 +
   1.162 +lemma holomorphic_on_powr_right:
   1.163 +    "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
   1.164 +    unfolding holomorphic_on_def
   1.165 +    using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
   1.166 +
   1.167 +
   1.168 +lemma norm_powr_real_powr:
   1.169 +  "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
   1.170 +  by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm ln_complex_def)
   1.171 +
   1.172 +lemma cmod_Ln_Reals [simp]:"z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (Ln z) = norm (ln (Re z))"
   1.173 +  using Ln_of_real by force
   1.174 +
   1.175 +
   1.176  subsection{*Relation between Square Root and exp/ln, hence its derivative*}
   1.177  
   1.178  lemma csqrt_exp_Ln:
   1.179 @@ -1336,10 +1444,6 @@
   1.180    using open_Compl
   1.181    by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
   1.182  
   1.183 -lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
   1.184 -  using closed_halfspace_Re_ge
   1.185 -  by (simp add: closed_Int closed_complex_Reals)
   1.186 -
   1.187  lemma continuous_within_csqrt_posreal:
   1.188      "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
   1.189  proof (cases "Im z = 0 --> 0 < Re(z)")
   1.190 @@ -1867,15 +1971,15 @@
   1.191               Re z = pi & Im z \<le> 0"
   1.192        shows "Arccos(cos z) = z"
   1.193  proof -
   1.194 -  have *: "((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z))) = sin z"
   1.195 +  have *: "((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z))) = sin z"
   1.196      by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square)
   1.197 -  have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2"
   1.198 +  have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2"
   1.199      by (simp add: field_simps power2_eq_square)
   1.200    then have "Arccos(cos z) = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
   1.201 -                           \<i> * csqrt (((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2)))"
   1.202 +                           \<i> * csqrt (((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2)))"
   1.203      by (simp add: cos_exp_eq Arccos_def exp_minus)
   1.204    also have "... = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
   1.205 -                              \<i> * ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))))"
   1.206 +                              \<i> * ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))))"
   1.207      apply (subst csqrt_square)
   1.208      using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z]
   1.209      apply (auto simp: * Re_sin Im_sin)
   1.210 @@ -2177,4 +2281,129 @@
   1.211  lemma of_real_arccos: "abs x \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
   1.212    by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
   1.213  
   1.214 +subsection{*Some interrelationships among the real inverse trig functions.*}
   1.215 +
   1.216 +lemma arccos_arctan:
   1.217 +  assumes "-1 < x" "x < 1"
   1.218 +    shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))"
   1.219 +proof -
   1.220 +  have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0"
   1.221 +  proof (rule sin_eq_0_pi)
   1.222 +    show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)"
   1.223 +      using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"]  arccos_bounded [of x] assms
   1.224 +      by (simp add: algebra_simps)
   1.225 +  next
   1.226 +    show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi"
   1.227 +      using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"]  arccos_bounded [of x] assms
   1.228 +      by (simp add: algebra_simps)
   1.229 +  next
   1.230 +    show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0"
   1.231 +      using assms
   1.232 +      by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
   1.233 +                    power2_eq_square square_eq_1_iff)
   1.234 +  qed
   1.235 +  then show ?thesis
   1.236 +    by simp
   1.237 +qed
   1.238 +
   1.239 +lemma arcsin_plus_arccos:
   1.240 +  assumes "-1 \<le> x" "x \<le> 1"
   1.241 +    shows "arcsin x + arccos x = pi/2"
   1.242 +proof -
   1.243 +  have "arcsin x = pi/2 - arccos x"
   1.244 +    apply (rule sin_inj_pi)
   1.245 +    using assms arcsin [OF assms] arccos [OF assms]
   1.246 +    apply (auto simp: algebra_simps sin_diff)
   1.247 +    done
   1.248 +  then show ?thesis
   1.249 +    by (simp add: algebra_simps)
   1.250 +qed
   1.251 +
   1.252 +lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x"
   1.253 +  using arcsin_plus_arccos by force
   1.254 +
   1.255 +lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x"
   1.256 +  using arcsin_plus_arccos by force
   1.257 +
   1.258 +lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
   1.259 +  by (simp add: arccos_arctan arcsin_arccos_eq)
   1.260 +
   1.261 +lemma zz: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
   1.262 +  by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
   1.263 +
   1.264 +lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
   1.265 +  apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
   1.266 +  apply (subst Arcsin_Arccos_csqrt_pos)
   1.267 +  apply (auto simp: power_le_one zz)
   1.268 +  done
   1.269 +
   1.270 +lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
   1.271 +  using arcsin_arccos_sqrt_pos [of "-x"]
   1.272 +  by (simp add: arcsin_minus)
   1.273 +
   1.274 +lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
   1.275 +  apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
   1.276 +  apply (subst Arccos_Arcsin_csqrt_pos)
   1.277 +  apply (auto simp: power_le_one zz)
   1.278 +  done
   1.279 +
   1.280 +lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
   1.281 +  using arccos_arcsin_sqrt_pos [of "-x"]
   1.282 +  by (simp add: arccos_minus)
   1.283 +
   1.284 +subsection{*continuity results for arcsin and arccos.*}
   1.285 +
   1.286 +lemma continuous_on_Arcsin_real [continuous_intros]:
   1.287 +    "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
   1.288 +proof -
   1.289 +  have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arcsin (Re x))) =
   1.290 +        continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arcsin (of_real (Re x)))))"
   1.291 +    by (rule continuous_on_cong [OF refl]) (simp add: arcsin_eq_Re_Arcsin)
   1.292 +  also have "... = ?thesis"
   1.293 +    by (rule continuous_on_cong [OF refl]) simp
   1.294 +  finally show ?thesis
   1.295 +    using continuous_on_arcsin [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
   1.296 +          continuous_on_of_real
   1.297 +    by fastforce
   1.298 +qed
   1.299 +
   1.300 +lemma continuous_within_Arcsin_real:
   1.301 +    "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arcsin"
   1.302 +proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
   1.303 +  case True then show ?thesis
   1.304 +    using continuous_on_Arcsin_real continuous_on_eq_continuous_within
   1.305 +    by blast
   1.306 +next
   1.307 +  case False
   1.308 +  with closed_real_abs_le [of 1] show ?thesis
   1.309 +    by (rule continuous_within_closed_nontrivial)
   1.310 +qed
   1.311 +
   1.312 +lemma continuous_on_Arccos_real:
   1.313 +    "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arccos"
   1.314 +proof -
   1.315 +  have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arccos (Re x))) =
   1.316 +        continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arccos (of_real (Re x)))))"
   1.317 +    by (rule continuous_on_cong [OF refl]) (simp add: arccos_eq_Re_Arccos)
   1.318 +  also have "... = ?thesis"
   1.319 +    by (rule continuous_on_cong [OF refl]) simp
   1.320 +  finally show ?thesis
   1.321 +    using continuous_on_arccos [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
   1.322 +          continuous_on_of_real
   1.323 +    by fastforce
   1.324 +qed
   1.325 +
   1.326 +lemma continuous_within_Arccos_real:
   1.327 +    "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arccos"
   1.328 +proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
   1.329 +  case True then show ?thesis
   1.330 +    using continuous_on_Arccos_real continuous_on_eq_continuous_within
   1.331 +    by blast
   1.332 +next
   1.333 +  case False
   1.334 +  with closed_real_abs_le [of 1] show ?thesis
   1.335 +    by (rule continuous_within_closed_nontrivial)
   1.336 +qed
   1.337 +
   1.338 +
   1.339  end