Theorems · Theorem · potential theory

InnerProductSpace.HarmonicContOnCl.circleAverage_eq

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

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

Defined in

Mathlib.Analysis.Complex.Harmonic.MeanValue

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace