Theorems · Theorem · complex analysis

circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ}
  {c w : ℂ} {s : Set ℂ},
  s.Countable →
    ContinuousOn f (Metric.closedBall c |R|) →
      (∀ z ∈ Metric.ball c |R| \ s, DifferentiableAt ℂ f z) →
        w ∈ Metric.ball c |R| → Real.circleAverage (fun z => ((z - c) / (z - w)) • f z) c R = f w

The Generalized Mean Value Property of complex differentiable functions: If f : ℂ → E is continuous on a closed disc of radius R and center c, and is complex differentiable at all but countably many points of its interior, then for every point w in the disk, the circle average circleAverage (fun z ↦ ((z - c) * (z - w)⁻¹) • f z) c R equals f w.

Defined in

Mathlib.Analysis.Complex.MeanValue

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace