The Poincaré metric is the length metric of its density

Hyperbolic/Distance.lean defines the hyperbolic distance on the complex open unit disc by the closed formula hyperbolicDist z w = Real.artanh (pseudoHyperbolicExpr z w), and Hyperbolic/Density.lean shows that its infinitesimal density is (1 - ‖z‖ ^ 2)⁻¹ and that the distance from the origin along a radius is the integral of that density along the radius. The latter file records, in so many words, what was still missing: "the density-weighted length of a general curve is not defined here, so this does not identify hyperbolicDist with the length metric of the density between arbitrary points". This file supplies the definition and the identification.

The definition is the obvious one: for a path γ : ℝ → ℂ in the disc,

TauCeti.hyperbolicLength γ a b = ∫ t in uIcc a b, ‖deriv γ t‖ / (1 - ‖γ t‖ ^ 2),

the Euclidean speed integrated against the Poincaré density over the unordered parameter interval, as for Mathlib's Manifold.pathELength: the length of a path does not depend on the orientation of its parameter interval, and is nonnegative. That is the length of γ measured against the density (1 - ‖z‖ ^ 2)⁻¹ in the sense of TauCeti.densityLength of TauCeti/Analysis/Calculus/DensityLength.lean, and hyperbolicLength is defined as that instance: everything about the parameter side of the integral — that the length is unoriented and additive, that it depends on the path only through its restriction to the parameter interval, that it is unchanged by an affine, monotone or antitone reparametrisation, and that comparing the density-weighted speeds of two paths compares their lengths — is proved there, for an arbitrary density on an arbitrary real normed space, and is only read off here. What this file adds is what the Poincaré density itself contributes. The two post-composition statements below — the Moebius invariance TauCeti.hyperbolicLength_unitDiscMoebiusFormula_comp and the Schwarz--Pick estimate TauCeti.hyperbolicLength_comp_le — reduce to a pointwise identity, respectively estimate, between density-weighted speeds, which is where the Poincaré density enters, the passage from there to the integrals being the general congruence and comparison; the lower bound below and the path attaining it are one-variable calculus arguments of their own, described next.

The theorem is that hyperbolicDist z w is the least such length over C¹ paths from z to w (TauCeti.isLeast_hyperbolicLength): no path is shorter (TauCeti.hyperbolicDist_le_hyperbolicLength), and one path realises the value (TauCeti.exists_hyperbolicLength_eq_hyperbolicDist). Regularity is always asked of the path relative to its parameter interval: continuity on the closed interval, an ordinary derivative at its interior points, and a derivative that extends continuously to the closed interval.

The proof

Both halves rest on one algebraic fact, which Conformal/SchwarzPick/AutomorphismIsometry.lean already supplies as the equality case of the infinitesimal Schwarz--Pick lemma (TauCeti.norm_deriv_div_one_sub_norm_sq_unitDiscMoebiusFormula_of_norm_lt_one): the disc Moebius factor M z = (z - c) / (1 - conj c * z) preserves the Poincaré density,

‖M ′ z‖ / (1 - ‖M z‖ ^ 2) = 1 / (1 - ‖z‖ ^ 2).

Integrating it along a path gives TauCeti.hyperbolicLength_unitDiscMoebiusFormula_comp: hyperbolic length is unchanged by post-composition with a disc Moebius factor. That is what moves an arbitrary path to one starting at the origin.

The lower bound. For a path with γ a = 0 the estimate is a one-variable calculus argument. Choosing a unit vector v with v * γ b = ‖γ b‖ — one exists for every γ b, including γ b = 0, by Mathlib's Complex.exists_norm_eq_mul_self — the real function ψ t = (v * γ t).re runs from 0 to ‖γ b‖ and satisfies |ψ| ≤ ‖γ‖ and |ψ ′| ≤ ‖γ ′‖. Hence, pointwise,

(Real.artanh ∘ ψ) ′ = ψ ′ / (1 - ψ ^ 2) ≤ ‖γ ′‖ / (1 - ‖γ‖ ^ 2),

the first inequality being 1 - ‖γ‖ ^ 2 ≤ 1 - ψ ^ 2 in the denominator. That is precisely the hypothesis of the displacement bound TauCeti.norm_sub_le_densityLength — a function of the parameter whose speed is dominated by the density-weighted speed of γ moves by at most the length of γ — read at the Poincaré density and at Real.artanh ∘ ψ, whose displacement is Real.artanh ‖γ b‖ = hyperbolicDist (γ a) (γ b). Projecting on a linear functional rather than on the norm is what keeps the comparison function differentiable where the path crosses the origin.

The bound is attained. By the same invariance it suffices to exhibit a shortest path from the origin, and the Euclidean radius t ↦ u * t is one: its hyperbolic length over [0, r] is ∫ t in (0)..r, (1 - t ^ 2)⁻¹ = Real.artanh r (TauCeti.hyperbolicLength_ray), which is Real.integral_one_sub_sq_inv_eq_artanh, the same input the radial statement of Hyperbolic/Density.lean spends. Transporting the radius by the Moebius factor centred at -z joins z to w with length hyperbolicDist z w. The minimisers exhibited here are therefore the radii through the origin and their Moebius images, the hyperbolic geodesics classified in Conformal/Poincare/Betweenness.lean; the converse — that a path of least length is a reparametrisation of one of them — is an equality case that this file does not prove.

Schwarz--Pick: hyperbolic length is contracted, and conformally invariant

The Moebius invariance above is the equality case of a one-sided estimate, and the estimate holds for every holomorphic self-map of the disc, not only for the automorphisms. Integrating the infinitesimal Schwarz--Pick inequality TauCeti.norm_deriv_div_one_sub_norm_sq_le of Conformal/SchwarzPick/Derivative.lean along a path, exactly as the Moebius statement integrates its equality case, gives TauCeti.hyperbolicLength_comp_le: post-composing a path with a holomorphic self-map of the disc does not increase its hyperbolic length. The comparison is termwise, because the chain rule turns the density-weighted speed of f ∘ γ into

‖deriv f (γ t)‖ / (1 - ‖f (γ t)‖ ^ 2) * ‖γ' t‖,

the first factor of which Schwarz--Pick bounds by (1 - ‖γ t‖ ^ 2)⁻¹; both integrands are continuous, since the derivative of a holomorphic function is again holomorphic, so TauCeti.densityLength_le_densityLength integrates the estimate. The Moebius invariance is the same reading of the same general lemma's equality counterpart TauCeti.densityLength_congr_of_eqOn, which asks for no integrability, and that is why it holds for a path with no regularity beyond a derivative inside its parameter interval.

Applying the estimate to a biholomorphism and to its inverse in turn pins the two lengths together and makes hyperbolic length a conformal invariant of the disc (TauCeti.hyperbolicLength_comp_eq_of_leftInvOn): no explicit automorphism formula enters, only the existence of a holomorphic inverse. Read at the standard automorphism z ↦ u * (z - c) / (1 - conj c * z) it recovers TauCeti.hyperbolicLength_unitDiscMoebiusFormula_comp with its rotation factor restored, the rotation costing nothing because multiplying a path by a unit scalar changes neither its Euclidean speed nor its distance from the origin (TauCeti.hyperbolicLength_const_mul). Reflection in the real axis is invariant too (TauCeti.hyperbolicLength_conj), which the conformal statement cannot see, conjugation being antiholomorphic; with it the invariance covers the whole isometry group of the Poincaré disc as Conformal/Poincare/Isometry/Classification.lean exhibits it.

Relation to Mathlib's Manifold.pathELength

Why TauCeti.densityLength, and not Mathlib's ℝ≥0∞-valued Manifold.pathELength of Mathlib/Geometry/Manifold/Riemannian/PathELength.lean, is the notion being instantiated is argued in TauCeti/Analysis/Calculus/DensityLength.lean. Should the Poincaré disc later be given a Riemannian structure, TauCeti.isLeast_hyperbolicLength is precisely the input needed to identify hyperbolicDist with Manifold.riemannianEDist, and this file should be refactored onto that API at that point.

Main declarations

• TauCeti.hyperbolicLength — the density-weighted length of a path in the disc, with TauCeti.hyperbolicLength_eq_integral rewriting it against an explicit derivative, and TauCeti.hyperbolicLength_symm, TauCeti.hyperbolicLength_nonneg, TauCeti.hyperbolicLength_const, TauCeti.hyperbolicLength_add the basic evaluations and operations.

• TauCeti.intervalIntegrable_norm_div_one_sub_norm_sq and TauCeti.intervalIntegrable_norm_deriv_div_one_sub_norm_sq — for a C¹ path in the disc the density-weighted speed is interval integrable, against an explicit derivative and against deriv respectively. The latter is the integrability hypothesis of TauCeti.hyperbolicLength_add, and what the Schwarz--Pick estimate and the lower bound below spend.

• TauCeti.hyperbolicLength_comp_of_deriv_nonneg and TauCeti.hyperbolicLength_comp_of_deriv_nonpos — hyperbolic length is a reparametrisation invariant: precomposing a path with a differentiable monotone, respectively antitone, map of the parameter transports the parameter interval and leaves the length unchanged. For the affine reparametrisations t ↦ s * t + d this needs nothing of the path, TauCeti.hyperbolicLength_comp_mul_add.

• TauCeti.hyperbolicLength_congr — the hyperbolic length of a path depends only on its values along its own parameter interval.

  These last three groups are the Poincaré readings of the density-independent statements TauCeti.densityLength_symm, TauCeti.densityLength_nonneg, TauCeti.densityLength_const, TauCeti.densityLength_add, TauCeti.densityLength_comp_of_deriv_nonneg, TauCeti.densityLength_comp_of_deriv_nonpos, TauCeti.densityLength_comp_mul_add and TauCeti.densityLength_congr, and are proved by naming them.

• TauCeti.hyperbolicLength_unitDiscMoebiusFormula_comp — hyperbolic length is a Moebius invariant, the integrated form of the infinitesimal isometry TauCeti.norm_deriv_div_one_sub_norm_sq_unitDiscMoebiusFormula_of_norm_lt_one; TauCeti.hyperbolicLength_const_mul is the same statement for a rotation, and TauCeti.hyperbolicLength_conj for the reflection in the real axis.

• TauCeti.hyperbolicLength_comp_le — Schwarz--Pick for the Poincaré length: post-composing a path in the disc with a holomorphic self-map of the disc does not increase its hyperbolic length.

• TauCeti.hyperbolicLength_comp_eq_of_leftInvOn — hyperbolic length is a conformal invariant: a holomorphic self-map of the disc with a holomorphic left inverse preserves it.

• TauCeti.hyperbolicLength_ray — the hyperbolic length of a Euclidean radius is Real.artanh of its Euclidean length.

• TauCeti.hyperbolicDist_le_hyperbolicLength — no C¹ path in the disc is hyperbolically shorter than the hyperbolic distance between its endpoints.

• TauCeti.exists_hyperbolicLength_eq_hyperbolicDist — the bound is attained.

• TauCeti.isLeast_hyperbolicLength — the Poincaré metric is the length metric of its density: hyperbolicDist z w is the least hyperbolic length of a C¹ path from z to w.

Coordination with upstream Mathlib

As with the rest of the L2 material of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md), this file is coordinated with the in-progress human-curated Riemann-mapping effort mathlib4#33505, which contains no hyperbolic metric on the disc; Mathlib has the hyperbolic metric on the upper half-plane (Analysis/Complex/UpperHalfPlane/Metric.lean) but neither a disc version nor a length-metric characterisation of it. Should a human-curated Poincaré metric land upstream, this file should be refactored onto it.

References

• L. V. Ahlfors, Conformal Invariants, Ch. 1 (the Poincaré metric as a length metric).
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. VII.

The hyperbolic length of a path

noncomputable def TauCeti.hyperbolicLength (γ : ℝ → ℂ) (a b : ℝ) : ℝ

The hyperbolic length of the path γ over the parameter interval with endpoints a and b: its length measured against the Poincaré density (1 - ‖z‖ ^ 2)⁻¹ of Conformal/Hyperbolic/Density.lean, in the sense of TauCeti.densityLength. Unfolded, it is the Euclidean speed ‖deriv γ t‖ integrated over the unordered interval uIcc a b against that density (TauCeti.hyperbolicLength_def).

Taking the integral over the unordered interval, as Mathlib's Manifold.pathELength does, makes the length independent of the orientation of the parameter interval (TauCeti.hyperbolicLength_symm) and nonnegative for a path in the disc whichever way round its endpoints are (TauCeti.hyperbolicLength_nonneg); it is a reparametrisation invariant of the path (TauCeti.hyperbolicLength_comp_of_deriv_nonneg and TauCeti.hyperbolicLength_comp_of_deriv_nonpos for the monotone and the antitone reparametrisations, TauCeti.hyperbolicLength_comp_mul_add for the affine ones).

