OneStepWeylKernel

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

The coordinate-carrier radial mollifier (Weyl, part 3)

OneStepSchauderWeyl proves the mollification half of Weyl's lemma: every convolution of a weakly harmonic H¹ function with a smooth compactly supported kernel has vanishing coordinate Laplacian on the region where the reflected kernel support stays inside the domain. OneStepSchauderReproducing proves the reproducing identity, but on the Euclidean carrier EuclideanSpace ℝ (Fin d) and for the Euclidean-radial kernel radialKernelScaled.

This module bridges the two carriers. It transports the native radial kernel to the CoarseGraining coordinate carrier Vec d,

  weylKernel d ε := (radialKernelScaled d ε) ∘ toEuc ,

records its support geometry there (the Euclidean ball of radius ε is contained in the sup-metric ball of radius ε, so nothing is lost), and proves the two facts the representative half of Weyl's lemma consumes:

• convolution_weylKernel_eq_self — a C² function with vanishing coordinate Laplacian on Metric.ball x ε reproduces itself against weylKernel d ε at x;
• euclideanCoordLaplacian_mollify_eq_zero / contDiff_mollify — the mollification of the zero-extended weakly harmonic function is C^∞ and has vanishing coordinate Laplacian at every point whose closed r-ball lies in the domain, for any smooth compactly supported kernel supported in closedBall 0 r.

The second item is stated for a general kernel on purpose: the representative half runs the reproducing identity (which needs radiality) against the mollification by a mathlib ContDiffBump (which is not radial but is the only kernel for which mathlib supplies almost-everywhere convergence). Both kernels must therefore be admissible for the harmonicity half.

1. The kernel on the coordinate carrier

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.weylKernel (d : ℕ) (eps : ℝ) : HCPolySupport.Vec d → ℝ

The native unit-mass radial mollifier, read on the CoarseGraining coordinate carrier Vec d through the identification toEuc.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.weylKernel_apply {d : ℕ} (eps : ℝ) (z : HCPolySupport.Vec d) : weylKernel d eps z = radialKernelScaled d eps (toEuc z)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.weylKernel_contDiff {d : ℕ} {eps : ℝ} {n : ℕ∞} : ContDiff ℝ (↑n) (weylKernel d eps)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.weylKernel_continuous {d : ℕ} {eps : ℝ} : Continuous (weylKernel d eps)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.weylKernel_neg {d : ℕ} (eps : ℝ) (z : HCPolySupport.Vec d) : weylKernel d eps (-z) = weylKernel d eps z

Evenness. The kernel is a function of the Euclidean norm, hence even.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.weylKernel_eq_zero_of_le_norm {d : ℕ} {eps : ℝ} (heps : 0 < eps) {z : HCPolySupport.Vec d} (hz : eps ≤ ‖z‖) : weylKernel d eps z = 0

The kernel vanishes outside the sup-metric ball of radius eps: the sup norm is dominated by the Euclidean norm, so the Euclidean support constraint is the stronger one.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.support_weylKernel_subset {d : ℕ} {eps : ℝ} (heps : 0 < eps) : Function.support (weylKernel d eps) ⊆ Metric.closedBall 0 eps

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.tsupport_weylKernel_subset {d : ℕ} {eps : ℝ} (heps : 0 < eps) : tsupport (weylKernel d eps) ⊆ Metric.closedBall 0 eps

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.weylKernel_hasCompactSupport {d : ℕ} {eps : ℝ} (heps : 0 < eps) : HasCompactSupport (weylKernel d eps)

2. The reproducing identity on the coordinate carrier

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.convolution_weylKernel_eq_self {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d → ℝ} (hw : ContDiff ℝ 2 w) {x : HCPolySupport.Vec d} {eps : ℝ} (heps : 0 < eps) (hzero : ∀ y ∈ Metric.ball x eps, HCPolySupport.euclideanCoordLaplacian w y = 0) : MeasureTheory.convolution (weylKernel d eps) w (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x = w x

Reproducing identity, coordinate carrier. A C² function whose coordinate Laplacian vanishes on the sup-metric ball Metric.ball x eps reproduces itself at x against the eps-scaled radial kernel.

The proof transports the Euclidean statement reproducing_of_radial across the measure-preserving identification toEuc; the classical harmonicity hypothesis it needs is exactly what harmonicOnNhd_ball_comp_toEuc_symm manufactures from the vanishing coordinate Laplacian, at the same radius.

3. The mollification of a weakly harmonic function

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.tsupport_comp_const_sub_subset_closedBall {d : ℕ} {K : HCPolySupport.Vec d → ℝ} {r : ℝ} (hKsub : tsupport K ⊆ Metric.closedBall 0 r) (A : HCPolySupport.Vec d) : (tsupport fun (y : HCPolySupport.Vec d) => K (A - y)) ⊆ Metric.closedBall A r

The reflected support of a kernel supported in closedBall 0 r sits in closedBall A r.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.memLp_indicator_h1 {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUm : MeasurableSet U) (u : HCPolySupport.H1Function U) : MeasureTheory.MemLp (U.indicator u.toFun) 2 MeasureTheory.volume

The zero extension of an H¹ function is globally square integrable.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.locallyIntegrable_indicator_h1 {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUm : MeasurableSet U) (u : HCPolySupport.H1Function U) : MeasureTheory.LocallyIntegrable (U.indicator u.toFun) MeasureTheory.volume

The zero extension of an H¹ function is locally integrable.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.contDiff_mollify {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUm : MeasurableSet U) (u : HCPolySupport.H1Function U) {K : HCPolySupport.Vec d → ℝ} (hK_supp : HasCompactSupport K) (hK : ContDiff ℝ (↑⊤) K) : ContDiff ℝ (↑⊤) (MeasureTheory.convolution K (U.indicator u.toFun) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

The mollification of the zero extension of an H¹ function is C^∞.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.euclideanCoordLaplacian_mollify_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUopen : IsOpen U) {u : HCPolySupport.H1Function U} (hu : Support.IsWeaklyHarmonicOn U u) {K : HCPolySupport.Vec d → ℝ} {r : ℝ} (hK_supp : HasCompactSupport K) (hK : ContDiff ℝ (↑⊤) K) (hKsub : tsupport K ⊆ Metric.closedBall 0 r) {A : HCPolySupport.Vec d} (hA : Metric.closedBall A r ⊆ U) : HCPolySupport.euclideanCoordLaplacian (MeasureTheory.convolution K (U.indicator u.toFun) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) A = 0

Harmonicity of the mollification, in the coordinate Laplacian. For any smooth kernel supported in closedBall 0 r, the mollification of the zero extension of a weakly harmonic function has vanishing coordinate Laplacian at every point whose closed r-ball lies inside the domain.