Schwarz--Pick for the pseudo-hyperbolic expression

This file proves the Schwarz--Pick contraction estimate for holomorphic self-maps of the complex unit disc, stated using Tau Ceti's pseudo-hyperbolic expression pseudoHyperbolicExpr z w = ‖(z - w) / (1 - conj w * z)‖.

It provides the pseudo-hyperbolic expression statement, plus a bundled Complex.UnitDisc form for callers working directly with disc points.

It also sets up the Schwarz--Pick conjugate schwarzPickConjugate f a, the self-map of the disc obtained by conjugating f by the Moebius factors centred at a and at f a, together with the scaffold lemma saying it is a holomorphic self-map fixing the origin and the lemma computing its value at a Moebius image. This is the construction Schwarz's lemma is applied to, shared by the contraction estimate here, the infinitesimal estimate in SchwarzPick/Derivative.lean, the equality case in SchwarzPick/Rigidity.lean and the automorphism classification.

This advances the conformal-mapping roadmap's L2 Schwarz--Pick target. It reuses Mathlib's Schwarz lemma and Tau Ceti's unit-disc Moebius 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. Mathlib already contains the preceding human-curated work in Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; none of it is duplicated here, and should that work land a human-curated Schwarz--Pick theorem this file should be refactored onto it.

noncomputable def TauCeti.schwarzPickConjugate (f : ℂ → ℂ) (a : ℂ) : ℂ → ℂ

The Schwarz--Pick conjugate of a self-map f of the open unit disc at a point a: f conjugated by the scalar Moebius formulas centred at -a on the source and at f a on the target. When f is a holomorphic self-map of the disc and ‖a‖ < 1 the conjugate is again a holomorphic self-map of the disc, but now fixing the origin (differentiableOn_and_mapsTo_ball_and_apply_zero_schwarzPickConjugate), so Schwarz's lemma applies to it at 0. This is the construction shared by the finite and infinitesimal Schwarz--Pick estimates and by the equality case of the finite estimate.

Equations

• TauCeti.schwarzPickConjugate f a = (fun (η : ℂ) => (η - f a) / (1 - (starRingEnd ℂ) (f a) * η)) ∘ f ∘ fun (ξ : ℂ) => (ξ - -a) / (1 - (starRingEnd ℂ) (-a) * ξ)

theorem TauCeti.schwarzPickConjugate_def (f : ℂ → ℂ) (a : ℂ) : schwarzPickConjugate f a = (fun (η : ℂ) => (η - f a) / (1 - (starRingEnd ℂ) (f a) * η)) ∘ f ∘ fun (ξ : ℂ) => (ξ - -a) / (1 - (starRingEnd ℂ) (-a) * ξ)

The Schwarz--Pick conjugate as a composite: the scalar Moebius formula centred at -a on the source, then f, then the scalar Moebius formula centred at f a on the target. The body of schwarzPickConjugate is not @[expose]d, so downstream files rewrite with this lemma rather than unfolding the definition.

@[simp]

theorem TauCeti.schwarzPickConjugate_apply_zero (f : ℂ → ℂ) (a : ℂ) : schwarzPickConjugate f a 0 = 0

The Schwarz--Pick conjugate of f at a fixes the origin: the source factor sends 0 to a, and the target factor sends f a to 0. No hypothesis on f or a is needed.

theorem TauCeti.differentiableOn_and_mapsTo_ball_and_apply_zero_schwarzPickConjugate {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) {a : ℂ} (ha : ‖a‖ < 1) : DifferentiableOn ℂ (schwarzPickConjugate f a) (Metric.ball 0 1) ∧ Set.MapsTo (schwarzPickConjugate f a) (Metric.ball 0 1) (Metric.ball 0 1) ∧ schwarzPickConjugate f a 0 = 0

Schwarz--Pick conjugation scaffold. For a holomorphic self-map f of the open unit disc and a disc point a, conjugating f by the Moebius automorphisms centred at a (on the source) and at f a (on the target) yields a holomorphic self-map of the disc that fixes the origin. This is the common scaffold of the finite and infinitesimal Schwarz--Pick estimates: applying Schwarz's lemma at 0 to the conjugate unwinds to the contraction estimate for f.

theorem TauCeti.schwarzPickConjugate_apply_unitDiscMoebiusFormula {f : ℂ → ℂ} {a z : ℂ} (ha : ‖a‖ < 1) (hz : ‖z‖ < 1) : schwarzPickConjugate f a ((z - a) / (1 - (starRingEnd ℂ) a * z)) = (f z - f a) / (1 - (starRingEnd ℂ) (f a) * f z)

Value of the Schwarz--Pick conjugate at a Moebius image. The Schwarz--Pick conjugate schwarzPickConjugate f a sends the Moebius image of a disc point z to the Moebius image of f z. Taking norms turns a Schwarz-lemma estimate for the conjugate at 0 into a pseudo-hyperbolic statement about f at z, a, so this is the evaluation step shared by the Schwarz--Pick contraction estimate and its equality case.

theorem TauCeti.pseudoHyperbolicExpr_map_le {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : pseudoHyperbolicExpr (f z) (f w) ≤ pseudoHyperbolicExpr z w

The Schwarz--Pick contraction estimate for the pseudo-hyperbolic expression on the open unit disc.

theorem TauCeti.pseudoHyperbolicExpr_map_le_unitDisc {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (z w : Complex.UnitDisc) : pseudoHyperbolicExpr (f ↑z) (f ↑w) ≤ pseudoHyperbolicExpr ↑z ↑w

Bundled unit-disc form of the Schwarz--Pick contraction estimate.