The Mean Value Property of Complex Differentiable Functions

This file established the classic mean value properties of complex differentiable functions, computing the value of a function at the center of a circle as a circle average. It also provides generalized versions that computing the value of a function at arbitrary points of a disk as circle averages over suitable weighted functions.

Generalized Mean Value Properties

For a complex differentiable function f, the theorems in this section compute values of f in the interior of a disk as circle averages of a weighted function.

theorem circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ} {c w : ℂ} {s : Set ℂ} (hs : s.Countable) (h₁f : ContinuousOn f (Metric.closedBall c |R|)) (h₂f : ∀ z ∈ Metric.ball c |R| \ s, DifferentiableAt ℂ f z) (hw : 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.

theorem DiffContOnCl.circleAverage_smul_div {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ} {c w : ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c |R|)) (hw : 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 complex differentiable at all points of a closed disc of radius R and center c, 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.

@[deprecated DiffContOnCl.circleAverage_smul_div (since := "2026-02-11")]

theorem circleAverage_sub_sub_inv_smul_of_differentiable_on {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ} {c w : ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c |R|)) (hw : w ∈ Metric.ball c |R|) : Real.circleAverage (fun (z : ℂ) => ((z - c) / (z - w)) • f z) c R = f w

Alias of DiffContOnCl.circleAverage_smul_div.

---

The Generalized 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 for every point w in the disk, the circle average circleAverage (fun z ↦ ((z - c) * (z - w)⁻¹) • f z) c R equals f w.

Classic Mean Value Properties

For a complex differentiable function f, the theorems in this section compute value of f at the center of a circle as a circle average of the function. This specializes the generalized mean value properties discussed in the previous section.

theorem circleAverage_of_differentiable_on_off_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ} {c : ℂ} {s : Set ℂ} (hs : s.Countable) (h₁f : ContinuousOn f (Metric.closedBall c |R|)) (h₂f : ∀ z ∈ Metric.ball c |R| \ s, DifferentiableAt ℂ f z) : Real.circleAverage f c R = f c

The 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 the circle average circleAverage f c R equals f c.

theorem DiffContOnCl.circleAverage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ} {c : ℂ} (hf : 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.

@[deprecated DiffContOnCl.circleAverage (since := "2026-02-11")]

theorem circleAverage_of_differentiable_on {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ} {c : ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c |R|)) : Real.circleAverage f c R = f c

Alias of DiffContOnCl.circleAverage.

---

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.