The definition is stated for an arbitrary γ : ℝ → ℂ, and only the derivative at the interior parameters enters (TauCeti.hyperbolicLength_eq_integral). It is the intended notion of length when γ is a C¹ path with values in the open unit disc, which is what the comparison with TauCeti.hyperbolicDist below assumes; the evaluations of the length itself need no such hypothesis.

Equations

• TauCeti.hyperbolicLength γ a b = TauCeti.densityLength (fun (z : ℂ) => (1 - ‖z‖ ^ 2)⁻¹) γ a b

theorem TauCeti.hyperbolicLength_def (γ : ℝ → ℂ) (a b : ℝ) : hyperbolicLength γ a b = ∫ (t : ℝ) in Set.uIcc a b, ‖deriv γ t‖ / (1 - ‖γ t‖ ^ 2)

The defining formula for the hyperbolic length of a path.

@[simp]

theorem TauCeti.hyperbolicLength_self (γ : ℝ → ℂ) (a : ℝ) : hyperbolicLength γ a a = 0

A degenerate parameter interval carries no hyperbolic length.

theorem TauCeti.hyperbolicLength_symm (γ : ℝ → ℂ) (a b : ℝ) : hyperbolicLength γ b a = hyperbolicLength γ a b

Hyperbolic length does not depend on the orientation of the parameter interval.

@[simp]

theorem TauCeti.hyperbolicLength_const (c : ℂ) (a b : ℝ) : hyperbolicLength (fun (x : ℝ) => c) a b = 0

A constant path has zero hyperbolic length.

theorem TauCeti.hyperbolicLength_eq_integral {γ γ' : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hderiv : ∀ t ∈ Set.Ioo a b, HasDerivAt γ (γ' t) t) : hyperbolicLength γ a b = ∫ (t : ℝ) in a..b, ‖γ' t‖ / (1 - ‖γ t‖ ^ 2)

The hyperbolic length computed from an explicit derivative rather than from deriv. The derivative is only asked for at the interior parameters, the two endpoints forming a null set.

theorem TauCeti.hyperbolicLength_nonneg {γ : ℝ → ℂ} {a b : ℝ} (hmem : ∀ t ∈ Set.uIoo a b, ‖γ t‖ < 1) : 0 ≤ hyperbolicLength γ a b

A path running through the open unit disc has nonnegative hyperbolic length, whichever way round its endpoints are: the Poincaré density is positive there. Only the interior parameters are asked about, the two endpoints forming a null set.

theorem TauCeti.intervalIntegrable_norm_div_one_sub_norm_sq {γ γ' : ℝ → ℂ} {a b : ℝ} (hγ : ContinuousOn γ (Set.uIcc a b)) (hγ' : ContinuousOn γ' (Set.uIcc a b)) (hmem : ∀ t ∈ Set.uIcc a b, ‖γ t‖ < 1) : IntervalIntegrable (fun (t : ℝ) => ‖γ' t‖ / (1 - ‖γ t‖ ^ 2)) MeasureTheory.volume a b

For a C¹ path in the disc the density-weighted speed is interval integrable: it is continuous, its denominator staying away from zero because the path stays in the open disc.

theorem TauCeti.intervalIntegrable_norm_deriv_div_one_sub_norm_sq {γ γ' : ℝ → ℂ} {a b : ℝ} (hγ : ContinuousOn γ (Set.uIcc a b)) (hγ' : ContinuousOn γ' (Set.uIcc a b)) (hderiv : ∀ t ∈ Set.uIoo a b, HasDerivAt γ (γ' t) t) (hmem : ∀ t ∈ Set.uIcc a b, ‖γ t‖ < 1) : IntervalIntegrable (fun (t : ℝ) => ‖deriv γ t‖ / (1 - ‖γ t‖ ^ 2)) MeasureTheory.volume a b

The same integrability read against deriv rather than against the explicit derivative, the two agreeing at the interior parameters and the two endpoints forming a null set. This is the shape in which the integrability is asked for by TauCeti.hyperbolicLength_add and by the comparison TauCeti.densityLength_le_densityLength.

theorem TauCeti.hyperbolicLength_congr {γ : ℝ → ℂ} {a b : ℝ} {δ : ℝ → ℂ} (hδ : Set.EqOn δ γ (Set.uIoo a b)) : hyperbolicLength δ a b = hyperbolicLength γ a b

