Translated mollifiers as spatial test functions

The slice form of a distributional identity is obtained by testing the space-time identity against the countable family of mollifier bumps centred at the points of a countable dense set. This file records the elementary properties of a single translated bump x ↦ mollifier ε (x - y): it is smooth, compactly supported with topological support the closed ball closedBall y ε, and its coordinate derivative is the translate of the coordinate derivative of the kernel.

theorem CKN.mollifier_eq_zero_of_lt_norm {d : ℕ} {ε : ℝ} (hε : 0 < ε) {z : Vec d} (hz : ε < ‖z‖) : mollifier ε hε z = 0

The mollifier vanishes outside its closed ball of radius ε.

theorem CKN.fderiv_mollifier_apply_eq_zero {d : ℕ} {ε : ℝ} (hε : 0 < ε) {z : Vec d} (hz : ε < ‖z‖) (i : Fin d) : (fderiv ℝ (mollifier ε hε) z) (basisVec i) = 0

Each coordinate derivative of the mollifier vanishes outside the closed ball of radius ε.

theorem CKN.continuous_fderiv_mollifier_apply {d : ℕ} {ε : ℝ} (hε : 0 < ε) (i : Fin d) : Continuous fun (z : Vec d) => (fderiv ℝ (mollifier ε hε) z) (basisVec i)

Each coordinate derivative of the mollifier is continuous.

theorem CKN.contDiff_mollifier_sub {d : ℕ} {ε : ℝ} (hε : 0 < ε) (y : Vec d) : ContDiff ℝ ↑⊤ fun (x : Vec d) => mollifier ε hε (x - y)

The translated mollifier is smooth.

theorem CKN.hasCompactSupport_mollifier_sub {d : ℕ} {ε : ℝ} (hε : 0 < ε) (y : Vec d) : HasCompactSupport fun (x : Vec d) => mollifier ε hε (x - y)

The translated mollifier has compact support.

theorem CKN.tsupport_mollifier_sub_eq {d : ℕ} {ε : ℝ} (hε : 0 < ε) (y : Vec d) : (tsupport fun (x : Vec d) => mollifier ε hε (x - y)) = Metric.closedBall y ε

The topological support of the translated mollifier is the closed ball of radius ε about the translation point.

theorem CKN.fderiv_mollifier_sub_apply {d : ℕ} {ε : ℝ} (hε : 0 < ε) (y x : Vec d) (i : Fin d) : (fderiv ℝ (fun (z : Vec d) => mollifier ε hε (z - y)) x) (basisVec i) = (fderiv ℝ (mollifier ε hε) (x - y)) (basisVec i)

The coordinate derivative of a translated mollifier is the translate of the coordinate derivative of the mollifier.