The pseudo-hyperbolic expression on the unit disc

This file records the scalar pseudo-hyperbolic expression ‖(z - w) / (1 - conj w * z)‖, on which the Schwarz--Pick lemma and the hyperbolic distance on the disc are built. The main API proves that the denominator is nonzero on the open unit disc — hence of positive norm (TauCeti.norm_one_sub_conj_mul_pos_of_norm_lt_one), a positivity side condition used when manipulating inequalities involving that denominator — that the hyperbolic defect 1 - ‖z‖ ^ 2 is positive there (TauCeti.one_sub_sq_norm_pos_of_norm_lt_one), that the expression is symmetric, that it is strictly less than one for two points of the unit disc — hence lies in Ioo (-1) 1 (TauCeti.pseudoHyperbolicExpr_mem_Ioo_of_norm_lt_one), the interval on which Real.artanh is a bijection onto ℝ — and that it is jointly continuous there (TauCeti.continuousOn_pseudoHyperbolicExpr). The Poincaré defect identity TauCeti.norm_sq_one_sub_conj_mul_sub_norm_sq_sub compares the numerator and the denominator, and yields TauCeti.norm_sub_eq_of_pseudoHyperbolicExpr_eq: between points of prescribed norms, the pseudo-hyperbolic expression determines the Euclidean distance.

References

• The Riemann mapping theorem development of leanprover-community/mathlib4#33505, and the parts of it already in Mathlib: Mathlib/Analysis/Complex/RiemannMapping.lean and Mathlib/Analysis/Complex/BranchLogRoot.lean.

noncomputable def TauCeti.pseudoHyperbolicExpr (z w : ℂ) : ℝ

The pseudo-hyperbolic expression on ℂ, written as a total real-valued function.

On the open unit disc this is the pseudo-hyperbolic expression. Outside the disc the same formula is still meaningful as a total expression in Lean, with division by zero evaluating to zero as usual.

Equations

• TauCeti.pseudoHyperbolicExpr z w = ‖(z - w) / (1 - (starRingEnd ℂ) w * z)‖

theorem TauCeti.pseudoHyperbolicExpr_def (z w : ℂ) : pseudoHyperbolicExpr z w = ‖(z - w) / (1 - (starRingEnd ℂ) w * z)‖

The defining formula for the pseudo-hyperbolic expression.

theorem TauCeti.pseudoHyperbolicExpr_eq_norm_div_norm (z w : ℂ) : pseudoHyperbolicExpr z w = ‖z - w‖ / ‖1 - (starRingEnd ℂ) w * z‖

The pseudo-hyperbolic expression as a quotient of two real norms, the form in which it is compared with the Euclidean distance ‖z - w‖.

@[simp]

theorem TauCeti.pseudoHyperbolicExpr_nonneg (z w : ℂ) : 0 ≤ pseudoHyperbolicExpr z w

@[simp]

theorem TauCeti.pseudoHyperbolicExpr_self (z : ℂ) : pseudoHyperbolicExpr z z = 0

The pseudo-hyperbolic expression from a point to itself is zero.

theorem TauCeti.pseudoHyperbolicExpr_comm (z w : ℂ) : pseudoHyperbolicExpr z w = pseudoHyperbolicExpr w z

The pseudo-hyperbolic expression is symmetric in its two arguments.

@[simp]

theorem TauCeti.pseudoHyperbolicExpr_conj (z w : ℂ) : pseudoHyperbolicExpr ((starRingEnd ℂ) z) ((starRingEnd ℂ) w) = pseudoHyperbolicExpr z w

Conjugation invariance. Conjugating both arguments leaves the pseudo-hyperbolic expression unchanged: conjugation is the orientation-reversing symmetry of the disc.

theorem TauCeti.pseudoHyperbolicExpr_eq_zero_of_eq {z w : ℂ} (h : z = w) : pseudoHyperbolicExpr z w = 0

If the two points are equal, their pseudo-hyperbolic expression is zero.

@[simp]

theorem TauCeti.pseudoHyperbolicExpr_zero_right (z : ℂ) : pseudoHyperbolicExpr z 0 = ‖z‖

The pseudo-hyperbolic expression with right endpoint zero is the norm.

@[simp]

theorem TauCeti.pseudoHyperbolicExpr_zero_left (w : ℂ) : pseudoHyperbolicExpr 0 w = ‖w‖

The pseudo-hyperbolic expression with left endpoint zero is the norm.

@[simp]

theorem TauCeti.pseudoHyperbolicExpr_const_mul {c : ℂ} (hc : ‖c‖ = 1) (z w : ℂ) : pseudoHyperbolicExpr (c * z) (c * w) = pseudoHyperbolicExpr z w

Rotation invariance. Multiplying both arguments by a unit-modulus constant leaves the pseudo-hyperbolic expression unchanged. This is a purely algebraic identity valid for all z, w; it is the rotation half of the disc-automorphism group.

theorem TauCeti.pseudoHyperbolicExpr_eq_zero_iff_of_den_ne_zero {z w : ℂ} (hden : 1 - (starRingEnd ℂ) w * z ≠ 0) : pseudoHyperbolicExpr z w = 0 ↔ z = w

If the denominator is nonzero, zero pseudo-hyperbolic expression characterizes equality.

