English
Two-case Schwarz lemma: if differentiable and mapsTo ball, then the norm dslope is bounded by R2/R1 on the ball.
Русский
Двухвариантная лемма Шварца: если дифференцируемо и отображает шар в шар, то норма dslope ограничена отношением R2/R1.
LaTeX
$$$\forall z\in\mathrm{Ball}(c,R_1): \|dslope f c z\| \le R_2/R_1.$$$
Lean4
/-- Two cases of the **Schwarz Lemma** (derivative and distance), merged together. -/
theorem norm_dslope_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
(h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) : ‖dslope f c z‖ ≤ R₂ / R₁ :=
by
have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
have hR₂ : 0 < R₂ := nonempty_ball.1 ⟨f z, h_maps hz⟩
rcases eq_or_ne (dslope f c z) 0 with hc | hc
· rw [hc, norm_zero]; exact div_nonneg hR₂.le hR₁.le
rcases exists_dual_vector ℂ _ hc with ⟨g, hg, hgf⟩
have hg' : ‖g‖₊ = 1 := NNReal.eq hg
have hg₀ : ‖g‖₊ ≠ 0 := by simpa only [hg'] using one_ne_zero
calc
‖dslope f c z‖ = ‖dslope (g ∘ f) c z‖ :=
by
rw [g.dslope_comp, hgf, RCLike.norm_ofReal, abs_norm]
exact fun _ => hd.differentiableAt (ball_mem_nhds _ hR₁)
_ ≤ R₂ / R₁ :=
by
refine schwarz_aux (g.differentiable.comp_differentiableOn hd) (MapsTo.comp ?_ h_maps) hz
simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_ball hg₀ (f c) R₂
