mathlib3 documentation

analysis.complex.schwarz

Schwarz lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove several versions of the Schwarz lemma.

Implementation notes #

We prove some versions of the Schwarz lemma for a map f : ℂ → E taking values in any normed space over complex numbers.

TODO #

Tags #

Schwarz lemma

theorem complex.schwarz_aux {R₁ R₂ : } {c z : } {f : } (hd : differentiable_on f (metric.ball c R₁)) (h_maps : set.maps_to f (metric.ball c R₁) (metric.ball (f c) R₂)) (hz : z metric.ball c R₁) :
dslope f c z R₂ / R₁

An auxiliary lemma for complex.norm_dslope_le_div_of_maps_to_ball.

theorem complex.norm_dslope_le_div_of_maps_to_ball {E : Type u_1} [normed_add_comm_group E] [normed_space E] {R₁ R₂ : } {f : E} {c z : } (hd : differentiable_on f (metric.ball c R₁)) (h_maps : set.maps_to f (metric.ball c R₁) (metric.ball (f c) R₂)) (hz : z metric.ball c R₁) :
dslope f c z R₂ / R₁

Two cases of the Schwarz Lemma (derivative and distance), merged together.

theorem complex.affine_of_maps_to_ball_of_exists_norm_dslope_eq_div {E : Type u_1} [normed_add_comm_group E] [normed_space E] {R₁ R₂ : } {f : E} {c z₀ : } [complete_space E] [strict_convex_space E] (hd : differentiable_on f (metric.ball c R₁)) (h_maps : set.maps_to f (metric.ball c R₁) (metric.ball (f c) R₂)) (h_z₀ : z₀ metric.ball c R₁) (h_eq : dslope f c z₀ = R₂ / R₁) :
set.eq_on f (λ (z : ), f c + (z - c) dslope f c z₀) (metric.ball c R₁)

Equality case in the Schwarz Lemma: in the setup of norm_dslope_le_div_of_maps_to_ball, if ‖dslope f c z₀‖ = R₂ / R₁ holds at a point in the ball then the map f is affine.

theorem complex.affine_of_maps_to_ball_of_exists_norm_dslope_eq_div' {E : Type u_1} [normed_add_comm_group E] [normed_space E] {R₁ R₂ : } {f : E} {c : } [complete_space E] [strict_convex_space E] (hd : differentiable_on f (metric.ball c R₁)) (h_maps : set.maps_to f (metric.ball c R₁) (metric.ball (f c) R₂)) (h_z₀ : (z₀ : ) (H : z₀ metric.ball c R₁), dslope f c z₀ = R₂ / R₁) :
(C : E), C = R₂ / R₁ set.eq_on f (λ (z : ), f c + (z - c) C) (metric.ball c R₁)
theorem complex.norm_deriv_le_div_of_maps_to_ball {E : Type u_1} [normed_add_comm_group E] [normed_space E] {R₁ R₂ : } {f : E} {c : } (hd : differentiable_on f (metric.ball c R₁)) (h_maps : set.maps_to f (metric.ball c R₁) (metric.ball (f c) R₂)) (h₀ : 0 < R₁) :
deriv f c R₂ / R₁

The Schwarz Lemma: if f : ℂ → E sends an open disk with center c and a positive radius R₁ to an open ball with center f c and radius R₂, then the absolute value of the derivative of f at c is at most the ratio R₂ / R₁.

theorem complex.dist_le_div_mul_dist_of_maps_to_ball {E : Type u_1} [normed_add_comm_group E] [normed_space E] {R₁ R₂ : } {f : E} {c z : } (hd : differentiable_on f (metric.ball c R₁)) (h_maps : set.maps_to f (metric.ball c R₁) (metric.ball (f c) R₂)) (hz : z metric.ball c R₁) :
has_dist.dist (f z) (f c) R₂ / R₁ * has_dist.dist z c

The Schwarz Lemma: if f : ℂ → E sends an open disk with center c and radius R₁ to an open ball with center f c and radius R₂, then for any z in the former disk we have dist (f z) (f c) ≤ (R₂ / R₁) * dist z c.

theorem complex.abs_deriv_le_div_of_maps_to_ball {f : } {c : } {R₁ R₂ : } (hd : differentiable_on f (metric.ball c R₁)) (h_maps : set.maps_to f (metric.ball c R₁) (metric.ball (f c) R₂)) (h₀ : 0 < R₁) :
complex.abs (deriv f c) R₂ / R₁

The Schwarz Lemma: if f : ℂ → ℂ sends an open disk with center c and a positive radius R₁ to an open disk with center f c and radius R₂, then the absolute value of the derivative of f at c is at most the ratio R₂ / R₁.

theorem complex.abs_deriv_le_one_of_maps_to_ball {f : } {c : } {R : } (hd : differentiable_on f (metric.ball c R)) (h_maps : set.maps_to f (metric.ball c R) (metric.ball c R)) (hc : f c = c) (h₀ : 0 < R) :

The Schwarz Lemma: if f : ℂ → ℂ sends an open disk of positive radius to itself and the center of this disk to itself, then the absolute value of the derivative of f at the center of this disk is at most 1.

theorem complex.dist_le_dist_of_maps_to_ball_self {f : } {c z : } {R : } (hd : differentiable_on f (metric.ball c R)) (h_maps : set.maps_to f (metric.ball c R) (metric.ball c R)) (hc : f c = c) (hz : z metric.ball c R) :

The Schwarz Lemma: if f : ℂ → ℂ sends an open disk to itself and the center c of this disk to itself, then for any point z of this disk we have dist (f z) c ≤ dist z c.

theorem complex.abs_le_abs_of_maps_to_ball_self {f : } {z : } {R : } (hd : differentiable_on f (metric.ball 0 R)) (h_maps : set.maps_to f (metric.ball 0 R) (metric.ball 0 R)) (h₀ : f 0 = 0) (hz : complex.abs z < R) :

The Schwarz Lemma: if f : ℂ → ℂ sends an open disk with center 0 to itself, the for any point z of this disk we have abs (f z) ≤ abs z.