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.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.103 +  fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
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.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
```