English
If a differentiable function f is bounded on its domain, then all its derivatives are controlled; in particular, the derivative can be forced to vanish at a point if the bound implies zero growth.
Русский
Если дифференцируемая функция ограничена на области определения, то её производная может быть вынужденной к нулю в точке при ограничениях роста функции.
LaTeX
$$$\\|\\mathrm{deriv}\, f\\, c\\| \\le C/R\\quad\\Rightarrow\\quad f\\text{ constant under suitable boundedness}.$$$
Lean4
/-- If `f` is complex differentiable on an open disc of radius `R > 0`, is continuous on its
closure, and its values on the boundary circle of this disc are bounded from above by `C`, then the
norm of its derivative at the center is at most `C / R`. -/
theorem norm_deriv_le_of_forall_mem_sphere_norm_le {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R)
(hd : DiffContOnCl ℂ f (ball c R)) (hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) : ‖deriv f c‖ ≤ C / R :=
by
set e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
have : HasDerivAt (e ∘ f) (e (deriv f c)) c :=
e.hasFDerivAt.comp_hasDerivAt c (hd.differentiableAt isOpen_ball <| mem_ball_self hR).hasDerivAt
calc
‖deriv f c‖ = ‖deriv (e ∘ f) c‖ := by
rw [this.deriv]
exact (UniformSpace.Completion.norm_coe _).symm
_ ≤ C / R :=
norm_deriv_le_aux hR (e.differentiable.comp_diffContOnCl hd) fun z hz =>
(UniformSpace.Completion.norm_coe _).trans_le (hC z hz)
