Hyperbolic balls of the Poincaré disc are Euclidean discs

The hyperbolic (Poincaré) metric TauCeti.hyperbolicDist on the open unit disc is Real.artanh of the pseudo-hyperbolic expression p (z, a) = ‖(z - a) / (1 - conj a * z)‖, and both are visibly non-Euclidean: the metric blows up at the boundary circle, and p is a Moebius quotient rather than a norm. Nevertheless the hyperbolic ball of radius R is the pseudo-hyperbolic ball of radius Real.tanh R, and every pseudo-hyperbolic ball of radius t ∈ [0, 1) is a Euclidean disc. This file proves that, with the centre and radius computed explicitly.

Fix a in the disc and a pseudo-hyperbolic radius t ∈ [0, 1). Writing D = 1 - t ^ 2 * ‖a‖ ^ 2, which is positive, put

• TauCeti.pseudoHyperbolicCenter a t = ((1 - t ^ 2) / D) • a,
• TauCeti.pseudoHyperbolicRadius a t = t * (1 - ‖a‖ ^ 2) / D.

Then {z ∈ 𝔻 | p (z, a) < t} is exactly the Euclidean disc of that centre and radius (TauCeti.sep_ball_pseudoHyperbolicExpr_lt_eq_ball), and likewise for ≤ and = with the closed disc and the circle. Substituting t = Real.tanh R converts these into statements about the hyperbolic metric, since Real.artanh and Real.tanh are inverse increasing bijections between (-1, 1) and ℝ: the hyperbolic ball of centre a and radius R is the Euclidean disc of centre pseudoHyperbolicCenter a (Real.tanh R) and radius pseudoHyperbolicRadius a (Real.tanh R) (TauCeti.sep_ball_hyperbolicDist_lt_eq_ball).

The computation

Everything comes from a single algebraic identity between real quadratics (TauCeti.sq_norm_sub_sub_mul_sq_norm_one_sub_conj_mul):

‖z - a‖ ^ 2 - t ^ 2 * ‖1 - conj a * z‖ ^ 2 = D * (‖z - pseudoHyperbolicCenter a t‖ ^ 2 - pseudoHyperbolicRadius a t ^ 2),

valid for every z : ℂ as soon as D ≠ 0. Expanding the three norms with Complex.normSq_sub turns each side into a real polynomial in ‖z‖, ‖a‖, (z * conj a).re and t, and the two agree after clearing the denominator D. Since D > 0, the left side is negative, zero or positive exactly when ‖z - c‖ is less than, equal to or greater than the radius, which is the whole content: the pseudo-hyperbolic condition ‖z - a‖ < t * ‖1 - conj a * z‖ is a Euclidean disc.

Three features of the statement are worth noting. First, the identity — and hence the description of the sublevel set of ‖z - a‖ - t * ‖1 - conj a * z‖ — needs no hypothesis on z at all; it is only the passage to the quotient p (z, a) that requires z in the disc, so that the Moebius denominator does not vanish. Second, the resulting Euclidean disc automatically lies inside the unit disc: ‖c‖ + s < 1 because 1 - ‖c‖ - s = (1 - ‖a‖) * (1 - t) * (1 - t * ‖a‖) / D (TauCeti.norm_pseudoHyperbolicCenter_add_pseudoHyperbolicRadius_lt_one). So the restriction to the disc in the set equalities is a genuine description of a subset of 𝔻, not an artefact. Third, each statement asks of the radius only what it uses. The pointwise comparisons (TauCeti.pseudoHyperbolicExpr_lt_iff_mem_ball and its ≤/= companions) place no bound on t at all: they assume 0 < D, which is what turns the identity into a comparison of discs. That is strictly weaker than -1 ≤ t ≤ 1, which implies it (TauCeti.one_sub_sq_mul_sq_norm_pos) and is how every application below discharges it; for a = 0, where D = 1, every real t is allowed. Positivity of D cannot be dropped: for t < -1 it can fail, and then s is positive while the pseudo-hyperbolic condition is still unsatisfiable. A negative t is admitted and is vacuous on both sides: p is nonnegative, so the pseudo-hyperbolic condition is unsatisfiable, and the Euclidean radius s is then negative (TauCeti.pseudoHyperbolicRadius_neg), so the Euclidean disc is empty as well.

