Theory Poincare_Lines_Axis_Intersections
theory Poincare_Lines_Axis_Intersections
imports Poincare_Between
begin
section‹Intersection of h-lines with the x-axis in the Poincar\'e model›
subsection‹Betweeness of x-axis intersection›
text‹The intersection point of the h-line determined by points $u$ and $v$ and the x-axis is between
$u$ and $v$, then $u$ and $v$ are in the opposite half-planes (one must be in the upper, and the
other one in the lower half-plane).›
lemma poincare_between_x_axis_intersection:
assumes "u ∈ unit_disc" and "v ∈ unit_disc" and "z ∈ unit_disc" and "u ≠ v"
assumes "u ∉ circline_set x_axis" and "v ∉ circline_set x_axis"
assumes "z ∈ circline_set (poincare_line u v) ∩ circline_set x_axis"
shows "poincare_between u z v ⟷ Arg (to_complex u) * Arg (to_complex v) < 0"
proof-
have "∀ u v. u ∈ unit_disc ∧ v ∈ unit_disc ∧ u ≠ v ∧
u ∉ circline_set x_axis ∧ v ∉ circline_set x_axis ∧
z ∈ circline_set (poincare_line u v) ∩ circline_set x_axis ⟶
(poincare_between u z v ⟷ Arg (to_complex u) * Arg (to_complex v) < 0)" (is "?P z")
proof (rule wlog_real_zero)
show "?P 0⇩h"
proof ((rule allI)+, rule impI, (erule conjE)+)
fix u v
assume *: "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
"u ∉ circline_set x_axis" "v ∉ circline_set x_axis"
"0⇩h ∈ circline_set (poincare_line u v) ∩ circline_set x_axis"
obtain u' v' where uv: "u = of_complex u'" "v = of_complex v'"
using * inf_or_of_complex[of u] inf_or_of_complex[of v]
by auto
hence "u ≠ 0⇩h" "v ≠ 0⇩h" "u' ≠ 0" "v' ≠ 0"
using *
by auto
hence "Arg u' ≠ 0" "Arg v' ≠ 0"
using * arg_0_iff[of u'] arg_0_iff[of v']
unfolding circline_set_x_axis uv
by auto
have "poincare_collinear {0⇩h, u, v}"
using *
unfolding poincare_collinear_def
by (rule_tac x="poincare_line u v" in exI, simp)
have "(∃k<0. u' = cor k * v') ⟷ (Arg u' * Arg v' < 0)" (is "?lhs ⟷ ?rhs")
proof
assume "?lhs"
then obtain k where "k < 0" "u' = cor k * v'"
by auto
thus ?rhs
using arg_mult_real_negative[of k v'] arg_uminus_opposite_sign[of v']
using ‹u' ≠ 0› ‹v' ≠ 0› ‹Arg u' ≠ 0› ‹Arg v' ≠ 0›
by (auto simp add: mult_neg_pos mult_pos_neg)
next
assume ?rhs
obtain ru rv φ where polar: "u' = cor ru * cis φ" "v' = cor rv * cis φ"
using ‹poincare_collinear {0⇩h, u, v}› poincare_collinear_zero_polar_form[of u' v'] uv * ‹u' ≠ 0› ‹v' ≠ 0›
by auto
have "ru * rv < 0"
using polar ‹?rhs› ‹u' ≠ 0› ‹v' ≠ 0›
using arg_mult_real_negative[of "ru" "cis φ"] arg_mult_real_positive[of "ru" "cis φ"]
using arg_mult_real_negative[of "rv" "cis φ"] arg_mult_real_positive[of "rv" "cis φ"]
apply (cases "ru > 0")
apply (cases "rv > 0", simp, simp add: mult_pos_neg)
apply (cases "rv > 0", simp add: mult_neg_pos, simp)
done
thus "?lhs"
using polar
by (rule_tac x="ru / rv" in exI, auto simp add: divide_less_0_iff mult_less_0_iff)
qed
thus "poincare_between u 0⇩h v = (Arg (to_complex u) * Arg (to_complex v) < 0)"
using poincare_between_u0v[of u v] * ‹u ≠ 0⇩h› ‹v ≠ 0⇩h› uv
by simp
qed
next
fix a z
assume 1: "is_real a" "cmod a < 1" "z ∈ unit_disc"
assume 2: "?P (moebius_pt (blaschke a) z)"
show "?P z"
proof ((rule allI)+, rule impI, (erule conjE)+)
fix u v
let ?M = "moebius_pt (blaschke a)"
let ?Mu = "?M u"
let ?Mv = "?M v"
assume *: "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v" "u ∉ circline_set x_axis" "v ∉ circline_set x_axis"
hence "u ≠ ∞⇩h" "v ≠ ∞⇩h"
by auto
have **: "⋀ x y :: real. x * y < 0 ⟷ sgn (x * y) < 0"
by simp
assume "z ∈ circline_set (poincare_line u v) ∩ circline_set x_axis"
thus "poincare_between u z v = (Arg (to_complex u) * Arg (to_complex v) < 0)"
using * 1 2[rule_format, of ?Mu ?Mv] ‹cmod a < 1› ‹is_real a› blaschke_unit_disc_fix[of a]
using inversion_noteq_unit_disc[of "of_complex a" u] ‹u ≠ ∞⇩h›
using inversion_noteq_unit_disc[of "of_complex a" v] ‹v ≠ ∞⇩h›
apply auto
apply (subst (asm) **, subst **, subst (asm) sgn_mult, subst sgn_mult, simp)
apply (subst (asm) **, subst (asm) **, subst (asm) sgn_mult, subst (asm) sgn_mult, simp)
done
qed
next
show "z ∈ unit_disc" by fact
next
show "is_real (to_complex z)"
using assms inf_or_of_complex[of z]
by (auto simp add: circline_set_x_axis)
qed
thus ?thesis
using assms
by simp
qed
subsection‹Check if an h-line intersects the x-axis›
lemma x_axis_intersection_equation:
assumes
"H = mk_circline A B C D" and
"(A, B, C, D) ∈ hermitean_nonzero"
shows "of_complex z ∈ circline_set x_axis ∩ circline_set H ⟷
A*z⇧2 + 2*Re B*z + D = 0 ∧ is_real z" (is "?lhs ⟷ ?rhs")
proof-
have "?lhs ⟷ A*z⇧2 + (B + cnj B)*z + D = 0 ∧ z = cnj z"
using assms
using circline_equation_x_axis[of z]
using circline_equation[of H A B C D z]
using hermitean_elems
by (auto simp add: power2_eq_square field_simps)
thus ?thesis
using eq_cnj_iff_real[of z]
using hermitean_elems[of A B C D]
by (simp add: complex_add_cnj complex_eq_if_Re_eq)
qed
text ‹Check if an h-line intersects x-axis within the unit disc - this could be generalized to
checking if an arbitrary circline intersects the x-axis, but we do not need that.›
definition intersects_x_axis_cmat :: "complex_mat ⇒ bool" where
[simp]: "intersects_x_axis_cmat H = (let (A, B, C, D) = H in A = 0 ∨ (Re B)⇧2 > (Re A)⇧2)"
lift_definition intersects_x_axis_clmat :: "circline_mat ⇒ bool" is intersects_x_axis_cmat
done
lift_definition intersects_x_axis :: "circline ⇒ bool" is intersects_x_axis_clmat
proof (transfer)
fix H1 H2
assume hh: "hermitean H1 ∧ H1 ≠ mat_zero" and "hermitean H2 ∧ H2 ≠ mat_zero"
obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
by (cases H1, cases H2, auto)
assume "circline_eq_cmat H1 H2"
then obtain k where k: "k ≠ 0 ∧ H2 = cor k *⇩s⇩m H1"
by auto
show "intersects_x_axis_cmat H1 = intersects_x_axis_cmat H2"
proof-
have "k ≠ 0 ⟹ (Re A1)⇧2 < (Re B1)⇧2 ⟷ (k * Re A1)⇧2 < (k * Re B1)⇧2"
by (smt mult_strict_left_mono power2_eq_square semiring_normalization_rules(13) zero_less_power2)
thus ?thesis
using * k
by auto
qed
qed
lemma intersects_x_axis_mk_circline:
assumes "is_real A" and "A ≠ 0 ∨ B ≠ 0"
shows "intersects_x_axis (mk_circline A B (cnj B) A) ⟷ A = 0 ∨ (Re B)⇧2 > (Re A)⇧2"
proof-
let ?H = "(A, B, (cnj B), A)"
have "hermitean ?H"
using ‹is_real A›
unfolding hermitean_def mat_adj_def mat_cnj_def
using eq_cnj_iff_real
by auto
moreover
have "?H ≠ mat_zero"
using assms
by auto
ultimately
show ?thesis
by (transfer, transfer, auto simp add: Let_def)
qed
lemma intersects_x_axis_iff:
assumes "is_poincare_line H"
shows "(∃ x ∈ unit_disc. x ∈ circline_set H ∩ circline_set x_axis) ⟷ intersects_x_axis H"
proof-
obtain Ac B C Dc where *: "H = mk_circline Ac B C Dc" "hermitean (Ac, B, C, Dc)" "(Ac, B, C, Dc) ≠ mat_zero"
using ex_mk_circline[of H]
by auto
hence "(cmod B)⇧2 > (cmod Ac)⇧2" "Ac = Dc"
using assms
using is_poincare_line_mk_circline
by auto
hence "H = mk_circline (Re Ac) B (cnj B) (Re Ac)" "hermitean (cor (Re Ac), B, (cnj B), cor (Re Ac))" "(cor (Re Ac), B, (cnj B), cor (Re Ac)) ≠ mat_zero"
using hermitean_elems[of Ac B C Dc] *
by auto
then obtain A where
*: "H = mk_circline (cor A) B (cnj B) (cor A)" "(cor A, B, (cnj B), cor A) ∈ hermitean_nonzero"
by auto
show ?thesis
proof (cases "A = 0")
case True
thus ?thesis
using *
using x_axis_intersection_equation[OF *(1-2), of 0]
using intersects_x_axis_mk_circline[of "cor A" B]
by auto
next
case False
show ?thesis
proof
assume "∃ x ∈ unit_disc. x ∈ circline_set H ∩ circline_set x_axis"
then obtain x where **: "of_complex x ∈ unit_disc" "of_complex x ∈ circline_set H ∩ circline_set x_axis"
by (metis inf_or_of_complex inf_notin_unit_disc)
hence "is_real x"
unfolding circline_set_x_axis
using of_complex_inj
by auto
hence eq: "A * (Re x)⇧2 + 2 * Re B * Re x + A = 0"
using **
using x_axis_intersection_equation[OF *(1-2), of "Re x"]
by simp
hence "(2 * Re B)⇧2 - 4 * A * A ≥ 0"
using discriminant_iff[of A _ "2 * Re B" A]
using discrim_def[of A "2 * Re B" A] False
by auto
hence "(Re B)⇧2 ≥ (Re A)⇧2"
by (simp add: power2_eq_square)
moreover
have "(Re B)⇧2 ≠ (Re A)⇧2"
proof (rule ccontr)
assume "¬ ?thesis"
hence "Re B = Re A ∨ Re B = - Re A"
using power2_eq_iff by blast
hence "A * (Re x)⇧2 + A * 2* Re x + A = 0 ∨ A * (Re x)⇧2 - A * 2 * Re x + A = 0"
using eq
by auto
hence "A * ((Re x)⇧2 + 2* Re x + 1) = 0 ∨ A * ((Re x)⇧2 - 2 * Re x + 1) = 0"
by (simp add: field_simps)
hence "(Re x)⇧2 + 2 * Re x + 1 = 0 ∨ (Re x)⇧2 - 2 * Re x + 1 = 0"
using ‹A ≠ 0›
by simp
hence "(Re x + 1)⇧2 = 0 ∨ (Re x - 1)⇧2 = 0"
by (simp add: power2_sum power2_diff field_simps)
hence "Re x = -1 ∨ Re x = 1"
by auto
thus False
using ‹is_real x› ‹of_complex x ∈ unit_disc›
by (auto simp add: cmod_eq_Re)
qed
ultimately
show "intersects_x_axis H"
using intersects_x_axis_mk_circline
using *
by auto
next
assume "intersects_x_axis H"
hence "(Re B)⇧2 > (Re A)⇧2"
using * False
using intersects_x_axis_mk_circline
by simp
hence discr: "(2 * Re B)⇧2 - 4 * A * A > 0"
by (simp add: power2_eq_square)
then obtain x1 x2 where
eqs: "A * x1⇧2 + 2 * Re B * x1 + A = 0" "A * x2⇧2 + 2 * Re B * x2 + A = 0" "x1 ≠ x2"
using discriminant_pos_ex[OF ‹A ≠ 0›, of "2 * Re B" A]
using discrim_def[of A "2 * Re B" A]
by auto
hence "x1 * x2 = 1"
using viette2[OF ‹A ≠ 0›, of "2 * Re B" A x1 x2] discr ‹A ≠ 0›
by auto
have "abs x1 ≠ 1" "abs x2 ≠ 1"
using eqs discr ‹x1 * x2 = 1›
by (auto simp add: abs_if power2_eq_square)
hence "abs x1 < 1 ∨ abs x2 < 1"
using ‹x1 * x2 = 1›
by (smt mult_le_cancel_left1 mult_minus_right)
thus "∃x ∈ unit_disc. x ∈ circline_set H ∩ circline_set x_axis"
using x_axis_intersection_equation[OF *(1-2), of x1]
using x_axis_intersection_equation[OF *(1-2), of x2]
using eqs
by auto
qed
qed
qed
subsection‹Check if a Poincar\'e line intersects the y-axis›
definition intersects_y_axis_cmat :: "complex_mat ⇒ bool" where
[simp]: "intersects_y_axis_cmat H = (let (A, B, C, D) = H in A = 0 ∨ (Im B)⇧2 > (Re A)⇧2)"
lift_definition intersects_y_axis_clmat :: "circline_mat ⇒ bool" is intersects_y_axis_cmat
done
lift_definition intersects_y_axis :: "circline ⇒ bool" is intersects_y_axis_clmat
proof (transfer)
fix H1 H2
assume hh: "hermitean H1 ∧ H1 ≠ mat_zero" and "hermitean H2 ∧ H2 ≠ mat_zero"
obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
by (cases H1, cases H2, auto)
assume "circline_eq_cmat H1 H2"
then obtain k where k: "k ≠ 0 ∧ H2 = cor k *⇩s⇩m H1"
by auto
show "intersects_y_axis_cmat H1 = intersects_y_axis_cmat H2"
proof-
have "k ≠ 0 ⟹ (Re A1)⇧2 < (Im B1)⇧2 ⟷ (k * Re A1)⇧2 < (k * Im B1)⇧2"
by (smt mult_strict_left_mono power2_eq_square semiring_normalization_rules(13) zero_less_power2)
thus ?thesis
using * k
by auto
qed
qed
lemma intersects_x_axis_intersects_y_axis [simp]:
shows "intersects_x_axis (moebius_circline (moebius_rotation (pi/2)) H) ⟷ intersects_y_axis H"
unfolding moebius_rotation_def moebius_similarity_def
by simp (transfer, transfer, auto simp add: mat_adj_def mat_cnj_def)
lemma intersects_y_axis_iff:
assumes "is_poincare_line H"
shows "(∃ y ∈ unit_disc. y ∈ circline_set H ∩ circline_set y_axis) ⟷ intersects_y_axis H" (is "?lhs ⟷ ?rhs")
proof-
let ?R = "moebius_rotation (pi / 2)"
let ?H' = "moebius_circline ?R H"
have 1: "is_poincare_line ?H'"
using assms
using unit_circle_fix_preserve_is_poincare_line[OF _ assms, of ?R]
by simp
show ?thesis
proof
assume "?lhs"
then obtain y where "y ∈ unit_disc" "y ∈ circline_set H ∩ circline_set y_axis"
by auto
hence "moebius_pt ?R y ∈ unit_disc ∧ moebius_pt ?R y ∈ circline_set ?H' ∩ circline_set x_axis"
using rotation_pi_2_y_axis
by (metis Int_iff circline_set_moebius_circline_E moebius_circline_comp_inv_left moebius_pt_comp_inv_left unit_disc_fix_discI unit_disc_fix_rotation)
thus ?rhs
using intersects_x_axis_iff[OF 1]
using intersects_x_axis_intersects_y_axis[of H]
by auto
next
assume "intersects_y_axis H"
hence "intersects_x_axis ?H'"
using intersects_x_axis_intersects_y_axis[of H]
by simp
then obtain x where *: "x ∈ unit_disc" "x ∈ circline_set ?H' ∩ circline_set x_axis"
using intersects_x_axis_iff[OF 1]
by auto
let ?y = "moebius_pt (-?R) x"
have "?y ∈ unit_disc ∧ ?y ∈ circline_set H ∩ circline_set y_axis"
using * rotation_pi_2_y_axis[symmetric]
by (metis Int_iff circline_set_moebius_circline_E moebius_pt_comp_inv_left moebius_rotation_uminus uminus_moebius_def unit_disc_fix_discI unit_disc_fix_rotation)
thus ?lhs
by auto
qed
qed
subsection‹Intersection point of a Poincar\'e line with the x-axis in the unit disc›
definition calc_x_axis_intersection_cvec :: "complex ⇒ complex ⇒ complex_vec" where
[simp]: "calc_x_axis_intersection_cvec A B =
(let discr = (Re B)⇧2 - (Re A)⇧2 in
(-Re(B) + sgn (Re B) * sqrt(discr), A))"
definition calc_x_axis_intersection_cmat_cvec :: "complex_mat ⇒ complex_vec" where [simp]:
"calc_x_axis_intersection_cmat_cvec H =
(let (A, B, C, D) = H in
if A ≠ 0 then
calc_x_axis_intersection_cvec A B
else
(0, 1)
)"
lift_definition calc_x_axis_intersection_clmat_hcoords :: "circline_mat ⇒ complex_homo_coords" is calc_x_axis_intersection_cmat_cvec
by (auto split: if_split_asm)
lift_definition calc_x_axis_intersection :: "circline ⇒ complex_homo" is calc_x_axis_intersection_clmat_hcoords
proof transfer
fix H1 H2
assume *: "hermitean H1 ∧ H1 ≠ mat_zero" "hermitean H2 ∧ H2 ≠ mat_zero"
obtain A1 B1 C1 D1 A2 B2 C2 D2 where hh: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
by (cases H1, cases H2, auto)
assume "circline_eq_cmat H1 H2"
then obtain k where k: "k ≠ 0" "H2 = cor k *⇩s⇩m H1"
by auto
have "calc_x_axis_intersection_cvec A1 B1 ≈⇩v calc_x_axis_intersection_cvec A2 B2"
using hh k
apply simp
apply (rule_tac x="cor k" in exI)
apply auto
apply (simp add: sgn_mult power_mult_distrib)
apply (subst right_diff_distrib[symmetric])
apply (subst real_sqrt_mult)
by (simp add: real_sgn_eq right_diff_distrib)
thus "calc_x_axis_intersection_cmat_cvec H1 ≈⇩v
calc_x_axis_intersection_cmat_cvec H2"
using hh k
by (auto simp del: calc_x_axis_intersection_cvec_def)
qed
lemma calc_x_axis_intersection_in_unit_disc:
assumes "is_poincare_line H" "intersects_x_axis H"
shows "calc_x_axis_intersection H ∈ unit_disc"
proof (cases "is_line H")
case True
thus ?thesis
using assms
unfolding unit_disc_def disc_def
by simp (transfer, transfer, auto simp add: vec_cnj_def)
next
case False
thus ?thesis
using assms
unfolding unit_disc_def disc_def
proof (simp, transfer, transfer)
fix H
assume hh: "hermitean H ∧ H ≠ mat_zero"
then obtain A B D where *: "H = (A, B, cnj B, D)" "is_real A" "is_real D"
using hermitean_elems
by (cases H) blast
assume "is_poincare_line_cmat H"
hence *: "H = (A, B, cnj B, A)" "is_real A"
using *
by auto
assume "¬ circline_A0_cmat H"
hence "A ≠ 0"
using *
by simp
assume "intersects_x_axis_cmat H"
hence "(Re B)⇧2 > (Re A)⇧2"
using * ‹A ≠ 0›
by (auto simp add: power2_eq_square complex.expand)
hence "Re B ≠ 0"
by auto
have "Re A ≠ 0"
using ‹is_real A› ‹A ≠ 0›
by (auto simp add: complex.expand)
have "sqrt((Re B)⇧2 - (Re A)⇧2) < sqrt((Re B)⇧2)"
using ‹Re A ≠ 0›
by (subst real_sqrt_less_iff) auto
also have "... = sgn (Re B) * (Re B)"
by (smt mult_minus_right nonzero_eq_divide_eq real_sgn_eq real_sqrt_abs)
finally
have 1: "sqrt((Re B)⇧2 - (Re A)⇧2) < sgn (Re B) * (Re B)"
.
have 2: "(Re B)⇧2 - (Re A)⇧2 < sgn (Re B) * (Re B) * sqrt((Re B)⇧2 - (Re A)⇧2)"
using ‹(Re B)⇧2 > (Re A)⇧2›
using mult_strict_right_mono[OF 1, of "sqrt ((Re B)⇧2 - (Re A)⇧2)"]
by simp
have 3: "(Re B)⇧2 - 2*sgn (Re B)*Re B*sqrt((Re B)⇧2 - (Re A)⇧2) + (Re B)⇧2 - (Re A)⇧2 < (Re A)⇧2"
using mult_strict_left_mono[OF 2, of 2]
by (simp add: field_simps)
have "(sgn (Re B))⇧2 = 1"
using ‹Re B ≠ 0›
by (simp add: sgn_if)
hence "(-Re B + sgn (Re B) * sqrt((Re B)⇧2 - (Re A)⇧2))⇧2 < (Re A)⇧2"
using ‹(Re B)⇧2 > (Re A)⇧2› 3
by (simp add: power2_diff field_simps)
thus "in_ocircline_cmat_cvec unit_circle_cmat (calc_x_axis_intersection_cmat_cvec H)"
using * ‹(Re B)⇧2 > (Re A)⇧2›
by (auto simp add: vec_cnj_def power2_eq_square split: if_split_asm)
qed
qed
lemma calc_x_axis_intersection:
assumes "is_poincare_line H" and "intersects_x_axis H"
shows "calc_x_axis_intersection H ∈ circline_set H ∩ circline_set x_axis"
proof (cases "is_line H")
case True
thus ?thesis
using assms
unfolding circline_set_def
by simp (transfer, transfer, auto simp add: vec_cnj_def)
next
case False
thus ?thesis
using assms
unfolding circline_set_def
proof (simp, transfer, transfer)
fix H
assume hh: "hermitean H ∧ H ≠ mat_zero"
then obtain A B D where *: "H = (A, B, cnj B, D)" "is_real A" "is_real D"
using hermitean_elems
by (cases H) blast
assume "is_poincare_line_cmat H"
hence *: "H = (A, B, cnj B, A)" "is_real A"
using *
by auto
assume "¬ circline_A0_cmat H"
hence "A ≠ 0"
using *
by auto
assume "intersects_x_axis_cmat H"
hence "(Re B)⇧2 > (Re A)⇧2"
using * ‹A ≠ 0›
by (auto simp add: power2_eq_square complex.expand)
hence "Re B ≠ 0"
by auto
show "on_circline_cmat_cvec H (calc_x_axis_intersection_cmat_cvec H) ∧
on_circline_cmat_cvec x_axis_cmat (calc_x_axis_intersection_cmat_cvec H)" (is "?P1 ∧ ?P2")
proof
show "on_circline_cmat_cvec H (calc_x_axis_intersection_cmat_cvec H)"
proof (cases "circline_A0_cmat H")
case True
thus ?thesis
using * ‹is_poincare_line_cmat H› ‹intersects_x_axis_cmat H›
by (simp add: vec_cnj_def)
next
case False
let ?x = "calc_x_axis_intersection_cvec A B"
let ?nom = "fst ?x" and ?den = "snd ?x"
have x: "?x = (?nom, ?den)"
by simp
hence "on_circline_cmat_cvec H (calc_x_axis_intersection_cvec A B)"
proof (subst *, subst x, subst on_circline_cmat_cvec_circline_equation)
have "(sgn(Re B))⇧2 = 1"
using ‹Re B ≠ 0› sgn_pos zero_less_power2 by fastforce
have "(sqrt((Re B)⇧2 - (Re A)⇧2))⇧2 = (Re B)⇧2 - (Re A)⇧2"
using ‹(Re B)⇧2 > (Re A)⇧2›
by simp
have "(-(Re B) + sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2))⇧2 =
(-(Re B))⇧2 + (sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2))⇧2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2)"
by (simp add: power2_diff)
also have "... = (Re B)*(Re B) + (sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2))⇧2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2)"
by (simp add: power2_eq_square)
also have "... = (Re B)*(Re B) + (sgn(Re B))⇧2*(sqrt((Re B)⇧2 - (Re A)⇧2))⇧2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2)"
by (simp add: power_mult_distrib)
also have "... = (Re B)*(Re B) + (Re B)⇧2 - (Re A)⇧2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2)"
using ‹(sqrt((Re B)⇧2 - (Re A)⇧2))⇧2 = (Re B)⇧2 - (Re A)⇧2› ‹(sgn(Re B))⇧2 = 1›
by simp
finally have "(-(Re B) + sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2))⇧2 =
(Re B)*(Re B) + (Re B)⇧2 - (Re A)⇧2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2)"
by simp
have "is_real ?nom" "is_real ?den"
using ‹is_real A›
by simp+
hence "cnj (?nom) = ?nom" "cnj (?den) = ?den"
by (simp add:eq_cnj_iff_real)+
hence "A*?nom*(cnj (?nom)) + B*?den*(cnj (?nom)) + (cnj B)*(cnj (?den))*?nom + A*?den*(cnj (?den))
= A*?nom*?nom + B*?den*?nom + (cnj B)*?den*?nom + A*?den*?den"
by auto
also have "... = A*?nom*?nom + (B + (cnj B))*?den*?nom + A*?den*?den"
by (simp add:field_simps)
also have "... = A*?nom*?nom + 2*(Re B)*?den*?nom + A*?den*?den"
by (simp add:complex_add_cnj)
also have "... = A*?nom⇧2 + 2*(Re B)*?den*?nom + A*?den*?den"
by (simp add:power2_eq_square)
also have "... = A*(-(Re B) + sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2))⇧2
+ 2*(Re B)*A*(-(Re B) + sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2)) + A*A*A"
unfolding calc_x_axis_intersection_cvec_def
by auto
also have "... = A*((Re B)*(Re B) + (Re B)⇧2 - (Re A)⇧2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2))
+ 2*(Re B)*A*(-(Re B) + sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2)) + A*A*A"
using ‹(-(Re B) + sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2))⇧2 =
(Re B)*(Re B) + (Re B)⇧2 - (Re A)⇧2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2)›
by simp
also have "... = A*((Re B)*(Re B) + (Re B)⇧2 - A⇧2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2))
+ 2*(Re B)*A*(-(Re B) + sgn(Re B)*sqrt((Re B)⇧2 - (Re A)⇧2)) + A*A*A"
using ‹is_real A›
by simp
also have "... = 0"
apply (simp add:field_simps)
by (simp add: power2_eq_square)
finally have "A*?nom*(cnj (?nom)) + B*?den*(cnj (?nom)) + (cnj B)*(cnj (?den))*?nom + A*?den*(cnj (?den)) = 0"
by simp
thus "circline_equation A B (cnj B) A ?nom ?den"
by simp
qed
thus ?thesis
using * ‹is_poincare_line_cmat H› ‹intersects_x_axis_cmat H›
by (simp add: vec_cnj_def)
qed
next
show "on_circline_cmat_cvec x_axis_cmat (calc_x_axis_intersection_cmat_cvec H)"
using * ‹is_poincare_line_cmat H› ‹intersects_x_axis_cmat H› ‹is_real A›
using eq_cnj_iff_real[of A]
by (simp add: vec_cnj_def)
qed
qed
qed
lemma unique_calc_x_axis_intersection:
assumes "is_poincare_line H" and "H ≠ x_axis"
assumes "x ∈ unit_disc" and "x ∈ circline_set H ∩ circline_set x_axis"
shows "x = calc_x_axis_intersection H"
proof-
have *: "intersects_x_axis H"
using assms
using intersects_x_axis_iff[OF assms(1)]
by auto
show "x = calc_x_axis_intersection H"
using calc_x_axis_intersection[OF assms(1) *]
using calc_x_axis_intersection_in_unit_disc[OF assms(1) *]
using assms
using unique_is_poincare_line[of x "calc_x_axis_intersection H" H x_axis]
by auto
qed
subsection‹Check if an h-line intersects the positive part of the x-axis›
definition intersects_x_axis_positive_cmat :: "complex_mat ⇒ bool" where
[simp]: "intersects_x_axis_positive_cmat H = (let (A, B, C, D) = H in Re A ≠ 0 ∧ Re B / Re A < -1)"
lift_definition intersects_x_axis_positive_clmat :: "circline_mat ⇒ bool" is intersects_x_axis_positive_cmat
done
lift_definition intersects_x_axis_positive :: "circline ⇒ bool" is intersects_x_axis_positive_clmat
proof (transfer)
fix H1 H2
assume hh: "hermitean H1 ∧ H1 ≠ mat_zero" and "hermitean H2 ∧ H2 ≠ mat_zero"
obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
by (cases H1, cases H2, auto)
assume "circline_eq_cmat H1 H2"
then obtain k where "k ≠ 0 ∧ H2 = cor k *⇩s⇩m H1"
by auto
thus "intersects_x_axis_positive_cmat H1 = intersects_x_axis_positive_cmat H2"
using *
by simp
qed
lemma intersects_x_axis_positive_mk_circline:
assumes "is_real A" and "A ≠ 0 ∨ B ≠ 0"
shows "intersects_x_axis_positive (mk_circline A B (cnj B) A) ⟷ Re B / Re A < -1"
proof-
let ?H = "(A, B, (cnj B), A)"
have "hermitean ?H"
using ‹is_real A›
unfolding hermitean_def mat_adj_def mat_cnj_def
using eq_cnj_iff_real
by auto
moreover
have "?H ≠ mat_zero"
using assms
by auto
ultimately
show ?thesis
by (transfer, transfer, auto simp add: Let_def)
qed
lemma intersects_x_axis_positive_intersects_x_axis [simp]:
assumes "intersects_x_axis_positive H"
shows "intersects_x_axis H"
proof-
have "⋀ a aa. ⟦ Re a ≠ 0; Re aa / Re a < - 1; ¬ (Re a)⇧2 < (Re aa)⇧2 ⟧ ⟹ aa = 0 ∧ a = 0"
by (smt less_divide_eq_1_pos one_less_power pos2 power2_minus power_divide zero_less_power2)
thus ?thesis
using assms
apply transfer
apply transfer
apply (auto simp add: hermitean_def mat_adj_def mat_cnj_def)
done
qed
lemma add_less_abs_positive_iff:
fixes a b :: real
assumes "abs b < abs a"
shows "a + b > 0 ⟷ a > 0"
using assms
by auto
lemma calc_x_axis_intersection_positive_abs':
fixes A B :: real
assumes "B⇧2 > A⇧2" and "A ≠ 0"
shows "abs (sgn(B) * sqrt(B⇧2 - A⇧2) / A) < abs(-B/A)"
proof-
from assms have "B ≠ 0"
by auto
have "B⇧2 - A⇧2 < B⇧2"
using ‹A ≠ 0›
by auto
hence "sqrt (B⇧2 - A⇧2) < abs B"
using real_sqrt_less_iff[of "B⇧2 - A⇧2" "B⇧2"]
by simp
thus ?thesis
using assms ‹B ≠ 0›
by (simp add: abs_mult divide_strict_right_mono)
qed
lemma calc_intersect_x_axis_positive_lemma:
assumes "B⇧2 > A⇧2" and "A ≠ 0"
shows "(-B + sgn B * sqrt(B⇧2 - A⇧2)) / A > 0 ⟷ -B/A > 1"
proof-
have "(-B + sgn B * sqrt(B⇧2 - A⇧2)) / A = -B / A + (sgn B * sqrt(B⇧2 - A⇧2)) / A"
using assms
by (simp add: field_simps)
moreover
have "-B / A + (sgn B * sqrt(B⇧2 - A⇧2)) / A > 0 ⟷ - B / A > 0"
using add_less_abs_positive_iff[OF calc_x_axis_intersection_positive_abs'[OF assms]]
by simp
moreover
hence "(B/A)⇧2 > 1"
using assms
by (simp add: power_divide)
hence "B/A > 1 ∨ B/A < -1"
by (smt one_power2 pos2 power2_minus power_0 power_strict_decreasing zero_power2)
hence "-B / A > 0 ⟷ -B / A > 1"
by auto
ultimately
show ?thesis
using assms
by auto
qed
lemma intersects_x_axis_positive_iff':
assumes "is_poincare_line H"
shows "intersects_x_axis_positive H ⟷
calc_x_axis_intersection H ∈ unit_disc ∧ calc_x_axis_intersection H ∈ circline_set H ∩ positive_x_axis" (is "?lhs ⟷ ?rhs")
proof
let ?x = "calc_x_axis_intersection H"
assume ?lhs
hence "?x ∈ circline_set x_axis" "?x ∈ circline_set H" "?x ∈ unit_disc"
using calc_x_axis_intersection_in_unit_disc[OF assms] calc_x_axis_intersection[OF assms]
by auto
moreover
have "Re (to_complex ?x) > 0"
using ‹?lhs› assms
proof (transfer, transfer)
fix H
assume hh: "hermitean H ∧ H ≠ mat_zero"
obtain A B C D where *: "H = (A, B, C, D)"
by (cases H, auto)
assume "intersects_x_axis_positive_cmat H"
hence **: "Re B / Re A < - 1" "Re A ≠ 0"
using *
by auto
have "(Re B)⇧2 > (Re A)⇧2"
using **
by (smt divide_less_eq_1_neg divide_minus_left less_divide_eq_1_pos real_sqrt_abs real_sqrt_less_iff right_inverse_eq)
have "is_real A" "A ≠ 0"
using hh hermitean_elems * ‹Re A ≠ 0› complex.expand[of A 0]
by auto
have "(cmod B)⇧2 > (cmod A)⇧2"
using ‹(Re B)⇧2 > (Re A)⇧2› ‹is_real A›
by (smt cmod_power2 power2_less_0 zero_power2)
have ***: "0 < (- Re B + sgn (Re B) * sqrt ((Re B)⇧2 - (Re A)⇧2)) / Re A"
using calc_intersect_x_axis_positive_lemma[of "Re A" "Re B"] ** ‹(Re B)⇧2 > (Re A)⇧2›
by auto
assume "is_poincare_line_cmat H"
hence "A = D"
using * hh
by simp
have "Re ((cor (sgn (Re B)) * cor (sqrt ((Re B)⇧2 - (Re A)⇧2)) - cor (Re B)) / A) = (sgn (Re B) * sqrt ((Re B)⇧2 - (Re A)⇧2) - Re B) / Re D"
using ‹is_real A› ‹A = D›
by (metis (no_types, lifting) Re_complex_of_real complex_of_real_Re of_real_diff of_real_divide of_real_mult)
thus "0 < Re (to_complex_cvec (calc_x_axis_intersection_cmat_cvec H))"
using * hh ** *** ‹(cmod B)⇧2 > (cmod A)⇧2› ‹(Re B)⇧2 > (Re A)⇧2› ‹A ≠ 0› ‹A = D›
by simp
qed
ultimately
show ?rhs
unfolding positive_x_axis_def
by auto
next
let ?x = "calc_x_axis_intersection H"
assume ?rhs
hence "Re (to_complex ?x) > 0" "?x ≠ ∞⇩h" "?x ∈ circline_set x_axis" "?x ∈ unit_disc" "?x ∈ circline_set H"
unfolding positive_x_axis_def
by auto
hence "intersects_x_axis H"
using intersects_x_axis_iff[OF assms]
by auto
thus ?lhs
using ‹Re (to_complex ?x) > 0› assms
proof (transfer, transfer)
fix H
assume hh: "hermitean H ∧ H ≠ mat_zero"
obtain A B C D where *: "H = (A, B, C, D)"
by (cases H, auto)
assume "0 < Re (to_complex_cvec (calc_x_axis_intersection_cmat_cvec H))" "intersects_x_axis_cmat H" "is_poincare_line_cmat H"
hence **: "A ≠ 0" "0 < Re ((cor (sgn (Re B)) * cor (sqrt ((Re B)⇧2 - (Re A)⇧2)) - cor (Re B)) / A)" "A = D" "is_real A" "(Re B)⇧2 > (Re A)⇧2"
using * hh hermitean_elems
by (auto split: if_split_asm)
have "Re A ≠ 0"
using complex.expand[of A 0] ‹A ≠ 0› ‹is_real A›
by auto
have "Re ((cor (sgn (Re B)) * cor (sqrt ((Re B)⇧2 - (Re D)⇧2)) - cor (Re B)) / D) = (sgn (Re B) * sqrt ((Re B)⇧2 - (Re D)⇧2) - Re B) / Re D"
using ‹is_real A› ‹A = D›
by (metis (no_types, lifting) Re_complex_of_real complex_of_real_Re of_real_diff of_real_divide of_real_mult)
thus "intersects_x_axis_positive_cmat H"
using * ** ‹Re A ≠ 0›
using calc_intersect_x_axis_positive_lemma[of "Re A" "Re B"]
by simp
qed
qed
lemma intersects_x_axis_positive_iff:
assumes "is_poincare_line H" and "H ≠ x_axis"
shows "intersects_x_axis_positive H ⟷
(∃ x. x ∈ unit_disc ∧ x ∈ circline_set H ∩ positive_x_axis)" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
thus ?rhs
using intersects_x_axis_positive_iff'[OF assms(1)]
by auto
next
assume ?rhs
then obtain x where "x ∈ unit_disc" "x ∈ circline_set H ∩ positive_x_axis"
by auto
thus ?lhs
using unique_calc_x_axis_intersection[OF assms, of x]
using intersects_x_axis_positive_iff'[OF assms(1)]
unfolding positive_x_axis_def
by auto
qed
subsection‹Check if an h-line intersects the positive part of the y-axis›
definition intersects_y_axis_positive_cmat :: "complex_mat ⇒ bool" where
[simp]: "intersects_y_axis_positive_cmat H = (let (A, B, C, D) = H in Re A ≠ 0 ∧ Im B / Re A < -1)"
lift_definition intersects_y_axis_positive_clmat :: "circline_mat ⇒ bool" is intersects_y_axis_positive_cmat
done
lift_definition intersects_y_axis_positive :: "circline ⇒ bool" is intersects_y_axis_positive_clmat
proof (transfer)
fix H1 H2
assume hh: "hermitean H1 ∧ H1 ≠ mat_zero" and "hermitean H2 ∧ H2 ≠ mat_zero"
obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
by (cases H1, cases H2, auto)
assume "circline_eq_cmat H1 H2"
then obtain k where "k ≠ 0 ∧ H2 = cor k *⇩s⇩m H1"
by auto
thus "intersects_y_axis_positive_cmat H1 = intersects_y_axis_positive_cmat H2"
using *
by simp
qed
lemma intersects_x_axis_positive_intersects_y_axis_positive [simp]:
shows "intersects_x_axis_positive (moebius_circline (moebius_rotation (-pi/2)) H) ⟷ intersects_y_axis_positive H"
using hermitean_elems
unfolding moebius_rotation_def moebius_similarity_def
by simp (transfer, transfer, auto simp add: mat_adj_def mat_cnj_def)
lemma intersects_y_axis_positive_iff:
assumes "is_poincare_line H" "H ≠ y_axis"
shows "(∃ y ∈ unit_disc. y ∈ circline_set H ∩ positive_y_axis) ⟷ intersects_y_axis_positive H" (is "?lhs ⟷ ?rhs")
proof-
let ?R = "moebius_rotation (-pi / 2)"
let ?H' = "moebius_circline ?R H"
have 1: "is_poincare_line ?H'"
using assms
using unit_circle_fix_preserve_is_poincare_line[OF _ assms(1), of ?R]
by simp
have 2: "moebius_circline ?R H ≠ x_axis"
proof (rule ccontr)
assume "¬ ?thesis"
hence "H = moebius_circline (moebius_rotation (pi/2)) x_axis"
using moebius_circline_comp_inv_left[of ?R H]
by auto
thus False
using ‹H ≠ y_axis›
by auto
qed
show ?thesis
proof
assume "?lhs"
then obtain y where "y ∈ unit_disc" "y ∈ circline_set H ∩ positive_y_axis"
by auto
hence "moebius_pt ?R y ∈ unit_disc" "moebius_pt ?R y ∈ circline_set ?H' ∩ positive_x_axis"
using rotation_minus_pi_2_positive_y_axis
by auto
thus ?rhs
using intersects_x_axis_positive_iff[OF 1 2]
using intersects_x_axis_positive_intersects_y_axis_positive[of H]
by auto
next
assume "intersects_y_axis_positive H"
hence "intersects_x_axis_positive ?H'"
using intersects_x_axis_positive_intersects_y_axis_positive[of H]
by simp
then obtain x where *: "x ∈ unit_disc" "x ∈ circline_set ?H' ∩ positive_x_axis"
using intersects_x_axis_positive_iff[OF 1 2]
by auto
let ?y = "moebius_pt (-?R) x"
have "?y ∈ unit_disc ∧ ?y ∈ circline_set H ∩ positive_y_axis"
using * rotation_minus_pi_2_positive_y_axis[symmetric]
by (metis Int_iff circline_set_moebius_circline_E image_eqI moebius_pt_comp_inv_image_left moebius_rotation_uminus uminus_moebius_def unit_disc_fix_discI unit_disc_fix_rotation)
thus ?lhs
by auto
qed
qed
subsection‹Position of the intersection point in the unit disc›
text‹Check if the intersection point of one h-line with the x-axis is located more outward the edge
of the disc than the intersection point of another h-line.›
definition outward_cmat :: "complex_mat ⇒ complex_mat ⇒ bool" where
[simp]: "outward_cmat H1 H2 = (let (A1, B1, C1, D1) = H1; (A2, B2, C2, D2) = H2
in -Re B1/Re A1 ≤ -Re B2/Re A2)"
lift_definition outward_clmat :: "circline_mat ⇒ circline_mat ⇒ bool" is outward_cmat
done
lift_definition outward :: "circline ⇒ circline ⇒ bool" is outward_clmat
apply transfer
apply simp
apply (case_tac circline_mat1, case_tac circline_mat2, case_tac circline_mat3, case_tac circline_mat4)
apply simp
apply (erule_tac exE)+
apply (erule_tac conjE)+
apply simp
done
lemma outward_mk_circline:
assumes "is_real A1" and "is_real A2" and "A1 ≠ 0 ∨ B1 ≠ 0" and "A2 ≠ 0 ∨ B2 ≠ 0"
shows "outward (mk_circline A1 B1 (cnj B1) A1) (mk_circline A2 B2 (cnj B2) A2) ⟷ - Re B1 / Re A1 ≤ - Re B2 / Re A2"
proof-
let ?H1 = "(A1, B1, (cnj B1), A1)"
let ?H2 = "(A2, B2, (cnj B2), A2)"
have "hermitean ?H1" "hermitean ?H2"
using ‹is_real A1› ‹is_real A2›
unfolding hermitean_def mat_adj_def mat_cnj_def
using eq_cnj_iff_real
by auto
moreover
have "?H1 ≠ mat_zero" "?H2 ≠ mat_zero"
using assms
by auto
ultimately
show ?thesis
by (transfer, transfer, auto simp add: Let_def)
qed
lemma calc_x_axis_intersection_fun_mono:
fixes x1 x2 :: real
assumes "x1 > 1" and "x2 > x1"
shows "x1 - sqrt(x1⇧2 - 1) > x2 - sqrt(x2⇧2 - 1)"
using assms
proof-
have *: "sqrt(x1⇧2 - 1) + sqrt(x2⇧2 - 1) > 0"
using assms
by (smt one_less_power pos2 real_sqrt_gt_zero)
have "sqrt(x1⇧2 - 1) < x1"
using real_sqrt_less_iff[of "x1⇧2 - 1" "x1⇧2"] ‹x1 > 1›
by auto
moreover
have "sqrt(x2⇧2 - 1) < x2"
using real_sqrt_less_iff[of "x2⇧2 - 1" "x2⇧2"] ‹x1 > 1› ‹x2 > x1›
by auto
ultimately
have "sqrt(x1⇧2 - 1) + sqrt(x2⇧2 - 1) < x1 + x2"
by simp
hence "(x1 + x2) / (sqrt(x1⇧2 - 1) + sqrt(x2⇧2 - 1)) > 1"
using *
using less_divide_eq_1_pos[of "sqrt(x1⇧2 - 1) + sqrt(x2⇧2 - 1)" "x1 + x2"]
by simp
hence "(x2⇧2 - x1⇧2) / (sqrt(x1⇧2 - 1) + sqrt(x2⇧2 - 1)) > x2 - x1"
using ‹x2 > x1›
using mult_less_cancel_left_pos[of "x2 - x1" 1 "(x2 + x1) / (sqrt(x1⇧2 - 1) + sqrt(x2⇧2 - 1))"]
by (simp add: power2_eq_square field_simps)
moreover
have "(x2⇧2 - x1⇧2) = (sqrt(x1⇧2 - 1) + sqrt(x2⇧2 - 1)) * ((sqrt(x2⇧2 - 1) - sqrt(x1⇧2 - 1)))"
using ‹x1 > 1› ‹x2 > x1›
by (simp add: field_simps)
ultimately
have "sqrt(x2⇧2 - 1) - sqrt(x1⇧2 - 1) > x2 - x1"
using *
by simp
thus ?thesis
by simp
qed
lemma calc_x_axis_intersection_mono:
fixes a1 b1 a2 b2 :: real
assumes "-b1/a1 > 1" and "a1 ≠ 0" and "-b2/a2 ≥ -b1/a1" and "a2 ≠ 0"
shows "(-b1 + sgn b1 * sqrt(b1⇧2 - a1⇧2)) / a1 ≥ (-b2 + sgn b2 * sqrt(b2⇧2 - a2⇧2)) / a2" (is "?lhs ≥ ?rhs")
proof-
have "?lhs = -b1/a1 - sqrt((-b1/a1)⇧2 - 1)"
proof (cases "b1 > 0")
case True
hence "a1 < 0"
using assms
by (smt divide_neg_pos)
thus ?thesis
using ‹b1 > 0› ‹a1 < 0›
by (simp add: real_sqrt_divide field_simps)
next
case False
hence "b1 < 0"
using assms
by (cases "b1 = 0") auto
hence "a1 > 0"
using assms
by (smt divide_pos_neg)
thus ?thesis
using ‹b1 < 0› ‹a1 > 0›
by (simp add: real_sqrt_divide field_simps)
qed
moreover
have "?rhs = -b2/a2 - sqrt((-b2/a2)⇧2 - 1)"
proof (cases "b2 > 0")
case True
hence "a2 < 0"
using assms
by (smt divide_neg_pos)
thus ?thesis
using ‹b2 > 0› ‹a2 < 0›
by (simp add: real_sqrt_divide field_simps)
next
case False
hence "b2 < 0"
using assms
by (cases "b2 = 0") auto
hence "a2 > 0"
using assms
by (smt divide_pos_neg)
thus ?thesis
using ‹b2 < 0› ‹a2 > 0›
by (simp add: real_sqrt_divide field_simps)
qed
ultimately
show ?thesis
using calc_x_axis_intersection_fun_mono[of "-b1/a1" "-b2/a2"]
using assms
by (cases "-b1/a1=-b2/a2", auto)
qed
lemma outward:
assumes "is_poincare_line H1" and "is_poincare_line H2"
assumes "intersects_x_axis_positive H1" and "intersects_x_axis_positive H2"
assumes "outward H1 H2"
shows "Re (to_complex (calc_x_axis_intersection H1)) ≥ Re (to_complex (calc_x_axis_intersection H2))"
proof-
have "intersects_x_axis H1" "intersects_x_axis H2"
using assms
by auto
thus ?thesis
using assms
proof (transfer, transfer)
fix H1 H2
assume hh: "hermitean H1 ∧ H1 ≠ mat_zero" "hermitean H2 ∧ H2 ≠ mat_zero"
obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
by (cases H1, cases H2, auto)
have "is_real A1" "is_real A2"
using hermitean_elems * hh
by auto
assume 1: "intersects_x_axis_positive_cmat H1" "intersects_x_axis_positive_cmat H2"
assume 2: "intersects_x_axis_cmat H1" "intersects_x_axis_cmat H2"
assume 3: "is_poincare_line_cmat H1" "is_poincare_line_cmat H2"
assume 4: "outward_cmat H1 H2"
have "A1 ≠ 0" "A2 ≠ 0"
using * ‹is_real A1› ‹is_real A2› 1 complex.expand[of A1 0] complex.expand[of A2 0]
by auto
hence "(sgn (Re B2) * sqrt ((Re B2)⇧2 - (Re A2)⇧2) - Re B2) / Re A2
≤ (sgn (Re B1) * sqrt ((Re B1)⇧2 - (Re A1)⇧2) - Re B1) / Re A1"
using calc_x_axis_intersection_mono[of "Re B1" "Re A1" "Re B2" "Re A2"]
using 1 4 *
by simp
moreover
have "(sgn (Re B2) * sqrt ((Re B2)⇧2 - (Re A2)⇧2) - Re B2) / Re A2 =
Re ((cor (sgn (Re B2)) * cor (sqrt ((Re B2)⇧2 - (Re A2)⇧2)) - cor (Re B2)) / A2)"
using ‹is_real A2› ‹A2 ≠ 0›
by (simp add: Re_divide_real)
moreover
have "(sgn (Re B1) * sqrt ((Re B1)⇧2 - (Re A1)⇧2) - Re B1) / Re A1 =
Re ((cor (sgn (Re B1)) * cor (sqrt ((Re B1)⇧2 - (Re A1)⇧2)) - cor (Re B1)) / A1)"
using ‹is_real A1› ‹A1 ≠ 0›
by (simp add: Re_divide_real)
ultimately
show "Re (to_complex_cvec (calc_x_axis_intersection_cmat_cvec H2))
≤ Re (to_complex_cvec (calc_x_axis_intersection_cmat_cvec H1))"
using 2 3 ‹A1 ≠ 0› ‹A2 ≠ 0› * ‹is_real A1› ‹is_real A2›
by (simp del: is_poincare_line_cmat_def intersects_x_axis_cmat_def)
qed
qed
subsection‹Ideal points and x-axis intersection›
lemma ideal_points_intersects_x_axis:
assumes "is_poincare_line H" and "ideal_points H = {i1, i2}" and "H ≠ x_axis"
shows "intersects_x_axis H ⟷ Im (to_complex i1) * Im (to_complex i2) < 0"
using assms
proof-
have "i1 ≠ i2"
using assms(1) assms(2) ex_poincare_line_points ideal_points_different(1)
by blast
have "calc_ideal_points H = {i1, i2}"
using assms
using ideal_points_unique
by auto
have "∀ i1 ∈ calc_ideal_points H.
∀ i2 ∈ calc_ideal_points H.
is_poincare_line H ∧ H ≠ x_axis ∧ i1 ≠ i2 ⟶ (Im (to_complex i1) * Im (to_complex i2) < 0 ⟷ intersects_x_axis H)"
proof (transfer, transfer, (rule ballI)+, rule impI, (erule conjE)+, case_tac H, case_tac i1, case_tac i2)
fix i11 i12 i21 i22 A B C D H i1 i2
assume H: "H = (A, B, C, D)" "hermitean H" "H ≠ mat_zero"
assume line: "is_poincare_line_cmat H"
assume i1: "i1 = (i11, i12)" "i1 ∈ calc_ideal_points_cmat_cvec H"
assume i2: "i2 = (i21, i22)" "i2 ∈ calc_ideal_points_cmat_cvec H"
assume different: "¬ i1 ≈⇩v i2"
assume not_x_axis: "¬ circline_eq_cmat H x_axis_cmat"
have "is_real A" "is_real D" "C = cnj B"
using H hermitean_elems
by auto
have "(cmod A)⇧2 < (cmod B)⇧2" "A = D"
using line H
by auto
let ?discr = "sqrt ((cmod B)⇧2 - (Re D)⇧2)"
let ?den = "(cmod B)⇧2"
let ?i1 = "B * (- D - 𝗂 * ?discr)"
let ?i2 = "B * (- D + 𝗂 * ?discr)"
have "i11 = ?i1 ∨ i11 = ?i2" "i12 = ?den"
"i21 = ?i1 ∨ i21 = ?i2" "i22 = ?den"
using i1 i2 H line
by (auto split: if_split_asm)
hence i: "i11 = ?i1 ∧ i21 = ?i2 ∨ i11 = ?i2 ∧ i21 = ?i1"
using ‹¬ i1 ≈⇩v i2› i1 i2
by auto
have "Im (i11 / i12) * Im (i21 / i22) = Im (?i1 / ?den) * Im (?i2 / ?den)"
using i ‹i12 = ?den› ‹i22 = ?den›
by auto
also have "... = Im (?i1) * Im (?i2) / ?den⇧2"
by simp
also have "... = (Im B * (Im B * (Re D * Re D)) - Re B * (Re B * ((cmod B)⇧2 - (Re D)⇧2))) / cmod B ^ 4"
using ‹(cmod B)⇧2 > (cmod A)⇧2› ‹A = D›
using ‹is_real D› cmod_eq_Re[of A]
by (auto simp add: field_simps)
also have "... = ((Im B)⇧2 * (Re D)⇧2 - (Re B)⇧2 * ((Re B)⇧2 + (Im B)⇧2 - (Re D)⇧2)) / cmod B ^ 4"
proof-
have "cmod B * cmod B = Re B * Re B + Im B * Im B"
by (metis cmod_power2 power2_eq_square)
thus ?thesis
by (simp add: power2_eq_square)
qed
also have "... = (((Re D)⇧2 - (Re B)⇧2) * ((Re B)⇧2 + (Im B)⇧2)) / cmod B ^ 4"
by (simp add: power2_eq_square field_simps)
finally have Im_product: "Im (i11 / i12) * Im (i21 / i22) = ((Re D)⇧2 - (Re B)⇧2) * ((Re B)⇧2 + (Im B)⇧2) / cmod B ^ 4"
.
show "Im (to_complex_cvec i1) * Im (to_complex_cvec i2) < 0 ⟷ intersects_x_axis_cmat H"
proof safe
assume opposite: "Im (to_complex_cvec i1) * Im (to_complex_cvec i2) < 0"
show "intersects_x_axis_cmat H"
proof-
have "((Re D)⇧2 - (Re B)⇧2) * ((Re B)⇧2 + (Im B)⇧2) / cmod B ^ 4 < 0"
using Im_product opposite i1 i2
by simp
hence "((Re D)⇧2 - (Re B)⇧2) * ((Re B)⇧2 + (Im B)⇧2) < 0"
by (simp add: divide_less_0_iff)
hence "(Re D)⇧2 < (Re B)⇧2"
by (simp add: mult_less_0_iff not_sum_power2_lt_zero)
thus ?thesis
using H ‹A = D› ‹is_real D›
by auto
qed
next
have *: "(∀k. k * Im B = 1 ⟶ k = 0) ⟶ Im B = 0"
apply (safe, erule_tac x="1 / Im B" in allE)
using divide_cancel_left by fastforce
assume "intersects_x_axis_cmat H"
hence "Re D = 0 ∨ (Re D)⇧2 < (Re B)⇧2"
using H ‹A = D›
by auto
hence "(Re D)⇧2 < (Re B)⇧2"
using ‹is_real D› line H ‹C = cnj B›
using not_x_axis *
by (auto simp add: complex_eq_iff)
hence "((Re D)⇧2 - (Re B)⇧2) * ((Re B)⇧2 + (Im B)⇧2) < 0"
by (metis add_cancel_left_left diff_less_eq mult_eq_0_iff mult_less_0_iff power2_eq_square power2_less_0 sum_squares_gt_zero_iff)
thus "Im (to_complex_cvec i1) * Im (to_complex_cvec i2) < 0"
using Im_product i1 i2
using divide_eq_0_iff divide_less_0_iff prod.simps(2) to_complex_cvec_def zero_complex.simps(1) zero_less_norm_iff
by fastforce
qed
qed
thus ?thesis
using assms ‹calc_ideal_points H = {i1, i2}› ‹i1 ≠ i2›
by auto
qed
end