From a countable family of mollifier bumps to every test function

A distributional identity that is only known against a countable family of test functions can be upgraded to all test functions when the family is rich enough. The family used here is the family of mollifier bumps x ↦ mollifier (sliceRadius n) (x - y) centred at the points y of a dense set. The upgrade has three steps.

• The pairing of a locally integrable field with a translated bump depends continuously on the centre, so vanishing on a dense set of centres gives vanishing at every admissible centre.
• Integrating the resulting identity against a test function ψ and exchanging the order of integration replaces the bump by the mollification of the transform of ψ that appears in the pairing.
• Letting the radius tend to zero recovers that transform itself.

The argument is carried out once, for an abstract kernel family κ and an abstract transform T of the test function, and then specialised to the two pairings used in paper/ckn.tex: the spatial divergence pairing ∑ᵢ gᵢ ∂ᵢψ and the plain multiplication pairing F ψ. This is the mechanism behind the almost-everywhere slice identities there: the null set produced by testing one test function at a time is replaced by a single null set valid for every test function.

noncomputable def CKN.sliceMollifierDeriv {d : ℕ} (n : ℕ) (i : Fin d) : Vec d → ℝ

The ith coordinate derivative of the mollifier of radius sliceRadius n.

Equations

• CKN.sliceMollifierDeriv n i z = (fderiv ℝ (CKN.mollifier (CKN.sliceRadius n) ⋯) z) (CKN.basisVec i)

theorem CKN.slice_pairing_zero_of_mollifier_family {d : ℕ} {ι : Type u_1} [Fintype ι] {Ω : Set (Vec d)} (hΩ : IsOpen Ω) {Q : Set (Vec d)} (hQ : Dense Q) {g : Vec d → ι → ℝ} (hg : ∀ (i : ι), MeasureTheory.LocallyIntegrableOn (fun (x : Vec d) => g x i) Ω MeasureTheory.volume) {κ : ℕ → ι → Vec d → ℝ} (hκcont : ∀ (n : ℕ) (i : ι), Continuous (κ n i)) (hκzero : ∀ (n : ℕ) (i : ι) (z : Vec d), sliceRadius n < ‖z‖ → κ n i z = 0) {ψ : Vec d → ℝ} (hψcont : Continuous ψ) (hψc : HasCompactSupport ψ) (hψΩ : tsupport ψ ⊆ Ω) {T : ι → Vec d → ℝ} (hTcont : ∀ (i : ι), Continuous (T i)) (hTsupp : ∀ (i : ι), ∀ x ∉ tsupport ψ, T i x = 0) (hid : ∀ (n : ℕ) (i : ι) (x : Vec d), ∫ (y : Vec d), ψ y * κ n i (x - y) = mollify (T i) (sliceRadius n) ⋯ x) (hzero : ∀ y ∈ Q, ∀ (n : ℕ), Metric.closedBall y (sliceRadius n) ⊆ Ω → ∫ (x : Vec d) in Ω, ∑ i : ι, g x i * κ n i (x - y) = 0) : ∫ (x : Vec d) in Ω, ∑ i : ι, g x i * T i x = 0

The general mollifier-bump family upgrade. The pairing of a field g that is locally integrable on an open set Ω against the kernels κ n i centred at the points of a dense set Q determines the pairing against any transform T of a compactly supported test function ψ, provided the two are linked by the mollification identity hid.

theorem CKN.slice_divergence_zero_of_mollifier_family {d : ℕ} {Ω : Set (Vec d)} (hΩ : IsOpen Ω) {Q : Set (Vec d)} (hQ : Dense Q) {g : Vec d → Fin d → ℝ} (hg : ∀ (i : Fin d), MeasureTheory.LocallyIntegrableOn (fun (x : Vec d) => g x i) Ω MeasureTheory.volume) (hzero : ∀ y ∈ Q, ∀ (n : ℕ), Metric.closedBall y (sliceRadius n) ⊆ Ω → ∫ (x : Vec d) in Ω, ∑ i : Fin d, g x i * (fderiv ℝ (fun (z : Vec d) => mollifier (sliceRadius n) ⋯ (z - y)) x) (basisVec i) = 0) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψΩ : tsupport ψ ⊆ Ω) : ∫ (x : Vec d) in Ω, ∑ i : Fin d, g x i * (fderiv ℝ ψ x) (basisVec i) = 0

The divergence instance of the mollifier-bump family upgrade. If the distributional divergence pairing of a field g that is locally integrable on an open set Ω vanishes against every mollifier bump centred at a point of a dense set Q and small enough to fit inside Ω, then it vanishes against every smooth compactly supported test function supported in Ω.

theorem CKN.slice_integral_mul_zero_of_mollifier_family {d : ℕ} {Ω : Set (Vec d)} (hΩ : IsOpen Ω) {Q : Set (Vec d)} (hQ : Dense Q) {F : Vec d → ℝ} (hF : MeasureTheory.LocallyIntegrableOn F Ω MeasureTheory.volume) (hzero : ∀ y ∈ Q, ∀ (n : ℕ), Metric.closedBall y (sliceRadius n) ⊆ Ω → ∫ (x : Vec d) in Ω, F x * mollifier (sliceRadius n) ⋯ (x - y) = 0) {ψ : Vec d → ℝ} (hψcont : Continuous ψ) (hψc : HasCompactSupport ψ) (hψΩ : tsupport ψ ⊆ Ω) : ∫ (x : Vec d) in Ω, F x * ψ x = 0

The multiplication instance of the mollifier-bump family upgrade. If the integral of a function F that is locally integrable on an open set Ω against every small mollifier bump centred at a point of a dense set Q vanishes, then ∫ F ψ vanishes for every continuous compactly supported ψ supported in Ω.