Schwarz lemma

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

• Complex.norm_deriv_le_div_of_mapsTo_ball, Complex.abs_deriv_le_div_of_mapsTo_ball: 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₁;

• Complex.dist_le_div_mul_dist_of_mapsTo_ball: if f : ℂ → E sends an open disk with center c and radius R₁ to an open disk 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;

• Complex.abs_deriv_le_one_of_mapsTo_ball: 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;

• Complex.dist_le_dist_of_mapsTo_ball_self: 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;

• Complex.abs_le_abs_of_mapsTo_ball_self: if f : ℂ → ℂ sends an open disk with center 0 to itself, then for any point z of this disk we have abs (f z) ≤ abs z.

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

• Prove that these inequalities are strict unless f is an affine map.

• Prove that any diffeomorphism of the unit disk to itself is a Möbius map.

Tags

Schwarz lemma

theorem Complex.schwarz_aux {R₁ R₂ : ℝ} {c z : ℂ} {f : ℂ → ℂ} (hd : DifferentiableOn ℂ f (Metric.ball c R₁)) (h_maps : Set.MapsTo 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_mapsTo_ball.

theorem Complex.norm_dslope_le_div_of_mapsTo_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z : ℂ} (hd : DifferentiableOn ℂ f (Metric.ball c R₁)) (h_maps : Set.MapsTo 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_mapsTo_ball_of_exists_norm_dslope_eq_div {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z₀ : ℂ} [CompleteSpace E] [StrictConvexSpace ℝ E] (hd : DifferentiableOn ℂ f (Metric.ball c R₁)) (h_maps : Set.MapsTo 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.EqOn f (fun (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_mapsTo_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_mapsTo_ball_of_exists_norm_dslope_eq_div' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c : ℂ} [CompleteSpace E] [StrictConvexSpace ℝ E] (hd : DifferentiableOn ℂ f (Metric.ball c R₁)) (h_maps : Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂)) (h_z₀ : ∃ z₀ ∈ Metric.ball c R₁, ‖dslope f c z₀‖ = R₂ / R₁) : ∃ (C : E), ‖C‖ = R₂ / R₁ ∧ Set.EqOn f (fun (z : ℂ) => f c + (z - c) • C) (Metric.ball c R₁)

theorem Complex.norm_deriv_le_div_of_mapsTo_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c : ℂ} (hd : DifferentiableOn ℂ f (Metric.ball c R₁)) (h_maps : Set.MapsTo 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_mapsTo_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z : ℂ} (hd : DifferentiableOn ℂ f (Metric.ball c R₁)) (h_maps : Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂)) (hz : z ∈ Metric.ball c R₁) : dist (f z) (f c) ≤ R₂ / R₁ * 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_mapsTo_ball {f : ℂ → ℂ} {c : ℂ} {R₁ R₂ : ℝ} (hd : DifferentiableOn ℂ f (Metric.ball c R₁)) (h_maps : Set.MapsTo 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_mapsTo_ball {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hd : DifferentiableOn ℂ f (Metric.ball c R)) (h_maps : Set.MapsTo f (Metric.ball c R) (Metric.ball c R)) (hc : f c = c) (h₀ : 0 < R) : Complex.abs (deriv f c) ≤ 1

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_mapsTo_ball_self {f : ℂ → ℂ} {c z : ℂ} {R : ℝ} (hd : DifferentiableOn ℂ f (Metric.ball c R)) (h_maps : Set.MapsTo f (Metric.ball c R) (Metric.ball c R)) (hc : f c = c) (hz : z ∈ Metric.ball c R) : dist (f z) c ≤ dist z c

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_mapsTo_ball_self {f : ℂ → ℂ} {z : ℂ} {R : ℝ} (hd : DifferentiableOn ℂ f (Metric.ball 0 R)) (h_maps : Set.MapsTo f (Metric.ball 0 R) (Metric.ball 0 R)) (h₀ : f 0 = 0) (hz : Complex.abs z < R) : Complex.abs (f z) ≤ Complex.abs z

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