# HG changeset patch # User paulson # Date 1530282150 -3600 # Node ID 4d09df93d1a23383b323b59c13e332b7ce35a77f # Parent 914e1bc7369abee4bbe30a6707e406473511e0da The unwinding number is an integer. diff -r 914e1bc7369a -r 4d09df93d1a2 src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Fri Jun 29 14:00:37 2018 +0100 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Fri Jun 29 15:22:30 2018 +0100 @@ -1177,21 +1177,6 @@ obtains w where "w \ 0" "z = w ^ n" by (metis exists_complex_root [of n z] assms power_0_left) -subsection\The Unwinding Number and the Ln-product Formula\ - -text\Note that in this special case the unwinding number is -1, 0 or 1.\ - -definition unwinding :: "complex \ complex" where - "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * \)" - -lemma unwinding_2pi: "(2*pi) * \ * unwinding(z) = z - Ln(exp z)" - by (simp add: unwinding_def) - -lemma Ln_times_unwinding: - "w \ 0 \ z \ 0 \ Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \ * unwinding(Ln w + Ln z)" - using unwinding_2pi by (simp add: exp_add) - - subsection\Derivative of Ln away from the branch cut\ lemma @@ -1465,6 +1450,10 @@ using mpi_less_Im_Ln Im_Ln_le_pi by (force simp: Ln_times) +corollary Ln_times_Reals: + "\r \ Reals; Re r > 0; z \ 0\ \ Ln(r * z) = ln (Re r) + Ln(z)" + using Ln_Reals_eq Ln_times_of_real by fastforce + corollary Ln_divide_of_real: "\r > 0; z \ 0\ \ Ln(z / of_real r) = Ln(z) - ln r" using Ln_times_of_real [of "inverse r" z] @@ -1571,10 +1560,10 @@ subsection\The Argument of a Complex Number\ +text\Finally: it's is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\ + definition Arg :: "complex \ real" where "Arg z \ (if z = 0 then 0 else Im (Ln z))" -text\Finally the Argument is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\ - lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)" by (simp add: Im_Ln_eq_pi Arg_def) @@ -1588,6 +1577,9 @@ using assms exp_Ln exp_eq_polar by (auto simp: Arg_def) +lemma is_Arg_Arg: "z \ 0 \ is_Arg z (Arg z)" + by (simp add: Arg_eq is_Arg_def) + lemma Argument_exists: assumes "z \ 0" and R: "R = {r-pi<..r+pi}" obtains s where "is_Arg z s" "s\R" @@ -1784,6 +1776,47 @@ using continuous_at_Arg continuous_at_imp_continuous_within by blast +subsection\The Unwinding Number and the Ln-product Formula\ + +text\Note that in this special case the unwinding number is -1, 0 or 1. But it's always an integer.\ + +lemma is_Arg_exp_Im: "is_Arg (exp z) (Im z)" + using exp_eq_polar is_Arg_def norm_exp_eq_Re by auto + +lemma is_Arg_exp_diff_2pi: + assumes "is_Arg (exp z) \" + shows "\k. Im z - of_int k * (2 * pi) = \" +proof (intro exI is_Arg_eqI) + let ?k = "\(Im z - \) / (2 * pi)\" + show "is_Arg (exp z) (Im z - real_of_int ?k * (2 * pi))" + by (metis diff_add_cancel is_Arg_2pi_iff is_Arg_exp_Im) + show "\Im z - real_of_int ?k * (2 * pi) - \\ < 2 * pi" + using floor_divide_upper [of "2*pi" "Im z - \"] floor_divide_lower [of "2*pi" "Im z - \"] + by (auto simp: algebra_simps abs_if) +qed (auto simp: is_Arg_exp_Im assms) + +lemma Arg_exp_diff_2pi: "\k. Im z - of_int k * (2 * pi) = Arg (exp z)" + using is_Arg_exp_diff_2pi [OF is_Arg_Arg] by auto + +lemma unwinding_in_Ints: "(z - Ln(exp z)) / (of_real(2*pi) * \) \ \" + using Arg_exp_diff_2pi [of z] + by (force simp: Ints_def image_def field_simps Arg_def intro!: complex_eqI) + +definition unwinding :: "complex \ int" where + "unwinding z \ THE k. of_int k = (z - Ln(exp z)) / (of_real(2*pi) * \)" + +lemma unwinding: "of_int (unwinding z) = (z - Ln(exp z)) / (of_real(2*pi) * \)" + using unwinding_in_Ints [of z] + unfolding unwinding_def Ints_def by force + +lemma unwinding_2pi: "(2*pi) * \ * unwinding(z) = z - Ln(exp z)" + by (simp add: unwinding) + +lemma Ln_times_unwinding: + "w \ 0 \ z \ 0 \ Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \ * unwinding(Ln w + Ln z)" + using unwinding_2pi by (simp add: exp_add) + + subsection\Relation between Ln and Arg2pi, and hence continuity of Arg2pi\ lemma Arg2pi_Ln: