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