HarmonicMollifyKernel

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

A smooth radial mollifying density and the smoothness of its radial potential

HarmonicSphereProfile and HarmonicSphereBump build, for every continuous annulus-supported density k of vanishing radial moment, a compactly supported C^2 function psi on Vec (m + 1) with Delta psi = k (|. - z|). That regularity is exactly what Green's second identity needs, but it is one degree too weak for the distributional harmonicity predicate of HarmonicWeak, whose test class is C^infty. This module supplies the missing regularity and the concrete density that the mollification argument runs on:

• the radial potential of a smooth annulus-supported density is itself smooth (contDiff_radialPotential_comp_of_contDiff), because the radial moment gains one derivative from the fundamental theorem of calculus, the radial slope divides by t^m away from the origin, and the potential gains one more derivative; near the origin the profile is constant, which is what contDiff_radial needs;
• an explicit smooth density mollifierProfile m delta, supported in the annulus (delta/2, delta), nonnegative, and normalized so that its radial moment equals 1 at every radius >= delta.

The annulus support -- rather than a density concentrated at the origin -- is forced by the potential construction: a radial density must vanish near the centre for its potential to be smooth there. It costs nothing, because an annulus density is still an approximate identity as delta -> 0.

Portability

This file depends only on Mathlib and on CoarseGraining (Homogenization.*) and on other files of this same harmonic/oscillation layer. It mentions no object of the manuscript: no model, no cutoff, no shell, no corrector, no cube. It is intended to be portable into CoarseGraining by a single mechanical namespace rename.

Contents

• contDiff_radialMoment, contDiffOn_radialSlope, contDiffOn_radialPotential -- the regularity chain for a smooth density.
• contDiff_radialPotential_comp_of_contDiff -- the smooth radial potential.
• contDiff_comp_euclideanNorm_sub_of_contDiff, tsupport_comp_euclideanNorm_sub_subset, hasCompactSupport_comp_euclideanNorm_sub -- a smooth annulus density read as a smooth compactly supported function on Vec (m + 1).
• unitAnnulusBump, annulusProfile, mollifierProfile -- the explicit density family, with radialMoment_mollifierProfile_of_le normalizing it.

References

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

Regularity of the radial potential of a smooth density

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_radialMoment {m : ℕ} {k : ℝ → ℝ} (hk : ContDiff ℝ (↑⊤) k) : ContDiff ℝ (↑⊤) (radialMoment m k)

The radial moment of a smooth density is smooth: it is an antiderivative of t ↦ t^m * k t.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiffOn_radialSlope {m : ℕ} {k : ℝ → ℝ} (hk : ContDiff ℝ (↑⊤) k) : ContDiffOn ℝ (↑⊤) (radialSlope m k) (Set.Ioi 0)

The radial slope of a smooth density is smooth away from the origin.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiffOn_radialPotential {m : ℕ} {k : ℝ → ℝ} {a : ℝ} (hk : ContDiff ℝ (↑⊤) k) (ha : 0 < a) (hk0 : ∀ s ≤ a, k s = 0) (b : ℝ) : ContDiffOn ℝ (↑⊤) (radialPotential m k b) (Set.Ioi 0)

The radial potential of a smooth annulus-supported density is smooth away from the origin.

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

The smooth radial potential. For a smooth density supported in an annulus [a, b] with a > 0, the radial potential composed with the Euclidean gauge is smooth on all of Vec (m + 1), centre included: it is constant on the ball of radius a.

A smooth annulus density as a function on the carrier

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

A smooth density vanishing near the origin is smooth as a radial function on Vec (m + 1).

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

A density vanishing outside [0, b] gives a radial function supported in the closed Euclidean ball of radius b.

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

The radial function attached to a density vanishing outside [0, b] has compact support.

The explicit smooth annulus density

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.unitAnnulusBumpData : ContDiffBump (3 / 4)

Bump data on the line: inner radius 1/8, outer radius 1/4, centre 3/4.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.unitAnnulusBump : ℝ → ℝ

