SSL Complex_Transcendental.thy Sprache: 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 exp_npi_numeral: "exp (\ * pi * Num.numeral n) = (-1) ^ Num.numeral n"
 by (metis exp_of_nat2_mult exp_pi_i' of_nat_numeral)

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)

lemma exp_analytic_on [analytic_intros]:
 assumes "f analytic_on A"
 shows "(\z. exp (f z)) analytic_on A"
 by (metis analytic_on_holomorphic assms holomorphic_on_exp')

lemma
 assumes "\w. w \ A \ exp (f w) = w"
 assumes "f holomorphic_on A" "z \ A" "open A"
 shows deriv_complex_logarithm: "deriv f z = 1 / z"
 and has_field_derivative_complex_logarithm: "(f has_field_derivative 1 / z) (at z)"
proof -
 have [simp]: "z \ 0"
 using assms(1)[of z] assms(3) by auto
 have deriv [derivative_intros]: "(f has_field_derivative deriv f z) (at z)"
 using assms holomorphic_derivI by blast
 have "((\w. w) has_field_derivative 1) (at z)"
 by (intro derivative_intros)
 also have "?this \ ((\w. exp (f w)) has_field_derivative 1) (at z)"
 by (smt (verit, best) assms has_field_derivative_transform_within_open)
 finally have "((\w. exp (f w)) has_field_derivative 1) (at z)" .
 moreover have "((\w. exp (f w)) has_field_derivative exp (f z) * deriv f z) (at z)"
 by (rule derivative_eq_intros refl)+
 ultimately have "exp (f z) * deriv f z = 1"
 using DERIV_unique by blast
 with assms show "deriv f z = 1 / z"
 by (simp add: field_simps)
 with deriv show "(f has_field_derivative 1 / z) (at z)"
 by simp
qed

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))"
 by (force simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
 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 (simp add: Complex_eq cis.code exp_eq_polar)

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)"
 by (simp add: cis_cnj exp_eq_polar)

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)

lemma analytic_on_sin [analytic_intros]: "f analytic_on A \ (\w. sin (f w)) analytic_on A"
 and analytic_on_cos [analytic_intros]: "f analytic_on A \ (\w. cos (f w)) analytic_on A"
 and analytic_on_sinh [analytic_intros]: "f analytic_on A \ (\w. sinh (f w)) analytic_on A"
 and analytic_on_cosh [analytic_intros]: "f analytic_on A \ (\w. cosh (f w)) analytic_on A"
 unfolding sin_exp_eq cos_exp_eq sinh_def cosh_def
 by (auto intro!: analytic_intros)

lemma analytic_on_tan [analytic_intros]:
 "f analytic_on A \ (\z. z \ A \ cos (f z) \ 0) \ (\w. tan (f w)) analytic_on A"
 and analytic_on_cot [analytic_intros]:
 "f analytic_on A \ (\z. z \ A \ sin (f z) \ 0) \ (\w. cot (f w)) analytic_on A"
 and analytic_on_tanh [analytic_intros]:
 "f analytic_on A \ (\z. z \ A \ cosh (f z) \ 0) \ (\w. tanh (f w)) analytic_on A"
 unfolding tan_def cot_def tanh_def by (auto intro!: analytic_intros)

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)"
 using Complex_eq Euler complex.sel by presburger

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 cos_one_2pi_int exp_zero mult.commute mult_1 of_int_mult of_int_numeral one_complex.simps(1))
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"
 by (metis assms cis_conv_exp cis_multiple_2pi mult.assoc mult.commute)

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

lemma exp_2pi_1_int [simp]: "exp (\ * (of_int j * (of_real pi * 2))) = 1"
 by (metis exp_add exp_not_eq_zero exp_plus_2pin mult_cancel_left1)

lemma exp_2pi_1_nat [simp]: "exp (\ * (of_nat j * (of_real pi * 2))) = 1"
 by (metis exp_2pi_1_int of_int_of_nat_eq)

