Compactness Mollifier Lp

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.mollify_lp_component_eq_inner (V : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (m : ℕ) (x : Foundation.Parabolic.Vec3) (i : Fin 3) : mollify (fun (y : Foundation.Parabolic.Vec3) => (↑↑V y).ofLp i) (sliceRadius m) ⋯ x = inner ℝ V (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (Pi.single i (mollifier (sliceRadius m) ⋯ (x - y)))) ⋯)

Mollifying a coordinate of a spatial L² function is the Hilbert pairing with the corresponding reflected mollifier test.