The Mean Value Property of Harmonic Functions on the Complex Plane

theorem HarmonicOnNhd.circleAverage_eq {f : ℂ → ℝ} {c : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c |R|)) : Real.circleAverage f c R = f c

The Mean Value Property of harmonic functions: If f : ℂ → ℝ is harmonic in a neighborhood of a closed disc of radius R and center c, then the circle average circleAverage f c R equals f c.