English
If the Scharz lemma bounds hold and equality occurs for a norm of dslope at a point z0 in the ball, then f is affine on the ball.
Русский
Если пределы Шварца выполняются и равенство достигается для нормы dslope в точке z0 внутри шара, то f является аффиной на шаре.
LaTeX
$$$\forall hd, hmaps, hz, h_eq:\; (\|dslope f c z0\| = R_2/R_1) \Rightarrow \; f(z) = f(c) + (z-c) \cdot dslope f c z0 \text{ на } \mathrm{Ball}(c,R_1).$$$
Lean4
/-- **Removable singularity** theorem: if a function `f : ℂ → E` is complex differentiable on a
punctured neighborhood of `c` and $f(z) - f(c)=o((z-c)^{-1})$, then `f` has a limit at `c`. -/
theorem tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO {f : ℂ → E} {c : ℂ}
(hd : ∀ᶠ z in 𝓝[≠] c, DifferentiableAt ℂ f z) (ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹) :
Tendsto f (𝓝[≠] c) (𝓝 <| limUnder (𝓝[≠] c) f) :=
by
rw [eventually_nhdsWithin_iff] at hd
have : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ { c }) := fun z hz =>
(hz.1 hz.2).differentiableWithinAt
have H := differentiableOn_update_limUnder_of_isLittleO hd this ho
exact continuousAt_update_same.1 (H.differentiableAt hd).continuousAt