lemma exp_integer_2pi_plus1:
 assumes "n \ \"
 shows "exp(((2 * n + 1) * pi) * \) = - 1"
 using exp_integer_2pi [OF assms]
 by (metis cis_conv_exp cis_mult cis_pi distrib_left mult.commute mult.right_neutral)

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
 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
 shows "(cmod (r1 * exp (\ * \1) - r2 * exp (\ * \2)))\<^sup>2 = r1\<^sup>2 + r2\<^sup>2 - 2*r1*r2*cos (\1 - \2)"
 using cmod_add_squared [of r1 _ "-r2"] by simp

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
 using assms by (auto simp: cmod_diff_squared 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 exp_i_ne_1:
 assumes "0 < x" "x < 2*pi"
 shows "exp(\ * of_real x) \ 1"
 by (smt (verit) Im_i_times Re_complex_of_real assms exp_complex_eqI exp_zero zero_complex.sel(2))

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 = complex_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 = complex_of_real(2 * n * pi))"
 by (metis Re_complex_of_real cos_of_real cos_one_2pi_int cos_one_sin_zero mult.commute of_real_1 sin_eq_0)

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 = complex_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 (metis (mono_tags, lifting) add_uminus_conv_diff csin_eq_1 equation_minus_iff 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 = complex_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. x = of_real(2 * n * pi) + of_real pi/2)"
 by (metis csin_eq_1 Re_complex_of_real id_apply of_real_add of_real_divide of_real_eq_id of_real_numeral)
 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. x = of_real(2 * n * pi) + 3/2*pi)"
 by (metis Re_complex_of_real csin_eq_minus1 id_apply of_real_add of_real_eq_id)
 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. x = of_real(2 * n * pi) + pi)"
 by (metis ccos_eq_minus1 id_apply of_real_add of_real_eq_id of_real_eq_iff)
 also have "\ = ?rhs"
 by (auto simp: algebra_simps)
 finally show ?thesis .
qed

lemma cos_gt_neg1:
 assumes "(t::real) \ {-pi<..
 shows "cos t > -1"
 using assms
 by simp (metis cos_minus cos_monotone_0_pi cos_monotone_minus_pi_0 cos_pi linorder_le_cases)

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 consider "sin ((w - z) / 2) = 0" | "cos ((w + z) / 2) = 0"
 by (metis divide_eq_0_iff nonzero_eq_divide_eq right_minus_eq sin_diff_sin zero_neq_numeral)
 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 consider "sin ((w + z) / 2) = 0" | "sin ((z - w) / 2) = 0"
 by (metis mult_eq_0_iff cos_diff_cos right_minus_eq zero_neq_numeral)
 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] unfolding cos_of_real
 by (metis Re_complex_of_real of_real_add of_real_minus)

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"
 using cos_double_sin [of "Re z"]
 apply (simp add: sin_cos_eq norm_cos_squared exp_minus mult.commute [of _ 2] exp_double)
 apply (simp add: algebra_simps power2_eq_square)
 done

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)"
 by (metis mult_2 norm_cos_le norm_ge_zero norm_one norm_triangle_mono one_le_exp_iff)

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

text \<open>For complex @{term z}, a tighter bound than in the previous result\<close>
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)"
 by (cases "even k") (intro derivative_eq_intros | simp add: power_Suc)+
 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)"
 by (cases "even k") (intro derivative_eq_intros | simp add: power_Suc)+
 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 "is_Arg z r" and "is_Arg z s" and "abs (r-s) < 2*pi" and "z \ 0"
 shows "r = s"
 using assms unfolding is_Arg_def
 by (metis Im_i_times Re_complex_of_real exp_complex_eqI mult_cancel_left mult_eq_0_iff)

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 "is_Arg z t"
 and "is_Arg z t'"
 and "0 \ t" "t < 2*pi"
 and "0 \ t'" "t' < 2*pi"
 and "z \ 0"
 shows "t' = t"
 using is_Arg_eqI assms by force

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
 then 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"
 by (metis (no_types, lifting) Arg2pi Arg2pi_eq Arg2pi_unique assms mult.assoc
 mult_eq_0_iff mult_pos_pos of_real_mult zero_less_norm_iff)

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_irrefl 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"
 using Arg2pi_le_pi [of z]
 by (smt (verit, del_insts) Arg2pi_0 Arg2pi_le_pi Arg2pi_minus uminus_complex.simps(2) zero_complex.simps(2))

lemma Arg2pi_eq_0: "Arg2pi z = 0 \ z \ \ \ 0 \ Re z"
proof (cases "z=0")
 case False
 then have "z \ \ \ 0 \ Re z \ z \ \ \ 0 \ Re (exp (\ * complex_of_real (Arg2pi z)))"
 by (metis cis.sel(1) cis_conv_exp cos_Arg2pi norm_ge_zero norm_le_zero_iff 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 (smt (verit, ccfv_SIG) Arg2pi_ge_0 Arg2pi_le_pi Arg2pi_lt_pi complex_is_Real_iff cos_pi)
 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)" (is "?lhs = ?rhs")
