# mathlib3documentation

analysis.complex.upper_half_plane.metric

# Metric on the upper half-plane #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define a metric_space structure on the upper_half_plane. We use hyperbolic (Poincaré) distance given by dist z w = 2 * arsinh (dist (z : ℂ) w / (2 * real.sqrt (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 topological_space 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.

@[protected, instance]
noncomputable def upper_half_plane.has_dist  :
Equations
theorem upper_half_plane.exp_half_dist (z w : upper_half_plane) :
rexp w / 2) = w + ( w)) / (2 * (z.im * w.im))
theorem upper_half_plane.cosh_dist (z w : upper_half_plane) :
real.cosh w) = 1 + ^ 2 / (2 * z.im * w.im)
theorem upper_half_plane.sinh_half_dist_add_dist (a b c : upper_half_plane) :
real.sinh b + c) / 2) = b * ( b) + * ( b)) / (2 * (a.im * c.im) * ( b))
@[protected]
theorem upper_half_plane.dist_eq_iff_eq_sinh {z w : upper_half_plane} {r : } :
= r / (2 * (z.im * w.im)) = real.sinh (r / 2)
theorem upper_half_plane.dist_eq_iff_eq_sq_sinh {z w : upper_half_plane} {r : } (hr : 0 r) :
= r ^ 2 / (4 * z.im * w.im) = real.sinh (r / 2) ^ 2
@[protected]
noncomputable def upper_half_plane.metric_space_aux  :

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

Equations
theorem upper_half_plane.cosh_dist' (z w : upper_half_plane) :
real.cosh w) = ((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
@[simp]
theorem upper_half_plane.center_re (z : upper_half_plane) (r : ) :
(z.center r).re = z.re
@[simp]
theorem upper_half_plane.center_im (z : upper_half_plane) (r : ) :
(z.center r).im = z.im *
theorem upper_half_plane.dist_coe_center_sq (z w : upper_half_plane) (r : ) :
(w.center r) ^ 2 = 2 * z.im * w.im * (real.cosh w) - + (w.im * ^ 2
theorem upper_half_plane.dist_coe_center (z w : upper_half_plane) (r : ) :
(w.center r) = (2 * z.im * w.im * (real.cosh w) - + (w.im * ^ 2)
@[simp]
theorem upper_half_plane.dist_of_re_eq {z w : upper_half_plane} (h : z.re = w.re) :

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

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

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 upper_half_plane.le_dist_coe (z w : upper_half_plane) :
w.im * (1 - rexp (- 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.

@[protected, instance]
noncomputable def upper_half_plane.metric_space  :

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

Equations
theorem upper_half_plane.im_pos_of_dist_center_le {z : upper_half_plane} {r : } {w : } (h : (z.center r) z.im * ) :
0 < w.im
@[protected, instance]
theorem upper_half_plane.isometry_pos_mul (a : {x // 0 < x}) :
@[protected, instance]

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