Compactness Mollifier Test

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.memLp_reflected_mollifier_coordinate (m : ℕ) (x : Foundation.Parabolic.Vec3) (i : Fin 3) : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (Pi.single i (mollifier (sliceRadius m) ⋯ (x - y)))) 2 MeasureTheory.volume

A reflected mollifier in one coordinate is a compactly supported L² test for weak convergence of vector-valued spatial slices.

theorem CKN.Leray.mollify_component_eq_cutoff_inner (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (χ : Foundation.Parabolic.Vec3 → ℝ) (hf : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (f y)) 2 MeasureTheory.volume) (m : ℕ) (x : Foundation.Parabolic.Vec3) (i : Fin 3) (hχ : ∀ (y : Vec 3), mollifier (sliceRadius m) ⋯ (x - y) ≠ 0 → χ y = 1) : mollify (fun (y : Vec 3) => f y i) (sliceRadius m) ⋯ x = inner ℝ (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (f y)) hf) (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (Pi.single i (mollifier (sliceRadius m) ⋯ (x - y)))) ⋯)

On the support of a reflected mollifier, a cutoff equal to one leaves the spatial Hilbert pairing equal to mollification.