Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Complex_Transcendental.thy Sprache: Isabelle

Original von: Isabelle^©

section \<open>Complex Transcendental Functions\<close>

text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close>

theory Complex_Transcendental
imports
 Complex_Analysis_Basics Summation_Tests "HOL-Library.Periodic_Fun"
begin

subsection\<open>Möbius transformations\<close>

(* TODO: Figure out what to do with Möbius transformations *)
definition\<^marker>\<open>tag important\<close> "moebius a b c d \<equiv> (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))"

theorem moebius_inverse:
 assumes "a * d \ b * c" "c * z + d \ 0"
 shows "moebius d (-b) (-c) a (moebius a b c d z) = z"
proof -
 from assms have "(-c) * moebius a b c d z + a \ 0" unfolding moebius_def
 by (simp add: field_simps)
 with assms show ?thesis
 unfolding moebius_def by (simp add: moebius_def divide_simps) (simp add: algebra_simps)?
qed

lemma moebius_inverse':
 assumes "a * d \ b * c" "c * z - a \ 0"
 shows "moebius a b c d (moebius d (-b) (-c) a z) = z"
 using assms moebius_inverse[of d a "-b" "-c" z]
 by (auto simp: algebra_simps)

lemma cmod_add_real_less:
 assumes "Im z \ 0" "r\0"
 shows "cmod (z + r) < cmod z + \r\"
proof (cases z)
 case (Complex x y)
 then have "0 < y * y"
 using assms mult_neg_neg by force
 with assms have "r * x / \r\ < sqrt (x*x + y*y)"
 by (simp add: real_less_rsqrt power2_eq_square)
 then show ?thesis using assms Complex
 apply (simp add: cmod_def)
 apply (rule power2_less_imp_less, auto)
 apply (simp add: power2_eq_square field_simps)
 done
qed

lemma cmod_diff_real_less: "Im z \ 0 \ x\0 \ cmod (z - x) < cmod z + \x\"
 using cmod_add_real_less [of z "-x"]
 by simp

lemma cmod_square_less_1_plus:
 assumes "Im z = 0 \ \Re z\ < 1"
 shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
proof (cases "Im z = 0 \ Re z = 0")
 case True
 with assms abs_square_less_1 show ?thesis
 by (force simp add: Re_power2 Im_power2 cmod_def)
next
 case False
 with cmod_diff_real_less [of "1 - z\<^sup>2" "1"] show ?thesis
 by (simp add: norm_power Im_power2)
qed

subsection\<^marker>\<open>tag unimportant\<close>\<open>The Exponential Function\<close>

lemma norm_exp_i_times [simp]: "norm (exp(\ * of_real y)) = 1"
 by simp

lemma norm_exp_imaginary: "norm(exp z) = 1 \ Re z = 0"
 by simp

lemma field_differentiable_within_exp: "exp field_differentiable (at z within s)"
 using DERIV_exp field_differentiable_at_within field_differentiable_def by blast

lemma continuous_within_exp:
 fixes z::"'a::{real_normed_field,banach}"
 shows "continuous (at z within s) exp"
by (simp add: continuous_at_imp_continuous_within)

lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"
 by (simp add: field_differentiable_within_exp holomorphic_on_def)

lemma holomorphic_on_exp' [holomorphic_intros]:
 "f holomorphic_on s \ (\x. exp (f x)) holomorphic_on s"
 using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def)

subsection\<open>Euler and de Moivre formulas\<close>

text\<open>The sine series times \<^term>\<open>i\<close>\<close>
lemma sin_i_eq: "(\n. (\ * sin_coeff n) * z^n) sums (\ * sin z)"
proof -
 have "(\n. \ * sin_coeff n *\<^sub>R z^n) sums (\ * sin z)"
 using sin_converges sums_mult by blast
 then show ?thesis
 by (simp add: scaleR_conv_of_real field_simps)
qed

theorem exp_Euler: "exp(\ * z) = cos(z) + \ * sin(z)"
proof -
 have "(\n. (cos_coeff n + \ * sin_coeff n) * z^n) = (\n. (\ * z) ^ n /\<^sub>R (fact n))"
 proof
 fix n
 show "(cos_coeff n + \ * sin_coeff n) * z^n = (\ * z) ^ n /\<^sub>R (fact n)"
 by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
 qed
 also have "... sums (exp (\ * z))"
 by (rule exp_converges)
 finally have "(\n. (cos_coeff n + \ * sin_coeff n) * z^n) sums (exp (\ * z))" .
 moreover have "(\n. (cos_coeff n + \ * sin_coeff n) * z^n) sums (cos z + \ * sin z)"
 using sums_add [OF cos_converges [of z] sin_i_eq [of z]]
 by (simp add: field_simps scaleR_conv_of_real)
 ultimately show ?thesis
 using sums_unique2 by blast
qed

corollary\<^marker>\<open>tag unimportant\<close> exp_minus_Euler: "exp(-(\ * z)) = cos(z) - \ * sin(z)"
 using exp_Euler [of "-z"]
 by simp

lemma sin_exp_eq: "sin z = (exp(\ * z) - exp(-(\ * z))) / (2*\)"
 by (simp add: exp_Euler exp_minus_Euler)

lemma sin_exp_eq': "sin z = \ * (exp(-(\ * z)) - exp(\ * z)) / 2"
 by (simp add: exp_Euler exp_minus_Euler)

lemma cos_exp_eq: "cos z = (exp(\ * z) + exp(-(\ * z))) / 2"
 by (simp add: exp_Euler exp_minus_Euler)

theorem Euler: "exp(z) = of_real(exp(Re z)) *
 (of_real(cos(Im z)) + \ * of_real(sin(Im z)))"
by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real Complex_eq)

lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
 by (simp add: sin_exp_eq field_simps Re_divide Im_exp)

lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
 by (simp add: sin_exp_eq field_simps Im_divide Re_exp)

lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
 by (simp add: cos_exp_eq field_simps Re_divide Re_exp)

lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
 by (simp add: cos_exp_eq field_simps Im_divide Im_exp)

lemma Re_sin_pos: "0 < Re z \ Re z < pi \ Re (sin z) > 0"
 by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)

lemma Im_sin_nonneg: "Re z = 0 \ 0 \ Im z \ 0 \ Im (sin z)"
 by (simp add: Re_sin Im_sin algebra_simps)

lemma Im_sin_nonneg2: "Re z = pi \ Im z \ 0 \ 0 \ Im (sin z)"
 by (simp add: Re_sin Im_sin algebra_simps)

subsection\<^marker>\<open>tag unimportant\<close>\<open>Relationships between real and complex trigonometric and hyperbolic functions\<close>

lemma real_sin_eq [simp]: "Re(sin(of_real x)) = sin x"
 by (simp add: sin_of_real)

lemma real_cos_eq [simp]: "Re(cos(of_real x)) = cos x"
 by (simp add: cos_of_real)

lemma DeMoivre: "(cos z + \ * sin z) ^ n = cos(n * z) + \ * sin(n * z)"
 by (metis exp_Euler [symmetric] exp_of_nat_mult mult.left_commute)

lemma exp_cnj: "cnj (exp z) = exp (cnj z)"
proof -
 have "(\n. cnj (z ^ n /\<^sub>R (fact n))) = (\n. (cnj z)^n /\<^sub>R (fact n))"
 by auto
 also have "... sums (exp (cnj z))"
 by (rule exp_converges)
 finally have "(\n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
 moreover have "(\n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
 by (metis exp_converges sums_cnj)
 ultimately show ?thesis
 using sums_unique2
 by blast
qed

lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
 by (simp add: sin_exp_eq exp_cnj field_simps)

lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
 by (simp add: cos_exp_eq exp_cnj field_simps)

lemma field_differentiable_at_sin: "sin field_differentiable at z"
 using DERIV_sin field_differentiable_def by blast

lemma field_differentiable_within_sin: "sin field_differentiable (at z within S)"
 by (simp add: field_differentiable_at_sin field_differentiable_at_within)

lemma field_differentiable_at_cos: "cos field_differentiable at z"
 using DERIV_cos field_differentiable_def by blast

lemma field_differentiable_within_cos: "cos field_differentiable (at z within S)"
 by (simp add: field_differentiable_at_cos field_differentiable_at_within)

lemma holomorphic_on_sin: "sin holomorphic_on S"
 by (simp add: field_differentiable_within_sin holomorphic_on_def)

lemma holomorphic_on_cos: "cos holomorphic_on S"
 by (simp add: field_differentiable_within_cos holomorphic_on_def)

lemma holomorphic_on_sin' [holomorphic_intros]:
 assumes "f holomorphic_on A"
 shows "(\x. sin (f x)) holomorphic_on A"
 using holomorphic_on_compose[OF assms holomorphic_on_sin] by (simp add: o_def)

lemma holomorphic_on_cos' [holomorphic_intros]:
 assumes "f holomorphic_on A"
 shows "(\x. cos (f x)) holomorphic_on A"
 using holomorphic_on_compose[OF assms holomorphic_on_cos] by (simp add: o_def)

