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 * Real.arsinh (dist ↑z ↑w / (2 * √(z.im * w.im))) }

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

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

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

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

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

theorem UpperHalfPlane.cosh_dist (z : UpperHalfPlane) (w : UpperHalfPlane) : Real.cosh (dist z w) = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)

theorem UpperHalfPlane.sinh_half_dist_add_dist (a : UpperHalfPlane) (b : UpperHalfPlane) (c : UpperHalfPlane) : Real.sinh ((dist a b + dist b c) / 2) = (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im) * 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)) ≤ Real.sinh (r / 2)

theorem UpperHalfPlane.dist_eq_iff_eq_sinh {z : UpperHalfPlane} {w : UpperHalfPlane} {r : ℝ} : dist z w = r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) = Real.sinh (r / 2)

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) = Real.sinh (r / 2) ^ 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)

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) : Real.cosh (dist z w) = ((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 * Real.cosh r }, ⋯⟩

@[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 * Real.cosh r

@[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 * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2

theorem UpperHalfPlane.dist_coe_center (z : UpperHalfPlane) (w : UpperHalfPlane) (r : ℝ) : dist ↑z ↑(w.center r) = √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 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 * Real.sinh r)

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 * Real.sinh r

@[simp]

theorem UpperHalfPlane.dist_self_center (z : UpperHalfPlane) (r : ℝ) : dist ↑z ↑(z.center r) = z.im * (Real.cosh r - 1)

@[simp]

theorem UpperHalfPlane.dist_center_dist (z : UpperHalfPlane) (w : UpperHalfPlane) : dist ↑z ↑(w.center (dist z w)) = w.im * Real.sinh (dist z w)

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 * Real.sinh r

theorem UpperHalfPlane.lt_dist_iff_lt_dist_coe_center {z : UpperHalfPlane} {w : UpperHalfPlane} {r : ℝ} : r < dist z w ↔ w.im * Real.sinh r < 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 * Real.sinh r

theorem UpperHalfPlane.le_dist_iff_le_dist_coe_center {z : UpperHalfPlane} {w : UpperHalfPlane} {r : ℝ} : r < dist z w ↔ w.im * Real.sinh r < dist ↑z ↑(w.center r)

theorem UpperHalfPlane.dist_of_re_eq {z : UpperHalfPlane} {w : UpperHalfPlane} (h : z.re = w.re) : dist z w = dist (Real.log z.im) (Real.log w.im)

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 (Real.log z.im) (Real.log w.im) ≤ 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 * Real.exp (dist z w)

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

theorem UpperHalfPlane.dist_coe_le (z : UpperHalfPlane) (w : UpperHalfPlane) : dist ↑z ↑w ≤ w.im * (Real.exp (dist z w) - 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 - Real.exp (-dist z w)) ≤ 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 * Real.sinh r) : 0 < w.im

theorem UpperHalfPlane.image_coe_closedBall (z : UpperHalfPlane) (r : ℝ) : UpperHalfPlane.coe '' Metric.closedBall z r = Metric.closedBall (↑(z.center r)) (z.im * Real.sinh r)

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

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

instance UpperHalfPlane.instProperSpace : ProperSpace UpperHalfPlane

Equations

• UpperHalfPlane.instProperSpace = ⋯

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

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 = ⋯