The hyperbolic length of a path depends only on its parameter interval. Two paths that agree inside the interval with endpoints a and b have the same hyperbolic length over it: at an interior parameter they have the same germ, hence the same derivative, and the two endpoints form a null set.

theorem TauCeti.hyperbolicLength_add {γ : ℝ → ℂ} {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) (hint : IntervalIntegrable (fun (t : ℝ) => ‖deriv γ t‖ / (1 - ‖γ t‖ ^ 2)) MeasureTheory.volume a c) : hyperbolicLength γ a b + hyperbolicLength γ b c = hyperbolicLength γ a c

Hyperbolic length is additive along the parameter interval: the lengths of the two halves of a path add up to the length of the whole, as soon as the density-weighted speed is integrable over the whole. For a C¹ path in the disc that hypothesis holds by continuity.

theorem TauCeti.hyperbolicLength_comp_mul_add (γ : ℝ → ℂ) {s : ℝ} (hs : s ≠ 0) (d a b : ℝ) : hyperbolicLength (fun (t : ℝ) => γ (s * t + d)) a b = hyperbolicLength γ (s * a + d) (s * b + d)

Hyperbolic length is invariant under affine reparametrisation. Replacing the parameter t by s * t + d for s ≠ 0, an orientation-preserving reparametrisation for 0 < s and an orientation-reversing one for s < 0, transports the parameter interval and leaves the length unchanged: two affinely reparametrised copies of one path have the same hyperbolic length. For instance s = r, d = 0 reads the path of TauCeti.exists_hyperbolicLength_eq_hyperbolicDist, defined on [0, r], on the parameter interval [0, 1] without changing its length.

theorem TauCeti.hyperbolicLength_comp_of_deriv_nonneg {γ : ℝ → ℂ} {a b : ℝ} {φ φ' : ℝ → ℝ} (hφ : ContinuousOn φ (Set.uIcc a b)) (hderiv : ∀ t ∈ Set.uIoo a b, HasDerivAt φ (φ' t) t) (hsign : ∀ t ∈ Set.uIoo a b, 0 ≤ φ' t) (hγ : ∀ t ∈ Set.uIoo a b, DifferentiableAt ℝ γ (φ t)) : hyperbolicLength (γ ∘ φ) a b = hyperbolicLength γ (φ a) (φ b)

Hyperbolic length is invariant under monotone reparametrisation. Precomposing a path with a map φ that is continuous on the parameter interval and has a nonnegative derivative inside it — so that φ is monotone there — reparametrises the path and transports the parameter interval, leaving the length unchanged.

theorem TauCeti.hyperbolicLength_comp_of_deriv_nonpos {γ : ℝ → ℂ} {a b : ℝ} {φ φ' : ℝ → ℝ} (hφ : ContinuousOn φ (Set.uIcc a b)) (hderiv : ∀ t ∈ Set.uIoo a b, HasDerivAt φ (φ' t) t) (hsign : ∀ t ∈ Set.uIoo a b, φ' t ≤ 0) (hγ : ∀ t ∈ Set.uIoo a b, DifferentiableAt ℝ γ (φ t)) : hyperbolicLength (γ ∘ φ) a b = hyperbolicLength γ (φ a) (φ b)

Hyperbolic length is invariant under antitone reparametrisation. The orientation-reversing counterpart of TauCeti.hyperbolicLength_comp_of_deriv_nonneg: precomposing a path with a map φ that is continuous on the parameter interval and has a nonpositive derivative inside it — so that φ is antitone there — leaves the length unchanged, the parameter interval being transported with its orientation reversed. Together the two lemmas say that hyperbolic length is a property of a path rather than of its parametrisation.

theorem TauCeti.hyperbolicLength_ray {u : ℂ} (hu : ‖u‖ = 1) {r : ℝ} (hr : 0 ≤ r) (hr1 : r < 1) : hyperbolicLength (fun (t : ℝ) => u * ↑t) 0 r = Real.artanh r

The hyperbolic length of a Euclidean radius. For a unit vector u and 0 ≤ r < 1, the path t ↦ u * t has hyperbolic length Real.artanh r over [0, r], which by TauCeti.hyperbolicDist_zero_right is the hyperbolic distance from 0 to its endpoint. This is the radial computation of Conformal/Hyperbolic/Density.lean read as a statement about lengths.

Conformal invariance of the density

@[simp]

theorem TauCeti.hyperbolicLength_const_mul {γ : ℝ → ℂ} {a b : ℝ} {u : ℂ} (hu : ‖u‖ = 1) : hyperbolicLength (fun (t : ℝ) => u * γ t) a b = hyperbolicLength γ a b

Hyperbolic length is a rotation invariant. Multiplying a path by a scalar of modulus one scales neither its Euclidean speed nor its distance from the origin, so it changes no term of the density-weighted integrand. Unlike the Moebius invariance below, this asks nothing of the path: where the path fails to be differentiable so does its rotation, and both sides read the same junk value of deriv.

@[simp]

theorem TauCeti.hyperbolicLength_conj (γ : ℝ → ℂ) (a b : ℝ) : hyperbolicLength (fun (t : ℝ) => (starRingEnd ℂ) (γ t)) a b = hyperbolicLength γ a b

Hyperbolic length is a conjugation invariant. Reflecting a path in the real axis leaves its hyperbolic length unchanged. As for the rotation invariance this asks nothing of the path: conjugation is a real-linear isometry, so it changes neither term of the density-weighted integrand, and at a parameter where the path fails to be differentiable both sides read the same junk value of deriv (deriv.star). Conjugation is antiholomorphic, so this is not an instance of the conformal invariance TauCeti.hyperbolicLength_comp_eq_of_leftInvOn below; together the two cover the whole isometry group of the Poincaré disc, which Conformal/Poincare/Isometry/Classification.lean exhibits as the standard automorphisms and their conjugates.

theorem TauCeti.hyperbolicLength_unitDiscMoebiusFormula_comp {γ γ' : ℝ → ℂ} {a b : ℝ} {c : ℂ} (hc : ‖c‖ < 1) (hderiv : ∀ t ∈ Set.uIoo a b, HasDerivAt γ (γ' t) t) (hmem : ∀ t ∈ Set.uIoo a b, ‖γ t‖ < 1) : hyperbolicLength (fun (t : ℝ) => (γ t - c) / (1 - (starRingEnd ℂ) c * γ t)) a b = hyperbolicLength γ a b

