src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
 changeset 61524 f2e51e704a96 parent 61518 ff12606337e9 child 61560 7c985fd653c5 child 61609 77b453bd616f
```     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Oct 27 23:18:32 2015 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Oct 29 15:40:52 2015 +0100
1.3 @@ -977,7 +977,6 @@
1.4    apply (auto simp: exp_of_nat_mult [symmetric])
1.5    done
1.6
1.7 -
1.8  subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
1.9
1.10  text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
1.11 @@ -1262,6 +1261,21 @@
1.12          Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
1.13    by (auto simp: of_real_numeral Ln_times)
1.14
1.15 +lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
1.16 +  by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
1.17 +
1.18 +lemma Ln_of_nat_over_of_nat:
1.19 +  assumes "m > 0" "n > 0"
1.20 +  shows   "Ln (of_nat m / of_nat n) = of_real (ln (of_nat m) - ln (of_nat n))"
1.21 +proof -
1.22 +  have "of_nat m / of_nat n = (of_real (of_nat m / of_nat n) :: complex)" by simp
1.23 +  also from assms have "Ln ... = of_real (ln (of_nat m / of_nat n))"
1.24 +    by (simp add: Ln_of_real[symmetric])
1.25 +  also from assms have "... = of_real (ln (of_nat m) - ln (of_nat n))"
1.26 +    by (simp add: ln_div)
1.27 +  finally show ?thesis .
1.28 +qed
1.29 +
1.30
1.31  subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
1.32
1.33 @@ -1445,6 +1459,15 @@
1.34    using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
1.35    by auto
1.36
1.37 +lemma cnj_powr:
1.38 +  assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"
1.39 +  shows   "cnj (a powr b) = cnj a powr cnj b"
1.40 +proof (cases "a = 0")
1.41 +  case False
1.42 +  with assms have "Im a = 0 \<Longrightarrow> Re a > 0" by (auto simp: complex_eq_iff)
1.43 +  with False show ?thesis by (simp add: powr_def exp_cnj cnj_Ln)
1.44 +qed simp
1.45 +
1.46  lemma powr_real_real:
1.47      "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
1.48    apply (simp add: powr_def)
1.49 @@ -1466,6 +1489,19 @@
1.50             \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
1.51    by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
1.52
1.53 +lemma powr_neg_real_complex:
1.54 +  shows   "(- of_real x) powr a = (-1) powr (of_real (sgn x) * a) * of_real x powr (a :: complex)"
1.55 +proof (cases "x = 0")
1.56 +  assume x: "x \<noteq> 0"
1.57 +  hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)
1.58 +  also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \<i>"
1.59 +    by (simp add: Ln_minus Ln_of_real)
1.60 +  also from x assms have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
1.61 +    by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)
1.62 +  also note cis_pi
1.63 +  finally show ?thesis by simp
1.64 +qed simp_all
1.65 +
1.66  lemma has_field_derivative_powr:
1.67      "(Im z = 0 \<Longrightarrow> 0 < Re z)
1.68       \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
1.69 @@ -1477,6 +1513,25 @@
1.70    apply (simp add: field_simps exp_diff)
1.71    done
1.72
1.73 +lemma has_field_derivative_powr_complex':
1.74 +  assumes "Im z \<noteq> 0 \<or> Re z > 0"
1.75 +  shows "((\<lambda>z. z powr r :: complex) has_field_derivative r * z powr (r - 1)) (at z)"
1.76 +proof (subst DERIV_cong_ev[OF refl _ refl])
1.77 +  from assms have "eventually (\<lambda>z. z \<noteq> 0) (nhds z)" by (intro t1_space_nhds) auto
1.78 +  thus "eventually (\<lambda>z. z powr r = Exp (r * Ln z)) (nhds z)"
1.79 +    unfolding powr_def by eventually_elim simp
1.80 +
1.81 +  have "((\<lambda>z. Exp (r * Ln z)) has_field_derivative Exp (r * Ln z) * (inverse z * r)) (at z)"
1.82 +    using assms by (auto intro!: derivative_eq_intros has_field_derivative_powr)
1.83 +  also have "Exp (r * Ln z) * (inverse z * r) = r * z powr (r - 1)"
1.84 +    unfolding powr_def by (simp add: assms exp_diff field_simps)
1.85 +  finally show "((\<lambda>z. Exp (r * Ln z)) has_field_derivative r * z powr (r - 1)) (at z)"
1.86 +    by simp
1.87 +qed
1.88 +
1.89 +declare has_field_derivative_powr_complex'[THEN DERIV_chain2, derivative_intros]
1.90 +
1.91 +
1.92  lemma has_field_derivative_powr_right:
1.93      "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
1.94    apply (simp add: powr_def)
```