mathlib3 documentation

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 :

has_dist upper_half_plane

Equations

upper_half_plane.has_dist = {dist := λ (z w : upper_half_plane), 2 * real.arsinh (has_dist.dist ↑z ↑w / (2 * √ (z.im * w.im)))}

theorem upper_half_plane.dist_eq (z w : upper_half_plane) :

has_dist.dist z w = 2 * real.arsinh (has_dist.dist ↑z ↑w / (2 * √ (z.im * w.im)))

theorem upper_half_plane.sinh_half_dist (z w : upper_half_plane) :

real.sinh (has_dist.dist z w / 2) = has_dist.dist ↑z ↑w / (2 * √ (z.im * w.im))

theorem upper_half_plane.cosh_half_dist (z w : upper_half_plane) :

real.cosh (has_dist.dist z w / 2) = has_dist.dist ↑z (⇑(star_ring_end ℂ) ↑w) / (2 * √ (z.im * w.im))

theorem upper_half_plane.tanh_half_dist (z w : upper_half_plane) :

real.tanh (has_dist.dist z w / 2) = has_dist.dist ↑z ↑w / has_dist.dist ↑z (⇑(star_ring_end ℂ) ↑w)

theorem upper_half_plane.exp_half_dist (z w : upper_half_plane) :

rexp (has_dist.dist z w / 2) = (has_dist.dist ↑z ↑w + has_dist.dist ↑z (⇑(star_ring_end ℂ) ↑w)) / (2 * √ (z.im * w.im))

theorem upper_half_plane.cosh_dist (z w : upper_half_plane) :

real.cosh (has_dist.dist z w) = 1 + has_dist.dist ↑z ↑w ^ 2 / (2 * z.im * w.im)

theorem upper_half_plane.sinh_half_dist_add_dist (a b c : upper_half_plane) :

real.sinh ((has_dist.dist a b + has_dist.dist b c) / 2) = (has_dist.dist ↑a ↑b * has_dist.dist ↑c (⇑(star_ring_end ℂ) ↑b) + has_dist.dist ↑b ↑c * has_dist.dist ↑a (⇑(star_ring_end ℂ) ↑b)) / (2 * √ (a.im * c.im) * has_dist.dist ↑b (⇑(star_ring_end ℂ) ↑b))

@[protected]

theorem upper_half_plane.dist_comm (z w : upper_half_plane) :

has_dist.dist z w = has_dist.dist w z

theorem upper_half_plane.dist_le_iff_le_sinh {z w : upper_half_plane} {r : ℝ} :

has_dist.dist z w ≤ r ↔ has_dist.dist ↑z ↑w / (2 * √ (z.im * w.im)) ≤ real.sinh (r / 2)

theorem upper_half_plane.dist_eq_iff_eq_sinh {z w : upper_half_plane} {r : ℝ} :

has_dist.dist z w = r ↔ has_dist.dist ↑z ↑w / (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) :

has_dist.dist z w = r ↔ has_dist.dist ↑z ↑w ^ 2 / (4 * z.im * w.im) = real.sinh (r / 2) ^ 2

@[protected]

theorem upper_half_plane.dist_triangle (a b c : upper_half_plane) :

has_dist.dist a c ≤ has_dist.dist a b + has_dist.dist b c

theorem upper_half_plane.dist_le_dist_coe_div_sqrt (z w : upper_half_plane) :

has_dist.dist z w ≤ has_dist.dist ↑z ↑w / √ (z.im * w.im)

noncomputable def upper_half_plane.metric_space_aux :

metric_space upper_half_plane

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

Equations

upper_half_plane.metric_space_aux = {to_pseudo_metric_space := {to_has_dist := {dist := has_dist.dist upper_half_plane.has_dist}, dist_self := upper_half_plane.metric_space_aux._proof_1, dist_comm := upper_half_plane.dist_comm, dist_triangle := upper_half_plane.dist_triangle, edist := λ (x y : upper_half_plane), ↑⟨has_dist.dist x y, _⟩, edist_dist := upper_half_plane.metric_space_aux._proof_3, to_uniform_space := uniform_space_of_dist has_dist.dist upper_half_plane.metric_space_aux._proof_4 upper_half_plane.dist_comm upper_half_plane.dist_triangle, uniformity_dist := upper_half_plane.metric_space_aux._proof_5, to_bornology := bornology.of_dist has_dist.dist upper_half_plane.metric_space_aux._proof_6 upper_half_plane.dist_comm upper_half_plane.dist_triangle, cobounded_sets := upper_half_plane.metric_space_aux._proof_7}, eq_of_dist_eq_zero := upper_half_plane.metric_space_aux._proof_8}

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)

noncomputable def upper_half_plane.center (z : upper_half_plane) (r : ℝ) :

upper_half_plane

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 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 * real.cosh r

@[simp]

theorem upper_half_plane.center_zero (z : upper_half_plane) :

z.center 0 = z

theorem upper_half_plane.dist_coe_center_sq (z w : upper_half_plane) (r : ℝ) :

has_dist.dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (real.cosh (has_dist.dist z w) - real.cosh r) + (w.im * real.sinh r) ^ 2

theorem upper_half_plane.dist_coe_center (z w : upper_half_plane) (r : ℝ) :

has_dist.dist ↑z ↑(w.center r) = √ (2 * z.im * w.im * (real.cosh (has_dist.dist z w) - real.cosh r) + (w.im * real.sinh r) ^ 2)

theorem upper_half_plane.cmp_dist_eq_cmp_dist_coe_center (z w : upper_half_plane) (r : ℝ) :

cmp (has_dist.dist z w) r = cmp (has_dist.dist ↑z ↑(w.center r)) (w.im * real.sinh r)

theorem upper_half_plane.dist_eq_iff_dist_coe_center_eq {z w : upper_half_plane} {r : ℝ} :

has_dist.dist z w = r ↔ has_dist.dist ↑z ↑(w.center r) = w.im * real.sinh r

@[simp]

theorem upper_half_plane.dist_self_center (z : upper_half_plane) (r : ℝ) :

has_dist.dist ↑z ↑(z.center r) = z.im * (real.cosh r - 1)

@[simp]

theorem upper_half_plane.dist_center_dist (z w : upper_half_plane) :

has_dist.dist ↑z ↑(w.center (has_dist.dist z w)) = w.im * real.sinh (has_dist.dist z w)

theorem upper_half_plane.dist_lt_iff_dist_coe_center_lt {z w : upper_half_plane} {r : ℝ} :

has_dist.dist z w < r ↔ has_dist.dist ↑z ↑(w.center r) < w.im * real.sinh r

theorem upper_half_plane.lt_dist_iff_lt_dist_coe_center {z w : upper_half_plane} {r : ℝ} :

r < has_dist.dist z w ↔ w.im * real.sinh r < has_dist.dist ↑z ↑(w.center r)

theorem upper_half_plane.dist_le_iff_dist_coe_center_le {z w : upper_half_plane} {r : ℝ} :

has_dist.dist z w ≤ r ↔ has_dist.dist ↑z ↑(w.center r) ≤ w.im * real.sinh r

theorem upper_half_plane.le_dist_iff_le_dist_coe_center {z w : upper_half_plane} {r : ℝ} :

r < has_dist.dist z w ↔ w.im * real.sinh r < has_dist.dist ↑z ↑(w.center r)

theorem upper_half_plane.dist_of_re_eq {z w : upper_half_plane} (h : z.re = w.re) :

has_dist.dist z w = has_dist.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 upper_half_plane.dist_log_im_le (z w : upper_half_plane) :

has_dist.dist (real.log z.im) (real.log w.im) ≤ has_dist.dist z w

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

theorem upper_half_plane.im_le_im_mul_exp_dist (z w : upper_half_plane) :

z.im ≤ w.im * rexp (has_dist.dist z w)

theorem upper_half_plane.im_div_exp_dist_le (z w : upper_half_plane) :

z.im / rexp (has_dist.dist z w) ≤ w.im

theorem upper_half_plane.dist_coe_le (z w : upper_half_plane) :

has_dist.dist ↑z ↑w ≤ w.im * (rexp (has_dist.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 upper_half_plane.le_dist_coe (z w : upper_half_plane) :

w.im * (1 - rexp (-has_dist.dist z w)) ≤ has_dist.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.

@[protected, instance]

noncomputable def upper_half_plane.metric_space :

metric_space upper_half_plane

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

Equations

upper_half_plane.metric_space = upper_half_plane.metric_space_aux.replace_topology upper_half_plane.metric_space._proof_1

theorem upper_half_plane.im_pos_of_dist_center_le {z : upper_half_plane} {r : ℝ} {w : ℂ} (h : has_dist.dist w ↑(z.center r) ≤ z.im * real.sinh r) :

0 < w.im

theorem upper_half_plane.image_coe_closed_ball (z : upper_half_plane) (r : ℝ) :

coe '' metric.closed_ball z r = metric.closed_ball ↑(z.center r) (z.im * real.sinh r)

theorem upper_half_plane.image_coe_ball (z : upper_half_plane) (r : ℝ) :

coe '' metric.ball z r = metric.ball ↑(z.center r) (z.im * real.sinh r)

theorem upper_half_plane.image_coe_sphere (z : upper_half_plane) (r : ℝ) :

coe '' metric.sphere z r = metric.sphere ↑(z.center r) (z.im * real.sinh r)

@[protected, instance]

def upper_half_plane.proper_space :

proper_space upper_half_plane

theorem upper_half_plane.isometry_vertical_line (a : ℝ) :

isometry (λ (y : ℝ), upper_half_plane.mk {re := a, im := rexp y} _)

theorem upper_half_plane.isometry_real_vadd (a : ℝ) :

isometry (has_vadd.vadd a)

theorem upper_half_plane.isometry_pos_mul (a : {x // 0 < x}) :

isometry (has_smul.smul a)

@[protected, instance]

def upper_half_plane.has_isometric_smul :

has_isometric_smul (matrix.special_linear_group (fin 2) ℝ) upper_half_plane

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