The mean-value property and the sub-mean-value inequality #
Let E be a finite-dimensional real inner product space with an additive Haar measure μ, and
let u : E → F be harmonic on a neighbourhood of the closed ball closedBall x₀ R. This file
proves the mean-value property: u x₀ is the average of u over the sphere of radius R
about x₀, and the average of u over the ball of radius R about x₀,
⨍ θ ∈ S, u (x₀ + R • θ) ∂μ.toSphere = u x₀ and ⨍ x in ball x₀ R, u x ∂μ = u x₀.
The sphere of radius R about x₀ is parametrized by the unit sphere S through
θ ↦ x₀ + R • θ, and carries Mathlib's surface measure μ.toSphere, the measure that makes
μ the product of the surface and radial measures in polar coordinates. Only the sphere average
needs E ≠ 0: in the trivial space the unit sphere is empty, and the integral identities hold
with both sides zero.
The argument #
Write Φ s = ∫ θ ∈ S, u (s • θ) ∂μ.toSphere for the sphere integral at radius s about the
origin. The classical proof differentiates Φ in s and evaluates Φ' by the divergence theorem
on the ball; the proof here instead shows that the distributional derivative of Φ on (0, R)
vanishes, and then applies the du Bois-Reymond lemma
ContinuousOn.exists_eqOn_const_Ioo_of_integral_deriv_smul_eq_zero. No divergence theorem is
needed.
A harmonic function is weakly harmonic
(InnerProductSpace.HarmonicOnNhd.integral_laplacian_smul_eq_zero): ∫ Δχ • u ∂μ = 0 for every
test function χ supported in the ball. Taking χ radial, χ x = ρ (‖x‖ ^ 2), the Laplacian
Δχ x = 4 ‖x‖² ρ'' (‖x‖²) + 2 n ρ' (‖x‖²) is radial too (ContDiff.laplacian_comp_norm_sq),
and integrating in polar coordinates with the radial variable
outermost (TauCeti.integral_eq_integral_Ioi_integral_toSphere) turns the identity into
∫ s in (0, ∞), s ^ (n - 1) (4 s² ρ'' (s²) + 2 n ρ' (s²)) • Φ s = 0,
whose weight is 2 (s ^ n ρ' (s ^ 2))'. Every test function ψ on (0, R) is of the form
ψ s = s ^ n ρ' (s ^ 2) for such a ρ, namely the primitive of t ↦ ψ (√t) / (√t) ^ n, so
∫ ψ' • Φ = 0 for all of them, and Φ is constant on (0, R). Continuity of Φ on [0, R]
gives Φ R = Φ 0 = μ.toSphere(S) • u 0; integrating the sphere identity over the radii s < R, in
polar coordinates once more, gives the ball version.
The same computation applies to any C² function, with Green's identity
∫ Δχ • u = ∫ χ • Δu (ContDiffOn.integral_laplacian_smul_eq_integral_smul_laplacian) in place
of weak harmonicity: 2 ∫ ψ' • Φ = ∫ χ • Δu, and the radial χ is nonpositive when ψ is
nonnegative. So if Δ f ≥ 0 on the ball, the distributional derivative of Φ is nonnegative,
Φ is nondecreasing by the monotone du Bois-Reymond lemma
ContinuousOn.monotoneOn_of_integral_deriv_mul_nonpos, and Φ 0 ≤ Φ R is the sub-mean-value
inequality μ.toSphere(S) * f 0 ≤ ∫ θ ∈ S, f (R • θ) ∂μ.toSphere, with its ball version
μ (ball 0 R) * f 0 ≤ ∫ x in ball 0 R, f x ∂μ. These hold for f of class C² on the open ball
and continuous on its closure, with no regularity assumed on the boundary sphere.
Main declarations #
InnerProductSpace.HarmonicOnNhd.integral_toSphere_eq,InnerProductSpace.HarmonicOnNhd.average_toSphere_eq: the mean-value property on spheres, in integral and in average form.InnerProductSpace.HarmonicOnNhd.setIntegral_ball_eq,InnerProductSpace.HarmonicOnNhd.setAverage_ball_eq: the mean-value property on balls, in integral and in average form.TauCeti.mul_le_integral_toSphere_of_laplacian_nonneg,TauCeti.le_average_toSphere_of_laplacian_nonneg: the sub-mean-value inequality on spheres for functions with nonnegative Laplacian, in integral and in average form.TauCeti.mul_le_setIntegral_ball_of_laplacian_nonneg,TauCeti.le_setAverage_ball_of_laplacian_nonneg: the sub-mean-value inequality on balls, in integral and in average form.
References #
- L. C. Evans, Partial Differential Equations, Section 2.2.2, Theorem 2.
- D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 2.1.
The mean-value property on spheres. If u is harmonic on a neighbourhood of the closed
ball closedBall x₀ R, 0 ≤ R, then the integral of u over the sphere of radius R about x₀,
parametrized by the unit sphere with the surface measure μ.toSphere, is the total surface
measure times u x₀. (In the trivial space the unit sphere is empty and both sides vanish.)
The mean-value property on spheres, average form. A function harmonic on a neighbourhood
of the closed ball closedBall x₀ R, 0 ≤ R, in a nontrivial space has value u x₀ at the
centre equal to its average over the sphere of radius R about x₀.
The mean-value property on balls. If u is harmonic on a neighbourhood of the closed
ball closedBall x₀ R, then the integral of u over the open ball of radius R about x₀ is
the measure of the ball times u x₀. (For R ≤ 0 the ball is empty and both sides vanish.)
The mean-value property on balls, average form. A function harmonic on a neighbourhood
of the closed ball closedBall x₀ R, 0 < R, has value u x₀ at the centre equal to its average
over the open ball of radius R about x₀.
The sub-mean-value inequality #
The sub-mean-value inequality on spheres. If f is C² on the ball ball x₀ R,
continuous on its closure, and has nonnegative Laplacian on the ball, then f x₀ times the total
surface measure is at most the integral of f over the sphere of radius R about x₀,
parametrized by the unit sphere with the surface measure μ.toSphere.
The sub-mean-value inequality on spheres, average form. A function which is C² on the
ball ball x₀ R, continuous on its closure, and has nonnegative Laplacian on the ball, is at most
its average over the sphere of radius R about x₀ at the centre.
The sub-mean-value inequality on balls. If f is C² on the ball ball x₀ R,
continuous on its closure, and has nonnegative Laplacian on the ball, then the measure of the ball
times f x₀ is at most the integral of f over the ball.
The sub-mean-value inequality on balls, average form. A function which is C² on the
ball ball x₀ R, 0 < R, continuous on its closure, and has nonnegative Laplacian on the ball,
is at most its average over the ball at the centre.