# 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 *)
definition✐‹tag 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
with assms show ?thesis
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)

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)"
then show ?thesis using assms Complex
apply (rule power2_less_imp_less, auto)
done
qed

lemma cmod_diff_real_less: "Im z ≠ 0 ⟹ x≠0 ⟹ cmod (z - x) < cmod z + ¦x¦"
by simp

lemma cmod_square_less_1_plus:
assumes "Im z = 0 ⟹ ¦Re z¦ < 1"
shows "(cmod z)⇧2 < 1 + cmod (1 - z⇧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⇧2" "1"] show ?thesis
qed

subsection✐‹tag 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"

lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"

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"
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 \<^term>‹i››
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
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]]
ultimately show ?thesis
using sums_unique2 by blast
qed

corollary✐‹tag 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*𝗂)"

lemma sin_exp_eq': "sin z = 𝗂 * (exp(-(𝗂 * z)) - exp(𝗂 * z)) / 2"

lemma cos_exp_eq:  "cos z = (exp(𝗂 * z) + exp(-(𝗂 * z))) / 2"

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✐‹tag unimportant›‹Relationships between real and complex trigonometric and hyperbolic functions›

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

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

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)"

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)"

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)"

lemma holomorphic_on_sin: "sin holomorphic_on S"

lemma holomorphic_on_cos: "cos holomorphic_on S"

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]: "sin analytic_on A"
using analytic_on_holomorphic holomorphic_on_sin by blast

lemma analytic_on_sin' [analytic_intros]:
"f analytic_on A ⟹ (⋀z. z ∈ A ⟹ f z ∉ range (λn. complex_of_real pi * of_int n)) ⟹
(λz. sin (f z)) analytic_on A"
using analytic_on_compose_gen[OF _ analytic_on_sin[of UNIV], of f A] by (simp add: o_def)

lemma analytic_on_cos [analytic_intros]: "cos analytic_on A"
using analytic_on_holomorphic holomorphic_on_cos by blast

lemma analytic_on_cos' [analytic_intros]:
"f analytic_on A ⟹ (⋀z. z ∈ A ⟹ f z ∉ range (λn. complex_of_real pi * of_int n)) ⟹
(λz. cos (f z)) analytic_on A"
using analytic_on_compose_gen[OF _ analytic_on_cos[of UNIV], of f A] by (simp add: o_def)

subsection✐‹tag 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"
also have "… ⟷ (Re w = Re z ∧ (∃n::int. Im w - Im z = of_int (2 * n) * pi))"
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"

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"
then have "norm (2 * of_int n * of_real pi * 𝗂) < 2*pi"
then show "n = 0"
by (auto simp: norm_mult)
qed

fixes r1 r2::real
shows "(cmod (r1 * exp (𝗂 * θ1) + r2 * exp (𝗂 * θ2)))⇧2 = r1⇧2 + r2⇧2 + 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)"
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 = r1⇧2 + r2⇧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 ⇢ 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 + R⇧2 - (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 + R⇧2 - (norm(?z j - ?Z))⇧2) / (2 * R * r j)) ⇢ ((R⇧2 + R⇧2 - (norm(?Z - ?Z))⇧2) / (2 * R * R))"
by (intro L rR tendsto_intros) (use ‹R > 0› in force)
moreover have "((R⇧2 + R⇧2 - (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 sin_cos_eq_iff: "sin y = sin x ∧ cos y = cos x ⟷ (∃n::int. y = x + 2 * pi * n)" (is "?L=?R")
proof
assume ?L
then have "cos (y-x) = 1"
using cos_add [of y "-x"] by simp
then show ?R
next
assume ?R
then show ?L
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))"

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"]

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"]

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"
also have "… ⟷ (∃n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
also have "… = ?rhs"
apply safe
apply (rule_tac [2] x="-(x+1)" in exI)
apply (rule_tac x="-(x+1)" in exI)
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"

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"]
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]
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

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)"

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)
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)
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)"

lemma cos_conv_cosh: "cos z = cosh (𝗂*z)"

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)"
also have "… ⟷ ?rhs"
by (subst complex_sin_eq) (force simp: field_simps complex_eq_iff)
finally show ?thesis .
qed

subsection✐‹tag 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 - (∑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 ‹For complex @{term z}, a tighter bound than in the previous result›
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¦"
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 - (∑k≤n. 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 -
(∑i≤n. (-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 - (∑k≤n. 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 -
(∑i≤n. (-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)›

definition✐‹tag important› is_Arg :: "[complex,real] ⇒ bool"
where "is_Arg z r ≡ z = of_real(norm z) * exp(𝗂 * of_real r)"

definition✐‹tag 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"

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. \<^term>‹Arg2pi› 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"

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
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 (rule theI [where a=t])
using t z False
apply (auto intro: Arg2pi_unique_lemma)
done
qed

corollary✐‹tag 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

corollary✐‹tag 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)"

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)

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"

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
by (metis (no_types, opaque_lifting) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
qed

subsection✐‹tag 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"

lemma holomorphic_on_tan: "(⋀z. z ∈ s ⟹ cos z ≠ 0) ⟹ tan holomorphic_on s"

subsection‹The principal branch of the Complex logarithm›

instantiation complex :: ln
begin

definition✐‹tag 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

subsection✐‹tag 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)

corollary✐‹tag unimportant› Ln_in_Reals [simp]: "z ∈ ℝ ⟹ Re z > 0 ⟹ ln z ∈ ℝ"
by (auto simp: Ln_of_real elim: Reals_cases)

corollary✐‹tag unimportant› Im_Ln_of_real [simp]: "r > 0 ⟹ Im (ln (of_real r)) = 0"

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)

corollary✐‹tag unimportant› ln_cmod_le:
assumes z: "z ≠ 0"
shows "ln (cmod z) ≤ cmod (Ln z)"
by (metis Re_Ln complex_Re_le_cmod z)

proposition✐‹tag 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)

corollary✐‹tag 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)

subsection✐‹tag 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)) o⇩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 = (λ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"

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"