UpperHalfPlane.dist_of_re_eq
theorem UpperHalfPlane.dist_of_re_eq : ∀ {z w : UpperHalfPlane}, z.re = w.re → dist z w = dist z.im.log w.im.log := by
sorry
This theorem states that for any two points `z` and `w` in the open upper half plane (a set of points whose imaginary part is greater than zero), if `z` and `w` lie on the same vertical line (i.e., their real parts are equal), then the Euclidean distance between `z` and `w` is equal to the distance between the logarithms of their imaginary parts.
More concisely: For points `z` and `w` in the open upper half plane with equal real parts, the Euclidean distance between them equals the absolute value difference of their logarithmic imaginary parts.
|
UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center
theorem UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center :
∀ (z w : UpperHalfPlane) (r : ℝ), cmp (dist z w) r = cmp (dist ↑z ↑(w.center r)) (w.im * r.sinh)
This theorem is stating that for all points `z` and `w` in the open upper half plane and any real number `r`, the comparison (ordered as less than, equal, or greater than) of the Euclidean distance between `z` and `w` with `r` is the same as the comparison of the Euclidean distance between `z` and the center of the circle with center `w` and radius `r` in the hyperbolic metric, with the product of the imaginary part of `w` and the hyperbolic sine of `r`. In other words, this theorem is comparing distances in two different geometric contexts: the usual Euclidean plane and a hyperbolic metric.
More concisely: For all `z` and `w` in the open upper half plane and real number `r`, the Euclidean distance between `z` and `w` is less than, equal to, or greater than `r` if and only if the hyperbolic distance between `z` and the center of the circle with center `w` and radius `r` is less than, equal to, or greater than the product of the imaginary part of `w` and the hyperbolic sine of `r`.
|
UpperHalfPlane.dist_log_im_le
theorem UpperHalfPlane.dist_log_im_le : ∀ (z w : UpperHalfPlane), dist z.im.log w.im.log ≤ dist z w
This theorem states that for any two points 'z' and 'w' in the open upper half plane, the hyperbolic distance between the points is always greater than or equal to the distance between the logarithms of their imaginary parts. In other words, it asserts a kind of lower bound on the hyperbolic distance between two points in the upper half plane, given by the logarithms of their imaginary parts.
More concisely: The hyperbolic distance between two complex numbers in the upper half plane is greater than or equal to the real part of the difference of their logarithms.
|
UpperHalfPlane.dist_eq
theorem UpperHalfPlane.dist_eq :
∀ (z w : UpperHalfPlane), dist z w = 2 * (dist ↑z ↑w / (2 * (z.im * w.im).sqrt)).arsinh
The theorem `UpperHalfPlane.dist_eq` states that for any two points `z` and `w` in the open upper half plane, the distance between `z` and `w` is twice the area hyperbolic sine of the ratio of the distance between `z` and `w` in the complex plane and twice the square root of the product of the imaginary parts of `z` and `w`. In other words, the theorem defines a distance metric on the open upper half plane using the area hyperbolic sine function. This function is geometrically significant in hyperbolic geometry and is used here to relate the Euclidean geometry of the complex plane with the hyperbolic geometry of the upper half plane.
More concisely: The theorem `UpperHalfPlane.dist_eq` asserts that the distance between two points in the open upper half plane is equal to twice the area hyperbolic sine of half the difference of their coordinates in the complex plane.
|
UpperHalfPlane.dist_coe_le
theorem UpperHalfPlane.dist_coe_le : ∀ (z w : UpperHalfPlane), dist ↑z ↑w ≤ w.im * ((dist z w).exp - 1)
The theorem `UpperHalfPlane.dist_coe_le` provides an upper bound on the complex distance between two points in the upper half plane. Specifically, for any two points `z` and `w` in the upper half plane, the complex distance between these two points is less than or equal to the imaginary part of `w` multiplied by the exponentiated hyperbolic distance between `z` and `w` minus one.
More concisely: For any complex numbers $z, w \in \mathbb{C}$ with positive imaginary parts, $|z - w| \leq \operatorname{Im}(w) \cdot e^{\operatorname{dist}_{\mathbb{H}}(\operatorname{Re}(z), \operatorname{Re}(w))}$, where $\mathbb{C}$ is the complex plane, $\mathbb{H}$ is the upper half-plane, $\operatorname{Re}(z)$, $\operatorname{Re}(w)$ are the real parts of $z$ and $w$, and $\operatorname{dist}_{\mathbb{H}}$ denotes the hyperbolic Euclidean distance in the upper half-plane.
|
UpperHalfPlane.sinh_half_dist
theorem UpperHalfPlane.sinh_half_dist :
∀ (z w : UpperHalfPlane), (dist z w / 2).sinh = dist ↑z ↑w / (2 * (z.im * w.im).sqrt)
The theorem `UpperHalfPlane.sinh_half_dist` states that for any two points `z` and `w` in the open upper half plane, the real hyperbolic sine of half the distance between `z` and `w` is equal to half the distance between the complexified versions of `z` and `w` divided by the square root of the product of the imaginary parts of `z` and `w`. In mathematical notation, this can be written as $\sinh\left(\frac{{\text{{dist}}(z, w)}}{2}\right) = \frac{{\text{{dist}}(\mathbf{C}(z), \mathbf{C}(w))}}{2 \sqrt{{\text{{Im}}(z) \cdot \text{{Im}}(w)}}}$, where $\mathbf{C}(z)$ and $\mathbf{C}(w)$ denote the complexified versions of `z` and `w`, and `Im` denotes the imaginary part of a complex number.
More concisely: The hyperbolic sine of half the real distance between two points in the open upper half plane is equal to one-half of the complex distance between their complexified versions divided by the square root of their imaginary product.
|
UpperHalfPlane.im_pos_of_dist_center_le
theorem UpperHalfPlane.im_pos_of_dist_center_le :
∀ {z : UpperHalfPlane} {r : ℝ} {w : ℂ}, dist w ↑(z.center r) ≤ z.im * r.sinh → 0 < w.im
This theorem states that for any point `z` in the upper half plane, any real number `r`, and any complex number `w`, if the Euclidean distance between `w` and the center of the circle (in the hyperbolic metric) with center `z` and radius `r` is less than or equal to the imaginary part of `z` multiplied by the hyperbolic sine of `r`, then the imaginary part of `w` is positive. This implies that `w` also falls in the upper half plane given certain conditions on its distance from a particular circle's center in the hyperbolic metric.
More concisely: If the Euclidean distance between a complex number `w` and the center `z` of a hyperbolic circle with radius `r` in the upper half plane is less than or equal to the imaginary part of `z` times the hyperbolic sine of `r`, then the imaginary part of `w` is positive.
|
UpperHalfPlane.le_dist_coe
theorem UpperHalfPlane.le_dist_coe : ∀ (z w : UpperHalfPlane), w.im * (1 - (-dist z w).exp) ≤ dist ↑z ↑w
This theorem provides an upper bound on the complex distance between any two points in the upper half plane. The upper bound is given in terms of the hyperbolic distance between the points and the imaginary part of one point. Specifically, it states that the product of the imaginary part of one point and the quantity (1 minus the exponential of the negative of the hyperbolic distance between the points) is less than or equal to the complex distance between the two points. Therefore, as the hyperbolic distance increases, the complex distance cannot exceed a certain limit defined by this relationship.
More concisely: For any two points in the upper half plane, the complex distance is bounded above by the product of the imaginary part of one point and (1 - exp(-hypothetic distance)), where hypothetic distance is the hyperbolic distance between the points.
|