tendsto_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under

English

Under Schwarz-type estimates, the norm of the dslope is bounded by R2/R1 on the ball when f maps to the ball of radius R2.

Русский

При оценках типа Шварца норма dslope ограничена отношением R2/R1 на шаре, если f отправляет шар в шар радиуса R2.

LaTeX

$$$\forall z\in\mathrm{Ball}(c,R_1): \|dslope f c z\| \le R_2/R_1.$$$

Lean4

/-- **Removable singularity** theorem: if a function `f : ℂ → E` is complex differentiable and
bounded on a punctured neighborhood of `c`, then `f` has a limit at `c`. -/
theorem tendsto_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under {f : ℂ → E} {c : ℂ}
    (hd : ∀ᶠ z in 𝓝[≠] c, DifferentiableAt ℂ f z) (hb : IsBoundedUnder (· ≤ ·) (𝓝[≠] c) fun z => ‖f z - f c‖) :
    Tendsto f (𝓝[≠] c) (𝓝 <| limUnder (𝓝[≠] c) f) :=
  tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO hd hb.isLittleO_sub_self_inv

Похожие утверждения