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.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.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.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
```