Spatial mollification at the L∞ endpoint #
Positive, unit-mass spatial mollification preserves an almost-everywhere
spatial bound. This is the endpoint domination used for the convection
density limit (lem:lps-comparison).
theorem
ESS.lps_endpoint_mollify_linf_bound
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
{ε M : ℝ}
(hε : 0 < ε)
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(hfBound : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), |f x| ≤ M)
(y : CKN.Foundation.Parabolic.Vec3)
:
A normalized nonnegative spatial mollifier does not increase an
almost-everywhere scalar L∞ bound.