None le.I.7.11.ii
Open In Colab Open In Colab Open In Colab Code Ocean

Google CoLab software installation

Lemma: the length from the cycle with a focus at one point.

Lemma I.7.11.ii [1] $ \newcommand{\scalar}[3][]{\left\langle #2,#3 \right\rangle_{#1}} \newcommand{\Space}[3][]{\mathbb{#2}^{#3}_{#1}} \newcommand{\Space}[3][]{\mathbb{#2}^{#3}_{#1}} \newcommand{\cycle}[3][]{{#1 C^{#2}_{#3}}} \newcommand{\realline}[3][]{#1 R^{#2}_{#3}} \newcommand{\bs}{\breve{\sigma}} \newcommand{\zcycle}[3][]{#1 Z^{#2}_{#3}} \newcommand{\SL}[1][2]{\mathrm{SL}_{#1}(\Space{R}{})} \newcommand{\rs}{\sigma_r} \newcommand{\lvec}[1]{\overrightarrow{#1}} \newcommand{\rmi}{\mathrm{i}} \newcommand{\alli}{\iota} \newcommand{\rme}{\mathrm{e}} \newcommand{\rmd}{\mathrm{d}} \newcommand{\rmh}{\mathrm{j}} \newcommand{\rmp}{\varepsilon} \newcommand{\modulus}[2][]{\left| #2 \right|_{#1}} \newcommand{\sperp}{⋋} $ For two points $P=u+\alli v$, $P'=u'+\alli v'\in\Space[\sigma]{R}{}$, The $\bs$-length from the $\rs$-focus between $P$ and $P'$ is \begin{equation} l_{f_{\bs}}^2(\lvec{PP'}) = (\rs-\bs) p^2-2vp, \end{equation} where: \begin{equation} p = \rs\left(-(v'-v)\pm\sqrt{\rs(u'-u)^2+(v'-v)^2-\sigma\rs v'^2}\right),\quad\text{if } \rs\neq0 \end{equation} \begin{equation} p = \frac{(u'-u)^2-\sigma v'^2}{2(v'-v)}, \quad\text{if } \rs=0. \end{equation}

Proof. To use the linear solver in \GiNaC\ we need to replace the condition C10.focus().op(1) == v by hand-made value for the parameter n.

There are two suitable values of n which correspond upward and downward parabolas, which are expressed by plus or minus before the square root. After the value of length was found we master a simpler expression for it which utilises the focal length [[p]] of the parabola.

In [1]:
from init_cycle import *
nu = varidx(symbol("nu"),2)

            Python wrappers for MoibInv Library
     ---------------------------------------------
Please cite this software as
V.V. Kisil, MoebInv: C++ libraries for manipulations in non-Euclidean geometry, SoftwareX, 11(2020),100385. doi:10.1016/j.softx.2019.100385.
     ---------------------------------------------

Using vector formalism and idx

signs_cube = {pow(sign, 3) : sign, pow(sign1, 3) : sign1}

In [2]:
signs_cube = {pow(sign1, 3) : sign}
In [3]:
def focal_length_check(p):
    er = clifford_unit(nu, diag_matrix([-1, sign5]), 2)
    C11 = C.subject_to([C.passing(P1), k==1, l == u, n == p])
    # And now we verify that the length is equal to (1-\sigma_1)p^2-2vp
    Len_c = C11.radius_sq(es).subs({pow(sign2,2) : 1}, subs_options.algebraic).normal()
    
    display(Latex("Verifying the f-length $%s$" % p))
    print("  [sanity check: cycle passes through (u1, v1): %s]" % C11.val(P1).normal().is_zero())
    print("  [sanity check: cycle's er-focus is  (u, v): %s]" % \
    (C11.focus(er,True).subs({pow(sign2,2) : 1}, subs_options.algebraic)-matrix([[u],[v]])).evalm().normal().is_zero_matrix())
    return Latex("Length between $(u,v)$ and $(u', v')$ is equal to $(\sigma_2-\sigma_1)p^2-2vp$: %s" %\
    ((Len_c - ((sign5-sign1)*pow(p, 2) - 2*v*p)).\
    subs(signs_cube, subs_options.algebraic).expand()\
    .subs({pow(sign2,2) : 1}, subs_options.algebraic).normal().is_zero()))

We made two checks for solution with positive sign...

In [4]:
sign5=sign2
focal_length_check(sign5*(-(v1-v)+pow(sign5*pow(u1-u, 2)+pow(v1-v, 2) \
-sign5*sign*pow(v1, 2),half)))
Verifying the f-length $- {({v'}-v-\sqrt{ {({u'}-u)}^{2} \sigma_2+{({v'}-v)}^{2}- \sigma {v'}^{2} \sigma_2})} \sigma_2$ 
  [sanity check: cycle passes through (u1, v1): True]
  [sanity check: cycle's er-focus is  (u, v): True]
Out[4]:
Length between $(u,v)$ and $(u', v')$ is equal to $(\sigma_2-\sigma_1)p^2-2vp$: True

...and with negative sign

In [5]:
focal_length_check(sign5*(-(v1-v)-pow(sign5*pow(u1-u, 2)+pow(v1-v, 2) \
-sign5*sign*pow(v1, 2),half)))
Verifying the f-length $- {({v'}-v+\sqrt{ {({u'}-u)}^{2} \sigma_2+{({v'}-v)}^{2}- \sigma {v'}^{2} \sigma_2})} \sigma_2$ 
  [sanity check: cycle passes through (u1, v1): True]
  [sanity check: cycle's er-focus is  (u, v): True]
Out[5]:
Length between $(u,v)$ and $(u', v')$ is equal to $(\sigma_2-\sigma_1)p^2-2vp$: True

finally we check the parabolic case formula

In [6]:
sign5=0;
focal_length_check((pow(u1-u,2)-sign*pow(v1,2))/(v1-v)/2)
Verifying the f-length $\frac{1}{2} \frac{{({u'}-u)}^{2}- \sigma {v'}^{2}}{{v'}-v}$ 
  [sanity check: cycle passes through (u1, v1): True]
  [sanity check: cycle's er-focus is  (u, v): True]
Out[6]:
Length between $(u,v)$ and $(u', v')$ is equal to $(\sigma_2-\sigma_1)p^2-2vp$: True

This notebook is a part of the MoebInv notebooks project [2] .

References

  1. Vladimir V. Kisil. Geometry of Möbius Transformations: Elliptic, Parabolic and Hyperbolic Actions of $SL_2(\mathbb{R})$. Imperial College Press, London, 2012. Includes a live DVD.

  2. Vladimir V. Kisil, MoebInv notebooks, 2019.

Back to Folder