theorem TauCeti.one_sub_conj_mul_ne_zero_of_norm_lt_one {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : 1 - (starRingEnd ℂ) w * z ≠ 0

On the open unit disc, the denominator in the pseudo-hyperbolic expression is nonzero.

theorem TauCeti.sub_ne_zero_and_one_sub_conj_mul_ne_zero_of_norm_lt_one_of_norm_eq_one {w z : ℂ} (hw : ‖w‖ < 1) (hz : ‖z‖ = 1) : z - w ≠ 0 ∧ 1 - (starRingEnd ℂ) w * z ≠ 0

If one point is inside the unit disc and the other is on its boundary, both the pseudo-hyperbolic numerator and denominator are nonzero.

theorem TauCeti.one_sub_conj_mul_ne_zero_of_mem_ball {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : 1 - (starRingEnd ℂ) w * z ≠ 0

For points in the open unit ball, the denominator in the pseudo-hyperbolic expression is nonzero.

theorem TauCeti.one_sub_conj_mul_ne_zero_unitDisc (z w : Complex.UnitDisc) : 1 - (starRingEnd ℂ) ↑w * ↑z ≠ 0

For bundled unit-disc points, the denominator in the pseudo-hyperbolic expression is nonzero.

theorem TauCeti.one_sub_sq_norm_pos_of_norm_lt_one {z : ℂ} (hz : ‖z‖ < 1) : 0 < 1 - ‖z‖ ^ 2

On the open unit disc, the hyperbolic defect 1 - ‖z‖ ^ 2 is positive.

theorem TauCeti.norm_one_sub_conj_mul_pos_of_norm_lt_one {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : 0 < ‖1 - (starRingEnd ℂ) w * z‖

On the open unit disc, the denominator in the pseudo-hyperbolic expression has positive norm. This is a positivity side condition used when manipulating inequalities involving this denominator.

theorem TauCeti.norm_one_sub_conj_mul_self_of_norm_le_one {w : ℂ} (hw : ‖w‖ ≤ 1) : ‖1 - (starRingEnd ℂ) w * w‖ = 1 - ‖w‖ ^ 2

For a point of norm at most one, the denominator of the Moebius factor evaluated at the factor's own center has norm 1 - ‖w‖ ^ 2.

theorem TauCeti.pseudoHyperbolicExpr_eq_zero_iff_of_norm_lt_one {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : pseudoHyperbolicExpr z w = 0 ↔ z = w

On the open unit disc, zero pseudo-hyperbolic expression characterizes equality.

theorem TauCeti.pseudoHyperbolicExpr_eq_zero_iff_of_mem_ball {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : pseudoHyperbolicExpr z w = 0 ↔ z = w

For points in the open unit ball, zero pseudo-hyperbolic expression characterizes equality.

@[simp]

theorem TauCeti.pseudoHyperbolicExpr_eq_zero_iff_unitDisc (z w : Complex.UnitDisc) : pseudoHyperbolicExpr ↑z ↑w = 0 ↔ z = w

For bundled unit-disc points, zero pseudo-hyperbolic expression characterizes equality.

theorem TauCeti.norm_sq_one_sub_conj_mul_sub_norm_sq_sub (z w : ℂ) : ‖1 - (starRingEnd ℂ) w * z‖ ^ 2 - ‖z - w‖ ^ 2 = (1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2)

Poincaré defect identity (norm form). The difference of the squared norms of the Moebius denominator and numerator factors is the product of the two hyperbolic defects: ‖1 - conj w * z‖ ^ 2 - ‖z - w‖ ^ 2 = (1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2).

theorem TauCeti.norm_sub_eq_of_pseudoHyperbolicExpr_eq {z w z' w' : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) (hnz : ‖z'‖ = ‖z‖) (hnw : ‖w'‖ = ‖w‖) (h : pseudoHyperbolicExpr z' w' = pseudoHyperbolicExpr z w) : ‖z' - w'‖ = ‖z - w‖

Equal norms plus equal pseudo-hyperbolic expression force equal distance. For four points of the open unit disc with ‖z'‖ = ‖z‖ and ‖w'‖ = ‖w‖, the pseudo-hyperbolic expression determines the Euclidean distance.

theorem TauCeti.norm_sub_lt_norm_one_sub_conj_mul_of_norm_lt_one {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : ‖z - w‖ < ‖1 - (starRingEnd ℂ) w * z‖

For two points of norm less than one, the numerator norm is smaller than the denominator norm in the pseudo-hyperbolic expression.

theorem TauCeti.pseudoHyperbolicExpr_lt_one_of_norm_lt_one {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : pseudoHyperbolicExpr z w < 1

The pseudo-hyperbolic expression of two points of norm less than one is strictly less than one.

theorem TauCeti.pseudoHyperbolicExpr_lt_one_of_mem_ball {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : pseudoHyperbolicExpr z w < 1

The pseudo-hyperbolic expression of two points in the open unit ball is strictly less than one.

theorem TauCeti.pseudoHyperbolicExpr_lt_one_unitDisc (z w : Complex.UnitDisc) : pseudoHyperbolicExpr ↑z ↑w < 1

The pseudo-hyperbolic expression of two bundled unit-disc points is strictly less than one.

theorem TauCeti.pseudoHyperbolicExpr_mem_Ioo_of_norm_lt_one {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : pseudoHyperbolicExpr z w ∈ Set.Ioo (-1) 1

The pseudo-hyperbolic expression of two points of norm less than one lies in the interval Ioo (-1) 1 on which Real.artanh is a strictly monotone bijection onto ℝ. This is the side condition of the Real.artanh lemmas applied to it to define the hyperbolic distance.

theorem TauCeti.continuousOn_pseudoHyperbolicExpr : ContinuousOn (fun (p : ℂ × ℂ) => pseudoHyperbolicExpr p.1 p.2) (Metric.ball 0 1 ×ˢ Metric.ball 0 1)

The pseudo-hyperbolic expression is continuous on the product of two copies of the open unit disc, where its Moebius denominator does not vanish.