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)