The physical regularization kernel

The scalar kernel induced by the regularized equation's profile is smooth, compactly supported, nonnegative and has unit mass. These properties instantiate the ordered Sobolev contraction estimate in eq:lps-Hm-energy.

theorem ESS.lps_regUniformMollifierKernel_properties (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : ContDiff ℝ (↑⊤) (CKN.Leray.regUniformMollifierKernel ρ ε hε) ∧ HasCompactSupport (CKN.Leray.regUniformMollifierKernel ρ ε hε) ∧ (∀ (x : CKN.Foundation.Parabolic.Vec3), 0 ≤ CKN.Leray.regUniformMollifierKernel ρ ε hε x) ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Leray.regUniformMollifierKernel ρ ε hε x = 1

The physical scalar regularization kernel has the smoothness, support and normalization required for H^m contraction (eq:lps-Hm-energy).