subsection\<^marker>\<open>tag unimportant\<close>\<open>More on the Polar Representation of Complex Numbers\<close>

lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
 by (simp add: Complex_eq exp_add exp_Euler exp_of_real sin_of_real cos_of_real)

lemma exp_eq_1: "exp z = 1 \ Re(z) = 0 \ (\n::int. Im(z) = of_int (2 * n) * pi)"
 (is "?lhs = ?rhs")
proof
 assume "exp z = 1"
 then have "Re z = 0"
 by (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
 with \<open>?lhs\<close> show ?rhs
 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)
next
 assume ?rhs then show ?lhs
 using Im_exp Re_exp complex_eq_iff
 by (simp add: cos_one_2pi_int cos_one_sin_zero mult.commute)
qed

lemma exp_eq: "exp w = exp z \ (\n::int. w = z + (of_int (2 * n) * pi) * \)"
 (is "?lhs = ?rhs")
proof -
 have "exp w = exp z \ exp (w-z) = 1"
 by (simp add: exp_diff)
 also have "... \ (Re w = Re z \ (\n::int. Im w - Im z = of_int (2 * n) * pi))"
 by (simp add: exp_eq_1)
 also have "... \ ?rhs"
 by (auto simp: algebra_simps intro!: complex_eqI)
 finally show ?thesis .
qed

lemma exp_complex_eqI: "\Im w - Im z\ < 2*pi \ exp w = exp z \ w = z"
 by (auto simp: exp_eq abs_mult)

lemma exp_integer_2pi:
 assumes "n \ \"
 shows "exp((2 * n * pi) * \) = 1"
proof -
 have "exp((2 * n * pi) * \) = exp 0"
 using assms unfolding Ints_def exp_eq by auto
 also have "... = 1"
 by simp
 finally show ?thesis .
qed

lemma exp_plus_2pin [simp]: "exp (z + \ * (of_int n * (of_real pi * 2))) = exp z"
 by (simp add: exp_eq)

lemma exp_integer_2pi_plus1:
 assumes "n \ \"
 shows "exp(((2 * n + 1) * pi) * \) = - 1"
proof -
 from assms obtain n' where [simp]: "n = of_int n'"
 by (auto simp: Ints_def)
 have "exp(((2 * n + 1) * pi) * \) = exp (pi * \)"
 using assms by (subst exp_eq) (auto intro!: exI[of _ n'] simp: algebra_simps)
 also have "... = - 1"
 by simp
 finally show ?thesis .
qed

lemma inj_on_exp_pi:
 fixes z::complex shows "inj_on exp (ball z pi)"
proof (clarsimp simp: inj_on_def exp_eq)
 fix y n
 assume "dist z (y + 2 * of_int n * of_real pi * \) < pi"
 "dist z y < pi"
 then have "dist y (y + 2 * of_int n * of_real pi * \) < pi+pi"
 using dist_commute_lessI dist_triangle_less_add by blast
 then have "norm (2 * of_int n * of_real pi * \) < 2*pi"
 by (simp add: dist_norm)
 then show "n = 0"
 by (auto simp: norm_mult)
qed

lemma cmod_add_squared:
 fixes r1 r2::real
 assumes "r1 \ 0" "r2 \ 0"
 shows "(cmod (r1 * exp (\ * \1) + r2 * exp (\ * \2)))\<^sup>2 = r1\<^sup>2 + r2\<^sup>2 + 2 * r1 * r2 * cos (\1 - \2)" (is "(cmod (?z1 + ?z2))\<^sup>2 = ?rhs")
proof -
 have "(cmod (?z1 + ?z2))\<^sup>2 = (?z1 + ?z2) * cnj (?z1 + ?z2)"
 by (rule complex_norm_square)
 also have "\ = (?z1 * cnj ?z1 + ?z2 * cnj ?z2) + (?z1 * cnj ?z2 + cnj ?z1 * ?z2)"
 by (simp add: algebra_simps)
 also have "\ = (norm ?z1)\<^sup>2 + (norm ?z2)\<^sup>2 + 2 * Re (?z1 * cnj ?z2)"
 unfolding complex_norm_square [symmetric] cnj_add_mult_eq_Re by simp
 also have "\ = ?rhs"
 by (simp add: norm_mult) (simp add: exp_Euler complex_is_Real_iff [THEN iffD1] cos_diff algebra_simps)
 finally show ?thesis
 using of_real_eq_iff by blast
qed

lemma cmod_diff_squared:
 fixes r1 r2::real
 assumes "r1 \ 0" "r2 \ 0"
 shows "(cmod (r1 * exp (\ * \1) - r2 * exp (\ * \2)))\<^sup>2 = r1\<^sup>2 + r2\<^sup>2 - 2*r1*r2*cos (\1 - \2)" (is "(cmod (?z1 - ?z2))\<^sup>2 = ?rhs")
proof -
 have "exp (\ * (\2 + pi)) = - exp (\ * \2)"
 by (simp add: exp_Euler cos_plus_pi sin_plus_pi)
 then have "(cmod (?z1 - ?z2))\<^sup>2 = cmod (?z1 + r2 * exp (\ * (\2 + pi))) ^2"
 by simp
 also have "\ = r1\<^sup>2 + r2\<^sup>2 + 2*r1*r2*cos (\1 - (\2 + pi))"
 using assms cmod_add_squared by blast
 also have "\ = ?rhs"
 by (simp add: add.commute diff_add_eq_diff_diff_swap)
 finally show ?thesis .
qed

lemma polar_convergence:
 fixes R::real
 assumes "\j. r j > 0" "R > 0"
 shows "((\j. r j * exp (\ * \ j)) \ (R * exp (\ * \))) \
 (r \<longlonglongrightarrow> R) \<and> (\<exists>k. (\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> \<Theta>)" (is "(?z \<longlonglongrightarrow> ?Z) = ?rhs")
proof
 assume L: "?z \ ?Z"
 have rR: "r \ R"
 using tendsto_norm [OF L] assms by (auto simp: norm_mult abs_of_pos)
 moreover obtain k where "(\j. \ j - of_int (k j) * (2 * pi)) \ \"
 proof -
 have "cos (\ j - \) = ((r j)\<^sup>2 + R\<^sup>2 - (norm(?z j - ?Z))\<^sup>2) / (2 * R * r j)" for j
 apply (subst cmod_diff_squared)
 using assms by (auto simp: field_split_simps less_le)
 moreover have "(\j. ((r j)\<^sup>2 + R\<^sup>2 - (norm(?z j - ?Z))\<^sup>2) / (2 * R * r j)) \ ((R\<^sup>2 + R\<^sup>2 - (norm(?Z - ?Z))\<^sup>2) / (2 * R * R))"
 by (intro L rR tendsto_intros) (use \<open>R > 0\<close> in force)
 moreover have "((R\<^sup>2 + R\<^sup>2 - (norm(?Z - ?Z))\<^sup>2) / (2 * R * R)) = 1"
 using \<open>R > 0\<close> by (simp add: power2_eq_square field_split_simps)
 ultimately have "(\j. cos (\ j - \)) \ 1"
 by auto
 then show ?thesis
 using that cos_diff_limit_1 by blast
 qed
 ultimately show ?rhs
 by metis
next
 assume R: ?rhs
 show "?z \ ?Z"
 proof (rule tendsto_mult)
 show "(\x. complex_of_real (r x)) \ of_real R"
 using R by (auto simp: tendsto_of_real_iff)
 obtain k where "(\j. \ j - of_int (k j) * (2 * pi)) \ \"
 using R by metis
 then have "(\j. complex_of_real (\ j - of_int (k j) * (2 * pi))) \ of_real \"
 using tendsto_of_real_iff by force
 then have "(\j. exp (\ * of_real (\ j - of_int (k j) * (2 * pi)))) \ exp (\ * \)"
 using tendsto_mult [OF tendsto_const] isCont_exp isCont_tendsto_compose by blast
 moreover have "exp (\ * of_real (\ j - of_int (k j) * (2 * pi))) = exp (\ * \ j)" for j
 unfolding exp_eq
 by (rule_tac x="- k j" in exI) (auto simp: algebra_simps)
 ultimately show "(\j. exp (\ * \ j)) \ exp (\ * \)"
 by auto
 qed
qed

lemma sin_cos_eq_iff: "sin y = sin x \ cos y = cos x \ (\n::int. y = x + 2 * pi * n)"
proof -
 { assume "sin y = sin x" "cos y = cos x"
 then have "cos (y-x) = 1"
 using cos_add [of y "-x"] by simp
 then have "\n::int. y-x = 2 * pi * n"
 using cos_one_2pi_int by auto }
 then show ?thesis
 apply (auto simp: sin_add cos_add)
 apply (metis add.commute diff_add_cancel)
 done
qed

lemma exp_i_ne_1:
 assumes "0 < x" "x < 2*pi"
 shows "exp(\ * of_real x) \ 1"
proof
 assume "exp (\ * of_real x) = 1"
 then have "exp (\ * of_real x) = exp 0"
 by simp
 then obtain n where "\ * of_real x = (of_int (2 * n) * pi) * \"
 by (simp only: Ints_def exp_eq) auto
 then have "of_real x = (of_int (2 * n) * pi)"
 by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
 then have "x = (of_int (2 * n) * pi)"
 by simp
 then show False using assms
 by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
qed

lemma sin_eq_0:
 fixes z::complex
 shows "sin z = 0 \ (\n::int. z = of_real(n * pi))"
 by (simp add: sin_exp_eq exp_eq)

lemma cos_eq_0:
 fixes z::complex
 shows "cos z = 0 \ (\n::int. z = of_real(n * pi) + of_real pi/2)"
 using sin_eq_0 [of "z - of_real pi/2"]
 by (simp add: sin_diff algebra_simps)

lemma cos_eq_1:
 fixes z::complex
 shows "cos z = 1 \ (\n::int. z = of_real(2 * n * pi))"
proof -
 have "cos z = cos (2*(z/2))"
 by simp
 also have "... = 1 - 2 * sin (z/2) ^ 2"
 by (simp only: cos_double_sin)
 finally have [simp]: "cos z = 1 \ sin (z/2) = 0"
 by simp
 show ?thesis
 by (auto simp: sin_eq_0)
qed

lemma csin_eq_1:
 fixes z::complex
 shows "sin z = 1 \ (\n::int. z = of_real(2 * n * pi) + of_real pi/2)"
 using cos_eq_1 [of "z - of_real pi/2"]
 by (simp add: cos_diff algebra_simps)

lemma csin_eq_minus1:
 fixes z::complex
 shows "sin z = -1 \ (\n::int. z = of_real(2 * n * pi) + 3/2*pi)"
 (is "_ = ?rhs")
proof -
 have "sin z = -1 \ sin (-z) = 1"
 by (simp add: equation_minus_iff)
 also have "... \ (\n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
 by (simp only: csin_eq_1)
 also have "... \ (\n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
 by (rule iff_exI) (metis add.inverse_inverse add_uminus_conv_diff minus_add_distrib)
 also have "... = ?rhs"
 apply safe
 apply (rule_tac [2] x="-(x+1)" in exI)
 apply (rule_tac x="-(x+1)" in exI)
 apply (simp_all add: algebra_simps)
 done
 finally show ?thesis .
qed

lemma ccos_eq_minus1:
 fixes z::complex
 shows "cos z = -1 \ (\n::int. z = of_real(2 * n * pi) + pi)"
 using csin_eq_1 [of "z - of_real pi/2"]
 by (simp add: sin_diff algebra_simps equation_minus_iff)

lemma sin_eq_1: "sin x = 1 \ (\n::int. x = (2 * n + 1 / 2) * pi)"
 (is "_ = ?rhs")
proof -
 have "sin x = 1 \ sin (complex_of_real x) = 1"
 by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
 also have "... \ (\n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
 by (simp only: csin_eq_1)
 also have "... \ (\n::int. x = of_real(2 * n * pi) + of_real pi/2)"
 by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])
 also have "... = ?rhs"
 by (auto simp: algebra_simps)
 finally show ?thesis .
qed

lemma sin_eq_minus1: "sin x = -1 \ (\n::int. x = (2*n + 3/2) * pi)" (is "_ = ?rhs")
proof -
 have "sin x = -1 \ sin (complex_of_real x) = -1"
 by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
 also have "... \ (\n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
 by (simp only: csin_eq_minus1)
 also have "... \ (\n::int. x = of_real(2 * n * pi) + 3/2*pi)"
 by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])
 also have "... = ?rhs"
 by (auto simp: algebra_simps)
 finally show ?thesis .
qed

lemma cos_eq_minus1: "cos x = -1 \ (\n::int. x = (2*n + 1) * pi)"
 (is "_ = ?rhs")
proof -
 have "cos x = -1 \ cos (complex_of_real x) = -1"
 by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
 also have "... \ (\n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
 by (simp only: ccos_eq_minus1)
 also have "... \ (\n::int. x = of_real(2 * n * pi) + pi)"
 by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])
 also have "... = ?rhs"
 by (auto simp: algebra_simps)
 finally show ?thesis .
qed

lemma dist_exp_i_1: "norm(exp(\ * of_real t) - 1) = 2 * \sin(t / 2)\"
proof -
 have "sqrt (2 - cos t * 2) = 2 * \sin (t / 2)\"
 using cos_double_sin [of "t/2"] by (simp add: real_sqrt_mult)
 then show ?thesis
 by (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
qed

lemma sin_cx_2pi [simp]: "\z = of_int m; even m\ \ sin (z * complex_of_real pi) = 0"
 by (simp add: sin_eq_0)

lemma cos_cx_2pi [simp]: "\z = of_int m; even m\ \ cos (z * complex_of_real pi) = 1"
 using cos_eq_1 by auto

lemma complex_sin_eq:
 fixes w :: complex
 shows "sin w = sin z \ (\n \ \. w = z + of_real(2*n*pi) \ w = -z + of_real((2*n + 1)*pi))"
 (is "?lhs = ?rhs")
proof
 assume ?lhs
 then have "sin w - sin z = 0"
 by (auto simp: algebra_simps)
 then have "sin ((w - z) / 2)*cos ((w + z) / 2) = 0"
 by (auto simp: sin_diff_sin)
 then consider "sin ((w - z) / 2) = 0" | "cos ((w + z) / 2) = 0"
 using mult_eq_0_iff by blast
 then show ?rhs
 proof cases
 case 1
 then show ?thesis
 by (simp add: sin_eq_0 algebra_simps) (metis Ints_of_int of_real_of_int_eq)
 next
 case 2
 then show ?thesis
 by (simp add: cos_eq_0 algebra_simps) (metis Ints_of_int of_real_of_int_eq)
 qed
next
 assume ?rhs
 then consider n::int where "w = z + of_real (2 * of_int n * pi)"
 | n::int where " w = -z + of_real ((2 * of_int n + 1) * pi)"
 using Ints_cases by blast
 then show ?lhs
 proof cases
 case 1
 then show ?thesis
 using Periodic_Fun.sin.plus_of_int [of z n]
 by (auto simp: algebra_simps)
 next
 case 2
 then show ?thesis
 using Periodic_Fun.sin.plus_of_int [of "-z" "n"]
 apply (simp add: algebra_simps)
 by (metis add.commute add.inverse_inverse add_diff_cancel_left diff_add_cancel sin_plus_pi)
 qed
qed

lemma complex_cos_eq:
 fixes w :: complex
 shows "cos w = cos z \ (\n \ \. w = z + of_real(2*n*pi) \ w = -z + of_real(2*n*pi))"
 (is "?lhs = ?rhs")
proof
 assume ?lhs
 then have "cos w - cos z = 0"
 by (auto simp: algebra_simps)
 then have "sin ((w + z) / 2) * sin ((z - w) / 2) = 0"
 by (auto simp: cos_diff_cos)
 then consider "sin ((w + z) / 2) = 0" | "sin ((z - w) / 2) = 0"
 using mult_eq_0_iff by blast
 then show ?rhs
 proof cases
 case 1
 then obtain n where "w + z = of_int n * (complex_of_real pi * 2)"
 by (auto simp: sin_eq_0 algebra_simps)
 then have "w = -z + of_real(2 * of_int n * pi)"
 by (auto simp: algebra_simps)
 then show ?thesis
 using Ints_of_int by blast
 next
 case 2
 then obtain n where "z = w + of_int n * (complex_of_real pi * 2)"
 by (auto simp: sin_eq_0 algebra_simps)
 then have "w = z + complex_of_real (2 * of_int(-n) * pi)"
 by (auto simp: algebra_simps)
 then show ?thesis
 using Ints_of_int by blast
 qed
next
 assume ?rhs
 then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \
 w = -z + of_real(2*n*pi)"
 using Ints_cases by (metis of_int_mult of_int_numeral)
 then show ?lhs
 using Periodic_Fun.cos.plus_of_int [of z n]
 apply (simp add: algebra_simps)
 by (metis cos.plus_of_int cos_minus minus_add_cancel mult.commute)
qed

lemma sin_eq:
 "sin x = sin y \ (\n \ \. x = y + 2*n*pi \ x = -y + (2*n + 1)*pi)"
 using complex_sin_eq [of x y]
 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)

lemma cos_eq:
 "cos x = cos y \ (\n \ \. x = y + 2*n*pi \ x = -y + 2*n*pi)"
 using complex_cos_eq [of x y]
 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)

lemma sinh_complex:
 fixes z :: complex
 shows "(exp z - inverse (exp z)) / 2 = -\ * sin(\ * z)"
 by (simp add: sin_exp_eq field_split_simps exp_minus)

lemma sin_i_times:
 fixes z :: complex
 shows "sin(\ * z) = \ * ((exp z - inverse (exp z)) / 2)"
 using sinh_complex by auto

lemma sinh_real:
 fixes x :: real
 shows "of_real((exp x - inverse (exp x)) / 2) = -\ * sin(\ * of_real x)"
 by (simp add: exp_of_real sin_i_times)

lemma cosh_complex:
 fixes z :: complex
 shows "(exp z + inverse (exp z)) / 2 = cos(\ * z)"
 by (simp add: cos_exp_eq field_split_simps exp_minus exp_of_real)

lemma cosh_real:
 fixes x :: real
 shows "of_real((exp x + inverse (exp x)) / 2) = cos(\ * of_real x)"
 by (simp add: cos_exp_eq field_split_simps exp_minus exp_of_real)

lemmas cos_i_times = cosh_complex [symmetric]

lemma norm_cos_squared:
 "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
proof (cases z)
 case (Complex x1 x2)
 then show ?thesis
 apply (simp only: cos_add cmod_power2 cos_of_real sin_of_real Complex_eq)
 apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
 apply (simp only: left_diff_distrib [symmetric] power_mult_distrib sin_squared_eq)
 apply (simp add: power2_eq_square field_split_simps)
 done
qed

lemma norm_sin_squared:
 "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
proof (cases z)
 case (Complex x1 x2)
 then show ?thesis
 apply (simp only: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq)
 apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
 apply (simp only: left_diff_distrib [symmetric] power_mult_distrib cos_squared_eq)
 apply (simp add: power2_eq_square field_split_simps)
 done
qed

lemma exp_uminus_Im: "exp (- Im z) \ exp (cmod z)"
 using abs_Im_le_cmod linear order_trans by fastforce

lemma norm_cos_le:
 fixes z::complex
 shows "norm(cos z) \ exp(norm z)"
proof -
 have "Im z \ cmod z"
 using abs_Im_le_cmod abs_le_D1 by auto
 then have "exp (- Im z) + exp (Im z) \ exp (cmod z) * 2"
 by (metis exp_uminus_Im add_mono exp_le_cancel_iff mult_2_right)
 then show ?thesis
 by (force simp add: cos_exp_eq norm_divide intro: order_trans [OF norm_triangle_ineq])
qed

lemma norm_cos_plus1_le:
 fixes z::complex
 shows "norm(1 + cos z) \ 2 * exp(norm z)"
proof -
 have mono: "\u w z::real. (1 \ w | 1 \ z) \ (w \ u & z \ u) \ 2 + w + z \ 4 * u"
 by arith
 have *: "Im z \ cmod z"
 using abs_Im_le_cmod abs_le_D1 by auto
 have triangle3: "\x y z. norm(x + y + z) \ norm(x) + norm(y) + norm(z)"
 by (simp add: norm_add_rule_thm)
 have "norm(1 + cos z) = cmod (1 + (exp (\ * z) + exp (- (\ * z))) / 2)"
 by (simp add: cos_exp_eq)
 also have "... = cmod ((2 + exp (\ * z) + exp (- (\ * z))) / 2)"
 by (simp add: field_simps)
 also have "... = cmod (2 + exp (\ * z) + exp (- (\ * z))) / 2"
 by (simp add: norm_divide)
 finally show ?thesis
 by (metis exp_eq_one_iff exp_le_cancel_iff mult_2 norm_cos_le norm_ge_zero norm_one norm_triangle_mono)
qed

lemma sinh_conv_sin: "sinh z = -\ * sin (\*z)"
 by (simp add: sinh_field_def sin_i_times exp_minus)

lemma cosh_conv_cos: "cosh z = cos (\*z)"
 by (simp add: cosh_field_def cos_i_times exp_minus)

lemma tanh_conv_tan: "tanh z = -\ * tan (\*z)"
 by (simp add: tanh_def sinh_conv_sin cosh_conv_cos tan_def)

lemma sin_conv_sinh: "sin z = -\ * sinh (\*z)"
 by (simp add: sinh_conv_sin)

lemma cos_conv_cosh: "cos z = cosh (\*z)"
 by (simp add: cosh_conv_cos)

lemma tan_conv_tanh: "tan z = -\ * tanh (\*z)"
 by (simp add: tan_def sin_conv_sinh cos_conv_cosh tanh_def)

lemma sinh_complex_eq_iff:
 "sinh (z :: complex) = sinh w \
 (\<exists>n\<in>\<int>. z = w - 2 * \ * of_real n * of_real pi \<or>
 z = -(2 * complex_of_real n + 1) * \ * complex_of_real pi - w)" (is "_ = ?rhs")
proof -
 have "sinh z = sinh w \ sin (\ * z) = sin (\ * w)"
 by (simp add: sinh_conv_sin)
 also have "\ \ ?rhs"
 by (subst complex_sin_eq) (force simp: field_simps complex_eq_iff)
 finally show ?thesis .
qed

subsection\<^marker>\<open>tag unimportant\<close>\<open>Taylor series for complex exponential, sine and cosine\<close>

declare power_Suc [simp del]

lemma Taylor_exp_field:
 fixes z::"'a::{banach,real_normed_field}"
 shows "norm (exp z - (\i\n. z ^ i / fact i)) \ exp (norm z) * (norm z ^ Suc n) / fact n"
proof (rule field_Taylor[of _ n "\k. exp" "exp (norm z)" 0 z, simplified])
 show "convex (closed_segment 0 z)"
 by (rule convex_closed_segment [of 0 z])
next
 fix k x
 assume "x \ closed_segment 0 z" "k \ n"
 show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
 using DERIV_exp DERIV_subset by blast
next
 fix x
 assume x: "x \ closed_segment 0 z"
 have "norm (exp x) \ exp (norm x)"
 by (rule norm_exp)
 also have "norm x \ norm z"
 using x by (auto simp: closed_segment_def intro!: mult_left_le_one_le)
 finally show "norm (exp x) \ exp (norm z)"
 by simp
qed auto

lemma Taylor_exp:
 "norm(exp z - (\k\n. z ^ k / (fact k))) \ exp\Re z\ * (norm z) ^ (Suc n) / (fact n)"
proof (rule complex_Taylor [of _ n "\k. exp" "exp\Re z\" 0 z, simplified])
 show "convex (closed_segment 0 z)"
 by (rule convex_closed_segment [of 0 z])
next
 fix k x
 assume "x \ closed_segment 0 z" "k \ n"
 show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
 using DERIV_exp DERIV_subset by blast
next
 fix x
 assume "x \ closed_segment 0 z"
 then obtain u where u: "x = complex_of_real u * z" "0 \ u" "u \ 1"
 by (auto simp: closed_segment_def scaleR_conv_of_real)
 then have "u * Re z \ \Re z\"
 by (metis abs_ge_self abs_ge_zero mult.commute mult.right_neutral mult_mono)
 then show "Re x \ \Re z\"
 by (simp add: u)
qed auto

lemma
 assumes "0 \ u" "u \ 1"
 shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \ exp \Im z\"
 and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \ exp \Im z\"
proof -
 have mono: "\u w z::real. w \ u \ z \ u \ (w + z)/2 \ u"
 by simp
 have *: "(cmod (exp (\ * (u * z))) + cmod (exp (- (\ * (u * z)))) ) / 2 \ exp \Im z\"
 proof (rule mono)
 show "cmod (exp (\ * (u * z))) \ exp \Im z\"
 using assms
 by (auto simp: abs_if mult_left_le_one_le not_less intro: order_trans [of _ 0])
 show "cmod (exp (- (\ * (u * z)))) \ exp \Im z\"
 using assms
 by (auto simp: abs_if mult_left_le_one_le mult_nonneg_nonpos intro: order_trans [of _ 0])
 qed
 have "cmod (sin (u *\<^sub>R z)) = cmod (exp (\ * (u * z)) - exp (- (\ * (u * z)))) / 2"
 by (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
 also have "... \ (cmod (exp (\ * (u * z))) + cmod (exp (- (\ * (u * z)))) ) / 2"
 by (intro divide_right_mono norm_triangle_ineq4) simp
 also have "... \ exp \Im z\"
 by (rule *)
 finally show "cmod (sin (u *\<^sub>R z)) \ exp \Im z\" .
 have "cmod (cos (u *\<^sub>R z)) = cmod (exp (\ * (u * z)) + exp (- (\ * (u * z)))) / 2"
 by (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
 also have "... \ (cmod (exp (\ * (u * z))) + cmod (exp (- (\ * (u * z)))) ) / 2"
 by (intro divide_right_mono norm_triangle_ineq) simp
 also have "... \ exp \Im z\"
 by (rule *)
 finally show "cmod (cos (u *\<^sub>R z)) \ exp \Im z\" .
qed

lemma Taylor_sin:
 "norm(sin z - (\k\n. complex_of_real (sin_coeff k) * z ^ k))
 \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
proof -
 have mono: "\u w z::real. w \ u \ z \ u \ w + z \ u*2"
 by arith
 have *: "cmod (sin z -
 (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
 \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
 proof (rule complex_Taylor [of "closed_segment 0 z" n
 "\k x. (-1)^(k div 2) * (if even k then sin x else cos x)"
 "exp\Im z\" 0 z, simplified])
 fix k x
 show "((\x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
 (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
 (at x within closed_segment 0 z)"
 apply (auto simp: power_Suc)
 apply (intro derivative_eq_intros | simp)+
 done
 next
 fix x
 assume "x \ closed_segment 0 z"
 then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \ exp \Im z\"
 by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
 qed
 have **: "\k. complex_of_real (sin_coeff k) * z ^ k
 = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
 by (auto simp: sin_coeff_def elim!: oddE)
 show ?thesis
 by (simp add: ** order_trans [OF _ *])
qed

lemma Taylor_cos:
 "norm(cos z - (\k\n. complex_of_real (cos_coeff k) * z ^ k))
 \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
proof -
 have mono: "\u w z::real. w \ u \ z \ u \ w + z \ u*2"
 by arith
 have *: "cmod (cos z -
 (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
 \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
 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,
simplified])
 fix k x
 assume "x \ closed_segment 0 z" "k \ n"
 show "((\x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
 (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
 (at x within closed_segment 0 z)"
 apply (auto simp: power_Suc)
 apply (intro derivative_eq_intros | simp)+
 done
 next
 fix x
 assume "x \ closed_segment 0 z"
 then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \ exp \Im z\"
 by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
 qed
 have **: "\k. complex_of_real (cos_coeff k) * z ^ k
 = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
 by (auto simp: cos_coeff_def elim!: evenE)
 show ?thesis
 by (simp add: ** order_trans [OF _ *])
qed

declare power_Suc [simp]

text\<open>32-bit Approximation to e\<close>
lemma e_approx_32: "\exp(1) - 5837465777 / 2147483648\ \ (inverse(2 ^ 32)::real)"
 using Taylor_exp [of 1 14] exp_le
 apply (simp add: sum_distrib_right in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
 apply (simp only: pos_le_divide_eq [symmetric])
 done

lemma e_less_272: "exp 1 < (272/100::real)"
 using e_approx_32
 by (simp add: abs_if split: if_split_asm)

lemma ln_272_gt_1: "ln (272/100) > (1::real)"
 by (metis e_less_272 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)

text\<open>Apparently redundant. But many arguments involve integers.\<close>
lemma ln3_gt_1: "ln 3 > (1::real)"
 by (simp add: less_trans [OF ln_272_gt_1])

subsection\<open>The argument of a complex number (HOL Light version)\<close>

definition\<^marker>\<open>tag important\<close> is_Arg :: "[complex,real] \<Rightarrow> bool"
 where "is_Arg z r \ z = of_real(norm z) * exp(\ * of_real r)"

definition\<^marker>\<open>tag important\<close> Arg2pi :: "complex \<Rightarrow> real"
 where "Arg2pi z \ if z = 0 then 0 else THE t. 0 \ t \ t < 2*pi \ is_Arg z t"

lemma is_Arg_2pi_iff: "is_Arg z (r + of_int k * (2 * pi)) \ is_Arg z r"
 by (simp add: algebra_simps is_Arg_def)

lemma is_Arg_eqI:
 assumes r: "is_Arg z r" and s: "is_Arg z s" and rs: "abs (r-s) < 2*pi" and "z \ 0"
 shows "r = s"
proof -
 have zr: "z = (cmod z) * exp (\ * r)" and zs: "z = (cmod z) * exp (\ * s)"
 using r s by (auto simp: is_Arg_def)
 with \<open>z \<noteq> 0\<close> have eq: "exp (\ * r) = exp (\ * s)"
 by (metis mult_eq_0_iff mult_left_cancel)
 have "\ * r = \ * s"
 by (rule exp_complex_eqI) (use rs in \<open>auto simp: eq exp_complex_eqI\<close>)
 then show ?thesis
 by simp
qed

text\<open>This function returns the angle of a complex number from its representation in polar coordinates.
Due to periodicity, its range is arbitrary. \<^term>\<open>Arg2pi\<close> follows HOL Light in adopting the interval \<open>[0,2\<pi>)\<close>.
But we have the same periodicity issue with logarithms, and it is usual to adopt the same interval
for the complex logarithm and argument functions. Further on down, we shall define both functions for the interval \<open>(-\<pi>,\<pi>]\<close>.
The present version is provided for compatibility.\<close>

lemma Arg2pi_0 [simp]: "Arg2pi(0) = 0"
 by (simp add: Arg2pi_def)

lemma Arg2pi_unique_lemma:
 assumes z: "is_Arg z t"
 and z': "is_Arg z t'"
 and t: "0 \ t" "t < 2*pi"
 and t': "0 \ t'" "t' < 2*pi"
 and nz: "z \ 0"
 shows "t' = t"
proof -
 have [dest]: "\x y z::real. x\0 \ x+y < z \ y
 by arith
 have "of_real (cmod z) * exp (\ * of_real t') = of_real (cmod z) * exp (\ * of_real t)"
 by (metis z z' is_Arg_def)
 then have "exp (\ * of_real t') = exp (\ * of_real t)"
 by (metis nz mult_left_cancel mult_zero_left z is_Arg_def)
 then have "sin t' = sin t \ cos t' = cos t"
 by (metis cis.simps cis_conv_exp)
 then obtain n::int where n: "t' = t + 2 * n * pi"
 by (auto simp: sin_cos_eq_iff)
 then have "n=0"
 by (cases n) (use t t' in \auto simp: mult_less_0_iff algebra_simps\)
 then show "t' = t"
 by (simp add: n)
qed

lemma Arg2pi: "0 \ Arg2pi z \ Arg2pi z < 2*pi \ is_Arg z (Arg2pi z)"
proof (cases "z=0")
 case True then show ?thesis
 by (simp add: Arg2pi_def is_Arg_def)
next
 case False
 obtain t where t: "0 \ t" "t < 2*pi"
 and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
 using sincos_total_2pi [OF complex_unit_circle [OF False]]
 by blast
 have z: "is_Arg z t"
 unfolding is_Arg_def
 using t False ReIm
 by (intro complex_eqI) (auto simp: exp_Euler sin_of_real cos_of_real field_split_simps)
 show ?thesis
 apply (simp add: Arg2pi_def False)
 apply (rule theI [where a=t])
 using t z False
 apply (auto intro: Arg2pi_unique_lemma)
 done
qed

corollary\<^marker>\<open>tag unimportant\<close>
 shows Arg2pi_ge_0: "0 \ Arg2pi z"
 and Arg2pi_lt_2pi: "Arg2pi z < 2*pi"
 and Arg2pi_eq: "z = of_real(norm z) * exp(\ * of_real(Arg2pi z))"
 using Arg2pi is_Arg_def by auto

lemma complex_norm_eq_1_exp: "norm z = 1 \ exp(\ * of_real (Arg2pi z)) = z"
 by (metis Arg2pi_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)

lemma Arg2pi_unique: "\of_real r * exp(\ * of_real a) = z; 0 < r; 0 \ a; a < 2*pi\ \ Arg2pi z = a"
 by (rule Arg2pi_unique_lemma [unfolded is_Arg_def, OF _ Arg2pi_eq]) (use Arg2pi [of z] in \<open>auto simp: norm_mult\<close>)

lemma cos_Arg2pi: "cmod z * cos (Arg2pi z) = Re z" and sin_Arg2pi: "cmod z * sin (Arg2pi z) = Im z"
 using Arg2pi_eq [of z] cis_conv_exp Re_rcis Im_rcis unfolding rcis_def by metis+

lemma Arg2pi_minus:
 assumes "z \ 0" shows "Arg2pi (-z) = (if Arg2pi z < pi then Arg2pi z + pi else Arg2pi z - pi)"
 apply (rule Arg2pi_unique [of "norm z", OF complex_eqI])
 using cos_Arg2pi sin_Arg2pi Arg2pi_ge_0 Arg2pi_lt_2pi [of z] assms
 by (auto simp: Re_exp Im_exp)

lemma Arg2pi_times_of_real [simp]:
 assumes "0 < r" shows "Arg2pi (of_real r * z) = Arg2pi z"
proof (cases "z=0")
 case False
 show ?thesis
 by (rule Arg2pi_unique [of "r * norm z"]) (use Arg2pi False assms is_Arg_def in auto)
qed auto

lemma Arg2pi_times_of_real2 [simp]: "0 < r \ Arg2pi (z * of_real r) = Arg2pi z"
 by (metis Arg2pi_times_of_real mult.commute)

lemma Arg2pi_divide_of_real [simp]: "0 < r \ Arg2pi (z / of_real r) = Arg2pi z"
 by (metis Arg2pi_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)

lemma Arg2pi_le_pi: "Arg2pi z \ pi \ 0 \ Im z"
proof (cases "z=0")
 case False
 have "0 \ Im z \ 0 \ Im (of_real (cmod z) * exp (\ * complex_of_real (Arg2pi z)))"
 by (metis Arg2pi_eq)
 also have "... = (0 \ Im (exp (\ * complex_of_real (Arg2pi z))))"
 using False by (simp add: zero_le_mult_iff)
 also have "... \ Arg2pi z \ pi"
 by (simp add: Im_exp) (metis Arg2pi_ge_0 Arg2pi_lt_2pi sin_lt_zero sin_ge_zero not_le)
 finally show ?thesis
 by blast
qed auto

lemma Arg2pi_lt_pi: "0 < Arg2pi z \ Arg2pi z < pi \ 0 < Im z"
proof (cases "z=0")
 case False
 have "0 < Im z \ 0 < Im (of_real (cmod z) * exp (\ * complex_of_real (Arg2pi z)))"
 by (metis Arg2pi_eq)
 also have "... = (0 < Im (exp (\ * complex_of_real (Arg2pi z))))"
 using False by (simp add: zero_less_mult_iff)
 also have "... \ 0 < Arg2pi z \ Arg2pi z < pi" (is "_ = ?rhs")
 proof -
 have "0 < sin (Arg2pi z) \ ?rhs"
 by (meson Arg2pi_ge_0 Arg2pi_lt_2pi less_le_trans not_le sin_le_zero sin_x_le_x)
 then show ?thesis
 by (auto simp: Im_exp sin_gt_zero)
 qed
 finally show ?thesis
 by blast
qed auto

lemma Arg2pi_eq_0: "Arg2pi z = 0 \ z \ \ \ 0 \ Re z"
proof (cases "z=0")
 case False
 have "z \ \ \ 0 \ Re z \ z \ \ \ 0 \ Re (of_real (cmod z) * exp (\ * complex_of_real (Arg2pi z)))"
 by (metis Arg2pi_eq)
 also have "... \ z \ \ \ 0 \ Re (exp (\ * complex_of_real (Arg2pi z)))"
 using False by (simp add: zero_le_mult_iff)
 also have "... \ Arg2pi z = 0"
 proof -
 have [simp]: "Arg2pi z = 0 \ z \ \"
 using Arg2pi_eq [of z] by (auto simp: Reals_def)
 moreover have "\z \ \; 0 \ cos (Arg2pi z)\ \ Arg2pi z = 0"
 by (metis Arg2pi_lt_pi Arg2pi_ge_0 Arg2pi_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
 ultimately show ?thesis
 by (auto simp: Re_exp)
 qed
 finally show ?thesis
 by blast
qed auto

corollary\<^marker>\<open>tag unimportant\<close> Arg2pi_gt_0:
 assumes "z \ \\<^sub>\\<^sub>0"
 shows "Arg2pi z > 0"
 using Arg2pi_eq_0 Arg2pi_ge_0 assms dual_order.strict_iff_order
 unfolding nonneg_Reals_def by fastforce

lemma Arg2pi_eq_pi: "Arg2pi z = pi \ z \ \ \ Re z < 0"
 using Arg2pi_le_pi [of z] Arg2pi_lt_pi [of z] Arg2pi_eq_0 [of z] Arg2pi_ge_0 [of z]
 by (fastforce simp: complex_is_Real_iff)

lemma Arg2pi_eq_0_pi: "Arg2pi z = 0 \ Arg2pi z = pi \ z \ \"
 using Arg2pi_eq_0 Arg2pi_eq_pi not_le by auto

lemma Arg2pi_of_real: "Arg2pi (of_real r) = (if r<0 then pi else 0)"
 using Arg2pi_eq_0_pi Arg2pi_eq_pi by fastforce

lemma Arg2pi_real: "z \ \ \ Arg2pi z = (if 0 \ Re z then 0 else pi)"
 using Arg2pi_eq_0 Arg2pi_eq_0_pi by auto

lemma Arg2pi_inverse: "Arg2pi(inverse z) = (if z \ \ then Arg2pi z else 2*pi - Arg2pi z)"
proof (cases "z=0")
 case False
 show ?thesis
 apply (rule Arg2pi_unique [of "inverse (norm z)"])
 using Arg2pi_eq False Arg2pi_ge_0 [of z] Arg2pi_lt_2pi [of z] Arg2pi_eq_0 [of z]
 by (auto simp: Arg2pi_real in_Reals_norm exp_diff field_simps)
qed auto

lemma Arg2pi_eq_iff:
 assumes "w \ 0" "z \ 0"
 shows "Arg2pi w = Arg2pi z \ (\x. 0 < x & w = of_real x * z)"
 using assms Arg2pi_eq [of z] Arg2pi_eq [of w]
 apply auto
 apply (rule_tac x="norm w / norm z" in exI)
 apply (simp add: field_split_simps)
 by (metis mult.commute mult.left_commute)

lemma Arg2pi_inverse_eq_0: "Arg2pi(inverse z) = 0 \ Arg2pi z = 0"
 by (metis Arg2pi_eq_0 Arg2pi_inverse inverse_inverse_eq)

lemma Arg2pi_divide:
 assumes "w \ 0" "z \ 0" "Arg2pi w \ Arg2pi z"
 shows "Arg2pi(z / w) = Arg2pi z - Arg2pi w"
 apply (rule Arg2pi_unique [of "norm(z / w)"])
 using assms Arg2pi_eq Arg2pi_ge_0 [of w] Arg2pi_lt_2pi [of z]
 apply (auto simp: exp_diff norm_divide field_simps)
 done

lemma Arg2pi_le_div_sum:
 assumes "w \ 0" "z \ 0" "Arg2pi w \ Arg2pi z"
 shows "Arg2pi z = Arg2pi w + Arg2pi(z / w)"
 by (simp add: Arg2pi_divide assms)

lemma Arg2pi_le_div_sum_eq:
 assumes "w \ 0" "z \ 0"
 shows "Arg2pi w \ Arg2pi z \ Arg2pi z = Arg2pi w + Arg2pi(z / w)"
 using assms by (auto simp: Arg2pi_ge_0 intro: Arg2pi_le_div_sum)

lemma Arg2pi_diff:
 assumes "w \ 0" "z \ 0"
 shows "Arg2pi w - Arg2pi z = (if Arg2pi z \ Arg2pi w then Arg2pi(w / z) else Arg2pi(w/z) - 2*pi)"
 using assms Arg2pi_divide Arg2pi_inverse [of "w/z"] Arg2pi_eq_0_pi
 by (force simp add: Arg2pi_ge_0 Arg2pi_divide not_le split: if_split_asm)

lemma Arg2pi_add:
 assumes "w \ 0" "z \ 0"
 shows "Arg2pi w + Arg2pi z = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi(w * z) else Arg2pi(w * z) + 2*pi)"
 using assms Arg2pi_diff [of "w*z" z] Arg2pi_le_div_sum_eq [of z "w*z"]
 apply (auto simp: Arg2pi_ge_0 Arg2pi_divide not_le)
 apply (metis Arg2pi_lt_2pi add.commute)
 apply (metis (no_types) Arg2pi add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
 done

lemma Arg2pi_times:
 assumes "w \ 0" "z \ 0"
 shows "Arg2pi (w * z) = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi w + Arg2pi z
 else (Arg2pi w + Arg2pi z) - 2*pi)"
 using Arg2pi_add [OF assms]
 by auto

lemma Arg2pi_cnj_eq_inverse: "z\0 \ Arg2pi (cnj z) = Arg2pi (inverse z)"
 apply (simp add: Arg2pi_eq_iff field_split_simps complex_norm_square [symmetric])
 by (metis of_real_power zero_less_norm_iff zero_less_power)

lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \ \ then Arg2pi z else 2*pi - Arg2pi z)"
proof (cases "z=0")
 case False
 then show ?thesis
 by (simp add: Arg2pi_cnj_eq_inverse Arg2pi_inverse)
qed auto

lemma Arg2pi_exp: "0 \ Im z \ Im z < 2*pi \ Arg2pi(exp z) = Im z"
 by (rule Arg2pi_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)

lemma complex_split_polar:
 obtains r a::real where "z = complex_of_real r * (cos a + \ * sin a)" "0 \ r" "0 \ a" "a < 2*pi"
 using Arg2pi cis.ctr cis_conv_exp unfolding Complex_eq is_Arg_def by fastforce

lemma Re_Im_le_cmod: "Im w * sin \ + Re w * cos \ \ cmod w"
proof (cases w rule: complex_split_polar)
 case (1 r a) with sin_cos_le1 [of a \<phi>] show ?thesis
 apply (simp add: norm_mult cmod_unit_one)
 by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
qed

subsection\<^marker>\<open>tag unimportant\<close>\<open>Analytic properties of tangent function\<close>

lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
 by (simp add: cnj_cos cnj_sin tan_def)

lemma field_differentiable_at_tan: "cos z \ 0 \ tan field_differentiable at z"
 unfolding field_differentiable_def
 using DERIV_tan by blast

lemma field_differentiable_within_tan: "cos z \ 0
 \<Longrightarrow> tan field_differentiable (at z within s)"
 using field_differentiable_at_tan field_differentiable_at_within by blast

lemma continuous_within_tan: "cos z \ 0 \ continuous (at z within s) tan"
 using continuous_at_imp_continuous_within isCont_tan by blast

lemma continuous_on_tan [continuous_intros]: "(\z. z \ s \ cos z \ 0) \ continuous_on s tan"
 by (simp add: continuous_at_imp_continuous_on)

lemma holomorphic_on_tan: "(\z. z \ s \ cos z \ 0) \ tan holomorphic_on s"
 by (simp add: field_differentiable_within_tan holomorphic_on_def)

subsection\<open>The principal branch of the Complex logarithm\<close>

instantiation complex :: ln
begin

definition\<^marker>\<open>tag important\<close> ln_complex :: "complex \<Rightarrow> complex"
 where "ln_complex \ \z. THE w. exp w = z & -pi < Im(w) & Im(w) \ pi"

text\<open>NOTE: within this scope, the constant Ln is not yet available!\<close>
lemma
 assumes "z \ 0"
 shows exp_Ln [simp]: "exp(ln z) = z"
 and mpi_less_Im_Ln: "-pi < Im(ln z)"
 and Im_Ln_le_pi: "Im(ln z) \ pi"
proof -
 obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
 using complex_unimodular_polar [of "z / (norm z)"] assms
 by (auto simp: norm_divide field_split_simps)
 obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
 using sincos_principal_value [of "\"] assms
 by (auto simp: norm_divide field_split_simps)
 have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \ pi" unfolding ln_complex_def
 apply (rule theI [where a = "Complex (ln(norm z)) \"])
 using z assms \<phi>
 apply (auto simp: field_simps exp_complex_eqI exp_eq_polar cis.code)
 done
 then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \ pi"
 by auto
qed

lemma Ln_exp [simp]:
 assumes "-pi < Im(z)" "Im(z) \ pi"
 shows "ln(exp z) = z"
proof (rule exp_complex_eqI)
 show "\Im (ln (exp z)) - Im z\ < 2 * pi"
 using assms mpi_less_Im_Ln [of "exp z"] Im_Ln_le_pi [of "exp z"] by auto
qed auto

subsection\<^marker>\<open>tag unimportant\<close>\<open>Relation to Real Logarithm\<close>

lemma Ln_of_real:
 assumes "0 < z"
 shows "ln(of_real z::complex) = of_real(ln z)"
proof -
 have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"
 by (simp add: exp_of_real)
 also have "... = of_real(ln z)"
 using assms by (subst Ln_exp) auto
 finally show ?thesis
 using assms by simp
qed

corollary\<^marker>\<open>tag unimportant\<close> Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
 by (auto simp: Ln_of_real elim: Reals_cases)

corollary\<^marker>\<open>tag unimportant\<close> Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
 by (simp add: Ln_of_real)

lemma cmod_Ln_Reals [simp]: "z \ \ \ 0 < Re z \ cmod (ln z) = norm (ln (Re z))"
 using Ln_of_real by force

lemma Ln_Reals_eq: "\x \ \; Re x > 0\ \ ln x = of_real (ln (Re x))"
 using Ln_of_real by force

lemma Ln_1 [simp]: "ln 1 = (0::complex)"
proof -
 have "ln (exp 0) = (0::complex)"
 by (simp add: del: exp_zero)
 then show ?thesis
 by simp
qed

lemma Ln_eq_zero_iff [simp]: "x \ \\<^sub>\\<^sub>0 \ ln x = 0 \ x = 1" for x::complex
 by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)

instance
 by intro_classes (rule ln_complex_def Ln_1)

end

abbreviation Ln :: "complex \ complex"
 where "Ln \ ln"

lemma Ln_eq_iff: "w \ 0 \ z \ 0 \ (Ln w = Ln z \ w = z)"
 by (metis exp_Ln)

lemma Ln_unique: "exp(z) = w \ -pi < Im(z) \ Im(z) \ pi \ Ln w = z"
 using Ln_exp by blast

lemma Re_Ln [simp]: "z \ 0 \ Re(Ln z) = ln(norm z)"
 by (metis exp_Ln ln_exp norm_exp_eq_Re)

corollary\<^marker>\<open>tag unimportant\<close> ln_cmod_le:
 assumes z: "z \ 0"
 shows "ln (cmod z) \ cmod (Ln z)"
 using norm_exp [of "Ln z", simplified exp_Ln [OF z]]
 by (metis Re_Ln complex_Re_le_cmod z)

proposition\<^marker>\<open>tag unimportant\<close> exists_complex_root:
 fixes z :: complex
 assumes "n \ 0" obtains w where "z = w ^ n"
proof (cases "z=0")
 case False
 then show ?thesis
 by (rule_tac w = "exp(Ln z / n)" in that) (simp add: assms exp_of_nat_mult [symmetric])
qed (use assms in auto)

corollary\<^marker>\<open>tag unimportant\<close> exists_complex_root_nonzero:
 fixes z::complex
 assumes "z \ 0" "n \ 0"
 obtains w where "w \ 0" "z = w ^ n"
 by (metis exists_complex_root [of n z] assms power_0_left)

subsection\<^marker>\<open>tag unimportant\<close>\<open>Derivative of Ln away from the branch cut\<close>

lemma
 assumes "z \ \\<^sub>\\<^sub>0"
 shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
 and Im_Ln_less_pi: "Im (Ln z) < pi"
proof -
 have znz [simp]: "z \ 0"
 using assms by auto
 then have "Im (Ln z) \ pi"
 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)
 then show *: "Im (Ln z) < pi" using assms Im_Ln_le_pi
 by (simp add: le_neq_trans)
 let ?U = "{w. -pi < Im(w) \ Im(w) < pi}"
 have 1: "open ?U"
 by (simp add: open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
 have 2: "\x. x \ ?U \ (exp has_derivative blinfun_apply(Blinfun ((*) (exp x)))) (at x)"
 by (simp add: bounded_linear_Blinfun_apply bounded_linear_mult_right has_field_derivative_imp_has_derivative)
 have 3: "continuous_on ?U (\x. Blinfun ((*) (exp x)))"
 unfolding blinfun_mult_right.abs_eq [symmetric] by (intro continuous_intros)
 have 4: "Ln z \ ?U"
 by (auto simp: mpi_less_Im_Ln *)
 have 5: "Blinfun ((*) (inverse z)) o\<^sub>L Blinfun ((*) (exp (Ln z))) = id_blinfun"
 by (rule blinfun_eqI) (simp add: bounded_linear_mult_right bounded_linear_Blinfun_apply)
 obtain U' V g g' where "open U'" and sub: "U' \ ?U"
 and "Ln z \ U'" "open V" "z \ V"
 and hom: "homeomorphism U' V exp g"
 and g: "\y. y \ V \ (g has_derivative (g' y)) (at y)"
 and g': "\y. y \ V \ g' y = inv ((*) (exp (g y)))"
 and bij: "\y. y \ V \ bij ((*) (exp (g y)))"
 using inverse_function_theorem [OF 1 2 3 4 5]
 by (simp add: bounded_linear_Blinfun_apply bounded_linear_mult_right) blast
 show "(Ln has_field_derivative inverse(z)) (at z)"
 unfolding has_field_derivative_def
 proof (rule has_derivative_transform_within_open)
 show g_eq_Ln: "g y = Ln y" if "y \ V" for y
 proof -
 obtain x where "y = exp x" "x \ U'"
 using hom homeomorphism_image1 that \<open>y \<in> V\<close> by blast
 then show ?thesis
 using sub hom homeomorphism_apply1 by fastforce
 qed
 have "0 \ V"
 by (meson exp_not_eq_zero hom homeomorphism_def)
 then have "\y. y \ V \ g' y = inv ((*) y)"
 by (metis exp_Ln g' g_eq_Ln)
 then have g': "g' z = (\<lambda>x. x/z)"
 by (metis (no_types, hide_lams) bij \<open>z \<in> V\<close> bij_inv_eq_iff exp_Ln g_eq_Ln nonzero_mult_div_cancel_left znz)
 show "(g has_derivative (*) (inverse z)) (at z)"
 using g [OF \<open>z \<in> V\<close>] g'
 by (simp add: \<open>z \<in> V\<close> field_class.field_divide_inverse has_derivative_imp_has_field_derivative has_field_derivative_imp_has_derivative)
 qed (auto simp: \<open>z \<in> V\<close> \<open>open V\<close>)
qed

declare has_field_derivative_Ln [derivative_intros]
declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]

lemma field_differentiable_at_Ln: "z \ \\<^sub>\\<^sub>0 \ Ln field_differentiable at z"
 using field_differentiable_def has_field_derivative_Ln by blast

lemma field_differentiable_within_Ln: "z \ \\<^sub>\\<^sub>0
 \<Longrightarrow> Ln field_differentiable (at z within S)"
 using field_differentiable_at_Ln field_differentiable_within_subset by blast

lemma continuous_at_Ln: "z \ \\<^sub>\\<^sub>0 \ continuous (at z) Ln"
 by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Ln)

lemma isCont_Ln' [simp,continuous_intros]:
 "\isCont f z; f z \ \\<^sub>\\<^sub>0\ \ isCont (\x. Ln (f x)) z"
 by (blast intro: isCont_o2 [OF _ continuous_at_Ln])

lemma continuous_within_Ln [continuous_intros]: "z \ \\<^sub>\\<^sub>0 \ continuous (at z within S) Ln"
 using continuous_at_Ln continuous_at_imp_continuous_within by blast

lemma continuous_on_Ln [continuous_intros]: "(\z. z \ S \ z \ \\<^sub>\\<^sub>0) \ continuous_on S Ln"
 by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)

lemma continuous_on_Ln' [continuous_intros]:
 "continuous_on S f \ (\z. z \ S \ f z \ \\<^sub>\\<^sub>0) \ continuous_on S (\x. Ln (f x))"
 by (rule continuous_on_compose2[OF continuous_on_Ln, of "UNIV - nonpos_Reals" S f]) auto

lemma holomorphic_on_Ln [holomorphic_intros]: "(\z. z \ S \ z \ \\<^sub>\\<^sub>0) \ Ln holomorphic_on S"
 by (simp add: field_differentiable_within_Ln holomorphic_on_def)

lemma holomorphic_on_Ln' [holomorphic_intros]:
 "(\z. z \ A \ f z \ \\<^sub>\\<^sub>0) \ f holomorphic_on A \ (\z. Ln (f z)) holomorphic_on A"
 using holomorphic_on_compose_gen[OF _ holomorphic_on_Ln, of f A "- \\<^sub>\\<^sub>0"]
 by (auto simp: o_def)

lemma tendsto_Ln [tendsto_intros]:
 fixes L F
 assumes "(f \ L) F" "L \ \\<^sub>\\<^sub>0"
 shows "((\x. Ln (f x)) \ Ln L) F"
proof -
 have "nhds L \ filtermap f F"
 using assms(1) by (simp add: filterlim_def)
 moreover have "\\<^sub>F y in nhds L. y \ - \\<^sub>\\<^sub>0"
 using eventually_nhds_in_open[of "- \\<^sub>\\<^sub>0" L] assms by (auto simp: open_Compl)
 ultimately have "\\<^sub>F y in filtermap f F. y \ - \\<^sub>\\<^sub>0" by (rule filter_leD)
 moreover have "continuous_on (-\\<^sub>\\<^sub>0) Ln" by (rule continuous_on_Ln) auto
 ultimately show ?thesis using continuous_on_tendsto_compose[of "- \\<^sub>\\<^sub>0" Ln f L F] assms
 by (simp add: eventually_filtermap)
qed

lemma divide_ln_mono:
 fixes x y::real
 assumes "3 \ x" "x \ y"
 shows "x / ln x \ y / ln y"
proof (rule exE [OF complex_mvt_line [of x y "\z. z / Ln z" "\z. 1/(Ln z) - 1/(Ln z)^2"]];
 clarsimp simp add: closed_segment_Reals closed_segment_eq_real_ivl assms)
 show "\u. \x \ u; u \ y\ \ ((\z. z / Ln z) has_field_derivative 1 / Ln u - 1 / (Ln u)\<^sup>2) (at u)"
 using \<open>3 \<le> x\<close> by (force intro!: derivative_eq_intros simp: field_simps power_eq_if)
 show "x / ln x \ y / ln y"
 if "Re (y / Ln y) - Re (x / Ln x) = (Re (1 / Ln u) - Re (1 / (Ln u)\<^sup>2)) * (y - x)"
 and x: "x \ u" "u \ y" for u
 proof -
 have eq: "y / ln y = (1 / ln u - 1 / (ln u)\<^sup>2) * (y - x) + x / ln x"
 using that \<open>3 \<le> x\<close> by (auto simp: Ln_Reals_eq in_Reals_norm group_add_class.diff_eq_eq)
 show ?thesis
 using exp_le \<open>3 \<le> x\<close> x by (simp add: eq) (simp add: power_eq_if divide_simps ln_ge_iff)
 qed
qed

theorem Ln_series:
 fixes z :: complex
 assumes "norm z < 1"
 shows "(\n. (-1)^Suc n / of_nat n * z^n) sums ln (1 + z)" (is "(\n. ?f n * z^n) sums _")
proof -
 let ?F = "\z. \n. ?f n * z^n" and ?F' = "\z. \n. diffs ?f n * z^n"
 have r: "conv_radius ?f = 1"
 by (intro conv_radius_ratio_limit_nonzero[of _ 1])
 (simp_all add: norm_divide LIMSEQ_Suc_n_over_n del: of_nat_Suc)

 have "\c. \z\ball 0 1. ln (1 + z) - ?F z = c"
 proof (rule has_field_derivative_zero_constant)
 fix z :: complex assume z': "z \ ball 0 1"
 hence z: "norm z < 1" by simp
 define t :: complex where "t = of_real (1 + norm z) / 2"
 from z have t: "norm z < norm t" "norm t < 1" unfolding t_def
 by (simp_all add: field_simps norm_divide del: of_real_add)

 have "Re (-z) \ norm (-z)" by (rule complex_Re_le_cmod)
 also from z have "... < 1" by simp
 finally have "((\z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)"
 by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
 moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
 by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all
 ultimately have "((\z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z))
 (at z within ball 0 1)"
 by (intro derivative_intros) (simp_all add: at_within_open[OF z'])
 also have "(\n. of_nat n * ?f n * z ^ (n - Suc 0)) sums ?F' z" using t r
 by (intro diffs_equiv termdiff_converges[OF t(1)] summable_in_conv_radius) simp_all
 from sums_split_initial_segment[OF this, of 1]
 have "(\i. (-z) ^ i) sums ?F' z" by (simp add: power_minus[of z] del: of_nat_Suc)
 hence "?F' z = inverse (1 + z)" using z by (simp add: sums_iff suminf_geometric divide_inverse)
 also have "inverse (1 + z) - inverse (1 + z) = 0" by simp
 finally show "((\z. ln (1 + z) - ?F z) has_field_derivative 0) (at z within ball 0 1)" .
 qed simp_all
 then obtain c where c: "\z. z \ ball 0 1 \ ln (1 + z) - ?F z = c" by blast
 from c[of 0] have "c = 0" by (simp only: powser_zero) simp
 with c[of z] assms have "ln (1 + z) = ?F z" by simp
 moreover have "summable (\n. ?f n * z^n)" using assms r
 by (intro summable_in_conv_radius) simp_all
 ultimately show ?thesis by (simp add: sums_iff)
qed

lemma Ln_series': "cmod z < 1 \ (\n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
 by (drule Ln_series) (simp add: power_minus')

lemma ln_series':
 assumes "abs (x::real) < 1"
 shows "(\n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
proof -
 from assms have "(\n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
 by (intro Ln_series') simp_all
 also have "(\n. - ((-of_real x)^n) / of_nat n) = (\n. complex_of_real (- ((-x)^n) / of_nat n))"
 by (rule ext) simp
 also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"
 by (subst Ln_of_real [symmetric]) simp_all
 finally show ?thesis by (subst (asm) sums_of_real_iff)
qed

lemma Ln_approx_linear:
 fixes z :: complex
 assumes "norm z < 1"
 shows "norm (ln (1 + z) - z) \ norm z^2 / (1 - norm z)"
proof -
 let ?f = "\n. (-1)^Suc n / of_nat n"
 from assms have "(\n. ?f n * z^n) sums ln (1 + z)" using Ln_series by simp
 moreover have "(\n. (if n = 1 then 1 else 0) * z^n) sums z" using powser_sums_if[of 1] by simp
 ultimately have "(\n. (?f n - (if n = 1 then 1 else 0)) * z^n) sums (ln (1 + z) - z)"
 by (subst left_diff_distrib, intro sums_diff) simp_all
 from sums_split_initial_segment[OF this, of "Suc 1"]
 have "(\i. (-(z^2)) * inverse (2 + of_nat i) * (- z)^i) sums (Ln (1 + z) - z)"
 by (simp add: power2_eq_square mult_ac power_minus[of z] divide_inverse)
 hence "(Ln (1 + z) - z) = (\i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)"
 by (simp add: sums_iff)
 also have A: "summable (\n. norm z^2 * (inverse (real_of_nat (Suc (Suc n))) * cmod z ^ n))"
 by (rule summable_mult, rule summable_comparison_test_ev[OF _ summable_geometric[of "norm z"]])
 (auto simp: assms field_simps intro!: always_eventually)
 hence "norm (\i. (-(z^2)) * inverse (of_nat (i+2)) * (-z)^i)
--> --------------------

--> maximum size reached

--> --------------------

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.61Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

Kontakt Drucken
Kontakt Hier finden Sie eine Liste der Produkte des Unternehmens
Mittel

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Complex_Transcendental.thy Sprache: Isabelle

Original von: Isabelle^©

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.61Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

schauen Sie vor die Tür

Die Firma ist wie angegeben erreichbar.

Bot Zugriff

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Complex_Transcendental.thy Sprache: Isabelle

Original von: Isabelle©

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.61Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

schauen Sie vor die Tür

Die Firma ist wie angegeben erreichbar.

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©