Theorems · Theorem · complex analysis

Complex.norm_fderiv_le_one_of_mapsTo_ball

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {R : ℝ} {f : E → F} {c : E},
  DifferentiableOn ℂ f (Metric.ball c R) →
    Set.MapsTo f (Metric.ball c R) (Metric.closedBall (f c) R) → 0 < R → ‖fderiv ℂ f c‖ ≤ 1

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.

Defined in

Mathlib.Analysis.Complex.Schwarz

Cited by

0 results in Mathlib

Foundations

Depth 295 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace