# Theory Complex_Geometry.More_Complex

(* -------------------------------------------------------------------------- *)
subsection ‹Library Additions for Complex Numbers›
(* -------------------------------------------------------------------------- *)

theory More_Complex
imports Complex_Main More_Transcendental Canonical_Angle
begin

text ‹Conjugation and @{term cis}›

declare cis_cnj[simp]

lemmas complex_cnj = complex_cnj_diff complex_cnj_mult complex_cnj_add complex_cnj_divide complex_cnj_minus

text ‹Some properties for @{term complex_of_real}. Also, since it is often used in our
formalization we abbreviate it to @{term cor}.›

abbreviation cor :: "real ⇒ complex" where
"cor ≡ complex_of_real"

lemma cmod_cis [simp]:
assumes "a ≠ 0"
shows "of_real (cmod a) * cis (Arg a) = a"
using assms
by (metis rcis_cmod_Arg rcis_def)

lemma cis_cmod [simp]:
assumes "a ≠ 0"
shows "cis (Arg a) * of_real (cmod a) = a"
by (metis assms cmod_cis mult.commute)

lemma cor_squared:
shows "(cor x)⇧2 = cor (x⇧2)"

lemma cor_sqrt_mult_cor_sqrt [simp]:
shows "cor (sqrt A) * cor (sqrt A) = cor ¦A¦"
by (metis of_real_mult real_sqrt_mult_self)

lemma cor_eq_0: "cor x + 𝗂 * cor y = 0 ⟷ x = 0 ∧ y = 0"
by (metis Complex_eq Im_complex_of_real Im_i_times Re_complex_of_real add_cancel_left_left of_real_eq_0_iff plus_complex.sel(2) zero_complex.code)

lemma one_plus_square_neq_zero [simp]:
shows "1 + (cor x)⇧2 ≠ 0"
by (metis (opaque_lifting, no_types) of_real_1 of_real_add of_real_eq_0_iff of_real_power power_one sum_power2_eq_zero_iff zero_neq_one)

these should be deprecated.›

lemma complex_real_two [simp]:
shows "Complex 2 0 = 2"

lemma complex_double [simp]:
shows "(Complex a b) * 2 = Complex (2*a) (2*b)"

lemma complex_half [simp]:
shows "(Complex a b) / 2 = Complex (a/2) (b/2)"
by (subst complex_eq_iff) auto

lemma Complex_scale1:
shows "Complex (a * b) (a * c) = cor a * Complex b c"
unfolding complex_of_real_def
unfolding Complex_eq

lemma Complex_scale2:
shows "Complex (a * c) (b * c) = Complex a b * cor c"
unfolding complex_of_real_def
unfolding Complex_eq

lemma Complex_scale3:
shows "Complex (a / b) (a / c) = cor a * Complex (1 / b) (1 / c)"
unfolding complex_of_real_def
unfolding Complex_eq

lemma Complex_scale4:
shows "c ≠ 0 ⟹ Complex (a / c) (b / c) = Complex a b / cor c"
unfolding complex_of_real_def
unfolding Complex_eq
by (auto simp add: field_simps power2_eq_square)

lemma Complex_Re_express_cnj:
shows "Complex (Re z) 0 = (z + cnj z) / 2"
by (cases z) (simp add: Complex_eq)

lemma Complex_Im_express_cnj:
shows "Complex 0 (Im z) = (z - cnj z)/2"
by (cases z) (simp add: Complex_eq)

text ‹Additional properties of @{term cmod}.›

lemma complex_mult_cnj_cmod:
shows "z * cnj z = cor ((cmod z)⇧2)"
using complex_norm_square
by auto

lemma cmod_square:
shows "(cmod z)⇧2 = Re (z * cnj z)"
using complex_mult_cnj_cmod[of z]

lemma cor_cmod_power_4 [simp]:
shows "cor (cmod z) ^ 4 = (z * cnj z)⇧2"

lemma cnjE:
assumes "x ≠ 0"
shows "cnj x = cor ((cmod x)⇧2) / x"
using complex_mult_cnj_cmod[of x] assms

lemma cmod_cor_divide [simp]:
shows "cmod (z / cor k) = cmod z / ¦k¦"

lemma cmod_mult_minus_left_distrib [simp]:
shows "cmod (z*z1 - z*z2) = cmod z * cmod(z1 - z2)"
by (metis norm_mult right_diff_distrib)

lemma cmod_eqI:
assumes "z1 * cnj z1 = z2 * cnj z2"
shows "cmod z1 = cmod z2"
using assms
by (subst complex_mod_sqrt_Re_mult_cnj)+ auto

lemma cmod_eqE:
assumes "cmod z1 = cmod z2"
shows "z1 * cnj z1 = z2 * cnj z2"

lemma cmod_eq_one [simp]:
shows "cmod a = 1 ⟷ a*cnj a = 1"
by (metis cmod_eqE cmod_eqI complex_cnj_one monoid_mult_class.mult.left_neutral norm_one)

text ‹We introduce @{term is_real} (the imaginary part of complex number is zero) and @{term is_imag}
(real part of complex number is zero) operators and prove some of their properties.›

abbreviation is_real where
"is_real z ≡ Im z = 0"

abbreviation is_imag where
"is_imag z ≡ Re z = 0"

lemma real_imag_0:
assumes "is_real a" "is_imag a"
shows "a = 0"
using assms

lemma complex_eq_if_Re_eq:
assumes "is_real z1" and "is_real z2"
shows "z1 = z2 ⟷ Re z1 = Re z2"
using assms
by (cases z1, cases z2) auto

lemma mult_reals [simp]:
assumes "is_real a" and "is_real b"
shows "is_real (a * b)"
using assms
by auto

lemma div_reals [simp]:
assumes "is_real a" and "is_real b"
shows "is_real (a / b)"
using assms

lemma complex_of_real_Re [simp]:
assumes "is_real k"
shows "cor (Re k) = k"
using assms
by (cases k) (auto simp add: complex_of_real_def)

lemma cor_cmod_real:
assumes "is_real a"
shows "cor (cmod a) = a ∨ cor (cmod a) = -a"
using assms
unfolding cmod_def
by (cases "Re a > 0") auto

lemma eq_cnj_iff_real:
shows "cnj z = z ⟷ is_real z"
by (cases z) (simp add: Complex_eq)

lemma eq_minus_cnj_iff_imag:
shows "cnj z = -z ⟷ is_imag z"
by (cases z) (simp add: Complex_eq)

lemma Re_divide_real:
assumes "is_real b" and "b ≠ 0"
shows "Re (a / b) = (Re a) / (Re b)"
using assms

lemma Re_mult_real:
assumes "is_real a"
shows "Re (a * b) = (Re a) * (Re b)"
using assms
by simp

lemma Im_mult_real:
assumes "is_real a"
shows "Im (a * b) = (Re a) * (Im b)"
using assms
by simp

lemma Im_divide_real:
assumes "is_real b" and "b ≠ 0"
shows "Im (a / b) = (Im a) / (Re b)"
using assms

lemma Re_sgn:
assumes "is_real R"
shows "Re (sgn R) = sgn (Re R)"
using assms
by (metis Re_sgn complex_of_real_Re norm_of_real real_sgn_eq)

lemma is_real_div:
assumes "b ≠ 0"
shows "is_real (a / b) ⟷ a*cnj b = b*cnj a"
using assms
by (metis complex_cnj_divide complex_cnj_zero_iff eq_cnj_iff_real frac_eq_eq mult.commute)

lemma is_real_mult_real:
assumes "is_real a" and "a ≠ 0"
shows "is_real b ⟷ is_real (a * b)"
using assms
by (cases a, auto simp add: Complex_eq)

lemma Im_express_cnj:
shows "Im z = (z - cnj z) / (2 * 𝗂)"

lemma Re_express_cnj:
shows "Re z = (z + cnj z) / 2"

text ‹Rotation of complex number for 90 degrees in the positive direction.›

abbreviation rot90 where
"rot90 z ≡ Complex (-Im z) (Re z)"

lemma rot90_ii:
shows "rot90 z = z * 𝗂"
by (metis Complex_mult_i complex_surj)

text ‹With @{term cnj_mix} we introduce scalar product between complex vectors. This operation shows
to be useful to succinctly express some conditions.›

abbreviation cnj_mix where
"cnj_mix z1 z2 ≡ cnj z1 * z2 + z1 * cnj z2"

abbreviation scalprod where
"scalprod z1 z2 ≡ cnj_mix z1 z2 / 2"

lemma cnj_mix_minus:
shows "cnj z1*z2 - z1*cnj z2 = 𝗂 * cnj_mix (rot90 z1) z2"
by (cases z1, cases z2) (simp add: Complex_eq field_simps)

lemma cnj_mix_minus':
shows "cnj z1*z2 - z1*cnj z2 = rot90 (cnj_mix (rot90 z1) z2)"
by (cases z1, cases z2) (simp add: Complex_eq field_simps)

lemma cnj_mix_real [simp]:
shows "is_real (cnj_mix z1 z2)"
by (cases z1, cases z2) simp

lemma scalprod_real [simp]:
shows "is_real (scalprod z1 z2)"
using cnj_mix_real
by simp

text ‹Additional properties of @{term cis} function.›

lemma cis_minus_pi2 [simp]:
shows "cis (-pi/2) = -𝗂"

lemma cis_pi2_minus_x [simp]:
shows "cis (pi/2 - x) = 𝗂 * cis(-x)"
using cis_divide[of "pi/2" x, symmetric]
using cis_divide[of 0 x, symmetric]
by simp

lemma cis_pm_pi [simp]:
shows "cis (x - pi) = - cis x" and  "cis (x + pi) = - cis x"

lemma cis_times_cis_opposite [simp]:
shows "cis φ * cis (- φ) = 1"

text ‹@{term cis} repeats only after $2k\pi$›
lemma cis_eq:
assumes "cis a = cis b"
shows "∃ k::int. a - b = 2 * k * pi"
using assms sin_cos_eq[of a b]
using cis.sel[of a] cis.sel[of b]
by (cases "cis a", cases "cis b") auto

text ‹@{term cis} is injective on $(-\pi, \pi]$.›
lemma cis_inj:
assumes "-pi < α" and "α ≤ pi" and "-pi < α'" and "α' ≤ pi"
assumes "cis α = cis α'"
shows "α = α'"
using assms
by (metis cis_Arg_unique sgn_cis)

text ‹@{term cis} of an angle combined with @{term cis} of the opposite angle›

lemma cis_diff_cis_opposite [simp]:
shows "cis φ - cis (- φ) = 2 * 𝗂 * sin φ"
using Im_express_cnj[of "cis φ"]
by simp

lemma cis_opposite_diff_cis [simp]:
shows "cis (-φ) - cis (φ) = - 2 * 𝗂 * sin φ"
using cis_diff_cis_opposite[of "-φ"]
by simp

shows "cis φ + cis (-φ) = 2 * cos φ"

text ‹@{term cis} equal to 1 or -1›
lemma cis_one [simp]:
assumes "sin φ = 0" and "cos φ = 1"
shows "cis φ = 1"
using assms
by (auto simp add: cis.ctr one_complex.code)

lemma cis_minus_one [simp]:
assumes "sin φ = 0" and "cos φ = -1"
shows "cis φ = -1"
using assms
by (auto simp add: cis.ctr Complex_eq_neg_1)

(* -------------------------------------------------------------------------- *)
subsubsection ‹Additional properties of complex number argument›
(* -------------------------------------------------------------------------- *)

text ‹@{term Arg} of real numbers›

lemma is_real_arg1:
assumes "Arg z = 0 ∨ Arg z = pi"
shows "is_real z"
using assms
using rcis_cmod_Arg[of z] Im_rcis[of "cmod z" "Arg z"]
by auto

lemma is_real_arg2:
assumes "is_real z"
shows "Arg z = 0 ∨ Arg z = pi"
proof (cases "z = 0")
case False
thus ?thesis
using Arg_bounded[of z]
by (smt (verit, best) Im_sgn assms cis.simps(2) cis_Arg div_0 sin_zero_pi_iff)

lemma arg_complex_of_real_positive [simp]:
assumes "k > 0"
shows "Arg (cor k) = 0"
proof-
have "cos (Arg (Complex k 0)) > 0"
using assms
using rcis_cmod_Arg[of "Complex k 0"] Re_rcis[of "cmod (Complex k 0)" "Arg (Complex k 0)"]
using cmod_eq_Re by force
thus ?thesis
using assms is_real_arg2[of "cor k"]
unfolding complex_of_real_def
by auto
qed

lemma arg_complex_of_real_negative [simp]:
assumes "k < 0"
shows "Arg (cor k) = pi"
proof-
have "cos (Arg (Complex k 0)) < 0"
using ‹k < 0› rcis_cmod_Arg[of "Complex k 0"] Re_rcis[of "cmod (Complex k 0)" "Arg (Complex k 0)"]
by (metis complex.sel(1) mult_less_0_iff norm_not_less_zero)
thus ?thesis
using assms is_real_arg2[of "cor k"]
unfolding complex_of_real_def
by auto
qed

lemma arg_0_iff:
shows "z ≠ 0 ∧ Arg z = 0 ⟷ is_real z ∧ Re z > 0"
by (smt arg_complex_of_real_negative arg_complex_of_real_positive Arg_zero complex_of_real_Re is_real_arg1 pi_gt_zero zero_complex.simps)

lemma arg_pi_iff:
shows "Arg z = pi ⟷ is_real z ∧ Re z < 0"
by (smt arg_complex_of_real_negative arg_complex_of_real_positive Arg_zero complex_of_real_Re is_real_arg1 pi_gt_zero zero_complex.simps)

text ‹@{term Arg} of imaginary numbers›

lemma is_imag_arg1:
assumes "Arg z = pi/2 ∨ Arg z = -pi/2"
shows "is_imag z"
using assms
using rcis_cmod_Arg[of z] Re_rcis[of "cmod z" "Arg z"]
by (metis cos_minus cos_pi_half minus_divide_left mult_eq_0_iff)

lemma is_imag_arg2:
assumes "is_imag z" and "z ≠ 0"
shows "Arg z = pi/2 ∨ Arg z = -pi/2"
using Arg_bounded assms cos_0_iff_canon cos_Arg_i_mult_zero by presburger

lemma arg_complex_of_real_times_i_positive [simp]:
assumes "k > 0"
shows "Arg (cor k * 𝗂) = pi / 2"
proof-
have "sin (Arg (Complex 0 k)) > 0"
using ‹k > 0› rcis_cmod_Arg[of "Complex 0 k"] Im_rcis[of "cmod (Complex 0 k)" "Arg (Complex 0 k)"]
by (smt complex.sel(2) mult_nonneg_nonpos norm_ge_zero)
thus ?thesis
using assms is_imag_arg2[of "cor k * 𝗂"]
using Arg_zero complex_of_real_i
by force
qed

