mathlib documentation

analysis.complex.upper_half_plane.metric

Metric on the upper half-plane #

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]
Equations
theorem upper_half_plane.dist_eq_iff_eq_sq_sinh {z w : upper_half_plane} {r : } (hr : 0 r) :
has_dist.dist z w = r has_dist.dist z w ^ 2 / (4 * z.im * w.im) = real.sinh (r / 2) ^ 2

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 (has_dist.dist z 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]

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.

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]

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

Equations