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.

instance UpperHalfPlane.instDist : Dist UpperHalfPlane

Equations

• UpperHalfPlane.instDist = { dist := fun (z w : UpperHalfPlane) => 2 * (dist ↑z ↑w / (2 * (z.im * w.im).sqrt)).arsinh }

theorem UpperHalfPlane.dist_eq (z : UpperHalfPlane) (w : UpperHalfPlane) : dist z w = 2 * (dist ↑z ↑w / (2 * (z.im * w.im).sqrt)).arsinh

theorem UpperHalfPlane.sinh_half_dist (z : UpperHalfPlane) (w : UpperHalfPlane) : (dist z w / 2).sinh = dist ↑z ↑w / (2 * (z.im * w.im).sqrt)

theorem UpperHalfPlane.cosh_half_dist (z : UpperHalfPlane) (w : UpperHalfPlane) : (dist z w / 2).cosh = dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * (z.im * w.im).sqrt)

theorem UpperHalfPlane.tanh_half_dist (z : UpperHalfPlane) (w : UpperHalfPlane) : (dist z w / 2).tanh = dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w)

theorem UpperHalfPlane.exp_half_dist (z : UpperHalfPlane) (w : UpperHalfPlane) : (dist z w / 2).exp = (dist ↑z ↑w + dist (↑z) ((starRingEnd ℂ) ↑w)) / (2 * (z.im * w.im).sqrt)

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) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * (a.im * c.im).sqrt * dist (↑b) ((starRingEnd ℂ) ↑b))

theorem UpperHalfPlane.dist_comm (z : UpperHalfPlane) (w : UpperHalfPlane) : dist z w = dist w z

theorem UpperHalfPlane.dist_le_iff_le_sinh {z : UpperHalfPlane} {w : UpperHalfPlane} {r : ℝ} : dist z w ≤ r ↔ dist ↑z ↑w / (2 * (z.im * w.im).sqrt) ≤ (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).sqrt) = (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

theorem UpperHalfPlane.dist_triangle (a : UpperHalfPlane) (b : UpperHalfPlane) (c : UpperHalfPlane) : dist a c ≤ dist a b + dist b c

theorem UpperHalfPlane.dist_le_dist_coe_div_sqrt (z : UpperHalfPlane) (w : UpperHalfPlane) : dist z w ≤ dist ↑z ↑w / (z.im * w.im).sqrt

def UpperHalfPlane.metricSpaceAux : MetricSpace UpperHalfPlane

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

Equations

• UpperHalfPlane.metricSpaceAux = MetricSpace.mk @UpperHalfPlane.metricSpaceAux.proof_6

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)

def UpperHalfPlane.center (z : UpperHalfPlane) (r : ℝ) : UpperHalfPlane

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 }, ⋯⟩

@[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).sqrt

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.im_le_im_mul_exp_dist (z : UpperHalfPlane) (w : UpperHalfPlane) : z.im ≤ w.im * (dist z w).exp

theorem UpperHalfPlane.im_div_exp_dist_le (z : UpperHalfPlane) (w : UpperHalfPlane) : z.im / (dist z w).exp ≤ w.im

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.

instance UpperHalfPlane.instMetricSpace : MetricSpace UpperHalfPlane

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

Equations

• UpperHalfPlane.instMetricSpace = UpperHalfPlane.metricSpaceAux.replaceTopology UpperHalfPlane.instMetricSpace.proof_1

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 : ℝ) : UpperHalfPlane.coe '' Metric.closedBall z r = Metric.closedBall (↑(z.center r)) (z.im * r.sinh)

theorem UpperHalfPlane.image_coe_ball (z : UpperHalfPlane) (r : ℝ) : UpperHalfPlane.coe '' Metric.ball z r = Metric.ball (↑(z.center r)) (z.im * r.sinh)

theorem UpperHalfPlane.image_coe_sphere (z : UpperHalfPlane) (r : ℝ) : UpperHalfPlane.coe '' Metric.sphere z r = Metric.sphere (↑(z.center r)) (z.im * r.sinh)

instance UpperHalfPlane.instProperSpace : ProperSpace UpperHalfPlane

Equations

• UpperHalfPlane.instProperSpace = ⋯

theorem UpperHalfPlane.isometry_vertical_line (a : ℝ) : Isometry fun (y : ℝ) => UpperHalfPlane.mk { re := a, im := y.exp } ⋯

theorem UpperHalfPlane.isometry_real_vadd (a : ℝ) : Isometry fun (x : UpperHalfPlane) => a +ᵥ x

theorem UpperHalfPlane.isometry_pos_mul (a : { x : ℝ // 0 < x }) : Isometry fun (x : UpperHalfPlane) => a • x

instance UpperHalfPlane.instIsometricSMulSpecialLinearGroupFinOfNatNatReal : IsometricSMul (Matrix.SpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane

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

Equations

• UpperHalfPlane.instIsometricSMulSpecialLinearGroupFinOfNatNatReal = ⋯