HarmonicMollifyWeyl

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Smooth approximation of a weakly harmonic function (interior Weyl lemma)

HarmonicWeak fixes the distributional predicate IsWeaklyHarmonicOn and shows it is consistent with the classical one for C^2 functions. It cannot bootstrap: a function that is merely locally integrable and weakly harmonic is not known there to be smooth, so none of the classical interior estimates apply to it. This module removes that obstruction on the interior, by mollification.

The argument

Write K_delta for the normalized smooth radial density of HarmonicMollifyKernel, supported in the Euclidean annulus (delta/2, delta) and of radial moment 1, and let

  (mollify delta u) (x) = ( int u (y) K_delta (|y - x|) dy ) / M_delta ,

where M_delta is the total mass of the density.

1. Smoothness. The kernel is smooth and compactly supported, so the convolution of a locally integrable function with it is smooth (contDiff_mollify, from Mathlib's contDiff_convolution_right).
2. The mass does not depend on the scale. The difference of two normalized densities has vanishing radial moment, hence integrates to zero (mollifierMass_eq_of_pos).
3. The mollification does not depend on the scale. This is the heart of the matter. The difference K_delta - K_epsilon is smooth, radial, supported in an annulus away from the origin, and of vanishing radial moment; so HarmonicSphereBump produces a compactly supported radial potential whose Laplacian is exactly that difference, and HarmonicMollifyKernel upgrades that potential to C^infty. Pairing the weak harmonicity of u against it gives mollify delta u = mollify epsilon u at every point whose closed ball of radius max delta epsilon lies in the harmonicity set (mollify_eq_mollify_of_isWeaklyHarmonicOn).
4. Self-adjointness. Fubini for the symmetric kernel gives int (mollify delta u) psi = int u (mollify delta psi) (integral_mollify_mul).
5. Passing to the limit. For a continuous compactly supported psi the mollification mollify delta psi converges to psi uniformly, by the concentration estimate of HarmonicMeanValue together with uniform continuity; all the mollifications live in one fixed compact set. Combining with 3 and 4, the distribution of u agrees with that of the fixed smooth function mollify r u on the interior set, and the fundamental lemma of the calculus of variations turns this into almost-everywhere equality.

The classical harmonicity of the smooth representative is then read off from HarmonicWeak: it is weakly harmonic because it agrees a.e. with u, and it is C^2, so its coordinate Laplacian vanishes pointwise.

The whole Weyl mechanism is packaged in exists_contDiff_ae_eq_of_isWeaklyHarmonicOn, whose statement mentions no oscillation, no cube and no scale family: it is the reusable part.

Portability

This file depends only on Mathlib and on CoarseGraining (Homogenization.*) and on other files of this same harmonic/oscillation layer. It mentions no object of the manuscript: no model, no cutoff, no shell, no corrector, no cube. It is intended to be portable into CoarseGraining by a single mechanical namespace rename.

Divergences and hypotheses

• Local integrability of u on the whole carrier is assumed, rather than on the harmonicity set only. This is what makes the convolution meaningful without a cut-off bookkeeping layer; a consumer holding an L^1 function on a bounded set extends it by zero.
• The interior set V is described by a uniform interior radius r rather than by compact containment. The two are equivalent for the sets used downstream and the uniform radius is what the argument actually consumes.

Contents

• mollifierMass, mollify -- the smoothing operator.
• contDiff_mollify -- smoothness.
• mollifierMass_eq_of_pos, mollify_eq_mollify_of_isWeaklyHarmonicOn -- scale independence.
• integral_mollify_mul -- self-adjointness (Fubini).
• abs_mollify_sub_le, mollify_eq_zero_of_notMem, hasCompactSupport_mollify -- concentration and support.
• exists_contDiff_ae_eq_of_isWeaklyHarmonicOn -- the interior Weyl lemma.

References

• ABK26, e.nablaw.oscillations (the eventual consumer).

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.norm_le_euclideanNorm {d : ℕ} (x : HCPolySupport.Vec d) : ‖x‖ ≤ euclideanNorm x

The Euclidean gauge dominates the sup norm of the carrier.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanNorm_sub_comm {d : ℕ} (x y : HCPolySupport.Vec d) : euclideanNorm (x - y) = euclideanNorm (y - x)

The Euclidean gauge is symmetric in its two arguments.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollifierMass (m : ℕ) (δ : ℝ) : ℝ

The mass of the radial mollifying density at scale δ.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integrable_mollifierProfile_comp {m : ℕ} {δ : ℝ} (hδ : 0 < δ) (z : HCPolySupport.Vec (m + 1)) : MeasureTheory.Integrable (fun (x : HCPolySupport.Vec (m + 1)) => mollifierProfile m δ (euclideanNorm (x - z))) MeasureTheory.volume

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integral_mollifierProfile_comp (m : ℕ) (δ : ℝ) (z : HCPolySupport.Vec (m + 1)) : ∫ (x : HCPolySupport.Vec (m + 1)), mollifierProfile m δ (euclideanNorm (x - z)) = mollifierMass m δ

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollifierMass_pos {m : ℕ} {δ : ℝ} (hδ : 0 < δ) : 0 < mollifierMass m δ

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollifierMass_eq_of_pos {m : ℕ} {δ ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) : mollifierMass m δ = mollifierMass m ε

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollify (m : ℕ) (δ : ℝ) (u : HCPolySupport.Vec (m + 1) → ℝ) : HCPolySupport.Vec (m + 1) → ℝ

The mollification of u at scale δ: the average of u against the normalized radial density supported in the Euclidean annulus (δ/2, δ).

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_mollifierKernel {m : ℕ} {δ : ℝ} (hδ : 0 < δ) : ContDiff ℝ ↑⊤ fun (w : HCPolySupport.Vec (m + 1)) => mollifierProfile m δ (euclideanNorm w)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasCompactSupport_mollifierKernel {m : ℕ} {δ : ℝ} (hδ : 0 < δ) : HasCompactSupport fun (w : HCPolySupport.Vec (m + 1)) => mollifierProfile m δ (euclideanNorm w)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_mollify {m : ℕ} {δ : ℝ} (hδ : 0 < δ) {u : HCPolySupport.Vec (m + 1) → ℝ} (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) : ContDiff ℝ (↑⊤) (mollify m δ u)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integrable_mul_mollifierProfile_comp {m : ℕ} {δ : ℝ} (hδ : 0 < δ) {u : HCPolySupport.Vec (m + 1) → ℝ} (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) (x : HCPolySupport.Vec (m + 1)) : MeasureTheory.Integrable (fun (y : HCPolySupport.Vec (m + 1)) => u y * mollifierProfile m δ (euclideanNorm (y - x))) MeasureTheory.volume

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollify_eq_mollify_of_isWeaklyHarmonicOn {m : ℕ} {U : Set (HCPolySupport.Vec (m + 1))} {u : HCPolySupport.Vec (m + 1) → ℝ} (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) (hw : IsWeaklyHarmonicOn U u) {δ ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) {x : HCPolySupport.Vec (m + 1)} (hball : HCPolySupport.euclideanClosedBall x (max δ ε) ⊆ U) : mollify m δ u x = mollify m ε u x

Mollification of a weakly harmonic function does not depend on the scale.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integral_mollify_mul {m : ℕ} {δ : ℝ} (hδ : 0 < δ) {u ψ : HCPolySupport.Vec (m + 1) → ℝ} (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) : ∫ (x : HCPolySupport.Vec (m + 1)), mollify m δ u x * ψ x = ∫ (y : HCPolySupport.Vec (m + 1)), u y * mollify m δ ψ y

The mollification is self-adjoint. Pairing the mollification of a locally integrable function against a compactly supported continuous test function is the same as pairing the function against the mollified test function. This is Fubini for the symmetric kernel.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.abs_mollify_sub_le {m : ℕ} {δ : ℝ} (hδ : 0 < δ) {ψ : HCPolySupport.Vec (m + 1) → ℝ} (hψ : Continuous ψ) {y : HCPolySupport.Vec (m + 1)} {η : ℝ} (hosc : ∀ x ∈ HCPolySupport.euclideanClosedBall y δ, |ψ x - ψ y| ≤ η) : |mollify m δ ψ y - ψ y| ≤ η

Concentration of the mollification. If a continuous function varies by at most η on the closed Euclidean ball of radius δ about y, then its mollification at scale δ differs from its value at y by at most η.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollify_eq_zero_of_notMem {m : ℕ} {δ R : ℝ} (hδ : 0 < δ) {ψ : HCPolySupport.Vec (m + 1) → ℝ} (hR : tsupport ψ ⊆ Metric.closedBall 0 R) {y : HCPolySupport.Vec (m + 1)} (hy : y ∉ Metric.closedBall 0 (R + δ)) : mollify m δ ψ y = 0

Outside a slight enlargement of its support the mollification vanishes.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasCompactSupport_mollify {m : ℕ} {δ R : ℝ} (hδ : 0 < δ) {ψ : HCPolySupport.Vec (m + 1) → ℝ} (hR : tsupport ψ ⊆ Metric.closedBall 0 R) : HasCompactSupport (mollify m δ ψ)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.exists_contDiff_ae_eq_of_isWeaklyHarmonicOn {m : ℕ} {U V : Set (HCPolySupport.Vec (m + 1))} (hV : IsOpen V) {r : ℝ} (hr : 0 < r) (hsub : ∀ x ∈ V, HCPolySupport.euclideanClosedBall x r ⊆ U) {u : HCPolySupport.Vec (m + 1) → ℝ} (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) (hw : IsWeaklyHarmonicOn U u) : ∃ (v : HCPolySupport.Vec (m + 1) → ℝ), ContDiff ℝ (↑⊤) v ∧ (∀ᵐ (x : HCPolySupport.Vec (m + 1)), x ∈ V → v x = u x) ∧ ∀ x ∈ V, HCPolySupport.euclideanCoordLaplacian v x = 0

Interior smoothness of a weakly harmonic function (Weyl's lemma).

If u is locally integrable and weakly harmonic on U, and V is an open set all of whose points carry a closed Euclidean ball of a fixed radius r inside U, then u agrees almost everywhere on V with a smooth function whose coordinate Laplacian vanishes at every point of V.

The witness is the mollification mollify m r u. Three facts drive the proof: the mollification is smooth because the kernel is; it does not depend on the scale, because the difference of two normalized radial densities has vanishing radial moment and is therefore the Laplacian of a smooth compactly supported radial potential, against which the weak harmonicity of u pairs to zero; and the mollification is self-adjoint, so that pairing it against a test function and letting the scale shrink recovers the pairing of u itself.