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 * 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 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.instDistUpperHalfPlane : Dist UpperHalfPlane

Equations

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

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

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

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

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 * Real.sqrt (UpperHalfPlane.im z * UpperHalfPlane.im w))

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

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 * Real.sqrt (UpperHalfPlane.im a * UpperHalfPlane.im c) * 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 * Real.sqrt (UpperHalfPlane.im z * UpperHalfPlane.im w)) ≤ Real.sinh (r / 2)

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

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) = ((UpperHalfPlane.re z - UpperHalfPlane.re w) ^ 2 + UpperHalfPlane.im z ^ 2 + UpperHalfPlane.im w ^ 2) / (2 * UpperHalfPlane.im z * UpperHalfPlane.im w)

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

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

Equations

• UpperHalfPlane.center z r = { val := { re := UpperHalfPlane.re z, im := UpperHalfPlane.im z * Real.cosh r }, property := (_ : 0 < UpperHalfPlane.im z * Real.cosh r) }

@[simp]

theorem UpperHalfPlane.center_re (z : UpperHalfPlane) (r : ℝ) : UpperHalfPlane.re (UpperHalfPlane.center z r) = UpperHalfPlane.re z

@[simp]

theorem UpperHalfPlane.center_im (z : UpperHalfPlane) (r : ℝ) : UpperHalfPlane.im (UpperHalfPlane.center z r) = UpperHalfPlane.im z * Real.cosh r

@[simp]

theorem UpperHalfPlane.center_zero (z : UpperHalfPlane) : UpperHalfPlane.center z 0 = z

theorem UpperHalfPlane.dist_coe_center_sq (z : UpperHalfPlane) (w : UpperHalfPlane) (r : ℝ) : dist ↑z ↑(UpperHalfPlane.center w r) ^ 2 = 2 * UpperHalfPlane.im z * UpperHalfPlane.im w * (Real.cosh (dist z w) - Real.cosh r) + (UpperHalfPlane.im w * Real.sinh r) ^ 2

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

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

@[simp]

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

@[simp]

theorem UpperHalfPlane.dist_center_dist (z : UpperHalfPlane) (w : UpperHalfPlane) : dist ↑z ↑(UpperHalfPlane.center w (dist z w)) = UpperHalfPlane.im w * 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 ↑(UpperHalfPlane.center w r) < UpperHalfPlane.im w * Real.sinh r

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

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

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

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

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

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

theorem UpperHalfPlane.dist_coe_le (z : UpperHalfPlane) (w : UpperHalfPlane) : dist ↑z ↑w ≤ UpperHalfPlane.im w * (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) : UpperHalfPlane.im w * (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.instMetricSpaceUpperHalfPlane : 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.instMetricSpaceUpperHalfPlane = MetricSpace.replaceTopology UpperHalfPlane.metricSpaceAux UpperHalfPlane.instMetricSpaceUpperHalfPlane.proof_1

theorem UpperHalfPlane.im_pos_of_dist_center_le {z : UpperHalfPlane} {r : ℝ} {w : ℂ} (h : dist w ↑(UpperHalfPlane.center z r) ≤ UpperHalfPlane.im z * Real.sinh r) : 0 < w.im

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

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

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

instance UpperHalfPlane.instProperSpaceUpperHalfPlaneToPseudoMetricSpaceInstMetricSpaceUpperHalfPlane : ProperSpace UpperHalfPlane

Equations

• UpperHalfPlane.instProperSpaceUpperHalfPlaneToPseudoMetricSpaceInstMetricSpaceUpperHalfPlane = (_ : ProperSpace UpperHalfPlane)

theorem UpperHalfPlane.isometry_vertical_line (a : ℝ) : Isometry fun (y : ℝ) => UpperHalfPlane.mk { re := a, im := Real.exp y } (_ : 0 < 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.instIsometricSMulSpecialLinearGroupFinOfNatNatInstOfNatNatInstDecidableEqFinFintypeRealCommRingUpperHalfPlaneToPseudoEMetricSpaceToEMetricSpaceInstMetricSpaceUpperHalfPlaneToSMulMonoidSLActionToAlgebraNormedFieldToSeminormedRingToSeminormedCommRingNormedCommRingToNormedAlgebraIsROrC : IsometricSMul (Matrix.SpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane

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

Equations

• One or more equations did not get rendered due to their size.