Theorems · Theorem · complex analysis

Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_div

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z₀ : ℂ}
  [StrictConvexSpace ℝ E],
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) →
      z₀ ∈ Metric.ball c R₁ →
        ‖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 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.

Defined in

Mathlib.Analysis.Complex.Schwarz

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceStrictConvexSpace