HarmonicSphereRadial

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

The radial Laplacian on the sup-normed carrier

Mathlib states the Laplacian only on an inner product space, and its harmonic layer (Analysis/InnerProductSpace/Harmonic/*) is therefore unavailable on Vec d, which carries no InnerProductSpace R instance at all. CoarseGraining's euclideanCoordLaplacian u x = sum_i d_i d_i u x is the carrier-native replacement, and this module computes it on a radial function w ↦ Phi (|w - z|), |·| the Euclidean gauge of HarmonicSphereNorm:

  Delta (Phi ∘ |· - z|) (x) = Phi'' (|x - z|) + (d - 1) * Phi' (|x - z|) / |x - z|

for x ≠ z, together with the smoothness statement that a radial function whose profile is constant near the origin is C^n on the whole carrier -- including at the centre, where the Euclidean gauge itself is not differentiable.

The proof is the elementary two-fold chain rule of HarmonicSphereNorm summed over the d coordinate directions; the identity sum_i (x i - z i)^2 = |x - z|^2 is what produces the dimensional coefficient.

Contents

• contDiff_vecNormSq, contDiffAt_euclideanNorm_sub -- smoothness of the Euclidean gauge away from its centre.
• euclideanCoordLaplacian_eq_zero_of_locally_const -- a function that is constant on a neighbourhood has vanishing coordinate Laplacian there.
• mem_euclideanBall_self, contDiff_radial -- smoothness of a radial function with a profile that is constant near the origin.
• euclideanCoordSecondDeriv_radial -- the single-direction second derivative.
• euclideanCoordLaplacian_radial -- the radial Laplacian.

References

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_vecNormSq {d : ℕ} {n : WithTop ℕ∞} : ContDiff ℝ n HCPolySupport.vecNormSq

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiffAt_euclideanNorm_sub {d : ℕ} {z x : HCPolySupport.Vec d} {n : WithTop ℕ∞} (hx : x ≠ z) : ContDiffAt ℝ n (fun (w : HCPolySupport.Vec d) => euclideanNorm (w - z)) x

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanCoordLaplacian_eq_zero_of_locally_const {d : ℕ} {f : HCPolySupport.Vec d → ℝ} {c : ℝ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {x : HCPolySupport.Vec d} (hx : x ∈ U) (hf : ∀ y ∈ U, f y = c) : HCPolySupport.euclideanCoordLaplacian f x = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mem_euclideanBall_self {d : ℕ} {z : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) : z ∈ HCPolySupport.euclideanBall z r

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_radial {d : ℕ} {Φ : ℝ → ℝ} {z : HCPolySupport.Vec d} {n : WithTop ℕ∞} {a : ℝ} (ha : 0 < a) (hsmooth : ∀ (t : ℝ), 0 < t → ContDiffAt ℝ n Φ t) (hconst : ∀ (t : ℝ), 0 ≤ t → t < a → Φ t = Φ 0) : ContDiff ℝ n fun (w : HCPolySupport.Vec d) => Φ (euclideanNorm (w - z))

A radial function whose profile is constant near the origin and smooth away from it is smooth on the whole carrier.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanCoordSecondDeriv_radial {d : ℕ} {Φ Φ' Φ'' : ℝ → ℝ} {z x : HCPolySupport.Vec d} (h1 : ∀ (t : ℝ), 0 < t → HasDerivAt Φ (Φ' t) t) (h2 : ∀ (t : ℝ), 0 < t → HasDerivAt Φ' (Φ'' t) t) (hx : x ≠ z) (i : Fin d) : HCPolySupport.euclideanCoordSecondDeriv i i (fun (w : HCPolySupport.Vec d) => Φ (euclideanNorm (w - z))) x = Φ'' (euclideanNorm (x - z)) * (x i - z i) ^ 2 / euclideanNorm (x - z) ^ 2 + Φ' (euclideanNorm (x - z)) / euclideanNorm (x - z) - Φ' (euclideanNorm (x - z)) * (x i - z i) ^ 2 / euclideanNorm (x - z) ^ 3

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanCoordLaplacian_radial {d : ℕ} {Φ Φ' Φ'' : ℝ → ℝ} {z x : HCPolySupport.Vec d} (h1 : ∀ (t : ℝ), 0 < t → HasDerivAt Φ (Φ' t) t) (h2 : ∀ (t : ℝ), 0 < t → HasDerivAt Φ' (Φ'' t) t) (hx : x ≠ z) : HCPolySupport.euclideanCoordLaplacian (fun (w : HCPolySupport.Vec d) => Φ (euclideanNorm (w - z))) x = Φ'' (euclideanNorm (x - z)) + (↑d - 1) * Φ' (euclideanNorm (x - z)) / euclideanNorm (x - z)