The reference smooth bump on the line, supported in the annulus (1/2, 1) and equal to 1 on [5/8, 7/8].

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.Corrector.unitAnnulusBump = ↑Algsuperdiff.Section3.Provider.Diffusivity.Corrector.unitAnnulusBumpData

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_unitAnnulusBump : ContDiff ℝ (↑⊤) unitAnnulusBump

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.unitAnnulusBump_nonneg (t : ℝ) : 0 ≤ unitAnnulusBump t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.support_unitAnnulusBump : Function.support unitAnnulusBump = Set.Ioo (1 / 2) 1

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.unitAnnulusBump_eq_zero_of_le {t : ℝ} (ht : t ≤ 1 / 2) : unitAnnulusBump t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.unitAnnulusBump_eq_zero_of_ge {t : ℝ} (ht : 1 ≤ t) : unitAnnulusBump t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.unitAnnulusBump_eq_one {t : ℝ} (h1 : 5 / 8 ≤ t) (h2 : t ≤ 7 / 8) : unitAnnulusBump t = 1

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusProfile (δ : ℝ) : ℝ → ℝ

The smooth annulus density at scale δ, supported in (δ/2, δ).

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusProfile δ t = Algsuperdiff.Section3.Provider.Diffusivity.Corrector.unitAnnulusBump (t / δ)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_annulusProfile (δ : ℝ) : ContDiff ℝ (↑⊤) (annulusProfile δ)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_annulusProfile (δ : ℝ) : Continuous (annulusProfile δ)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusProfile_nonneg (δ t : ℝ) : 0 ≤ annulusProfile δ t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusProfile_eq_zero_of_le {δ : ℝ} (hδ : 0 < δ) {t : ℝ} (ht : t ≤ δ / 2) : annulusProfile δ t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusProfile_eq_zero_of_ge {δ : ℝ} (hδ : 0 < δ) {t : ℝ} (ht : δ ≤ t) : annulusProfile δ t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.annulusProfile_eq_one {δ : ℝ} (hδ : 0 < δ) {t : ℝ} (h1 : 5 * δ / 8 ≤ t) (h2 : t ≤ 7 * δ / 8) : annulusProfile δ t = 1

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment_annulusProfile_pos (m : ℕ) {δ : ℝ} (hδ : 0 < δ) : 0 < radialMoment m (annulusProfile δ) δ

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment_sub {m : ℕ} {k₁ k₂ : ℝ → ℝ} (hk₁ : Continuous k₁) (hk₂ : Continuous k₂) (t : ℝ) : radialMoment m (fun (s : ℝ) => k₁ s - k₂ s) t = radialMoment m k₁ t - radialMoment m k₂ t

Radial moments are additive, hence subtractive.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollifierProfile (m : ℕ) (δ : ℝ) : ℝ → ℝ

The normalized smooth radial density at scale δ. It is smooth, nonnegative, supported in the annulus (δ/2, δ), and has radial moment 1.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_mollifierProfile (m : ℕ) (δ : ℝ) : ContDiff ℝ (↑⊤) (mollifierProfile m δ)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_mollifierProfile (m : ℕ) (δ : ℝ) : Continuous (mollifierProfile m δ)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollifierProfile_nonneg {m : ℕ} {δ : ℝ} (hδ : 0 < δ) (t : ℝ) : 0 ≤ mollifierProfile m δ t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollifierProfile_eq_zero_of_le {m : ℕ} {δ : ℝ} (hδ : 0 < δ) {t : ℝ} (ht : t ≤ δ / 2) : mollifierProfile m δ t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollifierProfile_eq_zero_of_ge {m : ℕ} {δ : ℝ} (hδ : 0 < δ) {t : ℝ} (ht : δ ≤ t) : mollifierProfile m δ t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mollifierProfile_pos_of_mem {m : ℕ} {δ : ℝ} (hδ : 0 < δ) {t : ℝ} (h1 : 5 * δ / 8 < t) (h2 : t < 7 * δ / 8) : 0 < mollifierProfile m δ t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment_mollifierProfile (m : ℕ) {δ : ℝ} (hδ : 0 < δ) : radialMoment m (mollifierProfile m δ) δ = 1

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.radialMoment_mollifierProfile_of_le (m : ℕ) {δ b : ℝ} (hδ : 0 < δ) (hb : δ ≤ b) : radialMoment m (mollifierProfile m δ) b = 1

The normalization is stable at every radius beyond the support.