Schwarz–Pick lemma

TheoremSchwarz–Pick lemma#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic on the open unit disc \(\mathbb{D} = \{z : |z| < 1\}\) and map \(\mathbb{D}\) into itself. Then for all \(z, w \in \mathbb{D}\), \(|f(z) - f(w)| / |1 - \overline{f(w)}\, f(z)| \le |z - w| / |1 - \bar w z|\).

theorem schwarzPick
    {f : ℂ → ℂ}
    (hf_diff : DifferentiableOn ℂ f (Metric.ball (0 : ℂ) 1))
    (hf_maps : Set.MapsTo f (Metric.ball (0 : ℂ) 1) (Metric.ball (0 : ℂ) 1)) :
    ∀ z ∈ Metric.ball (0 : ℂ) 1, ∀ w ∈ Metric.ball (0 : ℂ) 1,
      ‖(f z - f w) / (1 - star (f w) * f z)‖ ≤ ‖(z - w) / (1 - star w * z)‖

Sources

• Schwarz–Pick lemma, G. Pick (1916), building on Schwarz's lemma; see Ahlfors; Lean is holomorphic self-map of disc pseudo-hyperbolic distance nonincreasing inequality with star conj.

TheoremSchwarz–Pick lemma, derivative form#●ready to prove

Let \(\mathbb{D}=\{z\in\mathbb{C}:|z|<1\}\) be the open unit disc. If \(f:\mathbb{D}\to\mathbb{D}\) is holomorphic, then

\[ \frac{|f'(z)|}{1-|f(z)|^2}\le \frac{1}{1-|z|^2}\qquad\text{for all } z\in\mathbb{D}. \]

public theorem_wanted norm_deriv_div_one_sub_sq_le_of_mapsTo_unitBall (f : ℂ → ℂ)
    (hf_holo : DifferentiableOn ℂ f (Metric.ball 0 1))
    (hf_maps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) :
    ∀ z : ℂ, z ∈ Metric.ball 0 1 →
      norm (deriv f z) / (1 - (norm (f z)) ^ 2)
        ≤ 1 / (1 - (norm z) ^ 2)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l1_86.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.