The triangle inequality for the hyperbolic distance on the unit disc

This file proves the triangle inequality for the hyperbolic (Poincaré) distance hyperbolicDist on the complex open unit disc, the metric-completeness step deferred in HyperbolicDistance.lean.

The core analytic input is the strong triangle-type inequality for the pseudo-hyperbolic expression pseudoHyperbolicExpr z w = ‖(z - w) / (1 - conj w * z)‖, taken here in its origin-centred form pseudoHyperbolicExpr z w ≤ (‖z‖ + ‖w‖) / (1 + ‖z‖ * ‖w‖) (pseudoHyperbolicExpr_le_add_div_one_add_mul_of_norm_lt_one). Squaring, this rests on the factorisation ((‖z‖ + ‖w‖) ‖1 - conj w z‖) ^ 2 - (‖z - w‖ (1 + ‖z‖ ‖w‖)) ^ 2 = 2 (1 - ‖z‖ ^ 2)(1 - ‖w‖ ^ 2)(‖z‖ ‖w‖ + (z conj w).re), each factor of which is nonnegative on the disc.

The same factorisation, read as an equation rather than as a sign, says when the inequality is tight: the first two factors are strictly positive on the disc, so equality holds exactly when (z * conj w).re = -(‖z‖ * ‖w‖), that is exactly when z and w point in opposite directions. Flipping the sign of the difference ‖z‖ - ‖w‖ throughout gives the mirror statements — the reverse triangle inequality |‖z‖ - ‖w‖| / (1 - ‖z‖ * ‖w‖) ≤ pseudoHyperbolicExpr z w and its own equality case (z * conj w).re = ‖z‖ * ‖w‖, that is z and w pointing in the same direction. These two equality cases are what identify the degenerate hyperbolic triangles, and hence the hyperbolic geodesics, in Conformal/Poincare/Betweenness.lean.

Passing to the hyperbolic distance hyperbolicDist = artanh ∘ pseudoHyperbolicExpr uses the addition formula for the inverse hyperbolic tangent, Real.artanh a + Real.artanh b = Real.artanh ((a + b) / (1 + a * b)) (Real.artanh_add, proved in TauCeti/Analysis/SpecialFunctions/Artanh.lean), together with the isometry invariance of hyperbolicDist under the disc Moebius factors (hyperbolicDist_unitDiscMoebius): the general triangle inequality is reduced to the origin case by sending the middle point to 0.

Main results:

• pseudoHyperbolicExpr_le_add_div_one_add_mul_of_norm_lt_one — the strong pseudo-hyperbolic triangle inequality against the origin, and pseudoHyperbolicExpr_eq_add_div_one_add_mul_iff_of_norm_lt_one — its equality case;
• abs_sub_div_one_sub_mul_le_pseudoHyperbolicExpr_of_norm_lt_one — the reverse pseudo-hyperbolic triangle inequality against the origin, and pseudoHyperbolicExpr_eq_abs_sub_div_one_sub_mul_iff_of_norm_lt_one — its equality case;
• hyperbolicDist_triangle_zero — the hyperbolic triangle inequality with the origin as the middle point;
• hyperbolicDist_triangle / hyperbolicDist_triangle_unitDisc — the full hyperbolic triangle inequality hyperbolicDist z w ≤ hyperbolicDist z u + hyperbolicDist u w, in ball and bundled Complex.UnitDisc form;
• pseudoHyperbolicExpr_le_add_div_one_add_mul and abs_sub_div_one_sub_mul_le_pseudoHyperbolicExpr — the same two pseudo-hyperbolic inequalities with an arbitrary middle point u in place of the origin, with their equality cases pseudoHyperbolicExpr_eq_add_div_one_add_mul_iff and pseudoHyperbolicExpr_eq_abs_sub_div_one_sub_mul_iff;
• pseudoHyperbolicExpr_triangle — the plain triangle inequality pseudoHyperbolicExpr z w ≤ pseudoHyperbolicExpr z u + pseudoHyperbolicExpr u w, so that the pseudo-hyperbolic expression is itself a metric on the disc and not merely a monotone reparametrisation of one.