proof
 assume ?lhs
 then have "(cmod w) * (z / cmod z) = w"
 by (metis Arg2pi_eq assms(2) mult_eq_0_iff nonzero_mult_div_cancel_left)
 then show ?rhs
 by (metis assms divide_pos_pos of_real_divide times_divide_eq_left times_divide_eq_right zero_less_norm_iff)
qed auto

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"] Arg2pi [of "w * z"]
 by auto

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:
 assumes "z \ 0" shows "Arg2pi (cnj z) = Arg2pi (inverse z)"
proof -
 have "\r>0. of_real r / z = cnj z"
 by (metis assms complex_norm_square nonzero_mult_div_cancel_left zero_less_norm_iff zero_less_power)
 then show ?thesis
 by (metis Arg2pi_times_of_real2 divide_inverse_commute)
qed

lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \ \ then Arg2pi z else 2*pi - Arg2pi z)"
 by (metis Arg2pi_cnj_eq_inverse Arg2pi_inverse Reals_cnj_iff complex_cnj_zero)

lemma Arg2pi_exp: "0 \ Im z \ Im z < 2*pi \ Arg2pi(exp z) = Im z"
 by (simp add: Arg2pi_unique 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, opaque_lifting) 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)"
 by (smt (verit) Im_complex_of_real Ln_exp assms exp_ln of_real_exp pi_ge_two)

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)"
 by (smt (verit, best) Ln_of_real ln_one of_real_0 of_real_1)

lemma Ln_eq_zero_iff [simp]: "x \ \\<^sub>\\<^sub>0 \ ln x = 0 \ x = 1" for x::complex
 by (metis (mono_tags, lifting) Ln_1 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)"
 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"
 by (metis assms exp_Ln exp_of_nat_mult nonzero_mult_div_cancel_left of_nat_eq_0_iff power_0_left times_divide_eq_right)

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 Im_Ln_less_pi:
 assumes "z \ \\<^sub>\\<^sub>0"shows "Im (Ln z) < pi"
proof -
 have znz [simp]: "z \ 0"
 using assms by auto
 with Im_Ln_le_pi [of z] show ?thesis
 by (smt (verit, best) Arg2pi_eq_0_pi Arg2pi_exp Ln_in_Reals assms complex_is_Real_iff complex_nonpos_Reals_iff exp_Ln pi_ge_two)
qed

lemma has_field_derivative_Ln:
 assumes "z \ \\<^sub>\\<^sub>0"
 shows "(Ln has_field_derivative inverse(z)) (at z)"
