HarmonicSphereBump

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

The radial test bump: a compactly supported C^2 solution of Delta psi = k

Combining the radial Laplacian of HarmonicSphereRadial with the profile of HarmonicSphereProfile gives, for every continuous annulus-supported density k of vanishing radial moment, a compactly supported C^2 function on Vec (m + 1) whose coordinate Laplacian is exactly x ↦ k (|x - z|).

This is the test function that the Green pairing of HarmonicGreen will be run against. Its existence is the whole content of the classical statement that a radial density of vanishing mean is a Laplacian; the annulus support is what makes the construction elementary, because the profile is then constant near the origin and the Euclidean gauge is smooth on the support of the density.

Contents

• euclideanCoordLaplacian_radialPotential -- Delta psi = k (|· - z|) at every point of the carrier, including the centre.
• contDiff_radialPotential_comp -- psi is C^2.
• tsupport_radialPotential_comp_subset, hasCompactSupport_radialPotential_comp -- psi is supported in the closed Euclidean ball of radius b.

References

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanCoordLaplacian_radialPotential {m : ℕ} {k : ℝ → ℝ} {a b : ℝ} (hk : Continuous k) (ha : 0 < a) (hk0 : ∀ s ≤ a, k s = 0) (z x : HCPolySupport.Vec (m + 1)) : HCPolySupport.euclideanCoordLaplacian (fun (w : HCPolySupport.Vec (m + 1)) => radialPotential m k b (euclideanNorm (w - z))) x = k (euclideanNorm (x - z))

The radial potential solves the radial Laplace equation with right-hand side k in dimension m + 1, at every point of the carrier.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_radialPotential_comp {m : ℕ} {k : ℝ → ℝ} {a : ℝ} (hk : Continuous k) (ha : 0 < a) (hk0 : ∀ s ≤ a, k s = 0) (b : ℝ) (z : HCPolySupport.Vec (m + 1)) : ContDiff ℝ ↑2 fun (w : HCPolySupport.Vec (m + 1)) => radialPotential m k b (euclideanNorm (w - z))

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.tsupport_radialPotential_comp_subset {m : ℕ} {k : ℝ → ℝ} {b : ℝ} (hk : Continuous k) (hb : 0 < b) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) (hmom : radialMoment m k b = 0) (z : HCPolySupport.Vec (m + 1)) : (tsupport fun (w : HCPolySupport.Vec (m + 1)) => radialPotential m k b (euclideanNorm (w - z))) ⊆ HCPolySupport.euclideanClosedBall z b

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasCompactSupport_radialPotential_comp {m : ℕ} {k : ℝ → ℝ} {b : ℝ} (hk : Continuous k) (hb : 0 < b) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) (hmom : radialMoment m k b = 0) (z : HCPolySupport.Vec (m + 1)) : HasCompactSupport fun (w : HCPolySupport.Vec (m + 1)) => radialPotential m k b (euclideanNorm (w - z))