HarmonicSphereProfile

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

The radial profile that solves the radial Laplace equation

Given a continuous radial density k supported in an annulus [a, b] with 0 < a < b, the ordinary differential equation Psi'' + m * Psi' / t = k in dimension d = m + 1 is solved in closed form by

  Q t = int_0^t s^m k s ds ,   P t = Q t / t^m ,   Psi t = int_b^t P s ds .

Q vanishes below a, so P and hence Psi' vanish there and Psi is constant near the origin; and if the radial moment Q b vanishes, then P vanishes above b as well and Psi vanishes identically above b. The resulting profile is therefore constant near 0, compactly supported, and C^2 on (0, ∞) -- exactly the input that the radial Laplacian of HarmonicSphereRadial and the Green pairing of HarmonicGreen consume.

This module builds the three functions and proves their derivative, support and regularity properties. Nothing here is about harmonic functions.

Contents

• radialMoment, radialSlope, radialPotential -- the three functions.
• hasDerivAt_radialMoment, hasDerivAt_radialSlope, hasDerivAt_radialPotential -- their derivatives, the middle one being the explicit P' t = k t - m * Q t / t^(m+1).
• radialMoment_eq_zero_of_le, radialMoment_eq_of_ge, radialSlope_eq_zero_of_le, radialSlope_eq_zero_of_ge, radialPotential_eq_zero_of_ge, radialPotential_eq_of_le -- the support and constancy statements.
• continuous_radialSlope, contDiffAt_radialPotential -- regularity.

References

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment (m : ℕ) (k : ℝ → ℝ) (t : ℝ) : ℝ

The weighted radial integral defining the harmonic-sphere profile.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment m k t = ∫ (s : ℝ) in 0..t, s ^ m * k s

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialSlope (m : ℕ) (k : ℝ → ℝ) (t : ℝ) : ℝ

The radial derivative determined by the moment.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialSlope m k t = Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment m k t / t ^ m

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialPotential (m : ℕ) (k : ℝ → ℝ) (b t : ℝ) : ℝ

The radial primitive normalized to vanish at radius b.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialPotential m k b t = ∫ (s : ℝ) in b..t, Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialSlope m k s

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasDerivAt_radialMoment {m : ℕ} {k : ℝ → ℝ} (hk : Continuous k) (t : ℝ) : HasDerivAt (radialMoment m k) (t ^ m * k t) t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_radialMoment {m : ℕ} {k : ℝ → ℝ} (hk : Continuous k) : Continuous (radialMoment m k)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment_eq_zero_of_le {m : ℕ} {k : ℝ → ℝ} {a : ℝ} (ha : 0 ≤ a) (hk0 : ∀ s ≤ a, k s = 0) {t : ℝ} (ht : t ≤ a) : radialMoment m k t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment_eq_of_ge {m : ℕ} {k : ℝ → ℝ} {b : ℝ} (hk : Continuous k) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) {t : ℝ} (ht : b ≤ t) : radialMoment m k t = radialMoment m k b

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialSlope_eq_zero_of_le {m : ℕ} {k : ℝ → ℝ} {a : ℝ} (ha : 0 ≤ a) (hk0 : ∀ s ≤ a, k s = 0) {t : ℝ} (ht : t ≤ a) : radialSlope m k t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialSlope_eq_zero_of_ge {m : ℕ} {k : ℝ → ℝ} {b : ℝ} (hk : Continuous k) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) (hmom : radialMoment m k b = 0) {t : ℝ} (ht : b ≤ t) : radialSlope m k t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_radialSlope {m : ℕ} {k : ℝ → ℝ} {a : ℝ} (hk : Continuous k) (ha : 0 < a) (hk0 : ∀ s ≤ a, k s = 0) : Continuous (radialSlope m k)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasDerivAt_radialSlope {m : ℕ} {k : ℝ → ℝ} (hk : Continuous k) {t : ℝ} (ht : 0 < t) : HasDerivAt (radialSlope m k) (k t - ↑m * radialMoment m k t / t ^ (m + 1)) t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasDerivAt_radialPotential {m : ℕ} {k : ℝ → ℝ} {a : ℝ} (hk : Continuous k) (ha : 0 < a) (hk0 : ∀ s ≤ a, k s = 0) (b t : ℝ) : HasDerivAt (radialPotential m k b) (radialSlope m k t) t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialPotential_eq_zero_of_ge {m : ℕ} {k : ℝ → ℝ} {b : ℝ} (hk : Continuous k) (hkb : ∀ (s : ℝ), b ≤ s → k s = 0) (hmom : radialMoment m k b = 0) {t : ℝ} (ht : b ≤ t) : radialPotential m k b t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialPotential_eq_of_le {m : ℕ} {k : ℝ → ℝ} {a b : ℝ} (hk : Continuous k) (ha : 0 < a) (hk0 : ∀ s ≤ a, k s = 0) {t : ℝ} (ht : t ≤ a) : radialPotential m k b t = radialPotential m k b 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiffAt_radialPotential {m : ℕ} {k : ℝ → ℝ} {a : ℝ} (hk : Continuous k) (ha : 0 < a) (hk0 : ∀ s ≤ a, k s = 0) (b : ℝ) {t : ℝ} (ht : 0 < t) : ContDiffAt ℝ 2 (radialPotential m k b) t