Solenoidal slices: mollified divergence and gradient trace

The mollification of a weakly divergence-free field is divergence free, and the trace of the weak gradient of a weakly divergence-free field vanishes (prop:lps-local-strong).

theorem ESS.LPS.lps_conv_div_free {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsWeakDivFreeL2 a) {η : CKN.Foundation.Parabolic.Vec3 → ℝ} (hη : CKN.IsVlKernel η) (x : CKN.Foundation.Parabolic.Vec3) : ∑ i : Fin 3, CKN.vlConv (CKN.vlDeriv η i) (fun (y : CKN.Foundation.Parabolic.Vec3) => a y i) x = 0

The mollification of a weakly divergence-free field is pointwise divergence free.

theorem ESS.LPS.lps_weak_gradient_trace_zero {w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hw : CKN.IsWeakDivFreeL2 w) (hDw : MeasureTheory.MemLp Dw 2 MeasureTheory.volume) (hgrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => w x i) fun (x : CKN.Vec 3) => Dw x i) : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, Dw x j j = 0

The trace of the weak gradient of a weakly divergence-free field vanishes almost everywhere.