Existing in Mathlib · Complex analysis
Schwarz Lemma
A complex-differentiable map that sends an origin-centered open ball into the equal-radius closed ball and fixes the origin cannot move any selected point farther from the origin: inside the source ball, the image norm is at most the original norm.
- Schwarz lemma
- complex differentiability
- complex normed spaces
- open and closed balls
- fixed origin
- norm contraction
Exact theorem
Exact Mathlib statement
theorem Complex.norm_le_norm_of_mapsTo_ball {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {R : ℝ} {f : E → F} {z : E} (hd : DifferentiableOn ℂ f (Metric.ball 0 R)) (h_maps : MapsTo f (Metric.ball 0 R) (Metric.closedBall 0 R)) (h₀ : f 0 = 0) (hz : ‖z‖ < R) : ‖f z‖ ≤ ‖z‖The theorem at a glance
Schwarz lemma at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Schwarz lemma at a glance
Detailed visual description
The poster states the complex-differentiability, MapsTo, fixed-origin, and interior-point hypotheses before the exact non-strict norm conclusion. Two same-radius ball cross-sections place z in the source and a shorter radial f(z) in the target. Three source-faithful movements connect ball membership to the equal-radius distance estimate and the final simplification from distance to norm, while the footer excludes strictness, equality classification, and automorphism claims.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Equal-radius balls and a fixed center
Detailed visual description
Two identically sized circular norm contours have aligned charcoal centers. The left outer boundary is dashed and the right outer boundary is solid. A cobalt source segment is longer than an emerald target segment, and a single gold connector points from the source center toward the target center. Faint symmetric construction contours remain purely geometric.
Why it matters
A mathematical landmark
The Schwarz lemma is a central rigidity estimate in complex analysis. Mathlib's selected declaration records a flexible normed-space form: an equal-radius ball inclusion and one fixed point turn an analytic mapping condition into a precise pointwise norm bound.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib's origin-centered norm-contraction form of the Schwarz lemma for a map between possibly different complex normed spaces. The selected declaration assumes complex differentiability on ball 0 R, MapsTo that open ball into closedBall 0 R, f 0 = 0, and ‖z‖ < R; its exact endpoint is ‖f z‖ ≤ ‖z‖. It is not the nearby derivative-bound theorem, does not assert strict contraction or characterize equality, and does not classify automorphisms or Möbius maps.
- The selected declaration gives a non-strict norm inequality from the fixed origin; it does not claim strict contraction.
- It does not characterize the equality case or assert that f is linear, injective, surjective, invertible, or an automorphism.
- The endpoint is not the nearby derivative estimate and contains no bound on fderiv or deriv.
- The domain and codomain may be different complex normed spaces; the declaration is not restricted to a scalar map ℂ → ℂ or to the unit radius.
- MapsTo asserts inclusion in the target closed ball, not that the source ball maps onto it.
- ProofAtlas is indexing an existing upstream Mathlib theorem, and generated explanations and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
Complex.norm_le_norm_of_mapsTo_ballin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.schwarz-lemma.v001