OneStepSchauderWeyl

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

Weyl's lemma by mollification (Weyl, part 2)

The competitor of the Schauder gradient-Hölder estimate is produced as an H1Function W satisfying the variational condition Support.IsWeaklyHarmonicOn. This module proves that every CoarseGraining convex smoothing of such a function is classically harmonic on the interior ball:

• isWeaklyHarmonicOn_test_of_contDiff — instantiate the H¹₀ quantifier at a smooth compactly supported test;
• isWeaklyHarmonicOn_integral_mul_euclideanCoordLaplacian_eq_zero — the distributional form ∫_U u · Δψ = 0, obtained by moving the remaining derivative off the gradient, one coordinate at a time;
• euclideanCoordLaplacian_convolution_indicator_eq_zero — hence the mollified function has vanishing coordinate Laplacian wherever the reflected kernel support stays inside U;
• contDiff_convexApproxSmoothH1, euclideanCoordLaplacian_convexApproxSmoothH1_eq_zero, harmonicOnNhd_convexApproxSmoothH1_of_weaklyHarmonic — the same for CoarseGraining's concrete convex smoothing H1Function.convexApproxSmoothH1, transported across toEuc into Mathlib's HarmonicOnNhd at the full radius r.

Why the radius is not lost

The mollifier kernel scaledConvexApproxKernel ρ (ε r) is supported in the sup-metric ball closedBall 0 (ε r), and the convex smoothing evaluates the convolution at the contracted point (1-ε) • y + ε • x₀, within sup-distance (1-ε) r of x₀. The two contributions add to exactly r, so no inner/outer radius pair is needed; and the Euclidean ball is contained in the sup ball, so the HarmonicOnNhd conclusion holds on Metric.ball (toEuc x₀) r.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.isWeaklyHarmonicOn_test_of_contDiff {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUopen : IsOpen U) {u : HCPolySupport.H1Function U} (hu : Support.IsWeaklyHarmonicOn U u) {φ : HCPolySupport.Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_supp : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (u.grad x) (HCPolySupport.euclideanGradient φ x) = 0

Unpack weak harmonicity at a smooth compactly supported test function. The H¹₀ quantifier in IsWeaklyHarmonicOn is instantiated at Homogenization.H10Function.ofContDiff φ.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.isWeaklyHarmonicOn_integral_mul_euclideanCoordLaplacian_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUopen : IsOpen U) {u : HCPolySupport.H1Function U} (hu : Support.IsWeaklyHarmonicOn U u) {ψ : HCPolySupport.Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ_supp : HasCompactSupport ψ) (hψ_sub : tsupport ψ ⊆ U) : ∫ (x : HCPolySupport.Vec d) in U, u.toFun x * HCPolySupport.euclideanCoordLaplacian ψ x = 0

Weakly harmonic H¹ functions annihilate compactly supported Laplacian tests.

∫_U u · Δψ = 0 for smooth ψ with compact support inside U. This is the distributional (−Δu = 0) reading of the variational condition, and it is the form consumed by the convolution harmonicity argument.

Proof: for each coordinate i, the weak derivative identity of u applied to the test function ∂ᵢψ (still smooth, still compactly supported inside U) gives ∫_U u ∂ᵢ∂ᵢψ = -∫_U (∂ᵢu) (∂ᵢψ); summing over i turns the right-hand side into -∫_U ∇u · ∇ψ, which vanishes by weak harmonicity.

Support geometry of the scaled mollifier

The convolution harmonicity core

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.euclideanCoordLaplacian_convolution_indicator_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUopen : IsOpen U) {u : HCPolySupport.H1Function U} (hu : Support.IsWeaklyHarmonicOn U u) {K : HCPolySupport.Vec d → ℝ} (hK_supp : HasCompactSupport K) (hK : ContDiff ℝ (↑⊤) K) (A : HCPolySupport.Vec d) (hsub : (tsupport fun (y : HCPolySupport.Vec d) => K (A - y)) ⊆ U) : HCPolySupport.euclideanCoordLaplacian (MeasureTheory.convolution K (U.indicator u.toFun) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) A = 0

The mollified weakly harmonic function has vanishing Laplacian. If the reflected kernel y ↦ K (A - y) is supported inside U and u is weakly harmonic on U, then the coordinate Laplacian of the convolution K ⋆ (𝟙_U u) vanishes at A.

Proof: the Laplacian passes onto the kernel (euclideanCoordLaplacian_convolution_left); a change of variables (integral_mul_indicator_const_sub_eq_setIntegral) turns the resulting global integral into the pairing ∫_U u · Δψ with ψ y = K (A - y); and the point reflection leaves the Laplacian invariant (euclideanCoordLaplacian_comp_const_sub), so the pairing vanishes by IsWeaklyHarmonicOn.integral_mul_euclideanCoordLaplacian_eq_zero.

The CoarseGraining convex smoothing is harmonic on the ball

The L² approximation apex

MemLp bookkeeping for the smooth approximant on a bounded window

The apex on a supplied measurable window