Theorems · Theorem · complex analysis

DiffContOnCl.circleAverage

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ} {c : ℂ},
  DiffContOnCl ℂ f (Metric.ball c |R|) → Real.circleAverage f c R = f c

The Mean Value Property of complex differentiable functions: If f : ℂ → E is complex differentiable at all points of a closed disc of radius R and center c, then the circle average circleAverage f c R equals f c.

Defined in

Mathlib.Analysis.Complex.MeanValue

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace