--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Sat Apr 11 16:19:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Sat Apr 11 22:18:33 2015 +0100
@@ -899,15 +899,17 @@
subsection{*Complex logarithms (the conventional principal value)*}
-definition Ln :: "complex \<Rightarrow> complex"
- where "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
+instantiation complex :: ln
+begin
+definition ln_complex :: "complex \<Rightarrow> complex"
+ where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
lemma
assumes "z \<noteq> 0"
- shows exp_Ln [simp]: "exp(Ln z) = z"
- and mpi_less_Im_Ln: "-pi < Im(Ln z)"
- and Im_Ln_le_pi: "Im(Ln z) \<le> pi"
+ shows exp_Ln [simp]: "exp(ln z) = z"
+ and mpi_less_Im_Ln: "-pi < Im(ln z)"
+ and Im_Ln_le_pi: "Im(ln z) \<le> pi"
proof -
obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
using complex_unimodular_polar [of "z / (norm z)"] assms
@@ -915,23 +917,57 @@
obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
using sincos_principal_value [of "\<psi>"] assms
by (auto simp: norm_divide divide_simps)
- have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def
+ have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \<le> pi" unfolding ln_complex_def
apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
using z assms \<phi>
apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
done
- then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi"
+ then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \<le> pi"
by auto
qed
lemma Ln_exp [simp]:
assumes "-pi < Im(z)" "Im(z) \<le> pi"
- shows "Ln(exp z) = z"
+ shows "ln(exp z) = z"
apply (rule exp_complex_eqI)
using assms mpi_less_Im_Ln [of "exp z"] Im_Ln_le_pi [of "exp z"]
apply auto
done
+subsection{*Relation to Real Logarithm*}
+
+lemma Ln_of_real:
+ assumes "0 < z"
+ shows "ln(of_real z::complex) = of_real(ln z)"
+proof -
+ have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"
+ by (simp add: exp_of_real)
+ also have "... = of_real(ln z)"
+ using assms
+ by (subst Ln_exp) auto
+ finally show ?thesis
+ using assms by simp
+qed
+
+corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
+ by (auto simp: Ln_of_real elim: Reals_cases)
+
+lemma Ln_1: "ln 1 = (0::complex)"
+proof -
+ have "ln (exp 0) = (0::complex)"
+ by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one)
+ then show ?thesis
+ by simp
+qed
+
+instance
+ by intro_classes (rule ln_complex_def Ln_1)
+
+end
+
+abbreviation Ln :: "complex \<Rightarrow> complex"
+ where "Ln \<equiv> ln"
+
lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
by (metis exp_Ln)
@@ -1013,25 +1049,6 @@
by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
-subsection{*Relation to Real Logarithm*}
-
-lemma Ln_of_real:
- assumes "0 < z"
- shows "Ln(of_real z) = of_real(ln z)"
-proof -
- have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
- by (simp add: exp_of_real)
- also have "... = of_real(ln z)"
- using assms
- by (subst Ln_exp) auto
- finally show ?thesis
- using assms by simp
-qed
-
-corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> Ln z \<in> \<real>"
- by (auto simp: Ln_of_real elim: Reals_cases)
-
-
subsection{*Quadrant-type results for Ln*}
lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
@@ -1150,26 +1167,6 @@
inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
done
-lemma Ln_1 [simp]: "Ln 1 = 0"
-proof -
- have "Ln (exp 0) = 0"
- by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
- then show ?thesis
- by simp
-qed
-
-instantiation complex :: ln
-begin
-
-definition ln_complex :: "complex \<Rightarrow> complex"
- where "ln_complex \<equiv> Ln"
-
-instance
- by intro_classes (simp add: ln_complex_def)
-
-end
-
-
lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
apply (rule exp_complex_eqI)
using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
@@ -1270,11 +1267,11 @@
by (simp add: powr_def)
lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
- by (simp add: powr_def ln_complex_def)
+ by (simp add: powr_def)
lemma powr_nat:
fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
- by (simp add: exp_of_nat_mult powr_def ln_complex_def)
+ by (simp add: exp_of_nat_mult powr_def)
lemma powr_add:
fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
@@ -1289,45 +1286,45 @@
by (simp add: powr_def algebra_simps exp_diff)
lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
- apply (simp add: powr_def ln_complex_def)
+ apply (simp add: powr_def)
using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
by auto
lemma powr_real_real:
"\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
- apply (simp add: powr_def ln_complex_def)
+ apply (simp add: powr_def)
by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
lemma powr_of_real:
- fixes x::real
- shows "0 < x \<Longrightarrow> x powr y = x powr y"
- by (simp add: powr_def powr_real_real)
+ fixes x::real and y::real
+ shows "0 < x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
+ by (simp add: powr_def) (metis exp_of_real of_real_mult Ln_of_real)
lemma norm_powr_real_mono:
- "w \<in> \<real> \<Longrightarrow> 1 < Re w
- \<Longrightarrow> norm(w powr z1) \<le> norm(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
- by (auto simp: powr_def ln_complex_def algebra_simps Reals_def Ln_of_real)
+ "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
+ \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
+ by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
lemma powr_times_real:
"\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
\<Longrightarrow> (x * y) powr z = x powr z * y powr z"
- by (auto simp: Reals_def powr_def ln_complex_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
+ by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
lemma has_field_derivative_powr:
"(Im z = 0 \<Longrightarrow> 0 < Re z)
\<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
apply (cases "z=0", auto)
- apply (simp add: powr_def ln_complex_def)
+ apply (simp add: powr_def)
apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
- apply (auto simp: dist_complex_def ln_complex_def)
+ apply (auto simp: dist_complex_def)
apply (intro derivative_eq_intros | simp add: assms)+
apply (simp add: field_simps exp_diff)
done
lemma has_field_derivative_powr_right:
"w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
- apply (simp add: powr_def ln_complex_def)
+ apply (simp add: powr_def)
apply (intro derivative_eq_intros | simp add: assms)+
done
@@ -1335,16 +1332,14 @@
"w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
using complex_differentiable_def has_field_derivative_powr_right by blast
-
lemma holomorphic_on_powr_right:
"f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
unfolding holomorphic_on_def
using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
-
lemma norm_powr_real_powr:
"w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
- by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm ln_complex_def)
+ by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm)
lemma cmod_Ln_Reals [simp]:"z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (Ln z) = norm (ln (Re z))"
using Ln_of_real by force
@@ -2406,4 +2401,94 @@
qed
+subsection{*Roots of unity*}
+
+lemma complex_root_unity:
+ fixes j::nat
+ assumes "n \<noteq> 0"
+ shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
+proof -
+ have *: "of_nat j * (complex_of_real pi * 2) = complex_of_real (2 * real j * pi)"
+ by (simp add: of_real_numeral)
+ then show ?thesis
+ apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler)
+ apply (simp only: * cos_of_real sin_of_real)
+ apply (simp add: )
+ done
+qed
+
+lemma complex_root_unity_eq:
+ fixes j::nat and k::nat
+ assumes "1 \<le> n"
+ 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)
+ \<longleftrightarrow> j mod n = k mod n)"
+proof -
+ have "(\<exists>z::int. \<i> * (of_nat j * (of_real pi * 2)) =
+ \<i> * (of_nat k * (of_real pi * 2)) + \<i> * (of_int z * (of_nat n * (of_real pi * 2)))) \<longleftrightarrow>
+ (\<exists>z::int. of_nat j * (\<i> * (of_real pi * 2)) =
+ (of_nat k + of_nat n * of_int z) * (\<i> * (of_real pi * 2)))"
+ by (simp add: algebra_simps)
+ also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))"
+ by simp
+ also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * z)"
+ apply (rule HOL.iff_exI)
+ apply (auto simp: )
+ using of_int_eq_iff apply fastforce
+ by (metis of_int_add of_int_mult of_int_of_nat_eq)
+ also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
+ by (auto simp: zmod_eq_dvd_iff dvd_def algebra_simps)
+ also have "... \<longleftrightarrow> j mod n = k mod n"
+ by (metis of_nat_eq_iff zmod_int)
+ finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =
+ \<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" .
+ note * = this
+ show ?thesis
+ using assms
+ by (simp add: exp_eq divide_simps mult_ac of_real_numeral *)
+qed
+
+corollary bij_betw_roots_unity:
+ "bij_betw (\<lambda>j. exp(2 * of_real pi * \<i> * of_nat j / of_nat n))
+ {..<n} {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j. j < n}"
+ by (auto simp: bij_betw_def inj_on_def complex_root_unity_eq)
+
+lemma complex_root_unity_eq_1:
+ fixes j::nat and k::nat
+ assumes "1 \<le> n"
+ shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n) = 1 \<longleftrightarrow> n dvd j"
+proof -
+ have "1 = exp(2 * of_real pi * \<i> * (of_nat n / of_nat n))"
+ using assms by simp
+ then have "exp(2 * of_real pi * \<i> * (of_nat j / of_nat n)) = 1 \<longleftrightarrow> j mod n = n mod n"
+ using complex_root_unity_eq [of n j n] assms
+ by simp
+ then show ?thesis
+ by auto
+qed
+
+lemma finite_complex_roots_unity_explicit:
+ "finite {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
+by simp
+
+lemma card_complex_roots_unity_explicit:
+ "card {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n} = n"
+ by (simp add: Finite_Set.bij_betw_same_card [OF bij_betw_roots_unity, symmetric])
+
+lemma complex_roots_unity:
+ assumes "1 \<le> n"
+ shows "{z::complex. z^n = 1} = {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
+ apply (rule Finite_Set.card_seteq [symmetric])
+ using assms
+ apply (auto simp: card_complex_roots_unity_explicit finite_roots_unity complex_root_unity card_roots_unity)
+ done
+
+lemma card_complex_roots_unity: "1 \<le> n \<Longrightarrow> card {z::complex. z^n = 1} = n"
+ by (simp add: card_complex_roots_unity_explicit complex_roots_unity)
+
+lemma complex_not_root_unity:
+ "1 \<le> n \<Longrightarrow> \<exists>u::complex. norm u = 1 \<and> u^n \<noteq> 1"
+ apply (rule_tac x="exp (of_real pi * \<i> * of_real (1 / n))" in exI)
+ apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
+ done
+
end