Each of those five carries a hypothesis-free Complex.UnitDisc form, named by the suffix _unitDisc.

Together with the symmetry, nonnegativity and vanishing-on-the-diagonal lemmas already in HyperbolicDistance.lean, these give the metric-space axioms for hyperbolicDist on the open unit disc. A MetricSpace instance is deliberately not registered on Complex.UnitDisc, which already carries the Euclidean subspace metric; recording the Poincaré metric as an instance would require a dedicated type synonym and is left to future work.

The origin plays no role in the pseudo-hyperbolic statements: the whole point of pseudoHyperbolicExpr is that it is invariant under the disc Moebius factors (pseudoHyperbolicExpr_unitDiscMoebiusFormula_of_norm_lt_one), which act transitively. The last group of results above therefore removes it, and does so without repeating the transport argument: since hyperbolicDist = artanh ∘ pseudoHyperbolicExpr and artanh is a strictly monotone bijection (-1, 1) ≃ ℝ, an inequality between pseudo-hyperbolic expressions is equivalent to the corresponding inequality between hyperbolic distances, and the addition formula Real.artanh_add is exactly the dictionary translating the additive law d(z, u) + d(u, w) into the Moebius law (a + b) / (1 + a b). So the general forms are read off hyperbolicDist_triangle — which is where the transport already happened — and their equality cases off the injectivity of artanh.

This advances the conformal-mapping roadmap's L2 target "the hyperbolic / Poincaré metric on 𝔻" (see ConformalMapping/README.md). It reuses Tau Ceti's pseudo-hyperbolic, Moebius and Schwarz--Pick API. As with the rest of the L0--L3 conformal-mapping material, it is coordinated with the upstream Mathlib RMT effort leanprover-community/mathlib4#33505 and should be refactored to upstream API if that work lands a human-curated Poincaré metric.

