The infinitesimal Schwarz--Pick inequality

This file proves the differential (infinitesimal) form of the Schwarz--Pick lemma for holomorphic self-maps of the complex unit disc: if f is holomorphic on ball 0 1 and maps it into itself, then at every point z of the disc ‖deriv f z‖ / (1 - ‖f z‖ ^ 2) ≤ 1 / (1 - ‖z‖ ^ 2), i.e. f contracts the Poincaré (hyperbolic) metric |dz| / (1 - |z| ^ 2). The bundled Complex.UnitDisc form is norm_deriv_div_one_sub_norm_sq_le_unitDisc.

This advances the conformal-mapping roadmap's L2 Schwarz--Pick target (TauCetiRoadmap/ConformalMapping/README.md, the L2 hyperbolic/Poincaré-metric contraction), complementing Tau Ceti's finite Schwarz--Pick estimate pseudoHyperbolicExpr_map_le. It reuses Mathlib's Schwarz lemma (Complex.norm_deriv_le_one_of_mapsTo_ball) 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.

theorem TauCeti.hasDerivAt_schwarzPickConjugate_zero {f : ℂ → ℂ} {df z : ℂ} (hp_outer : 1 - (starRingEnd ℂ) (f z) * f z ≠ 0) (hf : HasDerivAt f df z) : HasDerivAt (schwarzPickConjugate f z) (df * (1 - (starRingEnd ℂ) z * z) / (1 - (starRingEnd ℂ) (f z) * f z)) 0

Chain rule for the Schwarz--Pick conjugate at the origin. The Schwarz--Pick conjugate schwarzPickConjugate f z sandwiches f between the unit-disc Moebius factors centred at -z and at f z, whose derivatives are 1 - conj z * z (the source factor at 0, where it takes the value z) and 1 / (1 - conj (f z) * f z) (the target factor at f z). So the derivative of the conjugate at the origin is the derivative of f at z, rescaled by the two Poincaré defects.

All the target factor needs is that its denominator 1 - conj (f z) * f z at f z — the Poincaré defect 1 - ‖f z‖ ^ 2 — does not vanish, which for ‖f z‖ < 1 is one_sub_conj_mul_ne_zero_of_norm_lt_one; the source factor is differentiated at the origin, where its denominator is 1, so no bound on z is required.

theorem TauCeti.norm_deriv_div_one_sub_norm_sq_le {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) {z : ℂ} (hz : z ∈ Metric.ball 0 1) : ‖deriv f z‖ / (1 - ‖f z‖ ^ 2) ≤ 1 / (1 - ‖z‖ ^ 2)

The infinitesimal Schwarz--Pick inequality. A holomorphic self-map f of the open unit disc contracts the Poincaré metric: at every point z of the disc, ‖deriv f z‖ / (1 - ‖f z‖ ^ 2) ≤ 1 / (1 - ‖z‖ ^ 2).

theorem TauCeti.norm_deriv_div_one_sub_norm_sq_le_unitDisc {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (z : Complex.UnitDisc) : ‖deriv f ↑z‖ / (1 - ‖f ↑z‖ ^ 2) ≤ 1 / (1 - ‖↑z‖ ^ 2)

Bundled unit-disc form of the infinitesimal Schwarz--Pick inequality: a holomorphic self-map f of the open unit disc contracts the Poincaré metric at every disc point z.