Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
authorpaulson <lp15@cam.ac.uk>
Sat Apr 11 22:18:33 2015 +0100 (2015-04-11)
changeset 60020065ecea354d0
parent 60019 4dda564e8a5d
child 60021 69e7fe18b7db
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
NEWS
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Sat Apr 11 16:19:59 2015 +0100
     1.2 +++ b/NEWS	Sat Apr 11 22:18:33 2015 +0100
     1.3 @@ -261,6 +261,10 @@
     1.4  * Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit
     1.5  additive inverse operation. INCOMPATIBILITY.
     1.6  
     1.7 +* Complex powers and square roots. The functions "ln" and "powr" are now
     1.8 +  overloaded for types real and complex, and 0 powr y = 0 by definition.
     1.9 +  INCOMPATIBILITY: type constraints may be necessary.
    1.10 +
    1.11  * The functions "sin" and "cos" are now defined for any type of sort
    1.12  "{real_normed_algebra_1,banach}" type, so in particular on "real" and
    1.13  "complex" uniformly. Minor INCOMPATIBILITY: type constraints may be
     2.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sat Apr 11 16:19:59 2015 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sat Apr 11 22:18:33 2015 +0100
     2.3 @@ -899,15 +899,17 @@
     2.4  
     2.5  subsection{*Complex logarithms (the conventional principal value)*}
     2.6  
     2.7 -definition Ln :: "complex \<Rightarrow> complex"
     2.8 -  where "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
     2.9 +instantiation complex :: ln
    2.10 +begin
    2.11  
    2.12 +definition ln_complex :: "complex \<Rightarrow> complex"
    2.13 +  where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
    2.14  
    2.15  lemma
    2.16    assumes "z \<noteq> 0"
    2.17 -    shows exp_Ln [simp]: "exp(Ln z) = z"
    2.18 -      and mpi_less_Im_Ln: "-pi < Im(Ln z)"
    2.19 -      and Im_Ln_le_pi:    "Im(Ln z) \<le> pi"
    2.20 +    shows exp_Ln [simp]:  "exp(ln z) = z"
    2.21 +      and mpi_less_Im_Ln: "-pi < Im(ln z)"
    2.22 +      and Im_Ln_le_pi:    "Im(ln z) \<le> pi"
    2.23  proof -
    2.24    obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
    2.25      using complex_unimodular_polar [of "z / (norm z)"] assms
    2.26 @@ -915,23 +917,57 @@
    2.27    obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
    2.28      using sincos_principal_value [of "\<psi>"] assms
    2.29      by (auto simp: norm_divide divide_simps)
    2.30 -  have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def
    2.31 +  have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \<le> pi" unfolding ln_complex_def
    2.32      apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
    2.33      using z assms \<phi>
    2.34      apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
    2.35      done
    2.36 -  then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi"
    2.37 +  then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \<le> pi"
    2.38      by auto
    2.39  qed
    2.40  
    2.41  lemma Ln_exp [simp]:
    2.42    assumes "-pi < Im(z)" "Im(z) \<le> pi"
    2.43 -    shows "Ln(exp z) = z"
    2.44 +    shows "ln(exp z) = z"
    2.45    apply (rule exp_complex_eqI)
    2.46    using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
    2.47    apply auto
    2.48    done
    2.49  
    2.50 +subsection{*Relation to Real Logarithm*}
    2.51 +
    2.52 +lemma Ln_of_real:
    2.53 +  assumes "0 < z"
    2.54 +    shows "ln(of_real z::complex) = of_real(ln z)"
    2.55 +proof -
    2.56 +  have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"
    2.57 +    by (simp add: exp_of_real)
    2.58 +  also have "... = of_real(ln z)"
    2.59 +    using assms
    2.60 +    by (subst Ln_exp) auto
    2.61 +  finally show ?thesis
    2.62 +    using assms by simp
    2.63 +qed
    2.64 +
    2.65 +corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
    2.66 +  by (auto simp: Ln_of_real elim: Reals_cases)
    2.67 +
    2.68 +lemma Ln_1: "ln 1 = (0::complex)"
    2.69 +proof -
    2.70 +  have "ln (exp 0) = (0::complex)"
    2.71 +    by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one)
    2.72 +  then show ?thesis
    2.73 +    by simp
    2.74 +qed
    2.75 +
    2.76 +instance
    2.77 +  by intro_classes (rule ln_complex_def Ln_1)
    2.78 +
    2.79 +end
    2.80 +
    2.81 +abbreviation Ln :: "complex \<Rightarrow> complex"
    2.82 +  where "Ln \<equiv> ln"
    2.83 +
    2.84  lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
    2.85    by (metis exp_Ln)
    2.86  
    2.87 @@ -1013,25 +1049,6 @@
    2.88    by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
    2.89  
    2.90  
    2.91 -subsection{*Relation to Real Logarithm*}
    2.92 -
    2.93 -lemma Ln_of_real:
    2.94 -  assumes "0 < z"
    2.95 -    shows "Ln(of_real z) = of_real(ln z)"
    2.96 -proof -
    2.97 -  have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
    2.98 -    by (simp add: exp_of_real)
    2.99 -  also have "... = of_real(ln z)"
   2.100 -    using assms
   2.101 -    by (subst Ln_exp) auto
   2.102 -  finally show ?thesis
   2.103 -    using assms by simp
   2.104 -qed
   2.105 -
   2.106 -corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> Ln z \<in> \<real>"
   2.107 -  by (auto simp: Ln_of_real elim: Reals_cases)
   2.108 -
   2.109 -
   2.110  subsection{*Quadrant-type results for Ln*}
   2.111  
   2.112  lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
   2.113 @@ -1150,26 +1167,6 @@
   2.114                 inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
   2.115    done
   2.116  
   2.117 -lemma Ln_1 [simp]: "Ln 1 = 0"
   2.118 -proof -
   2.119 -  have "Ln (exp 0) = 0"
   2.120 -    by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
   2.121 -  then show ?thesis
   2.122 -    by simp
   2.123 -qed
   2.124 -
   2.125 -instantiation complex :: ln
   2.126 -begin
   2.127 -
   2.128 -definition ln_complex :: "complex \<Rightarrow> complex"
   2.129 -  where "ln_complex \<equiv> Ln"
   2.130 -
   2.131 -instance 
   2.132 -  by intro_classes (simp add: ln_complex_def)
   2.133 -
   2.134 -end
   2.135 -
   2.136 -
   2.137  lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
   2.138    apply (rule exp_complex_eqI)
   2.139    using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
   2.140 @@ -1270,11 +1267,11 @@
   2.141    by (simp add: powr_def)
   2.142  
   2.143  lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
   2.144 -  by (simp add: powr_def ln_complex_def)
   2.145 +  by (simp add: powr_def)
   2.146  
   2.147  lemma powr_nat:
   2.148    fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
   2.149 -  by (simp add: exp_of_nat_mult powr_def ln_complex_def)
   2.150 +  by (simp add: exp_of_nat_mult powr_def)
   2.151  
   2.152  lemma powr_add:
   2.153    fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
   2.154 @@ -1289,45 +1286,45 @@
   2.155    by (simp add: powr_def algebra_simps exp_diff)
   2.156  
   2.157  lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
   2.158 -  apply (simp add: powr_def ln_complex_def)
   2.159 +  apply (simp add: powr_def)
   2.160    using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
   2.161    by auto
   2.162  
   2.163  lemma powr_real_real:
   2.164      "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
   2.165 -  apply (simp add: powr_def ln_complex_def)
   2.166 +  apply (simp add: powr_def)
   2.167    by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
   2.168         exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
   2.169  
   2.170  lemma powr_of_real:
   2.171 -  fixes x::real
   2.172 -  shows "0 < x \<Longrightarrow> x powr y = x powr y"
   2.173 -  by (simp add: powr_def powr_real_real)
   2.174 +  fixes x::real and y::real
   2.175 +  shows "0 < x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
   2.176 +  by (simp add: powr_def) (metis exp_of_real of_real_mult Ln_of_real)
   2.177  
   2.178  lemma norm_powr_real_mono:
   2.179 -    "w \<in> \<real> \<Longrightarrow> 1 < Re w
   2.180 -             \<Longrightarrow> norm(w powr z1) \<le> norm(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
   2.181 -  by (auto simp: powr_def ln_complex_def algebra_simps Reals_def Ln_of_real)
   2.182 +    "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
   2.183 +     \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
   2.184 +  by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
   2.185  
   2.186  lemma powr_times_real:
   2.187      "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
   2.188             \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
   2.189 -  by (auto simp: Reals_def powr_def ln_complex_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
   2.190 +  by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
   2.191  
   2.192  lemma has_field_derivative_powr:
   2.193      "(Im z = 0 \<Longrightarrow> 0 < Re z)
   2.194       \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
   2.195    apply (cases "z=0", auto)
   2.196 -  apply (simp add: powr_def ln_complex_def)
   2.197 +  apply (simp add: powr_def)
   2.198    apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
   2.199 -  apply (auto simp: dist_complex_def ln_complex_def)
   2.200 +  apply (auto simp: dist_complex_def)
   2.201    apply (intro derivative_eq_intros | simp add: assms)+
   2.202    apply (simp add: field_simps exp_diff)
   2.203    done
   2.204  
   2.205  lemma has_field_derivative_powr_right:
   2.206      "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
   2.207 -  apply (simp add: powr_def ln_complex_def)
   2.208 +  apply (simp add: powr_def)
   2.209    apply (intro derivative_eq_intros | simp add: assms)+
   2.210    done
   2.211  
   2.212 @@ -1335,16 +1332,14 @@
   2.213      "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
   2.214  using complex_differentiable_def has_field_derivative_powr_right by blast
   2.215  
   2.216 -
   2.217  lemma holomorphic_on_powr_right:
   2.218      "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
   2.219      unfolding holomorphic_on_def
   2.220      using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
   2.221  
   2.222 -
   2.223  lemma norm_powr_real_powr:
   2.224    "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
   2.225 -  by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm ln_complex_def)
   2.226 +  by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm)
   2.227  
   2.228  lemma cmod_Ln_Reals [simp]:"z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (Ln z) = norm (ln (Re z))"
   2.229    using Ln_of_real by force
   2.230 @@ -2406,4 +2401,94 @@
   2.231  qed
   2.232  
   2.233  
   2.234 +subsection{*Roots of unity*}
   2.235 +
   2.236 +lemma complex_root_unity:
   2.237 +  fixes j::nat
   2.238 +  assumes "n \<noteq> 0"
   2.239 +    shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
   2.240 +proof -
   2.241 +  have *: "of_nat j * (complex_of_real pi * 2) = complex_of_real (2 * real j * pi)"
   2.242 +    by (simp add: of_real_numeral)
   2.243 +  then show ?thesis
   2.244 +    apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler)
   2.245 +    apply (simp only: * cos_of_real sin_of_real)
   2.246 +    apply (simp add: )
   2.247 +    done
   2.248 +qed
   2.249 +
   2.250 +lemma complex_root_unity_eq:
   2.251 +  fixes j::nat and k::nat
   2.252 +  assumes "1 \<le> n"
   2.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)
   2.254 +           \<longleftrightarrow> j mod n = k mod n)"
   2.255 +proof -
   2.256 +    have "(\<exists>z::int. \<i> * (of_nat j * (of_real pi * 2)) =
   2.257 +               \<i> * (of_nat k * (of_real pi * 2)) + \<i> * (of_int z * (of_nat n * (of_real pi * 2)))) \<longleftrightarrow>
   2.258 +          (\<exists>z::int. of_nat j * (\<i> * (of_real pi * 2)) =
   2.259 +              (of_nat k + of_nat n * of_int z) * (\<i> * (of_real pi * 2)))"
   2.260 +      by (simp add: algebra_simps)
   2.261 +    also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))"
   2.262 +      by simp
   2.263 +    also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * z)"
   2.264 +      apply (rule HOL.iff_exI)
   2.265 +      apply (auto simp: )
   2.266 +      using of_int_eq_iff apply fastforce
   2.267 +      by (metis of_int_add of_int_mult of_int_of_nat_eq)
   2.268 +    also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
   2.269 +      by (auto simp: zmod_eq_dvd_iff dvd_def algebra_simps)
   2.270 +    also have "... \<longleftrightarrow> j mod n = k mod n"
   2.271 +      by (metis of_nat_eq_iff zmod_int)
   2.272 +    finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =
   2.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" .
   2.274 +   note * = this
   2.275 +  show ?thesis
   2.276 +    using assms
   2.277 +    by (simp add: exp_eq divide_simps mult_ac of_real_numeral *)
   2.278 +qed
   2.279 +
   2.280 +corollary bij_betw_roots_unity:
   2.281 +    "bij_betw (\<lambda>j. exp(2 * of_real pi * \<i> * of_nat j / of_nat n))
   2.282 +              {..<n}  {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j. j < n}"
   2.283 +  by (auto simp: bij_betw_def inj_on_def complex_root_unity_eq)
   2.284 +
   2.285 +lemma complex_root_unity_eq_1:
   2.286 +  fixes j::nat and k::nat
   2.287 +  assumes "1 \<le> n"
   2.288 +    shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n) = 1 \<longleftrightarrow> n dvd j"
   2.289 +proof -
   2.290 +  have "1 = exp(2 * of_real pi * \<i> * (of_nat n / of_nat n))"
   2.291 +    using assms by simp
   2.292 +  then have "exp(2 * of_real pi * \<i> * (of_nat j / of_nat n)) = 1 \<longleftrightarrow> j mod n = n mod n"
   2.293 +     using complex_root_unity_eq [of n j n] assms
   2.294 +     by simp
   2.295 +  then show ?thesis
   2.296 +    by auto
   2.297 +qed
   2.298 +
   2.299 +lemma finite_complex_roots_unity_explicit:
   2.300 +     "finite {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
   2.301 +by simp
   2.302 +
   2.303 +lemma card_complex_roots_unity_explicit:
   2.304 +     "card {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n} = n"
   2.305 +  by (simp add:  Finite_Set.bij_betw_same_card [OF bij_betw_roots_unity, symmetric])
   2.306 +
   2.307 +lemma complex_roots_unity:
   2.308 +  assumes "1 \<le> n"
   2.309 +    shows "{z::complex. z^n = 1} = {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
   2.310 +  apply (rule Finite_Set.card_seteq [symmetric])
   2.311 +  using assms
   2.312 +  apply (auto simp: card_complex_roots_unity_explicit finite_roots_unity complex_root_unity card_roots_unity)
   2.313 +  done
   2.314 +
   2.315 +lemma card_complex_roots_unity: "1 \<le> n \<Longrightarrow> card {z::complex. z^n = 1} = n"
   2.316 +  by (simp add: card_complex_roots_unity_explicit complex_roots_unity)
   2.317 +
   2.318 +lemma complex_not_root_unity:
   2.319 +    "1 \<le> n \<Longrightarrow> \<exists>u::complex. norm u = 1 \<and> u^n \<noteq> 1"
   2.320 +  apply (rule_tac x="exp (of_real pi * \<i> * of_real (1 / n))" in exI)
   2.321 +  apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
   2.322 +  done
   2.323 +
   2.324  end
     3.1 --- a/src/HOL/Transcendental.thy	Sat Apr 11 16:19:59 2015 +0100
     3.2 +++ b/src/HOL/Transcendental.thy	Sat Apr 11 22:18:33 2015 +0100
     3.3 @@ -1291,7 +1291,7 @@
     3.4  
     3.5  definition powr :: "['a,'a] => 'a::ln"     (infixr "powr" 80)
     3.6    -- {*exponentation via ln and exp*}
     3.7 -  where "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)"
     3.8 +  where  [code del]: "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)"
     3.9  
    3.10  
    3.11  instantiation real :: ln