theorem TauCeti.pseudoHyperbolicExpr_le_add_div_one_add_mul_of_norm_lt_one {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : pseudoHyperbolicExpr z w ≤ (‖z‖ + ‖w‖) / (1 + ‖z‖ * ‖w‖)

Strong pseudo-hyperbolic triangle inequality (origin form). For two points of the open unit disc, pseudoHyperbolicExpr z w ≤ (‖z‖ + ‖w‖) / (1 + ‖z‖ * ‖w‖). This is the ρ(z, w) ≤ (ρ(z, 0) + ρ(0, w)) / (1 + ρ(z, 0) ρ(0, w)) form of the pseudo-hyperbolic triangle inequality.

theorem TauCeti.pseudoHyperbolicExpr_eq_add_div_one_add_mul_iff_of_norm_lt_one {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : pseudoHyperbolicExpr z w = (‖z‖ + ‖w‖) / (1 + ‖z‖ * ‖w‖) ↔ (z * (starRingEnd ℂ) w).re = -(‖z‖ * ‖w‖)

Equality in the strong pseudo-hyperbolic triangle inequality against the origin. For two points of the open unit disc, pseudoHyperbolicExpr z w = (‖z‖ + ‖w‖) / (1 + ‖z‖ * ‖w‖) holds exactly when (z * conj w).re = -(‖z‖ * ‖w‖), that is (by the equality case of Complex.abs_re_le_norm) exactly when z and w point in opposite directions.

The two sides of the inequality are quotients of nonnegative reals with positive denominators, so they agree exactly when the cross-multiplied products do, hence exactly when the squares of those products do; and the shared defect identity displays that difference of squares as 2 (1 - ‖z‖ ^ 2)(1 - ‖w‖ ^ 2)(‖z‖ ‖w‖ + (z conj w).re), whose first two factors are positive on the disc.

theorem TauCeti.abs_sub_div_one_sub_mul_le_pseudoHyperbolicExpr_of_norm_lt_one {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : |‖z‖ - ‖w‖| / (1 - ‖z‖ * ‖w‖) ≤ pseudoHyperbolicExpr z w

Reverse strong pseudo-hyperbolic triangle inequality (origin form). For two points of the open unit disc, |‖z‖ - ‖w‖| / (1 - ‖z‖ * ‖w‖) ≤ pseudoHyperbolicExpr z w. This is the pseudo-hyperbolic form of |d(z, 0) - d(0, w)| ≤ d(z, w), the reverse triangle inequality against the origin, and it rests on the mirror factorisation (‖z - w‖ (1 - ‖z‖ ‖w‖)) ^ 2 - (|‖z‖ - ‖w‖| ‖1 - conj w z‖) ^ 2 = 2 (1 - ‖z‖ ^ 2)(1 - ‖w‖ ^ 2)(‖z‖ ‖w‖ - (z conj w).re) of the one behind pseudoHyperbolicExpr_le_add_div_one_add_mul_of_norm_lt_one.

theorem TauCeti.pseudoHyperbolicExpr_eq_abs_sub_div_one_sub_mul_iff_of_norm_lt_one {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : pseudoHyperbolicExpr z w = |‖z‖ - ‖w‖| / (1 - ‖z‖ * ‖w‖) ↔ (z * (starRingEnd ℂ) w).re = ‖z‖ * ‖w‖

Equality in the reverse pseudo-hyperbolic triangle inequality against the origin. For two points of the open unit disc, pseudoHyperbolicExpr z w = |‖z‖ - ‖w‖| / (1 - ‖z‖ * ‖w‖) holds exactly when (z * conj w).re = ‖z‖ * ‖w‖, that is exactly when z and w point in the same direction. Together with TauCeti.pseudoHyperbolicExpr_eq_add_div_one_add_mul_iff_of_norm_lt_one this pins down the two degenerate positions of a hyperbolic triangle with a vertex at the origin.

theorem TauCeti.hyperbolicDist_triangle_zero {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : hyperbolicDist z w ≤ hyperbolicDist z 0 + hyperbolicDist 0 w

Hyperbolic triangle inequality against the origin. For two points of the open unit disc, hyperbolicDist z w ≤ hyperbolicDist z 0 + hyperbolicDist 0 w.

theorem TauCeti.hyperbolicDist_triangle_unitDisc (u z w : Complex.UnitDisc) : hyperbolicDist ↑z ↑w ≤ hyperbolicDist ↑z ↑u + hyperbolicDist ↑u ↑w

Hyperbolic triangle inequality (bundled unit-disc form). hyperbolicDist z w ≤ hyperbolicDist z u + hyperbolicDist u w, proved by sending the middle point u to the origin with the Moebius isometry unitDiscMoebius u.

theorem TauCeti.hyperbolicDist_triangle {z w u : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) (hu : u ∈ Metric.ball 0 1) : hyperbolicDist z w ≤ hyperbolicDist z u + hyperbolicDist u w

Hyperbolic triangle inequality. The hyperbolic (Poincaré) distance on the complex open unit disc satisfies hyperbolicDist z w ≤ hyperbolicDist z u + hyperbolicDist u w.

The pseudo-hyperbolic inequalities at an arbitrary middle point

theorem TauCeti.pseudoHyperbolicExpr_le_add_div_one_add_mul {z w u : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) (hu : ‖u‖ < 1) : pseudoHyperbolicExpr z w ≤ (pseudoHyperbolicExpr z u + pseudoHyperbolicExpr u w) / (1 + pseudoHyperbolicExpr z u * pseudoHyperbolicExpr u w)

The strong pseudo-hyperbolic triangle inequality. For three points of the open unit disc, ρ(z, w) ≤ (ρ(z, u) + ρ(u, w)) / (1 + ρ(z, u) ρ(u, w)), where ρ = pseudoHyperbolicExpr. This is TauCeti.pseudoHyperbolicExpr_le_add_div_one_add_mul_of_norm_lt_one with the middle point freed from the origin: taking u = 0 and rewriting ρ(z, 0) = ‖z‖, ρ(0, w) = ‖w‖ (TauCeti.pseudoHyperbolicExpr_zero_right, TauCeti.pseudoHyperbolicExpr_zero_left) returns that statement.

The right-hand side is the Moebius sum of ρ(z, u) and ρ(u, w), the operation under which artanh carries ordinary addition. It is the sharp bound; TauCeti.pseudoHyperbolicExpr_triangle below is the weaker plain form.

theorem TauCeti.pseudoHyperbolicExpr_le_add_div_one_add_mul_unitDisc (z w u : Complex.UnitDisc) : pseudoHyperbolicExpr ↑z ↑w ≤ (pseudoHyperbolicExpr ↑z ↑u + pseudoHyperbolicExpr ↑u ↑w) / (1 + pseudoHyperbolicExpr ↑z ↑u * pseudoHyperbolicExpr ↑u ↑w)

The strong pseudo-hyperbolic triangle inequality (bundled unit-disc form). The hypothesis-free form of TauCeti.pseudoHyperbolicExpr_le_add_div_one_add_mul for points of Complex.UnitDisc.

theorem TauCeti.pseudoHyperbolicExpr_eq_add_div_one_add_mul_iff {z w u : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) (hu : ‖u‖ < 1) : pseudoHyperbolicExpr z w = (pseudoHyperbolicExpr z u + pseudoHyperbolicExpr u w) / (1 + pseudoHyperbolicExpr z u * pseudoHyperbolicExpr u w) ↔ hyperbolicDist z w = hyperbolicDist z u + hyperbolicDist u w

Equality in the strong pseudo-hyperbolic triangle inequality. The bound of TauCeti.pseudoHyperbolicExpr_le_add_div_one_add_mul is attained exactly on the degenerate hyperbolic triangles, those with hyperbolicDist z w = hyperbolicDist z u + hyperbolicDist u w, that is exactly when u lies on the hyperbolic geodesic segment from z to w.

theorem TauCeti.pseudoHyperbolicExpr_eq_add_div_one_add_mul_iff_unitDisc (z w u : Complex.UnitDisc) : pseudoHyperbolicExpr ↑z ↑w = (pseudoHyperbolicExpr ↑z ↑u + pseudoHyperbolicExpr ↑u ↑w) / (1 + pseudoHyperbolicExpr ↑z ↑u * pseudoHyperbolicExpr ↑u ↑w) ↔ hyperbolicDist ↑z ↑w = hyperbolicDist ↑z ↑u + hyperbolicDist ↑u ↑w

Equality in the strong pseudo-hyperbolic triangle inequality (bundled unit-disc form). The hypothesis-free form of TauCeti.pseudoHyperbolicExpr_eq_add_div_one_add_mul_iff for points of Complex.UnitDisc.

theorem TauCeti.pseudoHyperbolicExpr_triangle {z w u : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) (hu : ‖u‖ < 1) : pseudoHyperbolicExpr z w ≤ pseudoHyperbolicExpr z u + pseudoHyperbolicExpr u w

The pseudo-hyperbolic triangle inequality. For three points of the open unit disc, ρ(z, w) ≤ ρ(z, u) + ρ(u, w): the Moebius sum bounding ρ(z, w) in TauCeti.pseudoHyperbolicExpr_le_add_div_one_add_mul has denominator at least 1, so it is at most the ordinary sum.

With TauCeti.pseudoHyperbolicExpr_comm, TauCeti.pseudoHyperbolicExpr_self and TauCeti.pseudoHyperbolicExpr_eq_zero_iff_of_norm_lt_one this makes pseudoHyperbolicExpr a metric on the open unit disc in its own right, and not only a monotone reparametrisation of one. The Moebius sum is the sharp bound, so this weaker form is the one to quote when the denominator is a nuisance and the sharpness is not needed.

theorem TauCeti.pseudoHyperbolicExpr_triangle_unitDisc (z w u : Complex.UnitDisc) : pseudoHyperbolicExpr ↑z ↑w ≤ pseudoHyperbolicExpr ↑z ↑u + pseudoHyperbolicExpr ↑u ↑w

The pseudo-hyperbolic triangle inequality (bundled unit-disc form). The hypothesis-free form of TauCeti.pseudoHyperbolicExpr_triangle for points of Complex.UnitDisc, which together with TauCeti.pseudoHyperbolicExpr_comm, TauCeti.pseudoHyperbolicExpr_self and TauCeti.pseudoHyperbolicExpr_eq_zero_iff_unitDisc gives the metric axioms for pseudoHyperbolicExpr on that type.

theorem TauCeti.abs_sub_div_one_sub_mul_le_pseudoHyperbolicExpr {z w u : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) (hu : ‖u‖ < 1) : |pseudoHyperbolicExpr z u - pseudoHyperbolicExpr u w| / (1 - pseudoHyperbolicExpr z u * pseudoHyperbolicExpr u w) ≤ pseudoHyperbolicExpr z w

The reverse strong pseudo-hyperbolic triangle inequality. For three points of the open unit disc, |ρ(z, u) - ρ(u, w)| / (1 - ρ(z, u) ρ(u, w)) ≤ ρ(z, w). This is TauCeti.abs_sub_div_one_sub_mul_le_pseudoHyperbolicExpr_of_norm_lt_one with the middle point freed from the origin, in the same sense as TauCeti.pseudoHyperbolicExpr_le_add_div_one_add_mul.

theorem TauCeti.abs_sub_div_one_sub_mul_le_pseudoHyperbolicExpr_unitDisc (z w u : Complex.UnitDisc) : |pseudoHyperbolicExpr ↑z ↑u - pseudoHyperbolicExpr ↑u ↑w| / (1 - pseudoHyperbolicExpr ↑z ↑u * pseudoHyperbolicExpr ↑u ↑w) ≤ pseudoHyperbolicExpr ↑z ↑w

The reverse strong pseudo-hyperbolic triangle inequality (bundled unit-disc form). The hypothesis-free form of TauCeti.abs_sub_div_one_sub_mul_le_pseudoHyperbolicExpr for points of Complex.UnitDisc.

theorem TauCeti.pseudoHyperbolicExpr_eq_abs_sub_div_one_sub_mul_iff {z w u : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) (hu : ‖u‖ < 1) : pseudoHyperbolicExpr z w = |pseudoHyperbolicExpr z u - pseudoHyperbolicExpr u w| / (1 - pseudoHyperbolicExpr z u * pseudoHyperbolicExpr u w) ↔ hyperbolicDist z u = hyperbolicDist z w + hyperbolicDist w u ∨ hyperbolicDist u w = hyperbolicDist u z + hyperbolicDist z w

Equality in the reverse strong pseudo-hyperbolic triangle inequality. The bound of TauCeti.abs_sub_div_one_sub_mul_le_pseudoHyperbolicExpr is attained exactly when one of z, w lies on the hyperbolic geodesic segment joining u to the other — the two degenerate positions in which the triangle collapses with u outside, rather than inside, the segment [z, w].

theorem TauCeti.pseudoHyperbolicExpr_eq_abs_sub_div_one_sub_mul_iff_unitDisc (z w u : Complex.UnitDisc) : pseudoHyperbolicExpr ↑z ↑w = |pseudoHyperbolicExpr ↑z ↑u - pseudoHyperbolicExpr ↑u ↑w| / (1 - pseudoHyperbolicExpr ↑z ↑u * pseudoHyperbolicExpr ↑u ↑w) ↔ hyperbolicDist ↑z ↑u = hyperbolicDist ↑z ↑w + hyperbolicDist ↑w ↑u ∨ hyperbolicDist ↑u ↑w = hyperbolicDist ↑u ↑z + hyperbolicDist ↑z ↑w

Equality in the reverse strong pseudo-hyperbolic triangle inequality (bundled unit-disc form). The hypothesis-free form of TauCeti.pseudoHyperbolicExpr_eq_abs_sub_div_one_sub_mul_iff for points of Complex.UnitDisc.