Smooth approximation in L^{5/2} ∩ L² with support in positive times #
A space-time function in L^{5/2} ∩ L² vanishing at nonpositive times is the
limit, in both norms, of smooth compactly supported functions whose supports
stay in positive times: truncate to a bounded set at positive times, then
mollify at a scale below the time gap. This is the density step used to extend
the forced heat estimates of lem:pv-stokes to rough tensors.
theorem
ESS.tendsto_eLpNorm_truncation
{f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{p : ENNReal}
(hp0 : p ≠ 0)
(hptop : p ≠ ⊤)
(hf : MeasureTheory.MemLp f p MeasureTheory.volume)
(hsupp : ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), f z ≠ 0 → 0 < z.2)
:
Filter.Tendsto
(fun (k : ℕ) => MeasureTheory.eLpNorm ((positiveTimeTruncation k).indicator f - f) p MeasureTheory.volume)
Filter.atTop (nhds 0)
Truncating a function in L^p vanishing at nonpositive times to the bounded
positive-time sets converges in L^p.
theorem
ESS.exists_smooth_approx_two_norms
{f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(h52 : MeasureTheory.MemLp f (ENNReal.ofReal (5 / 2)) MeasureTheory.volume)
(h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hsupp : ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), f z ≠ 0 → 0 < z.2)
:
∃ (h : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
(∀ (n : ℕ), ContDiff ℝ (↑⊤) (h n)) ∧ (∀ (n : ℕ), HasCompactSupport (h n)) ∧ (∀ (n : ℕ), tsupport (h n) ⊆ {p : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < p.2}) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (h n - f) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume)
Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (h n - f) 2 MeasureTheory.volume) Filter.atTop (nhds 0)
A function in L^{5/2} ∩ L² vanishing at nonpositive times is a limit in both
norms of smooth compactly supported functions supported in positive times.