Weyl's lemma #
Let E be a finite-dimensional real inner product space with an additive Haar measure μ, and
let Ω ⊆ E be open. A function u locally integrable on Ω is weakly harmonic there
(TauCeti.WeaklyHarmonicOn) if
∫ Δφ • u ∂μ = 0 for every test function φ ∈ 𝓓(Ω),
that is, if its distributional Laplacian vanishes on Ω. Every harmonic function is weakly
harmonic (InnerProductSpace.HarmonicOnNhd.weaklyHarmonicOn). Weyl's lemma is
the converse for finite-dimensional real normed coefficient spaces: a weakly harmonic function
agrees almost everywhere on Ω with a function harmonic on Ω, that is, twice continuously
differentiable with vanishing Laplacian. No differentiability
of u is assumed, so a locally integrable distributional solution of Δu = 0 is, after
modification on a null set, a classical one.
For a function continuous on Ω no modification is needed, and harmonicity on Ω is equivalent
to weak harmonicity there (TauCeti.harmonicOnNhd_iff_weaklyHarmonicOn).
The argument #
Fix a closed ball closedBall x (3R) ⊆ Ω, let f be u cut off to it, and mollify:
uₙ = ρₙ ⋆ f with ρₙ a normalized smooth bump of radius rₙ → 0, rₙ ≤ R. Each uₙ is
smooth, and on ball x (2R) its Laplacian is ∫ Δρₙ(y - t) u(t) dt, the pairing of u with the
Laplacian of the test function t ↦ ρₙ(y - t), so it vanishes: uₙ is harmonic there. By the
mean-value property, uₙ y is the average of uₙ over ball y R for y ∈ ball x R, so
|uₙ y - ⨍_{ball y R} f| ≤ ‖uₙ - f‖_{L¹} / μ(ball 0 R),
and uₙ → f in L¹ makes the convergence of uₙ to y ↦ ⨍_{ball y R} f uniform on ball x R.
A locally uniform limit of harmonic functions is harmonic, and since also uₙ → f almost
everywhere (Lebesgue differentiation), this limit is a harmonic function equal to u almost
everywhere on ball x R.
For real-valued functions, these local harmonic representatives are glued by the limit of the
ball averages of u: near each point, the average of u over every small ball about y equals
the value at y of the
local representative, by its mean-value property. This defines a single function, harmonic on Ω
and equal to u almost everywhere on Ω. For finite-dimensional coefficients, apply the scalar
result to each continuous coordinate functional and reconstruct by a finite sum.
Main declarations #
TauCeti.WeaklyHarmonicOn: weak harmonicity on an open set.TauCeti.WeaklyHarmonicOn.mono,TauCeti.WeaklyHarmonicOn.congr_ae,TauCeti.WeaklyHarmonicOn.add, …: weak harmonicity is local, depends only on the a.e. class of the function onΩ, and is closed under the linear operations.TauCeti.WeaklyHarmonicOn.clm_comp: continuous linear maps preserve weak harmonicity.TauCeti.HasWeakLineDerivOn.weaklyHarmonicOn,TauCeti.HasWeakFDerivOn.weaklyHarmonicOn: weak derivatives of weakly harmonic functions are weakly harmonic.TauCeti.WeaklyHarmonicOn.exists_harmonicOnNhd_ae_eq: Weyl's lemma.TauCeti.harmonicOnNhd_iff_weaklyHarmonicOn: a continuous function is harmonic onΩif and only if it is weakly harmonic there.
References #
- H. Weyl, The method of orthogonal projection in potential theory, Duke Math. J. 7 (1940), 411–444.
- L. Hörmander, The Analysis of Linear Partial Differential Operators I, Theorem 4.4.1.
- G. B. Folland, Introduction to Partial Differential Equations, 2nd ed., Corollary 2.20.
WeaklyHarmonicOn μ Ω u says that u is weakly harmonic on the open set Ω: it is
locally integrable on Ω and its distributional Laplacian vanishes there, that is,
∫ Δφ • u ∂μ = 0 for every test function φ ∈ 𝓓(Ω).
Local integrability is part of the definition because MeasureTheory.integral is 0 on a
non-integrable function, so without it the identity would hold for junk reasons.
Instances For
The constructor-and-eliminator form of WeaklyHarmonicOn. The definition is sealed by the
module system, so downstream modules use this theorem rather than unfolding it.
A weakly harmonic function on Ω is locally integrable on Ω.
The identity defining weak harmonicity: ∫ Δφ • w ∂μ = 0 for every test function on Ω.
A weakly harmonic function on Ω is weakly harmonic on every smaller open set: weak
harmonicity is a local notion.
The zero function is weakly harmonic, for every μ.
Weak harmonicity is preserved by negation.
Weak harmonicity is preserved by multiplication by a real scalar.
Weak derivatives of weakly harmonic functions are weakly harmonic. If w is weakly
harmonic on Ω and w' is a weak derivative of w in the direction v on Ω, then w' is
weakly harmonic on Ω: the Laplacian commutes with ∂_v on test functions.
The full weak Fréchet derivative of a weakly harmonic function is weakly harmonic. Each evaluation is a weak directional derivative, and evaluation commutes with integration.
Replacing w by a function agreeing with it almost everywhere on Ω preserves weak
harmonicity: only the restriction of w to Ω is seen.
Weak harmonicity is preserved by addition.
Weak harmonicity is preserved by subtraction.
A continuous linear map of complete real normed spaces preserves weak harmonicity.
A harmonic function is weakly harmonic.
Weyl's lemma with finite-dimensional coefficients. A weakly harmonic function with values in a finite-dimensional real normed space agrees almost everywhere with a function harmonic on the same open set. No differentiability of the original function is assumed.
Weyl's lemma for continuous functions. A function continuous on the open set Ω is
harmonic on Ω if and only if it is weakly harmonic there: ∫ Δφ • u ∂μ = 0 for every test
function φ ∈ 𝓓(Ω).