The Mean Value Property of Complex Differentiable Functions #
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)
:
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
circleAverage_of_differentiable_on
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[CompleteSpace E]
{f : ℂ → E}
{R : ℝ}
{c : ℂ}
(hf : ∀ z ∈ Metric.closedBall c |R|, DifferentiableAt ℂ f z)
:
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.