lemma arg_complex_of_real_times_i_negative [simp]:
assumes "k < 0"
shows "Arg (cor k * 𝗂) = - pi / 2"
proof-
have "sin (Arg (Complex 0 k)) < 0"
using ‹k < 0› rcis_cmod_Arg[of "Complex 0 k"] Im_rcis[of "cmod (Complex 0 k)" "Arg (Complex 0 k)"]
by (metis complex.sel(2) mult_less_0_iff norm_not_less_zero)
thus ?thesis
using assms is_imag_arg2[of "cor k * 𝗂"]
using Arg_zero complex_of_real_i[of k]
by (smt complex.sel(1) sin_pi_half sin_zero)
qed

lemma arg_pi2_iff:
shows "z ≠ 0 ∧ Arg z = pi / 2 ⟷ is_imag z ∧ Im z > 0"
by (smt Im_rcis Re_i_times Re_rcis arcsin_minus_1 cos_pi_half divide_minus_left mult.commute mult_cancel_right1 rcis_cmod_Arg is_imag_arg2 sin_arcsin sin_pi_half zero_less_mult_pos zero_less_norm_iff)

lemma arg_minus_pi2_iff:
shows "z ≠ 0 ∧ Arg z = - pi / 2 ⟷ is_imag z ∧ Im z < 0"
by (smt arg_pi2_iff complex.expand divide_cancel_right pi_neq_zero is_imag_arg1 is_imag_arg2 zero_complex.simps(1) zero_complex.simps(2))

text ‹Argument is a canonical angle›

lemma canon_ang_arg:
shows "⇂Arg z⇃ = Arg z"
using canon_ang_id[of "Arg z"] Arg_bounded
by simp

lemma arg_cis:
shows "Arg (cis φ) = ⇂φ⇃"
using cis_Arg_unique canon_ang canon_ang_cos canon_ang_sin cis.ctr sgn_cis by presburger

text ‹Cosine and sine of @{term Arg}›

lemma cos_arg:
assumes "z ≠ 0"
shows "cos (Arg z) = Re z / cmod z"
by (metis Complex.Re_sgn cis.simps(1) assms cis_Arg)

lemma sin_arg:
assumes "z ≠ 0"
shows "sin (Arg z) = Im z / cmod z"
by (metis Complex.Im_sgn cis.simps(2) assms cis_Arg)

text ‹Argument of product›

lemma cis_arg_mult:
assumes "z1 * z2 ≠ 0"
shows "cis (Arg (z1 * z2)) = cis (Arg z1 + Arg z2)"
by (metis assms cis_Arg cis_mult mult_eq_0_iff sgn_mult)

lemma arg_mult_2kpi:
assumes "z1 * z2 ≠ 0"
shows "∃ k::int. Arg (z1 * z2) = Arg z1 + Arg z2 + 2*k*pi"
proof-
have "cis (Arg (z1*z2)) = cis (Arg z1 + Arg z2)"
by (rule cis_arg_mult[OF assms])
thus ?thesis
using cis_eq[of "Arg (z1*z2)" "Arg z1 + Arg z2"]
qed

lemma arg_mult:
assumes "z1 * z2 ≠ 0"
shows "Arg(z1 * z2) = ⇂Arg z1 + Arg z2⇃"
proof-
obtain k::int where "Arg(z1 * z2) = Arg z1 + Arg z2 + 2*k*pi"
using arg_mult_2kpi[of z1 z2]
using assms
by auto
hence "⇂Arg(z1 * z2)⇃ = ⇂Arg z1 + Arg z2⇃"
using canon_ang_eq
thus ?thesis
using canon_ang_arg[of "z1*z2"]
by auto
qed

lemma arg_mult_real_positive [simp]:
assumes "k > 0"
shows "Arg (cor k * z) = Arg z"
proof (cases "z = 0")
case False
thus ?thesis
using arg_mult assms canon_ang_arg by force
qed (auto simp: Arg_zero)

lemma arg_mult_real_negative [simp]:
assumes "k < 0"
shows "Arg (cor k * z) = Arg (-z)"
proof (cases "z = 0")
case False
thus ?thesis
using assms
by (metis arg_mult_real_positive minus_mult_commute neg_0_less_iff_less of_real_minus minus_minus)
qed (auto simp: Arg_zero)

lemma arg_div_real_positive [simp]:
assumes "k > 0"
shows "Arg (z / cor k) = Arg z"
proof(cases "z = 0")
case True
thus ?thesis
by auto
next
case False
thus ?thesis
using assms
using arg_mult_real_positive[of "1/k" z]
by auto
qed

lemma arg_div_real_negative [simp]:
assumes "k < 0"
shows "Arg (z / cor k) = Arg (-z)"
proof(cases "z = 0")
case True
thus ?thesis
by auto
next
case False
thus ?thesis
using assms
using arg_mult_real_negative[of "1/k" z]
by auto
qed

lemma arg_mult_eq:
assumes "z * z1 ≠ 0" and "z * z2 ≠ 0"
assumes "Arg (z * z1) = Arg (z * z2)"
shows "Arg z1 = Arg z2"
by (metis (no_types, lifting) arg_cis assms canon_ang_arg cis_Arg mult_eq_0_iff nonzero_mult_div_cancel_left sgn_divide)

text ‹Argument of conjugate›

lemma arg_cnj_pi:
assumes "Arg z = pi"
shows "Arg (cnj z) = pi"
using arg_pi_iff assms by auto

lemma arg_cnj_not_pi:
assumes "Arg z ≠ pi"
shows "Arg (cnj z) = -Arg z"
proof(cases "Arg z = 0")
case True
thus ?thesis
using eq_cnj_iff_real[of z] is_real_arg1[of z] by force
next
case False
have "Arg (cnj z) = Arg z ∨ Arg(cnj z) = -Arg z"
using Arg_bounded[of z] Arg_bounded[of "cnj z"]
by (smt (verit, best) arccos_cos arccos_cos2 cnj.sel(1) complex_cnj_zero_iff complex_mod_cnj cos_arg)
moreover
have "Arg (cnj z) ≠ Arg z"
using sin_0_iff_canon[of "Arg (cnj z)"] Arg_bounded False assms
by (metis complex_mod_cnj eq_cnj_iff_real is_real_arg2 rcis_cmod_Arg)
ultimately
show ?thesis
by auto
qed

text ‹Argument of reciprocal›

lemma arg_inv_not_pi:
assumes "z ≠ 0" and "Arg z ≠ pi"
shows "Arg (1 / z) = - Arg z"
proof-
have "1/z = cnj z / cor ((cmod z)⇧2 )"
using ‹z ≠ 0› complex_mult_cnj_cmod[of z]
thus ?thesis
using arg_div_real_positive[of "(cmod z)⇧2" "cnj z"] ‹z ≠ 0›
using arg_cnj_not_pi[of z] ‹Arg z ≠ pi›
by auto
qed

lemma arg_inv_pi:
assumes "z ≠ 0" and "Arg z = pi"
shows "Arg (1 / z) = pi"
proof-
have "1/z = cnj z / cor ((cmod z)⇧2 )"
using ‹z ≠ 0› complex_mult_cnj_cmod[of z]
thus ?thesis
using arg_div_real_positive[of "(cmod z)⇧2" "cnj z"] ‹z ≠ 0›
using arg_cnj_pi[of z] ‹Arg z = pi›
by auto
qed

lemma arg_inv_2kpi:
assumes "z ≠ 0"
shows "∃ k::int. Arg (1 / z) = - Arg z + 2*k*pi"
using arg_inv_pi[OF assms]
using arg_inv_not_pi[OF assms]
by (cases "Arg z = pi") (rule_tac x="1" in exI, simp, rule_tac x="0" in exI, simp)

lemma arg_inv:
assumes "z ≠ 0"
shows "Arg (1 / z) = ⇂- Arg z⇃"
by (metis arg_inv_not_pi arg_inv_pi assms canon_ang_arg canon_ang_uminus_pi)

text ‹Argument of quotient›

lemma arg_div_2kpi:
assumes "z1 ≠ 0" and "z2 ≠ 0"
shows "∃ k::int. Arg (z1 / z2) = Arg z1 - Arg z2 + 2*k*pi"
proof-
obtain x1 where "Arg (z1 * (1 / z2)) = Arg z1 + Arg (1 / z2) + 2 * real_of_int x1 * pi"
using assms arg_mult_2kpi[of z1 "1/z2"]
by auto
moreover
obtain x2 where "Arg (1 / z2) = - Arg z2 + 2 * real_of_int x2 * pi"
using assms arg_inv_2kpi[of z2]
by auto
ultimately
show ?thesis
by (rule_tac x="x1 + x2" in exI, simp add: field_simps)
qed

lemma arg_div:
assumes "z1 ≠ 0" and "z2 ≠ 0"
shows "Arg(z1 / z2) = ⇂Arg z1 - Arg z2⇃"
proof-
obtain k::int where "Arg(z1 / z2) = Arg z1 - Arg z2 + 2*k*pi"
using arg_div_2kpi[of z1 z2]
using assms
by auto
hence "canon_ang(Arg(z1 / z2)) = canon_ang(Arg z1 - Arg z2)"
using canon_ang_eq
thus ?thesis
using canon_ang_arg[of "z1/z2"]
by auto
qed

text ‹Argument of opposite›

lemma arg_uminus:
assumes "z ≠ 0"
shows "Arg (-z) = ⇂Arg z + pi⇃"
using assms
using arg_mult[of "-1" z]
using arg_complex_of_real_negative[of "-1"]

lemma arg_uminus_opposite_sign:
assumes "z ≠ 0"
shows "Arg z > 0 ⟷ ¬ Arg (-z) > 0"
proof (cases "Arg z = 0")
case True
thus ?thesis
using assms
next
case False
show ?thesis
proof (cases "Arg z > 0")
case True
thus ?thesis
using assms
using Arg_bounded[of z]
using canon_ang_plus_pi1[of "Arg z"]
next
case False
thus ?thesis
using ‹Arg z ≠ 0›
using assms
using Arg_bounded[of z]
using canon_ang_plus_pi2[of "Arg z"]
qed
qed

text ‹Sign of argument is the same as the sign of the Imaginary part›

lemma arg_Im_sgn:
assumes "¬ is_real z"
shows "sgn (Arg z) = sgn (Im z)"
proof-
have "z ≠ 0"
using assms
by auto
then obtain r φ where polar: "z = cor r * cis φ" "φ = Arg z" "r > 0"
by (smt cmod_cis mult_eq_0_iff norm_ge_zero of_real_0)
hence "Im z = r * sin φ"
by (metis Im_mult_real Re_complex_of_real cis.simps(2) Im_complex_of_real)
hence  "Im z > 0 ⟷ sin φ > 0" "Im z < 0 ⟷ sin φ < 0"
using ‹r > 0›
using mult_pos_pos mult_nonneg_nonneg zero_less_mult_pos mult_less_cancel_left
by smt+
moreover
have "φ ≠ pi" "φ ≠ 0"
using ‹¬ is_real z› polar cis_pi
by force+
hence "sin φ > 0 ⟷ φ > 0" "φ < 0 ⟷ sin φ < 0"
using ‹φ = Arg z› ‹φ ≠ 0› ‹φ ≠ pi›
using Arg_bounded[of z]
by (smt sin_gt_zero sin_le_zero sin_pi_minus sin_0_iff_canon sin_ge_zero)+
ultimately
show ?thesis
using ‹φ = Arg z›
by auto
qed

subsubsection ‹Complex square root›

definition
"ccsqrt z = rcis (sqrt (cmod z)) (Arg z / 2)"

lemma square_ccsqrt [simp]:
shows "(ccsqrt x)⇧2 = x"
unfolding ccsqrt_def
by (subst DeMoivre2) (simp add: rcis_cmod_Arg)

lemma ex_complex_sqrt:
shows "∃ s::complex. s*s = z"
unfolding power2_eq_square[symmetric]
by (rule_tac x="csqrt z" in exI) simp

lemma ccsqrt:
assumes "s * s = z"
shows "s = ccsqrt z ∨ s = -ccsqrt z"
proof (cases "s = 0")
case True
thus ?thesis
using assms
unfolding ccsqrt_def
by simp
next
case False
then obtain k::int where "cmod s * cmod s = cmod z" "2 * Arg s - Arg z = 2*k*pi"
using assms
using rcis_cmod_Arg[of z] rcis_cmod_Arg[of s]
using arg_mult[of s s]
using canon_ang(3)[of "2*Arg s"]
by (auto simp add: norm_mult arg_mult)
have *: "sqrt (cmod z) = cmod s"
using ‹cmod s * cmod s = cmod z›
by (smt norm_not_less_zero real_sqrt_abs2)

have **: "Arg z / 2 = Arg s - k*pi"
using ‹2 * Arg s - Arg z = 2*k*pi›
by simp

have "cis (Arg s - k*pi) = cis (Arg s) ∨ cis (Arg s - k*pi) = -cis (Arg s)"
proof (cases "even k")
case True
hence "cis (Arg s - k*pi) = cis (Arg s)"
by (simp add: cis_def complex.corec cos_diff sin_diff)
thus ?thesis
by simp
next
case False
hence "cis (Arg s - k*pi) = -cis (Arg s)"
by (simp add: cis_def complex.corec Complex_eq cos_diff sin_diff)
thus ?thesis
by simp
qed
thus ?thesis
proof
assume ***: "cis (Arg s - k * pi) = cis (Arg s)"
hence "s = ccsqrt z"
using rcis_cmod_Arg[of s]
unfolding ccsqrt_def rcis_def
by (subst *, subst **, subst ***, simp)
thus ?thesis
by simp
next
assume ***: "cis (Arg s - k * pi) = -cis (Arg s)"
hence "s = - ccsqrt z"
using rcis_cmod_Arg[of s]
unfolding ccsqrt_def rcis_def
by (subst *, subst **, subst ***, simp)
thus ?thesis
by simp
qed
qed

lemma null_ccsqrt [simp]:
shows "ccsqrt x = 0 ⟷ x = 0"
unfolding ccsqrt_def
by auto

lemma ccsqrt_mult:
shows "ccsqrt (a * b) = ccsqrt a * ccsqrt b ∨
ccsqrt (a * b) = - ccsqrt a * ccsqrt b"
proof (cases "a = 0 ∨ b = 0")
case True
thus ?thesis
by auto
next
case False
obtain k::int where "Arg a + Arg b - ⇂Arg a + Arg b⇃ = 2 * real_of_int k * pi"
using canon_ang(3)[of "Arg a + Arg b"]
by auto
hence *: "⇂Arg a + Arg b⇃ = Arg a + Arg b - 2 * (real_of_int k) * pi"

have "cis (⇂Arg a + Arg b⇃ / 2) = cis (Arg a / 2 + Arg b / 2) ∨ cis (⇂Arg a + Arg b⇃ / 2) = - cis (Arg a / 2 + Arg b / 2)"
using cos_even_kpi[of k] cos_odd_kpi[of k]
by ((subst *)+, (subst diff_divide_distrib)+, (subst add_divide_distrib)+)
(cases "even k", auto simp add: cis_def complex.corec Complex_eq cos_diff sin_diff)
thus ?thesis
using False
unfolding ccsqrt_def
by (smt (verit, best) arg_mult mult_minus_left mult_minus_right no_zero_divisors norm_mult rcis_def rcis_mult real_sqrt_mult)
qed

lemma csqrt_real:
assumes "is_real x"
shows "(Re x ≥ 0 ∧ ccsqrt x = cor (sqrt (Re x))) ∨
(Re x < 0 ∧ ccsqrt x = 𝗂 * cor (sqrt (- (Re x))))"
proof (cases "x = 0")
case True
thus ?thesis
by auto
next
case False
show ?thesis
proof (cases "Re x > 0")
case True
hence "Arg x = 0"
using ‹is_real x›
by (metis arg_complex_of_real_positive complex_of_real_Re)
thus ?thesis
using ‹Re x > 0› ‹is_real x›
unfolding ccsqrt_def
next
case False
hence "Re x < 0"
using ‹x ≠ 0› ‹is_real x›
using complex_eq_if_Re_eq by auto
hence "Arg x = pi"
using ‹is_real x›
by (metis arg_complex_of_real_negative complex_of_real_Re)
thus ?thesis
using ‹Re x < 0› ‹is_real x›
unfolding ccsqrt_def rcis_def
by (simp add: cis_def complex.corec Complex_eq cmod_eq_Re)
qed
qed

text ‹Rotation of complex vector to x-axis.›

lemma is_real_rot_to_x_axis:
assumes "z ≠ 0"
shows "is_real (cis (-Arg z) * z)"
proof (cases "Arg z = pi")
case True
thus ?thesis
using is_real_arg1[of z]
by auto
next
case False
hence "⇂- Arg z⇃ = - Arg z"
using canon_ang_eqI[of "- Arg z" "-Arg z"]
using Arg_bounded[of z]
hence "Arg (cis (- (Arg z)) * z) = 0"
using arg_mult[of "cis (- (Arg z))" z] ‹z ≠ 0›
using arg_cis[of "- Arg z"]
by simp
thus ?thesis
using is_real_arg1[of "cis (- Arg z) * z"]
by auto
qed

lemma positive_rot_to_x_axis:
assumes "z ≠ 0"
shows "Re (cis (-Arg z) * z) > 0"
using assms
by (smt Re_complex_of_real cis_rcis_eq mult_cancel_right1 rcis_cmod_Arg rcis_mult rcis_zero_arg zero_less_norm_iff)

text ‹Inequalities involving @{term cmod}.›

lemma cmod_1_plus_mult_le:
shows "cmod (1 + z*w) ≤ sqrt((1 + (cmod z)⇧2) * (1 + (cmod w)⇧2))"
proof-
have "Re ((1+z*w)*(1+cnj z*cnj w)) ≤ Re (1+z*cnj z)* Re (1+w*cnj w)"
proof-
have "Re ((w - cnj z)*cnj(w - cnj z)) ≥ 0"
by (subst complex_mult_cnj_cmod) (simp add: power2_eq_square)
hence "Re (z*w + cnj z * cnj w) ≤ Re (w*cnj w) + Re(z*cnj z)"
thus ?thesis
qed
hence "(cmod (1 + z * w))⇧2 ≤ (1 + (cmod z)⇧2) * (1 + (cmod w)⇧2)"
by (subst cmod_square)+ simp
thus ?thesis
by (metis abs_norm_cancel real_sqrt_abs real_sqrt_le_iff)
qed

lemma cmod_diff_ge:
shows "cmod (b - c) ≥ sqrt (1 + (cmod b)⇧2) - sqrt (1 + (cmod c)⇧2)"
proof-
have "(cmod (b - c))⇧2 + (1/2*Im(b*cnj c - c*cnj b))⇧2 ≥ 0"
by simp
hence "(cmod (b - c))⇧2 ≥ - (1/2*Im(b*cnj c - c*cnj b))⇧2"
by simp
hence "(cmod (b - c))⇧2 ≥ (1/2*Re(b*cnj c + c*cnj b))⇧2 - Re(b*cnj b*c*cnj c) "
by (auto simp add: power2_eq_square field_simps)
hence "Re ((b - c)*(cnj b - cnj c)) ≥ (1/2*Re(b*cnj c + c*cnj b))⇧2 - Re(b*cnj b*c*cnj c)"
by (subst (asm) cmod_square) simp
moreover
have "(1 + (cmod b)⇧2) * (1 + (cmod c)⇧2) = 1 + Re(b*cnj b) + Re(c*cnj c) + Re(b*cnj b*c*cnj c)"
by (subst cmod_square)+ (simp add: field_simps power2_eq_square)
moreover
have "(1 + Re (scalprod b c))⇧2 = 1 + 2*Re(scalprod b c) + ((Re (scalprod b c))⇧2)"
by (subst power2_sum) simp
hence "(1 + Re (scalprod b c))⇧2 = 1 + Re(b*cnj c + c*cnj b) + (1/2 * Re (b*cnj c + c*cnj b))⇧2"
by simp
ultimately
have "(1 + (cmod b)⇧2) * (1 + (cmod c)⇧2) ≥ (1 + Re (scalprod b c))⇧2"
moreover
have "sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2)) ≥ 0"
by (metis one_power2 real_sqrt_sum_squares_mult_ge_zero)
ultimately
have "sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2)) ≥ 1 + Re (scalprod b c)"
by (metis power2_le_imp_le real_sqrt_ge_0_iff real_sqrt_pow2_iff)
hence "Re ((b - c) * (cnj b - cnj c)) ≥ 1 + Re (c*cnj c) + 1 + Re (b*cnj b) - 2*sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2))"
hence *: "(cmod (b - c))⇧2 ≥ (sqrt (1 + (cmod b)⇧2) - sqrt (1 + (cmod c)⇧2))⇧2"
apply (subst cmod_square)+
apply (subst (asm) cmod_square)+
apply (subst power2_diff)
apply (subst real_sqrt_pow2, simp)
apply (subst real_sqrt_pow2, simp)
done
thus ?thesis
proof (cases "sqrt (1 + (cmod b)⇧2) - sqrt (1 + (cmod c)⇧2) > 0")
case True
thus ?thesis
using power2_le_imp_le[OF *]
by simp
next
case False
hence "0 ≥ sqrt (1 + (cmod b)⇧2) - sqrt (1 + (cmod c)⇧2)"
by (metis less_eq_real_def linorder_neqE_linordered_idom)
moreover
have "cmod (b - c) ≥ 0"
by simp
ultimately
show ?thesis
qed
qed