proof -
 have znz [simp]: "z \ 0"
 using assms by auto
 then have "Im (Ln z) \ pi"
 by (smt (verit, best) Arg2pi_eq_0_pi Arg2pi_exp Ln_in_Reals assms complex_is_Real_iff complex_nonpos_Reals_iff exp_Ln pi_ge_two)
 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 (simp add: Im_Ln_less_pi assms 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
 by (smt (verit, ccfv_threshold) Ln_exp hom homeomorphism_def imageI mem_Collect_eq sub subset_iff that)
 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 \<open>z \<in> V\<close> bij 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: divide_inverse_commute)
 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]: "S \ \\<^sub>\\<^sub>0 = {} \ Ln holomorphic_on S"
 by (simp add: disjoint_iff 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 analytic_on_ln [analytic_intros]:
 assumes "f analytic_on A" "f ` A \ \\<^sub>\\<^sub>0 = {}"
 shows "(\w. ln (f w)) analytic_on A"
proof -
 have *: "ln analytic_on (-\\<^sub>\\<^sub>0)"
 by (subst analytic_on_open) (auto intro!: holomorphic_intros)
 have "(ln \ f) analytic_on A"
 by (rule analytic_on_compose_gen[OF assms(1) *]) (use assms(2) in auto)
 thus ?thesis
 by (simp add: o_def)
qed

lemma tendsto_Ln [tendsto_intros]:
 assumes "(f \ L) F" "L \ \\<^sub>\\<^sub>0"
 shows "((\x. Ln (f x)) \ Ln L) F"
 by (simp add: assms isCont_tendsto_compose)

lemma divide_ln_mono:
 fixes x y::real
 assumes "3 \ x" "x \ y"
 shows "x / ln x \ y / ln y"
proof -
 have "\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)
 moreover
 have "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
 ultimately show ?thesis
 using complex_mvt_line [of x y "\z. z / Ln z" "\z. 1/(Ln z) - 1/(Ln z)^2"] assms
 by (force simp add: closed_segment_Reals closed_segment_eq_real_ivl)
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':
 fixes x::real
 assumes "\x\ < 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 (smt (verit) Ln_of_real of_real_1 of_real_add)
 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)
 \<le> (\<Sum>i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))"
 by (intro summable_norm)
 (auto simp: norm_power norm_inverse norm_mult mult_ac simp del: of_nat_add of_nat_Suc)
 also have "norm ((-z)^2 * (-z)^i) * inverse (of_nat (i+2)) \ norm ((-z)^2 * (-z)^i) * 1" for i
 by (intro mult_left_mono) (simp_all add: field_split_simps)
 hence "(\i. norm (-(z^2) * inverse (of_nat (i+2)) * (-z)^i))
 \<le> (\<Sum>i. norm (-(z^2) * (-z)^i))"
 using A assms
 unfolding norm_power norm_inverse norm_divide norm_mult
 apply (intro suminf_le summable_mult summable_geometric)
 apply (auto simp: norm_power field_simps simp del: of_nat_add of_nat_Suc)
 done
 also have "\ = norm z^2 * (\i. norm z^i)" using assms
 by (subst suminf_mult [symmetric]) (auto intro!: summable_geometric simp: norm_mult norm_power)
 also have "(\i. norm z^i) = inverse (1 - norm z)" using assms
 by (subst suminf_geometric) (simp_all add: divide_inverse)
 also have "norm z^2 * \ = norm z^2 / (1 - norm z)" by (simp add: divide_inverse)
 finally show ?thesis .
qed

lemma norm_Ln_le:
 fixes z :: complex
 assumes "norm z < 1/2"
 shows "norm (Ln(1+z)) \ 2 * norm z"
proof -
 have sums: "(\n. - ((- z) ^ n) / of_nat n) sums ln (1 + z)"
 by (intro Ln_series') (use assms in auto)
 have summable: "summable (\n. norm (- ((- z) ^ n / of_nat n)))"
 using ln_series'[of "-norm z"] assms
 by (simp add: sums_iff summable_minus_iff norm_power norm_divide)

 have "norm (ln (1 + z)) = norm (\n. -((-z) ^ n / of_nat n))"
 using sums by (simp add: sums_iff)
 also have "\ \ (\n. norm (-((-z) ^ n / of_nat n)))"
 using summable by (rule summable_norm)
 also have "\ = (\n. norm (-((-z) ^ Suc n / of_nat (Suc n))))"
 using summable by (subst suminf_split_head) auto
 also have "\ \ (\n. norm z * (1 / 2) ^ n)"
 proof (rule suminf_le)
 show "summable (\n. norm z * (1 / 2) ^ n)"
 by (intro summable_mult summable_geometric) auto
 next
 show "summable (\n. norm (- ((- z) ^ Suc n / of_nat (Suc n))))"
 using summable by (subst summable_Suc_iff)
 next
 fix n
 have "norm (-((-z) ^ Suc n / of_nat (Suc n))) = norm z * (norm z ^ n / real (Suc n))"
 by (simp add: norm_power norm_divide norm_mult del: of_nat_Suc)
 also have "\ \ norm z * ((1 / 2) ^ n / 1)"
 using assms by (intro mult_left_mono frac_le power_mono) auto
 finally show "norm (- ((- z) ^ Suc n / of_nat (Suc n))) \ norm z * (1 / 2) ^ n"
 by simp
 qed
 also have "\ = norm z * (\n. (1 / 2) ^ n)"
 by (subst suminf_mult) (auto intro: summable_geometric)
 also have "(\n. (1 / 2 :: real) ^ n) = 2"
 using geometric_sums[of "1 / 2 :: real"] by (simp add: sums_iff)
 finally show ?thesis
 by (simp add: mult_ac)
qed

subsection\<^marker>\<open>tag unimportant\<close>\<open>Quadrant-type results for Ln\<close>

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

--> maximum size reached

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

quality98%

¤ Dauer der Verarbeitung: 0.37 Sekunden ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.