Hyperbolic length is a Moebius invariant. Post-composing a path in the disc with the Moebius factor z ↦ (z - c) / (1 - conj c * z) leaves its hyperbolic length unchanged: this is the infinitesimal Poincaré isometry TauCeti.norm_deriv_div_one_sub_norm_sq_unitDiscMoebiusFormula_of_norm_lt_one integrated along the path. It is the tool that moves the starting point of a path to the origin.

Only the density-weighted speeds of the two paths are compared, and they agree at every interior parameter, so this is TauCeti.densityLength_congr_of_eqOn and needs no integrability: the path is asked for nothing beyond a derivative inside its parameter interval, and to stay in the disc there, the two endpoints forming a null set — unlike the Schwarz--Pick estimate TauCeti.hyperbolicLength_comp_le below, whose two integrands are only comparable.

Schwarz--Pick: holomorphic self-maps of the disc contract hyperbolic length

theorem TauCeti.hyperbolicLength_comp_le {γ γ' : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hγ : ContinuousOn γ (Set.uIcc a b)) (hderiv : ∀ t ∈ Set.uIoo a b, HasDerivAt γ (γ' t) t) (hγ' : ContinuousOn γ' (Set.uIcc a b)) (hmem : ∀ t ∈ Set.uIcc a b, ‖γ t‖ < 1) : hyperbolicLength (f ∘ γ) a b ≤ hyperbolicLength γ a b

Schwarz--Pick for the Poincaré length. Post-composing a path in the open unit disc with a holomorphic self-map of the disc does not increase its hyperbolic length. This is the infinitesimal Schwarz--Pick inequality TauCeti.norm_deriv_div_one_sub_norm_sq_le integrated along the path, in the same way as TauCeti.hyperbolicLength_unitDiscMoebiusFormula_comp integrates its equality case; the path is asked to be C¹ on its parameter interval, as in TauCeti.hyperbolicDist_le_hyperbolicLength, so that both density-weighted speeds are integrable, which is what TauCeti.densityLength_le_densityLength spends to turn the pointwise comparison of the two integrands into a comparison of the two lengths.

theorem TauCeti.hyperbolicLength_comp_eq_of_leftInvOn {γ γ' : ℝ → ℂ} {a b : ℝ} {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hfmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hg : DifferentiableOn ℂ g (Metric.ball 0 1)) (hgmaps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hgf : Set.LeftInvOn g f (Metric.ball 0 1)) (hγ : ContinuousOn γ (Set.uIcc a b)) (hderiv : ∀ t ∈ Set.uIoo a b, HasDerivAt γ (γ' t) t) (hγ' : ContinuousOn γ' (Set.uIcc a b)) (hmem : ∀ t ∈ Set.uIcc a b, ‖γ t‖ < 1) : hyperbolicLength (f ∘ γ) a b = hyperbolicLength γ a b

Hyperbolic length is a conformal invariant of the disc. A holomorphic self-map of the open unit disc that has a holomorphic left inverse there preserves the hyperbolic length of every C¹ path in the disc: the Schwarz--Pick estimate TauCeti.hyperbolicLength_comp_le applied to the map and to its inverse in turn traps the two lengths at each other. No explicit automorphism formula enters, only the existence of the holomorphic inverse.

The distance is a lower bound for the length

theorem TauCeti.hyperbolicDist_le_hyperbolicLength {γ γ' : ℝ → ℂ} {a b : ℝ} (hγ : ContinuousOn γ (Set.uIcc a b)) (hderiv : ∀ t ∈ Set.uIoo a b, HasDerivAt γ (γ' t) t) (hγ' : ContinuousOn γ' (Set.uIcc a b)) (hmem : ∀ t ∈ Set.uIcc a b, ‖γ t‖ < 1) : hyperbolicDist (γ a) (γ b) ≤ hyperbolicLength γ a b

No path in the disc is hyperbolically shorter than the hyperbolic distance between its endpoints. For a path γ staying in the open unit disc, continuous on its parameter interval and continuously differentiable inside it, hyperbolicDist (γ a) (γ b) ≤ hyperbolicLength γ a b.

The starting point is moved to the origin by the Moebius factor centred at γ a, which changes neither side: the left-hand side because the factor is a hyperbolic isometry, the right-hand side by TauCeti.hyperbolicLength_unitDiscMoebiusFormula_comp.

The bound is attained

theorem TauCeti.exists_hyperbolicLength_eq_hyperbolicDist {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : ∃ (r : ℝ) (γ : ℝ → ℂ) (γ' : ℝ → ℂ), 0 ≤ r ∧ ContinuousOn γ (Set.Icc 0 r) ∧ (∀ t ∈ Set.Ioo 0 r, HasDerivAt γ (γ' t) t) ∧ ContinuousOn γ' (Set.Icc 0 r) ∧ (∀ t ∈ Set.Icc 0 r, ‖γ t‖ < 1) ∧ γ 0 = z ∧ γ r = w ∧ hyperbolicLength γ 0 r = hyperbolicDist z w

The hyperbolic distance is realised by a path. Any two points of the open unit disc are joined by a C¹ path in the disc whose hyperbolic length is exactly their hyperbolic distance, namely the Moebius image of a Euclidean radius.

theorem TauCeti.isLeast_hyperbolicLength {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : IsLeast {L : ℝ | ∃ (r : ℝ) (γ : ℝ → ℂ) (γ' : ℝ → ℂ), 0 ≤ r ∧ ContinuousOn γ (Set.Icc 0 r) ∧ (∀ t ∈ Set.Ioo 0 r, HasDerivAt γ (γ' t) t) ∧ ContinuousOn γ' (Set.Icc 0 r) ∧ (∀ t ∈ Set.Icc 0 r, ‖γ t‖ < 1) ∧ γ 0 = z ∧ γ r = w ∧ hyperbolicLength γ 0 r = L} (hyperbolicDist z w)

The Poincaré metric is the length metric of the Poincaré density. For two points of the open unit disc, hyperbolicDist z w is the least hyperbolic length of a path in the disc running from z to w that is continuous on its parameter interval and continuously differentiable inside it.

Together with the classification of the hyperbolic geodesics in Conformal/Poincare/Betweenness.lean this closes the circle of descriptions of the Poincaré metric: the closed formula of Hyperbolic/Distance.lean, the infinitesimal density of Hyperbolic/Density.lean, and the induced length metric all agree.