lemma cmod_diff_le:
shows "cmod (b - c) ≤ sqrt (1 + (cmod b)⇧2) + sqrt (1 + (cmod c)⇧2)"
proof-
have "(cmod (b + c))⇧2 + (1/2*Im(b*cnj c - c*cnj b))⇧2 ≥ 0"
by simp
hence "(cmod (b + c))⇧2 ≥ - (1/2*Im(b*cnj c - c*cnj b))⇧2"
by simp
hence "(cmod (b + c))⇧2 ≥ (1/2*Re(b*cnj c + c*cnj b))⇧2 - Re(b*cnj b*c*cnj c) "
by (auto simp add: power2_eq_square field_simps)
hence "Re ((b + c)*(cnj b + cnj c)) ≥ (1/2*Re(b*cnj c + c*cnj b))⇧2 - Re(b*cnj b*c*cnj c)"
by (subst (asm) cmod_square) simp
moreover
have "(1 + (cmod b)⇧2) * (1 + (cmod c)⇧2) = 1 + Re(b*cnj b) + Re(c*cnj c) + Re(b*cnj b*c*cnj c)"
by (subst cmod_square)+ (simp add: field_simps power2_eq_square)
moreover
have ++: "2*Re(scalprod b c) = Re(b*cnj c + c*cnj b)"
by simp
have "(1 - Re (scalprod b c))⇧2 = 1 - 2*Re(scalprod b c) + ((Re (scalprod b c))⇧2)"
by (subst power2_diff) simp
hence "(1 - Re (scalprod b c))⇧2 = 1 - Re(b*cnj c + c*cnj b) + (1/2 * Re (b*cnj c + c*cnj b))⇧2"
by (subst ++[symmetric]) simp
ultimately
have "(1 + (cmod b)⇧2) * (1 + (cmod c)⇧2) ≥ (1 - Re (scalprod b c))⇧2"
moreover
have "sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2)) ≥ 0"
by (metis one_power2 real_sqrt_sum_squares_mult_ge_zero)
ultimately
have "sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2)) ≥ 1 - Re (scalprod b c)"
by (metis power2_le_imp_le real_sqrt_ge_0_iff real_sqrt_pow2_iff)
hence "Re ((b - c) * (cnj b - cnj c)) ≤ 1 + Re (c*cnj c) + 1 + Re (b*cnj b) + 2*sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2))"
hence *: "(cmod (b - c))⇧2 ≤ (sqrt (1 + (cmod b)⇧2) + sqrt (1 + (cmod c)⇧2))⇧2"
apply (subst cmod_square)+
apply (subst (asm) cmod_square)+
apply (subst power2_sum)
apply (subst real_sqrt_pow2, simp)
apply (subst real_sqrt_pow2, simp)
done
thus ?thesis
using power2_le_imp_le[OF *]
by simp
qed

text ‹Definition of Euclidean distance between two complex numbers.›

definition cdist where
[simp]: "cdist z1 z2 ≡ cmod (z2 - z1)"

text ‹Misc. properties of complex numbers.›

lemma ex_complex_to_complex [simp]:
fixes z1 z2 :: complex
assumes "z1 ≠ 0" and "z2 ≠ 0"
shows "∃k. k ≠ 0 ∧ z2 = k * z1"
using assms
by (rule_tac x="z2/z1" in exI) simp

lemma ex_complex_to_one [simp]:
fixes z::complex
assumes "z ≠ 0"
shows "∃k. k ≠ 0 ∧ k * z = 1"
using assms
by (rule_tac x="1/z" in exI) simp

lemma ex_complex_to_complex2 [simp]:
fixes z::complex
shows "∃k. k ≠ 0 ∧ k * z = z"
by (rule_tac x="1" in exI) simp

lemma complex_sqrt_1:
fixes z::complex
assumes "z ≠ 0"
shows "z = 1 / z ⟷ z = 1 ∨ z = -1"
using assms
using nonzero_eq_divide_eq square_eq_iff
by fastforce

end