A strict form of the Schwarz lemma #
Schwarz's lemma bounds the derivative at the centre of a ball by R₂ / R₁ when a holomorphic
map into a strictly convex complex normed space sends ball c R₁ into closedBall (g c) R₂.
This file records the strict form: the bound is attained only by an injective map, so a
non-injective one has ‖deriv g c‖ < R₂ / R₁.
The argument #
Mathlib's Complex.norm_deriv_le_div_of_mapsTo_ball gives ‖deriv g c‖ ≤ R₂ / R₁. In the equality
case Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_div — the equality case of Schwarz, available
for ℂ because it is a strictly convex space — forces g to be the affine map
z ↦ g c + (z - c) • deriv g c on the ball. The slope is a nonzero vector, having norm
R₂ / R₁ > 0, so that map is injective, contradicting the hypothesis.
Both radii must be positive. With R₂ = 0 the target is the single point g c, so g is constant
and not injective, while the claimed bound ‖deriv g c‖ < 0 is false.
Main statements #
TauCeti.norm_deriv_lt_div_of_not_injOn— the strict bound.TauCeti.norm_deriv_lt_one_of_not_injOn— its equal-radius form.
Coordination with upstream Mathlib #
The Riemann mapping theorem is being formalized upstream at mathlib4#33505, which proves the L0–L3 prerequisites internally as private lemmas. The declaration here is an explicitly temporary shim: delete it and refactor downstream consumers onto the exported Mathlib version once that lands.
References #
- L. Ahlfors, Complex Analysis, Ch. 6 §1.2.
Strict Schwarz lemma. A holomorphic map of ball c R₁ into closedBall (g c) R₂ that is
not injective has ‖deriv g c‖ < R₂ / R₁.
Schwarz's lemma gives ‖deriv g c‖ ≤ R₂ / R₁; in the equality case the map is affine with nonzero
slope, hence injective. Both radii must be positive: for R₂ = 0 the map is constant, so it is
not injective and the strict bound fails.
Strict Schwarz lemma, equal radii. A holomorphic map of ball c R into
closedBall (g c) R that is not injective has ‖deriv g c‖ < 1.