src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
changeset 60020 065ecea354d0
parent 60017 b785d6d06430
child 60141 833adf7db7d8
     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sat Apr 11 16:19:59 2015 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sat Apr 11 22:18:33 2015 +0100
     1.3 @@ -899,15 +899,17 @@
     1.4  
     1.5  subsection{*Complex logarithms (the conventional principal value)*}
     1.6  
     1.7 -definition Ln :: "complex \<Rightarrow> complex"
     1.8 -  where "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
     1.9 +instantiation complex :: ln
    1.10 +begin
    1.11  
    1.12 +definition ln_complex :: "complex \<Rightarrow> complex"
    1.13 +  where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
    1.14  
    1.15  lemma
    1.16    assumes "z \<noteq> 0"
    1.17 -    shows exp_Ln [simp]: "exp(Ln z) = z"
    1.18 -      and mpi_less_Im_Ln: "-pi < Im(Ln z)"
    1.19 -      and Im_Ln_le_pi:    "Im(Ln z) \<le> pi"
    1.20 +    shows exp_Ln [simp]:  "exp(ln z) = z"
    1.21 +      and mpi_less_Im_Ln: "-pi < Im(ln z)"
    1.22 +      and Im_Ln_le_pi:    "Im(ln z) \<le> pi"
    1.23  proof -
    1.24    obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
    1.25      using complex_unimodular_polar [of "z / (norm z)"] assms
    1.26 @@ -915,23 +917,57 @@
    1.27    obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
    1.28      using sincos_principal_value [of "\<psi>"] assms
    1.29      by (auto simp: norm_divide divide_simps)
    1.30 -  have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def
    1.31 +  have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \<le> pi" unfolding ln_complex_def
    1.32      apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
    1.33      using z assms \<phi>
    1.34      apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
    1.35      done
    1.36 -  then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi"
    1.37 +  then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \<le> pi"
    1.38      by auto
    1.39  qed
    1.40  
    1.41  lemma Ln_exp [simp]:
    1.42    assumes "-pi < Im(z)" "Im(z) \<le> pi"
    1.43 -    shows "Ln(exp z) = z"
    1.44 +    shows "ln(exp z) = z"
    1.45    apply (rule exp_complex_eqI)
    1.46    using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
    1.47    apply auto
    1.48    done
    1.49  
    1.50 +subsection{*Relation to Real Logarithm*}
    1.51 +
    1.52 +lemma Ln_of_real:
    1.53 +  assumes "0 < z"
    1.54 +    shows "ln(of_real z::complex) = of_real(ln z)"
    1.55 +proof -
    1.56 +  have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"
    1.57 +    by (simp add: exp_of_real)
    1.58 +  also have "... = of_real(ln z)"
    1.59 +    using assms
    1.60 +    by (subst Ln_exp) auto
    1.61 +  finally show ?thesis
    1.62 +    using assms by simp
    1.63 +qed
    1.64 +
    1.65 +corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
    1.66 +  by (auto simp: Ln_of_real elim: Reals_cases)
    1.67 +
    1.68 +lemma Ln_1: "ln 1 = (0::complex)"
    1.69 +proof -
    1.70 +  have "ln (exp 0) = (0::complex)"
    1.71 +    by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one)
    1.72 +  then show ?thesis
    1.73 +    by simp
    1.74 +qed
    1.75 +
    1.76 +instance
    1.77 +  by intro_classes (rule ln_complex_def Ln_1)
    1.78 +
    1.79 +end
    1.80 +
    1.81 +abbreviation Ln :: "complex \<Rightarrow> complex"
    1.82 +  where "Ln \<equiv> ln"
    1.83 +
    1.84  lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
    1.85    by (metis exp_Ln)
    1.86  
    1.87 @@ -1013,25 +1049,6 @@
    1.88    by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
    1.89  
    1.90  
    1.91 -subsection{*Relation to Real Logarithm*}
    1.92 -
    1.93 -lemma Ln_of_real:
    1.94 -  assumes "0 < z"
    1.95 -    shows "Ln(of_real z) = of_real(ln z)"
    1.96 -proof -
    1.97 -  have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
    1.98 -    by (simp add: exp_of_real)
    1.99 -  also have "... = of_real(ln z)"
   1.100 -    using assms
   1.101 -    by (subst Ln_exp) auto
   1.102 -  finally show ?thesis
   1.103 -    using assms by simp
   1.104 -qed
   1.105 -
   1.106 -corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> Ln z \<in> \<real>"
   1.107 -  by (auto simp: Ln_of_real elim: Reals_cases)
   1.108 -
   1.109 -
   1.110  subsection{*Quadrant-type results for Ln*}
   1.111  
   1.112  lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
   1.113 @@ -1150,26 +1167,6 @@
   1.114                 inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
   1.115    done
   1.116  
   1.117 -lemma Ln_1 [simp]: "Ln 1 = 0"
   1.118 -proof -
   1.119 -  have "Ln (exp 0) = 0"
   1.120 -    by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
   1.121 -  then show ?thesis
   1.122 -    by simp
   1.123 -qed
   1.124 -
   1.125 -instantiation complex :: ln
   1.126 -begin
   1.127 -
   1.128 -definition ln_complex :: "complex \<Rightarrow> complex"
   1.129 -  where "ln_complex \<equiv> Ln"
   1.130 -
   1.131 -instance 
   1.132 -  by intro_classes (simp add: ln_complex_def)
   1.133 -
   1.134 -end
   1.135 -
   1.136 -
   1.137  lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
   1.138    apply (rule exp_complex_eqI)
   1.139    using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
   1.140 @@ -1270,11 +1267,11 @@
   1.141    by (simp add: powr_def)
   1.142  
   1.143  lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
   1.144 -  by (simp add: powr_def ln_complex_def)
   1.145 +  by (simp add: powr_def)
   1.146  
   1.147  lemma powr_nat:
   1.148    fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
   1.149 -  by (simp add: exp_of_nat_mult powr_def ln_complex_def)
   1.150 +  by (simp add: exp_of_nat_mult powr_def)
   1.151  
   1.152  lemma powr_add:
   1.153    fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
   1.154 @@ -1289,45 +1286,45 @@
   1.155    by (simp add: powr_def algebra_simps exp_diff)
   1.156  
   1.157  lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
   1.158 -  apply (simp add: powr_def ln_complex_def)
   1.159 +  apply (simp add: powr_def)
   1.160    using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
   1.161    by auto
   1.162  
   1.163  lemma powr_real_real:
   1.164      "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
   1.165 -  apply (simp add: powr_def ln_complex_def)
   1.166 +  apply (simp add: powr_def)
   1.167    by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
   1.168         exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
   1.169  
   1.170  lemma powr_of_real:
   1.171 -  fixes x::real
   1.172 -  shows "0 < x \<Longrightarrow> x powr y = x powr y"
   1.173 -  by (simp add: powr_def powr_real_real)
   1.174 +  fixes x::real and y::real
   1.175 +  shows "0 < x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
   1.176 +  by (simp add: powr_def) (metis exp_of_real of_real_mult Ln_of_real)
   1.177  
   1.178  lemma norm_powr_real_mono:
   1.179 -    "w \<in> \<real> \<Longrightarrow> 1 < Re w
   1.180 -             \<Longrightarrow> norm(w powr z1) \<le> norm(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
   1.181 -  by (auto simp: powr_def ln_complex_def algebra_simps Reals_def Ln_of_real)
   1.182 +    "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
   1.183 +     \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
   1.184 +  by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
   1.185  
   1.186  lemma powr_times_real:
   1.187      "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
   1.188             \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
   1.189 -  by (auto simp: Reals_def powr_def ln_complex_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
   1.190 +  by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
   1.191  
   1.192  lemma has_field_derivative_powr:
   1.193      "(Im z = 0 \<Longrightarrow> 0 < Re z)
   1.194       \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
   1.195    apply (cases "z=0", auto)
   1.196 -  apply (simp add: powr_def ln_complex_def)
   1.197 +  apply (simp add: powr_def)
   1.198    apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
   1.199 -  apply (auto simp: dist_complex_def ln_complex_def)
   1.200 +  apply (auto simp: dist_complex_def)
   1.201    apply (intro derivative_eq_intros | simp add: assms)+
   1.202    apply (simp add: field_simps exp_diff)
   1.203    done
   1.204  
   1.205  lemma has_field_derivative_powr_right:
   1.206      "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
   1.207 -  apply (simp add: powr_def ln_complex_def)
   1.208 +  apply (simp add: powr_def)
   1.209    apply (intro derivative_eq_intros | simp add: assms)+
   1.210    done
   1.211  
   1.212 @@ -1335,16 +1332,14 @@
   1.213      "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
   1.214  using complex_differentiable_def has_field_derivative_powr_right by blast
   1.215  
   1.216 -
   1.217  lemma holomorphic_on_powr_right:
   1.218      "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
   1.219      unfolding holomorphic_on_def
   1.220      using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
   1.221  
   1.222 -
   1.223  lemma norm_powr_real_powr:
   1.224    "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
   1.225 -  by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm ln_complex_def)
   1.226 +  by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm)
   1.227  
   1.228  lemma cmod_Ln_Reals [simp]:"z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (Ln z) = norm (ln (Re z))"
   1.229    using Ln_of_real by force
   1.230 @@ -2406,4 +2401,94 @@
   1.231  qed
   1.232  
   1.233  
   1.234 +subsection{*Roots of unity*}
   1.235 +
   1.236 +lemma complex_root_unity:
   1.237 +  fixes j::nat
   1.238 +  assumes "n \<noteq> 0"
   1.239 +    shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
   1.240 +proof -
   1.241 +  have *: "of_nat j * (complex_of_real pi * 2) = complex_of_real (2 * real j * pi)"
   1.242 +    by (simp add: of_real_numeral)
   1.243 +  then show ?thesis
   1.244 +    apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler)
   1.245 +    apply (simp only: * cos_of_real sin_of_real)
   1.246 +    apply (simp add: )
   1.247 +    done
   1.248 +qed
   1.249 +
   1.250 +lemma complex_root_unity_eq:
   1.251 +  fixes j::nat and k::nat
   1.252 +  assumes "1 \<le> n"
   1.253 +    shows "(exp(2 * of_real pi * \<i> * of_nat j / of_nat n) = exp(2 * of_real pi * \<i> * of_nat k / of_nat n)
   1.254 +           \<longleftrightarrow> j mod n = k mod n)"
   1.255 +proof -
   1.256 +    have "(\<exists>z::int. \<i> * (of_nat j * (of_real pi * 2)) =
   1.257 +               \<i> * (of_nat k * (of_real pi * 2)) + \<i> * (of_int z * (of_nat n * (of_real pi * 2)))) \<longleftrightarrow>
   1.258 +          (\<exists>z::int. of_nat j * (\<i> * (of_real pi * 2)) =
   1.259 +              (of_nat k + of_nat n * of_int z) * (\<i> * (of_real pi * 2)))"
   1.260 +      by (simp add: algebra_simps)
   1.261 +    also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))"
   1.262 +      by simp
   1.263 +    also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * z)"
   1.264 +      apply (rule HOL.iff_exI)
   1.265 +      apply (auto simp: )
   1.266 +      using of_int_eq_iff apply fastforce
   1.267 +      by (metis of_int_add of_int_mult of_int_of_nat_eq)
   1.268 +    also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
   1.269 +      by (auto simp: zmod_eq_dvd_iff dvd_def algebra_simps)
   1.270 +    also have "... \<longleftrightarrow> j mod n = k mod n"
   1.271 +      by (metis of_nat_eq_iff zmod_int)
   1.272 +    finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =
   1.273 +             \<i> * (of_nat k * (of_real pi * 2)) + \<i> * (of_int z * (of_nat n * (of_real pi * 2)))) \<longleftrightarrow> j mod n = k mod n" .
   1.274 +   note * = this
   1.275 +  show ?thesis
   1.276 +    using assms
   1.277 +    by (simp add: exp_eq divide_simps mult_ac of_real_numeral *)
   1.278 +qed
   1.279 +
   1.280 +corollary bij_betw_roots_unity:
   1.281 +    "bij_betw (\<lambda>j. exp(2 * of_real pi * \<i> * of_nat j / of_nat n))
   1.282 +              {..<n}  {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j. j < n}"
   1.283 +  by (auto simp: bij_betw_def inj_on_def complex_root_unity_eq)
   1.284 +
   1.285 +lemma complex_root_unity_eq_1:
   1.286 +  fixes j::nat and k::nat
   1.287 +  assumes "1 \<le> n"
   1.288 +    shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n) = 1 \<longleftrightarrow> n dvd j"
   1.289 +proof -
   1.290 +  have "1 = exp(2 * of_real pi * \<i> * (of_nat n / of_nat n))"
   1.291 +    using assms by simp
   1.292 +  then have "exp(2 * of_real pi * \<i> * (of_nat j / of_nat n)) = 1 \<longleftrightarrow> j mod n = n mod n"
   1.293 +     using complex_root_unity_eq [of n j n] assms
   1.294 +     by simp
   1.295 +  then show ?thesis
   1.296 +    by auto
   1.297 +qed
   1.298 +
   1.299 +lemma finite_complex_roots_unity_explicit:
   1.300 +     "finite {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
   1.301 +by simp
   1.302 +
   1.303 +lemma card_complex_roots_unity_explicit:
   1.304 +     "card {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n} = n"
   1.305 +  by (simp add:  Finite_Set.bij_betw_same_card [OF bij_betw_roots_unity, symmetric])
   1.306 +
   1.307 +lemma complex_roots_unity:
   1.308 +  assumes "1 \<le> n"
   1.309 +    shows "{z::complex. z^n = 1} = {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
   1.310 +  apply (rule Finite_Set.card_seteq [symmetric])
   1.311 +  using assms
   1.312 +  apply (auto simp: card_complex_roots_unity_explicit finite_roots_unity complex_root_unity card_roots_unity)
   1.313 +  done
   1.314 +
   1.315 +lemma card_complex_roots_unity: "1 \<le> n \<Longrightarrow> card {z::complex. z^n = 1} = n"
   1.316 +  by (simp add: card_complex_roots_unity_explicit complex_roots_unity)
   1.317 +
   1.318 +lemma complex_not_root_unity:
   1.319 +    "1 \<le> n \<Longrightarrow> \<exists>u::complex. norm u = 1 \<and> u^n \<noteq> 1"
   1.320 +  apply (rule_tac x="exp (of_real pi * \<i> * of_real (1 / n))" in exI)
   1.321 +  apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
   1.322 +  done
   1.323 +
   1.324  end