OneStepWeylRepresentative #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Weyl's lemma, representative half #
OneStepSchauderWeyl bridged variational harmonicity to classical
harmonicity for the smoothings of a weakly harmonic H¹ function. What was
missing — the residue — is the statement that some such smoothing is the
function, almost everywhere:
for
uweakly harmonic on an openUandε > 0there is a globallyC^∞functionv, classically harmonic on the inner regionΩ_ε = {p : closedBall p ε ⊆ U}, withv = ualmost everywhere onΩ_ε.
This module proves it (exists_harmonicRepresentative,
exists_harmonicRepresentative_on), and then removes the inner-region
restriction: exists_harmonicRepresentative_full glues the representatives at
radii 1/(k+1) into a single function which is classically harmonic on all
of U and agrees almost everywhere with the zero extension 𝟙_U u — the
statement of Weyl's lemma proper, and the one the excess-decay compositions
consume (OneStepSchauderComposeInterior, OneStepSchauderComposeBoundary).
The device #
Two mollifications are used, and each supplies exactly one thing the other cannot.
- the radial kernel
weylKernel d (ε/2)reproduces classically harmonic functions (convolution_weylKernel_eq_self) — radiality is what the spherical mean value property needs, and mathlib'sContDiffBumpis not radial; - mathlib's bump kernels
(weylBump ρ n).normed volumeconverge to the function almost everywhere (ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable) — the Lebesgue differentiation input, which the radial kernel does not carry in mathlib.
Both are smooth and compactly supported, so both mollify a weakly harmonic
function to a function with vanishing coordinate Laplacian
(euclideanCoordLaplacian_mollify_eq_zero, stated for a general kernel exactly
for this reason). Writing K := weylKernel d (ε/2), b_n for the n-th bump
mollification of the zero extension g := 𝟙_U u, and v := K ⋆ g, the two are
tied together at a point p of Ω_ε by
(b_n) p = (K ⋆ b_n) p -- K reproduces the harmonic b_n on ball p (ε/2)
= (φ_n ⋆ (K ⋆ g)) p -- associativity + commutativity of convolution
= (φ_n ⋆ v) p ,
and letting n → ∞: the left side tends to g p for almost every p, the
right side to v p because v is continuous. Note that no ε-independence
argument is needed: the radial kernel is taken at half the margin, so a
single fixed v serves the whole inner region.
1. The inner region #
The ε-inner region of U: the points whose closed sup-metric ε-ball lies inside U.
Equations
Instances For
The inner region is open. The closed ball is compact and U is open, so a whole
neighbourhood of admissible centres is available.
2. The bump sequence #
The mathlib bump family used for the Lebesgue-differentiation input: outer radii
ρ/(n+1) → 0, inner radii exactly half of those (so the ratio stays bounded by 2, as
ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable requires).
Equations
Instances For
3. Associativity and commutativity of the two mollifications #
Commutativity of scalar convolution on the coordinate carrier.
Associativity of scalar convolution for two smooth compactly supported kernels against a
locally integrable field. The four integrability side conditions of
MeasureTheory.convolution_assoc are discharged from compact support alone.
The two mollifications commute. K ⋆ (b ⋆ g) = b ⋆ (K ⋆ g) for smooth compactly
supported K, b and locally integrable g.
4. Weyl's lemma, representative half #
Weyl's lemma, representative half.
For u weakly harmonic on an open set U and ε > 0 there is a globally C^∞ function v
which is classically harmonic (mathlib's HarmonicOnNhd, after transport across toEuc) on the
inner region Ω_ε = {p : closedBall p ε ⊆ U} and agrees with u at almost every point of Ω_ε.
U is not assumed bounded or convex.
Weyl's lemma, representative half, on a supplied window. The window form consumed by the
interior Schauder producer: on any measurable W all of whose points carry an ε-ball inside U,
the weakly harmonic u has a globally smooth, classically harmonic representative.
5. Weyl's lemma on the whole domain #
Two continuous functions which agree almost everywhere on an open set agree on it.
Weyl's lemma.
For u weakly harmonic on an open set U there is a function v on the coordinate carrier
which is classically harmonic (mathlib's HarmonicOnNhd, after transport across toEuc) on all
of U, and which agrees almost everywhere with the zero extension of u.
The fixed-radius representative exists_harmonicRepresentative is harmonic only on the inner
region Ω_ε; here the representatives at radii 1/(k+1) are glued. They are pairwise consistent
because each equals u almost everywhere on the common inner region and each is continuous
(eqOn_of_ae_eq_of_continuous), so on every inner region the sequence is eventually constant and
its limit is a single well-defined function.
The second conjunct is stated as a global almost-everywhere identity with the zero extension
𝟙_U u, which is what makes v square integrable on any window (see
memLp_harmonicRepresentative_full): v is not claimed smooth off U.
Weyl's lemma, packaged for the excess-decay chain. The representative is additionally
square integrable on every window, because it agrees almost everywhere with the zero extension of
u.
6. Harmonic representatives and measure-preserving involutions #
A classical harmonic representative is continuous on its coordinate window.
Harmonicity transfers through equality on an open coordinate window.
On an invariant open set, an a.e.-equal continuous representative inherits oddness.
Symmetrization makes a harmonic a.e. representative globally odd under a continuous measure-preserving involution, without changing it on the invariant open set.