Theorems · Theorem · complex analysis

Complex.norm_deriv_le_of_forall_mem_sphere_norm_le

∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] {c : ℂ} {R C : ℝ} {f : ℂ → F},
  0 < R → DiffContOnCl ℂ f (Metric.ball c R) → (∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) → ‖deriv f c‖ ≤ C / R

Cauchy's estimate for the first order derivative: 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. Note that this theorem does not require the completeness of the codomain of f. In contrast, the completeness is needed for norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le.

Defined in

Mathlib.Analysis.Complex.Liouville

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace