English
If f is differentiable on the closed disc and circleAverage equals the center value, then f is constant on the disc.
Русский
Если f дифференцируема на замкнутом диске и окружная средняя равна значению в центре, то f постоянна на диске.
LaTeX
$$$circleAverage f c R = f(c)$ for differentiable f on closedBall(c,R)$$
Lean4
/-- 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`.
-/
theorem circleAverage_of_differentiable_on (hf : ∀ z ∈ closedBall c |R|, DifferentiableAt ℂ f z) :
circleAverage f c R = f c :=
circleAverage_of_differentiable_on_off_countable Set.countable_empty
(fun x hx ↦ (hf x hx).continuousAt.continuousWithinAt) fun z hz ↦ hf z (by simp_all [le_of_lt])
