Theorems · Theorem · potential theory

InnerProductSpace.HarmonicOnNhd.circleAverage_eq

∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [CompleteSpace F] {f : ℂ → F} {c : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c |R|) → Real.circleAverage f c R = f c

The Mean Value Property of harmonic functions: If f : ℂ → 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.

Defined in

Mathlib.Analysis.Complex.Harmonic.MeanValue

Cited by

5 results in Mathlib

Foundations

Depth 288 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace