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|))
:
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.
theorem
HarmonicContOnCl.circleAverage_eq
{f : ℂ → ℝ}
{c : ℂ}
{R : ℝ}
(h₁f : InnerProductSpace.HarmonicContOnCl f (Metric.ball c |R|))
:
The Mean Value Property of harmonic functions: If f : ℂ → ℝ is harmonic on a disc of radius
|R| and center c and continuous on its closure, then the circle average circleAverage f c R
equals f c.