Theory Complex_Geometry.Canonical_Angle

(* -------------------------------------------------------------------------- *)
subsection ‹Canonical angle› 
(* -------------------------------------------------------------------------- *)

text ‹Canonize any angle to $(-\pi, \pi]$ (taking account of $2\pi$ periodicity of @{term sin} and
@{term cos}). With this function, for example, multiplicative properties of @{term arg} for complex
numbers can easily be expressed and proved.›

theory Canonical_Angle
imports More_Transcendental
begin


abbreviation canon_ang_P where
 "canon_ang_P α α' ≡ (-pi < α' ∧ α' ≤ pi) ∧ (∃ k::int. α - α' = 2*k*pi)"

definition canon_ang :: "real ⇒ real" ("⇂_⇃") where
  "⇂α⇃ = (THE α'. canon_ang_P α α')"

text ‹There is a canonical angle for every angle.›
lemma canon_ang_ex:
  shows "∃ α'. canon_ang_P α α'"
proof-
  have ***: "∀ α::real. ∃ α'. 0 < α' ∧ α' ≤ 1 ∧ (∃ k::int. α' = α - k)"
  proof
    fix α::real
    show "∃α'>0. α' ≤ 1 ∧ (∃k::int. α' = α - k)"
    proof (cases "α = floor α")
      case True
      thus ?thesis
        by (rule_tac x="α - floor α + 1" in exI, auto) (rule_tac x="floor α - 1" in exI, auto)
    next
      case False
      thus ?thesis
        using real_of_int_floor_ge_diff_one[of "α"]
        using of_int_floor_le[of "α"]
        by (rule_tac x="α - floor α" in exI) smt
    qed
  qed

  have **: "∀ α::real. ∃ α'. 0 < α' ∧ α' ≤ 2 ∧ (∃ k::int. α - α' = 2*k - 1)"
  proof
    fix α::real
    from ***[rule_format, of "(α + 1) /2"]
    obtain α' and k::int where "0 < α'" "α' ≤ 1" "α' = (α + 1)/2 - k"
      by force
    hence "0 < α'" "α' ≤ 1" "α' = α/2 - k + 1/2"
      by auto
    thus "∃α'>0. α' ≤ 2 ∧ (∃k::int. α - α' = real_of_int (2 * k - 1))"
      by (rule_tac x="2*α'" in exI) auto
  qed
  have *: "∀ α::real. ∃ α'. -1 < α' ∧ α' ≤ 1 ∧ (∃ k::int. α - α' = 2*k)"
  proof
    fix α::real
    from ** obtain α' and k :: int where
      "0 < α' ∧ α' ≤ 2 ∧ α - α' = 2*k - 1"
      by force
    thus "∃α'>-1. α' ≤ 1 ∧ (∃k. α - α' = real_of_int (2 * (k::int)))"
      by (rule_tac x="α' - 1" in exI) (auto simp add: field_simps)
  qed
  obtain α' k where 1: "α' >- 1 ∧ α' ≤ 1" and 2: "α / pi - α' = real_of_int (2 * k)"
    using *[rule_format, of "α / pi"]
    by auto
  have "α'*pi > -pi ∧ α'*pi ≤ pi" 
    using 1
    by (smt mult.commute mult_le_cancel_left1 mult_minus_right pi_gt_zero)
  moreover
  have "α - α'*pi = 2 * real_of_int k * pi"
    using 2
    by (auto simp add: field_simps)
  ultimately
  show ?thesis
    by auto
qed

text ‹Canonical angle of any angle is unique.›
lemma canon_ang_unique:
  assumes "canon_ang_P α α⇩1" and "canon_ang_P α α⇩2"
  shows "α⇩1 = α⇩2"
proof-
  obtain k1::int where "α - α⇩1 = 2*k1*pi"
    using assms(1)
    by auto
  obtain k2::int where "α - α⇩2 = 2*k2*pi"
    using assms(2)
    by auto
  hence *: "-α⇩1 + α⇩2 = 2*(k1 - k2)*pi"
    using ‹α - α⇩1 = 2*k1*pi›
    by (simp add:field_simps)
  moreover
  have "-α⇩1 + α⇩2 < 2 * pi" "-α⇩1 + α⇩2 > -2*pi"
    using assms
    by auto
  ultimately
  have "-α⇩1 + α⇩2 = 0"
    using mult_less_cancel_right[of "-2" pi "real_of_int(2 * (k1 - k2))"]
    by auto
  thus ?thesis
    by auto
qed

text ‹Canonical angle is always in $(-\pi, \pi]$ and differs from the starting angle by $2k\pi$.›
lemma canon_ang:
  shows "-pi < ⇂α⇃" and "⇂α⇃ ≤ pi" and "∃ k::int. α - ⇂α⇃ = 2*k*pi"
proof-
  obtain α' where "canon_ang_P α α'"
    using canon_ang_ex[of α]
    by auto
  have "canon_ang_P α ⇂α⇃"
    unfolding canon_ang_def
  proof (rule theI[where a="α'"])
    show "canon_ang_P α α'"
      by fact
  next
    fix α''
    assume "canon_ang_P α α''"
    thus "α'' = α'"
      using ‹canon_ang_P α α'›
      using canon_ang_unique[of α' α α'']
      by simp
  qed
  thus "-pi < ⇂α⇃" "⇂α⇃ ≤ pi" "∃ k::int. α - ⇂α⇃ = 2*k*pi"
    by auto
qed

text ‹Angles in $(-\pi, \pi]$ are already canonical.›
lemma canon_ang_id:
  assumes  "-pi < α ∧ α ≤ pi"
  shows "⇂α⇃ = α"
  using assms
  using canon_ang_unique[of "canon_ang α" α α] canon_ang[of α]
  by auto

text ‹Angles that differ by $2k\pi$ have equal canonical angles.›
lemma canon_ang_eq:
  assumes "∃ k::int. α⇩1 - α⇩2 = 2*k*pi"
  shows "⇂α⇩1⇃ = ⇂α⇩2⇃"
proof-
  obtain k'::int where *: "- pi < ⇂α⇩1⇃" "⇂α⇩1⇃ ≤ pi" "α⇩1 - ⇂α⇩1⇃ = 2 * k' * pi"
    using canon_ang[of α⇩1]
    by auto

  obtain k''::int where **: "- pi < ⇂α⇩2⇃" "⇂α⇩2⇃ ≤ pi" "α⇩2 - ⇂α⇩2⇃ = 2 * k'' * pi"
    using canon_ang[of α⇩2]
    by auto

  obtain k::int where ***: "α⇩1 - α⇩2 = 2*k*pi"
    using assms
    by auto

  have "∃m::int. α⇩1 - ⇂α⇩2⇃ = 2 * m * pi"
    using **(3) ***
    by (rule_tac x="k+k''" in exI) (auto simp add: field_simps)

  thus ?thesis
    using canon_ang_unique[of "⇂α⇩1⇃" α⇩1 "⇂α⇩2⇃"] * **
    by auto
qed

text ‹Introduction and elimination rules›
lemma canon_ang_eqI:
  assumes "∃k::int. α' - α = 2 * k * pi" and "- pi < α' ∧ α' ≤ pi"
  shows "⇂α⇃ = α'"
  using assms
  using canon_ang_eq[of α' α]
  using canon_ang_id[of α']
  by auto

lemma canon_ang_eqE:
  assumes "⇂α⇩1⇃ = ⇂α⇩2⇃"
  shows "∃ (k::int). α⇩1 - α⇩2 = 2 *k * pi"
proof-
  obtain k1 k2 :: int where
    "α⇩1 - ⇂α⇩1⇃ = 2 * k1 * pi"
    "α⇩2 - ⇂α⇩2⇃ = 2 * k2 * pi"
    using canon_ang[of α⇩1] canon_ang[of α⇩2]
    by auto
  thus ?thesis
    using assms
    by (rule_tac x="k1 - k2" in exI) (auto simp add: field_simps)
qed

text ‹Canonical angle of opposite angle›

lemma canon_ang_uminus:
  assumes "⇂α⇃ ≠ pi"
  shows "⇂-α⇃ = -⇂α⇃"
proof (rule canon_ang_eqI)
  show "∃x::int. - ⇂α⇃ - - α = 2 * x * pi"
    using canon_ang(3)[of α]
    by (metis minus_diff_eq minus_diff_minus)
next
  show "- pi < - ⇂α⇃ ∧ - ⇂α⇃ ≤ pi"
    using canon_ang(1)[of α] canon_ang(2)[of α] assms
    by auto
qed

lemma canon_ang_uminus_pi:
  assumes "⇂α⇃ = pi"
  shows "⇂-α⇃ = ⇂α⇃"
proof (rule canon_ang_eqI)
  obtain k::int where "α - ⇂α⇃ = 2 * k * pi"
    using canon_ang(3)[of α]
    by auto
  thus "∃x::int. ⇂α⇃ - - α = 2 * x * pi"
    using assms
    by (rule_tac x="k+(1::int)" in exI) (auto simp add: field_simps)
next
  show "- pi < ⇂α⇃ ∧ ⇂α⇃ ≤ pi"
    using assms
    by auto
qed

text ‹Canonical angle of difference of two angles›
lemma canon_ang_diff:
  shows "⇂α - β⇃ = ⇂⇂α⇃ - ⇂β⇃⇃"
proof (rule canon_ang_eq)
  show "∃x::int. α - β - (⇂α⇃ - ⇂β⇃) = 2 * x * pi"
  proof-
    obtain k1::int where "α - ⇂α⇃ = 2*k1*pi"
      using canon_ang(3)
      by auto
    moreover
    obtain k2::int where "β - ⇂β⇃ = 2*k2*pi"
      using canon_ang(3)
      by auto
    ultimately
    show ?thesis
      by (rule_tac x="k1 - k2" in exI) (auto simp add: field_simps)
  qed
qed

text ‹Canonical angle of sum of two angles›
lemma canon_ang_sum:
  shows "⇂α + β⇃ = ⇂⇂α⇃ + ⇂β⇃⇃"
proof (rule canon_ang_eq)
  show "∃x::int. α + β - (⇂α⇃ + ⇂β⇃) = 2 * x * pi"
  proof-
    obtain k1::int where "α - ⇂α⇃ = 2*k1*pi"
      using canon_ang(3)
      by auto
    moreover
    obtain k2::int where "β - ⇂β⇃ = 2*k2*pi"
      using canon_ang(3)
      by auto
    ultimately
    show ?thesis
      by (rule_tac x="k1 + k2" in exI) (auto simp add: field_simps)
  qed
qed

text ‹Canonical angle of angle from $(0, 2\pi]$ shifted by $\pi$›

lemma canon_ang_plus_pi1:
  assumes "0 < α" and "α ≤ 2*pi"
  shows "⇂α + pi⇃ = α - pi"
proof (rule canon_ang_eqI)
  show "∃ x::int. α - pi - (α + pi) = 2 * x * pi"
    by (rule_tac x="-1" in exI) auto
next
  show "- pi < α - pi ∧ α - pi ≤ pi"
    using assms
    by auto
qed

lemma canon_ang_minus_pi1:
  assumes "0 < α" and "α ≤ 2*pi"
  shows "⇂α - pi⇃ = α - pi"
proof (rule canon_ang_id)
  show "- pi < α - pi ∧ α - pi ≤ pi"
    using assms
    by auto
qed

text ‹Canonical angle of angles from $(-2\pi, 0]$ shifted by $\pi$›

lemma canon_ang_plus_pi2:
  assumes "-2*pi < α" and "α ≤ 0"
  shows "⇂α + pi⇃ = α + pi"
proof (rule canon_ang_id)
  show "- pi < α + pi ∧ α + pi ≤ pi"
    using assms
    by auto
qed

lemma canon_ang_minus_pi2:
  assumes "-2*pi < α" and "α ≤ 0"
  shows "⇂α - pi⇃ = α + pi"
proof (rule canon_ang_eqI)
  show "∃ x::int. α + pi - (α - pi) = 2 * x * pi"
    by (rule_tac x="1" in exI) auto
next
  show "- pi < α + pi ∧ α + pi ≤ pi"
    using assms
    by auto
qed

text ‹Canonical angle of angle in $(\pi, 3\pi]$.›
lemma canon_ang_pi_3pi: 
  assumes "pi < α" and "α ≤ 3 * pi"
  shows "⇂α⇃ = α - 2*pi"
proof-
  have "∃x. - pi = pi * real_of_int x"
    by (rule_tac x="-1" in exI, simp)
  thus ?thesis
    using assms canon_ang_eqI[of "α - 2*pi" "α"]
    by auto
qed

text ‹Canonical angle of angle in $(-3\pi, -\pi]$.›
lemma canon_ang_minus_3pi_minus_pi: 
  assumes "-3*pi < α" and "α ≤ -pi"
  shows "⇂α⇃ = α + 2*pi"
proof-
  have "∃x. pi = pi * real_of_int x"
    by (rule_tac x="1" in exI, simp)
  thus ?thesis
    using assms canon_ang_eqI[of "α + 2*pi" "α"]
    by auto
qed

text ‹Canonical angles for some special angles›

lemma zero_canonical [simp]:
  shows "⇂0⇃ = 0"
  using canon_ang_eqI[of 0 0]
  by simp

lemma pi_canonical [simp]:
  shows "⇂pi⇃ = pi"
  by (simp add: canon_ang_id)

lemma two_pi_canonical [simp]:
  shows "⇂2 * pi⇃ = 0"
  using canon_ang_plus_pi1[of "pi"]
  by simp

text ‹Canonization preserves sine and cosine›
lemma canon_ang_sin [simp]:
  shows "sin ⇂α⇃ = sin α"
proof-
  obtain x::int where "α = ⇂α⇃ + pi * (x * 2)"
    using canon_ang(3)[of α]
    by (auto simp add: field_simps)
  thus ?thesis
    using sin_periodic_int[of "⇂α⇃" x]
    by (simp add: field_simps)
qed

lemma canon_ang_cos [simp]:
  shows "cos ⇂α⇃ = cos α"
proof-
  obtain x::int where "α = ⇂α⇃ + pi * (x * 2)"
    using canon_ang(3)[of α]
    by (auto simp add: field_simps)
  thus ?thesis
    using cos_periodic_int[of "⇂α⇃" x]
    by (simp add: field_simps)
qed

end