src/HOL/Analysis/Complex_Transcendental.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69508 2a4c8a2a3f8e child 69566 c41954ee87cf permissions -rw-r--r--
capitalize proper names in lemma names
 wenzelm@60420  1 section \Complex Transcendental Functions\  lp15@59745  2 lp15@61711  3 text\By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\  lp15@61711  4 lp15@59745  5 theory Complex_Transcendental  lp15@62534  6 imports  eberlm@62049  7  Complex_Analysis_Basics  hoelzl@63594  8  Summation_Tests  wenzelm@66453  9  "HOL-Library.Periodic_Fun"  lp15@59745  10 begin  lp15@59745  11 eberlm@69180  12 subsection\Möbius transformations\  eberlm@69180  13 eberlm@62049  14 (* TODO: Figure out what to do with Möbius transformations *)  eberlm@69180  15 definition%important "moebius a b c d = (\z. (a*z+b) / (c*z+d :: 'a :: field))"  eberlm@69180  16 eberlm@69180  17 theorem moebius_inverse:  eberlm@62049  18  assumes "a * d \ b * c" "c * z + d \ 0"  eberlm@62049  19  shows "moebius d (-b) (-c) a (moebius a b c d z) = z"  eberlm@62049  20 proof -  eberlm@62049  21  from assms have "(-c) * moebius a b c d z + a \ 0" unfolding moebius_def  eberlm@62049  22  by (simp add: field_simps)  eberlm@62049  23  with assms show ?thesis  eberlm@62049  24  unfolding moebius_def by (simp add: moebius_def divide_simps) (simp add: algebra_simps)?  eberlm@62049  25 qed  eberlm@62049  26 lp15@62534  27 lemma moebius_inverse':  eberlm@62049  28  assumes "a * d \ b * c" "c * z - a \ 0"  eberlm@62049  29  shows "moebius a b c d (moebius d (-b) (-c) a z) = z"  eberlm@62049  30  using assms moebius_inverse[of d a "-b" "-c" z]  eberlm@62049  31  by (auto simp: algebra_simps)  eberlm@62049  32 lp15@59870  33 lemma cmod_add_real_less:  lp15@59870  34  assumes "Im z \ 0" "r\0"  wenzelm@61945  35  shows "cmod (z + r) < cmod z + \r\"  lp15@59870  36 proof (cases z)  lp15@59870  37  case (Complex x y)  lp15@59870  38  have "r * x / \r\ < sqrt (x*x + y*y)"  lp15@59870  39  apply (rule real_less_rsqrt)  lp15@59870  40  using assms  lp15@59870  41  apply (simp add: Complex power2_eq_square)  lp15@59870  42  using not_real_square_gt_zero by blast  lp15@59870  43  then show ?thesis using assms Complex  lp15@68257  44  apply (simp add: cmod_def)  lp15@59870  45  apply (rule power2_less_imp_less, auto)  lp15@59870  46  apply (simp add: power2_eq_square field_simps)  lp15@59870  47  done  lp15@59870  48 qed  lp15@59870  49 wenzelm@61945  50 lemma cmod_diff_real_less: "Im z \ 0 \ x\0 \ cmod (z - x) < cmod z + \x\"  lp15@59870  51  using cmod_add_real_less [of z "-x"]  lp15@59870  52  by simp  lp15@59870  53 lp15@59870  54 lemma cmod_square_less_1_plus:  lp15@59870  55  assumes "Im z = 0 \ \Re z\ < 1"  lp15@59870  56  shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"  lp15@68257  57 proof (cases "Im z = 0 \ Re z = 0")  lp15@68257  58  case True  lp15@68493  59  with assms abs_square_less_1 show ?thesis  lp15@68257  60  by (force simp add: Re_power2 Im_power2 cmod_def)  lp15@68257  61 next  lp15@68257  62  case False  lp15@68257  63  with cmod_diff_real_less [of "1 - z\<^sup>2" "1"] show ?thesis  lp15@68257  64  by (simp add: norm_power Im_power2)  lp15@68257  65 qed  lp15@59870  66 eberlm@69180  67 subsection%unimportant\The Exponential Function\  lp15@59745  68 lp15@68499  69 lemma norm_exp_i_times [simp]: "norm (exp(\ * of_real y)) = 1"  lp15@68499  70  by simp  lp15@68499  71 lp15@68499  72 lemma norm_exp_imaginary: "norm(exp z) = 1 \ Re z = 0"  lp15@68499  73  by simp  lp15@68499  74 lp15@62534  75 lemma field_differentiable_within_exp: "exp field_differentiable (at z within s)"  lp15@62534  76  using DERIV_exp field_differentiable_at_within field_differentiable_def by blast  lp15@59745  77 lp15@59745  78 lemma continuous_within_exp:  lp15@59745  79  fixes z::"'a::{real_normed_field,banach}"  lp15@59745  80  shows "continuous (at z within s) exp"  lp15@59745  81 by (simp add: continuous_at_imp_continuous_within)  lp15@59745  82 lp15@62381  83 lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"  lp15@62534  84  by (simp add: field_differentiable_within_exp holomorphic_on_def)  lp15@59745  85 eberlm@66480  86 lemma holomorphic_on_exp' [holomorphic_intros]:  eberlm@66480  87  "f holomorphic_on s \ (\x. exp (f x)) holomorphic_on s"  eberlm@66480  88  using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def)  eberlm@66480  89 nipkow@67968  90 subsection\Euler and de Moivre formulas\  wenzelm@60420  91 wenzelm@60420  92 text\The sine series times @{term i}\  lp15@65064  93 lemma sin_i_eq: "(\n. (\ * sin_coeff n) * z^n) sums (\ * sin z)"  lp15@59745  94 proof -  wenzelm@63589  95  have "(\n. \ * sin_coeff n *\<^sub>R z^n) sums (\ * sin z)"  lp15@59745  96  using sin_converges sums_mult by blast  lp15@59745  97  then show ?thesis  lp15@59745  98  by (simp add: scaleR_conv_of_real field_simps)  lp15@59745  99 qed  lp15@59745  100 wenzelm@63589  101 theorem exp_Euler: "exp(\ * z) = cos(z) + \ * sin(z)"  lp15@59745  102 proof -  lp15@68257  103  have "(\n. (cos_coeff n + \ * sin_coeff n) * z^n) = (\n. (\ * z) ^ n /\<^sub>R (fact n))"  lp15@59745  104  proof  lp15@59745  105  fix n  wenzelm@63589  106  show "(cos_coeff n + \ * sin_coeff n) * z^n = (\ * z) ^ n /\<^sub>R (fact n)"  lp15@59745  107  by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)  lp15@59745  108  qed  wenzelm@63589  109  also have "... sums (exp (\ * z))"  lp15@59745  110  by (rule exp_converges)  wenzelm@63589  111  finally have "(\n. (cos_coeff n + \ * sin_coeff n) * z^n) sums (exp (\ * z))" .  wenzelm@63589  112  moreover have "(\n. (cos_coeff n + \ * sin_coeff n) * z^n) sums (cos z + \ * sin z)"  lp15@65064  113  using sums_add [OF cos_converges [of z] sin_i_eq [of z]]  lp15@59745  114  by (simp add: field_simps scaleR_conv_of_real)  lp15@59745  115  ultimately show ?thesis  lp15@59745  116  using sums_unique2 by blast  lp15@59745  117 qed  lp15@59745  118 eberlm@69180  119 corollary%unimportant exp_minus_Euler: "exp(-(\ * z)) = cos(z) - \ * sin(z)"  lp15@59745  120  using exp_Euler [of "-z"]  lp15@59745  121  by simp  lp15@59745  122 wenzelm@63589  123 lemma sin_exp_eq: "sin z = (exp(\ * z) - exp(-(\ * z))) / (2*\)"  lp15@59745  124  by (simp add: exp_Euler exp_minus_Euler)  lp15@59745  125 wenzelm@63589  126 lemma sin_exp_eq': "sin z = \ * (exp(-(\ * z)) - exp(\ * z)) / 2"  lp15@59745  127  by (simp add: exp_Euler exp_minus_Euler)  lp15@59745  128 wenzelm@63589  129 lemma cos_exp_eq: "cos z = (exp(\ * z) + exp(-(\ * z))) / 2"  lp15@59745  130  by (simp add: exp_Euler exp_minus_Euler)  lp15@59745  131 eberlm@69180  132 theorem Euler: "exp(z) = of_real(exp(Re z)) *  eberlm@69180  133  (of_real(cos(Im z)) + \ * of_real(sin(Im z)))"  eberlm@69180  134 by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real Complex_eq)  eberlm@69180  135 eberlm@69180  136 lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"  eberlm@69180  137  by (simp add: sin_exp_eq field_simps Re_divide Im_exp)  eberlm@69180  138 eberlm@69180  139 lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"  eberlm@69180  140  by (simp add: sin_exp_eq field_simps Im_divide Re_exp)  eberlm@69180  141 eberlm@69180  142 lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"  eberlm@69180  143  by (simp add: cos_exp_eq field_simps Re_divide Re_exp)  eberlm@69180  144 eberlm@69180  145 lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"  eberlm@69180  146  by (simp add: cos_exp_eq field_simps Im_divide Im_exp)  eberlm@69180  147 eberlm@69180  148 lemma Re_sin_pos: "0 < Re z \ Re z < pi \ Re (sin z) > 0"  eberlm@69180  149  by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)  eberlm@69180  150 eberlm@69180  151 lemma Im_sin_nonneg: "Re z = 0 \ 0 \ Im z \ 0 \ Im (sin z)"  eberlm@69180  152  by (simp add: Re_sin Im_sin algebra_simps)  eberlm@69180  153 eberlm@69180  154 lemma Im_sin_nonneg2: "Re z = pi \ Im z \ 0 \ 0 \ Im (sin z)"  eberlm@69180  155  by (simp add: Re_sin Im_sin algebra_simps)  eberlm@69180  156 eberlm@69180  157 subsection%unimportant\Relationships between real and complex trigonometric and hyperbolic functions\  lp15@59745  158 lp15@68257  159 lemma real_sin_eq [simp]: "Re(sin(of_real x)) = sin x"  lp15@59745  160  by (simp add: sin_of_real)  lp15@59862  161 lp15@68257  162 lemma real_cos_eq [simp]: "Re(cos(of_real x)) = cos x"  lp15@59745  163  by (simp add: cos_of_real)  lp15@59745  164 wenzelm@63589  165 lemma DeMoivre: "(cos z + \ * sin z) ^ n = cos(n * z) + \ * sin(n * z)"  lp15@68257  166  by (metis exp_Euler [symmetric] exp_of_nat_mult mult.left_commute)  lp15@68257  167 lp15@68257  168 lemma exp_cnj: "cnj (exp z) = exp (cnj z)"  lp15@59745  169 proof -  lp15@59745  170  have "(\n. cnj (z ^ n /\<^sub>R (fact n))) = (\n. (cnj z)^n /\<^sub>R (fact n))"  lp15@59745  171  by auto  lp15@59745  172  also have "... sums (exp (cnj z))"  lp15@59745  173  by (rule exp_converges)  lp15@59745  174  finally have "(\n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .  lp15@59745  175  moreover have "(\n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"  lp15@59862  176  by (metis exp_converges sums_cnj)  lp15@59745  177  ultimately show ?thesis  lp15@59745  178  using sums_unique2  lp15@59862  179  by blast  lp15@59745  180 qed  lp15@59745  181 lp15@59745  182 lemma cnj_sin: "cnj(sin z) = sin(cnj z)"  lp15@59745  183  by (simp add: sin_exp_eq exp_cnj field_simps)  lp15@59745  184 lp15@59745  185 lemma cnj_cos: "cnj(cos z) = cos(cnj z)"  lp15@59745  186  by (simp add: cos_exp_eq exp_cnj field_simps)  lp15@59745  187 lp15@62534  188 lemma field_differentiable_at_sin: "sin field_differentiable at z"  lp15@62534  189  using DERIV_sin field_differentiable_def by blast  lp15@62534  190 lp15@68257  191 lemma field_differentiable_within_sin: "sin field_differentiable (at z within S)"  lp15@62534  192  by (simp add: field_differentiable_at_sin field_differentiable_at_within)  lp15@62534  193 lp15@62534  194 lemma field_differentiable_at_cos: "cos field_differentiable at z"  lp15@62534  195  using DERIV_cos field_differentiable_def by blast  lp15@62534  196 lp15@68257  197 lemma field_differentiable_within_cos: "cos field_differentiable (at z within S)"  lp15@62534  198  by (simp add: field_differentiable_at_cos field_differentiable_at_within)  lp15@59745  199 lp15@68257  200 lemma holomorphic_on_sin: "sin holomorphic_on S"  lp15@62534  201  by (simp add: field_differentiable_within_sin holomorphic_on_def)  lp15@59745  202 lp15@68257  203 lemma holomorphic_on_cos: "cos holomorphic_on S"  lp15@62534  204  by (simp add: field_differentiable_within_cos holomorphic_on_def)  lp15@59745  205 eberlm@68721  206 lemma holomorphic_on_sin' [holomorphic_intros]:  eberlm@68721  207  assumes "f holomorphic_on A"  eberlm@68721  208  shows "(\x. sin (f x)) holomorphic_on A"  eberlm@68721  209  using holomorphic_on_compose[OF assms holomorphic_on_sin] by (simp add: o_def)  eberlm@68721  210 eberlm@68721  211 lemma holomorphic_on_cos' [holomorphic_intros]:  eberlm@68721  212  assumes "f holomorphic_on A"  eberlm@68721  213  shows "(\x. cos (f x)) holomorphic_on A"  eberlm@68721  214  using holomorphic_on_compose[OF assms holomorphic_on_cos] by (simp add: o_def)  eberlm@68721  215 eberlm@69180  216 subsection%unimportant\More on the Polar Representation of Complex Numbers\  lp15@59746  217 lp15@59746  218 lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"  lp15@65274  219  by (simp add: Complex_eq exp_add exp_Euler exp_of_real sin_of_real cos_of_real)  lp15@59746  220 lp15@59746  221 lemma exp_eq_1: "exp z = 1 \ Re(z) = 0 \ (\n::int. Im(z) = of_int (2 * n) * pi)"  lp15@65274  222  (is "?lhs = ?rhs")  lp15@68493  223 proof  lp15@65274  224  assume "exp z = 1"  lp15@65274  225  then have "Re z = 0"  lp15@65274  226  by (metis exp_eq_one_iff norm_exp_eq_Re norm_one)  lp15@65274  227  with \?lhs\ show ?rhs  lp15@65274  228  by (metis Re_exp complex_Re_of_int cos_one_2pi_int exp_zero mult.commute mult_numeral_1 numeral_One of_int_mult of_int_numeral)  lp15@65274  229 next  lp15@65274  230  assume ?rhs then show ?lhs  lp15@68499  231  using Im_exp Re_exp complex_eq_iff  lp15@68499  232  by (simp add: cos_one_2pi_int cos_one_sin_zero mult.commute)  lp15@65274  233 qed  lp15@59746  234 wenzelm@63589  235 lemma exp_eq: "exp w = exp z \ (\n::int. w = z + (of_int (2 * n) * pi) * \)"  lp15@59746  236  (is "?lhs = ?rhs")  lp15@59746  237 proof -  lp15@59746  238  have "exp w = exp z \ exp (w-z) = 1"  lp15@59746  239  by (simp add: exp_diff)  lp15@59746  240  also have "... \ (Re w = Re z \ (\n::int. Im w - Im z = of_int (2 * n) * pi))"  lp15@59746  241  by (simp add: exp_eq_1)  lp15@59746  242  also have "... \ ?rhs"  lp15@59746  243  by (auto simp: algebra_simps intro!: complex_eqI)  lp15@59746  244  finally show ?thesis .  lp15@59746  245 qed  lp15@59746  246 wenzelm@61945  247 lemma exp_complex_eqI: "\Im w - Im z\ < 2*pi \ exp w = exp z \ w = z"  lp15@59746  248  by (auto simp: exp_eq abs_mult)  lp15@59746  249 lp15@59862  250 lemma exp_integer_2pi:  wenzelm@61070  251  assumes "n \ \"  wenzelm@63589  252  shows "exp((2 * n * pi) * \) = 1"  lp15@59746  253 proof -  wenzelm@63589  254  have "exp((2 * n * pi) * \) = exp 0"  lp15@68257  255  using assms unfolding Ints_def exp_eq by auto  lp15@59746  256  also have "... = 1"  lp15@59746  257  by simp  lp15@59746  258  finally show ?thesis .  lp15@59746  259 qed  lp15@59746  260 lp15@64287  261 lemma exp_plus_2pin [simp]: "exp (z + \ * (of_int n * (of_real pi * 2))) = exp z"  lp15@64287  262  by (simp add: exp_eq)  lp15@64287  263 eberlm@66466  264 lemma exp_integer_2pi_plus1:  eberlm@66466  265  assumes "n \ \"  eberlm@66466  266  shows "exp(((2 * n + 1) * pi) * \) = - 1"  eberlm@66466  267 proof -  eberlm@66466  268  from assms obtain n' where [simp]: "n = of_int n'"  eberlm@66466  269  by (auto simp: Ints_def)  eberlm@66466  270  have "exp(((2 * n + 1) * pi) * \) = exp (pi * \)"  eberlm@66466  271  using assms by (subst exp_eq) (auto intro!: exI[of _ n'] simp: algebra_simps)  eberlm@66466  272  also have "... = - 1"  eberlm@66466  273  by simp  eberlm@66466  274  finally show ?thesis .  eberlm@66466  275 qed  eberlm@66466  276 lp15@64287  277 lemma inj_on_exp_pi:  lp15@64287  278  fixes z::complex shows "inj_on exp (ball z pi)"  lp15@64287  279 proof (clarsimp simp: inj_on_def exp_eq)  lp15@64287  280  fix y n  lp15@64287  281  assume "dist z (y + 2 * of_int n * of_real pi * \) < pi"  lp15@64287  282  "dist z y < pi"  lp15@64287  283  then have "dist y (y + 2 * of_int n * of_real pi * \) < pi+pi"  lp15@64287  284  using dist_commute_lessI dist_triangle_less_add by blast  lp15@64287  285  then have "norm (2 * of_int n * of_real pi * \) < 2*pi"  lp15@64287  286  by (simp add: dist_norm)  lp15@64287  287  then show "n = 0"  lp15@64287  288  by (auto simp: norm_mult)  lp15@64287  289 qed  lp15@64287  290 lp15@68585  291 lemma cmod_add_squared:  lp15@68585  292  fixes r1 r2::real  lp15@68585  293  assumes "r1 \ 0" "r2 \ 0"  lp15@68585  294  shows "(cmod (r1 * exp (\ * \1) + r2 * exp (\ * \2)))\<^sup>2 = r1\<^sup>2 + r2\<^sup>2 + 2 * r1 * r2 * cos (\1 - \2)" (is "(cmod (?z1 + ?z2))\<^sup>2 = ?rhs")  lp15@68585  295 proof -  lp15@68585  296  have "(cmod (?z1 + ?z2))\<^sup>2 = (?z1 + ?z2) * cnj (?z1 + ?z2)"  lp15@68585  297  by (rule complex_norm_square)  lp15@68585  298  also have "\ = (?z1 * cnj ?z1 + ?z2 * cnj ?z2) + (?z1 * cnj ?z2 + cnj ?z1 * ?z2)"  lp15@68585  299  by (simp add: algebra_simps)  lp15@68585  300  also have "\ = (norm ?z1)\<^sup>2 + (norm ?z2)\<^sup>2 + 2 * Re (?z1 * cnj ?z2)"  lp15@68585  301  unfolding complex_norm_square [symmetric] cnj_add_mult_eq_Re by simp  lp15@68585  302  also have "\ = ?rhs"  lp15@68585  303  by (simp add: norm_mult) (simp add: exp_Euler complex_is_Real_iff [THEN iffD1] cos_diff algebra_simps)  lp15@68585  304  finally show ?thesis  lp15@68585  305  using of_real_eq_iff by blast  lp15@68585  306 qed  lp15@68585  307 lp15@68585  308 lemma cmod_diff_squared:  lp15@68585  309  fixes r1 r2::real  lp15@68585  310  assumes "r1 \ 0" "r2 \ 0"  lp15@68585  311  shows "(cmod (r1 * exp (\ * \1) - r2 * exp (\ * \2)))\<^sup>2 = r1\<^sup>2 + r2\<^sup>2 - 2*r1*r2*cos (\1 - \2)" (is "(cmod (?z1 - ?z2))\<^sup>2 = ?rhs")  lp15@68585  312 proof -  lp15@68585  313  have "exp (\ * (\2 + pi)) = - exp (\ * \2)"  lp15@68585  314  by (simp add: exp_Euler cos_plus_pi sin_plus_pi)  lp15@68585  315  then have "(cmod (?z1 - ?z2))\<^sup>2 = cmod (?z1 + r2 * exp (\ * (\2 + pi))) ^2"  lp15@68585  316  by simp  lp15@68585  317  also have "\ = r1\<^sup>2 + r2\<^sup>2 + 2*r1*r2*cos (\1 - (\2 + pi))"  lp15@68585  318  using assms cmod_add_squared by blast  lp15@68585  319  also have "\ = ?rhs"  lp15@68585  320  by (simp add: add.commute diff_add_eq_diff_diff_swap)  lp15@68585  321  finally show ?thesis .  lp15@68585  322 qed  lp15@68585  323 lp15@68585  324 lemma polar_convergence:  lp15@68585  325  fixes R::real  lp15@68585  326  assumes "\j. r j > 0" "R > 0"  lp15@68585  327  shows "((\j. r j * exp (\ * \ j)) \ (R * exp (\ * \))) \  lp15@68585  328  (r \ R) \ (\k. (\j. \ j - of_int (k j) * (2 * pi)) \ \)" (is "(?z \ ?Z) = ?rhs")  lp15@68585  329 proof  lp15@68585  330  assume L: "?z \ ?Z"  lp15@68585  331  have rR: "r \ R"  lp15@68585  332  using tendsto_norm [OF L] assms by (auto simp: norm_mult abs_of_pos)  lp15@68585  333  moreover obtain k where "(\j. \ j - of_int (k j) * (2 * pi)) \ \"  lp15@68585  334  proof -  lp15@68585  335  have "cos (\ j - \) = ((r j)\<^sup>2 + R\<^sup>2 - (norm(?z j - ?Z))\<^sup>2) / (2 * R * r j)" for j  lp15@68585  336  apply (subst cmod_diff_squared)  lp15@68585  337  using assms by (auto simp: divide_simps less_le)  lp15@68585  338  moreover have "(\j. ((r j)\<^sup>2 + R\<^sup>2 - (norm(?z j - ?Z))\<^sup>2) / (2 * R * r j)) \ ((R\<^sup>2 + R\<^sup>2 - (norm(?Z - ?Z))\<^sup>2) / (2 * R * R))"  lp15@68585  339  by (intro L rR tendsto_intros) (use \R > 0\ in force)  lp15@68585  340  moreover have "((R\<^sup>2 + R\<^sup>2 - (norm(?Z - ?Z))\<^sup>2) / (2 * R * R)) = 1"  lp15@68585  341  using \R > 0\ by (simp add: power2_eq_square divide_simps)  lp15@68585  342  ultimately have "(\j. cos (\ j - \)) \ 1"  lp15@68585  343  by auto  lp15@68585  344  then show ?thesis  lp15@68585  345  using that cos_diff_limit_1 by blast  lp15@68585  346  qed  lp15@68585  347  ultimately show ?rhs  lp15@68585  348  by metis  lp15@68585  349 next  lp15@68585  350  assume R: ?rhs  lp15@68585  351  show "?z \ ?Z"  lp15@68585  352  proof (rule tendsto_mult)  lp15@68585  353  show "(\x. complex_of_real (r x)) \ of_real R"  lp15@68585  354  using R by (auto simp: tendsto_of_real_iff)  lp15@68585  355  obtain k where "(\j. \ j - of_int (k j) * (2 * pi)) \ \"  lp15@68585  356  using R by metis  lp15@68585  357  then have "(\j. complex_of_real (\ j - of_int (k j) * (2 * pi))) \ of_real \"  lp15@68585  358  using tendsto_of_real_iff by force  lp15@68585  359  then have "(\j. exp (\ * of_real (\ j - of_int (k j) * (2 * pi)))) \ exp (\ * \)"  lp15@68585  360  using tendsto_mult [OF tendsto_const] isCont_exp isCont_tendsto_compose by blast  lp15@68585  361  moreover have "exp (\ * of_real (\ j - of_int (k j) * (2 * pi))) = exp (\ * \ j)" for j  lp15@68585  362  unfolding exp_eq  lp15@68585  363  by (rule_tac x="- k j" in exI) (auto simp: algebra_simps)  lp15@68585  364  ultimately show "(\j. exp (\ * \ j)) \ exp (\ * \)"  lp15@68585  365  by auto  lp15@68585  366  qed  lp15@68585  367 qed  lp15@68585  368 lp15@68499  369 lemma sin_cos_eq_iff: "sin y = sin x \ cos y = cos x \ (\n::int. y = x + 2 * pi * n)"  lp15@59746  370 proof -  lp15@59746  371  { assume "sin y = sin x" "cos y = cos x"  lp15@59746  372  then have "cos (y-x) = 1"  lp15@59746  373  using cos_add [of y "-x"] by simp  lp15@68499  374  then have "\n::int. y-x = 2 * pi * n"  lp15@68499  375  using cos_one_2pi_int by auto }  lp15@59746  376  then show ?thesis  lp15@59746  377  apply (auto simp: sin_add cos_add)  lp15@68499  378  apply (metis add.commute diff_add_cancel)  lp15@59746  379  done  lp15@59746  380 qed  lp15@59746  381 lp15@59862  382 lemma exp_i_ne_1:  lp15@59746  383  assumes "0 < x" "x < 2*pi"  lp15@59746  384  shows "exp(\ * of_real x) \ 1"  lp15@59862  385 proof  lp15@59746  386  assume "exp (\ * of_real x) = 1"  lp15@59746  387  then have "exp (\ * of_real x) = exp 0"  lp15@59746  388  by simp  lp15@59746  389  then obtain n where "\ * of_real x = (of_int (2 * n) * pi) * \"  lp15@59746  390  by (simp only: Ints_def exp_eq) auto  lp15@68257  391  then have "of_real x = (of_int (2 * n) * pi)"  lp15@59746  392  by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)  lp15@68257  393  then have "x = (of_int (2 * n) * pi)"  lp15@59746  394  by simp  lp15@59746  395  then show False using assms  lp15@59746  396  by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)  lp15@59746  397 qed  lp15@59746  398 lp15@59862  399 lemma sin_eq_0:  lp15@59746  400  fixes z::complex  lp15@59746  401  shows "sin z = 0 \ (\n::int. z = of_real(n * pi))"  lp15@68257  402  by (simp add: sin_exp_eq exp_eq)  lp15@59746  403 lp15@59862  404 lemma cos_eq_0:  lp15@59746  405  fixes z::complex  lp15@59746  406  shows "cos z = 0 \ (\n::int. z = of_real(n * pi) + of_real pi/2)"  lp15@59746  407  using sin_eq_0 [of "z - of_real pi/2"]  lp15@59746  408  by (simp add: sin_diff algebra_simps)  lp15@59746  409 lp15@59862  410 lemma cos_eq_1:  lp15@59746  411  fixes z::complex  lp15@59746  412  shows "cos z = 1 \ (\n::int. z = of_real(2 * n * pi))"  lp15@59746  413 proof -  lp15@59746  414  have "cos z = cos (2*(z/2))"  lp15@59746  415  by simp  lp15@59746  416  also have "... = 1 - 2 * sin (z/2) ^ 2"  lp15@59746  417  by (simp only: cos_double_sin)  lp15@59746  418  finally have [simp]: "cos z = 1 \ sin (z/2) = 0"  lp15@59746  419  by simp  lp15@59746  420  show ?thesis  lp15@68257  421  by (auto simp: sin_eq_0)  lp15@59862  422 qed  lp15@59746  423 lp15@59746  424 lemma csin_eq_1:  lp15@59746  425  fixes z::complex  lp15@59746  426  shows "sin z = 1 \ (\n::int. z = of_real(2 * n * pi) + of_real pi/2)"  lp15@59746  427  using cos_eq_1 [of "z - of_real pi/2"]  lp15@59746  428  by (simp add: cos_diff algebra_simps)  lp15@59746  429 lp15@59746  430 lemma csin_eq_minus1:  lp15@59746  431  fixes z::complex  lp15@59746  432  shows "sin z = -1 \ (\n::int. z = of_real(2 * n * pi) + 3/2*pi)"  lp15@59746  433  (is "_ = ?rhs")  lp15@59746  434 proof -  lp15@59746  435  have "sin z = -1 \ sin (-z) = 1"  lp15@59746  436  by (simp add: equation_minus_iff)  lp15@68257  437  also have "... \ (\n::int. -z = of_real(2 * n * pi) + of_real pi/2)"  lp15@59746  438  by (simp only: csin_eq_1)  lp15@68257  439  also have "... \ (\n::int. z = - of_real(2 * n * pi) - of_real pi/2)"  lp15@59746  440  apply (rule iff_exI)  lp15@68257  441  by (metis (no_types) is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff)  lp15@59746  442  also have "... = ?rhs"  lp15@68257  443  apply safe  lp15@59746  444  apply (rule_tac [2] x="-(x+1)" in exI)  lp15@59746  445  apply (rule_tac x="-(x+1)" in exI)  lp15@59746  446  apply (simp_all add: algebra_simps)  lp15@59746  447  done  lp15@59746  448  finally show ?thesis .  lp15@59862  449 qed  lp15@59746  450 lp15@59862  451 lemma ccos_eq_minus1:  lp15@59746  452  fixes z::complex  lp15@59746  453  shows "cos z = -1 \ (\n::int. z = of_real(2 * n * pi) + pi)"  lp15@59746  454  using csin_eq_1 [of "z - of_real pi/2"]  lp15@68257  455  by (simp add: sin_diff algebra_simps equation_minus_iff)  lp15@59746  456 lp15@59746  457 lemma sin_eq_1: "sin x = 1 \ (\n::int. x = (2 * n + 1 / 2) * pi)"  lp15@59746  458  (is "_ = ?rhs")  lp15@59746  459 proof -  lp15@59746  460  have "sin x = 1 \ sin (complex_of_real x) = 1"  lp15@59746  461  by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)  lp15@68257  462  also have "... \ (\n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"  lp15@59746  463  by (simp only: csin_eq_1)  lp15@68257  464  also have "... \ (\n::int. x = of_real(2 * n * pi) + of_real pi/2)"  lp15@68257  465  by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])  lp15@59746  466  also have "... = ?rhs"  lp15@59746  467  by (auto simp: algebra_simps)  lp15@59746  468  finally show ?thesis .  lp15@59862  469 qed  lp15@59746  470 lp15@59746  471 lemma sin_eq_minus1: "sin x = -1 \ (\n::int. x = (2*n + 3/2) * pi)" (is "_ = ?rhs")  lp15@59746  472 proof -  lp15@59746  473  have "sin x = -1 \ sin (complex_of_real x) = -1"  lp15@59746  474  by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)  lp15@68257  475  also have "... \ (\n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"  lp15@59746  476  by (simp only: csin_eq_minus1)  lp15@68257  477  also have "... \ (\n::int. x = of_real(2 * n * pi) + 3/2*pi)"  lp15@68257  478  by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])  lp15@59746  479  also have "... = ?rhs"  lp15@59746  480  by (auto simp: algebra_simps)  lp15@59746  481  finally show ?thesis .  lp15@59862  482 qed  lp15@59746  483 lp15@59746  484 lemma cos_eq_minus1: "cos x = -1 \ (\n::int. x = (2*n + 1) * pi)"  lp15@59746  485  (is "_ = ?rhs")  lp15@59746  486 proof -  lp15@59746  487  have "cos x = -1 \ cos (complex_of_real x) = -1"  lp15@59746  488  by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)  lp15@68257  489  also have "... \ (\n::int. complex_of_real x = of_real(2 * n * pi) + pi)"  lp15@59746  490  by (simp only: ccos_eq_minus1)  lp15@68257  491  also have "... \ (\n::int. x = of_real(2 * n * pi) + pi)"  lp15@68257  492  by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])  lp15@59746  493  also have "... = ?rhs"  lp15@59746  494  by (auto simp: algebra_simps)  lp15@59746  495  finally show ?thesis .  lp15@59862  496 qed  lp15@59746  497 lp15@65064  498 lemma dist_exp_i_1: "norm(exp(\ * of_real t) - 1) = 2 * \sin(t / 2)\"  lp15@59862  499  apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)  lp15@59746  500  using cos_double_sin [of "t/2"]  lp15@59746  501  apply (simp add: real_sqrt_mult)  lp15@59746  502  done  lp15@59746  503 lp15@64773  504 lp15@64773  505 lemma complex_sin_eq:  lp15@64773  506  fixes w :: complex  lp15@64773  507  shows "sin w = sin z \ (\n \ \. w = z + of_real(2*n*pi) \ w = -z + of_real((2*n + 1)*pi))"  lp15@64773  508  (is "?lhs = ?rhs")  lp15@64773  509 proof  lp15@64773  510  assume ?lhs  lp15@64773  511  then have "sin w - sin z = 0"  lp15@64773  512  by (auto simp: algebra_simps)  lp15@64773  513  then have "sin ((w - z) / 2)*cos ((w + z) / 2) = 0"  lp15@64773  514  by (auto simp: sin_diff_sin)  lp15@64773  515  then consider "sin ((w - z) / 2) = 0" | "cos ((w + z) / 2) = 0"  lp15@64773  516  using mult_eq_0_iff by blast  lp15@64773  517  then show ?rhs  lp15@64773  518  proof cases  lp15@64773  519  case 1  lp15@64773  520  then show ?thesis  lp15@68257  521  by (simp add: sin_eq_0 algebra_simps) (metis Ints_of_int of_real_of_int_eq)  lp15@64773  522  next  lp15@64773  523  case 2  lp15@64773  524  then show ?thesis  lp15@68257  525  by (simp add: cos_eq_0 algebra_simps) (metis Ints_of_int of_real_of_int_eq)  lp15@64773  526  qed  lp15@64773  527 next  lp15@64773  528  assume ?rhs  lp15@64773  529  then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \  lp15@64773  530  w = -z + of_real ((2* of_int n + 1)*pi)"  lp15@64773  531  using Ints_cases by blast  lp15@64773  532  then show ?lhs  lp15@64773  533  using Periodic_Fun.sin.plus_of_int [of z n]  lp15@64773  534  apply (auto simp: algebra_simps)  lp15@64773  535  by (metis (no_types, hide_lams) add_diff_cancel_left add_diff_cancel_left' add_minus_cancel  lp15@64773  536  mult.commute sin.plus_of_int sin_minus sin_plus_pi)  lp15@64773  537 qed  lp15@64773  538 lp15@64773  539 lemma complex_cos_eq:  lp15@64773  540  fixes w :: complex  lp15@68257  541  shows "cos w = cos z \ (\n \ \. w = z + of_real(2*n*pi) \ w = -z + of_real(2*n*pi))"  lp15@64773  542  (is "?lhs = ?rhs")  lp15@64773  543 proof  lp15@64773  544  assume ?lhs  lp15@64773  545  then have "cos w - cos z = 0"  lp15@64773  546  by (auto simp: algebra_simps)  lp15@64773  547  then have "sin ((w + z) / 2) * sin ((z - w) / 2) = 0"  lp15@64773  548  by (auto simp: cos_diff_cos)  lp15@64773  549  then consider "sin ((w + z) / 2) = 0" | "sin ((z - w) / 2) = 0"  lp15@64773  550  using mult_eq_0_iff by blast  lp15@64773  551  then show ?rhs  lp15@64773  552  proof cases  lp15@64773  553  case 1  lp15@64773  554  then show ?thesis  lp15@68257  555  apply (simp add: sin_eq_0 algebra_simps)  lp15@64773  556  by (metis Ints_of_int of_real_of_int_eq)  lp15@64773  557  next  lp15@64773  558  case 2  lp15@64773  559  then show ?thesis  lp15@68257  560  apply (clarsimp simp: sin_eq_0 algebra_simps)  lp15@64773  561  by (metis Ints_of_int add_minus_cancel distrib_right mult_of_int_commute mult_zero_right of_int_0 of_int_add of_real_of_int_eq)  lp15@64773  562  qed  lp15@64773  563 next  lp15@64773  564  assume ?rhs  lp15@64773  565  then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \  lp15@64773  566  w = -z + of_real(2*n*pi)"  lp15@64773  567  using Ints_cases by (metis of_int_mult of_int_numeral)  lp15@64773  568  then show ?lhs  lp15@64773  569  using Periodic_Fun.cos.plus_of_int [of z n]  lp15@68257  570  apply (simp add: algebra_simps)  lp15@64773  571  by (metis cos.plus_of_int cos_minus minus_add_cancel mult.commute)  lp15@64773  572 qed  lp15@64773  573 lp15@64773  574 lemma sin_eq:  lp15@64773  575  "sin x = sin y \ (\n \ \. x = y + 2*n*pi \ x = -y + (2*n + 1)*pi)"  lp15@64773  576  using complex_sin_eq [of x y]  lp15@64773  577  by (simp only: sin_of_real Re_complex_of_real of_real_add [symmetric] of_real_minus [symmetric] of_real_mult [symmetric] of_real_eq_iff)  lp15@64773  578 lp15@64773  579 lemma cos_eq:  lp15@64773  580  "cos x = cos y \ (\n \ \. x = y + 2*n*pi \ x = -y + 2*n*pi)"  lp15@64773  581  using complex_cos_eq [of x y]  lp15@64773  582  by (simp only: cos_of_real Re_complex_of_real of_real_add [symmetric] of_real_minus [symmetric] of_real_mult [symmetric] of_real_eq_iff)  lp15@64773  583 lp15@59746  584 lemma sinh_complex:  lp15@59746  585  fixes z :: complex  wenzelm@63589  586  shows "(exp z - inverse (exp z)) / 2 = -\ * sin(\ * z)"  lp15@65274  587  by (simp add: sin_exp_eq divide_simps exp_minus)  lp15@59746  588 lp15@65064  589 lemma sin_i_times:  lp15@59746  590  fixes z :: complex  wenzelm@63589  591  shows "sin(\ * z) = \ * ((exp z - inverse (exp z)) / 2)"  lp15@59746  592  using sinh_complex by auto  lp15@59746  593 lp15@59746  594 lemma sinh_real:  lp15@59746  595  fixes x :: real  wenzelm@63589  596  shows "of_real((exp x - inverse (exp x)) / 2) = -\ * sin(\ * of_real x)"  lp15@65274  597  by (simp add: exp_of_real sin_i_times)  lp15@59746  598 lp15@59746  599 lemma cosh_complex:  lp15@59746  600  fixes z :: complex  wenzelm@63589  601  shows "(exp z + inverse (exp z)) / 2 = cos(\ * z)"  lp15@65274  602  by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real)  lp15@59746  603 lp15@59746  604 lemma cosh_real:  lp15@59746  605  fixes x :: real  wenzelm@63589  606  shows "of_real((exp x + inverse (exp x)) / 2) = cos(\ * of_real x)"  lp15@65274  607  by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real)  lp15@59746  608 lp15@65064  609 lemmas cos_i_times = cosh_complex [symmetric]  lp15@59746  610 lp15@59862  611 lemma norm_cos_squared:  lp15@59746  612  "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"  lp15@59746  613  apply (cases z)  lp15@65274  614  apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real Complex_eq)  lp15@61694  615  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)  lp15@68257  616  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib sin_squared_eq)  lp15@59746  617  apply (simp add: power2_eq_square algebra_simps divide_simps)  lp15@59746  618  done  lp15@59746  619 lp15@59746  620 lemma norm_sin_squared:  lp15@59746  621  "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"  lp15@59746  622  apply (cases z)  lp15@65274  623  apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq)  lp15@61694  624  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)  lp15@68257  625  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib cos_squared_eq)  lp15@59746  626  apply (simp add: power2_eq_square algebra_simps divide_simps)  lp15@59862  627  done  lp15@59746  628 lp15@59746  629 lemma exp_uminus_Im: "exp (- Im z) \ exp (cmod z)"  lp15@59746  630  using abs_Im_le_cmod linear order_trans by fastforce  lp15@59746  631 lp15@59862  632 lemma norm_cos_le:  lp15@59746  633  fixes z::complex  lp15@59746  634  shows "norm(cos z) \ exp(norm z)"  lp15@59746  635 proof -  lp15@59746  636  have "Im z \ cmod z"  lp15@59746  637  using abs_Im_le_cmod abs_le_D1 by auto  lp15@59746  638  with exp_uminus_Im show ?thesis  lp15@59746  639  apply (simp add: cos_exp_eq norm_divide)  lp15@59746  640  apply (rule order_trans [OF norm_triangle_ineq], simp)  lp15@59746  641  apply (metis add_mono exp_le_cancel_iff mult_2_right)  lp15@59746  642  done  lp15@59746  643 qed  lp15@59746  644 lp15@59862  645 lemma norm_cos_plus1_le:  lp15@59746  646  fixes z::complex  lp15@59746  647  shows "norm(1 + cos z) \ 2 * exp(norm z)"  lp15@59746  648 proof -  lp15@59746  649  have mono: "\u w z::real. (1 \ w | 1 \ z) \ (w \ u & z \ u) \ 2 + w + z \ 4 * u"  lp15@59746  650  by arith  lp15@59746  651  have *: "Im z \ cmod z"  lp15@59746  652  using abs_Im_le_cmod abs_le_D1 by auto  lp15@59746  653  have triangle3: "\x y z. norm(x + y + z) \ norm(x) + norm(y) + norm(z)"  lp15@59746  654  by (simp add: norm_add_rule_thm)  lp15@59746  655  have "norm(1 + cos z) = cmod (1 + (exp (\ * z) + exp (- (\ * z))) / 2)"  lp15@59746  656  by (simp add: cos_exp_eq)  lp15@59746  657  also have "... = cmod ((2 + exp (\ * z) + exp (- (\ * z))) / 2)"  lp15@59746  658  by (simp add: field_simps)  lp15@59746  659  also have "... = cmod (2 + exp (\ * z) + exp (- (\ * z))) / 2"  lp15@59746  660  by (simp add: norm_divide)  lp15@59746  661  finally show ?thesis  lp15@68257  662  by (metis exp_eq_one_iff exp_le_cancel_iff mult_2 norm_cos_le norm_ge_zero norm_one norm_triangle_mono)  lp15@59746  663 qed  lp15@59746  664 eberlm@67578  665 lemma sinh_conv_sin: "sinh z = -\ * sin (\*z)"  eberlm@67578  666  by (simp add: sinh_field_def sin_i_times exp_minus)  eberlm@67578  667 eberlm@67578  668 lemma cosh_conv_cos: "cosh z = cos (\*z)"  eberlm@67578  669  by (simp add: cosh_field_def cos_i_times exp_minus)  eberlm@67578  670 eberlm@67578  671 lemma tanh_conv_tan: "tanh z = -\ * tan (\*z)"  eberlm@67578  672  by (simp add: tanh_def sinh_conv_sin cosh_conv_cos tan_def)  eberlm@67578  673 eberlm@67578  674 lemma sin_conv_sinh: "sin z = -\ * sinh (\*z)"  eberlm@67578  675  by (simp add: sinh_conv_sin)  eberlm@67578  676 eberlm@67578  677 lemma cos_conv_cosh: "cos z = cosh (\*z)"  eberlm@67578  678  by (simp add: cosh_conv_cos)  eberlm@67578  679 eberlm@67578  680 lemma tan_conv_tanh: "tan z = -\ * tanh (\*z)"  eberlm@67578  681  by (simp add: tan_def sin_conv_sinh cos_conv_cosh tanh_def)  eberlm@67578  682 eberlm@67578  683 lemma sinh_complex_eq_iff:  eberlm@67578  684  "sinh (z :: complex) = sinh w \  eberlm@67578  685  (\n\\. z = w - 2 * \ * of_real n * of_real pi \  eberlm@67578  686  z = -(2 * complex_of_real n + 1) * \ * complex_of_real pi - w)" (is "_ = ?rhs")  eberlm@67578  687 proof -  eberlm@67578  688  have "sinh z = sinh w \ sin (\ * z) = sin (\ * w)"  eberlm@67578  689  by (simp add: sinh_conv_sin)  eberlm@67578  690  also have "\ \ ?rhs"  eberlm@67578  691  by (subst complex_sin_eq) (force simp: field_simps complex_eq_iff)  eberlm@67578  692  finally show ?thesis .  eberlm@67578  693 qed  eberlm@67578  694 eberlm@67578  695 eberlm@69180  696 subsection%unimportant\Taylor series for complex exponential, sine and cosine\  lp15@59746  697 lp15@59746  698 declare power_Suc [simp del]  lp15@59746  699 immler@66252  700 lemma Taylor_exp_field:  immler@66252  701  fixes z::"'a::{banach,real_normed_field}"  immler@66252  702  shows "norm (exp z - (\i\n. z ^ i / fact i)) \ exp (norm z) * (norm z ^ Suc n) / fact n"  nipkow@69529  703 proof (rule field_Taylor[of _ n "\k. exp" "exp (norm z)" 0 z, simplified])  immler@66252  704  show "convex (closed_segment 0 z)"  immler@66252  705  by (rule convex_closed_segment [of 0 z])  immler@66252  706 next  immler@66252  707  fix k x  immler@66252  708  assume "x \ closed_segment 0 z" "k \ n"  immler@66252  709  show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"  immler@66252  710  using DERIV_exp DERIV_subset by blast  immler@66252  711 next  immler@66252  712  fix x  immler@66252  713  assume x: "x \ closed_segment 0 z"  immler@66252  714  have "norm (exp x) \ exp (norm x)"  immler@66252  715  by (rule norm_exp)  immler@66252  716  also have "norm x \ norm z"  immler@66252  717  using x by (auto simp: closed_segment_def intro!: mult_left_le_one_le)  immler@66252  718  finally show "norm (exp x) \ exp (norm z)"  immler@66252  719  by simp  lp15@68257  720 qed auto  immler@66252  721 lp15@59862  722 lemma Taylor_exp:  lp15@59746  723  "norm(exp z - (\k\n. z ^ k / (fact k))) \ exp\Re z\ * (norm z) ^ (Suc n) / (fact n)"  nipkow@69529  724 proof (rule complex_Taylor [of _ n "\k. exp" "exp\Re z\" 0 z, simplified])  lp15@59746  725  show "convex (closed_segment 0 z)"  paulson@61518  726  by (rule convex_closed_segment [of 0 z])  lp15@59746  727 next  lp15@59746  728  fix k x  lp15@59746  729  assume "x \ closed_segment 0 z" "k \ n"  lp15@59746  730  show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"  lp15@59746  731  using DERIV_exp DERIV_subset by blast  lp15@59746  732 next  lp15@59746  733  fix x  lp15@59746  734  assume "x \ closed_segment 0 z"  lp15@59746  735  then show "Re x \ \Re z\"  lp15@68257  736  apply (clarsimp simp: closed_segment_def scaleR_conv_of_real)  lp15@59746  737  by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans)  lp15@68257  738 qed auto  lp15@59746  739 lp15@59862  740 lemma  lp15@59746  741  assumes "0 \ u" "u \ 1"  lp15@59862  742  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \ exp \Im z\"  lp15@59746  743  and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \ exp \Im z\"  lp15@59746  744 proof -  lp15@68257  745  have mono: "\u w z::real. w \ u \ z \ u \ (w + z)/2 \ u"  lp15@68257  746  by simp  lp15@68257  747  have *: "(cmod (exp (\ * (u * z))) + cmod (exp (- (\ * (u * z)))) ) / 2 \ exp \Im z\"  lp15@68257  748  proof (rule mono)  lp15@68257  749  show "cmod (exp (\ * (u * z))) \ exp \Im z\"  lp15@68257  750  apply (simp add: abs_if mult_left_le_one_le assms not_less)  lp15@68257  751  by (meson assms(1) mult_nonneg_nonneg neg_le_0_iff_le order_trans)  lp15@68257  752  show "cmod (exp (- (\ * (u * z)))) \ exp \Im z\"  lp15@68257  753  apply (simp add: abs_if mult_left_le_one_le assms)  lp15@68257  754  by (meson \0 \ u\ less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)  lp15@68257  755  qed  lp15@68257  756  have "cmod (sin (u *\<^sub>R z)) = cmod (exp (\ * (u * z)) - exp (- (\ * (u * z)))) / 2"  lp15@68257  757  by (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)  lp15@68257  758  also have "... \ (cmod (exp (\ * (u * z))) + cmod (exp (- (\ * (u * z)))) ) / 2"  lp15@68257  759  by (intro divide_right_mono norm_triangle_ineq4) simp  lp15@68257  760  also have "... \ exp \Im z\"  lp15@68257  761  by (rule *)  lp15@68257  762  finally show "cmod (sin (u *\<^sub>R z)) \ exp \Im z\" .  lp15@68257  763  have "cmod (cos (u *\<^sub>R z)) = cmod (exp (\ * (u * z)) + exp (- (\ * (u * z)))) / 2"  lp15@68257  764  by (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)  lp15@68257  765  also have "... \ (cmod (exp (\ * (u * z))) + cmod (exp (- (\ * (u * z)))) ) / 2"  lp15@68257  766  by (intro divide_right_mono norm_triangle_ineq) simp  lp15@68257  767  also have "... \ exp \Im z\"  lp15@68257  768  by (rule *)  lp15@68257  769  finally show "cmod (cos (u *\<^sub>R z)) \ exp \Im z\" .  lp15@59746  770 qed  lp15@59862  771 lp15@59862  772 lemma Taylor_sin:  lp15@59862  773  "norm(sin z - (\k\n. complex_of_real (sin_coeff k) * z ^ k))  lp15@59746  774  \ exp\Im z\ * (norm z) ^ (Suc n) / (fact n)"  lp15@59746  775 proof -  lp15@59746  776  have mono: "\u w z::real. w \ u \ z \ u \ w + z \ u*2"  lp15@59746  777  by arith  lp15@59746  778  have *: "cmod (sin z -  lp15@59746  779  (\i\n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))  lp15@59862  780  \ exp \Im z\ * cmod z ^ Suc n / (fact n)"  nipkow@69529  781  proof (rule complex_Taylor [of "closed_segment 0 z" n  lp15@61609  782  "\k x. (-1)^(k div 2) * (if even k then sin x else cos x)"  lp15@60162  783  "exp\Im z\" 0 z, simplified])  lp15@59746  784  fix k x  lp15@59746  785  show "((\x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative  lp15@59746  786  (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))  lp15@59746  787  (at x within closed_segment 0 z)"  lp15@59746  788  apply (auto simp: power_Suc)  lp15@59746  789  apply (intro derivative_eq_intros | simp)+  lp15@59746  790  done  lp15@59746  791  next  lp15@59746  792  fix x  lp15@59746  793  assume "x \ closed_segment 0 z"  lp15@59746  794  then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \ exp \Im z\"  lp15@59746  795  by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)  lp15@59862  796  qed  lp15@59746  797  have **: "\k. complex_of_real (sin_coeff k) * z ^ k  lp15@59746  798  = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"  lp15@59746  799  by (auto simp: sin_coeff_def elim!: oddE)  lp15@59746  800  show ?thesis  lp15@59746  801  apply (rule order_trans [OF _ *])  lp15@59746  802  apply (simp add: **)  lp15@59746  803  done  lp15@59746  804 qed  lp15@59746  805 lp15@59862  806 lemma Taylor_cos:  lp15@59862  807  "norm(cos z - (\k\n. complex_of_real (cos_coeff k) * z ^ k))  lp15@59746  808  \ exp\Im z\ * (norm z) ^ Suc n / (fact n)"  lp15@59746  809 proof -  lp15@59746  810  have mono: "\u w z::real. w \ u \ z \ u \ w + z \ u*2"  lp15@59746  811  by arith  lp15@59746  812  have *: "cmod (cos z -  lp15@59746  813  (\i\n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))  lp15@59862  814  \ exp \Im z\ * cmod z ^ Suc n / (fact n)"  nipkow@69529  815  proof (rule complex_Taylor [of "closed_segment 0 z" n "\k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\Im z\" 0 z,  lp15@59746  816 simplified])  lp15@59746  817  fix k x  lp15@59746  818  assume "x \ closed_segment 0 z" "k \ n"  lp15@59746  819  show "((\x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative  lp15@59746  820  (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))  lp15@59746  821  (at x within closed_segment 0 z)"  lp15@59746  822  apply (auto simp: power_Suc)  lp15@59746  823  apply (intro derivative_eq_intros | simp)+  lp15@59746  824  done  lp15@59746  825  next  lp15@59746  826  fix x  lp15@59746  827  assume "x \ closed_segment 0 z"  lp15@59746  828  then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \ exp \Im z\"  lp15@59746  829  by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)  lp15@59862  830  qed  lp15@59746  831  have **: "\k. complex_of_real (cos_coeff k) * z ^ k  lp15@59746  832  = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"  lp15@59746  833  by (auto simp: cos_coeff_def elim!: evenE)  lp15@59746  834  show ?thesis  lp15@59746  835  apply (rule order_trans [OF _ *])  lp15@59746  836  apply (simp add: **)  lp15@59746  837  done  lp15@59746  838 qed  lp15@59746  839 lp15@60162  840 declare power_Suc [simp]  lp15@59746  841 wenzelm@60420  842 text\32-bit Approximation to e\  wenzelm@61945  843 lemma e_approx_32: "\exp(1) - 5837465777 / 2147483648\ \ (inverse(2 ^ 32)::real)"  lp15@59751  844  using Taylor_exp [of 1 14] exp_le  nipkow@64267  845  apply (simp add: sum_distrib_right in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)  nipkow@66611  846  apply (simp only: pos_le_divide_eq [symmetric])  lp15@59751  847  done  lp15@59751  848 lp15@65719  849 lemma e_less_272: "exp 1 < (272/100::real)"  lp15@60017  850  using e_approx_32  nipkow@62390  851  by (simp add: abs_if split: if_split_asm)  lp15@60017  852 lp15@65719  853 lemma ln_272_gt_1: "ln (272/100) > (1::real)"  lp15@65719  854  by (metis e_less_272 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)  lp15@65719  855 lp15@65719  856 text\Apparently redundant. But many arguments involve integers.\  lp15@60017  857 lemma ln3_gt_1: "ln 3 > (1::real)"  lp15@65719  858  by (simp add: less_trans [OF ln_272_gt_1])  lp15@60017  859 lp15@68499  860 subsection\The argument of a complex number (HOL Light version)\  lp15@68499  861 eberlm@69180  862 definition%important is_Arg :: "[complex,real] \ bool"  lp15@68499  863  where "is_Arg z r \ z = of_real(norm z) * exp(\ * of_real r)"  lp15@68499  864 eberlm@69180  865 definition%important Arg2pi :: "complex \ real"  lp15@68499  866  where "Arg2pi z \ if z = 0 then 0 else THE t. 0 \ t \ t < 2*pi \ is_Arg z t"  lp15@68499  867 lp15@68517  868 lemma is_Arg_2pi_iff: "is_Arg z (r + of_int k * (2 * pi)) \ is_Arg z r"  lp15@68517  869  by (simp add: algebra_simps is_Arg_def)  lp15@68517  870 lp15@68517  871 lemma is_Arg_eqI:  lp15@68517  872  assumes r: "is_Arg z r" and s: "is_Arg z s" and rs: "abs (r-s) < 2*pi" and "z \ 0"  lp15@68517  873  shows "r = s"  lp15@68517  874 proof -  lp15@68517  875  have zr: "z = (cmod z) * exp (\ * r)" and zs: "z = (cmod z) * exp (\ * s)"  lp15@68517  876  using r s by (auto simp: is_Arg_def)  lp15@68517  877  with \z \ 0\ have eq: "exp (\ * r) = exp (\ * s)"  lp15@68517  878  by (metis mult_eq_0_iff vector_space_over_itself.scale_left_imp_eq)  lp15@68517  879  have "\ * r = \ * s"  lp15@68517  880  by (rule exp_complex_eqI) (use rs in \auto simp: eq exp_complex_eqI\)  lp15@68517  881  then show ?thesis  lp15@68517  882  by simp  lp15@68517  883 qed  lp15@68517  884 lp15@68499  885 text\This function returns the angle of a complex number from its representation in polar coordinates.  lp15@68499  886 Due to periodicity, its range is arbitrary. @{term Arg2pi} follows HOL Light in adopting the interval $[0,2\pi)$.  lp15@68499  887 But we have the same periodicity issue with logarithms, and it is usual to adopt the same interval  lp15@68499  888 for the complex logarithm and argument functions. Further on down, we shall define both functions for the interval $(-\pi,\pi]$.  lp15@68499  889 The present version is provided for compatibility.\  lp15@59746  890 lp15@68493  891 lemma Arg2pi_0 [simp]: "Arg2pi(0) = 0"  lp15@68493  892  by (simp add: Arg2pi_def)  lp15@68493  893 lp15@68493  894 lemma Arg2pi_unique_lemma:  lp15@68499  895  assumes z: "is_Arg z t"  lp15@68499  896  and z': "is_Arg z t'"  lp15@59746  897  and t: "0 \ t" "t < 2*pi"  lp15@59746  898  and t': "0 \ t'" "t' < 2*pi"  lp15@59746  899  and nz: "z \ 0"  lp15@59746  900  shows "t' = t"  lp15@59746  901 proof -  lp15@59746  902  have [dest]: "\x y z::real. x\0 \ x+y < z \ y * of_real t') = of_real (cmod z) * exp (\ * of_real t)"  lp15@68499  905  by (metis z z' is_Arg_def)  lp15@59746  906  then have "exp (\ * of_real t') = exp (\ * of_real t)"  lp15@68499  907  by (metis nz mult_left_cancel mult_zero_left z is_Arg_def)  lp15@59746  908  then have "sin t' = sin t \ cos t' = cos t"  lp15@59746  909  apply (simp add: exp_Euler sin_of_real cos_of_real)  lp15@59746  910  by (metis Complex_eq complex.sel)  lp15@61609  911  then obtain n::int where n: "t' = t + 2 * n * pi"  lp15@59746  912  by (auto simp: sin_cos_eq_iff)  lp15@59746  913  then have "n=0"  lp15@68257  914  by (cases n) (use t t' in \auto simp: mult_less_0_iff algebra_simps\)  lp15@59746  915  then show "t' = t"  lp15@68257  916  by (simp add: n)  lp15@59746  917 qed  lp15@59746  918 lp15@68499  919 lemma Arg2pi: "0 \ Arg2pi z \ Arg2pi z < 2*pi \ is_Arg z (Arg2pi z)"  lp15@59746  920 proof (cases "z=0")  lp15@59746  921  case True then show ?thesis  lp15@68499  922  by (simp add: Arg2pi_def is_Arg_def)  lp15@59746  923 next  lp15@59746  924  case False  lp15@59746  925  obtain t where t: "0 \ t" "t < 2*pi"  lp15@59746  926  and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"  lp15@59746  927  using sincos_total_2pi [OF complex_unit_circle [OF False]]  lp15@59746  928  by blast  lp15@68499  929  have z: "is_Arg z t"  lp15@68499  930  unfolding is_Arg_def  lp15@59746  931  apply (rule complex_eqI)  lp15@59746  932  using t False ReIm  lp15@59746  933  apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)  lp15@59746  934  done  lp15@59746  935  show ?thesis  lp15@68493  936  apply (simp add: Arg2pi_def False)  lp15@59746  937  apply (rule theI [where a=t])  lp15@59746  938  using t z False  lp15@68493  939  apply (auto intro: Arg2pi_unique_lemma)  lp15@59746  940  done  lp15@59746  941 qed  lp15@59746  942 eberlm@69180  943 corollary%unimportant  lp15@68493  944  shows Arg2pi_ge_0: "0 \ Arg2pi z"  lp15@68493  945  and Arg2pi_lt_2pi: "Arg2pi z < 2*pi"  lp15@68493  946  and Arg2pi_eq: "z = of_real(norm z) * exp(\ * of_real(Arg2pi z))"  lp15@68499  947  using Arg2pi is_Arg_def by auto  lp15@68493  948 lp15@68493  949 lemma complex_norm_eq_1_exp: "norm z = 1 \ exp(\ * of_real (Arg2pi z)) = z"  lp15@68493  950  by (metis Arg2pi_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)  lp15@68493  951 lp15@68493  952 lemma Arg2pi_unique: "\of_real r * exp(\ * of_real a) = z; 0 < r; 0 \ a; a < 2*pi\ \ Arg2pi z = a"  lp15@68499  953  by (rule Arg2pi_unique_lemma [unfolded is_Arg_def, OF _ Arg2pi_eq]) (use Arg2pi [of z] in \auto simp: norm_mult\)  lp15@68493  954 lp15@68493  955 lemma Arg2pi_minus: "z \ 0 \ Arg2pi (-z) = (if Arg2pi z < pi then Arg2pi z + pi else Arg2pi z - pi)"  lp15@68493  956  apply (rule Arg2pi_unique [of "norm z"])  lp15@59746  957  apply (rule complex_eqI)  lp15@68493  958  using Arg2pi_ge_0 [of z] Arg2pi_eq [of z] Arg2pi_lt_2pi [of z]  lp15@59746  959  apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])  lp15@59746  960  apply (metis Re_rcis Im_rcis rcis_def)+  lp15@59746  961  done  lp15@59746  962 lp15@68493  963 lemma Arg2pi_times_of_real [simp]:  lp15@68493  964  assumes "0 < r" shows "Arg2pi (of_real r * z) = Arg2pi z"  lp15@68257  965 proof (cases "z=0")  lp15@68257  966  case False  lp15@68257  967  show ?thesis  lp15@68499  968  by (rule Arg2pi_unique [of "r * norm z"]) (use Arg2pi False assms is_Arg_def in auto)  lp15@68257  969 qed auto  lp15@59746  970 lp15@68493  971 lemma Arg2pi_times_of_real2 [simp]: "0 < r \ Arg2pi (z * of_real r) = Arg2pi z"  lp15@68493  972  by (metis Arg2pi_times_of_real mult.commute)  lp15@68493  973 lp15@68493  974 lemma Arg2pi_divide_of_real [simp]: "0 < r \ Arg2pi (z / of_real r) = Arg2pi z"  lp15@68493  975  by (metis Arg2pi_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)  lp15@68493  976 lp15@68493  977 lemma Arg2pi_le_pi: "Arg2pi z \ pi \ 0 \ Im z"  lp15@59746  978 proof (cases "z=0")  lp15@59746  979  case False  lp15@68493  980  have "0 \ Im z \ 0 \ Im (of_real (cmod z) * exp (\ * complex_of_real (Arg2pi z)))"  lp15@68493  981  by (metis Arg2pi_eq)  lp15@68493  982  also have "... = (0 \ Im (exp (\ * complex_of_real (Arg2pi z))))"  lp15@68257  983  using False by (simp add: zero_le_mult_iff)  lp15@68493  984  also have "... \ Arg2pi z \ pi"  lp15@68493  985  by (simp add: Im_exp) (metis Arg2pi_ge_0 Arg2pi_lt_2pi sin_lt_zero sin_ge_zero not_le)  lp15@59746  986  finally show ?thesis  lp15@59746  987  by blast  lp15@68257  988 qed auto  lp15@59746  989 lp15@68493  990 lemma Arg2pi_lt_pi: "0 < Arg2pi z \ Arg2pi z < pi \ 0 < Im z"  lp15@59746  991 proof (cases "z=0")  lp15@59746  992  case False  lp15@68493  993  have "0 < Im z \ 0 < Im (of_real (cmod z) * exp (\ * complex_of_real (Arg2pi z)))"  lp15@68493  994  by (metis Arg2pi_eq)  lp15@68493  995  also have "... = (0 < Im (exp (\ * complex_of_real (Arg2pi z))))"  lp15@68257  996  using False by (simp add: zero_less_mult_iff)  lp15@68493  997  also have "... \ 0 < Arg2pi z \ Arg2pi z < pi"  lp15@68493  998  using Arg2pi_ge_0 Arg2pi_lt_2pi sin_le_zero sin_gt_zero  lp15@59746  999  apply (auto simp: Im_exp)  lp15@59746  1000  using le_less apply fastforce  lp15@59746  1001  using not_le by blast  lp15@59746  1002  finally show ?thesis  lp15@59746  1003  by blast  lp15@68257  1004 qed auto  lp15@59746  1005 lp15@68493  1006 lemma Arg2pi_eq_0: "Arg2pi z = 0 \ z \ \ \ 0 \ Re z"  lp15@59746  1007 proof (cases "z=0")  lp15@59746  1008  case False  lp15@68493  1009  have "z \ \ \ 0 \ Re z \ z \ \ \ 0 \ Re (of_real (cmod z) * exp (\ * complex_of_real (Arg2pi z)))"  lp15@68493  1010  by (metis Arg2pi_eq)  lp15@68493  1011  also have "... \ z \ \ \ 0 \ Re (exp (\ * complex_of_real (Arg2pi z)))"  lp15@68257  1012  using False by (simp add: zero_le_mult_iff)  lp15@68493  1013  also have "... \ Arg2pi z = 0"  lp15@68257  1014  proof -  lp15@68493  1015  have [simp]: "Arg2pi z = 0 \ z \ \"  lp15@68493  1016  using Arg2pi_eq [of z] by (auto simp: Reals_def)  lp15@68493  1017  moreover have "\z \ \; 0 \ cos (Arg2pi z)\ \ Arg2pi z = 0"  lp15@68493  1018  by (metis Arg2pi_lt_pi Arg2pi_ge_0 Arg2pi_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)  lp15@68257  1019  ultimately show ?thesis  lp15@68257  1020  by (auto simp: Re_exp)  lp15@68257  1021  qed  lp15@59746  1022  finally show ?thesis  lp15@59746  1023  by blast  lp15@68257  1024 qed auto  lp15@59746  1025 eberlm@69180  1026 corollary%unimportant Arg2pi_gt_0:  lp15@68499  1027  assumes "z \ \\<^sub>\\<^sub>0"  lp15@68493  1028  shows "Arg2pi z > 0"  lp15@68499  1029  using Arg2pi_eq_0 Arg2pi_ge_0 assms dual_order.strict_iff_order  lp15@68499  1030  unfolding nonneg_Reals_def by fastforce  lp15@68493  1031 lp15@68493  1032 lemma Arg2pi_eq_pi: "Arg2pi z = pi \ z \ \ \ Re z < 0"  lp15@68499  1033  using Arg2pi_le_pi [of z] Arg2pi_lt_pi [of z] Arg2pi_eq_0 [of z] Arg2pi_ge_0 [of z]  lp15@68499  1034  by (fastforce simp: complex_is_Real_iff)  lp15@68493  1035 lp15@68493  1036 lemma Arg2pi_eq_0_pi: "Arg2pi z = 0 \ Arg2pi z = pi \ z \ \"  lp15@68493  1037  using Arg2pi_eq_0 Arg2pi_eq_pi not_le by auto  lp15@68493  1038 lp15@68517  1039 lemma Arg2pi_of_real: "Arg2pi (of_real r) = (if r<0 then pi else 0)"  lp15@68517  1040  using Arg2pi_eq_0_pi Arg2pi_eq_pi by fastforce  lp15@68517  1041 lp15@68499  1042 lemma Arg2pi_real: "z \ \ \ Arg2pi z = (if 0 \ Re z then 0 else pi)"  lp15@68499  1043  using Arg2pi_eq_0 Arg2pi_eq_0_pi by auto  lp15@68499  1044 lp15@68499  1045 lemma Arg2pi_inverse: "Arg2pi(inverse z) = (if z \ \ then Arg2pi z else 2*pi - Arg2pi z)"  lp15@68257  1046 proof (cases "z=0")  lp15@68257  1047  case False  lp15@68257  1048  show ?thesis  lp15@68493  1049  apply (rule Arg2pi_unique [of "inverse (norm z)"])  lp15@68499  1050  using Arg2pi_eq False Arg2pi_ge_0 [of z] Arg2pi_lt_2pi [of z] Arg2pi_eq_0 [of z]  lp15@68499  1051  by (auto simp: Arg2pi_real in_Reals_norm exp_diff field_simps)  lp15@68257  1052 qed auto  lp15@59746  1053 lp15@68493  1054 lemma Arg2pi_eq_iff:  lp15@59746  1055  assumes "w \ 0" "z \ 0"  lp15@68493  1056  shows "Arg2pi w = Arg2pi z \ (\x. 0 < x & w = of_real x * z)"  lp15@68493  1057  using assms Arg2pi_eq [of z] Arg2pi_eq [of w]  lp15@59746  1058  apply auto  lp15@59746  1059  apply (rule_tac x="norm w / norm z" in exI)  lp15@59746  1060  apply (simp add: divide_simps)  lp15@59746  1061  by (metis mult.commute mult.left_commute)  lp15@59746  1062 lp15@68493  1063 lemma Arg2pi_inverse_eq_0: "Arg2pi(inverse z) = 0 \ Arg2pi z = 0"  lp15@68493  1064  by (metis Arg2pi_eq_0 Arg2pi_inverse inverse_inverse_eq)  lp15@68493  1065 lp15@68493  1066 lemma Arg2pi_divide:  lp15@68493  1067  assumes "w \ 0" "z \ 0" "Arg2pi w \ Arg2pi z"  lp15@68493  1068  shows "Arg2pi(z / w) = Arg2pi z - Arg2pi w"  lp15@68493  1069  apply (rule Arg2pi_unique [of "norm(z / w)"])  lp15@68493  1070  using assms Arg2pi_eq Arg2pi_ge_0 [of w] Arg2pi_lt_2pi [of z]  lp15@68257  1071  apply (auto simp: exp_diff norm_divide field_simps)  lp15@59746  1072  done  lp15@59746  1073 lp15@68493  1074 lemma Arg2pi_le_div_sum:  lp15@68493  1075  assumes "w \ 0" "z \ 0" "Arg2pi w \ Arg2pi z"  lp15@68493  1076  shows "Arg2pi z = Arg2pi w + Arg2pi(z / w)"  lp15@68493  1077  by (simp add: Arg2pi_divide assms)  lp15@68493  1078 lp15@68493  1079 lemma Arg2pi_le_div_sum_eq:  lp15@59746  1080  assumes "w \ 0" "z \ 0"  lp15@68493  1081  shows "Arg2pi w \ Arg2pi z \ Arg2pi z = Arg2pi w + Arg2pi(z / w)"  lp15@68493  1082  using assms by (auto simp: Arg2pi_ge_0 intro: Arg2pi_le_div_sum)  lp15@68493  1083 lp15@68493  1084 lemma Arg2pi_diff:  lp15@59746  1085  assumes "w \ 0" "z \ 0"  lp15@68493  1086  shows "Arg2pi w - Arg2pi z = (if Arg2pi z \ Arg2pi w then Arg2pi(w / z) else Arg2pi(w/z) - 2*pi)"  lp15@68499  1087  using assms Arg2pi_divide Arg2pi_inverse [of "w/z"] Arg2pi_eq_0_pi  lp15@68499  1088  by (force simp add: Arg2pi_ge_0 Arg2pi_divide not_le split: if_split_asm)  lp15@68493  1089 lp15@68493  1090 lemma Arg2pi_add:  lp15@59746  1091  assumes "w \ 0" "z \ 0"  lp15@68493  1092  shows "Arg2pi w + Arg2pi z = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi(w * z) else Arg2pi(w * z) + 2*pi)"  lp15@68493  1093  using assms Arg2pi_diff [of "w*z" z] Arg2pi_le_div_sum_eq [of z "w*z"]  lp15@68493  1094  apply (auto simp: Arg2pi_ge_0 Arg2pi_divide not_le)  lp15@68493  1095  apply (metis Arg2pi_lt_2pi add.commute)  lp15@68493  1096  apply (metis (no_types) Arg2pi add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)  lp15@59746  1097  done  lp15@59746  1098 lp15@68493  1099 lemma Arg2pi_times:  lp15@59746  1100  assumes "w \ 0" "z \ 0"  lp15@68493  1101  shows "Arg2pi (w * z) = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi w + Arg2pi z  lp15@68493  1102  else (Arg2pi w + Arg2pi z) - 2*pi)"  lp15@68493  1103  using Arg2pi_add [OF assms]  lp15@59746  1104  by auto  lp15@59746  1105 lp15@68493  1106 lemma Arg2pi_cnj_eq_inverse: "z\0 \ Arg2pi (cnj z) = Arg2pi (inverse z)"  lp15@68493  1107  apply (simp add: Arg2pi_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)  lp15@68257  1108  by (metis of_real_power zero_less_norm_iff zero_less_power)  lp15@68257  1109 lp15@68499  1110 lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \ \ then Arg2pi z else 2*pi - Arg2pi z)"  lp15@68257  1111 proof (cases "z=0")  lp15@68257  1112  case False  lp15@68257  1113  then show ?thesis  lp15@68493  1114  by (simp add: Arg2pi_cnj_eq_inverse Arg2pi_inverse)  lp15@68257  1115 qed auto  lp15@59746  1116 lp15@68493  1117 lemma Arg2pi_exp: "0 \ Im z \ Im z < 2*pi \ Arg2pi(exp z) = Im z"  lp15@68493  1118  by (rule Arg2pi_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)  lp15@61762  1119 lp15@61762  1120 lemma complex_split_polar:  lp15@61762  1121  obtains r a::real where "z = complex_of_real r * (cos a + \ * sin a)" "0 \ r" "0 \ a" "a < 2*pi"  lp15@68499  1122  using Arg2pi cis.ctr cis_conv_exp unfolding Complex_eq is_Arg_def by fastforce  lp15@59751  1123 lp15@61806  1124 lemma Re_Im_le_cmod: "Im w * sin \ + Re w * cos \ \ cmod w"  lp15@61806  1125 proof (cases w rule: complex_split_polar)  lp15@61806  1126  case (1 r a) with sin_cos_le1 [of a \] show ?thesis  lp15@61806  1127  apply (simp add: norm_mult cmod_unit_one)  lp15@61806  1128  by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)  lp15@61806  1129 qed  lp15@61806  1130 eberlm@69180  1131 subsection%unimportant\Analytic properties of tangent function\  lp15@59751  1132 lp15@59751  1133 lemma cnj_tan: "cnj(tan z) = tan(cnj z)"  lp15@59751  1134  by (simp add: cnj_cos cnj_sin tan_def)  lp15@59751  1135 nipkow@69508  1136 lemma field_differentiable_at_tan: "cos z \ 0 \ tan field_differentiable at z"  lp15@62534  1137  unfolding field_differentiable_def  lp15@59751  1138  using DERIV_tan by blast  lp15@59751  1139 nipkow@69508  1140 lemma field_differentiable_within_tan: "cos z \ 0  lp15@62534  1141  \ tan field_differentiable (at z within s)"  lp15@62534  1142  using field_differentiable_at_tan field_differentiable_at_within by blast  lp15@59751  1143 nipkow@69508  1144 lemma continuous_within_tan: "cos z \ 0 \ continuous (at z within s) tan"  lp15@59751  1145  using continuous_at_imp_continuous_within isCont_tan by blast  lp15@59751  1146 nipkow@69508  1147 lemma continuous_on_tan [continuous_intros]: "(\z. z \ s \ cos z \ 0) \ continuous_on s tan"  lp15@59751  1148  by (simp add: continuous_at_imp_continuous_on)  lp15@59751  1149 nipkow@69508  1150 lemma holomorphic_on_tan: "(\z. z \ s \ cos z \ 0) \ tan holomorphic_on s"  lp15@62534  1151  by (simp add: field_differentiable_within_tan holomorphic_on_def)  lp15@59751  1152 lp15@59751  1153 eberlm@69180  1154 subsection\The principal branch of the Complex logarithm\  lp15@59751  1155 lp15@60020  1156 instantiation complex :: ln  lp15@60020  1157 begin  lp15@60017  1158 eberlm@69180  1159 definition%important ln_complex :: "complex \ complex"  lp15@60020  1160  where "ln_complex \ \z. THE w. exp w = z & -pi < Im(w) & Im(w) \ pi"  lp15@59751  1161 lp15@65585  1162 text\NOTE: within this scope, the constant Ln is not yet available!\  lp15@59751  1163 lemma  lp15@59751  1164  assumes "z \ 0"  lp15@60020  1165  shows exp_Ln [simp]: "exp(ln z) = z"  lp15@60020  1166  and mpi_less_Im_Ln: "-pi < Im(ln z)"  lp15@60020  1167  and Im_Ln_le_pi: "Im(ln z) \ pi"  lp15@59751  1168 proof -  lp15@59751  1169  obtain \ where z: "z / (cmod z) = Complex (cos \) (sin \)"  lp15@59751  1170  using complex_unimodular_polar [of "z / (norm z)"] assms  lp15@59751  1171  by (auto simp: norm_divide divide_simps)  lp15@59751  1172  obtain \ where \: "- pi < \" "\ \ pi" "sin \ = sin \" "cos \ = cos \"  lp15@59751  1173  using sincos_principal_value [of "\"] assms  lp15@59751  1174  by (auto simp: norm_divide divide_simps)  lp15@60020  1175  have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \ pi" unfolding ln_complex_def  lp15@59751  1176  apply (rule theI [where a = "Complex (ln(norm z)) \"])  lp15@59751  1177  using z assms \  lp15@61762  1178  apply (auto simp: field_simps exp_complex_eqI exp_eq_polar cis.code)  lp15@59751  1179  done  lp15@60020  1180  then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \ pi"  lp15@59751  1181  by auto  lp15@59751  1182 qed  lp15@59751  1183 lp15@59751  1184 lemma Ln_exp [simp]:  lp15@59751  1185  assumes "-pi < Im(z)" "Im(z) \ pi"  lp15@60020  1186  shows "ln(exp z) = z"  lp15@59751  1187  apply (rule exp_complex_eqI)  lp15@59751  1188  using assms mpi_less_Im_Ln [of "exp z"] Im_Ln_le_pi [of "exp z"]  lp15@59751  1189  apply auto  lp15@59751  1190  done  lp15@59751  1191 eberlm@69180  1192 subsection%unimportant\Relation to Real Logarithm\  lp15@60020  1193 lp15@60020  1194 lemma Ln_of_real:  lp15@60020  1195  assumes "0 < z"  lp15@60020  1196  shows "ln(of_real z::complex) = of_real(ln z)"  lp15@60020  1197 proof -  lp15@60020  1198  have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"  lp15@60020  1199  by (simp add: exp_of_real)  lp15@60020  1200  also have "... = of_real(ln z)"  lp15@68257  1201  using assms by (subst Ln_exp) auto  lp15@60020  1202  finally show ?thesis  lp15@60020  1203  using assms by simp  lp15@60020  1204 qed  lp15@60020  1205 eberlm@69180  1206 corollary%unimportant Ln_in_Reals [simp]: "z \ \ \ Re z > 0 \ ln z \ \"  lp15@60020  1207  by (auto simp: Ln_of_real elim: Reals_cases)  lp15@60020  1208 eberlm@69180  1209 corollary%unimportant Im_Ln_of_real [simp]: "r > 0 \ Im (ln (of_real r)) = 0"  lp15@60150  1210  by (simp add: Ln_of_real)  lp15@60150  1211 wenzelm@61070  1212 lemma cmod_Ln_Reals [simp]: "z \ \ \ 0 < Re z \ cmod (ln z) = norm (ln (Re z))"  lp15@60150  1213  using Ln_of_real by force  lp15@60150  1214 lp15@65719  1215 lemma Ln_Reals_eq: "\x \ \; Re x > 0\ \ ln x = of_real (ln (Re x))"  lp15@65719  1216  using Ln_of_real by force  lp15@65719  1217 lp15@65585  1218 lemma Ln_1 [simp]: "ln 1 = (0::complex)"  lp15@60020  1219 proof -  lp15@60020  1220  have "ln (exp 0) = (0::complex)"  lp15@68257  1221  by (simp add: del: exp_zero)  lp15@60020  1222  then show ?thesis  lp15@68493  1223  by simp  lp15@60020  1224 qed  lp15@60020  1225 lp15@68493  1226 lp15@65585  1227 lemma Ln_eq_zero_iff [simp]: "x \ \\<^sub>\\<^sub>0 \ ln x = 0 \ x = 1" for x::complex  lp15@65585  1228  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)  lp15@65585  1229 lp15@60020  1230 instance  lp15@60020  1231  by intro_classes (rule ln_complex_def Ln_1)  lp15@60020  1232 lp15@60020  1233 end  lp15@60020  1234 lp15@60020  1235 abbreviation Ln :: "complex \ complex"  lp15@60020  1236  where "Ln \ ln"  lp15@60020  1237 lp15@59751  1238 lemma Ln_eq_iff: "w \ 0 \ z \ 0 \ (Ln w = Ln z \ w = z)"  lp15@59751  1239  by (metis exp_Ln)  lp15@59751  1240 lp15@59751  1241 lemma Ln_unique: "exp(z) = w \ -pi < Im(z) \ Im(z) \ pi \ Ln w = z"  lp15@59751  1242  using Ln_exp by blast  lp15@59751  1243 lp15@59751  1244 lemma Re_Ln [simp]: "z \ 0 \ Re(Ln z) = ln(norm z)"  wenzelm@63092  1245  by (metis exp_Ln ln_exp norm_exp_eq_Re)  lp15@60150  1246 eberlm@69180  1247 corollary%unimportant ln_cmod_le:  lp15@60150  1248  assumes z: "z \ 0"  lp15@60150  1249  shows "ln (cmod z) \ cmod (Ln z)"  lp15@60150  1250  using norm_exp [of "Ln z", simplified exp_Ln [OF z]]  lp15@60150  1251  by (metis Re_Ln complex_Re_le_cmod z)  lp15@59751  1252 eberlm@69180  1253 proposition%unimportant exists_complex_root:  lp15@62843  1254  fixes z :: complex  lp15@62843  1255  assumes "n \ 0" obtains w where "z = w ^ n"  lp15@68257  1256 proof (cases "z=0")  lp15@68257  1257  case False  lp15@68257  1258  then show ?thesis  lp15@68257  1259  by (rule_tac w = "exp(Ln z / n)" in that) (simp add: assms exp_of_nat_mult [symmetric])  lp15@68257  1260 qed (use assms in auto)  lp15@59751  1261 eberlm@69180  1262 corollary%unimportant exists_complex_root_nonzero:  lp15@62843  1263  fixes z::complex  lp15@62843  1264  assumes "z \ 0" "n \ 0"  lp15@62843  1265  obtains w where "w \ 0" "z = w ^ n"  lp15@62843  1266  by (metis exists_complex_root [of n z] assms power_0_left)  lp15@62843  1267 eberlm@69180  1268 subsection%unimportant\Derivative of Ln away from the branch cut\  lp15@59751  1269 lp15@59751  1270 lemma  paulson@62131  1271  assumes "z \ \\<^sub>\\<^sub>0"  lp15@59751  1272  shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"  lp15@59751  1273  and Im_Ln_less_pi: "Im (Ln z) < pi"  lp15@59751  1274 proof -  lp15@59751  1275  have znz: "z \ 0"  lp15@59751  1276  using assms by auto  paulson@62131  1277  then have "Im (Ln z) \ pi"  paulson@62131  1278  by (metis (no_types) Im_exp Ln_in_Reals assms complex_nonpos_Reals_iff complex_is_Real_iff exp_Ln mult_zero_right not_less pi_neq_zero sin_pi znz)  paulson@62131  1279  then show *: "Im (Ln z) < pi" using assms Im_Ln_le_pi  paulson@62131  1280  by (simp add: le_neq_trans znz)  lp15@62534  1281  have "(exp has_field_derivative z) (at (Ln z))"  lp15@62534  1282  by (metis znz DERIV_exp exp_Ln)  lp15@62534  1283  then show "(Ln has_field_derivative inverse(z)) (at z)"  lp15@68255  1284  apply (rule has_field_derivative_inverse_strong_x  lp15@68255  1285  [where S = "{w. -pi < Im(w) \ Im(w) < pi}"])  lp15@59751  1286  using znz *  lp15@68255  1287  apply (auto simp: continuous_on_exp [OF continuous_on_id] open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt mpi_less_Im_Ln)  lp15@59751  1288  done  lp15@59751  1289 qed  lp15@59751  1290 lp15@59751  1291 declare has_field_derivative_Ln [derivative_intros]  lp15@59751  1292 declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]  lp15@59751  1293 lp15@62534  1294 lemma field_differentiable_at_Ln: "z \ \\<^sub>\\<^sub>0 \ Ln field_differentiable at z"  lp15@62534  1295  using field_differentiable_def has_field_derivative_Ln by blast  lp15@62534  1296 lp15@62534  1297 lemma field_differentiable_within_Ln: "z \ \\<^sub>\\<^sub>0  lp15@67371  1298  \ Ln field_differentiable (at z within S)"  lp15@62534  1299  using field_differentiable_at_Ln field_differentiable_within_subset by blast  lp15@59751  1300 paulson@62131  1301 lemma continuous_at_Ln: "z \ \\<^sub>\\<^sub>0 \ continuous (at z) Ln"  lp15@62534  1302  by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Ln)  lp15@59751  1303 lp15@59862  1304 lemma isCont_Ln' [simp]:  paulson@62131  1305  "\isCont f z; f z \ \\<^sub>\\<^sub>0\ \ isCont (\x. Ln (f x)) z"  lp15@59862  1306  by (blast intro: isCont_o2 [OF _ continuous_at_Ln])  lp15@59862  1307 lp15@67371  1308 lemma continuous_within_Ln: "z \ \\<^sub>\\<^sub>0 \ continuous (at z within S) Ln"  lp15@59751  1309  using continuous_at_Ln continuous_at_imp_continuous_within by blast  lp15@59751  1310 lp15@67371  1311 lemma continuous_on_Ln [continuous_intros]: "(\z. z \ S \ z \ \\<^sub>\\<^sub>0) \ continuous_on S Ln"  lp15@59751  1312  by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)  lp15@59751  1313 lp15@68493  1314 lemma continuous_on_Ln' [continuous_intros]:  lp15@67371  1315  "continuous_on S f \ (\z. z \ S \ f z \ \\<^sub>\\<^sub>0) \ continuous_on S (\x. Ln (f x))"  lp15@67371  1316  by (rule continuous_on_compose2[OF continuous_on_Ln, of "UNIV - nonpos_Reals" S f]) auto  lp15@67371  1317 lp15@67371  1318 lemma holomorphic_on_Ln [holomorphic_intros]: "(\z. z \ S \ z \ \\<^sub>\\<^sub>0) \ Ln holomorphic_on S"  lp15@62534  1319  by (simp add: field_differentiable_within_Ln holomorphic_on_def)  lp15@59751  1320 eberlm@68721  1321 lemma holomorphic_on_Ln' [holomorphic_intros]:  eberlm@68721  1322  "(\z. z \ A \ f z \ \\<^sub>\\<^sub>0) \ f holomorphic_on A \ (\z. Ln (f z)) holomorphic_on A"  eberlm@68721  1323  using holomorphic_on_compose_gen[OF _ holomorphic_on_Ln, of f A "- \\<^sub>\\<^sub>0"]  eberlm@68721  1324  by (auto simp: o_def)  eberlm@68721  1325 lp15@67371  1326 lemma tendsto_Ln [tendsto_intros]:  lp15@67371  1327  fixes L F  lp15@67371  1328  assumes "(f \ L) F" "L \ \\<^sub>\\<^sub>0"  lp15@67371  1329  shows "((\x. Ln (f x)) \ Ln L) F"  lp15@67371  1330 proof -  lp15@67371  1331  have "nhds L \ filtermap f F"  lp15@67371  1332  using assms(1) by (simp add: filterlim_def)  lp15@67371  1333  moreover have "\\<^sub>F y in nhds L. y \ - \\<^sub>\\<^sub>0"  lp15@67371  1334  using eventually_nhds_in_open[of "- \\<^sub>\\<^sub>0" L] assms by (auto simp: open_Compl)  lp15@67371  1335  ultimately have "\\<^sub>F y in filtermap f F. y \ - \\<^sub>\\<^sub>0" by (rule filter_leD)  lp15@67371  1336  moreover have "continuous_on (-\\<^sub>\\<^sub>0) Ln" by (rule continuous_on_Ln) auto  lp15@67371  1337  ultimately show ?thesis using continuous_on_tendsto_compose[of "- \\<^sub>\\<^sub>0" Ln f L F] assms  lp15@67371  1338  by (simp add: eventually_filtermap)  lp15@67371  1339 qed  lp15@67371  1340 lp15@65719  1341 lemma divide_ln_mono:  lp15@65719  1342  fixes x y::real  lp15@65719  1343  assumes "3 \ x" "x \ y"  lp15@65719  1344  shows "x / ln x \ y / ln y"  lp15@65719  1345 proof (rule exE [OF complex_mvt_line [of x y "\z. z / Ln z" "\z. 1/(Ln z) - 1/(Ln z)^2"]];  lp15@65719  1346  clarsimp simp add: closed_segment_Reals closed_segment_eq_real_ivl assms)  lp15@65719  1347  show "\u. \x \ u; u \ y\ \ ((\z. z / Ln z) has_field_derivative 1 / Ln u - 1 / (Ln u)\<^sup>2) (at u)"  lp15@68257  1348  using \3 \ x\ by (force intro!: derivative_eq_intros simp: field_simps power_eq_if)  lp15@65719  1349  show "x / ln x \ y / ln y"  lp15@65719  1350  if "Re (y / Ln y) - Re (x / Ln x) = (Re (1 / Ln u) - Re (1 / (Ln u)\<^sup>2)) * (y - x)"  lp15@65719  1351  and x: "x \ u" "u \ y" for u  lp15@65719  1352  proof -  lp15@65719  1353  have eq: "y / ln y = (1 / ln u - 1 / (ln u)\<^sup>2) * (y - x) + x / ln x"  lp15@65719  1354  using that \3 \ x\ by (auto simp: Ln_Reals_eq in_Reals_norm group_add_class.diff_eq_eq)  lp15@65719  1355  show ?thesis  lp15@65719  1356  using exp_le \3 \ x\ x by (simp add: eq) (simp add: power_eq_if divide_simps ln_ge_iff)  lp15@65719  1357  qed  lp15@65719  1358 qed  lp15@68493  1359 eberlm@69180  1360 theorem Ln_series:  eberlm@69180  1361  fixes z :: complex  eberlm@69180  1362  assumes "norm z < 1"  eberlm@69180  1363  shows "(\n. (-1)^Suc n / of_nat n * z^n) sums ln (1 + z)" (is "(\n. ?f n * z^n) sums _")  eberlm@69180  1364 proof -  eberlm@69180  1365  let ?F = "\z. \n. ?f n * z^n" and ?F' = "\z. \n. diffs ?f n * z^n"  eberlm@69180  1366  have r: "conv_radius ?f = 1"  eberlm@69180  1367  by (intro conv_radius_ratio_limit_nonzero[of _ 1])  eberlm@69180  1368  (simp_all add: norm_divide LIMSEQ_Suc_n_over_n del: of_nat_Suc)  eberlm@69180  1369 eberlm@69180  1370  have "\c. \z\ball 0 1. ln (1 + z) - ?F z = c"  eberlm@69180  1371  proof (rule has_field_derivative_zero_constant)  eberlm@69180  1372  fix z :: complex assume z': "z \ ball 0 1"  eberlm@69180  1373  hence z: "norm z < 1" by simp  eberlm@69180  1374  define t :: complex where "t = of_real (1 + norm z) / 2"  eberlm@69180  1375  from z have t: "norm z < norm t" "norm t < 1" unfolding t_def  eberlm@69180  1376  by (simp_all add: field_simps norm_divide del: of_real_add)  eberlm@69180  1377 eberlm@69180  1378  have "Re (-z) \ norm (-z)" by (rule complex_Re_le_cmod)  eberlm@69180  1379  also from z have "... < 1" by simp  eberlm@69180  1380  finally have "((\z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)"  eberlm@69180  1381  by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)  eberlm@69180  1382  moreover have "(?F has_field_derivative ?F' z) (at z)" using t r  eberlm@69180  1383  by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all  eberlm@69180  1384  ultimately have "((\z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))  eberlm@69180  1385  (at z within ball 0 1)"  eberlm@69180  1386  by (intro derivative_intros) (simp_all add: at_within_open[OF z'])  eberlm@69180  1387  also have "(\n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r  eberlm@69180  1388  by (intro diffs_equiv termdiff_converges[OF t(1)] summable_in_conv_radius) simp_all  eberlm@69180  1389  from sums_split_initial_segment[OF this, of 1]  eberlm@69180  1390  have "(\i. (-z) ^ i) sums ?F' z" by (simp add: power_minus[of z] del: of_nat_Suc)  eberlm@69180  1391  hence "?F' z = inverse (1 + z)" using z by (simp add: sums_iff suminf_geometric divide_inverse)  eberlm@69180  1392  also have "inverse (1 + z) - inverse (1 + z) = 0" by simp  eberlm@69180  1393  finally show "((\z. ln (1 + z) - ?F z) has_field_derivative 0) (at z within ball 0 1)" .  eberlm@69180  1394  qed simp_all  eberlm@69180  1395  then obtain c where c: "\z. z \ ball 0 1 \ ln (1 + z) - ?F z = c" by blast  eberlm@69180  1396  from c[of 0] have "c = 0" by (simp only: powser_zero) simp  eberlm@69180  1397  with c[of z] assms have "ln (1 + z) = ?F z" by simp  eberlm@69180  1398  moreover have "summable (\n. ?f n * z^n)" using assms r  eberlm@69180  1399  by (intro summable_in_conv_radius) simp_all  eberlm@69180  1400  ultimately show ?thesis by (simp add: sums_iff)  eberlm@69180  1401 qed  eberlm@69180  1402 eberlm@69180  1403 lemma Ln_series': "cmod z < 1 \ (\n. - ((-z)^n) / of_nat n) sums ln (1 + z)"  eberlm@69180  1404  by (drule Ln_series) (simp add: power_minus')  eberlm@69180  1405 eberlm@69180  1406 lemma ln_series':  eberlm@69180  1407  assumes "abs (x::real) < 1"  eberlm@69180  1408  shows "(\n. - ((-x)^n) / of_nat n) sums ln (1 + x)"  eberlm@69180  1409 proof -  eberlm@69180  1410  from assms have "(\n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"  eberlm@69180  1411  by (intro Ln_series') simp_all  eberlm@69180  1412  also have "(\n. - ((-of_real x)^n) / of_nat n) = (\n. complex_of_real (- ((-x)^n) / of_nat n))"  eberlm@69180  1413  by (rule ext) simp  eberlm@69180  1414  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"  eberlm@69180  1415  by (subst Ln_of_real [symmetric]) simp_all  eberlm@69180  1416  finally show ?thesis by (subst (asm) sums_of_real_iff)  eberlm@69180  1417 qed  eberlm@69180  1418 eberlm@69180  1419 lemma Ln_approx_linear:  eberlm@69180  1420  fixes z :: complex  eberlm@69180  1421  assumes "norm z < 1"  eberlm@69180  1422  shows "norm (ln (1 + z) - z) \ norm z^2 / (1 - norm z)"  eberlm@69180  1423 proof -  eberlm@69180  1424  let ?f = "\n. (-1)^Suc n / of_nat n"  eberlm@69180  1425  from assms have "(\n. ?f n * z^n) sums ln (1 + z)" using Ln_series by simp  eberlm@69180  1426  moreover have "(\n. (if n = 1 then 1 else 0) * z^n) sums z" using powser_sums_if[of 1] by simp  eberlm@69180  1427  ultimately have "(\n. (?f n - (if n = 1 then 1 else 0)) * z^n) sums (ln (1 + z) - z)"  eberlm@69180  1428  by (subst left_diff_distrib, intro sums_diff) simp_all  eberlm@69180  1429  from sums_split_initial_segment[OF this, of "Suc 1"]  eberlm@69180  1430  have "(\i. (-(z^2)) * inverse (2 + of_nat i) * (- z)^i) sums (Ln (1 + z) - z)"  eberlm@69180  1431  by (simp add: power2_eq_square mult_ac power_minus[of z] divide_inverse)  eberlm@69180  1432  hence "(Ln (1 + z) - z) = (\i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)"  eberlm@69180  1433  by (simp add: sums_iff)  eberlm@69180  1434  also have A: "summable (\n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"  eberlm@69180  1435  by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])  eberlm@69180  1436  (auto simp: assms field_simps intro!: always_eventually)  eberlm@69180  1437  hence "norm (\i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i) \  eberlm@69180  1438  (\i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"  eberlm@69180  1439  by (intro summable_norm)  eberlm@69180  1440  (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)  eberlm@69180  1441  also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \ norm ((-z)^2 * (-z)^i) * 1" for i  eberlm@69180  1442  by (intro mult_left_mono) (simp_all add: divide_simps)  eberlm@69180  1443  hence "(\i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))  eberlm@69180  1444  \ (\i. norm (-(z^2) * (-z)^i))"  eberlm@69180  1445  using A assms  eberlm@69180  1446  apply (simp_all only: norm_power norm_inverse norm_divide norm_mult)  eberlm@69180  1447  apply (intro suminf_le summable_mult summable_geometric)  eberlm@69180  1448  apply (auto simp: norm_power field_simps simp del: of_nat_add of_nat_Suc)  eberlm@69180  1449  done  eberlm@69180  1450  also have "... = norm z^2 * (\i. norm z^i)" using assms  eberlm@69180  1451  by (subst suminf_mult [symmetric]) (auto intro!: summable_geometric simp: norm_mult norm_power)  eberlm@69180  1452  also have "(\i. norm z^i) = inverse (1 - norm z)" using assms  eberlm@69180  1453  by (subst suminf_geometric) (simp_all add: divide_inverse)  eberlm@69180  1454  also have "norm z^2 * ... = norm z^2 / (1 - norm z)" by (simp add: divide_inverse)  eberlm@69180  1455  finally show ?thesis .  eberlm@69180  1456 qed  eberlm@69180  1457 eberlm@69180  1458 eberlm@69180  1459 subsection%unimportant\Quadrant-type results for Ln\  lp15@59751  1460 lp15@59751  1461 lemma cos_lt_zero_pi: "pi/2 < x \ x < 3*pi/2 \ cos x < 0"  lp15@59751  1462  using cos_minus_pi cos_gt_zero_pi [of "x-pi"]  lp15@59751  1463  by simp  lp15@59751  1464 lp15@59751  1465 lemma Re_Ln_pos_lt:  lp15@59751  1466  assumes "z \ 0"  wenzelm@61945  1467  shows "\Im(Ln z)\ < pi/2 \ 0 < Re(z)"  lp15@59751  1468 proof -  lp15@59751  1469  { fix w  lp15@59751  1470  assume "w = Ln z"  lp15@59751  1471  then have w: "Im w \ pi" "- pi < Im w"  lp15@59751  1472  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms  lp15@59751  1473  by auto  wenzelm@61945  1474  then have "\Im w\ < pi/2 \ 0 < Re(exp w)"  lp15@59751  1475  using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]  lp15@68257  1476  apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi abs_if split: if_split_asm)  lp15@68257  1477  apply (metis cos_minus cos_pi_half divide_minus_left less_irrefl linorder_neqE_linordered_idom nonzero_mult_div_cancel_right zero_neq_numeral)+  lp15@59751  1478  done  lp15@59751  1479  }  lp15@59751  1480  then show ?thesis using assms  lp15@59751  1481  by auto  lp15@59751  1482 qed  lp15@59751  1483 lp15@59751  1484 lemma Re_Ln_pos_le:  lp15@59751  1485  assumes "z \ 0"  wenzelm@61945  1486  shows "\Im(Ln z)\ \ pi/2 \ 0 \ Re(z)"  lp15@59751  1487 proof -  lp15@59751  1488  { fix w  lp15@59751  1489  assume "w = Ln z"  lp15@59751  1490  then have w: "Im w \ pi" "- pi < Im w"  lp15@59751  1491  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms  lp15@59751  1492  by auto  wenzelm@61945  1493  then have "\Im w\ \ pi/2 \ 0 \ Re(exp w)"  lp15@59751  1494  apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)  lp15@59751  1495  using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le  nipkow@62390  1496  apply (auto simp: abs_if split: if_split_asm)  lp15@59751  1497  done  lp15@59751  1498  }  lp15@59751  1499  then show ?thesis using assms  lp15@59751  1500  by auto  lp15@59751  1501 qed  lp15@59751  1502 lp15@59751  1503 lemma Im_Ln_pos_lt:  lp15@59751  1504  assumes "z \ 0"  lp15@59751  1505  shows "0 < Im(Ln z) \ Im(Ln z) < pi \ 0 < Im(z)"  lp15@59751  1506 proof -  lp15@59751  1507  { fix w  lp15@59751  1508  assume "w = Ln z"  lp15@59751  1509  then have w: "Im w \ pi" "- pi < Im w"  lp15@59751  1510  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms  lp15@59751  1511  by auto  lp15@59751  1512  then have "0 < Im w \ Im w < pi \ 0 < Im(exp w)"  lp15@59751  1513  using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"]  lp15@68257  1514  apply (simp add: Im_exp zero_less_mult_iff)  lp15@59751  1515  using less_linear apply fastforce  lp15@59751  1516  done  lp15@59751  1517  }  lp15@59751  1518  then show ?thesis using assms  lp15@59751  1519  by auto  lp15@59751  1520 qed  lp15@59751  1521 lp15@59751  1522 lemma Im_Ln_pos_le:  lp15@59751  1523  assumes "z \ 0"  lp15@59751  1524  shows "0 \ Im(Ln z) \ Im(Ln z) \ pi \ 0 \ Im(z)"  lp15@59751  1525 proof -  lp15@59751  1526  { fix w  lp15@59751  1527  assume "w = Ln z"  lp15@59751  1528  then have w: "Im w \ pi" "- pi < Im w"  lp15@59751  1529  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms  lp15@59751  1530  by auto  lp15@59751  1531  then have "0 \ Im w \ Im w \ pi \ 0 \ Im(exp w)"  lp15@59751  1532  using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"]  lp15@59751  1533  apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero)  lp15@59751  1534  apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi)  lp15@59751  1535  done }  lp15@59751  1536  then show ?thesis using assms  lp15@59751  1537  by auto  lp15@59751  1538 qed  lp15@59751  1539 wenzelm@61945  1540 lemma Re_Ln_pos_lt_imp: "0 < Re(z) \ \Im(Ln z)\ < pi/2"  lp15@59751  1541  by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))  lp15@59751  1542 lp15@59751  1543 lemma Im_Ln_pos_lt_imp: "0 < Im(z) \ 0 < Im(Ln z) \ Im(Ln z) < pi"  lp15@59751  1544  by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))  lp15@59751  1545 paulson@62131  1546 text\A reference to the set of positive real numbers\  lp15@59751  1547 lemma Im_Ln_eq_0: "z \ 0 \ (Im(Ln z) = 0 \ 0 < Re(z) \ Im(z) = 0)"  lp15@62534  1548 by (metis Im_complex_of_real Im_exp Ln_in_Reals Re_Ln_pos_lt Re_Ln_pos_lt_imp  paulson@62131  1549  Re_complex_of_real complex_is_Real_iff exp_Ln exp_of_real pi_gt_zero)  lp15@59751  1550 lp15@59751  1551 lemma Im_Ln_eq_pi: "z \ 0 \ (Im(Ln z) = pi \ Re(z) < 0 \ Im(z) = 0)"  lp15@62534  1552 by (metis Im_Ln_eq_0 Im_Ln_pos_le Im_Ln_pos_lt add.left_neutral complex_eq less_eq_real_def  paulson@62131  1553  mult_zero_right not_less_iff_gr_or_eq pi_ge_zero pi_neq_zero rcis_zero_arg rcis_zero_mod)  lp15@59751  1554 lp15@59751  1555 eberlm@69180  1556 subsection%unimportant\More Properties of Ln\  lp15@59751  1557 lp15@68257  1558 lemma cnj_Ln: assumes "z \ \\<^sub>\\<^sub>0" shows "cnj(Ln z) = Ln(cnj z)"  lp15@68257  1559 proof (cases "z=0")  lp15@68257  1560  case False  lp15@68257  1561  show ?thesis  lp15@68257  1562  proof (rule exp_complex_eqI)  lp15@68257  1563  have "\Im (cnj (Ln z)) - Im (Ln (cnj z))\ \ \Im (cnj (Ln z))\ + \Im (Ln (cnj z))\"  lp15@68257  1564  by (rule abs_triangle_ineq4)  lp15@68257  1565  also have "... < pi + pi"  lp15@68257  1566  proof -  lp15@68257  1567  have "\Im (cnj (Ln z))\ < pi"  lp15@68257  1568  by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)  lp15@68257  1569  moreover have "\Im (Ln (cnj z))\ \ pi"  lp15@68493  1570  by (meson abs_le_iff complex_cnj_zero_iff less_eq_real_def minus_less_iff False Im_Ln_le_pi mpi_less_Im_Ln)  lp15@68257  1571  ultimately show ?thesis  lp15@68257  1572  by simp  lp15@68257  1573  qed  lp15@68257  1574  finally show "\Im (cnj (Ln z)) - Im (Ln (cnj z))\ < 2 * pi"  lp15@68257  1575  by simp  lp15@68257  1576  show "exp (cnj (Ln z)) = exp (Ln (cnj z))"  lp15@68257  1577  by (metis False complex_cnj_zero_iff exp_Ln exp_cnj)  lp15@68493  1578  qed  lp15@68257  1579 qed (use assms in auto)  lp15@68257  1580 lp15@68257  1581 lp15@68257  1582 lemma Ln_inverse: assumes "z \ \\<^sub>\\<^sub>0" shows "Ln(inverse z) = -(Ln z)"  lp15@68257  1583 proof (cases "z=0")  lp15@68257  1584  case False  lp15@68257  1585  show ?thesis  lp15@68257  1586  proof (rule exp_complex_eqI)  lp15@68257  1587  have "\Im (Ln (inverse z)) - Im (- Ln z)\ \ \Im (Ln (inverse z))\ + \Im (- Ln z)\"  lp15@68257  1588  by (rule abs_triangle_ineq4)  lp15@68257  1589  also have "... < pi + pi"  lp15@68257  1590  proof -  lp15@68257  1591  have "\Im (Ln (inverse z))\ < pi"  lp15@68257  1592  by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)  lp15@68257  1593  moreover have "\Im (- Ln z)\ \ pi"  lp15@68257  1594  using False Im_Ln_le_pi mpi_less_Im_Ln by fastforce  lp15@68257  1595  ultimately show ?thesis  lp15@68257  1596  by simp  lp15@68257  1597  qed  lp15@68493  1598  finally show "\Im (Ln (inverse z)) - Im (- Ln z)\ < 2 * pi"  lp15@68257  1599  by simp  lp15@68257  1600  show "exp (Ln (inverse z)) = exp (- Ln z)"  lp15@68257  1601  by (simp add: False exp_minus)  lp15@68493  1602  qed  lp15@68257  1603 qed (use assms in auto)  lp15@59751  1604 wenzelm@63589  1605 lemma Ln_minus1 [simp]: "Ln(-1) = \ * pi"  lp15@59751  1606  apply (rule exp_complex_eqI)  lp15@59751  1607  using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi  lp15@59751  1608  apply (auto simp: abs_if)  lp15@59751  1609  done  lp15@59751  1610 wenzelm@63589  1611 lemma Ln_ii [simp]: "Ln \ = \ * of_real pi/2"  wenzelm@63589  1612  using Ln_exp [of "\ * (of_real pi/2)"]  lp15@59751  1613  unfolding exp_Euler  lp15@59751  1614  by simp  lp15@59751  1615 wenzelm@63589  1616 lemma Ln_minus_ii [simp]: "Ln(-\) = - (\ * pi/2)"  lp15@59751  1617 proof -  wenzelm@63589  1618  have "Ln(-\) = Ln(inverse \)" by simp  wenzelm@63589  1619  also have "... = - (Ln \)" using Ln_inverse by blast  wenzelm@63589  1620  also have "... = - (\ * pi/2)" by simp  lp15@59751  1621  finally show ?thesis .  lp15@59751  1622 qed  lp15@59751  1623 lp15@59751  1624 lemma Ln_times:  lp15@59751  1625  assumes "w \ 0" "z \ 0"  lp15@59751  1626  shows "Ln(w * z) =  lp15@68257  1627  (if Im(Ln w + Ln z) \ -pi then (Ln(w) + Ln(z)) + \ * of_real(2*pi)  lp15@68257  1628  else if Im(Ln w + Ln z) > pi then (Ln(w) + Ln(z)) - \ * of_real(2*pi)  lp15@68257  1629  else Ln(w) + Ln(z))"  lp15@59751  1630  using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]  lp15@59751  1631  using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]  paulson@62131  1632  by (auto simp: exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)  lp15@59751  1633 eberlm@69180  1634 corollary%unimportant Ln_times_simple:  lp15@59751  1635  "\w \ 0; z \ 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \ pi\  lp15@59751  1636  \ Ln(w * z) = Ln(w) + Ln(z)"  lp15@59751  1637  by (simp add: Ln_times)  lp15@59751  1638 eberlm@69180  1639 corollary%unimportant Ln_times_of_real:  lp15@60150  1640  "\r > 0; z \ 0\ \ Ln(of_real r * z) = ln r + Ln(z)"  lp15@60150  1641  using mpi_less_Im_Ln Im_Ln_le_pi  lp15@60150  1642  by (force simp: Ln_times)  lp15@60150  1643 eberlm@69180  1644 corollary%unimportant Ln_times_Reals:  lp15@68535  1645  "\r \ Reals; Re r > 0; z \ 0\ \ Ln(r * z) = ln (Re r) + Ln(z)"  lp15@68535  1646  using Ln_Reals_eq Ln_times_of_real by fastforce  lp15@68535  1647 eberlm@69180  1648 corollary%unimportant Ln_divide_of_real:  lp15@60150  1649  "\r > 0; z \ 0\ \ Ln(z / of_real r) = Ln(z) - ln r"  lp15@60150  1650 using Ln_times_of_real [of "inverse r" z]  lp15@61609  1651 by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric]  lp15@60150  1652  del: of_real_inverse)  lp15@60150  1653 eberlm@69180  1654 corollary%unimportant Ln_prod:  lp15@68499  1655  fixes f :: "'a \ complex"  lp15@68499  1656  assumes "finite A" "\x. x \ A \ f x \ 0"  lp15@68499  1657  shows "\n. Ln (prod f A) = (\x \ A. Ln (f x) + (of_int (n x) * (2 * pi)) * \)"  lp15@68499  1658  using assms  lp15@68499  1659 proof (induction A)  lp15@68499  1660  case (insert x A)  lp15@68499  1661  then obtain n where n: "Ln (prod f A) = (\x\A. Ln (f x) + of_real (of_int (n x) * (2 * pi)) * \)"  lp15@68499  1662  by auto  lp15@68499  1663  define D where "D \ Im (Ln (f x)) + Im (Ln (prod f A))"  lp15@68499  1664  define q::int where "q \ (if D \ -pi then 1 else if D > pi then -1 else 0)"  lp15@68499  1665  have "prod f A \ 0" "f x \ 0"  lp15@68499  1666  by (auto simp: insert.hyps insert.prems)  lp15@68499  1667  with insert.hyps pi_ge_zero show ?case  lp15@68499  1668  by (rule_tac x="n(x:=q)" in exI) (force simp: Ln_times q_def D_def n intro!: sum.cong)  lp15@68499  1669 qed auto  lp15@68499  1670 lp15@59751  1671 lemma Ln_minus:  lp15@59751  1672  assumes "z \ 0"  nipkow@69508  1673  shows "Ln(-z) = (if Im(z) \ 0 \ $$Re(z) < 0 \ Im(z) = 0)  wenzelm@63589  1674  then Ln(z) + \ * pi  wenzelm@63589  1675  else Ln(z) - \ * pi)" (is "_ = ?rhs")  lp15@59751  1676  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms  lp15@59751  1677  Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]  paulson@62131  1678  by (fastforce simp: exp_add exp_diff exp_Euler intro!: Ln_unique)  lp15@59751  1679 lp15@59751  1680 lemma Ln_inverse_if:  lp15@59751  1681  assumes "z \ 0"  paulson@62131  1682  shows "Ln (inverse z) = (if z \ \\<^sub>\\<^sub>0 then -(Ln z) + \ * 2 * complex_of_real pi else -(Ln z))"  paulson@62131  1683 proof (cases "z \ \\<^sub>\\<^sub>0")  paulson@62131  1684  case False then show ?thesis  lp15@59751  1685  by (simp add: Ln_inverse)  lp15@59751  1686 next  paulson@62131  1687  case True  lp15@59751  1688  then have z: "Im z = 0" "Re z < 0"  lp15@59751  1689  using assms  paulson@62131  1690  apply (auto simp: complex_nonpos_Reals_iff)  paulson@62131  1691  by (metis complex_is_Real_iff le_imp_less_or_eq of_real_0 of_real_Re)  lp15@59751  1692  have "Ln(inverse z) = Ln(- (inverse (-z)))"  lp15@59751  1693  by simp  lp15@59751  1694  also have "... = Ln (inverse (-z)) + \ * complex_of_real pi"  lp15@59751  1695  using assms z  lp15@59751  1696  apply (simp add: Ln_minus)  lp15@59751  1697  apply (simp add: field_simps)  lp15@59751  1698  done  lp15@59751  1699  also have "... = - Ln (- z) + \ * complex_of_real pi"  lp15@59751  1700  apply (subst Ln_inverse)  lp15@62534  1701  using z by (auto simp add: complex_nonneg_Reals_iff)  lp15@59751  1702  also have "... = - (Ln z) + \ * 2 * complex_of_real pi"  lp15@68257  1703  by (subst Ln_minus) (use assms z in auto)  paulson@62131  1704  finally show ?thesis by (simp add: True)  lp15@59751  1705 qed  lp15@59751  1706 lp15@59751  1707 lemma Ln_times_ii:  lp15@59751  1708  assumes "z \ 0"  wenzelm@63589  1709  shows "Ln(\ * z) = (if 0 \ Re(z) | Im(z) < 0  wenzelm@63589  1710  then Ln(z) + \ * of_real pi/2  wenzelm@63589  1711  else Ln(z) - \ * of_real(3 * pi/2))"  lp15@59751  1712  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms  lp15@59751  1713  Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]  lp15@65064  1714  by (simp add: Ln_times) auto  lp15@59751  1715 lp15@65587  1716 lemma Ln_of_nat [simp]: "0 < n \ Ln (of_nat n) = of_real (ln (of_nat n))"  eberlm@61524  1717  by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all  eberlm@61524  1718 lp15@61609  1719 lemma Ln_of_nat_over_of_nat:  eberlm@61524  1720  assumes "m > 0" "n > 0"  eberlm@61524  1721  shows "Ln (of_nat m / of_nat n) = of_real (ln (of_nat m) - ln (of_nat n))"  eberlm@61524  1722 proof -  eberlm@61524  1723  have "of_nat m / of_nat n = (of_real (of_nat m / of_nat n) :: complex)" by simp  eberlm@61524  1724  also from assms have "Ln ... = of_real (ln (of_nat m / of_nat n))"  eberlm@61524  1725  by (simp add: Ln_of_real[symmetric])  eberlm@61524  1726  also from assms have "... = of_real (ln (of_nat m) - ln (of_nat n))"  eberlm@61524  1727  by (simp add: ln_div)  eberlm@61524  1728  finally show ?thesis .  eberlm@61524  1729 qed  eberlm@61524  1730 eberlm@67278  1731 lemma Ln_measurable [measurable]: "Ln \ measurable borel borel"  eberlm@67278  1732 proof -  eberlm@67278  1733  have *: "Ln (-of_real x) = of_real (ln x) + \ * pi" if "x > 0" for x  eberlm@67278  1734  using that by (subst Ln_minus) (auto simp: Ln_of_real)  eberlm@67278  1735  have **: "Ln (of_real x) = of_real (ln (-x)) + \ * pi" if "x < 0" for x  eberlm@67278  1736  using *[of "-x"] that by simp  lp15@67976  1737  have cont: "(\x. indicat_real (- \\<^sub>\\<^sub>0) x *\<^sub>R Ln x) \ borel_measurable borel"  eberlm@67278  1738  by (intro borel_measurable_continuous_on_indicator continuous_intros) auto  eberlm@67278  1739  have "(\x. if x \ \\<^sub>\\<^sub>0 then ln (-Re x) + \ * pi else indicator (-\\<^sub>\\<^sub>0) x *\<^sub>R Ln x) \ borel \\<^sub>M borel"  eberlm@67278  1740  (is "?f \ _") by (rule measurable_If_set[OF _ cont]) auto  eberlm@67278  1741  hence "(\x. if x = 0 then Ln 0 else ?f x) \ borel \\<^sub>M borel" by measurable  eberlm@67278  1742  also have "(\x. if x = 0 then Ln 0 else ?f x) = Ln"  eberlm@67278  1743  by (auto simp: fun_eq_iff ** nonpos_Reals_def)  eberlm@67278  1744  finally show ?thesis .  eberlm@67278  1745 qed  eberlm@67278  1746 eberlm@67278  1747 lemma powr_complex_measurable [measurable]:  eberlm@67278  1748  assumes [measurable]: "f \ measurable M borel" "g \ measurable M borel"  eberlm@67278  1749  shows "(\x. f x powr g x :: complex) \ measurable M borel"  eberlm@67278  1750  using assms by (simp add: powr_def)  eberlm@67278  1751 lp15@68499  1752 subsection\The Argument of a Complex Number\  lp15@68499  1753 lp15@68535  1754 text\Finally: it's is defined for the same interval as the complex logarithm: (-\pi,\pi].\  lp15@68535  1755 eberlm@69180  1756 definition%important Arg :: "complex \ real" where "Arg z \ (if z = 0 then 0 else Im (Ln z))"  lp15@68499  1757 lp15@68527  1758 lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"  lp15@68527  1759  by (simp add: Im_Ln_eq_pi Arg_def)  lp15@68527  1760 lp15@68527  1761 lemma mpi_less_Arg: "-pi < Arg z"  lp15@68527  1762  and Arg_le_pi: "Arg z \ pi"  lp15@68527  1763  by (auto simp: Arg_def mpi_less_Im_Ln Im_Ln_le_pi)  lp15@68527  1764 lp15@68527  1765 lemma  lp15@68527  1766  assumes "z \ 0"  lp15@68527  1767  shows Arg_eq: "z = of_real(norm z) * exp(\ * Arg z)"  lp15@68527  1768  using assms exp_Ln exp_eq_polar  lp15@68527  1769  by (auto simp: Arg_def)  lp15@68527  1770 lp15@68535  1771 lemma is_Arg_Arg: "z \ 0 \ is_Arg z (Arg z)"  lp15@68535  1772  by (simp add: Arg_eq is_Arg_def)  lp15@68535  1773 lp15@68527  1774 lemma Argument_exists:  lp15@68527  1775  assumes "z \ 0" and R: "R = {r-pi<..r+pi}"  lp15@68527  1776  obtains s where "is_Arg z s" "s\R"  lp15@68527  1777 proof -  lp15@68527  1778  let ?rp = "r - Arg z + pi"  lp15@68527  1779  define k where "k \ \?rp / (2 * pi)\"  lp15@68527  1780  have "(Arg z + of_int k * (2 * pi)) \ R"  lp15@68527  1781  using floor_divide_lower [of "2*pi" ?rp] floor_divide_upper [of "2*pi" ?rp]  lp15@68527  1782  by (auto simp: k_def algebra_simps R)  lp15@68527  1783  then show ?thesis  lp15@68527  1784  using Arg_eq \z \ 0\ is_Arg_2pi_iff is_Arg_def that by blast  lp15@68527  1785 qed  lp15@68527  1786 lp15@68527  1787 lemma Argument_exists_unique:  lp15@68527  1788  assumes "z \ 0" and R: "R = {r-pi<..r+pi}"  lp15@68527  1789  obtains s where "is_Arg z s" "s\R" "\t. \is_Arg z t; t\R\ \ s=t"  lp15@68527  1790 proof -  lp15@68527  1791  obtain s where s: "is_Arg z s" "s\R"  lp15@68527  1792  using Argument_exists [OF assms] .  lp15@68527  1793  moreover have "\t. \is_Arg z t; t\R\ \ s=t"  lp15@68527  1794  using assms s by (auto simp: is_Arg_eqI)  lp15@68527  1795  ultimately show thesis  lp15@68527  1796  using that by blast  lp15@68527  1797 qed  lp15@68527  1798 lp15@68527  1799 lemma Argument_Ex1:  lp15@68527  1800  assumes "z \ 0" and R: "R = {r-pi<..r+pi}"  lp15@68527  1801  shows "\!s. is_Arg z s \ s \ R"  lp15@68527  1802  using Argument_exists_unique [OF assms] by metis  lp15@68527  1803 lp15@68527  1804 lemma Arg_divide:  lp15@68527  1805  assumes "w \ 0" "z \ 0"  lp15@68527  1806  shows "is_Arg (z / w) (Arg z - Arg w)"  lp15@68527  1807  using Arg_eq [of z] Arg_eq [of w] Arg_eq [of "norm(z / w)"] assms  lp15@68527  1808  by (auto simp: is_Arg_def norm_divide field_simps exp_diff Arg_of_real)  lp15@68527  1809 lp15@68499  1810 lemma Arg_unique_lemma:  lp15@68499  1811  assumes z: "is_Arg z t"  lp15@68499  1812  and z': "is_Arg z t'"  lp15@68499  1813  and t: "- pi < t" "t \ pi"  lp15@68499  1814  and t': "- pi < t'" "t' \ pi"  lp15@68499  1815  and nz: "z \ 0"  lp15@68499  1816  shows "t' = t"  lp15@68499  1817  using Arg2pi_unique_lemma [of "- (inverse z)"]  lp15@68499  1818 proof -  lp15@68499  1819  have "pi - t' = pi - t"  lp15@68499  1820  proof (rule Arg2pi_unique_lemma [of "- (inverse z)"])  lp15@68499  1821  have "- (inverse z) = - (inverse (of_real(norm z) * exp(\ * t)))"  lp15@68499  1822  by (metis is_Arg_def z)  lp15@68499  1823  also have "... = (cmod (- inverse z)) * exp (\ * (pi - t))"  lp15@68499  1824  by (auto simp: field_simps exp_diff norm_divide)  lp15@68499  1825  finally show "is_Arg (- inverse z) (pi - t)"  lp15@68499  1826  unfolding is_Arg_def .  lp15@68499  1827  have "- (inverse z) = - (inverse (of_real(norm z) * exp(\ * t')))"  lp15@68499  1828  by (metis is_Arg_def z')  lp15@68499  1829  also have "... = (cmod (- inverse z)) * exp (\ * (pi - t'))"  lp15@68499  1830  by (auto simp: field_simps exp_diff norm_divide)  lp15@68499  1831  finally show "is_Arg (- inverse z) (pi - t')"  lp15@68499  1832  unfolding is_Arg_def .  lp15@68499  1833  qed (use assms in auto)  lp15@68499  1834  then show ?thesis  lp15@68499  1835  by simp  lp15@68499  1836 qed  lp15@68499  1837 lp15@68499  1838 lemma complex_norm_eq_1_exp_eq: "norm z = 1 \ exp(\ * (Arg z)) = z"  lp15@68499  1839  by (metis Arg_eq exp_not_eq_zero exp_zero mult.left_neutral norm_zero of_real_1 norm_exp_i_times)  lp15@68499  1840 lp15@68499  1841 lemma Arg_unique: "\of_real r * exp(\ * a) = z; 0 < r; -pi < a; a \ pi\ \ Arg z = a"  lp15@68499  1842  by (rule Arg_unique_lemma [unfolded is_Arg_def, OF _ Arg_eq])  lp15@68499  1843  (use mpi_less_Arg Arg_le_pi in \auto simp: norm_mult$$  lp15@68499  1844 lp15@68499  1845 lemma Arg_minus:  lp15@68499  1846  assumes "z \ 0"  lp15@68499  1847  shows "Arg (-z) = (if Arg z \ 0 then Arg z + pi else Arg z - pi)"  lp15@68499  1848 proof -  lp15@68499  1849  have [simp]: "cmod z * cos (Arg z) = Re z"  lp15@68499  1850  using assms Arg_eq [of z] by (metis Re_exp exp_Ln norm_exp_eq_Re Arg_def)  lp15@68499  1851  have [simp]: "cmod z * sin (Arg z) = Im z"  lp15@68499  1852  using assms Arg_eq [of z] by (metis Im_exp exp_Ln norm_exp_eq_Re Arg_def)  lp15@68499  1853  show ?thesis  lp15@68499  1854  apply (rule Arg_unique [of "norm z"])  lp15@68499  1855  apply (rule complex_eqI)  lp15@68499  1856  using mpi_less_Arg [of z] Arg_le_pi [of z] assms  lp15@68499  1857  apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])  lp15@68499  1858  done  lp15@68499  1859 qed  lp15@68499  1860 lp15@68499  1861 lemma Arg_times_of_real [simp]:  lp15@68499  1862  assumes "0 < r" shows "Arg (of_real r * z) = Arg z"  lp15@68499  1863 proof (cases "z=0")  lp15@68499  1864  case True  lp15@68499  1865  then show ?thesis  lp15@68499  1866  by (simp add: Arg_def)  lp15@68499  1867 next  lp15@68499  1868  case False  lp15@68499  1869  with Arg_eq assms show ?thesis  lp15@68499  1870  by (auto simp: mpi_less_Arg Arg_le_pi intro!: Arg_unique [of "r * norm z"])  lp15@68499  1871 qed  lp15@68499  1872 lp15@68499  1873 lemma Arg_times_of_real2 [simp]: "0 < r \ Arg (z * of_real r) = Arg z"  lp15@68499  1874  by (metis Arg_times_of_real mult.commute)  lp15@68499  1875 lp15@68499  1876 lemma Arg_divide_of_real [simp]: "0 < r \ Arg (z / of_real r) = Arg z"  lp15@68499  1877  by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)  lp15@68499  1878 lp15@68499  1879 lemma Arg_less_0: "0 \ Arg z \ 0 \ Im z"  lp15@68499  1880  using Im_Ln_le_pi Im_Ln_pos_le  lp15@68499  1881  by (simp add: Arg_def)  lp15@68499  1882 lp15@68499  1883 lemma Arg_eq_pi: "Arg z = pi \ Re z < 0 \ Im z = 0"  lp15@68499  1884  by (auto simp: Arg_def Im_Ln_eq_pi)  lp15@68499  1885 lp15@68499  1886 lemma Arg_lt_pi: "0 < Arg z \ Arg z < pi \ 0 < Im z"  lp15@68499  1887  using Arg_less_0 [of z] Im_Ln_pos_lt  lp15@68499  1888  by (auto simp: order.order_iff_strict Arg_def)  lp15@68499  1889 lp15@68499  1890 lemma Arg_eq_0: "Arg z = 0 \ z \ \ \ 0 \ Re z"  lp15@68499  1891  using complex_is_Real_iff  lp15@68499  1892  by (simp add: Arg_def Im_Ln_eq_0) (metis less_eq_real_def of_real_Re of_real_def scale_zero_left)  lp15@68499  1893 eberlm@69180  1894 corollary%unimportant Arg_ne_0: assumes "z \ \\<^sub>\\<^sub>0" shows "Arg z \ 0"  lp15@68499  1895  using assms by (auto simp: nonneg_Reals_def Arg_eq_0)  lp15@68499  1896 lp15@68499  1897 lemma Arg_eq_pi_iff: "Arg z = pi \ z \ \ \ Re z < 0"  lp15@68499  1898 proof (cases "z=0")  lp15@68499  1899  case False  lp15@68499  1900  then show ?thesis  lp15@68499  1901  using Arg_eq_0 [of "-z"] Arg_eq_pi complex_is_Real_iff by blast  lp15@68499  1902 qed (simp add: Arg_def)  lp15@68499  1903 lp15@68499  1904 lemma Arg_eq_0_pi: "Arg z = 0 \ Arg z = pi \ z \ \"  lp15@68499  1905  using Arg_eq_pi_iff Arg_eq_0 by force  lp15@68499  1906 lp15@68499  1907 lemma Arg_real: "z \ \ \ Arg z = (if 0 \ Re z then 0 else pi)"  lp15@68499  1908  using Arg_eq_0 Arg_eq_0_pi by auto  lp15@68499  1909 lp15@68499  1910 lemma Arg_inverse: "Arg(inverse z) = (if z \ \ then Arg z else - Arg z)"  lp15@68499  1911 proof (cases "z \ \")  lp15@68499  1912  case True  lp15@68499  1913  then show ?thesis  lp15@68499  1914  by simp (metis Arg2pi_inverse Arg2pi_real Arg_real Reals_inverse)  lp15@68499  1915 next  lp15@68499  1916  case False  lp15@68499  1917  then have "Arg z < pi" "z \ 0"  lp15@68527  1918  using Arg_eq_0_pi Arg_le_pi by (auto simp: less_eq_real_def)  lp15@68499  1919  then show ?thesis  lp15@68499  1920  apply (simp add: False)  lp15@68499  1921  apply (rule Arg_unique [of "inverse (norm z)"])  lp15@68499  1922  using False mpi_less_Arg [of z] Arg_eq [of z]  lp15@68499  1923  apply (auto simp: exp_minus field_simps)  lp15@68499  1924  done  lp15@68499  1925 qed  lp15@68499  1926 lp15@68499  1927 lemma Arg_eq_iff:  lp15@68499  1928  assumes "w \ 0" "z \ 0"  lp15@68499  1929  shows "Arg w = Arg z \ (\x. 0 < x \ w = of_real x * z)"  lp15@68499  1930  using assms Arg_eq [of z] Arg_eq [of w]  lp15@68499  1931  apply auto  lp15@68499  1932  apply (rule_tac x="norm w / norm z" in exI)  lp15@68499  1933  apply (simp add: divide_simps)  lp15@68499  1934  by (metis mult.commute mult.left_commute)  lp15@68499  1935 lp15@68499  1936 lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \ Arg z = 0"  lp15@68499  1937  by (metis Arg_eq_0 Arg_inverse inverse_inverse_eq)  lp15@68499  1938 lp15@68499  1939 lemma Arg_cnj_eq_inverse: "z\0 \ Arg (cnj z) = Arg (inverse z)"  lp15@68499  1940  apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)  lp15@68499  1941  by (metis of_real_power zero_less_norm_iff zero_less_power)  lp15@68499  1942 lp15@68499  1943 lemma Arg_cnj: "Arg(cnj z) = (if z \ \ then Arg z else - Arg z)"  lp15@68499  1944  by (metis Arg_cnj_eq_inverse Arg_inverse Reals_0 complex_cnj_zero)  lp15@68499  1945 lp15@68499  1946 lemma Arg_exp: "-pi < Im z \ Im z \ pi \ Arg(exp z) = Im z"  lp15@68499  1947  by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)  lp15@68499  1948 lp15@68499  1949 lemma Ln_Arg: "z\0 \ Ln(z) = ln(norm z) + \ * Arg(z)"  lp15@68499  1950  by (metis Arg_def Re_Ln complex_eq)  lp15@68499  1951 lp15@68517  1952 lemma continuous_at_Arg:  lp15@68517  1953  assumes "z \ \\<^sub>\\<^sub>0"  lp15@68517  1954  shows "continuous (at z) Arg"  lp15@68517  1955 proof -  lp15@68517  1956  have [simp]: "(\z. Im (Ln z)) \z\ Arg z"  lp15@68517  1957  using Arg_def assms continuous_at by fastforce  lp15@68517  1958  show ?thesis  lp15@68517  1959  unfolding continuous_at  lp15@68517  1960  proof (rule Lim_transform_within_open)  lp15@68517  1961  show "\w. \w \ - \\<^sub>\\<^sub>0; w \ z\ \ Im (Ln w) = Arg w"  lp15@68517  1962  by (metis Arg_def Compl_iff nonpos_Reals_zero_I)  lp15@68517  1963  qed (use assms in auto)  lp15@68517  1964 qed  lp15@68517  1965 lp15@68517  1966 lemma continuous_within_Arg: "z \ \\<^sub>\\<^sub>0 \ continuous (at z within S) Arg"  lp15@68517  1967  using continuous_at_Arg continuous_at_imp_continuous_within by blast  lp15@68499  1968 lp15@59751  1969 eberlm@69180  1970 subsection\The Unwinding Number and the Ln product Formula\  lp15@68535  1971 lp15@68535  1972 text\Note that in this special case the unwinding number is -1, 0 or 1. But it's always an integer.\  lp15@68535  1973 lp15@68535  1974 lemma is_Arg_exp_Im: "is_Arg (exp z) (Im z)"  lp15@68535  1975  using exp_eq_polar is_Arg_def norm_exp_eq_Re by auto  lp15@68535  1976 lp15@68535  1977 lemma is_Arg_exp_diff_2pi:  lp15@68535  1978  assumes "is_Arg (exp z) \"  lp15@68535  1979  shows "\k. Im z - of_int k * (2 * pi) = \"  lp15@68535  1980 proof (intro exI is_Arg_eqI)  lp15@68535  1981  let ?k = "$$Im z -$$ / (2 * pi)\"  lp15@68535  1982  show "is_Arg (exp z) (Im z - real_of_int ?k * (2 * pi))"  lp15@68535  1983  by (metis diff_add_cancel is_Arg_2pi_iff is_Arg_exp_Im)  lp15@68535  1984  show "\Im z - real_of_int ?k * (2 * pi) - \\ < 2 * pi"  lp15@68535  1985  using floor_divide_upper [of "2*pi" "Im z - \"] floor_divide_lower [of "2*pi" "Im z - \"]  lp15@68535  1986  by (auto simp: algebra_simps abs_if)  lp15@68535  1987 qed (auto simp: is_Arg_exp_Im assms)  lp15@68535  1988 lp15@68535  1989 lemma Arg_exp_diff_2pi: "\k. Im z - of_int k * (2 * pi) = Arg (exp z)"  lp15@68535  1990  using is_Arg_exp_diff_2pi [OF is_Arg_Arg] by auto  lp15@68535  1991 lp15@68535  1992 lemma unwinding_in_Ints: "(z - Ln(exp z)) / (of_real(2*pi) * \) \ \"  lp15@68535  1993  using Arg_exp_diff_2pi [of z]  lp15@68535  1994  by (force simp: Ints_def image_def field_simps Arg_def intro!: complex_eqI)  lp15@68535  1995 eberlm@69180  1996 definition%important unwinding :: "complex \ int" where  lp15@68535  1997  "unwinding z \ THE k. of_int k = (z - Ln(exp z)) / (of_real(2*pi) * \)"  lp15@68535  1998 lp15@68535  1999 lemma unwinding: "of_int (unwinding z) = (z - Ln(exp z)) / (of_real(2*pi) * \)"  lp15@68535  2000  using unwinding_in_Ints [of z]  lp15@68535  2001  unfolding unwinding_def Ints_def by force  lp15@68535  2002 lp15@68535  2003 lemma unwinding_2pi: "(2*pi) * \ * unwinding(z) = z - Ln(exp z)"  lp15@68535  2004  by (simp add: unwinding)  lp15@68535  2005 lp15@68535  2006 lemma Ln_times_unwinding:  lp15@68535  2007  "w \ 0 \ z \ 0 \ Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \ * unwinding(Ln w + Ln z)"  lp15@68535  2008  using unwinding_2pi by (simp add: exp_add)  lp15@68535  2009 lp15@68535  2010 eberlm@69180  2011 subsection%unimportant\Relation between Ln and Arg2pi, and hence continuity of Arg2pi\  lp15@68493  2012 lp15@68493  2013 lemma Arg2pi_Ln:  lp15@68493  2014  assumes "0 < Arg2pi z" shows "Arg2pi z = Im(Ln(-z)) + pi"  lp15@60150  2015 proof (cases "z = 0")  lp15@60150  2016  case True  lp15@60150  2017  with assms show ?thesis  lp15@60150  2018  by simp  lp15@60150  2019 next  lp15@60150  2020  case False  lp15@68493  2021  then have "z / of_real(norm z) = exp(\ * of_real(Arg2pi z))"  lp15@68493  2022  using Arg2pi [of z]  lp15@68499  2023  by (metis is_Arg_def abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)  lp15@68493  2024  then have "- z / of_real(norm z) = exp (\ * (of_real (Arg2pi z) - pi))"  lp15@60150  2025  using cis_conv_exp cis_pi  lp15@60150  2026  by (auto simp: exp_diff algebra_simps)  lp15@68493  2027  then have "ln (- z / of_real(norm z)) = ln (exp (\ * (of_real (Arg2pi z) - pi)))"  lp15@60150  2028  by simp  lp15@68493  2029  also have "... = \ * (of_real(Arg2pi z) - pi)"  lp15@68493  2030  using Arg2pi [of z] assms pi_not_less_zero  lp15@60150  2031  by auto  lp15@68493  2032  finally have "Arg2pi z = Im (Ln (- z / of_real (cmod z))) + pi"  lp15@60150  2033  by simp  lp15@60150  2034  also have "... = Im (Ln (-z) - ln (cmod z)) + pi"  lp15@60150  2035  by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)  lp15@60150  2036  also have "... = Im (Ln (-z)) + pi"  lp15@60150  2037  by simp  lp15@60150  2038  finally show ?thesis .  lp15@60150  2039 qed  lp15@60150  2040 lp15@68493  2041 lemma continuous_at_Arg2pi:  paulson@62131  2042  assumes "z \ \\<^sub>\\<^sub>0"  lp15@68493  2043  shows "continuous (at z) Arg2pi"  lp15@60150  2044 proof -  lp15@60150  2045  have *: "isCont (\z. Im (Ln (- z)) + pi) z"  lp15@60150  2046  by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+  lp15@68499  2047  have [simp]: "Im x \ 0 \ Im (Ln (- x)) + pi = Arg2pi x" for x  lp15@68499  2048  using Arg2pi_Ln by (simp add: Arg2pi_gt_0 complex_nonneg_Reals_iff)  paulson@62131  2049  consider "Re z < 0" | "Im z \ 0" using assms  lp15@62534  2050  using complex_nonneg_Reals_iff not_le by blast  lp15@68493  2051  then have [simp]: "(\z. Im (Ln (- z)) + pi) \z\ Arg2pi z"  lp15@68499  2052  using "*" by (simp add: Arg2pi_Ln Arg2pi_gt_0 assms continuous_within)  paulson@62131  2053  show ?thesis  lp15@68257  2054  unfolding continuous_at  lp15@68257  2055  proof (rule Lim_transform_within_open)  lp15@68493  2056  show "\x. \x \ - \\<^sub>\\<^sub>0; x \ z\ \ Im (Ln (- x)) + pi = Arg2pi x"  lp15@68493  2057  by (auto simp add: Arg2pi_Ln [OF Arg2pi_gt_0] complex_nonneg_Reals_iff)  lp15@68257  2058  qed (use assms in auto)  lp15@60150  2059 qed  lp15@60150  2060 eberlm@62049  2061 lp15@68493  2062 text\Relation between Arg2pi and arctangent in upper halfplane\  lp15@68493  2063 lemma Arg2pi_arctan_upperhalf:  lp15@60150  2064  assumes "0 < Im z"  lp15@68493  2065  shows "Arg2pi z = pi/2 - arctan(Re z / Im z)"  lp15@60150  2066 proof (cases "z = 0")  lp15@60150  2067  case False  lp15@60150  2068  show ?thesis  lp15@68493  2069  proof (rule Arg2pi_unique [of "norm z"])  lp15@68257  2070  show "(cmod z) * exp (\ * (pi / 2 - arctan (Re z / Im z))) = z"  lp15@68257  2071  apply (auto simp: exp_Euler cos_diff sin_diff)  lp15@68257  2072  using assms norm_complex_def [of z, symmetric]  lp15@68257  2073  apply (simp add: sin_of_real cos_of_real sin_arctan cos_arctan field_simps real_sqrt_divide)  lp15@68257  2074  apply (metis complex_eq)  lp15@68257  2075  done  lp15@68257  2076  qed (use False arctan [of "Re z / Im z"] in auto)  lp15@68257  2077 qed (use assms in auto)  lp15@60150  2078 lp15@68493  2079 lemma Arg2pi_eq_Im_Ln:  lp15@61609  2080  assumes "0 \ Im z" "0 < Re z"  lp15@68493  2081  shows "Arg2pi z = Im (Ln z)"  lp15@68257  2082 proof (cases "Im z = 0")  lp15@60150  2083  case True then show ?thesis  lp15@68493  2084  using Arg2pi_eq_0 Ln_in_Reals assms(2) complex_is_Real_iff by auto  lp15@60150  2085 next  lp15@61609  2086  case False  lp15@68493  2087  then have *: "Arg2pi z > 0"  lp15@68493  2088  using Arg2pi_gt_0 complex_is_Real_iff by blast  lp15@68257  2089  then have "z \ 0"  lp15@68257  2090  by auto  lp15@68257  2091  with * assms False show ?thesis  lp15@68493  2092  by (subst Arg2pi_Ln) (auto simp: Ln_minus)  lp15@60150  2093 qed  lp15@60150  2094 lp15@68493  2095 lemma continuous_within_upperhalf_Arg2pi:  lp15@60150  2096  assumes "z \ 0"  lp15@68493  2097  shows "continuous (at z within {z. 0 \ Im z}) Arg2pi"  paulson@62131  2098 proof (cases "z \ \\<^sub>\\<^sub>0")  lp15@60150  2099  case False then show ?thesis  lp15@68493  2100  using continuous_at_Arg2pi continuous_at_imp_continuous_within by auto  lp15@60150  2101 next  lp15@60150  2102  case True  lp15@60150  2103  then have z: "z \ \" "0 < Re z"  paulson@62131  2104  using assms by (auto simp: complex_nonneg_Reals_iff complex_is_Real_iff complex_neq_0)  lp15@68493  2105  then have [simp]: "Arg2pi z = 0" "Im (Ln z) = 0"  lp15@68493  2106  by (auto simp: Arg2pi_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)  lp15@61609  2107  show ?thesis  lp15@60150  2108  proof (clarsimp simp add: continuous_within Lim_within dist_norm)  lp15@60150  2109  fix e::real  lp15@60150  2110  assume "0 < e"  lp15@60150  2111  moreover have "continuous (at z) (\x. Im (Ln x))"  paulson@62131  2112  using z by (simp add: continuous_at_Ln complex_nonpos_Reals_iff)  lp15@60150  2113  ultimately  lp15@60150  2114  obtain d where d: "d>0" "\x. x \ z \ cmod (x - z) < d \ \Im (Ln x)\ < e"  lp15@60150  2115  by (auto simp: continuous_within Lim_within dist_norm)  lp15@60150  2116  { fix x  lp15@60150  2117  assume "cmod (x - z) < Re z / 2"  lp15@60150  2118  then have "\Re x - Re z\ < Re z / 2"  lp15@60150  2119  by (metis le_less_trans abs_Re_le_cmod minus_complex.simps(1))  lp15@60150  2120  then have "0 < Re x"  lp15@60150  2121  using z by linarith  lp15@60150  2122  }  lp15@68493  2123  then show "\d>0. \x. 0 \ Im x \ x \ z \ cmod (x - z) < d \ \Arg2pi x\ < e"  lp15@60150  2124  apply (rule_tac x="min d (Re z / 2)" in exI)  lp15@60150  2125  using z d  lp15@68493  2126  apply (auto simp: Arg2pi_eq_Im_Ln)  lp15@60150  2127  done  lp15@60150  2128  qed  lp15@60150  2129 qed  lp15@60150  2130 lp15@68493  2131 lemma continuous_on_upperhalf_Arg2pi: "continuous_on ({z. 0 \ Im z} - {0}) Arg2pi"  lp15@68257  2132  unfolding continuous_on_eq_continuous_within  lp15@68493  2133  by (metis DiffE Diff_subset continuous_within_subset continuous_within_upperhalf_Arg2pi insertCI)  lp15@68493  2134 lp15@68493  2135 lemma open_Arg2pi2pi_less_Int:  lp15@60150  2136  assumes "0 \ s" "t \ 2*pi"  lp15@68493  2137  shows "open ({y. s < Arg2pi y} \ {y. Arg2pi y < t})"  lp15@60150  2138 proof -  lp15@68493  2139  have 1: "continuous_on (UNIV - \\<^sub>\\<^sub>0) Arg2pi"  lp15@68493  2140  using continuous_at_Arg2pi continuous_at_imp_continuous_within  paulson@62131  2141  by (auto simp: continuous_on_eq_continuous_within)  paulson@62131  2142  have 2: "open (UNIV - \\<^sub>\\<^sub>0 :: complex set)" by (simp add: open_Diff)  lp15@60150  2143  have "open ({z. s < z} \ {z. z < t})"  lp15@60150  2144  using open_lessThan [of t] open_greaterThan [of s]  lp15@60150  2145  by (metis greaterThan_def lessThan_def open_Int)  lp15@68493  2146  moreover have "{y. s < Arg2pi y} \ {y. Arg2pi y < t} \ - \\<^sub>\\<^sub>0"  lp15@68493  2147  using assms by (auto simp: Arg2pi_real complex_nonneg_Reals_iff complex_is_Real_iff)  lp15@60150  2148  ultimately show ?thesis  lp15@61609  2149  using continuous_imp_open_vimage [OF 1 2, of "{z. Re z > s} \ {z. Re z < t}"]  lp15@60150  2150  by auto  lp15@60150  2151 qed  lp15@60150  2152 lp15@68493  2153 lemma open_Arg2pi2pi_gt: "open {z. t < Arg2pi z}"  lp15@60150  2154 proof (cases "t < 0")  lp15@68493  2155  case True then have "{z. t < Arg2pi z} = UNIV"  lp15@68493  2156  using Arg2pi_ge_0 less_le_trans by auto  lp15@60150  2157  then show ?thesis  lp15@60150  2158  by simp  lp15@60150  2159 next  lp15@60150  2160  case False then show ?thesis  lp15@68493  2161  using open_Arg2pi2pi_less_Int [of t "2*pi"] Arg2pi_lt_2pi  lp15@60150  2162  by auto  lp15@60150  2163 qed  lp15@60150  2164 lp15@68493  2165 lemma closed_Arg2pi2pi_le: "closed {z. Arg2pi z \ t}"  lp15@68493  2166  using open_Arg2pi2pi_gt [of t]  lp15@60150  2167  by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)  lp15@60017  2168 eberlm@69180  2169 subsection%unimportant\Complex Powers\  lp15@60017  2170 lp15@60017  2171 lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"  lp15@60020  2172  by (simp add: powr_def)  lp15@60017  2173 lp15@60017  2174 lemma powr_nat:  lp15@60017  2175  fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"  lp15@60020  2176  by (simp add: exp_of_nat_mult powr_def)  lp15@60017  2177 lp15@60017  2178 lemma norm_powr_real: "w \ \ \ 0 < Re w \ norm(w powr z) = exp(Re z * ln(Re w))"  lp15@60020  2179  apply (simp add: powr_def)  lp15@68281  2180  using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def by auto  lp15@60017  2181 lp15@65583  2182 lemma powr_complexpow [simp]:  lp15@65583  2183  fixes x::complex shows "x \ 0 \ x powr (of_nat n) = x^n"  lp15@65583  2184  by (induct n) (auto simp: ac_simps powr_add)  lp15@65583  2185 lp15@65583  2186 lemma powr_complexnumeral [simp]:  lp15@65583  2187  fixes x::complex shows "x \ 0 \ x powr (numeral n) = x ^ (numeral n)"  lp15@65583  2188  by (metis of_nat_numeral powr_complexpow)  lp15@65583  2189 eberlm@61524  2190 lemma cnj_powr:  eberlm@61524  2191  assumes "Im a = 0 \ Re a \ 0"  eberlm@61524  2192  shows "cnj (a powr b) = cnj a powr cnj b"  eberlm@61524  2193 proof (cases "a = 0")  eberlm@61524  2194  case False  paulson@62131  2195  with assms have "a \ \\<^sub>\\<^sub>0" by (auto simp: complex_eq_iff complex_nonpos_Reals_iff)  eberlm@61524  2196  with False show ?thesis by (simp add: powr_def exp_cnj cnj_Ln)  eberlm@61524  2197 qed simp  eberlm@61524  2198 lp15@60017  2199 lemma powr_real_real:  lp15@68281  2200  assumes "w \ \" "z \ \" "0 < Re w"  lp15@68281  2201  shows "w powr z = exp(Re z * ln(Re w))"  lp15@68281  2202 proof -  lp15@68281  2203  have "w \ 0"  lp15@68281  2204  using assms by auto  lp15@68281  2205  with assms show ?thesis  lp15@68281  2206  by (simp add: powr_def Ln_Reals_eq of_real_exp)  lp15@68281  2207 qed  lp15@60017  2208 lp15@60017  2209 lemma powr_of_real:  lp15@60020  2210  fixes x::real and y::real  eberlm@63296  2211  shows "0 \ x \ of_real x powr (of_real y::complex) = of_real (x powr y)"  eberlm@63296  2212  by (simp_all add: powr_def exp_eq_polar)  lp15@60017  2213 wl302@67706  2214 lemma powr_of_int:  wl302@67706  2215  fixes z::complex and n::int  wl302@67706  2216  assumes "z\(0::complex)"  wl302@67706  2217  shows "z powr of_int n = (if n\0 then z^nat n else inverse (z^nat (-n)))"  wl302@67706  2218  by (metis assms not_le of_int_of_nat powr_complexpow powr_minus)  wl302@67706  2219 eberlm@67135  2220 lemma powr_Reals_eq: "\x \ \; y \ \; Re x \ 0\ \ x powr y = of_real (Re x powr Re y)"  lp15@68257  2221  by (metis of_real_Re powr_of_real)  lp15@65719  2222 lp15@60017  2223 lemma norm_powr_real_mono:  lp15@60020  2224  "\w \ \; 1 < Re w\  lp15@60020  2225  \ cmod(w powr z1) \ cmod(w powr z2) \ Re z1 \ Re z2"  lp15@60020  2226  by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)  lp15@60017  2227 lp15@60017  2228 lemma powr_times_real:  lp15@60017  2229  "\x \ \; y \ \; 0 \ Re x; 0 \ Re y\  lp15@60017  2230  \ (x * y) powr z = x powr z * y powr z"  lp15@60020  2231  by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)  lp15@60017  2232 lp15@65719  2233 lemma Re_powr_le: "r \ \\<^sub>\\<^sub>0 \ Re (r powr z) \ Re r powr Re z"  lp15@65719  2234  by (auto simp: powr_def nonneg_Reals_def order_trans [OF complex_Re_le_cmod])  lp15@65719  2235 lp15@65719  2236 lemma  lp15@65719  2237  fixes w::complex  lp15@65719  2238  shows Reals_powr [simp]: "\w \ \\<^sub>\\<^sub>0; z \ \\ \ w powr z \ \"  lp15@65719  2239  and nonneg_Reals_powr [simp]: "\w \ \\<^sub>\\<^sub>0; z \ \\ \ w powr z \ \\<^sub>\\<^sub>0"  lp15@65719  2240  by (auto simp: nonneg_Reals_def Reals_def powr_of_real)  lp15@65719  2241 eberlm@61524  2242 lemma powr_neg_real_complex:  eberlm@61524  2243  shows "(- of_real x) powr a = (-1) powr (of_real (sgn x) * a) * of_real x powr (a :: complex)"  eberlm@61524  2244 proof (cases "x = 0")  eberlm@61524  2245  assume x: "x \ 0"  eberlm@61524  2246  hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)  eberlm@61524  2247  also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \"  eberlm@61524  2248  by (simp add: Ln_minus Ln_of_real)  wenzelm@63092  2249  also from x have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"  eberlm@61524  2250  by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)  eberlm@61524  2251  also note cis_pi  eberlm@61524  2252  finally show ?thesis by simp  eberlm@61524  2253 qed simp_all  eberlm@61524  2254 lp15@60017  2255 lemma has_field_derivative_powr:  paulson@62131  2256  fixes z :: complex  lp15@68257  2257  assumes "z \ \\<^sub>\\<^sub>0"  lp15@68257  2258  shows "((\z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"  lp15@68257  2259 proof (cases "z=0")  lp15@68257  2260  case False  lp15@68281  2261  show ?thesis  lp15@68281  2262  unfolding powr_def  lp15@68281  2263  proof (rule DERIV_transform_at)  lp15@68281  2264  show "((\z. exp (s * Ln z)) has_field_derivative s * (if z = 0 then 0 else exp ((s - 1) * Ln z)))  lp15@68281  2265  (at z)"  lp15@68281  2266  apply (intro derivative_eq_intros | simp add: assms)+  lp15@68281  2267  by (simp add: False divide_complex_def exp_diff left_diff_distrib')  lp15@68281  2268  qed (use False in auto)  lp15@68257  2269 qed (use assms in auto)  lp15@60017  2270 paulson@62131  2271 declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]  eberlm@61524  2272 wl302@67706  2273 lemma has_field_derivative_powr_of_int:  lp15@68493  2274  fixes z :: complex  wl302@67706  2275  assumes gderiv:"(g has_field_derivative gd) (at z within s)" and "g z\0"  wl302@67706  2276  shows "((\z. g z powr of_int n) has_field_derivative (n * g z powr (of_int n - 1) * gd)) (at z within s)"  wl302@67706  2277 proof -  wl302@67706  2278  define dd where "dd = of_int n * g z powr (of_int (n - 1)) * gd"  wl302@67706  2279  obtain e where "e>0" and e_dist:"\y\s. dist z y < e \ g y \ 0"  wl302@67706  2280  using DERIV_continuous[OF gderiv,THEN continuous_within_avoid] \g z\0\ by auto  wl302@67706  2281  have ?thesis when "n\0"  wl302@67706  2282  proof -  wl302@67706  2283  define dd' where "dd' = of_int n * g z ^ (nat n - 1) * gd"  wl302@67706  2284  have "dd=dd'"  wl302@67706  2285  proof (cases "n=0")  wl302@67706  2286  case False  wl302@67706  2287  then have "n-1 \0" using \n\0\ by auto  wl302@67706  2288  then have "g z powr (of_int (n - 1)) = g z ^ (nat n - 1)"  lp15@68493  2289  using powr_of_int[OF \g z\0\,of "n-1"] by (simp add: nat_diff_distrib')  wl302@67706  2290  then show ?thesis unfolding dd_def dd'_def by simp  wl302@67706  2291  qed (simp add:dd_def dd'_def)  wl302@67706  2292  then have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s)  wl302@67706  2293  \ ((\z. g z powr of_int n) has_field_derivative dd') (at z within s)"  wl302@67706  2294  by simp  wl302@67706  2295  also have "... \ ((\z. g z ^ nat n) has_field_derivative dd') (at z within s)"  lp15@68281  2296  proof (rule has_field_derivative_cong_eventually)  lp15@68281  2297  show "\\<^sub>F x in at z within s. g x powr of_int n = g x ^ nat n"  lp15@68281  2298  unfolding eventually_at  wl302@67706  2299  apply (rule exI[where x=e])  wl302@67706  2300  using powr_of_int that \e>0\ e_dist by (simp add: dist_commute)  lp15@68281  2301  qed (use powr_of_int \g z\0\ that in simp)  wl302@67706  2302  also have "..." unfolding dd'_def using gderiv that  wl302@67706  2303  by (auto intro!: derivative_eq_intros)  wl302@67706  2304  finally have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s)" .  wl302@67706  2305  then show ?thesis unfolding dd_def by simp  wl302@67706  2306  qed  wl302@67706  2307  moreover have ?thesis when "n<0"  wl302@67706  2308  proof -  wl302@67706  2309  define dd' where "dd' = of_int n / g z ^ (nat (1 - n)) * gd"  wl302@67706  2310  have "dd=dd'"  wl302@67706  2311  proof -  wl302@67706  2312  have "g z powr of_int (n - 1) = inverse (g z ^ nat (1-n))"  wl302@67706  2313  using powr_of_int[OF \g z\0\,of "n-1"] that by auto  wl302@67706  2314  then show ?thesis  wl302@67706  2315  unfolding dd_def dd'_def by (simp add: divide_inverse)  wl302@67706  2316  qed  wl302@67706  2317  then have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s)  wl302@67706  2318  \ ((\z. g z powr of_int n) has_field_derivative dd') (at z within s)"  wl302@67706  2319  by simp  wl302@67706  2320  also have "... \ ((\z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within s)"  lp15@68281  2321  proof (rule has_field_derivative_cong_eventually)  lp15@68281  2322  show "\\<^sub>F x in at z within s. g x powr of_int n = inverse (g x ^ nat (- n))"  lp15@68281  2323  unfolding eventually_at  wl302@67706  2324  apply (rule exI[where x=e])  wl302@67706  2325  using powr_of_int that \e>0\ e_dist by (simp add: dist_commute)  lp15@68281  2326  qed (use powr_of_int \g z\0\ that in simp)  lp15@68281  2327  also have "..."  lp15@68281  2328  proof -  lp15@68281  2329  have "nat (- n) + nat (1 - n) - Suc 0 = nat (- n) + nat (- n)"  lp15@68281  2330  by auto  lp15@68281  2331  then show ?thesis  lp15@68281  2332  unfolding dd'_def using gderiv that \g z\0\  lp15@68281  2333  by (auto intro!: derivative_eq_intros simp add:divide_simps power_add[symmetric])  lp15@68281  2334  qed  wl302@67706  2335  finally have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s)" .  wl302@67706  2336  then show ?thesis unfolding dd_def by simp  wl302@67706  2337  qed  wl302@67706  2338  ultimately show ?thesis by force  wl302@67706  2339 qed  wl302@67706  2340