Schwarz lemma #
In this file we prove several versions of the Schwarz lemma.
Complex.norm_deriv_le_div_of_mapsTo_ball. Letf : ℂ → Ebe a complex analytic function on an open disk with centercand a positive radiusR₁. Iffsends this ball to a closed ball with centerf cand radiusR₂, then the norm of the derivative offatcis at most the ratioR₂ / R₁.Complex.dist_le_div_mul_dist_of_mapsTo_ball. Letf : E → Fbe a complex analytic function on an open ball with centercand radiusR₁. Iffsends this ball to a closed ball with centerf cand radiusR₂, then for anyzin the former ball we havedist (f z) (f c) ≤ (R₂ / R₁) * dist z c.Complex.norm_deriv_le_one_of_mapsTo_ball. Iff : ℂ → Eis complex analytic on an open disk with centercand a positive radiusR₁, and it sends this disk to a closed ball with centerf cand radius the same radius, then the norm of the derivative offat the center of this disk is at most1.Complex.dist_le_dist_of_mapsTo_ball. Letf : E → Fbe a complex analytic function on an open ball with centerc. Iffsends this ball to a closed ball with centerf cand the same radius, then for anyzin the former ball we havedist (f z) (f c) ≤ dist z c.Complex.norm_le_norm_of_mapsTo_ball: Letf : E → Fbe a complex analytic on an open ball with center at the origin. Iffsends this ball to the closed ball with center0of the same radius andf 0 = 0, then for any pointzof this disk we have‖f z‖ ≤ ‖z‖.
Implementation notes #
Traditionally, the Schwarz lemma is formulated for maps f : ℂ → ℂ.
We generalize all versions of the lemma to the case of maps to any normed space.
For the versions that don't use deriv or dslope,
we state it for maps between any two normed spaces.
TODO #
- Prove that any diffeomorphism of the unit disk to itself is a Möbius map.
Tags #
Schwarz lemma
Let f : E → F be a complex analytic map
sending an open ball of radius R₁ to a closed ball of radius R₂.
If f w - f c = o(‖w - c‖ ^ n), then for any z in the ball in the domain,
we have dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1).
For n = 0, this theorem gives a usual Schwarz lemma,
see dist_le_div_mul_dist_of_mapsTo_ball below.
The Schwarz Lemma. Let f : E → F be a complex analytic function
on an open ball with center c and radius R₁.
If f sends this ball to a closed ball with center f c and radius R₂,
then for any z in the former ball we have dist (f z) (f c) ≤ (R₂ / R₁) * dist z c.
The Schwarz Lemma. Let f : E → F be a complex analytic function
on an open ball with center c and positive radius R₁.
If f sends this ball to a closed ball with center f c and radius R₂,
then the norm of the Fréchet derivative of f at c is at most R₂ / R₁.
The Schwarz Lemma. Let f : E → F be a complex analytic function
on an open ball with center c.
If f sends this ball to a closed ball with center f c and the same radius,
then for any z in the former ball we have dist (f z) (f c) ≤ dist z c.
Alias of Complex.dist_le_dist_of_mapsTo_ball.
The Schwarz Lemma. Let f : E → F be a complex analytic function
on an open ball with center c.
If f sends this ball to a closed ball with center f c and the same radius,
then for any z in the former ball we have dist (f z) (f c) ≤ dist z c.
The Schwarz Lemma. Let f : E → F be a complex analytic function
on an open ball with center c and a positive radius.
If f sends this ball to a closed ball with center f c and the same radius,
then the norm of the Fréchet derivative of f at c is at most one.
The Schwarz Lemma.
Let f : E → F be a complex analytic on an open ball with center at the origin.
If f sends this ball to the closed ball with center 0 of the same radius and f 0 = 0,
then for any point z of this disk we have ‖f z‖ ≤ ‖z‖.
Alias of Complex.norm_le_norm_of_mapsTo_ball.
The Schwarz Lemma.
Let f : E → F be a complex analytic on an open ball with center at the origin.
If f sends this ball to the closed ball with center 0 of the same radius and f 0 = 0,
then for any point z of this disk we have ‖f z‖ ≤ ‖z‖.
The Schwarz Lemma: if f : ℂ → E is complex analytic
on an open disk with center c and a positive radius R₁,
and it sends this disk to a closed ball with center f c and radius R₂,
then the norm of the derivative of f at c is at most the ratio R₂ / R₁.
The Schwarz Lemma: if f : ℂ → E is complex analytic
on an open disk with center c and a positive radius R₁,
and it sends this disk to a closed ball with center f c and radius the same radius,
then the norm of the derivative of f at the center of this disk is at most 1.
Two cases of the Schwarz Lemma (derivative and distance), merged together.
If f : ℂ → E is a complex analytic function on an open ball ball c R₁
hat sends it to a closed ball closedBall (f c) R₂, then the norm of dslope f c z,
which is defined as (z - c)⁻¹ • (f z - f c) for z ≠ c and as deriv f c for z = c,
is not greater than the ratio R₂ / R₁.
Equality case in the Schwarz Lemma: in the setup of norm_dslope_le_div_of_mapsTo_ball,
if ‖dslope f c z₀‖ = R₂ / R₁ holds at a point in the ball
then the map f is affine with slope dslope f c z₀.
Note that this lemma requires the codomain to be a strictly convex space.
Indeed, for E = ℂ × ℂ there is a counterexample:
the map f := fun z ↦ (z, z ^ 2) sends ball 0 1 to closedBall 0 1,
‖dslope f 0 0‖ = ‖deriv f 0‖ = ‖(1, 0)‖ = 1, but the map is not an affine map.
Alias of Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_div.
Equality case in the Schwarz Lemma: in the setup of norm_dslope_le_div_of_mapsTo_ball,
if ‖dslope f c z₀‖ = R₂ / R₁ holds at a point in the ball
then the map f is affine with slope dslope f c z₀.
Note that this lemma requires the codomain to be a strictly convex space.
Indeed, for E = ℂ × ℂ there is a counterexample:
the map f := fun z ↦ (z, z ^ 2) sends ball 0 1 to closedBall 0 1,
‖dslope f 0 0‖ = ‖deriv f 0‖ = ‖(1, 0)‖ = 1, but the map is not an affine map.
Equality case in the Schwarz Lemma: in the setup of norm_dslope_le_div_of_mapsTo_ball,
if there exists a point z₀ in the ball such that ‖dslope f c z₀‖ = R₂ / R₁,
then the map f is affine with the absolute value of the slope equal to R₂ / R₁.
This is an existence version of affine_of_mapsTo_ball_of_norm_dslope_eq_div above.
TODO: once the deprecated alias affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div is gone,
rename this theorem to affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div.