Theorems · Theorem · complex analysis

Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le

∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] [CompleteSpace F] {c : ℂ} {R C : ℝ} {f : ℂ → F}
  (n : ℕ),
  0 < R →
    DiffContOnCl ℂ f (Metric.ball c R) →
      (∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) → ‖iteratedDeriv n f c‖ ≤ ↑n.factorial * C / R ^ n

Cauchy's estimate for derivatives: 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 n-th derivative at the center is at most n.factorial * C / R ^ n.

Defined in

Mathlib.Analysis.Complex.Liouville

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace