The converse of the mean-value property

Let E be a finite-dimensional real inner product space with an additive Haar measure μ. A function harmonic near a closed ball equals its average over the ball at the centre (InnerProductSpace.HarmonicOnNhd.setAverage_ball_eq). This file proves the converse: a function continuous on an open set U that equals its average over ball x r at the centre x, for every x ∈ U and for arbitrarily small radii r > 0, is harmonic on U. Thus harmonic functions are exactly the continuous functions with the mean-value property, and harmonicity can be verified without differentiating. This is how one shows that a limit or an envelope of harmonic functions is harmonic, as in Perron's method for the Dirichlet problem.

The argument

The first ingredient is the maximum principle for the sub-mean-value property (TauCeti.le_of_le_setAverage_ball_le_frontier, in TauCeti.MeasureTheory.Integral.SubMeanValue): if u is continuous on a compact set K and u x ≤ ⨍ y in ball x r, u y ∂μ for arbitrarily small r at every interior point x, then u is bounded on K by its bounds on frontier K.

For the converse, fix x ∈ U and a closed ball closedBall x r ⊆ U. The Dirichlet problem on the ball has a solution h, harmonic in ball x r, continuous on closedBall x r and equal to u on sphere x r (TauCeti.exists_harmonicOnNhd_ball_continuousOn_closedBall_eqOn_sphere). By the mean-value property of h, the difference u - h has the mean-value property on small balls inside ball x r, and it vanishes on the sphere. The maximum principle, applied to u - h and to h - u, gives u = h on the closed ball, so u is harmonic near x.

Main declarations

• TauCeti.harmonicOnNhd_of_setAverage_ball_eq: the converse of the mean-value property.
• TauCeti.harmonicOnNhd_iff_continuousOn_setAverage_ball_eq: the mean-value characterization of harmonic functions on an open set.

References

• L. C. Evans, Partial Differential Equations, Section 2.2.3, Theorem 3, and Problem 2.5.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 2.7.

theorem TauCeti.harmonicOnNhd_of_setAverage_ball_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → ℝ} {U : Set E} (hU : IsOpen U) (hu : ContinuousOn u U) (hmean : ∀ x ∈ U, ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ⨍ (y : E) in Metric.ball x r, u y ∂μ = u x) : InnerProductSpace.HarmonicOnNhd u U

The converse of the mean-value property. Let U be open and let u be continuous on U. If at every point x ∈ U the value u x equals the average of u over ball x r for arbitrarily small radii r > 0, then u is harmonic on U.

theorem TauCeti.harmonicOnNhd_iff_continuousOn_setAverage_ball_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → ℝ} {U : Set E} (hU : IsOpen U) : InnerProductSpace.HarmonicOnNhd u U ↔ ContinuousOn u U ∧ ∀ x ∈ U, ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ⨍ (y : E) in Metric.ball x r, u y ∂μ = u x

The mean-value characterization of harmonic functions. On an open set U, a function is harmonic if and only if it is continuous and, at every point x ∈ U, equal to its average over ball x r for arbitrarily small radii r > 0. A harmonic function in fact has this property for every radius r > 0 with closedBall x r ⊆ U (InnerProductSpace.HarmonicOnNhd.setAverage_ball_eq).