Documentation

Mathlib.Analysis.Complex.Harmonic.MeanValue

The Mean Value Property of Vector-Valued Harmonic Functions #

This file establishes the mean value property for harmonic functions f : ℂ → F, where F is an arbitrary complete real normed vector space. This generalizes the mean value property for real-valued harmonic functions.

Completeness of F cannot be dropped: circleAverage is defined in terms of the Bochner integral, which is junk (zero) whenever the target space is incomplete.

The proof reduces to the real-valued case. Circle averages commute with continuous linear maps, and composition with continuous linear maps preserves harmonicity. Thus, g (circleAverage f c R) equals circleAverage (g ∘ f) c R = g (f c) for every continuous linear functional g : F →L[ℝ] ℝ. Since continuous linear functionals separate the points of a normed space (Hahn-Banach, in the form of SeparatingDual.eq_iff_forall_dual_eq), this suffices.

Compatibility of HarmonicContOnCl with Linear Maps #

source
theorem InnerProductSpace.HarmonicContOnCl.comp_CLM {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {s : Set E} (h : HarmonicContOnCl f s) (l : F →L[ℝ] G) :
HarmonicContOnCl (⇑l ∘ f) s

Compositions of continuous ℝ-linear maps with functions that are harmonic on a set and continuous on its closure are again harmonic on the set and continuous on its closure.

The Mean Value Property #

source
theorem InnerProductSpace.HarmonicOnNhd.circleAverage_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℂ → F} {c : ℂ} {R : ℝ} (hf : 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.

source
theorem InnerProductSpace.HarmonicContOnCl.circleAverage_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℂ → F} {c : ℂ} {R : ℝ} (hf : 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.

source
@[deprecated InnerProductSpace.HarmonicOnNhd.circleAverage_eq (since := "2026-08-04")]
theorem HarmonicOnNhd.circleAverage_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℂ → F} {c : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c |R|)) :
Real.circleAverage f c R = f c

Alias of InnerProductSpace.HarmonicOnNhd.circleAverage_eq.

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.

source
@[deprecated InnerProductSpace.HarmonicContOnCl.circleAverage_eq (since := "2026-08-04")]
theorem HarmonicContOnCl.circleAverage_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℂ → F} {c : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicContOnCl f (Metric.ball c |R|)) :
Real.circleAverage f c R = f c

Alias of InnerProductSpace.HarmonicContOnCl.circleAverage_eq.

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.