# Metric on the upper half-plane #

In this file we define a MetricSpace structure on the UpperHalfPlane. We use hyperbolic (Poincaré) distance given by dist z w = 2 * arsinh (dist (z : ℂ) w / (2 * √(z.im * w.im))) instead of the induced Euclidean distance because the hyperbolic distance is invariant under holomorphic automorphisms of the upper half-plane. However, we ensure that the projection to TopologicalSpace is definitionally equal to the induced topological space structure.

We also prove that a metric ball/closed ball/sphere in Poincaré metric is a Euclidean ball/closed ball/sphere with another center and radius.

Equations
theorem UpperHalfPlane.dist_eq (z : UpperHalfPlane) (w : UpperHalfPlane) :
dist z w = 2 * (dist z w / (2 * (z.im * w.im))).arsinh
theorem UpperHalfPlane.sinh_half_dist (z : UpperHalfPlane) (w : UpperHalfPlane) :
(dist z w / 2).sinh = dist z w / (2 * (z.im * w.im))
theorem UpperHalfPlane.cosh_half_dist (z : UpperHalfPlane) (w : UpperHalfPlane) :
(dist z w / 2).cosh = dist (z) (() w) / (2 * (z.im * w.im))
theorem UpperHalfPlane.tanh_half_dist (z : UpperHalfPlane) (w : UpperHalfPlane) :
(dist z w / 2).tanh = dist z w / dist (z) (() w)
theorem UpperHalfPlane.exp_half_dist (z : UpperHalfPlane) (w : UpperHalfPlane) :
(dist z w / 2).exp = (dist z w + dist (z) (() w)) / (2 * (z.im * w.im))
theorem UpperHalfPlane.cosh_dist (z : UpperHalfPlane) (w : UpperHalfPlane) :
(dist z w).cosh = 1 + dist z w ^ 2 / (2 * z.im * w.im)
theorem UpperHalfPlane.sinh_half_dist_add_dist (a : UpperHalfPlane) (b : UpperHalfPlane) (c : UpperHalfPlane) :
((dist a b + dist b c) / 2).sinh = (dist a b * dist (c) (() b) + dist b c * dist (a) (() b)) / (2 * (a.im * c.im) * dist (b) (() b))
theorem UpperHalfPlane.dist_le_iff_le_sinh {z : UpperHalfPlane} {w : UpperHalfPlane} {r : } :
dist z w r dist z w / (2 * (z.im * w.im)) (r / 2).sinh
theorem UpperHalfPlane.dist_eq_iff_eq_sinh {z : UpperHalfPlane} {w : UpperHalfPlane} {r : } :
dist z w = r dist z w / (2 * (z.im * w.im)) = (r / 2).sinh
theorem UpperHalfPlane.dist_eq_iff_eq_sq_sinh {z : UpperHalfPlane} {w : UpperHalfPlane} {r : } (hr : 0 r) :
dist z w = r dist z w ^ 2 / (4 * z.im * w.im) = (r / 2).sinh ^ 2

An auxiliary MetricSpace instance on the upper half-plane. This instance has bad projection to TopologicalSpace. We replace it later.

Equations
Instances For
theorem UpperHalfPlane.cosh_dist' (z : UpperHalfPlane) (w : UpperHalfPlane) :
(dist z w).cosh = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im)

Euclidean center of the circle with center z and radius r in the hyperbolic metric.

Equations
• z.center r = { re := z.re, im := z.im * r.cosh },
Instances For
@[simp]
theorem UpperHalfPlane.center_re (z : UpperHalfPlane) (r : ) :
(z.center r).re = z.re
@[simp]
theorem UpperHalfPlane.center_im (z : UpperHalfPlane) (r : ) :
(z.center r).im = z.im * r.cosh
@[simp]
theorem UpperHalfPlane.center_zero (z : UpperHalfPlane) :
z.center 0 = z
theorem UpperHalfPlane.dist_coe_center_sq (z : UpperHalfPlane) (w : UpperHalfPlane) (r : ) :
dist z (w.center r) ^ 2 = 2 * z.im * w.im * ((dist z w).cosh - r.cosh) + (w.im * r.sinh) ^ 2
theorem UpperHalfPlane.dist_coe_center (z : UpperHalfPlane) (w : UpperHalfPlane) (r : ) :
dist z (w.center r) = (2 * z.im * w.im * ((dist z w).cosh - r.cosh) + (w.im * r.sinh) ^ 2)
theorem UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center (z : UpperHalfPlane) (w : UpperHalfPlane) (r : ) :
cmp (dist z w) r = cmp (dist z (w.center r)) (w.im * r.sinh)
theorem UpperHalfPlane.dist_eq_iff_dist_coe_center_eq {z : UpperHalfPlane} {w : UpperHalfPlane} {r : } :
dist z w = r dist z (w.center r) = w.im * r.sinh
@[simp]
theorem UpperHalfPlane.dist_self_center (z : UpperHalfPlane) (r : ) :
dist z (z.center r) = z.im * (r.cosh - 1)
@[simp]
theorem UpperHalfPlane.dist_center_dist (z : UpperHalfPlane) (w : UpperHalfPlane) :
dist z (w.center (dist z w)) = w.im * (dist z w).sinh
theorem UpperHalfPlane.dist_lt_iff_dist_coe_center_lt {z : UpperHalfPlane} {w : UpperHalfPlane} {r : } :
dist z w < r dist z (w.center r) < w.im * r.sinh
theorem UpperHalfPlane.lt_dist_iff_lt_dist_coe_center {z : UpperHalfPlane} {w : UpperHalfPlane} {r : } :
r < dist z w w.im * r.sinh < dist z (w.center r)
theorem UpperHalfPlane.dist_le_iff_dist_coe_center_le {z : UpperHalfPlane} {w : UpperHalfPlane} {r : } :
dist z w r dist z (w.center r) w.im * r.sinh
theorem UpperHalfPlane.le_dist_iff_le_dist_coe_center {z : UpperHalfPlane} {w : UpperHalfPlane} {r : } :
r < dist z w w.im * r.sinh < dist z (w.center r)
theorem UpperHalfPlane.dist_of_re_eq {z : UpperHalfPlane} {w : UpperHalfPlane} (h : z.re = w.re) :
dist z w = dist z.im.log w.im.log

For two points on the same vertical line, the distance is equal to the distance between the logarithms of their imaginary parts.

theorem UpperHalfPlane.dist_log_im_le (z : UpperHalfPlane) (w : UpperHalfPlane) :
dist z.im.log w.im.log dist z w

Hyperbolic distance between two points is greater than or equal to the distance between the logarithms of their imaginary parts.

theorem UpperHalfPlane.dist_coe_le (z : UpperHalfPlane) (w : UpperHalfPlane) :
dist z w w.im * ((dist z w).exp - 1)

An upper estimate on the complex distance between two points in terms of the hyperbolic distance and the imaginary part of one of the points.

theorem UpperHalfPlane.le_dist_coe (z : UpperHalfPlane) (w : UpperHalfPlane) :
w.im * (1 - (-dist z w).exp) dist z w

An upper estimate on the complex distance between two points in terms of the hyperbolic distance and the imaginary part of one of the points.

The hyperbolic metric on the upper half plane. We ensure that the projection to TopologicalSpace is definitionally equal to the subtype topology.

Equations
theorem UpperHalfPlane.im_pos_of_dist_center_le {z : UpperHalfPlane} {r : } {w : } (h : dist w (z.center r) z.im * r.sinh) :
0 < w.im
theorem UpperHalfPlane.image_coe_closedBall (z : UpperHalfPlane) (r : ) :
= Metric.closedBall ((z.center r)) (z.im * r.sinh)
theorem UpperHalfPlane.image_coe_ball (z : UpperHalfPlane) (r : ) :
= Metric.ball ((z.center r)) (z.im * r.sinh)
theorem UpperHalfPlane.image_coe_sphere (z : UpperHalfPlane) (r : ) :
= Metric.sphere ((z.center r)) (z.im * r.sinh)
Equations
theorem UpperHalfPlane.isometry_vertical_line (a : ) :
Isometry fun (y : ) => UpperHalfPlane.mk { re := a, im := y.exp }
theorem UpperHalfPlane.isometry_pos_mul (a : { x : // 0 < x }) :
Isometry fun (x : UpperHalfPlane) => a x

SL(2, ℝ) acts on the upper half plane as an isometry.

Equations