Theory Complex_Transcendental

section ‹Complex Transcendental Functions›

text‹By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)›

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

subsection‹Möbius transformations›

(* TODO: Figure out what to do with Möbius transformations *)
definitiontag important› "moebius a b c d  (λ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" "r0"
    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  x0  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)2 < 1 + cmod (1 - z2)"
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 - z2" "1"] show ?thesis
    by (simp add: norm_power Im_power2)
qed

subsectiontag unimportant›‹The Exponential Function›

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‹Euler and de Moivre formulas›

text‹The sine series times termi
lemma sin_i_eq: "(λn. (𝗂 * sin_coeff n) * z^n) sums (𝗂 * sin z)"
proof -
  have "(λn. 𝗂 * sin_coeff n *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 /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

corollarytag unimportant› 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)

subsectiontag unimportant›‹Relationships between real and complex trigonometric and hyperbolic functions›

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)

subsectiontag unimportant›‹More on the Polar Representation of Complex Numbers›

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 ?lhs 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_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)))2 = r12 + r22 + 2 * r1 * r2 * cos (θ1 - θ2)" (is "(cmod (?z1 + ?z2))2 = ?rhs")
proof -
  have "(cmod (?z1 + ?z2))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)2 + (norm ?z2)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)))2 = r12 + r22 - 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  R)  (k. (λj. θ j - of_int (k j) * (2 * pi))  Θ)"    (is "(?z  ?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)2 + R2 - (norm(?z j - ?Z))2) / (2 * R * r j)" for j
      using assms by (auto simp: cmod_diff_squared less_le)
    moreover have "(λj. ((r j)2 + R2 - (norm(?z j - ?Z))2) / (2 * R * r j))  ((R2 + R2 - (norm(?Z - ?Z))2) / (2 * R * R))"
      by (intro L rR tendsto_intros) (use R > 0 in force)
    moreover have "((R2 + R2 - (norm(?Z - ?Z))2) / (2 * R * R)) = 1"
      using R > 0 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<..<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 
      (n. z = w - 2 * 𝗂 * of_real n * of_real pi 
              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


subsectiontag unimportant›‹Taylor series for complex exponential, sine and cosine›

declare power_Suc [simp del]

lemma Taylor_exp_field:
  fixes z::"'a::{banach,real_normed_field}"
  shows "norm (exp z - (in. 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 ‹For complex @{term z}, a tighter bound than in the previous result›
lemma Taylor_exp:
  "norm(exp z - (kn. 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 *R z))  exp ¦Im z¦"
    and cmod_cos_le_exp: "cmod (cos (u *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 *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 *R z))  exp ¦Im z¦" .
  have "cmod (cos (u *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 *R z))  exp ¦Im z¦" .
qed

lemma Taylor_sin:
  "norm(sin z - (kn. complex_of_real (sin_coeff k) * z ^ k))
    exp¦Im z¦ * (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 -
                 (in. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
            exp ¦Im z¦ * 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 - (kn. complex_of_real (cos_coeff k) * z ^ k))
    exp¦Im z¦ * (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 -
                 (in. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
            exp ¦Im z¦ * 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‹32-bit Approximation to e›
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‹Apparently redundant. But many arguments involve integers.›
lemma ln3_gt_1: "ln 3 > (1::real)"
  by (simp add: less_trans [OF ln_272_gt_1])

subsection‹The argument of a complex number (HOL Light version)›

definitiontag important› is_Arg :: "[complex,real]  bool"
  where "is_Arg z r  z = of_real(norm z) * exp(𝗂 * of_real r)"

definitiontag important› Arg2pi :: "complex  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‹This function returns the angle of a complex number from its representation in polar coordinates.
Due to periodicity, its range is arbitrary. termArg2pi follows HOL Light in adopting the interval [0,2π)›.
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 (-π,π]›.
The present version is provided for compatibility.›

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

corollarytag unimportant›
  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 auto simp: norm_mult)

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

corollarytag unimportant› Arg2pi_gt_0:
  assumes "z  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 φ] 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

subsectiontag unimportant›‹Analytic properties of tangent function›

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
          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‹The principal branch of the Complex logarithm›

instantiation complex :: ln
begin

definitiontag important› ln_complex :: "complex  complex"
  where "ln_complex  λz. THE w. exp w = z & -pi < Im(w) & Im(w)  pi"

text‹NOTE: within this scope, the constant Ln is not yet available!›
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 ψ where z: "z / (cmod z) = Complex (cos ψ) (sin ψ)"
    using complex_unimodular_polar [of "z / (norm z)"] assms
    by (auto simp: norm_divide field_split_simps)
  obtain φ where φ: "- pi < φ" "φ  pi" "sin φ = sin ψ" "cos φ = cos ψ"
    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 φ
    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

subsectiontag unimportant›‹Relation to Real Logarithm›

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)

corollarytag unimportant› Ln_in_Reals [simp]: "z    Re z > 0  ln z  "
  by (auto simp: Ln_of_real elim: Reals_cases)

corollarytag unimportant› Im_Ln_of_real [simp]: "r > 0  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  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)

corollarytag unimportant› ln_cmod_le:
  assumes z: "z  0"
    shows "ln (cmod z)  cmod (Ln z)"
  by (metis Re_Ln complex_Re_le_cmod z)

propositiontag unimportant› 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)

corollarytag unimportant› 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)

subsectiontag unimportant›‹Derivative of Ln away from the branch cut›

lemma Im_Ln_less_pi: 
  assumes "z  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  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)) oL 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 = (λx. x/z)"
      by (metis z  V 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 z  V] g' by (simp add: divide_inverse_commute)
  qed (auto simp: z  V open V)
qed

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

lemma field_differentiable_at_Ln: "z  0  Ln field_differentiable at z"
  using field_differentiable_def has_field_derivative_Ln by blast

lemma field_differentiable_within_Ln: "z  0
          Ln field_differentiable (at z within S)"
  using field_differentiable_at_Ln field_differentiable_within_subset by blast

lemma continuous_at_Ln: "z  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  0  isCont (λx. Ln (f x)) z"
  by (blast intro: isCont_o2 [OF _ continuous_at_Ln])

lemma continuous_within_Ln [continuous_intros]: "z  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  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  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  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  0)  f holomorphic_on A  (λz. Ln (f z)) holomorphic_on A"
  using holomorphic_on_compose_gen[OF _ holomorphic_on_Ln, of f A "- 0"]
  by (auto simp: o_def)

lemma analytic_on_ln [analytic_intros]:
  assumes "f analytic_on A" "f ` A  0 =