At the moment it is to hot for real mathematics but I wanted to have a function that relates the lengths of the real sides of an Ideal Lambert quadrilateral
An Ideal Lambert quadrilateral (my term, not an official name) is a Lambert Quadrilateral ( https://en.wikipedia.org/wiki/Lambert_quadrilateral ) where the not right angled vertex is an ideal point https://en.wikipedia.org/wiki/Ideal_point so the fourth angle is zero.
and the question is how do the lengths of the sides that *not meet at the ideal vertex relate to eachother.
the proper way to get this function is complicated and tedious and so so I thought is there no shortcut? (and it is hot now)
What do we know about this function and which functions are this way?
If we call this relation $f(x)$ we have the following facts:
we only need to concider values of $ x \gt 0 $
$ \forall x\gt 0 : f(x) \ge 0 $
$ \forall x \gt 0 : f(f(x)) = x $
$ \forall x \gt 0, y : x \le y \to f(y) \le f(x) $
and the only function I know where all these apply is the function
$$ g(x) = \frac{1}{x} $$
Is this enough to conclude that $f(x) = g(x) $ or are there other functions where these relations hold and i do need to do my tedious mathematics?
as you can see in the diagram of the upper half plane in $\mathbb C,$ the ratio (or difference) of lengths of the two finite sides varies continuously with the real parameter I am calling $A,$ with $A > 0.$ The three (finite) vertices are at $$ i, \; \; \; \; A + i \sqrt {1 + A^2}, \; \; \; \; \frac{-1}{A} + \frac{i}{A} \sqrt {1 + A^2}. $$
Oh, for real $E$ and real $F > 0,$ the following is a geodesic parametrized by arc length $t:$ $$ E + F \tanh t + i F \operatorname{sech} t. $$ This is one way to find out the lengths of the two finite Lambert segments in the diagram.
ADDED: if we call $s > 0, t > 0$ the lengths of the two finite edges, the requested relationship is not quite reciprocals, instead $$ e^s = \frac{e^t + 1}{e^t - 1} $$ and $$ e^t = \frac{e^s + 1}{e^s - 1} $$ Note that the Möbius transformation $$ f(z) = \frac{z+1}{z-1} $$ is its own inverse.
Since, for some $0 \leq u < 1,$ we have bounds $$ u - \frac{u^2}{2} \leq \log (1+u) \leq u, $$ the relationship $$s = \log \left(1 + \frac{2}{e^t - 1} \right) $$ says that, as $t \rightarrow +\infty,$ that $$ s \approx \frac{2}{e^t}. $$
Here is a graph of $ s = \log \left( \frac{e^t + 1}{e^t - 1} \right) $