The set-level statements assume 0 < D as well, and add to it only an upper bound on t, because they describe the intersection with 𝔻 and so need the Euclidean disc to lie inside it. The endpoint t = 1 is admitted by the open ball (TauCeti.sep_ball_pseudoHyperbolicExpr_lt_eq_ball, on t ≤ 1), where c = 0 and s = 1 and the description degenerates to the statement that p (·, a) < 1 cuts out all of 𝔻; the closed disc and the circle need t < 1, since at t = 1 they would contain the unit circle, which the pseudo-hyperbolic conditions never reach. No lower bound on t is asked for: exactly as in the pointwise statements, a negative t empties both sides. It is this range that makes the statements about the hyperbolic metric unconditional in R, since Real.tanh R always lies in (-1, 1) (TauCeti.one_sub_sq_tanh_mul_sq_norm_pos).

The Euclidean centre c is not a unless a = 0 or t = 0: a hyperbolic ball is a Euclidean disc, but an off-centre one, its Euclidean centre pulled towards the origin by the factor (1 - t ^ 2) / D. The hyperbolic centre does lie inside it (TauCeti.mem_ball_pseudoHyperbolicCenter), as it must.

What this adds

Poincare/Topology.lean already identifies the closed hyperbolic ball about the origin with a Euclidean ball (TauCeti.hyperbolicDist_zero_le_iff_norm_le_tanh, the case a = 0, where the Moebius denominator is 1 and the computation is immediate) and uses it for properness. The general centre is what a local argument needs, and it is not a formal consequence of the special case: the disc automorphism moving a to the origin is a hyperbolic isometry but not a Euclidean one. Being a Moebius map it does carry the centred Euclidean disc onto a Euclidean disc — that is the very fact being proved here — but it preserves neither the Euclidean centre nor the Euclidean radius, so transport through it still leaves both to be computed. Those transformed values are the point.

Two immediate consequences are recorded: hyperbolic balls are convex for the Euclidean structure (TauCeti.convex_sep_ball_hyperbolicDist_lt), a fact with no hyperbolic proof at this stage of the development, since geodesic convexity is a different statement; and the balls of the metric space TauCeti.PoincareDisc are characterised in Euclidean terms (TauCeti.PoincareDisc.mem_ball_iff).

Generality

In accordance with the generality bar of ConformalMapping/README.md, which fixes scalar ℂ for every theorem added in layers L0–L6, everything below is stated for ℂ. The statements are not merely specialised but genuinely two-dimensional: the identity above is the complex-analytic Apollonius computation, and its conclusion — that a Moebius sublevel set is a disc — has no analogue in a general normed space.

Main definitions

• TauCeti.pseudoHyperbolicCenter — the Euclidean centre of the pseudo-hyperbolic ball.
• TauCeti.pseudoHyperbolicRadius — its Euclidean radius.

Main results

• TauCeti.sq_norm_sub_sub_mul_sq_norm_one_sub_conj_mul — the Apollonius identity the file runs on.
• TauCeti.norm_pseudoHyperbolicCenter_add_pseudoHyperbolicRadius_lt_one, TauCeti.closedBall_pseudoHyperbolicCenter_subset_ball and TauCeti.ball_pseudoHyperbolicCenter_subset_ball — the Euclidean disc lies inside 𝔻.
• TauCeti.pseudoHyperbolicExpr_lt_iff_mem_ball, TauCeti.pseudoHyperbolicExpr_le_iff_mem_closedBall and TauCeti.pseudoHyperbolicExpr_eq_iff_mem_sphere — the pointwise form.
• TauCeti.sep_ball_pseudoHyperbolicExpr_lt_eq_ball, TauCeti.sep_ball_pseudoHyperbolicExpr_le_eq_closedBall and TauCeti.sep_ball_pseudoHyperbolicExpr_eq_eq_sphere — pseudo-hyperbolic balls, closed balls and circles are Euclidean ones.
• TauCeti.sep_ball_hyperbolicDist_lt_eq_ball, TauCeti.sep_ball_hyperbolicDist_le_eq_closedBall and TauCeti.sep_ball_hyperbolicDist_eq_eq_sphere — the same for the hyperbolic metric, with t = Real.tanh R.
• TauCeti.PoincareDisc.mem_ball_iff, TauCeti.PoincareDisc.mem_closedBall_iff and TauCeti.PoincareDisc.mem_sphere_iff — the balls, closed balls and spheres of the Poincaré metric space, read on the Euclidean disc.

This carries the conformal-mapping roadmap's L2 target "the hyperbolic / Poincaré metric on 𝔻" (see ConformalMapping/README.md) onto its metric geometry, completing the basic ball API of that metric. As with the rest of the L0–L3 conformal-mapping material it is coordinated with the upstream Mathlib Riemann mapping effort leanprover-community/mathlib4#33505, which contains the preceding human-curated work along with Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; none of that material describes the hyperbolic metric on the disc.

The closest formal precedent anywhere is Mathlib's upper half-plane model, Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean, which does carry the analogous ball description, and whose API shape the development below follows: UpperHalfPlane.center z r is the Euclidean centre of the hyperbolic ball of centre z and radius r, UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center and its consequences UpperHalfPlane.dist_lt_iff_dist_coe_center_lt, UpperHalfPlane.dist_le_iff_dist_coe_center_le and UpperHalfPlane.dist_eq_iff_dist_coe_center_eq are the pointwise comparisons, and UpperHalfPlane.image_coe_ball, UpperHalfPlane.image_coe_closedBall and UpperHalfPlane.image_coe_sphere are the set-level identifications. What is supplied here is the disc-model counterpart: the two models are conformally but not Euclidean-equivalent, so the formulas differ (z.im * Real.cosh r and z.im * Real.sinh r on ℍ, against TauCeti.pseudoHyperbolicCenter and TauCeti.pseudoHyperbolicRadius here), and Mathlib has no metric on 𝔻 to state them about. Nothing here duplicates that file; the parallel is one of shape, and it is what fixes the shape of the API below.

References

• L. V. Ahlfors, Conformal Invariants, Ch. 1.
• J. B. Garnett and D. E. Marshall, Harmonic Measure, Ch. I §1.
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, §1.2.

The Euclidean centre and radius

noncomputable def TauCeti.pseudoHyperbolicCenter (a : ℂ) (t : ℝ) : ℂ

The Euclidean centre of the pseudo-hyperbolic ball of centre a and radius t: the hyperbolic centre a pulled towards the origin by the factor (1 - t ^ 2) / (1 - t ^ 2 * ‖a‖ ^ 2).

Equations

• TauCeti.pseudoHyperbolicCenter a t = ((1 - t ^ 2) / (1 - t ^ 2 * ‖a‖ ^ 2)) • a

noncomputable def TauCeti.pseudoHyperbolicRadius (a : ℂ) (t : ℝ) : ℝ

The Euclidean radius of the pseudo-hyperbolic ball of centre a and radius t.

Equations

• TauCeti.pseudoHyperbolicRadius a t = t * (1 - ‖a‖ ^ 2) / (1 - t ^ 2 * ‖a‖ ^ 2)

theorem TauCeti.pseudoHyperbolicCenter_def (a : ℂ) (t : ℝ) : pseudoHyperbolicCenter a t = ((1 - t ^ 2) / (1 - t ^ 2 * ‖a‖ ^ 2)) • a

The defining formula for TauCeti.pseudoHyperbolicCenter, so that the advertised expression is available without unfolding the definition.

theorem TauCeti.pseudoHyperbolicRadius_def (a : ℂ) (t : ℝ) : pseudoHyperbolicRadius a t = t * (1 - ‖a‖ ^ 2) / (1 - t ^ 2 * ‖a‖ ^ 2)

The defining formula for TauCeti.pseudoHyperbolicRadius, so that the advertised expression is available without unfolding the definition.

@[simp]

theorem TauCeti.pseudoHyperbolicCenter_zero_left (t : ℝ) : pseudoHyperbolicCenter 0 t = 0

Balls centred at the origin are unmoved: the Euclidean centre of a pseudo-hyperbolic ball about 0 is 0.

@[simp]

theorem TauCeti.pseudoHyperbolicRadius_zero_left (t : ℝ) : pseudoHyperbolicRadius 0 t = t

Balls centred at the origin have their Euclidean radius equal to the pseudo-hyperbolic one, so that at the origin the two descriptions of a ball coincide.

@[simp]

theorem TauCeti.pseudoHyperbolicCenter_zero_right (a : ℂ) : pseudoHyperbolicCenter a 0 = a

A ball of radius 0 is centred at its hyperbolic centre.

@[simp]

theorem TauCeti.pseudoHyperbolicRadius_zero_right (a : ℂ) : pseudoHyperbolicRadius a 0 = 0

A ball of radius 0 has Euclidean radius 0.

theorem TauCeti.one_sub_sq_mul_sq_norm_pos {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (ht₀ : -1 ≤ t) (ht₁ : t ≤ 1) : 0 < 1 - t ^ 2 * ‖a‖ ^ 2

The denominator 1 - t ^ 2 * ‖a‖ ^ 2 is positive for a disc centre and a radius in [-1, 1]. Its positivity — the hypothesis the pointwise results below actually run on — is what makes the Apollonius identity a genuine comparison of discs rather than a degenerate one.

theorem TauCeti.one_sub_sq_tanh_mul_sq_norm_pos {a : ℂ} (ha : ‖a‖ < 1) (R : ℝ) : 0 < 1 - Real.tanh R ^ 2 * ‖a‖ ^ 2

The denominator is positive at the pseudo-hyperbolic radius Real.tanh R of a hyperbolic ball, whatever the hyperbolic radius R, since Real.tanh takes its values in (-1, 1). This is how every statement about the hyperbolic metric discharges that hypothesis.

theorem TauCeti.pseudoHyperbolicRadius_nonneg {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (hD : 0 < 1 - t ^ 2 * ‖a‖ ^ 2) (ht : 0 ≤ t) : 0 ≤ pseudoHyperbolicRadius a t

The Euclidean radius of a pseudo-hyperbolic ball of nonnegative radius is nonnegative.

theorem TauCeti.pseudoHyperbolicRadius_pos {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (hD : 0 < 1 - t ^ 2 * ‖a‖ ^ 2) (ht : 0 < t) : 0 < pseudoHyperbolicRadius a t

The Euclidean radius of a pseudo-hyperbolic ball of positive radius is positive.

theorem TauCeti.pseudoHyperbolicRadius_neg {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (hD : 0 < 1 - t ^ 2 * ‖a‖ ^ 2) (ht : t < 0) : pseudoHyperbolicRadius a t < 0

A negative pseudo-hyperbolic radius gives a negative Euclidean radius, so that the Euclidean disc it describes is empty — as is the pseudo-hyperbolic ball of radius t.

The Euclidean disc lies inside the unit disc

theorem TauCeti.norm_pseudoHyperbolicCenter_add_pseudoHyperbolicRadius_lt_one {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (ht₀ : 0 ≤ t) (ht₁ : t < 1) : ‖pseudoHyperbolicCenter a t‖ + pseudoHyperbolicRadius a t < 1

A pseudo-hyperbolic ball stays inside the unit disc, quantitatively: the Euclidean centre and radius satisfy ‖c‖ + s < 1, because 1 - ‖c‖ - s = (1 - ‖a‖) * (1 - t) * (1 - t * ‖a‖) / (1 - t ^ 2 * ‖a‖ ^ 2) and each of the three factors is positive.

theorem TauCeti.closedBall_pseudoHyperbolicCenter_subset_ball {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (ht₀ : 0 ≤ t) (ht₁ : t < 1) : Metric.closedBall (pseudoHyperbolicCenter a t) (pseudoHyperbolicRadius a t) ⊆ Metric.ball 0 1

The closed Euclidean disc describing a pseudo-hyperbolic ball is contained in the open unit disc; a fortiori so is the open one.

theorem TauCeti.ball_pseudoHyperbolicCenter_subset_ball {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : Metric.ball (pseudoHyperbolicCenter a t) (pseudoHyperbolicRadius a t) ⊆ Metric.ball 0 1

The open Euclidean disc describing a pseudo-hyperbolic ball is contained in the open unit disc. Unlike TauCeti.closedBall_pseudoHyperbolicCenter_subset_ball this survives the endpoint t = 1, where the Euclidean centre is 0, the Euclidean radius is 1 and the two open discs are equal.

The Apollonius identity

theorem TauCeti.sq_norm_sub_sub_mul_sq_norm_one_sub_conj_mul (a z : ℂ) (t : ℝ) (hD : 1 - t ^ 2 * ‖a‖ ^ 2 ≠ 0) : ‖z - a‖ ^ 2 - t ^ 2 * ‖1 - (starRingEnd ℂ) a * z‖ ^ 2 = (1 - t ^ 2 * ‖a‖ ^ 2) * (‖z - pseudoHyperbolicCenter a t‖ ^ 2 - pseudoHyperbolicRadius a t ^ 2)

The Apollonius identity for the Moebius factor. For every z : ℂ,

‖z - a‖ ^ 2 - t ^ 2 * ‖1 - conj a * z‖ ^ 2 = (1 - t ^ 2 * ‖a‖ ^ 2) * (‖z - pseudoHyperbolicCenter a t‖ ^ 2 - pseudoHyperbolicRadius a t ^ 2).

Both sides are real quadratics in z.re and z.im with the same leading coefficient 1 - t ^ 2 * ‖a‖ ^ 2, and the definitions of TauCeti.pseudoHyperbolicCenter and TauCeti.pseudoHyperbolicRadius are exactly what completes the square. No hypothesis is placed on z, and the disc hypothesis on a enters only through the nonvanishing of the denominator.

Pseudo-hyperbolic balls are Euclidean discs

theorem TauCeti.pseudoHyperbolicExpr_lt_iff_mem_ball {a z : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (hz : ‖z‖ < 1) (hD : 0 < 1 - t ^ 2 * ‖a‖ ^ 2) : pseudoHyperbolicExpr z a < t ↔ z ∈ Metric.ball (pseudoHyperbolicCenter a t) (pseudoHyperbolicRadius a t)

The pseudo-hyperbolic ball is a Euclidean disc. A point z of the unit disc satisfies pseudoHyperbolicExpr z a < t exactly when it lies in the Euclidean disc of centre TauCeti.pseudoHyperbolicCenter a t and radius TauCeti.pseudoHyperbolicRadius a t.

Clearing the Moebius denominator — legitimate because z and a lie in the disc — turns the left-hand condition into ‖z - a‖ < t * ‖1 - conj a * z‖, and squaring both sides makes TauCeti.sq_norm_sub_sub_mul_sq_norm_one_sub_conj_mul applicable; the factor 1 - t ^ 2 * ‖a‖ ^ 2 it produces is positive by hypothesis, so it does not affect the sign.

Positivity of that factor is all that is asked of t; it holds in particular for every t ∈ [-1, 1] (TauCeti.one_sub_sq_mul_sq_norm_pos), and for every real t when a = 0. A negative t is allowed and makes both sides empty, the Euclidean radius being negative.

theorem TauCeti.pseudoHyperbolicExpr_le_iff_mem_closedBall {a z : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (hz : ‖z‖ < 1) (hD : 0 < 1 - t ^ 2 * ‖a‖ ^ 2) : pseudoHyperbolicExpr z a ≤ t ↔ z ∈ Metric.closedBall (pseudoHyperbolicCenter a t) (pseudoHyperbolicRadius a t)

The closed pseudo-hyperbolic ball is a closed Euclidean disc, the ≤ companion of TauCeti.pseudoHyperbolicExpr_lt_iff_mem_ball with the same proof, and under the same hypothesis: at t = 1 the closed Euclidean disc is the closed unit disc, and for t < 0 both sides are empty.

theorem TauCeti.pseudoHyperbolicExpr_eq_iff_mem_sphere {a z : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (hz : ‖z‖ < 1) (hD : 0 < 1 - t ^ 2 * ‖a‖ ^ 2) : pseudoHyperbolicExpr z a = t ↔ z ∈ Metric.sphere (pseudoHyperbolicCenter a t) (pseudoHyperbolicRadius a t)

The pseudo-hyperbolic circle is a Euclidean circle. A point z of the unit disc satisfies pseudoHyperbolicExpr z a = t exactly when it lies on the Euclidean circle of centre TauCeti.pseudoHyperbolicCenter a t and radius TauCeti.pseudoHyperbolicRadius a t: the level set is what the closed disc has and the open one has not. The endpoint t = 1 is allowed, and there — as for t < 0 — both sides are empty.

Both directions are the antisymmetry of ≤ (le_antisymm_iff), with the missing inequality supplied by the < statement through not_lt.

theorem TauCeti.mem_ball_pseudoHyperbolicCenter {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (hD : 0 < 1 - t ^ 2 * ‖a‖ ^ 2) (ht : 0 < t) : a ∈ Metric.ball (pseudoHyperbolicCenter a t) (pseudoHyperbolicRadius a t)

The hyperbolic centre of a ball of positive radius lies in the Euclidean disc describing it — off centre, but inside.

theorem TauCeti.sep_ball_pseudoHyperbolicExpr_lt_eq_ball {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (hD : 0 < 1 - t ^ 2 * ‖a‖ ^ 2) (ht₁ : t ≤ 1) : {z : ℂ | z ∈ Metric.ball 0 1 ∧ pseudoHyperbolicExpr z a < t} = Metric.ball (pseudoHyperbolicCenter a t) (pseudoHyperbolicRadius a t)

A pseudo-hyperbolic ball of the unit disc is a Euclidean disc, in set form. Beyond the positivity of 1 - t ^ 2 * ‖a‖ ^ 2 shared with the pointwise form, only an upper bound on t is needed, so that the Euclidean disc lies inside 𝔻. The endpoint t = 1 is allowed, and there both sides are the unit disc; for t < 0 both sides are empty.

theorem TauCeti.sep_ball_pseudoHyperbolicExpr_le_eq_closedBall {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (hD : 0 < 1 - t ^ 2 * ‖a‖ ^ 2) (ht₁ : t < 1) : {z : ℂ | z ∈ Metric.ball 0 1 ∧ pseudoHyperbolicExpr z a ≤ t} = Metric.closedBall (pseudoHyperbolicCenter a t) (pseudoHyperbolicRadius a t)

A closed pseudo-hyperbolic ball of the unit disc is a closed Euclidean disc, in set form. As for TauCeti.sep_ball_pseudoHyperbolicExpr_lt_eq_ball the radius is bounded only from above, here strictly, since at t = 1 the closed Euclidean disc would meet the unit circle. For t < 0 both sides are empty.

theorem TauCeti.sep_ball_pseudoHyperbolicExpr_eq_eq_sphere {a : ℂ} {t : ℝ} (ha : ‖a‖ < 1) (hD : 0 < 1 - t ^ 2 * ‖a‖ ^ 2) (ht₁ : t < 1) : {z : ℂ | z ∈ Metric.ball 0 1 ∧ pseudoHyperbolicExpr z a = t} = Metric.sphere (pseudoHyperbolicCenter a t) (pseudoHyperbolicRadius a t)

A pseudo-hyperbolic circle of the unit disc is a Euclidean circle: the level set is the difference of the closed and the open disc. The hypotheses are those of TauCeti.sep_ball_pseudoHyperbolicExpr_le_eq_closedBall, of which this is the boundary part. For t < 0 both sides are empty.

Hyperbolic balls

theorem TauCeti.hyperbolicDist_lt_iff_pseudoHyperbolicExpr_lt_tanh {a z : ℂ} {R : ℝ} (ha : ‖a‖ < 1) (hz : ‖z‖ < 1) : hyperbolicDist z a < R ↔ pseudoHyperbolicExpr z a < Real.tanh R

The hyperbolic distance is below R exactly when the pseudo-hyperbolic expression is below Real.tanh R: the hyperbolic distance is Real.artanh of the pseudo-hyperbolic expression, and Real.artanh is the increasing inverse of Real.tanh.

theorem TauCeti.hyperbolicDist_le_iff_pseudoHyperbolicExpr_le_tanh {a z : ℂ} {R : ℝ} (ha : ‖a‖ < 1) (hz : ‖z‖ < 1) : hyperbolicDist z a ≤ R ↔ pseudoHyperbolicExpr z a ≤ Real.tanh R

The ≤ companion of TauCeti.hyperbolicDist_lt_iff_pseudoHyperbolicExpr_lt_tanh.

theorem TauCeti.hyperbolicDist_eq_iff_pseudoHyperbolicExpr_eq_tanh {a z : ℂ} {R : ℝ} (ha : ‖a‖ < 1) (hz : ‖z‖ < 1) : hyperbolicDist z a = R ↔ pseudoHyperbolicExpr z a = Real.tanh R

The hyperbolic distance equals R exactly when the pseudo-hyperbolic expression equals Real.tanh R, the = companion of TauCeti.hyperbolicDist_lt_iff_pseudoHyperbolicExpr_lt_tanh.

theorem TauCeti.sep_ball_hyperbolicDist_lt_eq_ball {a : ℂ} {R : ℝ} (ha : ‖a‖ < 1) : {z : ℂ | z ∈ Metric.ball 0 1 ∧ hyperbolicDist z a < R} = Metric.ball (pseudoHyperbolicCenter a (Real.tanh R)) (pseudoHyperbolicRadius a (Real.tanh R))

A hyperbolic ball of the Poincaré disc is a Euclidean disc. The hyperbolic ball of centre a and radius R is the Euclidean disc of centre pseudoHyperbolicCenter a (Real.tanh R) and radius pseudoHyperbolicRadius a (Real.tanh R); for R < 0 both sides are empty, the Euclidean radius being negative.

The Euclidean centre is a only for a = 0 or R = 0; for a ≠ 0 the hyperbolic ball is an off-centre Euclidean disc, pulled towards the origin. For a = 0 the Euclidean centre is the origin and the Euclidean radius is Real.tanh R (TauCeti.pseudoHyperbolicCenter_zero_left, TauCeti.pseudoHyperbolicRadius_zero_left).

theorem TauCeti.sep_ball_hyperbolicDist_le_eq_closedBall {a : ℂ} {R : ℝ} (ha : ‖a‖ < 1) : {z : ℂ | z ∈ Metric.ball 0 1 ∧ hyperbolicDist z a ≤ R} = Metric.closedBall (pseudoHyperbolicCenter a (Real.tanh R)) (pseudoHyperbolicRadius a (Real.tanh R))

A closed hyperbolic ball of the Poincaré disc is a closed Euclidean disc, the ≤ companion of TauCeti.sep_ball_hyperbolicDist_lt_eq_ball.

Specialising to a = 0 recovers TauCeti.hyperbolicDist_zero_le_iff_norm_le_tanh of Poincare/Topology.lean: the Euclidean centre is then the origin and the Euclidean radius is Real.tanh R.

theorem TauCeti.sep_ball_hyperbolicDist_eq_eq_sphere {a : ℂ} {R : ℝ} (ha : ‖a‖ < 1) : {z : ℂ | z ∈ Metric.ball 0 1 ∧ hyperbolicDist z a = R} = Metric.sphere (pseudoHyperbolicCenter a (Real.tanh R)) (pseudoHyperbolicRadius a (Real.tanh R))

A hyperbolic circle of the Poincaré disc is a Euclidean circle, the = companion of TauCeti.sep_ball_hyperbolicDist_lt_eq_ball.

theorem TauCeti.convex_sep_ball_hyperbolicDist_lt {a : ℂ} {R : ℝ} (ha : ‖a‖ < 1) : Convex ℝ {z : ℂ | z ∈ Metric.ball 0 1 ∧ hyperbolicDist z a < R}

Hyperbolic balls are Euclidean-convex. Being Euclidean discs, the balls of the hyperbolic metric are convex for the linear structure of ℂ. This is a different notion from the geodesic convexity of the hyperbolic metric, which is a separate statement about the hyperbolic geodesics of Poincare/Geodesic.lean: it is convexity for the Euclidean structure, and it has no proof internal to the hyperbolic metric.

theorem TauCeti.PoincareDisc.mem_ball_iff {R : ℝ} (x w : PoincareDisc) : w ∈ Metric.ball x R ↔ ↑(toUnitDisc w) ∈ Metric.ball (pseudoHyperbolicCenter (↑(toUnitDisc x)) (Real.tanh R)) (pseudoHyperbolicRadius (↑(toUnitDisc x)) (Real.tanh R))

The balls of the Poincaré metric space, read on the Euclidean disc. A point of TauCeti.PoincareDisc lies in the hyperbolic ball of centre x and radius R exactly when its Euclidean coordinate lies in the corresponding Euclidean disc; for R < 0 both sides are empty.

theorem TauCeti.PoincareDisc.mem_closedBall_iff {R : ℝ} (x w : PoincareDisc) : w ∈ Metric.closedBall x R ↔ ↑(toUnitDisc w) ∈ Metric.closedBall (pseudoHyperbolicCenter (↑(toUnitDisc x)) (Real.tanh R)) (pseudoHyperbolicRadius (↑(toUnitDisc x)) (Real.tanh R))

The closed balls of the Poincaré metric space, read on the Euclidean disc, the ≤ companion of TauCeti.PoincareDisc.mem_ball_iff.

theorem TauCeti.PoincareDisc.mem_sphere_iff {R : ℝ} (x w : PoincareDisc) : w ∈ Metric.sphere x R ↔ ↑(toUnitDisc w) ∈ Metric.sphere (pseudoHyperbolicCenter (↑(toUnitDisc x)) (Real.tanh R)) (pseudoHyperbolicRadius (↑(toUnitDisc x)) (Real.tanh R))

The spheres of the Poincaré metric space, read on the Euclidean disc, the = companion of TauCeti.PoincareDisc.mem_ball_iff.