Theory Poincare_Between
theory Poincare_Between
imports Poincare_Distance
begin
section‹H-betweenness in the Poincar\'e model›
subsection ‹H-betwenness expressed by a cross-ratio›
text‹The point $v$ is h-between $u$ and $w$ if the cross-ratio between the pairs $u$ and $w$ and $v$
and inverse of $v$ is real and negative.›
definition poincare_between :: "complex_homo ⇒ complex_homo ⇒ complex_homo ⇒ bool" where
"poincare_between u v w ⟷
u = v ∨ v = w ∨
(let cr = cross_ratio u v w (inversion v)
in is_real (to_complex cr) ∧ Re (to_complex cr) < 0)"
subsubsection ‹H-betwenness is preserved by h-isometries›
text ‹Since they preserve cross-ratio and inversion, h-isometries (unit disc preserving Möbius
transformations and conjugation) preserve h-betweeness.›
lemma unit_disc_fix_moebius_preserve_poincare_between [simp]:
assumes "unit_disc_fix M" and "u ∈ unit_disc" and "v ∈ unit_disc" and "w ∈ unit_disc"
shows "poincare_between (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) ⟷
poincare_between u v w"
proof (cases "u = v ∨ v = w")
case True
thus ?thesis
using assms
unfolding poincare_between_def
by auto
next
case False
moreover
hence "moebius_pt M u ≠ moebius_pt M v ∧ moebius_pt M v ≠ moebius_pt M w"
by auto
moreover
have "v ≠ inversion v" "w ≠ inversion v"
using inversion_noteq_unit_disc[of v w]
using inversion_noteq_unit_disc[of v v]
using ‹v ∈ unit_disc› ‹w ∈ unit_disc›
by auto
ultimately
show ?thesis
using assms
using unit_circle_fix_moebius_pt_inversion[of M v, symmetric]
unfolding poincare_between_def
by (simp del: unit_circle_fix_moebius_pt_inversion)
qed
lemma conjugate_preserve_poincare_between [simp]:
assumes "u ∈ unit_disc" and "v ∈ unit_disc" and "w ∈ unit_disc"
shows "poincare_between (conjugate u) (conjugate v) (conjugate w) ⟷
poincare_between u v w"
proof (cases "u = v ∨ v = w")
case True
thus ?thesis
using assms
unfolding poincare_between_def
by auto
next
case False
moreover
hence "conjugate u ≠ conjugate v ∧ conjugate v ≠ conjugate w"
using conjugate_inj by blast
moreover
have "v ≠ inversion v" "w ≠ inversion v"
using inversion_noteq_unit_disc[of v w]
using inversion_noteq_unit_disc[of v v]
using ‹v ∈ unit_disc› ‹w ∈ unit_disc›
by auto
ultimately
show ?thesis
using assms
using conjugate_cross_ratio[of v w "inversion v" u]
unfolding poincare_between_def
by (metis conjugate_id_iff conjugate_involution inversion_def inversion_sym o_apply)
qed
subsubsection ‹Some elementary properties of h-betwenness›
lemma poincare_between_nonstrict [simp]:
shows "poincare_between u u v" and "poincare_between u v v"
by (simp_all add: poincare_between_def)
lemma poincare_between_sandwich:
assumes "u ∈ unit_disc" and "v ∈ unit_disc"
assumes "poincare_between u v u"
shows "u = v"
proof (rule ccontr)
assume "¬ ?thesis"
thus False
using assms
using inversion_noteq_unit_disc[of v u]
using cross_ratio_1[of v u "inversion v"]
unfolding poincare_between_def Let_def
by auto
qed
lemma poincare_between_rev:
assumes "u ∈ unit_disc" and "v ∈ unit_disc" and "w ∈ unit_disc"
shows "poincare_between u v w ⟷ poincare_between w v u"
using assms
using inversion_noteq_unit_disc[of v w]
using inversion_noteq_unit_disc[of v u]
using cross_ratio_commute_13[of u v w "inversion v"]
using cross_ratio_not_inf[of w "inversion v" v u]
using cross_ratio_not_zero[of w v u "inversion v"]
using inf_or_of_complex[of "cross_ratio w v u (inversion v)"]
unfolding poincare_between_def
by (auto simp add: Let_def Im_complex_div_eq_0 Re_divide divide_less_0_iff)
subsubsection ‹H-betwenness and h-collinearity›
text‹Three points can be in an h-between relation only when they are h-collinear.›
lemma poincare_between_poincare_collinear [simp]:
assumes in_disc: "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc"
assumes betw: "poincare_between u v w"
shows "poincare_collinear {u, v, w}"
proof (cases "u = v ∨ v = w")
case True
thus ?thesis
using assms
by auto
next
case False
hence distinct: "distinct [u, v, w, inversion v]"
using in_disc inversion_noteq_unit_disc[of v v] inversion_noteq_unit_disc[of v u] inversion_noteq_unit_disc[of v w]
using betw poincare_between_sandwich[of w v]
by (auto simp add: poincare_between_def Let_def)
then obtain H where *: "{u, v, w, inversion v} ⊆ circline_set H"
using assms
unfolding poincare_between_def
using four_points_on_circline_iff_cross_ratio_real[of u v w "inversion v"]
by auto
hence "H = poincare_line u v"
using assms distinct
using unique_circline_set[of u v "inversion v"]
using poincare_line[of u v] poincare_line_inversion[of u v]
unfolding circline_set_def
by auto
thus ?thesis
using * assms False
unfolding poincare_collinear_def
by (rule_tac x="poincare_line u v" in exI) simp
qed
lemma poincare_between_poincare_line_uvz:
assumes "u ≠ v" and "u ∈ unit_disc" and "v ∈ unit_disc" and
"z ∈ unit_disc" and "poincare_between u v z"
shows "z ∈ circline_set (poincare_line u v)"
using assms
using poincare_between_poincare_collinear[of u v z]
using unique_poincare_line[OF assms(1-3)]
unfolding poincare_collinear_def
by auto
lemma poincare_between_poincare_line_uzv:
assumes "u ≠ v" and "u ∈ unit_disc" and "v ∈ unit_disc" and
"z ∈ unit_disc" "poincare_between u z v"
shows "z ∈ circline_set (poincare_line u v)"
using assms
using poincare_between_poincare_collinear[of u z v]
using unique_poincare_line[OF assms(1-3)]
unfolding poincare_collinear_def
by auto
subsubsection ‹H-betweeness on Euclidean segments›
text‹If the three points lie on an h-line that is a Euclidean line (e.g., if it contains zero),
h-betweenness can be characterized much simpler than in the definition.›
lemma poincare_between_x_axis_u0v:
assumes "is_real u'" and "u' ≠ 0" and "v' ≠ 0"
shows "poincare_between (of_complex u') 0⇩h (of_complex v') ⟷ is_real v' ∧ Re u' * Re v' < 0"
proof-
have "Re u' ≠ 0"
using ‹is_real u'› ‹u' ≠ 0›
using complex_eq_if_Re_eq
by auto
have nz: "of_complex u' ≠ 0⇩h" "of_complex v' ≠ 0⇩h"
by (simp_all add: ‹u' ≠ 0› ‹v' ≠ 0›)
hence "0⇩h ≠ of_complex v'"
by metis
let ?cr = "cross_ratio (of_complex u') 0⇩h (of_complex v') ∞⇩h"
have "is_real (to_complex ?cr) ∧ Re (to_complex ?cr) < 0 ⟷ is_real v' ∧ Re u' * Re v' < 0"
using cross_ratio_0inf[of v' u'] ‹v' ≠ 0› ‹u' ≠ 0› ‹is_real u'›
by (metis Re_complex_div_lt_0 Re_mult_real complex_cnj_divide divide_cancel_left eq_cnj_iff_real to_complex_of_complex)
thus ?thesis
unfolding poincare_between_def inversion_zero
using ‹of_complex u' ≠ 0⇩h› ‹0⇩h ≠ of_complex v'›
by simp
qed
lemma poincare_between_u0v:
assumes "u ∈ unit_disc" and "v ∈ unit_disc" and "u ≠ 0⇩h" and "v ≠ 0⇩h"
shows "poincare_between u 0⇩h v ⟷ (∃ k < 0. to_complex u = cor k * to_complex v)" (is "?P u v")
proof (cases "u = v")
case True
thus ?thesis
using assms
using inf_or_of_complex[of v]
using poincare_between_sandwich[of u "0⇩h"]
by auto
next
case False
have "∀ u. u ∈ unit_disc ∧ u ≠ 0⇩h ⟶ ?P u v" (is "?P' v")
proof (rule wlog_rotation_to_positive_x_axis)
fix φ v
let ?M = "moebius_pt (moebius_rotation φ)"
assume 1: "v ∈ unit_disc" "v ≠ 0⇩h"
assume 2: "?P' (?M v)"
show "?P' v"
proof (rule allI, rule impI, (erule conjE)+)
fix u
assume 3: "u ∈ unit_disc" "u ≠ 0⇩h"
have "poincare_between (?M u) 0⇩h (?M v) ⟷ poincare_between u 0⇩h v"
using ‹u ∈ unit_disc› ‹v ∈ unit_disc›
using unit_disc_fix_moebius_preserve_poincare_between unit_disc_fix_rotation zero_in_unit_disc
by fastforce
thus "?P u v"
using 1 2[rule_format, of "?M u"] 3
using inf_or_of_complex[of u] inf_or_of_complex[of v]
by auto
qed
next
fix x
assume 1: "is_real x" "0 < Re x" "Re x < 1"
hence "x ≠ 0"
by auto
show "?P' (of_complex x)"
proof (rule allI, rule impI, (erule conjE)+)
fix u
assume 2: "u ∈ unit_disc" "u ≠ 0⇩h"
then obtain u' where "u = of_complex u'"
using inf_or_of_complex[of u]
by auto
show "?P u (of_complex x)"
using 1 2 ‹x ≠ 0› ‹u = of_complex u'›
using poincare_between_rev[of u "0⇩h" "of_complex x"]
using poincare_between_x_axis_u0v[of x u'] ‹is_real x›
apply (auto simp add: cmod_eq_Re)
apply (rule_tac x="Re u' / Re x" in exI, simp add: divide_neg_pos algebra_split_simps)
using mult_neg_pos mult_pos_neg
by blast
qed
qed fact+
thus ?thesis
using assms
by auto
qed
lemma poincare_between_u0v_polar_form:
assumes "x ∈ unit_disc" and "y ∈ unit_disc" and "x ≠ 0⇩h" and "y ≠ 0⇩h" and
"to_complex x = cor rx * cis φ" "to_complex y = cor ry * cis φ"
shows "poincare_between x 0⇩h y ⟷ rx * ry < 0" (is "?P x y rx ry")
proof-
from assms have "rx ≠ 0" "ry ≠ 0"
using inf_or_of_complex[of x] inf_or_of_complex[of y]
by auto
have "(∃k<0. cor rx = cor k * cor ry ) = (rx * ry < 0)"
proof
assume "∃k<0. cor rx = cor k * cor ry"
then obtain k where "k < 0" "cor rx = cor k * cor ry"
by auto
hence "rx = k * ry"
using of_real_eq_iff
by fastforce
thus "rx * ry < 0"
using ‹k < 0› ‹rx ≠ 0› ‹ry ≠ 0›
by (smt (z3) divisors_zero mult_nonneg_nonpos mult_nonpos_nonpos zero_less_mult_pos2)
next
assume "rx * ry < 0"
hence "rx = (rx/ry)*ry" "rx / ry < 0"
using ‹rx ≠ 0› ‹ry ≠ 0›
by (auto simp add: divide_less_0_iff algebra_split_simps)
thus "∃k<0. cor rx = cor k * cor ry"
using ‹rx ≠ 0› ‹ry ≠ 0›
by (rule_tac x="rx / ry" in exI, simp)
qed
thus ?thesis
using assms
using poincare_between_u0v[OF assms(1-4)]
by auto
qed
lemma poincare_between_x_axis_0uv:
fixes x y :: real
assumes "-1 < x" and "x < 1" and "x ≠ 0"
assumes "-1 < y" and "y < 1" and "y ≠ 0"
shows "poincare_between 0⇩h (of_complex x) (of_complex y) ⟷
(x < 0 ∧ y < 0 ∧ y ≤ x) ∨ (x > 0 ∧ y > 0 ∧ x ≤ y)" (is "?lhs ⟷ ?rhs")
proof (cases "x = y")
case True
thus ?thesis
using assms
unfolding poincare_between_def
by auto
next
case False
let ?x = "of_complex x" and ?y = "of_complex y"
have "?x ∈ unit_disc" "?y ∈ unit_disc"
using assms
by auto
have distinct: "distinct [0⇩h, ?x, ?y, inversion ?x]"
using ‹x ≠ 0› ‹y ≠ 0› ‹x ≠ y› ‹?x ∈ unit_disc› ‹?y ∈ unit_disc›
using inversion_noteq_unit_disc[of ?x ?y]
using inversion_noteq_unit_disc[of ?x ?x]
using inversion_noteq_unit_disc[of ?x "0⇩h"]
using of_complex_inj[of x y]
by (metis distinct_length_2_or_more distinct_singleton of_complex_zero_iff of_real_eq_0_iff of_real_eq_iff zero_in_unit_disc)
let ?cr = "cross_ratio 0⇩h ?x ?y (inversion ?x)"
have "Re (to_complex ?cr) = x⇧2 * (x*y - 1) / (x * (y - x))"
using ‹x ≠ 0› ‹x ≠ y›
unfolding inversion_def
by simp (transfer, transfer, auto simp add: vec_cnj_def power2_eq_square field_simps split: if_split_asm)
moreover
{
fix a b :: real
assume "b ≠ 0"
hence "a < 0 ⟷ b⇧2 * a < (0::real)"
by (metis mult.commute mult_eq_0_iff mult_neg_pos mult_pos_pos not_less_iff_gr_or_eq not_real_square_gt_zero power2_eq_square)
}
hence "x⇧2 * (x*y - 1) < 0"
using assms
by (smt (z3) minus_mult_minus mult_le_cancel_left1)
moreover
have "x * (y - x) > 0 ⟷ ?rhs"
using ‹x ≠ 0› ‹y ≠ 0› ‹x ≠ y›
by (smt (z3) mult_le_0_iff)
ultimately
have *: "Re (to_complex ?cr) < 0 ⟷ ?rhs"
by (simp add: divide_less_0_iff)
show ?thesis
proof
assume ?lhs
have "is_real (to_complex ?cr)" "Re (to_complex ?cr) < 0"
using ‹?lhs› distinct
unfolding poincare_between_def Let_def
by auto
thus ?rhs
using *
by simp
next
assume ?rhs
hence "Re (to_complex ?cr) < 0"
using *
by simp
moreover
have "{0⇩h, of_complex (cor x), of_complex (cor y), inversion (of_complex (cor x))} ⊆ circline_set x_axis"
using ‹x ≠ 0› is_real_inversion[of "cor x"]
using inf_or_of_complex[of "inversion ?x"]
by (auto simp del: inversion_of_complex)
hence "is_real (to_complex ?cr)"
using four_points_on_circline_iff_cross_ratio_real[OF distinct]
by auto
ultimately
show ?lhs
using distinct
unfolding poincare_between_def Let_def
by auto
qed
qed
lemma poincare_between_0uv:
assumes "u ∈ unit_disc" and "v ∈ unit_disc" and "u ≠ 0⇩h" and "v ≠ 0⇩h"
shows "poincare_between 0⇩h u v ⟷
(let u' = to_complex u; v' = to_complex v in Arg u' = Arg v' ∧ cmod u' ≤ cmod v')" (is "?P u v")
proof (cases "u = v")
case True
thus ?thesis
by simp
next
case False
have "∀ v. v ∈ unit_disc ∧ v ≠ 0⇩h ∧ v ≠ u ⟶ (poincare_between 0⇩h u v ⟷ (let u' = to_complex u; v' = to_complex v in Arg u' = Arg v' ∧ cmod u' ≤ cmod v'))" (is "?P' u")
proof (rule wlog_rotation_to_positive_x_axis)
show "u ∈ unit_disc" "u ≠ 0⇩h"
by fact+
next
fix x
assume *: "is_real x" "0 < Re x" "Re x < 1"
hence "of_complex x ∈ unit_disc" "of_complex x ≠ 0⇩h" "of_complex x ∈ circline_set x_axis"
unfolding circline_set_x_axis
by (auto simp add: cmod_eq_Re)
show "?P' (of_complex x)"
proof safe
fix v
assume "v ∈ unit_disc" "v ≠ 0⇩h" "v ≠ of_complex x" "poincare_between 0⇩h (of_complex x) v"
hence "v ∈ circline_set x_axis"
using poincare_between_poincare_line_uvz[of "0⇩h" "of_complex x" v]
using poincare_line_0_real_is_x_axis[of "of_complex x"]
using ‹of_complex x ≠ 0⇩h› ‹v ≠ 0⇩h› ‹v ≠ of_complex x› ‹of_complex x ∈ unit_disc› ‹of_complex x ∈ circline_set x_axis›
by auto
obtain v' where "v = of_complex v'"
using ‹v ∈ unit_disc›
using inf_or_of_complex[of v]
by auto
hence **: "v = of_complex v'" "-1 < Re v'" "Re v' < 1" "Re v' ≠ 0" "is_real v'"
using ‹v ∈ unit_disc› ‹v ≠ 0⇩h› ‹v ∈ circline_set x_axis› of_complex_inj[of v']
unfolding circline_set_x_axis
by (auto simp add: cmod_eq_Re real_imag_0)
show "let u' = to_complex (of_complex x); v' = to_complex v in Arg u' = Arg v' ∧ cmod u' ≤ cmod v'"
using poincare_between_x_axis_0uv[of "Re x" "Re v'"] * **
using ‹poincare_between 0⇩h (of_complex x) v›
using arg_complex_of_real_positive[of "Re x"] arg_complex_of_real_negative[of "Re x"]
using arg_complex_of_real_positive[of "Re v'"] arg_complex_of_real_negative[of "Re v'"]
by (auto simp add: cmod_eq_Re)
next
fix v
assume "v ∈ unit_disc" "v ≠ 0⇩h" "v ≠ of_complex x"
then obtain v' where **: "v = of_complex v'" "v' ≠ 0" "v' ≠ x"
using inf_or_of_complex[of v]
by auto blast
assume "let u' = to_complex (of_complex x); v' = to_complex v in Arg u' = Arg v' ∧ cmod u' ≤ cmod v'"
hence ***: "Re x < 0 ∧ Re v' < 0 ∧ Re v' ≤ Re x ∨ 0 < Re x ∧ 0 < Re v' ∧ Re x ≤ Re v'" "is_real v'"
using arg_pi_iff[of x] arg_pi_iff[of v']
using arg_0_iff[of x] arg_0_iff[of v']
using * **
by (smt (z3) cmod_Re_le_iff to_complex_of_complex)+
have "-1 < Re v'" "Re v' < 1" "Re v' ≠ 0" "is_real v'"
using ‹v ∈ unit_disc› ** ‹is_real v'›
by (auto simp add: cmod_eq_Re complex_eq_if_Re_eq)
thus "poincare_between 0⇩h (of_complex x) v"
using poincare_between_x_axis_0uv[of "Re x" "Re v'"] * ** ***
by simp
qed
next
fix φ u
assume "u ∈ unit_disc" "u ≠ 0⇩h"
let ?M = "moebius_rotation φ"
assume *: "?P' (moebius_pt ?M u)"
show "?P' u"
proof (rule allI, rule impI, (erule conjE)+)
fix v
assume "v ∈ unit_disc" "v ≠ 0⇩h" "v ≠ u"
have "moebius_pt ?M v ≠ moebius_pt ?M u"
using ‹v ≠ u›
by auto
obtain u' v' where "v = of_complex v'" "u = of_complex u'" "v' ≠ 0" "u' ≠ 0"
using inf_or_of_complex[of u] inf_or_of_complex[of v]
using ‹v ∈ unit_disc› ‹u ∈ unit_disc› ‹v ≠ 0⇩h› ‹u ≠ 0⇩h›
by auto
thus "?P u v"
using *[rule_format, of "moebius_pt ?M v"]
using ‹moebius_pt ?M v ≠ moebius_pt ?M u›
using unit_disc_fix_moebius_preserve_poincare_between[of ?M "0⇩h" u v]
using ‹v ∈ unit_disc› ‹u ∈ unit_disc› ‹v ≠ 0⇩h› ‹u ≠ 0⇩h›
using arg_mult_eq[of "cis φ" u' v']
by simp (auto simp add: arg_mult norm_mult)
qed
qed
thus ?thesis
using assms False
by auto
qed
lemma poincare_between_y_axis_0uv:
fixes x y :: real
assumes "-1 < x" and "x < 1" and "x ≠ 0"
assumes "-1 < y" and "y < 1" and "y ≠ 0"
shows "poincare_between 0⇩h (of_complex (𝗂 * x)) (of_complex (𝗂 * y)) ⟷
(x < 0 ∧ y < 0 ∧ y ≤ x) ∨ (x > 0 ∧ y > 0 ∧ x ≤ y)" (is "?lhs ⟷ ?rhs")
using assms
using poincare_between_0uv[of "of_complex (𝗂 * x)" "of_complex (𝗂 * y)"]
using arg_pi2_iff[of "𝗂 * cor x"] arg_pi2_iff[of "𝗂 * cor y"]
using arg_minus_pi2_iff[of "𝗂 * cor x"] arg_minus_pi2_iff[of "𝗂 * cor y"]
apply (simp add: norm_mult)
apply (smt (verit, best))
done
lemma poincare_between_x_axis_uvw:
fixes x y z :: real
assumes "-1 < x" and "x < 1"
assumes "-1 < y" and "y < 1" and "y ≠ x"
assumes "-1 < z" and "z < 1" and "z ≠ x"
shows "poincare_between (of_complex x) (of_complex y) (of_complex z) ⟷
(y < x ∧ z < x ∧ z ≤ y) ∨ (y > x ∧ z > x ∧ y ≤ z)" (is "?lhs ⟷ ?rhs")
proof (cases "x = 0 ∨ y = 0 ∨ z = 0")
case True
thus ?thesis
proof (cases "x = 0")
case True
thus ?thesis
using poincare_between_x_axis_0uv assms
by simp
next
case False
show ?thesis
proof (cases "z = 0")
case True
thus ?thesis
using poincare_between_x_axis_0uv assms poincare_between_rev
by (smt (z3) norm_of_real of_complex_zero of_real_0 poincare_between_nonstrict(2) unit_disc_iff_cmod_lt_1)
next
case False
have "y = 0"
using ‹x ≠ 0› ‹z ≠ 0› ‹x = 0 ∨ y = 0 ∨ z = 0›
by simp
have "poincare_between (of_complex x) 0⇩h (of_complex z) = (is_real z ∧ x * z < 0)"
using ‹x ≠ 0› ‹z ≠ 0› poincare_between_x_axis_u0v
by auto
moreover
have "x * z < 0 ⟷ ?rhs"
using True ‹x ≠ 0› ‹z ≠ 0›
by (smt (z3) zero_le_mult_iff)
ultimately
show ?thesis
using ‹y = 0›
by auto
qed
qed
next
case False
thus ?thesis
proof (cases "z = y")
case True
thus ?thesis
using assms
unfolding poincare_between_def
by auto
next
case False
let ?x = "of_complex x" and ?y = "of_complex y" and ?z = "of_complex z"
have "?x ∈ unit_disc" "?y ∈ unit_disc" "?z ∈ unit_disc"
using assms
by auto
have distinct: "distinct [?x, ?y, ?z, inversion ?y]"
using ‹y ≠ x› ‹z ≠ x› False ‹?x ∈ unit_disc› ‹?y ∈ unit_disc› ‹?z ∈ unit_disc›
using inversion_noteq_unit_disc[of ?y ?y]
using inversion_noteq_unit_disc[of ?y ?x]
using inversion_noteq_unit_disc[of ?y ?z]
using of_complex_inj[of x y] of_complex_inj[of y z] of_complex_inj[of x z]
by auto
have "cor y * cor x ≠ 1"
using assms
by (smt (z3) minus_mult_minus mult_less_cancel_left2 mult_less_cancel_right2 of_real_1 of_real_eq_iff of_real_mult)
let ?cr = "cross_ratio ?x ?y ?z (inversion ?y)"
have "Re (to_complex ?cr) = (x - y) * (z*y - 1)/ ((x*y - 1)*(z - y))"
proof-
have " ⋀y x z. ⟦y ≠ x; z ≠ x; z ≠ y; cor y * cor x ≠ 1; x ≠ 0; y ≠ 0; z ≠ 0⟧ ⟹
(y * y + y * (y * (x * z)) - (y * x + y * (y * (y * z)))) /
(y * y + y * (y * (x * z)) - (y * z + y * (y * (y * x)))) =
(y + y * (x * z) - (x + y * (y * z))) / (y + y * (x * z) - (z + y * (y * x)))"
by (metis (no_types, opaque_lifting) ab_group_add_class.ab_diff_conv_add_uminus distrib_left mult_divide_mult_cancel_left_if mult_minus_right)
thus ?thesis
using ‹y ≠ x› ‹z ≠ x› False ‹¬ (x = 0 ∨ y = 0 ∨ z = 0)›
using ‹cor y * cor x ≠ 1›
unfolding inversion_def
by (transfer, transfer, auto simp add: vec_cnj_def power2_eq_square field_simps split: if_split_asm)
qed
moreover
have "(x*y - 1) < 0"
using assms
by (smt (z3) minus_mult_minus mult_less_cancel_right2 zero_less_mult_iff)
moreover
have "(z*y - 1) < 0"
using assms
by (smt (z3) minus_mult_minus mult_less_cancel_right2 zero_less_mult_iff)
moreover
have "(x - y) / (z - y) < 0 ⟷ ?rhs"
using ‹y ≠ x› ‹z ≠ x› False ‹¬ (x = 0 ∨ y = 0 ∨ z = 0)›
by (smt (z3) divide_less_cancel divide_nonneg_nonpos divide_nonneg_pos divide_nonpos_nonneg divide_nonpos_nonpos)
ultimately
have *: "Re (to_complex ?cr) < 0 ⟷ ?rhs"
by (smt (z3) algebra_split_simps(24) minus_divide_left zero_less_divide_iff zero_less_mult_iff)
show ?thesis
proof
assume ?lhs
have "is_real (to_complex ?cr)" "Re (to_complex ?cr) < 0"
using ‹?lhs› distinct
unfolding poincare_between_def Let_def
by auto
thus ?rhs
using *
by simp
next
assume ?rhs
hence "Re (to_complex ?cr) < 0"
using *
by simp
moreover
have "{of_complex (cor x), of_complex (cor y), of_complex (cor z), inversion (of_complex (cor y))} ⊆ circline_set x_axis"
using ‹¬ (x = 0 ∨ y = 0 ∨ z = 0)› is_real_inversion[of "cor y"]
using inf_or_of_complex[of "inversion ?y"]
by (auto simp del: inversion_of_complex)
hence "is_real (to_complex ?cr)"
using four_points_on_circline_iff_cross_ratio_real[OF distinct]
by auto
ultimately
show ?lhs
using distinct
unfolding poincare_between_def Let_def
by auto
qed
qed
qed
subsubsection ‹H-betweenness and h-collinearity›
text‹For three h-collinear points at least one of the three possible h-betweeness relations must
hold.›
lemma poincare_collinear3_between:
assumes "u ∈ unit_disc" and "v ∈ unit_disc" and "w ∈ unit_disc"
assumes "poincare_collinear {u, v, w}"
shows "poincare_between u v w ∨ poincare_between u w v ∨ poincare_between v u w" (is "?P' u v w")
proof (cases "u=v")
case True
thus ?thesis
using assms
by auto
next
case False
have "∀ w. w ∈ unit_disc ∧ poincare_collinear {u, v, w} ⟶ ?P' u v w" (is "?P u v")
proof (rule wlog_positive_x_axis[where P="?P"])
fix x
assume x: "is_real x" "0 < Re x" "Re x < 1"
hence "x ≠ 0"
using complex.expand[of x 0]
by auto
hence *: "poincare_line 0⇩h (of_complex x) = x_axis"
using x poincare_line_0_real_is_x_axis[of "of_complex x"]
unfolding circline_set_x_axis
by auto
have "of_complex x ∈ unit_disc"
using x
by (auto simp add: cmod_eq_Re)
have "of_complex x ≠ 0⇩h"
using ‹x ≠ 0›
by auto
show "?P 0⇩h (of_complex x)"
proof safe
fix w
assume "w ∈ unit_disc"
assume "poincare_collinear {0⇩h, of_complex x, w}"
hence "w ∈ circline_set x_axis"
using * unique_poincare_line[of "0⇩h" "of_complex x"] ‹of_complex x ∈ unit_disc› ‹x ≠ 0› ‹of_complex x ≠ 0⇩h›
unfolding poincare_collinear_def
by auto
then obtain w' where w': "w = of_complex w'" "is_real w'"
using ‹w ∈ unit_disc›
using inf_or_of_complex[of w]
unfolding circline_set_x_axis
by auto
hence "-1 < Re w'" "Re w' < 1"
using ‹w ∈ unit_disc›
by (auto simp add: cmod_eq_Re)
assume 1: "¬ poincare_between (of_complex x) 0⇩h w"
hence "w ≠ 0⇩h" "w' ≠ 0"
using w'
unfolding poincare_between_def
by auto
hence "Re w' ≠ 0"
using w' complex.expand[of w' 0]
by auto
have "Re w' ≥ 0"
using 1 poincare_between_x_axis_u0v[of x w'] ‹Re x > 0› ‹is_real x› ‹x ≠ 0› ‹w' ≠ 0› w'
using mult_pos_neg
by force
moreover
assume "¬ poincare_between 0⇩h (of_complex x) w"
hence "Re w' < Re x"
using poincare_between_x_axis_0uv[of "Re x" "Re w'"]
using w' x ‹-1 < Re w'› ‹Re w' < 1› ‹Re w' ≠ 0›
by auto
ultimately
show "poincare_between 0⇩h w (of_complex x)"
using poincare_between_x_axis_0uv[of "Re w'" "Re x"]
using w' x ‹-1 < Re w'› ‹Re w' < 1› ‹Re w' ≠ 0›
by auto
qed
next
show "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
by fact+
next
fix M u v
assume 1: "unit_disc_fix M" "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
let ?Mu = "moebius_pt M u" and ?Mv = "moebius_pt M v"
assume 2: "?P ?Mu ?Mv"
show "?P u v"
proof safe
fix w
assume "w ∈ unit_disc" "poincare_collinear {u, v, w}" "¬ poincare_between u v w" "¬ poincare_between v u w"
thus "poincare_between u w v"
using 1 2[rule_format, of "moebius_pt M w"]
by simp
qed
qed
thus ?thesis
using assms
by simp
qed
lemma poincare_collinear3_iff:
assumes "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc"
shows "poincare_collinear {u, v, w} ⟷ poincare_between u v w ∨ poincare_between v u w ∨ poincare_between v w u"
using assms
by (metis poincare_collinear3_between insert_commute poincare_between_poincare_collinear poincare_between_rev)
subsection ‹Some properties of betweenness›
lemma poincare_between_transitivity:
assumes "a ∈ unit_disc" and "x ∈ unit_disc" and "b ∈ unit_disc" and "y ∈ unit_disc" and
"poincare_between a x b" and "poincare_between a b y"
shows "poincare_between x b y"
proof(cases "a = b")
case True
thus ?thesis
using assms
using poincare_between_sandwich by blast
next
case False
have "∀ x. ∀ y. poincare_between a x b ∧ poincare_between a b y ∧ x ∈ unit_disc
∧ y ∈ unit_disc ⟶ poincare_between x b y" (is "?P a b")
proof (rule wlog_positive_x_axis[where P="?P"])
show "a ∈ unit_disc"
using assms by simp
next
show "b ∈ unit_disc"
using assms by simp
next
show "a ≠ b"
using False by simp
next
fix M u v
assume *: "unit_disc_fix M" "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
"∀x y. poincare_between (moebius_pt M u) x (moebius_pt M v) ∧
poincare_between (moebius_pt M u) (moebius_pt M v) y ∧
x ∈ unit_disc ∧ y ∈ unit_disc ⟶
poincare_between x (moebius_pt M v) y"
show "∀x y. poincare_between u x v ∧ poincare_between u v y ∧ x ∈ unit_disc ∧ y ∈ unit_disc
⟶ poincare_between x v y"
proof safe
fix x y
assume "poincare_between u x v" "poincare_between u v y" " x ∈ unit_disc" "y ∈ unit_disc"
have "poincare_between (moebius_pt M u) (moebius_pt M x) (moebius_pt M v)"
using ‹poincare_between u x v› ‹unit_disc_fix M› ‹x ∈ unit_disc› ‹u ∈ unit_disc› ‹v ∈ unit_disc›
by simp
moreover
have "poincare_between (moebius_pt M u) (moebius_pt M v) (moebius_pt M y)"
using ‹poincare_between u v y› ‹unit_disc_fix M› ‹y ∈ unit_disc› ‹u ∈ unit_disc› ‹v ∈ unit_disc›
by simp
moreover
have "(moebius_pt M x) ∈ unit_disc"
using ‹unit_disc_fix M› ‹x ∈ unit_disc› by simp
moreover
have "(moebius_pt M y) ∈ unit_disc"
using ‹unit_disc_fix M› ‹y ∈ unit_disc› by simp
ultimately
have "poincare_between (moebius_pt M x) (moebius_pt M v) (moebius_pt M y)"
using * by blast
thus "poincare_between x v y"
using ‹y ∈ unit_disc› * ‹x ∈ unit_disc› by simp
qed
next
fix x
assume xx: "is_real x" "0 < Re x" "Re x < 1"
hence "of_complex x ∈ unit_disc"
using cmod_eq_Re by auto
hence "of_complex x ≠ ∞⇩h"
by simp
have " of_complex x ≠ 0⇩h"
using xx by auto
have "of_complex x ∈ circline_set x_axis"
using xx by simp
show "∀m n. poincare_between 0⇩h m (of_complex x) ∧ poincare_between 0⇩h (of_complex x) n ∧
m ∈ unit_disc ∧ n ∈ unit_disc ⟶ poincare_between m (of_complex x) n"
proof safe
fix m n
assume **: "poincare_between 0⇩h m (of_complex x)" "poincare_between 0⇩h (of_complex x) n"
"m ∈ unit_disc" " n ∈ unit_disc"
show "poincare_between m (of_complex x) n"
proof(cases "m = 0⇩h")
case True
thus ?thesis
using ** by auto
next
case False
hence "m ∈ circline_set x_axis"
using poincare_between_poincare_line_uzv[of "0⇩h" "of_complex x" m]
using poincare_line_0_real_is_x_axis[of "of_complex x"]
using ‹of_complex x ∈ unit_disc› ‹of_complex x ≠ ∞⇩h› ‹of_complex x ≠ 0⇩h›
using ‹of_complex x ∈ circline_set x_axis› ‹m ∈ unit_disc› **(1)
by simp
then obtain m' where "m = of_complex m'" "is_real m'"
using inf_or_of_complex[of m] ‹m ∈ unit_disc›
unfolding circline_set_x_axis
by auto
hence "Re m' ≤ Re x"
using ‹poincare_between 0⇩h m (of_complex x)› xx ‹of_complex x ≠ 0⇩h›
using False ** ‹of_complex x ∈ unit_disc›
using cmod_Re_le_iff poincare_between_0uv by auto
have "n ≠ 0⇩h"
using **(2, 4) ‹of_complex x ≠ 0⇩h› ‹of_complex x ∈ unit_disc›
using poincare_between_sandwich by fastforce
have "n ∈ circline_set x_axis"
using poincare_between_poincare_line_uvz[of "0⇩h" "of_complex x" n]
using poincare_line_0_real_is_x_axis[of "of_complex x"]
using ‹of_complex x ∈ unit_disc› ‹of_complex x ≠ ∞⇩h› ‹of_complex x ≠ 0⇩h›
using ‹of_complex x ∈ circline_set x_axis› ‹n ∈ unit_disc› **(2)
by simp
then obtain n' where "n = of_complex n'" "is_real n'"
using inf_or_of_complex[of n] ‹n ∈ unit_disc›
unfolding circline_set_x_axis
by auto
hence "Re x ≤ Re n'"
using ‹poincare_between 0⇩h (of_complex x) n› xx ‹of_complex x ≠ 0⇩h›
using False ** ‹of_complex x ∈ unit_disc› ‹n ≠ 0⇩h›
using cmod_Re_le_iff poincare_between_0uv
by (metis Re_complex_of_real arg_0_iff rcis_cmod_Arg rcis_zero_arg to_complex_of_complex)
have "poincare_between (of_complex m') (of_complex x) (of_complex n')"
using ‹Re x ≤ Re n'› ‹Re m' ≤ Re x›
using poincare_between_x_axis_uvw[of "Re m'" "Re x" "Re n'"]
using ‹is_real n'› ‹is_real m'› ‹n ∈ unit_disc› ‹n = of_complex n'›
using xx ‹m = of_complex m'› ‹m ∈ unit_disc›
by (smt (z3) complex_of_real_Re norm_of_real poincare_between_def unit_disc_iff_cmod_lt_1)
thus ?thesis
using ‹n = of_complex n'› ‹m = of_complex m'›
by auto
qed
qed
qed
thus ?thesis
using assms
by blast
qed
subsection‹Poincare between - sum distances›
text‹Another possible definition of the h-betweenness relation is given in terms of h-distances
between pairs of points. We prove it as a characterization equivalent to our cross-ratio based
definition.›
lemma poincare_between_sum_distances_x_axis_u0v:
assumes "of_complex u' ∈ unit_disc" "of_complex v' ∈ unit_disc"
assumes "is_real u'" "u' ≠ 0" "v' ≠ 0"
shows "poincare_distance (of_complex u') 0⇩h + poincare_distance 0⇩h (of_complex v') = poincare_distance (of_complex u') (of_complex v') ⟷
is_real v' ∧ Re u' * Re v' < 0" (is "?P u' v' ⟷ ?Q u' v'")
proof-
have "Re u' ≠ 0"
using ‹is_real u'› ‹u' ≠ 0›
using complex_eq_if_Re_eq
by simp
let ?u = "cmod u'" and ?v = "cmod v'" and ?uv = "cmod (u' - v')"
have disc: "?u⇧2 < 1" "?v⇧2 < 1"
using unit_disc_cmod_square_lt_1[OF assms(1)]
using unit_disc_cmod_square_lt_1[OF assms(2)]
by auto
have "poincare_distance (of_complex u') 0⇩h + poincare_distance 0⇩h (of_complex v') =
arcosh (((1 + ?u⇧2) * (1 + ?v⇧2) + 4 * ?u * ?v) / ((1 - ?u⇧2) * (1 - ?v⇧2)))" (is "_ = arcosh ?r1")
using poincare_distance_formula_zero_sum[OF assms(1-2)]
by (simp add: Let_def)
moreover
have "poincare_distance (of_complex u') (of_complex v') =
arcosh (((1 - ?u⇧2) * (1 - ?v⇧2) + 2 * ?uv⇧2) / ((1 - ?u⇧2) * (1 - ?v⇧2)))" (is "_ = arcosh ?r2")
using disc
using poincare_distance_formula[OF assms(1-2)]
by (subst add_divide_distrib) simp
moreover
have "arcosh ?r1 = arcosh ?r2 ⟷ ?Q u' v'"
proof
assume "arcosh ?r1 = arcosh ?r2"
hence "?r1 = ?r2"
proof (subst (asm) arcosh_eq_iff)
show "?r1 ≥ 1"
proof-
have "(1 - ?u⇧2) * (1 - ?v⇧2) ≤ (1 + ?u⇧2) * (1 + ?v⇧2) + 4 * ?u * ?v"
by (simp add: field_simps)
thus ?thesis
using disc
by simp
qed
next
show "?r2 ≥ 1"
using disc
by simp
qed
hence "(1 + ?u⇧2) * (1 + ?v⇧2) + 4 * ?u * ?v = (1 - ?u⇧2) * (1 - ?v⇧2) + 2 * ?uv⇧2"
using disc
by auto
hence "(cmod (u' - v'))⇧2 = (cmod u' + cmod v')⇧2"
by (simp add: field_simps power2_eq_square)
hence *: "Re u' * Re v' + ¦Re u'¦ * sqrt ((Im v')⇧2 + (Re v')⇧2) = 0"
using ‹is_real u'›
unfolding cmod_power2 cmod_def
by (simp add: field_simps) (simp add: power2_eq_square field_simps)
hence "sqrt ((Im v')⇧2 + (Re v')⇧2) = ¦Re v'¦"
using ‹Re u' ≠ 0› ‹v' ≠ 0›
by (smt (z3) complex_neq_0 mult.commute mult_cancel_right mult_minus_left real_sqrt_gt_0_iff)
hence "Im v' = 0"
by (smt (z3) Im_eq_0 norm_complex_def)
moreover
hence "Re u' * Re v' = - ¦Re u'¦ * ¦Re v'¦"
using *
by simp
hence "Re u' * Re v' < 0"
using ‹Re u' ≠ 0› ‹v' ≠ 0›
by (simp add: ‹is_real v'› complex_eq_if_Re_eq)
ultimately
show "?Q u' v'"
by simp
next
assume "?Q u' v'"
hence "is_real v'" "Re u' * Re v' < 0"
by auto
have "?r1 = ?r2"
proof (cases "Re u' > 0")
case True
hence "Re v' < 0"
using ‹Re u' * Re v' < 0›
by (smt (z3) zero_le_mult_iff)
show ?thesis
using disc ‹is_real u'› ‹is_real v'›
using ‹Re u' > 0› ‹Re v' < 0›
unfolding cmod_power2 cmod_def
by simp (simp add: power2_eq_square field_simps)
next
case False
hence "Re u' < 0"
using ‹Re u' ≠ 0›
by simp
hence "Re v' > 0"
using ‹Re u' * Re v' < 0›
by (smt (z3) zero_le_mult_iff)
show ?thesis
using disc ‹is_real u'› ‹is_real v'›
using ‹Re u' < 0› ‹Re v' > 0›
unfolding cmod_power2 cmod_def
by simp (simp add: power2_eq_square field_simps)
qed
thus "arcosh ?r1 = arcosh ?r2"
by metis
qed
ultimately
show ?thesis
by simp
qed
text‹
Different proof of the previous theorem relying on the cross-ratio definition, and not the distance formula.
We suppose that this could be also used to prove the triangle inequality.
›
lemma poincare_between_sum_distances_x_axis_u0v_different_proof:
assumes "of_complex u' ∈ unit_disc" "of_complex v' ∈ unit_disc"
assumes "is_real u'" "u' ≠ 0" "v' ≠ 0" "is_real v'"
shows "poincare_distance (of_complex u') 0⇩h + poincare_distance 0⇩h (of_complex v') = poincare_distance (of_complex u') (of_complex v') ⟷
Re u' * Re v' < 0" (is "?P u' v' ⟷ ?Q u' v'")
proof-
have "-1 < Re u'" "Re u' < 1" "Re u' ≠ 0"
using assms
by (auto simp add: cmod_eq_Re complex_eq_if_Re_eq)
have "-1 < Re v'" "Re v' < 1" "Re v' ≠ 0"
using assms
by (auto simp add: cmod_eq_Re complex_eq_if_Re_eq)
have "¦ln (Re ((1 - u') / (1 + u')))¦ + ¦ln (Re ((1 - v') / (1 + v')))¦ =
¦ln (Re ((1 + u') * (1 - v') / ((1 - u') * (1 + v'))))¦ ⟷ Re u' * Re v' < 0" (is "¦ln ?a1¦ + ¦ln ?a2¦ = ¦ln ?a3¦ ⟷ _")
proof-
have 1: "0 < ?a1" "ln ?a1 > 0 ⟷ Re u' < 0"
using ‹Re u' < 1› ‹Re u' > -1› ‹is_real u'›
using complex_is_Real_iff
by auto
have 2: "0 < ?a2" "ln ?a2 > 0 ⟷ Re v' < 0"
using ‹Re v' < 1› ‹Re v' > -1› ‹is_real v'›
using complex_is_Real_iff
by auto
have 3: "0 < ?a3" "ln ?a3 > 0 ⟷ Re v' < Re u'"
using ‹Re u' < 1› ‹Re u' > -1› ‹is_real u'›
using ‹Re v' < 1› ‹Re v' > -1› ‹is_real v'›
using complex_is_Real_iff
by auto (simp add: field_simps)+
show ?thesis
proof
assume *: "Re u' * Re v' < 0"
show "¦ln ?a1¦ + ¦ln ?a2¦ = ¦ln ?a3¦"
proof (cases "Re u' > 0")
case True
hence "Re v' < 0"
using *
by (smt (z3) mult_nonneg_nonneg)
show ?thesis
using 1 2 3 ‹Re u' > 0› ‹Re v' < 0›
using ‹Re u' < 1› ‹Re u' > -1› ‹is_real u'›
using ‹Re v' < 1› ‹Re v' > -1› ‹is_real v'›
using complex_is_Real_iff
using ln_div ln_mult
by simp
next
case False
hence "Re v' > 0" "Re u' < 0"
using *
by (smt (z3) zero_le_mult_iff)+
show ?thesis
using 1 2 3 ‹Re u' < 0› ‹Re v' > 0›
using ‹Re u' < 1› ‹Re u' > -1› ‹is_real u'›
using ‹Re v' < 1› ‹Re v' > -1› ‹is_real v'›
using complex_is_Real_iff
using ln_div ln_mult
by simp
qed
next
assume *: "¦ln ?a1¦ + ¦ln ?a2¦ = ¦ln ?a3¦"
{
assume "Re u' > 0" "Re v' > 0"
hence False
using * 1 2 3
using ‹Re u' < 1› ‹Re u' > -1› ‹is_real u'›
using ‹Re v' < 1› ‹Re v' > -1› ‹is_real v'›
using complex_is_Real_iff
using ln_mult ln_div
by (cases "Re v' < Re u'") auto
}
moreover
{
assume "Re u' < 0" "Re v' < 0"
hence False
using * 1 2 3
using ‹Re u' < 1› ‹Re u' > -1› ‹is_real u'›
using ‹Re v' < 1› ‹Re v' > -1› ‹is_real v'›
using complex_is_Real_iff
using ln_mult ln_div
by (cases "Re v' < Re u'") auto
}
ultimately
show "Re u' * Re v' < 0"
using ‹Re u' ≠ 0› ‹Re v' ≠ 0›
by (smt (z3) divisors_zero mult_le_0_iff)
qed
qed
thus ?thesis
using assms
apply (subst poincare_distance_sym, simp, simp)
apply (subst poincare_distance_zero_x_axis, simp, simp add: circline_set_x_axis)
apply (subst poincare_distance_zero_x_axis, simp, simp add: circline_set_x_axis)
apply (subst poincare_distance_x_axis_x_axis, simp, simp, simp add: circline_set_x_axis, simp add: circline_set_x_axis)
apply simp
done
qed
lemma poincare_between_sum_distances:
assumes "u ∈ unit_disc" and "v ∈ unit_disc" and "w ∈ unit_disc"
shows "poincare_between u v w ⟷
poincare_distance u v + poincare_distance v w = poincare_distance u w" (is "?P' u v w")
proof (cases "u = v")
case True
thus ?thesis
using assms
by simp
next
case False
have "∀ w. w ∈ unit_disc ⟶ (poincare_between u v w ⟷ poincare_distance u v + poincare_distance v w = poincare_distance u w)" (is "?P u v")
proof (rule wlog_positive_x_axis)
fix x
assume "is_real x" "0 < Re x" "Re x < 1"
have "of_complex x ∈ circline_set x_axis"
using ‹is_real x›
by (auto simp add: circline_set_x_axis)
have "of_complex x ∈ unit_disc"
using ‹is_real x› ‹0 < Re x› ‹Re x < 1›
by (simp add: cmod_eq_Re)
have "x ≠ 0"
using ‹is_real x› ‹Re x > 0›
by auto
show "?P (of_complex x) 0⇩h"
proof (rule allI, rule impI)
fix w
assume "w ∈ unit_disc"
then obtain w' where "w = of_complex w'"
using inf_or_of_complex[of w]
by auto
show "?P' (of_complex x) 0⇩h w"
proof (cases "w = 0⇩h")
case True
thus ?thesis
by simp
next
case False
hence "w' ≠ 0"
using ‹w = of_complex w'›
by auto
show ?thesis
using ‹is_real x› ‹x ≠ 0› ‹w = of_complex w'› ‹w' ≠ 0›
using ‹of_complex x ∈ unit_disc› ‹w ∈ unit_disc›
apply simp
apply (subst poincare_between_x_axis_u0v, simp_all)
apply (subst poincare_between_sum_distances_x_axis_u0v, simp_all)
done
qed
qed
next
show "v ∈ unit_disc" "u ∈ unit_disc"
using assms
by auto
next
show "v ≠ u"
using ‹u ≠ v›
by simp
next
fix M u v
assume *: "unit_disc_fix M" "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v" and
**: "?P (moebius_pt M v) (moebius_pt M u)"
show "?P v u"
proof (rule allI, rule impI)
fix w
assume "w ∈ unit_disc"
hence "moebius_pt M w ∈ unit_disc"
using ‹unit_disc_fix M›
by auto
thus "?P' v u w"
using ‹u ∈ unit_disc› ‹v ∈ unit_disc› ‹w ∈ unit_disc› ‹unit_disc_fix M›
using **[rule_format, of "moebius_pt M w"]
by auto
qed
qed
thus ?thesis
using assms
by simp
qed
subsection ‹Some more properties of h-betweenness.›
text ‹Some lemmas proved earlier are proved almost directly using the sum of distances characterization.›
lemma unit_disc_fix_moebius_preserve_poincare_between':
assumes "unit_disc_fix M" and "u ∈ unit_disc" and "v ∈ unit_disc" and "w ∈ unit_disc"
shows "poincare_between (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) ⟷
poincare_between u v w"
using assms
using poincare_between_sum_distances
by simp
lemma conjugate_preserve_poincare_between':
assumes "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc"
shows "poincare_between (conjugate u) (conjugate v) (conjugate w) ⟷ poincare_between u v w"
using assms
using poincare_between_sum_distances
by simp
text ‹There is a unique point on a ray on the given distance from the given starting point›
lemma unique_poincare_distance_on_ray:
assumes "d ≥ 0" "u ≠ v" "u ∈ unit_disc" "v ∈ unit_disc"
assumes "y ∈ unit_disc" "poincare_distance u y = d" "poincare_between u v y"
assumes "z ∈ unit_disc" "poincare_distance u z = d" "poincare_between u v z"
shows "y = z"
proof-
have "∀ d y z. d ≥ 0 ∧
y ∈ unit_disc ∧ poincare_distance u y = d ∧ poincare_between u v y ∧
z ∈ unit_disc ∧ poincare_distance u z = d ∧ poincare_between u v z ⟶ y = z" (is "?P u v")
proof (rule wlog_positive_x_axis[where P="?P"])
fix x
assume x: "is_real x" "0 < Re x" "Re x < 1"
hence "x ≠ 0"
using complex.expand[of x 0]
by auto
hence *: "poincare_line 0⇩h (of_complex x) = x_axis"
using x poincare_line_0_real_is_x_axis[of "of_complex x"]
unfolding circline_set_x_axis
by auto
have "of_complex x ∈ unit_disc"
using x
by (auto simp add: cmod_eq_Re)
have "Arg x = 0"
using x
using arg_0_iff by blast
show "?P 0⇩h (of_complex x)"
proof safe
fix y z
assume "y ∈ unit_disc" "z ∈ unit_disc"
then obtain y' z' where yz: "y = of_complex y'" "z = of_complex z'"
using inf_or_of_complex[of y] inf_or_of_complex[of z]
by auto
assume betw: "poincare_between 0⇩h (of_complex x) y" "poincare_between 0⇩h (of_complex x) z"
hence "y ≠ 0⇩h" "z ≠ 0⇩h"
using ‹x ≠ 0› ‹of_complex x ∈ unit_disc› ‹y ∈ unit_disc›
using poincare_between_sandwich[of "0⇩h" "of_complex x"]
using of_complex_zero_iff[of x]
by force+
hence "Arg y' = 0" "cmod y' ≥ cmod x" "Arg z' = 0" "cmod z' ≥ cmod x"
using poincare_between_0uv[of "of_complex x" y] poincare_between_0uv[of "of_complex x" z]
using ‹of_complex x ∈ unit_disc› ‹x ≠ 0› ‹Arg x = 0› ‹y ∈ unit_disc› ‹z ∈ unit_disc› betw yz
by (simp_all add: Let_def)
hence *: "is_real y'" "is_real z'" "Re y' > 0" "Re z' > 0"
using arg_0_iff[of y'] arg_0_iff[of z'] x ‹y ≠ 0⇩h› ‹z ≠ 0⇩h› yz
by auto
assume "poincare_distance 0⇩h z = poincare_distance 0⇩h y" "0 ≤ poincare_distance 0⇩h y"
thus "y = z"
using * yz ‹y ∈ unit_disc› ‹z ∈ unit_disc›
using unique_x_axis_poincare_distance_positive[of "poincare_distance 0⇩h y"]
by (auto simp add: cmod_eq_Re unit_disc_to_complex_inj)
qed
next
show "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
by fact+
next
fix M u v
assume *: "unit_disc_fix M" "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
assume **: "?P (moebius_pt M u) (moebius_pt M v)"
show "?P u v"
proof safe
fix d y z
assume ***: "0 ≤ poincare_distance u y"
"y ∈ unit_disc" "poincare_between u v y"
"z ∈ unit_disc" "poincare_between u v z"
"poincare_distance u z = poincare_distance u y"
let ?Mu = "moebius_pt M u" and ?Mv = "moebius_pt M v" and ?My = "moebius_pt M y" and ?Mz = "moebius_pt M z"
have "?Mu ∈ unit_disc" "?Mv ∈ unit_disc" "?My ∈ unit_disc" "?Mz ∈ unit_disc"
using ‹u ∈ unit_disc› ‹v ∈ unit_disc› ‹y ∈ unit_disc› ‹z ∈ unit_disc›
using ‹unit_disc_fix M›
by auto
hence "?My = ?Mz"
using * ***
using **[rule_format, of "poincare_distance ?Mu ?My" ?My ?Mz]
by simp
thus "y = z"
using bij_moebius_pt[of M]
unfolding bij_def inj_on_def
by blast
qed
qed
thus ?thesis
using assms
by auto
qed
end