src/HOL/Analysis/Complex_Transcendental.thy
changeset 65583 8d53b3bebab4
parent 65578 e4997c181cce
child 65585 a043de9ad41e
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Apr 25 21:31:28 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 26 15:53:35 2017 +0100
     1.3 @@ -1046,6 +1046,9 @@
     1.4    apply auto
     1.5    done
     1.6  
     1.7 +lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln x = 0 \<longleftrightarrow> x = 1"
     1.8 +  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
     1.9 +
    1.10  subsection\<open>Relation to Real Logarithm\<close>
    1.11  
    1.12  lemma Ln_of_real:
    1.13 @@ -1679,23 +1682,19 @@
    1.14    fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
    1.15    by (simp add: exp_of_nat_mult powr_def)
    1.16  
    1.17 -lemma powr_add_complex:
    1.18 -  fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
    1.19 -  by (simp add: powr_def algebra_simps exp_add)
    1.20 -
    1.21 -lemma powr_minus_complex:
    1.22 -  fixes w::complex shows  "w powr (-z) = inverse(w powr z)"
    1.23 -  by (simp add: powr_def exp_minus)
    1.24 -
    1.25 -lemma powr_diff_complex:
    1.26 -  fixes w::complex shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
    1.27 -  by (simp add: powr_def algebra_simps exp_diff)
    1.28 -
    1.29  lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
    1.30    apply (simp add: powr_def)
    1.31    using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
    1.32    by auto
    1.33  
    1.34 +lemma powr_complexpow [simp]:
    1.35 +  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (of_nat n) = x^n"
    1.36 +  by (induct n) (auto simp: ac_simps powr_add)
    1.37 +
    1.38 +lemma powr_complexnumeral [simp]:
    1.39 +  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (numeral n) = x ^ (numeral n)"
    1.40 +  by (metis of_nat_numeral powr_complexpow)
    1.41 +
    1.42  lemma cnj_powr:
    1.43    assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"
    1.44    shows   "cnj (a powr b) = cnj a powr cnj b"
    1.45 @@ -1759,16 +1758,15 @@
    1.46    apply (intro derivative_eq_intros | simp)+
    1.47    done
    1.48  
    1.49 -lemma field_differentiable_powr_right:
    1.50 +lemma field_differentiable_powr_right [derivative_intros]:
    1.51    fixes w::complex
    1.52 -  shows
    1.53 -    "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
    1.54 +  shows "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
    1.55  using field_differentiable_def has_field_derivative_powr_right by blast
    1.56  
    1.57 -lemma holomorphic_on_powr_right:
    1.58 +lemma holomorphic_on_powr_right [holomorphic_intros]:
    1.59      "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
    1.60 -    unfolding holomorphic_on_def field_differentiable_def
    1.61 -by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
    1.62 +  unfolding holomorphic_on_def field_differentiable_def
    1.63 +  by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
    1.64  
    1.65  lemma norm_powr_real_powr:
    1.66    "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
    1.67 @@ -2562,6 +2560,9 @@
    1.68    using arctan_bounds[of "1/5"   4]
    1.69          arctan_bounds[of "1/239" 4]
    1.70    by (simp_all add: eval_nat_numeral)
    1.71 +    
    1.72 +corollary pi_gt3: "pi > 3"
    1.73 +  using pi_approx by simp
    1.74  
    1.75  
    1.76  subsection\<open>Inverse Sine\<close>